24 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
mstreamt & result() const
std::vector< literalt > bvt