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)
CNF Generation, via Tseitin.
void gate_implies(literalt a, literalt b, literalt o)
Tseitin encoding of implication between two literals.
virtual literalt lequal(literalt a, literalt b) override
void lcnf(literalt l0, literalt l1)
void gate_nand(literalt a, literalt b, literalt o)
Tseitin encoding of NAND of two literals.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
bool process_clause(const bvt &bv, bvt &dest)
filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses
virtual literalt lnor(literalt a, literalt b) override
static var_not unused_var_no()
static bvt eliminate_duplicates(const bvt &)
eliminate duplicates from given vector of literals
void gate_or(literalt a, literalt b, literalt o)
Tseitin encoding of disjunction of two literals.
virtual literalt lselect(literalt a, literalt b, literalt c) override
virtual literalt land(literalt a, literalt b) override
void gate_xor(literalt a, literalt b, literalt o)
Tseitin encoding of XOR of two literals.
virtual literalt new_variable() override
Generate a new variable and return it as a literal.
void gate_nor(literalt a, literalt b, literalt o)
Tseitin encoding of NOR of two literals.
virtual literalt limplies(literalt a, literalt b) override
virtual literalt lor(literalt a, literalt b) override
literalt const_literal(bool value)
static bool is_all(const bvt &bv, literalt l)
virtual void set_no_variables(size_t no)
void gate_and(literalt a, literalt b, literalt o)
Tseitin encoding of conjunction of two literals.
void gate_equal(literalt a, literalt b, literalt o)
Tseitin encoding of equality between two literals.
virtual literalt lnand(literalt a, literalt b) override
std::vector< literalt > bvt
virtual literalt lxor(const bvt &bv) override
Tseitin encoding of XOR between multiple literals.