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