16 const std::string &benchmark,
17 const std::string &source,
18 const std::string &logic,
19 std::ostream &_out):out(_out)
21 out <<
"(benchmark " << benchmark <<
"\n";
22 out <<
":source { " << source <<
" }" <<
"\n";
23 out <<
":status unknown" <<
"\n";
24 out <<
":logic " << logic <<
" ; SMT1" <<
"\n";
35 out <<
":formula true" <<
"\n";
36 out <<
") ; benchmark" <<
"\n";
45 out <<
":assumption ; land" <<
"\n";
62 out <<
":assumption ; lor" <<
"\n";
84 out <<
":assumption ; lxor" <<
"\n";
112 out <<
":assumption ; land" <<
"\n";
138 out <<
":assumption ; lor" <<
"\n";
162 out <<
":assumption ; lxor" <<
"\n";
213 out <<
":assumption ; lselect" <<
"\n";
235 out <<
":assumption ; lcnf" <<
"\n";
239 out <<
"false ; the empty clause";
240 else if(bv.size()==1)
246 for(bvt::const_iterator it=bv.begin(); it!=bv.end(); it++)
262 std::string v=
"B"+std::to_string(l.
var_no());
265 return "(not "+v+
")";
277 unsigned v=literal.
var_no();
281 return literal.
sign()?!
r:
r;
289 unsigned v=literal.
var_no();
std::vector< tvt > assignment
virtual literalt lnor(literalt a, literalt b)
virtual void lcnf(const bvt &bv)
virtual literalt land(literalt a, literalt b)
#define forall_literals(it, bv)
virtual literalt lxor(const bvt &bv)
virtual literalt new_variable()
std::string smt1_literal(literalt l)
virtual literalt lor(literalt a, literalt b)
virtual literalt limplies(literalt a, literalt b)
virtual literalt lselect(literalt a, literalt b, literalt c)
literalt const_literal(bool value)
virtual void set_assignment(literalt a, bool value)
virtual literalt lequal(literalt a, literalt b)
virtual literalt lnand(literalt a, literalt b)
virtual propt::resultt prop_solve()
smt1_propt(const std::string &_benchmark, const std::string &_source, const std::string &_logic, std::ostream &_out)
std::vector< literalt > bvt
virtual tvt l_get(literalt literal) const