Skip to content

GitLab

Commit 20683e2d authored by Kučera Petr RNDr. Ph.D.'s avatar Kučera Petr RNDr. Ph.D.
Browse files

encode_bitvecotr_gt, passing by reference

parent e1edbb95
Hide whitespace changes
Inline Side-by-side
lib/up_levels.cpp
View file @ 20683e2d
......@@ -10,8 +10,7 @@
#include "up_levels.h"
SUBool::UPLevels::UPLevels(const CNF &cnf, VarStore &var_store,
bool literal_levels, unsigned level_bound,
const std::string &name_base)
bool literal_levels, unsigned level_bound, const std::string &name_base)
: mCnf(cnf), mVarStore(var_store), mLiteralLevels(literal_levels),
mLevelBound(level_bound), mLevelVars(), mNameBase(name_base),
mMaxVariable(0)
......@@ -72,13 +71,12 @@ SUBool::UPLevels::AddVariable()
unsigned
SUBool::UPLevels::EncodeGT(const Literal &left, const Literal &right,
std::vector<Clause> *clauses) const
std::vector<Clause> *clauses) const
{
// auto max_var = mVarStore.LastVariable();
// auto clauses_size = clauses->size();
return encode_bitvector_gt(LevelVars(left), LevelVars(right), mVarStore,
clauses, mNameBase + "g", left.ToString(),
right.ToString());
clauses, mNameBase + "g", left.ToString(), right.ToString());
// std::cout << "comparison size: " << mVarStore.LastVariable() - max_var <<
// " "
//<< clauses->size() - clauses_size << std::endl;
......@@ -92,9 +90,8 @@ SUBool::UPLevels::MaxVariable() const
unsigned
SUBool::new_aux_comparison_var(const std::string &name_base,
const std::string &left_desc,
const std::string &right_desc, unsigned bit,
VarStore &var_store)
const std::string &left_desc, const std::string &right_desc, unsigned bit,
VarStore &var_store)
{
var_store.NameStream() << name_base << "_{" << left_desc << ", "
<< right_desc << "}^{" << bit << "}";
......@@ -102,17 +99,15 @@ SUBool::new_aux_comparison_var(const std::string &name_base,
}
unsigned
SUBool::encode_bitvector_gt(const std::vector<unsigned> left_bv,
const std::vector<unsigned> right_bv,
VarStore &var_store, std::vector<Clause> *clauses,
const std::string &name_base,
const std::string &left_desc,
const std::string &right_desc)
SUBool::encode_bitvector_gt(const std::vector<unsigned> &left_bv,
const std::vector<unsigned> &right_bv, VarStore &var_store,
std::vector<Clause> *clauses, const std::string &name_base,
const std::string &left_desc, const std::string &right_desc)
{
if (clauses == nullptr)
{
throw NullPointerException("UPEncLogarithmic::AddLevelGT",
"clauses == nullptr");
throw NullPointerException(
"UPEncLogarithmic::AddLevelGT", "clauses == nullptr");
}
if (left_bv.size() == 0)
{
......@@ -126,27 +121,27 @@ SUBool::encode_bitvector_gt(const std::vector<unsigned> left_bv,
/* XXX */
// The opposite implication for G var in comparison.
clauses->emplace_back(Literal(g, true), Literal(left_bv[b], false),
Literal(right_bv[b], true));
Literal(right_bv[b], true));
/* */
while (b > 0)
{
--b;
unsigned ng = new_aux_comparison_var(name_base, left_desc, right_desc, b,
var_store);
unsigned ng = new_aux_comparison_var(
name_base, left_desc, right_desc, b, var_store);
clauses->emplace_back(Literal(ng, false), Literal(left_bv[b], true),
Literal(right_bv[b], false));
clauses->emplace_back(Literal(ng, false), Literal(left_bv[b], true),
Literal(g, true));
clauses->emplace_back(Literal(ng, false), Literal(right_bv[b], false),
Literal(g, true));
Literal(right_bv[b], false));
clauses->emplace_back(
Literal(ng, false), Literal(left_bv[b], true), Literal(g, true));
clauses->emplace_back(
Literal(ng, false), Literal(right_bv[b], false), Literal(g, true));
/* XXX */
// The opposite implications for G var in comparison.
clauses->emplace_back(Literal(ng, true), Literal(left_bv[b], false),
Literal(right_bv[b], true));
clauses->emplace_back(Literal(ng, true), Literal(left_bv[b], false),
Literal(g, false));
clauses->emplace_back(Literal(ng, true), Literal(right_bv[b], true),
Literal(g, false));
Literal(right_bv[b], true));
clauses->emplace_back(
Literal(ng, true), Literal(left_bv[b], false), Literal(g, false));
clauses->emplace_back(
Literal(ng, true), Literal(right_bv[b], true), Literal(g, false));
/* */
g = ng;
}
......@@ -154,8 +149,8 @@ SUBool::encode_bitvector_gt(const std::vector<unsigned> left_bv,
}
SUBool::NFSize
SUBool::UPLevels::CountInitialSize(const CNF &cnf, bool literal_levels,
unsigned level_bound)
SUBool::UPLevels::CountInitialSize(
const CNF &cnf, bool literal_levels, unsigned level_bound)
{
return CountAddVariable(literal_levels, level_bound) * cnf.MaxVariable();
}
......@@ -168,12 +163,12 @@ SUBool::UPLevels::CountAddVariable(bool literal_levels, unsigned level_bound)
}
SUBool::NFSize
SUBool::UPLevels::CountEncodeGTSize(bool /*literal_levels*/,
unsigned level_bound)
SUBool::UPLevels::CountEncodeGTSize(
bool /*literal_levels*/, unsigned level_bound)
{
// std::cout << "est comparison size: " << level_bound << " "
//<< 3 + 6 * (level_bound - 1) << std::endl;
return {/*.max_variable = */ level_bound,
/*.size = */ 3 + 6 * (level_bound - 1),
/*.len = */ 7 + 18 * (level_bound - 1)};
/*.size = */ 3 + 6 * (level_bound - 1),
/*.len = */ 7 + 18 * (level_bound - 1)};
}
lib/up_levels.h
View file @ 20683e2d
......@@ -17,16 +17,12 @@ namespace SUBool
{
unsigned new_aux_comparison_var(const std::string &name_base,
const std::string &left_desc,
const std::string &right_desc, unsigned bit,
VarStore &var_store);
unsigned encode_bitvector_gt(const std::vector<unsigned> left_bv,
const std::vector<unsigned> right_bv,
VarStore &var_store,
std::vector<Clause> *clauses,
const std::string &name_base,
const std::string &left_desc,
const std::string &right_desc);
const std::string &left_desc, const std::string &right_desc,
unsigned bit, VarStore &var_store);
unsigned encode_bitvector_gt(const std::vector<unsigned> &left_bv,
const std::vector<unsigned> &right_bv, VarStore &var_store,
std::vector<Clause> *clauses, const std::string &name_base,
const std::string &left_desc, const std::string &right_desc);
class UPLevels
{
......@@ -42,13 +38,13 @@ namespace SUBool
public:
UPLevels(const CNF &cnf, VarStore &var_store, bool literal_levels,
unsigned level_bound, const std::string &name_base);
unsigned level_bound, const std::string &name_base);
const std::vector<unsigned> &LevelVars(unsigned var) const;
const std::vector<unsigned> &LevelVars(const Literal &lit) const;
void AddVariable();
unsigned EncodeGT(const Literal &left, const Literal &right,
std::vector<Clause> *clauses) const;
std::vector<Clause> *clauses) const;
unsigned MaxVariable() const;
unsigned
LevelBound() const
......@@ -61,11 +57,11 @@ namespace SUBool
return mLevelBound;
}
static NFSize CountInitialSize(const CNF &cnf, bool literal_levels,
unsigned level_bound);
static NFSize CountInitialSize(
const CNF &cnf, bool literal_levels, unsigned level_bound);
static NFSize CountAddVariable(bool literal_levels, unsigned level_bound);
static NFSize CountEncodeGTSize(bool literal_levels,
unsigned level_bound);
static NFSize CountEncodeGTSize(
bool literal_levels, unsigned level_bound);
};
}; // namespace SUBool
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment