166 return land(bv[0], bv[1]);
168 for(
const auto &l : bv)
181 for(
const auto &l :
new_bv)
190 for(
const auto &l :
new_bv)
209 return lor(bv[0], bv[1]);
211 for(
const auto &l : bv)
224 for(
const auto &l :
new_bv)
233 for(
const auto &l :
new_bv)
252 return lxor(bv[0], bv[1]);
256 for(
const auto &l : bv)
266 if(
a.is_true() ||
b.is_false())
268 if(
b.is_true() ||
a.is_false())
282 if(
a.is_false() ||
b.is_true())
284 if(
b.is_false() ||
a.is_true())
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());
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");
453 "unknown variable " + std::to_string(l.var_no()) +
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)
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.