43 for(std::size_t i=0; i<width; i++)
void lcnf(literalt l0, literalt l1)
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
virtual literalt new_variable()=0
virtual void set_assignment(literalt a, bool value)
mstreamt & result() const
virtual bool is_in_conflict(literalt l) const
virtual void copy_assignment_from(const propt &prop)
std::vector< literalt > bvt