40 lits.push_back(
neg(a));
41 lits.push_back(
neg(b));
42 lits.push_back(
pos(o));
167 return land(bv[0], bv[1]);
169 for(
const auto &l : bv)
180 lits[1]=
neg(literal);
182 for(
const auto &l : new_bv)
189 lits.reserve(new_bv.size()+1);
191 for(
const auto &l : new_bv)
192 lits.push_back(
neg(l));
194 lits.push_back(
pos(literal));
210 return lor(bv[0], bv[1]);
212 for(
const auto &l : bv)
223 lits[1]=
pos(literal);
225 for(
const auto &l : new_bv)
232 lits.reserve(new_bv.size()+1);
234 for(
const auto &l : new_bv)
235 lits.push_back(
pos(l));
237 lits.push_back(
neg(literal));
253 return lxor(bv[0], bv[1]);
257 for(
const auto &l : bv)
258 literal=
lxor(l, literal);
350 return a.
sign() ? b : c;
372 #ifdef OPTIMAL_COMPACT_ITE
402 std::set<literalt> s;
405 dest.reserve(bv.size());
407 for(
const auto &l : bv)
408 if(s.insert(l).second)
426 for(
const auto &l : bv)
429 INVARIANT(l.var_no() != 0,
"variable 0 must not be used");
434 "variable 'unused_var_no' must not be used");
450 dest.reserve(bv.size());
452 for(
const auto &l : bv)
461 std::sort(dest.begin(), dest.end());
468 bvt::iterator it=dest.begin();
480 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
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.