39 lits.push_back(
neg(a));
40 lits.push_back(
neg(b));
41 lits.push_back(
pos(o));
166 return land(bv[0], bv[1]);
168 for(
const auto &l : bv)
179 lits[1]=
neg(literal);
181 for(
const auto &l : new_bv)
188 lits.reserve(new_bv.size()+1);
190 for(
const auto &l : new_bv)
191 lits.push_back(
neg(l));
193 lits.push_back(
pos(literal));
209 return lor(bv[0], bv[1]);
211 for(
const auto &l : bv)
222 lits[1]=
pos(literal);
224 for(
const auto &l : new_bv)
231 lits.reserve(new_bv.size()+1);
233 for(
const auto &l : new_bv)
234 lits.push_back(
pos(l));
236 lits.push_back(
neg(literal));
252 return lxor(bv[0], bv[1]);
256 for(
const auto &l : bv)
257 literal=
lxor(l, literal);
349 return a.
sign() ? b : c;
371 #ifdef OPTIMAL_COMPACT_ITE
400 result.reserve(width);
403 result.emplace_back(i,
false);
416 std::sort(dest.begin(), dest.end());
417 auto last = std::unique(dest.begin(), dest.end());
418 dest.erase(last, dest.end());
435 for(
const auto &l : bv)
438 INVARIANT(l.var_no() != 0,
"variable 0 must not be used");
443 "variable 'unused_var_no' must not be used");
459 dest.reserve(bv.size());
461 for(
const auto &l : bv)
470 std::sort(dest.begin(), dest.end());
477 bvt::iterator it=dest.begin();
489 else if(previous==!l)
static bool is_all(const bvt &bv, literalt l)
void gate_equal(literalt a, literalt b, literalt o)
Tseitin encoding of equality between two literals.
bool process_clause(const bvt &bv, bvt &dest) const
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
bvt new_variables(std::size_t width) override
Generate a vector of new variables.
void gate_or(literalt a, literalt b, literalt o)
Tseitin encoding of disjunction of two literals.
virtual literalt limplies(literalt a, literalt b) override
virtual literalt lselect(literalt a, literalt b, literalt c) override
virtual void set_no_variables(size_t no)
static bvt eliminate_duplicates(const bvt &)
eliminate duplicates from given vector of literals
void gate_nand(literalt a, literalt b, literalt o)
Tseitin encoding of NAND of two literals.
virtual literalt new_variable() override
Generate a new variable and return it as a literal.
void gate_xor(literalt a, literalt b, literalt o)
Tseitin encoding of XOR of two literals.
void gate_nor(literalt a, literalt b, literalt o)
Tseitin encoding of NOR of two literals.
virtual literalt lequal(literalt a, literalt b) override
virtual literalt land(literalt a, literalt b) override
void gate_implies(literalt a, literalt b, literalt o)
Tseitin encoding of implication between two literals.
virtual literalt lxor(const bvt &bv) override
Tseitin encoding of XOR between multiple literals.
void gate_and(literalt a, literalt b, literalt o)
Tseitin encoding of conjunction of two literals.
virtual literalt lnand(literalt a, literalt b) override
virtual literalt lnor(literalt a, literalt b) override
virtual literalt lor(literalt a, literalt b) override
static var_not unused_var_no()
void lcnf(literalt l0, literalt l1)
CNF Generation, via Tseitin.
std::vector< literalt > bvt
literalt const_literal(bool value)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.