From c199344bbf443fe0ce880b0f24a1f11e56249455 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Dec 2017 11:12:27 -0800 Subject: [PATCH] fix sat model converter to work with incrementality Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 2 +- src/sat/sat_model_converter.cpp | 5 + src/sat/sat_model_converter.h | 6 +- src/sat/sat_solver.h | 1 + src/sat/sat_solver/inc_sat_solver.cpp | 9 +- src/sat/tactic/goal2sat.cpp | 336 ++++++++++++-------------- src/sat/tactic/goal2sat.h | 37 ++- src/sat/tactic/sat_tactic.cpp | 2 +- 8 files changed, 198 insertions(+), 200 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 48ce6d22d..97fa23a79 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -171,7 +171,7 @@ extern "C" { sat::solver solver(to_solver_ref(s)->get_params(), m.limit()); parse_dimacs(is, solver); sat2goal s2g; - model_converter_ref mc; + ref mc; atom2bool_var a2b(m); goal g(m); s2g(solver, a2b, to_solver_ref(s)->get_params(), g, mc); diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index fac4cface..cc6614621 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -324,6 +324,11 @@ namespace sat { m_entries.append(src.m_entries); } + void model_converter::flush(model_converter & src) { + m_entries.append(src.m_entries); + src.m_entries.reset(); + } + void model_converter::collect_vars(bool_var_set & s) const { for (entry const & e : m_entries) s.insert(e.m_var); } diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index 28f23c063..88fdfe5b7 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -113,8 +113,12 @@ namespace sat { bool check_invariant(unsigned num_vars) const; void display(std::ostream & out) const; bool check_model(model const & m) const; - void copy(model_converter const & src); + + /* + \brief Append entries from src, then remove entries in src. + */ + void flush(model_converter& src); void collect_vars(bool_var_set & s) const; unsigned max_var(unsigned min) const; /* diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 56d1ace39..bbeb87f83 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -351,6 +351,7 @@ namespace sat { bool model_is_current() const { return m_model_is_current; } literal_vector const& get_core() const { return m_core; } model_converter const & get_model_converter() const { return m_mc; } + void flush(model_converter& mc) { mc.flush(m_mc); } void set_model(model const& mdl); char const* get_reason_unknown() const { return m_reason_unknown.c_str(); } bool check_clauses(model const& m) const; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index d731c246c..39b58e3a5 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -61,7 +61,7 @@ class inc_sat_solver : public solver { proof_converter_ref m_pc; model_converter_ref m_mc; model_converter_ref m_mc0; - model_converter_ref m_sat_mc; + ref m_sat_mc; mutable model_converter_ref m_cached_mc; svector m_weights; std::string m_unknown; @@ -120,7 +120,7 @@ public: for (expr* f : m_internalized_fmls) result->m_internalized_fmls.push_back(tr(f)); if (m_mc) result->m_mc = m_mc->translate(tr); if (m_mc0) result->m_mc0 = m_mc0->translate(tr); - //if (m_sat_mc) result->m_sat_mc = m_sat_mc->translate(tr); MN: commenting this line removes bloat + if (m_sat_mc) result->m_sat_mc = dynamic_cast(m_sat_mc->translate(tr)); // copy m_bb_rewriter? result->m_internalized_converted = m_internalized_converted; return result; @@ -531,6 +531,11 @@ private: m_pc = g->pc(); m_mc = g->mc(); TRACE("sat", g->display_with_dependencies(tout);); + + // ensure that if goal is already internalized, then import mc from m_solver. + if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m); + m_sat_mc->flush_smc(m_solver); + m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, is_incremental(), is_lemma); m_goal2sat.get_interpreted_atoms(atoms); if (!atoms.empty()) { diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 3e2abf8e8..bcfb06356 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -878,173 +878,135 @@ void goal2sat::get_interpreted_atoms(expr_ref_vector& atoms) { } +sat2goal::mc::mc(ast_manager& m): m(m), m_var2expr(m) {} + +void sat2goal::mc::flush_smc(sat::solver& s) { + s.flush(m_smc); +} + +void sat2goal::mc::flush_gmc() { + sat::literal_vector updates; + m_smc.expand(updates); + m_smc.reset(); + if (!m_gmc) m_gmc = alloc(generic_model_converter, m); + // now gmc owns the model converter + sat::literal_vector clause; + expr_ref_vector tail(m); + expr_ref def(m); + for (sat::literal l : updates) { + if (l == sat::null_literal) { + sat::literal lit0 = clause[0]; + for (unsigned i = 1; i < clause.size(); ++i) { + tail.push_back(lit2expr(~clause[i])); + } + def = m.mk_or(lit2expr(lit0), mk_and(tail)); + if (lit0.sign()) { + lit0.neg(); + def = m.mk_not(def); + } + m_gmc->add(lit2expr(lit0), def); + clause.reset(); + tail.reset(); + } + else { + clause.push_back(l); + } + } +} + +model_converter* sat2goal::mc::translate(ast_translation& translator) { + mc* result = alloc(mc, m); + result->m_smc.copy(m_smc); + result->m_gmc = m_gmc ? dynamic_cast(m_gmc->translate(translator)) : nullptr; + for (app* e : m_var2expr) { + result->m_var2expr.push_back(translator(e)); + } + return result; +} + +void sat2goal::mc::collect(ast_pp_util& visitor) { + flush_gmc(); + collect(visitor); +} + +void sat2goal::mc::display(std::ostream& out) { + flush_gmc(); + if (m_gmc) m_gmc->display(out); +} + +void sat2goal::mc::operator()(model_ref & md) { + model_evaluator ev(*md); + ev.set_model_completion(false); + + // create a SAT model using md + sat::model sat_md; + expr_ref val(m); + for (expr * atom : m_var2expr) { + if (!atom) { + sat_md.push_back(l_undef); + continue; + } + ev(atom, val); + if (m.is_true(val)) + sat_md.push_back(l_true); + else if (m.is_false(val)) + sat_md.push_back(l_false); + else + sat_md.push_back(l_undef); + } + + // apply SAT model converter + m_smc(sat_md); + + // register value of non-auxiliary boolean variables back into md + unsigned sz = m_var2expr.size(); + for (sat::bool_var v = 0; v < sz; v++) { + app * atom = m_var2expr.get(v); + if (atom && is_uninterp_const(atom)) { + func_decl * d = atom->get_decl(); + lbool new_val = sat_md[v]; + if (new_val == l_true) + md->register_decl(d, m.mk_true()); + else if (new_val == l_false) + md->register_decl(d, m.mk_false()); + } + } + // apply externalized model converter + if (m_gmc) (*m_gmc)(md); + TRACE("sat_mc", tout << "after sat_mc\n"; model_v2_pp(tout, *md);); +} + + +void sat2goal::mc::operator()(expr_ref& fml) { + flush_gmc(); + if (m_gmc) (*m_gmc)(fml); +} + +void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) { + VERIFY(!m_var2expr.get(v, nullptr)); + m_var2expr.reserve(v + 1); + m_var2expr.set(v, atom); + if (aux) { + SASSERT(is_uninterp_const(atom)); + SASSERT(m.is_bool(atom)); + if (!m_gmc) m_gmc = alloc(generic_model_converter, m); + m_gmc->hide(atom->get_decl()); + } +} + +expr_ref sat2goal::mc::lit2expr(sat::literal l) { + VERIFY(m_var2expr.get(l.var())); + expr_ref result(m_var2expr.get(l.var()), m); + if (l.sign()) { + result = m.mk_not(result); + } + return result; +} + + struct sat2goal::imp { - // Wrapper for sat::model_converter: converts it into an "AST level" model_converter. - class sat_model_converter : public model_converter { - model_converter_ref m_cached_mc; - sat::model_converter m_mc; - expr_ref_vector m_var2expr; - generic_model_converter_ref m_fmc; // filter for eliminating fresh variables introduced in the assertion-set --> sat conversion - generic_model_converter_ref m_imc; // used to ensure correctness in incremental calls with simplifications that require model conversions - - sat_model_converter(ast_manager & m): - m_var2expr(m) { - } - - void ensure_imc() { - if (m_imc) return; - m_imc = alloc(generic_model_converter, m()); - sat::literal_vector updates; - m_mc.expand(updates); - sat::literal_vector clause; - expr_ref_vector tail(m()); - expr_ref def(m()); - for (sat::literal l : updates) { - if (l == sat::null_literal) { - sat::literal lit0 = clause[0]; - for (unsigned i = 1; i < clause.size(); ++i) { - tail.push_back(lit2expr(~clause[i])); - } - def = m().mk_or(lit2expr(lit0), mk_and(tail)); - if (lit0.sign()) { - lit0.neg(); - def = m().mk_not(def); - } - m_imc->add(lit2expr(lit0), def); - clause.reset(); - tail.reset(); - } - else { - clause.push_back(l); - } - } - } - - public: - sat_model_converter(ast_manager & m, sat::solver const & s):m_var2expr(m) { - m_mc.copy(s.get_model_converter()); - m_fmc = alloc(generic_model_converter, m); - m_imc = nullptr; - } - - ast_manager & m() { return m_var2expr.get_manager(); } - - void init(unsigned num_vars) { - m_var2expr.resize(num_vars); - } - - void insert(unsigned v, expr * atom, bool aux) { - VERIFY(!m_var2expr.get(v)); - m_var2expr[v] = atom; - if (aux) { - SASSERT(is_uninterp_const(atom)); - SASSERT(m().is_bool(atom)); - m_fmc->hide(to_app(atom)->get_decl()); - } - } - - void finish() { - sat::literal_vector updates; - m_mc.expand(updates); - for (sat::literal l : updates) { - if (l != sat::null_literal && !m_var2expr.get(l.var())) { - insert(l.var(), m().mk_fresh_const(0, m().mk_bool_sort()), true); - } - } - m_imc = nullptr; - } - - virtual void operator()(model_ref & md) { - TRACE("sat_mc", tout << "before sat_mc\n"; model_v2_pp(tout, *md); display(tout);); - // REMARK: potential problem - // model_evaluator can't evaluate quantifiers. Then, - // an eliminated variable that depends on a quantified expression can't be recovered. - // A similar problem also affects any model_converter that uses elim_var_model_converter. - // - // Possible solution: - // model_converters reject any variable elimination that depends on a quantified expression. - - model_evaluator ev(*md); - ev.set_model_completion(false); - - // create a SAT model using md - sat::model sat_md; - expr_ref val(m()); - for (expr * atom : m_var2expr) { - if (!atom) { - sat_md.push_back(l_undef); - continue; - } - ev(atom, val); - if (m().is_true(val)) - sat_md.push_back(l_true); - else if (m().is_false(val)) - sat_md.push_back(l_false); - else - sat_md.push_back(l_undef); - } - - // apply SAT model converter - m_mc(sat_md); - - // register value of non-auxiliary boolean variables back into md - unsigned sz = m_var2expr.size(); - for (sat::bool_var v = 0; v < sz; v++) { - expr * atom = m_var2expr.get(v); - if (atom && is_uninterp_const(atom)) { - func_decl * d = to_app(atom)->get_decl(); - lbool new_val = sat_md[v]; - if (new_val == l_true) - md->register_decl(d, m().mk_true()); - else if (new_val == l_false) - md->register_decl(d, m().mk_false()); - } - } - - // apply filter model converter - (*m_fmc)(md); - TRACE("sat_mc", tout << "after sat_mc\n"; model_v2_pp(tout, *md);); - } - - virtual model_converter * translate(ast_translation & translator) { - sat_model_converter * res = alloc(sat_model_converter, translator.to()); - res->m_mc = m_mc; - res->m_fmc = static_cast(m_fmc->translate(translator)); - for (expr* e : m_var2expr) - res->m_var2expr.push_back(e ? translator(e) : nullptr); - return res; - } - - expr_ref lit2expr(sat::literal l) { - VERIFY(m_var2expr.get(l.var())); - expr_ref result(m_var2expr.get(l.var()), m()); - if (l.sign()) { - result = m().mk_not(result); - } - return result; - } - - void display(std::ostream & out) { - ensure_imc(); - m_imc->display(out); - m_fmc->display(out); - } - - virtual void collect(ast_pp_util& visitor) { - m_env = &visitor.env(); - for (expr* e : m_var2expr) if (e) visitor.coll.visit(e); - if (m_fmc) m_fmc->collect(visitor); - ensure_imc(); - m_imc->collect(visitor); - } - - void operator()(expr_ref& formula) override { - ensure_imc(); - (*m_imc)(formula); - } - }; - + typedef mc sat_model_converter; typedef ref sat_model_converter_ref; ast_manager & m; @@ -1073,12 +1035,11 @@ struct sat2goal::imp { m_lit2expr.resize(num_vars * 2); map.mk_inv(m_lit2expr); if (mc) { - mc->init(num_vars); for (sat::bool_var v = 0; v < num_vars; v++) { - checkpoint(); + checkpoint(); sat::literal l(v, false); if (m_lit2expr.get(l.index())) { - mc->insert(v, m_lit2expr.get(l.index()), false); + mc->insert(v, to_app(m_lit2expr.get(l.index())), false); SASSERT(m_lit2expr.get((~l).index())); } } @@ -1088,9 +1049,12 @@ struct sat2goal::imp { expr * lit2expr(sat_model_converter_ref& mc, sat::literal l) { if (!m_lit2expr.get(l.index())) { SASSERT(m_lit2expr.get((~l).index()) == 0); - app * aux = m.mk_fresh_const(0, m.mk_bool_sort()); - if (mc) - mc->insert(l.var(), aux, true); + app* aux = mc ? mc->var2expr(l.var()) : nullptr; + if (!aux) { + aux = m.mk_fresh_const(0, m.mk_bool_sort()); + if (mc) + mc->insert(l.var(), aux, true); + } m_lit2expr.set(l.index(), aux); m_lit2expr.set((~l).index(), m.mk_not(aux)); } @@ -1160,27 +1124,26 @@ struct sat2goal::imp { return dynamic_cast(s.get_extension()); } - void operator()(sat::solver const & s, atom2bool_var const & map, goal & r, model_converter_ref & mc) { + void operator()(sat::solver & s, atom2bool_var const & map, goal & r, ref & mc) { if (s.inconsistent()) { r.assert_expr(m.mk_false()); return; } - ref _mc; - if (r.models_enabled()) { - _mc = alloc(sat_model_converter, m, s); - mc = _mc.get(); + if (r.models_enabled() && !mc) { + mc = alloc(sat_model_converter, m); } - init_lit2expr(s, map, _mc); + if (mc) mc->flush_smc(s); + init_lit2expr(s, map, mc); // collect units unsigned num_vars = s.num_vars(); for (sat::bool_var v = 0; v < num_vars; v++) { checkpoint(); switch (s.value(v)) { case l_true: - r.assert_expr(lit2expr(_mc, sat::literal(v, false))); + r.assert_expr(lit2expr(mc, sat::literal(v, false))); break; case l_false: - r.assert_expr(lit2expr(_mc, sat::literal(v, true))); + r.assert_expr(lit2expr(mc, sat::literal(v, true))); break; case l_undef: break; @@ -1191,28 +1154,27 @@ struct sat2goal::imp { s.collect_bin_clauses(bin_clauses, m_learned); for (sat::solver::bin_clause const& bc : bin_clauses) { checkpoint(); - r.assert_expr(m.mk_or(lit2expr(_mc, bc.first), lit2expr(_mc, bc.second))); + r.assert_expr(m.mk_or(lit2expr(mc, bc.first), lit2expr(mc, bc.second))); } // collect clauses - assert_clauses(_mc, s, s.clauses(), r, true); + assert_clauses(mc, s, s.clauses(), r, true); sat::ba_solver* ext = get_ba_solver(s); if (ext) { for (auto* c : ext->constraints()) { switch (c->tag()) { case sat::ba_solver::card_t: - assert_card(_mc, r, c->to_card()); + assert_card(mc, r, c->to_card()); break; case sat::ba_solver::pb_t: - assert_pb(_mc, r, c->to_pb()); + assert_pb(mc, r, c->to_pb()); break; case sat::ba_solver::xor_t: - assert_xor(_mc, r, c->to_xor()); + assert_xor(mc, r, c->to_xor()); break; } } } - if (_mc) _mc->finish(); } void add_clause(sat_model_converter_ref& mc, sat::literal_vector const& lits, expr_ref_vector& lemmas) { @@ -1255,8 +1217,8 @@ struct sat2goal::scoped_set_imp { } }; -void sat2goal::operator()(sat::solver const & t, atom2bool_var const & m, params_ref const & p, - goal & g, model_converter_ref & mc) { +void sat2goal::operator()(sat::solver & t, atom2bool_var const & m, params_ref const & p, + goal & g, ref & mc) { imp proc(g.m(), p); scoped_set_imp set(this, &proc); proc(t, m, g, mc); diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index 9d2f310fc..43ee5a835 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -32,6 +32,7 @@ Notes: #include "tactic/goal.h" #include "sat/sat_solver.h" #include "tactic/model_converter.h" +#include "tactic/generic_model_converter.h" #include "sat/tactic/atom2bool_var.h" class goal2sat { @@ -73,8 +74,35 @@ class sat2goal { imp * m_imp; struct scoped_set_imp; public: + + class mc : public model_converter { + ast_manager& m; + sat::model_converter m_smc; + generic_model_converter_ref m_gmc; + app_ref_vector m_var2expr; + + // flushes from m_smc to m_gmc; + void flush_gmc(); + + public: + mc(ast_manager& m); + virtual ~mc() {} + // flush model converter from SAT solver to this structure. + void flush_smc(sat::solver& s); + void operator()(model_ref& md) override; + void operator()(expr_ref& fml) override; + model_converter* translate(ast_translation& translator) override; + void collect(ast_pp_util& visitor) override; + void display(std::ostream& out) override; + + app* var2expr(sat::bool_var v) const { return m_var2expr.get(v, nullptr); } + expr_ref lit2expr(sat::literal l); + void insert(sat::bool_var v, app * atom, bool aux); + }; + sat2goal(); + static void collect_param_descrs(param_descrs & r); /** @@ -85,14 +113,7 @@ public: \warning conversion throws a tactic_exception, if it is interrupted (by set_cancel), or memory consumption limit is reached (set with param :max-memory). */ - void operator()(sat::solver const & t, atom2bool_var const & m, params_ref const & p, goal & s, model_converter_ref & mc); - - - /** - \brief extract learned clauses only that are in the domain of m. - - */ - void get_learned(sat::solver const& s, atom2bool_var const& m, params_ref const& p, expr_ref_vector& learned); + void operator()(sat::solver & t, atom2bool_var const & m, params_ref const & p, goal & s, ref & mc); }; diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index a708f99bf..6beec79c9 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -108,7 +108,7 @@ class sat_tactic : public tactic { IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "\"formula constains interpreted atoms, recovering formula from sat solver...\"\n";); #endif m_solver.pop_to_base_level(); - model_converter_ref mc; + ref mc; m_sat2goal(m_solver, map, m_params, *(g.get()), mc); g->add(mc.get()); }