14 const std::string &benchmark,
15 const std::string &source,
16 const std::string &logic,
20 core_enabled(_core_enabled)
22 out <<
"; SMT 2" <<
"\n";
24 out <<
"(set-info :source \"" << source <<
"\")" <<
"\n";
25 out <<
"(set-option :produce-models true)" <<
"\n";
29 out <<
"(set-option :produce-unsat-cores true)" <<
"\n";
32 out <<
"(set-logic " << logic <<
")" <<
"\n";
44 out <<
"(check-sat)" <<
"\n";
47 for(smt2_identifierst::const_iterator
51 out <<
"(get-value (" << *it <<
"))" <<
"\n";
56 out <<
"(get-unsat-core)" <<
"\n";
58 out <<
"; end of SMT2 file" <<
"\n";
67 out <<
"; land" <<
"\n";
84 out <<
"; lor" <<
"\n";
106 out <<
"; lxor" <<
"\n";
134 out <<
"; land" <<
"\n";
160 out <<
"; lor" <<
"\n";
184 out <<
"; lxor" <<
"\n";
235 out <<
"; lselect" <<
"\n";
236 out <<
" (if_then_else " 270 out <<
"(assert ; lcnf" <<
"\n";
275 else if(bv.size()==1)
281 for(bvt::const_iterator it=bv.begin(); it!=bv.end(); it++)
297 std::string v=
"B"+std::to_string(l.
var_no());
302 return "(not "+v+
")";
314 unsigned v=literal.
var_no();
318 return literal.
sign()?!r:
r;
326 unsigned v=literal.
var_no();
virtual literalt lselect(literalt a, literalt b, literalt c)
virtual literalt lxor(const bvt &bv)
virtual literalt land(literalt a, literalt b)
virtual void lcnf(const bvt &bv)
virtual literalt limplies(literalt a, literalt b)
virtual literalt lequal(literalt a, literalt b)
virtual propt::resultt prop_solve()
smt2_propt(const std::string &_benchmark, const std::string &_source, const std::string &_logic, bool _core_enabled, std::ostream &_out)
#define forall_literals(it, bv)
smt2_identifierst smt2_identifiers
std::string smt2_literal(literalt l)
virtual tvt l_get(literalt literal) const
virtual literalt lor(literalt a, literalt b)
virtual literalt lnand(literalt a, literalt b)
virtual literalt lnor(literalt a, literalt b)
literalt define_new_variable()
literalt const_literal(bool value)
virtual void set_assignment(literalt a, bool value)
std::vector< tvt > assignment
virtual literalt new_variable()
std::vector< literalt > bvt