73 out <<
"%% limplies\n";
122 return lxor(bv[0], bv[1]);
127 literal=
lxor(*it, literal);
225 out <<
"%% lselect\n";
240 l.
set(_no_variables,
false);
249 l.
set(_no_variables,
false);
260 std::set<literalt> s;
262 new_bv.reserve(bv.size());
264 for(bvt::const_iterator it=bv.begin(); it!=bv.end(); it++)
266 if(s.insert(*it).second)
267 new_bv.push_back(*it);
269 if(s.find(!*it)!=s.end())
275 assert(!new_bv.empty());
280 for(bvt::const_iterator it=new_bv.begin(); it!=new_bv.end(); it++)
282 if(it!=new_bv.begin())
298 return "(NOT l"+std::to_string(l.
var_no())+
")";
300 return "l"+std::to_string(l.
var_no());
305 out <<
"QUERY FALSE;\n";
virtual void limplies(literalt a, literalt b, literalt o)
virtual void lor(literalt a, literalt b, literalt o)
#define forall_literals(it, bv)
virtual void lnor(literalt a, literalt b, literalt o)
virtual void lxor(literalt a, literalt b, literalt o)
virtual void land(literalt a, literalt b, literalt o)
literalt const_literal(bool value)
cvc_propt(std::ostream &_out)
virtual void lcnf(const bvt &bv)
literalt def_cvc_literal()
std::string cvc_literal(literalt l)
virtual void lequal(literalt a, literalt b, literalt o)
virtual literalt new_variable()
virtual propt::resultt prop_solve()
virtual void lnand(literalt a, literalt b, literalt o)
virtual literalt lselect(literalt a, literalt b, literalt c)
std::vector< literalt > bvt