From 3ec1a1002c3a68653fff58de7a15475e412b4f52 Mon Sep 17 00:00:00 2001 From: Jamey Sharp Date: Mon, 13 Sep 2021 14:53:31 -0700 Subject: [PATCH 1/2] split sat2goal out of goal2sat These two classes need different things out of the sat::solver class, and separating them makes it easier to fiddle with their dependencies independently. I also fiddled with some headers to make it possible to include sat_solver_core.h instead of sat_solver.h. --- src/api/api_solver.cpp | 1 + src/sat/sat_solver/inc_sat_solver.cpp | 1 + src/sat/sat_solver_core.h | 2 +- src/sat/smt/sat_internalizer.h | 35 +++ src/sat/smt/sat_smt.h | 15 +- src/sat/tactic/CMakeLists.txt | 1 + src/sat/tactic/goal2sat.cpp | 287 ---------------------- src/sat/tactic/goal2sat.h | 57 +---- src/sat/tactic/sat2goal.cpp | 331 ++++++++++++++++++++++++++ src/sat/tactic/sat2goal.h | 84 +++++++ src/sat/tactic/sat_tactic.cpp | 1 + src/shell/dimacs_frontend.cpp | 1 + 12 files changed, 459 insertions(+), 357 deletions(-) create mode 100644 src/sat/smt/sat_internalizer.h create mode 100644 src/sat/tactic/sat2goal.cpp create mode 100644 src/sat/tactic/sat2goal.h diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 2b590c070ee..2837d6a3680 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -42,6 +42,7 @@ Revision History: #include "sat/dimacs.h" #include "sat/sat_solver.h" #include "sat/tactic/goal2sat.h" +#include "sat/tactic/sat2goal.h" extern "C" { diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index d3782cf5348..e2ce4363774 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -42,6 +42,7 @@ Module Name: #include "sat/sat_params.hpp" #include "sat/smt/euf_solver.h" #include "sat/tactic/goal2sat.h" +#include "sat/tactic/sat2goal.h" #include "sat/tactic/sat_tactic.h" #include "sat/sat_simplifier_params.hpp" diff --git a/src/sat/sat_solver_core.h b/src/sat/sat_solver_core.h index 40ac4cbc4ee..3be1aa1927f 100644 --- a/src/sat/sat_solver_core.h +++ b/src/sat/sat_solver_core.h @@ -18,7 +18,7 @@ Revision History: --*/ #pragma once - +#include "sat/sat_model_converter.h" #include "sat/sat_types.h" namespace sat { diff --git a/src/sat/smt/sat_internalizer.h b/src/sat/smt/sat_internalizer.h new file mode 100644 index 00000000000..43413a8930f --- /dev/null +++ b/src/sat/smt/sat_internalizer.h @@ -0,0 +1,35 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + sat_internalizer.h + +Abstract: + + Header for SMT theories over SAT solver + +Author: + + Nikolaj Bjorner (nbjorner) 2020-08-25 + +--*/ +#pragma once + +#include "util/sat_literal.h" + +namespace sat { + class sat_internalizer { + public: + virtual ~sat_internalizer() {} + virtual bool is_bool_op(expr* e) const = 0; + virtual literal internalize(expr* e, bool learned) = 0; + virtual bool_var to_bool_var(expr* e) = 0; + virtual bool_var add_bool_var(expr* e) = 0; + virtual void cache(app* t, literal l) = 0; + virtual void uncache(literal l) = 0; + virtual void push() = 0; + virtual void pop(unsigned n) = 0; + virtual void set_expr2var_replay(obj_map* r) = 0; + }; +} diff --git a/src/sat/smt/sat_smt.h b/src/sat/smt/sat_smt.h index 0ba632f6391..b509f0a9e13 100644 --- a/src/sat/smt/sat_smt.h +++ b/src/sat/smt/sat_smt.h @@ -19,6 +19,7 @@ Module Name: #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "sat/sat_solver.h" +#include "sat/smt/sat_internalizer.h" namespace sat { @@ -28,20 +29,6 @@ namespace sat { eframe(expr* e) : m_e(e), m_idx(0) {} }; - class sat_internalizer { - public: - virtual ~sat_internalizer() {} - virtual bool is_bool_op(expr* e) const = 0; - virtual literal internalize(expr* e, bool learned) = 0; - virtual bool_var to_bool_var(expr* e) = 0; - virtual bool_var add_bool_var(expr* e) = 0; - virtual void cache(app* t, literal l) = 0; - virtual void uncache(literal l) = 0; - virtual void push() = 0; - virtual void pop(unsigned n) = 0; - virtual void set_expr2var_replay(obj_map* r) = 0; - }; - class constraint_base { extension* m_ex; unsigned m_mem[0]; diff --git a/src/sat/tactic/CMakeLists.txt b/src/sat/tactic/CMakeLists.txt index d1924d67928..59e7db1ab15 100644 --- a/src/sat/tactic/CMakeLists.txt +++ b/src/sat/tactic/CMakeLists.txt @@ -1,6 +1,7 @@ z3_add_component(sat_tactic SOURCES goal2sat.cpp + sat2goal.cpp sat_tactic.cpp COMPONENT_DEPENDENCIES sat diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 76e11474e5d..bdb37bc7910 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -1053,290 +1053,3 @@ sat::sat_internalizer& goal2sat::si(ast_manager& m, params_ref const& p, sat::so m_imp = alloc(imp, m, p, t, a2b, dep2asm, default_external); return *m_imp; } - - - -sat2goal::mc::mc(ast_manager& m): m(m), m_var2expr(m) {} - -void sat2goal::mc::flush_smc(sat::solver_core& s, atom2bool_var const& map) { - s.flush(m_smc); - m_var2expr.resize(s.num_vars()); - map.mk_var_inv(m_var2expr); - flush_gmc(); -} - -void sat2goal::mc::flush_gmc() { - sat::literal_vector updates; - m_smc.expand(updates); - if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); - // now gmc owns the model converter - sat::literal_vector clause; - expr_ref_vector tail(m); - expr_ref def(m); - auto is_literal = [&](expr* e) { expr* r; return is_uninterp_const(e) || (m.is_not(e, r) && is_uninterp_const(r)); }; - - for (unsigned i = 0; i < updates.size(); ++i) { - sat::literal l = updates[i]; - 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); - } - expr_ref e = lit2expr(lit0); - if (is_literal(e)) - m_gmc->add(e, def); - clause.reset(); - tail.reset(); - } - // short circuit for equivalences: - else if (clause.empty() && tail.empty() && - i + 5 < updates.size() && - updates[i] == ~updates[i + 3] && - updates[i + 1] == ~updates[i + 4] && - updates[i + 2] == sat::null_literal && - updates[i + 5] == sat::null_literal) { - sat::literal r = ~updates[i+1]; - if (l.sign()) { - l.neg(); - r.neg(); - } - - expr* a = lit2expr(l); - if (is_literal(a)) - m_gmc->add(a, lit2expr(r)); - i += 5; - } - else { - clause.push_back(l); - } - } -} - -model_converter* sat2goal::mc::translate(ast_translation& translator) { - mc* result = alloc(mc, translator.to()); - result->m_smc.copy(m_smc); - result->m_gmc = m_gmc ? dynamic_cast(m_gmc->translate(translator)) : nullptr; - for (expr* e : m_var2expr) { - result->m_var2expr.push_back(translator(e)); - } - return result; -} - -void sat2goal::mc::set_env(ast_pp_util* visitor) { - flush_gmc(); - if (m_gmc) m_gmc->set_env(visitor); -} - -void sat2goal::mc::display(std::ostream& out) { - flush_gmc(); - if (m_gmc) m_gmc->display(out); -} - -void sat2goal::mc::get_units(obj_map& units) { - flush_gmc(); - if (m_gmc) m_gmc->get_units(units); -} - - -void sat2goal::mc::operator()(sat::model& md) { - m_smc(md); -} - -void sat2goal::mc::operator()(model_ref & md) { - // apply externalized model converter - CTRACE("sat_mc", m_gmc, m_gmc->display(tout << "before sat_mc\n"); model_v2_pp(tout, *md);); - if (m_gmc) (*m_gmc)(md); - CTRACE("sat_mc", m_gmc, m_gmc->display(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, expr * atom, bool aux) { - SASSERT(!m_var2expr.get(v, nullptr)); - m_var2expr.reserve(v + 1); - m_var2expr.set(v, atom); - if (aux) { - SASSERT(m.is_bool(atom)); - if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); - if (is_uninterp_const(atom)) - m_gmc->hide(to_app(atom)->get_decl()); - } - TRACE("sat_mc", tout << "insert " << v << "\n";); -} - -expr_ref sat2goal::mc::lit2expr(sat::literal l) { - sat::bool_var v = l.var(); - if (!m_var2expr.get(v)) { - app* aux = m.mk_fresh_const(nullptr, m.mk_bool_sort()); - m_var2expr.set(v, aux); - if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); - m_gmc->hide(aux->get_decl()); - } - VERIFY(m_var2expr.get(v)); - expr_ref result(m_var2expr.get(v), m); - if (l.sign()) { - result = m.mk_not(result); - } - return result; -} - - -struct sat2goal::imp { - - typedef mc sat_model_converter; - - ast_manager & m; - expr_ref_vector m_lit2expr; - unsigned long long m_max_memory; - bool m_learned; - - imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m) { - updt_params(p); - } - - void updt_params(params_ref const & p) { - m_learned = p.get_bool("learned", false); - m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); - } - - void checkpoint() { - if (!m.inc()) - throw tactic_exception(m.limit().get_cancel_msg()); - if (memory::get_allocation_size() > m_max_memory) - throw tactic_exception(TACTIC_MAX_MEMORY_MSG); - } - - expr * lit2expr(ref& mc, sat::literal l) { - if (!m_lit2expr.get(l.index())) { - SASSERT(m_lit2expr.get((~l).index()) == 0); - expr* aux = mc ? mc->var2expr(l.var()) : nullptr; - if (!aux) { - aux = m.mk_fresh_const(nullptr, m.mk_bool_sort()); - if (mc) { - mc->insert(l.var(), aux, true); - } - } - sat::literal lit(l.var(), false); - m_lit2expr.set(lit.index(), aux); - m_lit2expr.set((~lit).index(), m.mk_not(aux)); - } - return m_lit2expr.get(l.index()); - } - - void assert_clauses(ref& mc, sat::solver_core const & s, sat::clause_vector const& clauses, goal & r, bool asserted) { - ptr_buffer lits; - unsigned small_lbd = 3; // s.get_config().m_gc_small_lbd; - for (sat::clause* cp : clauses) { - checkpoint(); - lits.reset(); - sat::clause const & c = *cp; - if (asserted || m_learned || c.glue() <= small_lbd) { - for (sat::literal l : c) { - lits.push_back(lit2expr(mc, l)); - } - r.assert_expr(m.mk_or(lits)); - } - } - } - - void operator()(sat::solver_core & s, atom2bool_var const & map, goal & r, ref & mc) { - if (s.at_base_lvl() && s.inconsistent()) { - r.assert_expr(m.mk_false()); - return; - } - if (r.models_enabled() && !mc) { - mc = alloc(sat_model_converter, m); - } - if (mc) mc->flush_smc(s, map); - m_lit2expr.resize(s.num_vars() * 2); - map.mk_inv(m_lit2expr); - // collect units - unsigned trail_sz = s.init_trail_size(); - for (unsigned i = 0; i < trail_sz; ++i) { - checkpoint(); - r.assert_expr(lit2expr(mc, s.trail_literal(i))); - } - // collect binary clauses - svector bin_clauses; - s.collect_bin_clauses(bin_clauses, m_learned, false); - for (sat::solver::bin_clause const& bc : bin_clauses) { - checkpoint(); - r.assert_expr(m.mk_or(lit2expr(mc, bc.first), lit2expr(mc, bc.second))); - } - // collect clauses - assert_clauses(mc, s, s.clauses(), r, true); - - auto* ext = s.get_extension(); - if (ext) { - std::function l2e = [&](sat::literal lit) { - return expr_ref(lit2expr(mc, lit), m); - }; - expr_ref_vector fmls(m); - pb::solver* ba = dynamic_cast(ext); - if (ba) { - ba->to_formulas(l2e, fmls); - } - else - dynamic_cast(ext)->to_formulas(l2e, fmls); - for (expr* f : fmls) - r.assert_expr(f); - } - } - - void add_clause(ref& mc, sat::literal_vector const& lits, expr_ref_vector& lemmas) { - expr_ref_vector lemma(m); - for (sat::literal l : lits) { - expr* e = lit2expr(mc, l); - if (!e) return; - lemma.push_back(e); - } - lemmas.push_back(mk_or(lemma)); - } - - void add_clause(ref& mc, sat::clause const& c, expr_ref_vector& lemmas) { - expr_ref_vector lemma(m); - for (sat::literal l : c) { - expr* e = lit2expr(mc, l); - if (!e) return; - lemma.push_back(e); - } - lemmas.push_back(mk_or(lemma)); - } - -}; - -sat2goal::sat2goal():m_imp(nullptr) { -} - -void sat2goal::collect_param_descrs(param_descrs & r) { - insert_max_memory(r); - r.insert("learned", CPK_BOOL, "(default: false) collect also learned clauses."); -} - -struct sat2goal::scoped_set_imp { - sat2goal * m_owner; - scoped_set_imp(sat2goal * o, sat2goal::imp * i):m_owner(o) { - m_owner->m_imp = i; - } - ~scoped_set_imp() { - m_owner->m_imp = nullptr; - } -}; - -void sat2goal::operator()(sat::solver_core & 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 bc6b8dcb1d6..8b344c9c348 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -29,11 +29,9 @@ Module Name: #pragma once #include "tactic/goal.h" -#include "sat/sat_solver.h" -#include "tactic/model_converter.h" -#include "tactic/generic_model_converter.h" +#include "sat/sat_solver_core.h" #include "sat/smt/atom2bool_var.h" -#include "sat/smt/sat_smt.h" +#include "sat/smt/sat_internalizer.h" class goal2sat { struct imp; @@ -77,54 +75,3 @@ class goal2sat { void user_pop(unsigned n); }; - - -class sat2goal { - struct imp; - 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; - expr_ref_vector m_var2expr; - - // flushes from m_smc to m_gmc; - void flush_gmc(); - - public: - mc(ast_manager& m); - ~mc() override {} - // flush model converter from SAT solver to this structure. - void flush_smc(sat::solver_core& s, atom2bool_var const& map); - void operator()(sat::model& m); - void operator()(model_ref& md) override; - void operator()(expr_ref& fml) override; - model_converter* translate(ast_translation& translator) override; - void set_env(ast_pp_util* visitor) override; - void display(std::ostream& out) override; - void get_units(obj_map& units) override; - expr* var2expr(sat::bool_var v) const { return m_var2expr.get(v, nullptr); } - expr_ref lit2expr(sat::literal l); - void insert(sat::bool_var v, expr * atom, bool aux); - }; - - sat2goal(); - - - static void collect_param_descrs(param_descrs & r); - - /** - \brief Translate the state of the SAT engine back into a goal. - The SAT solver may use variables that are not in \c m. The translator - creates fresh boolean AST variables for them. They are stored in fvars. - - \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_core & t, atom2bool_var const & m, params_ref const & p, goal & s, ref & mc); - -}; - diff --git a/src/sat/tactic/sat2goal.cpp b/src/sat/tactic/sat2goal.cpp new file mode 100644 index 00000000000..3fbcc50ee0b --- /dev/null +++ b/src/sat/tactic/sat2goal.cpp @@ -0,0 +1,331 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + sat2goal.cpp + +Abstract: + + "Compile" a goal into the SAT engine. + Atoms are "abstracted" into boolean variables. + The mapping between boolean variables and atoms + can be used to convert back the state of the + SAT engine into a goal. + + The idea is to support scenarios such as: + 1) simplify, blast, convert into SAT, and solve + 2) convert into SAT, apply SAT for a while, learn new units, and translate back into a goal. + 3) convert into SAT, apply SAT preprocessor (failed literal propagation, resolution, etc) and translate back into a goal. + 4) Convert boolean structure into SAT, convert atoms into another engine, combine engines using lazy combination, solve. + +Author: + + Leonardo (leonardo) 2011-10-26 + +Notes: + +--*/ +#include "util/ref_util.h" +#include "ast/ast_smt2_pp.h" +#include "ast/ast_pp.h" +#include "ast/ast_smt2_pp.h" +#include "ast/ast_ll_pp.h" +#include "ast/pb_decl_plugin.h" +#include "ast/ast_util.h" +#include "ast/for_each_expr.h" +#include "model/model_evaluator.h" +#include "model/model_v2_pp.h" +#include "tactic/tactic.h" +#include "tactic/generic_model_converter.h" +#include "sat/sat_cut_simplifier.h" +#include "sat/sat_drat.h" +#include "sat/tactic/sat2goal.h" +#include "sat/smt/pb_solver.h" +#include "sat/smt/euf_solver.h" +#include "sat/smt/sat_th.h" +#include "sat/sat_params.hpp" +#include + +sat2goal::mc::mc(ast_manager& m): m(m), m_var2expr(m) {} + +void sat2goal::mc::flush_smc(sat::solver_core& s, atom2bool_var const& map) { + s.flush(m_smc); + m_var2expr.resize(s.num_vars()); + map.mk_var_inv(m_var2expr); + flush_gmc(); +} + +void sat2goal::mc::flush_gmc() { + sat::literal_vector updates; + m_smc.expand(updates); + if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); + // now gmc owns the model converter + sat::literal_vector clause; + expr_ref_vector tail(m); + expr_ref def(m); + auto is_literal = [&](expr* e) { expr* r; return is_uninterp_const(e) || (m.is_not(e, r) && is_uninterp_const(r)); }; + + for (unsigned i = 0; i < updates.size(); ++i) { + sat::literal l = updates[i]; + 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); + } + expr_ref e = lit2expr(lit0); + if (is_literal(e)) + m_gmc->add(e, def); + clause.reset(); + tail.reset(); + } + // short circuit for equivalences: + else if (clause.empty() && tail.empty() && + i + 5 < updates.size() && + updates[i] == ~updates[i + 3] && + updates[i + 1] == ~updates[i + 4] && + updates[i + 2] == sat::null_literal && + updates[i + 5] == sat::null_literal) { + sat::literal r = ~updates[i+1]; + if (l.sign()) { + l.neg(); + r.neg(); + } + + expr* a = lit2expr(l); + if (is_literal(a)) + m_gmc->add(a, lit2expr(r)); + i += 5; + } + else { + clause.push_back(l); + } + } +} + +model_converter* sat2goal::mc::translate(ast_translation& translator) { + mc* result = alloc(mc, translator.to()); + result->m_smc.copy(m_smc); + result->m_gmc = m_gmc ? dynamic_cast(m_gmc->translate(translator)) : nullptr; + for (expr* e : m_var2expr) { + result->m_var2expr.push_back(translator(e)); + } + return result; +} + +void sat2goal::mc::set_env(ast_pp_util* visitor) { + flush_gmc(); + if (m_gmc) m_gmc->set_env(visitor); +} + +void sat2goal::mc::display(std::ostream& out) { + flush_gmc(); + if (m_gmc) m_gmc->display(out); +} + +void sat2goal::mc::get_units(obj_map& units) { + flush_gmc(); + if (m_gmc) m_gmc->get_units(units); +} + + +void sat2goal::mc::operator()(sat::model& md) { + m_smc(md); +} + +void sat2goal::mc::operator()(model_ref & md) { + // apply externalized model converter + CTRACE("sat_mc", m_gmc, m_gmc->display(tout << "before sat_mc\n"); model_v2_pp(tout, *md);); + if (m_gmc) (*m_gmc)(md); + CTRACE("sat_mc", m_gmc, m_gmc->display(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, expr * atom, bool aux) { + SASSERT(!m_var2expr.get(v, nullptr)); + m_var2expr.reserve(v + 1); + m_var2expr.set(v, atom); + if (aux) { + SASSERT(m.is_bool(atom)); + if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); + if (is_uninterp_const(atom)) + m_gmc->hide(to_app(atom)->get_decl()); + } + TRACE("sat_mc", tout << "insert " << v << "\n";); +} + +expr_ref sat2goal::mc::lit2expr(sat::literal l) { + sat::bool_var v = l.var(); + if (!m_var2expr.get(v)) { + app* aux = m.mk_fresh_const(nullptr, m.mk_bool_sort()); + m_var2expr.set(v, aux); + if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); + m_gmc->hide(aux->get_decl()); + } + VERIFY(m_var2expr.get(v)); + expr_ref result(m_var2expr.get(v), m); + if (l.sign()) { + result = m.mk_not(result); + } + return result; +} + + +struct sat2goal::imp { + + typedef mc sat_model_converter; + + ast_manager & m; + expr_ref_vector m_lit2expr; + unsigned long long m_max_memory; + bool m_learned; + + imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m) { + updt_params(p); + } + + void updt_params(params_ref const & p) { + m_learned = p.get_bool("learned", false); + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + } + + void checkpoint() { + if (!m.inc()) + throw tactic_exception(m.limit().get_cancel_msg()); + if (memory::get_allocation_size() > m_max_memory) + throw tactic_exception(TACTIC_MAX_MEMORY_MSG); + } + + expr * lit2expr(ref& mc, sat::literal l) { + if (!m_lit2expr.get(l.index())) { + SASSERT(m_lit2expr.get((~l).index()) == 0); + expr* aux = mc ? mc->var2expr(l.var()) : nullptr; + if (!aux) { + aux = m.mk_fresh_const(nullptr, m.mk_bool_sort()); + if (mc) { + mc->insert(l.var(), aux, true); + } + } + sat::literal lit(l.var(), false); + m_lit2expr.set(lit.index(), aux); + m_lit2expr.set((~lit).index(), m.mk_not(aux)); + } + return m_lit2expr.get(l.index()); + } + + void assert_clauses(ref& mc, sat::solver_core const & s, sat::clause_vector const& clauses, goal & r, bool asserted) { + ptr_buffer lits; + unsigned small_lbd = 3; // s.get_config().m_gc_small_lbd; + for (sat::clause* cp : clauses) { + checkpoint(); + lits.reset(); + sat::clause const & c = *cp; + if (asserted || m_learned || c.glue() <= small_lbd) { + for (sat::literal l : c) { + lits.push_back(lit2expr(mc, l)); + } + r.assert_expr(m.mk_or(lits)); + } + } + } + + void operator()(sat::solver_core & s, atom2bool_var const & map, goal & r, ref & mc) { + if (s.at_base_lvl() && s.inconsistent()) { + r.assert_expr(m.mk_false()); + return; + } + if (r.models_enabled() && !mc) { + mc = alloc(sat_model_converter, m); + } + if (mc) mc->flush_smc(s, map); + m_lit2expr.resize(s.num_vars() * 2); + map.mk_inv(m_lit2expr); + // collect units + unsigned trail_sz = s.init_trail_size(); + for (unsigned i = 0; i < trail_sz; ++i) { + checkpoint(); + r.assert_expr(lit2expr(mc, s.trail_literal(i))); + } + // collect binary clauses + svector bin_clauses; + s.collect_bin_clauses(bin_clauses, m_learned, false); + for (sat::solver::bin_clause const& bc : bin_clauses) { + checkpoint(); + r.assert_expr(m.mk_or(lit2expr(mc, bc.first), lit2expr(mc, bc.second))); + } + // collect clauses + assert_clauses(mc, s, s.clauses(), r, true); + + auto* ext = s.get_extension(); + if (ext) { + std::function l2e = [&](sat::literal lit) { + return expr_ref(lit2expr(mc, lit), m); + }; + expr_ref_vector fmls(m); + pb::solver* ba = dynamic_cast(ext); + if (ba) { + ba->to_formulas(l2e, fmls); + } + else + dynamic_cast(ext)->to_formulas(l2e, fmls); + for (expr* f : fmls) + r.assert_expr(f); + } + } + + void add_clause(ref& mc, sat::literal_vector const& lits, expr_ref_vector& lemmas) { + expr_ref_vector lemma(m); + for (sat::literal l : lits) { + expr* e = lit2expr(mc, l); + if (!e) return; + lemma.push_back(e); + } + lemmas.push_back(mk_or(lemma)); + } + + void add_clause(ref& mc, sat::clause const& c, expr_ref_vector& lemmas) { + expr_ref_vector lemma(m); + for (sat::literal l : c) { + expr* e = lit2expr(mc, l); + if (!e) return; + lemma.push_back(e); + } + lemmas.push_back(mk_or(lemma)); + } + +}; + +sat2goal::sat2goal():m_imp(nullptr) { +} + +void sat2goal::collect_param_descrs(param_descrs & r) { + insert_max_memory(r); + r.insert("learned", CPK_BOOL, "(default: false) collect also learned clauses."); +} + +struct sat2goal::scoped_set_imp { + sat2goal * m_owner; + scoped_set_imp(sat2goal * o, sat2goal::imp * i):m_owner(o) { + m_owner->m_imp = i; + } + ~scoped_set_imp() { + m_owner->m_imp = nullptr; + } +}; + +void sat2goal::operator()(sat::solver_core & 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/sat2goal.h b/src/sat/tactic/sat2goal.h new file mode 100644 index 00000000000..969b66e2396 --- /dev/null +++ b/src/sat/tactic/sat2goal.h @@ -0,0 +1,84 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + sat2goal.h + +Abstract: + + "Compile" a goal into the SAT engine. + Atoms are "abstracted" into boolean variables. + The mapping between boolean variables and atoms + can be used to convert back the state of the + SAT engine into a goal. + + The idea is to support scenarios such as: + 1) simplify, blast, convert into SAT, and solve + 2) convert into SAT, apply SAT for a while, learn new units, and translate back into a goal. + 3) convert into SAT, apply SAT preprocessor (failed literal propagation, resolution, etc) and translate back into a goal. + 4) Convert boolean structure into SAT, convert atoms into another engine, combine engines using lazy combination, solve. + +Author: + + Leonardo (leonardo) 2011-10-26 + +Notes: + +--*/ +#pragma once + +#include "tactic/goal.h" +#include "sat/sat_model_converter.h" +#include "sat/sat_solver_core.h" +#include "tactic/generic_model_converter.h" +#include "sat/smt/atom2bool_var.h" + +class sat2goal { + struct imp; + 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; + expr_ref_vector m_var2expr; + + // flushes from m_smc to m_gmc; + void flush_gmc(); + + public: + mc(ast_manager& m); + ~mc() override {} + // flush model converter from SAT solver to this structure. + void flush_smc(sat::solver_core& s, atom2bool_var const& map); + void operator()(sat::model& m); + void operator()(model_ref& md) override; + void operator()(expr_ref& fml) override; + model_converter* translate(ast_translation& translator) override; + void set_env(ast_pp_util* visitor) override; + void display(std::ostream& out) override; + void get_units(obj_map& units) override; + expr* var2expr(sat::bool_var v) const { return m_var2expr.get(v, nullptr); } + expr_ref lit2expr(sat::literal l); + void insert(sat::bool_var v, expr * atom, bool aux); + }; + + sat2goal(); + + + static void collect_param_descrs(param_descrs & r); + + /** + \brief Translate the state of the SAT engine back into a goal. + The SAT solver may use variables that are not in \c m. The translator + creates fresh boolean AST variables for them. They are stored in fvars. + + \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_core & 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 c8c009bbf3f..bbea0960431 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -20,6 +20,7 @@ Module Name: #include "model/model_v2_pp.h" #include "tactic/tactical.h" #include "sat/tactic/goal2sat.h" +#include "sat/tactic/sat2goal.h" #include "sat/sat_solver.h" #include "sat/sat_params.hpp" diff --git a/src/shell/dimacs_frontend.cpp b/src/shell/dimacs_frontend.cpp index ec157a291e5..a5d562440e2 100644 --- a/src/shell/dimacs_frontend.cpp +++ b/src/shell/dimacs_frontend.cpp @@ -26,6 +26,7 @@ Revision History: #include "sat/sat_params.hpp" #include "sat/sat_solver.h" #include "sat/tactic/goal2sat.h" +#include "sat/tactic/sat2goal.h" #include "ast/reg_decl_plugins.h" #include "tactic/tactic.h" #include "tactic/fd_solver/fd_solver.h" From 52432c11f9349c0958fa961a09aa287a7f7134e4 Mon Sep 17 00:00:00 2001 From: Jamey Sharp Date: Mon, 13 Sep 2021 14:04:08 -0700 Subject: [PATCH 2/2] limit solver_core methods to those needed by goal2sat And switch sat2goal and sat_tactic over to relying on the derived sat::solver class instead. There were no other uses of solver_core. I'm hoping this makes it feasible to reuse goal2sat's CNF conversion from places like the tseitin-cnf tactic, so they can be unified into a single implementation. --- src/sat/sat_solver.h | 68 +++++++++++++++++++++++------------ src/sat/sat_solver_core.h | 59 ------------------------------ src/sat/tactic/sat2goal.cpp | 8 ++--- src/sat/tactic/sat2goal.h | 6 ++-- src/sat/tactic/sat_tactic.cpp | 2 +- 5 files changed, 54 insertions(+), 89 deletions(-) diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index a5d83f273c9..b6affe4ee4e 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -244,12 +244,13 @@ namespace sat { // Misc // // ----------------------- - void updt_params(params_ref const & p) override; + void updt_params(params_ref const & p); static void collect_param_descrs(param_descrs & d); - void collect_statistics(statistics & st) const override; + // collect statistics from sat solver + void collect_statistics(statistics & st) const; void reset_statistics(); - void display_status(std::ostream & out) const override; + void display_status(std::ostream & out) const; /** \brief Copy (non learned) clauses from src to this solver. @@ -351,14 +352,19 @@ namespace sat { // // ----------------------- public: - bool inconsistent() const override { return m_inconsistent; } - unsigned num_vars() const override { return m_justification.size(); } - unsigned num_clauses() const override; + // is the state inconsistent? + bool inconsistent() const { return m_inconsistent; } + + // number of variables and clauses + unsigned num_vars() const { return m_justification.size(); } + unsigned num_clauses() const; + void num_binary(unsigned& given, unsigned& learned) const; unsigned num_restarts() const { return m_restarts; } - bool is_external(bool_var v) const override { return m_external[v]; } + bool is_external(bool_var v) const { return m_external[v]; } + bool is_external(literal l) const { return is_external(l.var()); } void set_external(bool_var v) override; - void set_non_external(bool_var v) override; + void set_non_external(bool_var v); bool was_eliminated(bool_var v) const { return m_eliminated[v]; } void set_eliminated(bool_var v, bool f) override; bool was_eliminated(literal l) const { return was_eliminated(l.var()); } @@ -368,16 +374,14 @@ namespace sat { unsigned scope_lvl() const { return m_scope_lvl; } unsigned search_lvl() const { return m_search_lvl; } bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; } - bool at_base_lvl() const override { return m_scope_lvl == 0; } + bool at_base_lvl() const { return m_scope_lvl == 0; } lbool value(literal l) const { return m_assignment[l.index()]; } lbool value(bool_var v) const { return m_assignment[literal(v, false).index()]; } justification get_justification(literal l) const { return m_justification[l.var()]; } justification get_justification(bool_var v) const { return m_justification[v]; } unsigned lvl(bool_var v) const { return m_justification[v].level(); } unsigned lvl(literal l) const { return m_justification[l.var()].level(); } - unsigned init_trail_size() const override { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; } unsigned trail_size() const { return m_trail.size(); } - literal trail_literal(unsigned i) const override { return m_trail[i]; } literal scope_literal(unsigned n) const { return m_trail[m_scopes[n].m_trail_lim]; } void assign(literal l, justification j) { TRACE("sat_assign", tout << l << " previous value: " << value(l) << " j: " << j << "\n";); @@ -430,7 +434,7 @@ namespace sat { bool canceled() { return !m_rlimit.inc(); } config const& get_config() const { return m_config; } drat& get_drat() { return m_drat; } - drat* get_drat_ptr() override { return &m_drat; } + drat* get_drat_ptr() { return &m_drat; } void set_incremental(bool b) { m_config.m_incremental = b; } bool is_incremental() const { return m_config.m_incremental; } extension* get_extension() const override { return m_ext.get(); } @@ -472,15 +476,37 @@ namespace sat { // // ----------------------- public: - lbool check(unsigned num_lits = 0, literal const* lits = nullptr) override; + lbool check(unsigned num_lits = 0, literal const* lits = nullptr); - model const & get_model() const override { return m_model; } + // retrieve model if solver return sat + model const & get_model() const { return m_model; } bool model_is_current() const { return m_model_is_current; } - literal_vector const& get_core() const override { return m_core; } + + // retrieve core from assumptions + literal_vector const& get_core() const { return m_core; } + model_converter const & get_model_converter() const { return m_mc; } - void flush(model_converter& mc) override { mc.flush(m_mc); } + + // The following methods are used when converting the state from the SAT solver back + // to a set of assertions. + + // retrieve model converter that handles variable elimination and other transformations + void flush(model_converter& mc) { mc.flush(m_mc); } + + // size of initial trail containing unit clauses + unsigned init_trail_size() const { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; } + + // literal at trail index i + literal trail_literal(unsigned i) const { return m_trail[i]; } + + // collect n-ary clauses + clause_vector const& clauses() const { return m_clauses; } + + // collect binary clauses + void collect_bin_clauses(svector & r, bool learned, bool learned_only) const; + void set_model(model const& mdl, bool is_current); - char const* get_reason_unknown() const override { return m_reason_unknown.c_str(); } + char const* get_reason_unknown() const { return m_reason_unknown.c_str(); } bool check_clauses(model const& m) const; bool is_assumption(bool_var v) const; void set_activity(bool_var v, unsigned act); @@ -688,7 +714,7 @@ namespace sat { public: void user_push() override; void user_pop(unsigned num_scopes) override; - void pop_to_base_level() override; + void pop_to_base_level(); unsigned num_user_scopes() const override { return m_user_scope_literals.size(); } unsigned num_scopes() const override { return m_scopes.size(); } reslimit& rlimit() { return m_rlimit; } @@ -788,8 +814,6 @@ namespace sat { clause * const * begin_learned() const { return m_learned.begin(); } clause * const * end_learned() const { return m_learned.end(); } clause_vector const& learned() const { return m_learned; } - clause_vector const& clauses() const override { return m_clauses; } - void collect_bin_clauses(svector & r, bool learned, bool learned_only) const override; // ----------------------- @@ -798,11 +822,11 @@ namespace sat { // // ----------------------- public: - bool check_invariant() const override; + bool check_invariant() const; void display(std::ostream & out) const; void display_watches(std::ostream & out) const; void display_watches(std::ostream & out, literal lit) const; - void display_dimacs(std::ostream & out) const override; + void display_dimacs(std::ostream & out) const; std::ostream& display_model(std::ostream& out) const; void display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const; void display_assignment(std::ostream & out) const; diff --git a/src/sat/sat_solver_core.h b/src/sat/sat_solver_core.h index 3be1aa1927f..ca66003cb7b 100644 --- a/src/sat/sat_solver_core.h +++ b/src/sat/sat_solver_core.h @@ -25,7 +25,6 @@ namespace sat { class cut_simplifier; class extension; - class drat; class solver_core { protected: @@ -34,27 +33,6 @@ namespace sat { solver_core(reslimit& l) : m_rlimit(l) {} virtual ~solver_core() {} - virtual void pop_to_base_level() {} - virtual bool at_base_lvl() const { return true; } - - // retrieve model if solver return sat - virtual model const & get_model() const = 0; - - // retrieve core from assumptions - virtual literal_vector const& get_core() const = 0; - - // is the state inconsistent? - virtual bool inconsistent() const = 0; - - // number of variables and clauses - virtual unsigned num_vars() const = 0; - virtual unsigned num_clauses() const = 0; - - // check satisfiability - virtual lbool check(unsigned num_lits = 0, literal const* lits = nullptr) = 0; - - virtual char const* get_reason_unknown() const { return "reason unavailable"; } - // add clauses virtual void add_clause(unsigned n, literal* lits, status st) = 0; void add_clause(literal l1, literal l2, status st) { @@ -68,18 +46,7 @@ namespace sat { // create boolean variable, tagged as external (= true) or internal (can be eliminated). virtual bool_var add_var(bool ext) = 0; - // update parameters - virtual void updt_params(params_ref const& p) {} - - - virtual bool check_invariant() const { return true; } - virtual void display_status(std::ostream& out) const {} - virtual void display_dimacs(std::ostream& out) const {} - - virtual bool is_external(bool_var v) const { return true; } - bool is_external(literal l) const { return is_external(l.var()); } virtual void set_external(bool_var v) {} - virtual void set_non_external(bool_var v) {} virtual void set_eliminated(bool_var v, bool f) {} virtual void set_phase(literal l) { } @@ -96,32 +63,6 @@ namespace sat { virtual void set_extension(extension* e) { if (e) throw default_exception("optional API not supported"); } virtual cut_simplifier* get_cut_simplifier() { return nullptr; } - - virtual drat* get_drat_ptr() { return nullptr; } - - - // The following methods are used when converting the state from the SAT solver back - // to a set of assertions. - - // retrieve model converter that handles variable elimination and other transformations - virtual void flush(model_converter& mc) {} - - // size of initial trail containing unit clauses - virtual unsigned init_trail_size() const = 0; - - // literal at trail index i - virtual literal trail_literal(unsigned i) const = 0; - - // collect n-ary clauses - virtual clause_vector const& clauses() const = 0; - - // collect binary clauses - typedef std::pair bin_clause; - virtual void collect_bin_clauses(svector & r, bool learned, bool learned_only) const = 0; - - // collect statistics from sat solver - virtual void collect_statistics(statistics & st) const {} - }; }; diff --git a/src/sat/tactic/sat2goal.cpp b/src/sat/tactic/sat2goal.cpp index 3fbcc50ee0b..482e441efb3 100644 --- a/src/sat/tactic/sat2goal.cpp +++ b/src/sat/tactic/sat2goal.cpp @@ -49,7 +49,7 @@ Module Name: sat2goal::mc::mc(ast_manager& m): m(m), m_var2expr(m) {} -void sat2goal::mc::flush_smc(sat::solver_core& s, atom2bool_var const& map) { +void sat2goal::mc::flush_smc(sat::solver& s, atom2bool_var const& map) { s.flush(m_smc); m_var2expr.resize(s.num_vars()); map.mk_var_inv(m_var2expr); @@ -223,7 +223,7 @@ struct sat2goal::imp { return m_lit2expr.get(l.index()); } - void assert_clauses(ref& mc, sat::solver_core const & s, sat::clause_vector const& clauses, goal & r, bool asserted) { + void assert_clauses(ref& mc, sat::solver const & s, sat::clause_vector const& clauses, goal & r, bool asserted) { ptr_buffer lits; unsigned small_lbd = 3; // s.get_config().m_gc_small_lbd; for (sat::clause* cp : clauses) { @@ -239,7 +239,7 @@ struct sat2goal::imp { } } - void operator()(sat::solver_core & s, atom2bool_var const & map, goal & r, ref & mc) { + void operator()(sat::solver & s, atom2bool_var const & map, goal & r, ref & mc) { if (s.at_base_lvl() && s.inconsistent()) { r.assert_expr(m.mk_false()); return; @@ -323,7 +323,7 @@ struct sat2goal::scoped_set_imp { } }; -void sat2goal::operator()(sat::solver_core & t, atom2bool_var const & m, params_ref const & p, +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); diff --git a/src/sat/tactic/sat2goal.h b/src/sat/tactic/sat2goal.h index 969b66e2396..b911f7b47ce 100644 --- a/src/sat/tactic/sat2goal.h +++ b/src/sat/tactic/sat2goal.h @@ -30,7 +30,7 @@ Module Name: #include "tactic/goal.h" #include "sat/sat_model_converter.h" -#include "sat/sat_solver_core.h" +#include "sat/sat_solver.h" #include "tactic/generic_model_converter.h" #include "sat/smt/atom2bool_var.h" @@ -53,7 +53,7 @@ class sat2goal { mc(ast_manager& m); ~mc() override {} // flush model converter from SAT solver to this structure. - void flush_smc(sat::solver_core& s, atom2bool_var const& map); + void flush_smc(sat::solver& s, atom2bool_var const& map); void operator()(sat::model& m); void operator()(model_ref& md) override; void operator()(expr_ref& fml) override; @@ -79,6 +79,6 @@ class sat2goal { \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_core & t, atom2bool_var const & m, params_ref const & p, goal & s, ref & mc); + 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 bbea0960431..521a70fb77b 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -30,7 +30,7 @@ class sat_tactic : public tactic { ast_manager & m; goal2sat m_goal2sat; sat2goal m_sat2goal; - scoped_ptr m_solver; + scoped_ptr m_solver; params_ref m_params; imp(ast_manager & _m, params_ref const & p):