From dd0decfe5d6c11780a04ba3eec971fc42e1010c3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 30 Jan 2023 16:12:25 -0800 Subject: [PATCH] create simplifier_solver wrapper to supply simplifier layer move sat_smt_preprocess to solver fix bugs in model_reconstruction_trail for dependency replay This is a preparatory step for exposing pre-processing as tactics. --- scripts/mk_project.py | 6 +- src/CMakeLists.txt | 4 +- .../simplifiers/model_reconstruction_trail.h | 6 +- src/sat/sat_solver/CMakeLists.txt | 1 - src/sat/sat_solver/sat_smt_preprocess.cpp | 106 ------ src/sat/sat_solver/sat_smt_solver.cpp | 173 +++------- src/solver/CMakeLists.txt | 4 + src/solver/simplifier_solver.cpp | 317 ++++++++++++++++++ src/solver/simplifier_solver.h | 25 ++ src/solver/solver_preprocess.cpp | 78 +++++ .../solver_preprocess.h} | 2 +- 11 files changed, 474 insertions(+), 248 deletions(-) delete mode 100644 src/sat/sat_solver/sat_smt_preprocess.cpp create mode 100644 src/solver/simplifier_solver.cpp create mode 100644 src/solver/simplifier_solver.h create mode 100644 src/solver/solver_preprocess.cpp rename src/{sat/sat_solver/sat_smt_preprocess.h => solver/solver_preprocess.h} (94%) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index e87c36d85..44e436daf 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -41,7 +41,9 @@ def init_project_def(): add_lib('converters', ['model'], 'ast/converters') add_lib('simplifiers', ['euf', 'normal_forms', 'bit_blaster', 'converters', 'substitution'], 'ast/simplifiers') add_lib('tactic', ['simplifiers']) - add_lib('solver', ['params', 'model', 'tactic', 'proofs']) + add_lib('mbp', ['model', 'simplex'], 'qe/mbp') + add_lib('qe_lite', ['tactic', 'mbp'], 'qe/lite') + add_lib('solver', ['params', 'smt_params', 'model', 'tactic', 'qe_lite', 'proofs']) add_lib('cmd_context', ['solver', 'rewriter', 'params']) add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2') add_lib('pattern', ['normal_forms', 'smt2parser', 'rewriter'], 'ast/pattern') @@ -50,8 +52,6 @@ def init_project_def(): add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa') add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern'], 'tactic/core') add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith') - add_lib('mbp', ['model', 'simplex'], 'qe/mbp') - add_lib('qe_lite', ['tactic', 'mbp'], 'qe/lite') add_lib('solver_assertions', ['pattern','smt_params','cmd_context','qe_lite'], 'solver/assertions') add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 652aef4ac..e091db15f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -55,6 +55,8 @@ add_subdirectory(ast/converters) add_subdirectory(ast/substitution) add_subdirectory(ast/simplifiers) add_subdirectory(tactic) +add_subdirectory(qe/mbp) +add_subdirectory(qe/lite) add_subdirectory(smt/params) add_subdirectory(parsers/util) add_subdirectory(math/grobner) @@ -68,8 +70,6 @@ add_subdirectory(solver) add_subdirectory(cmd_context) add_subdirectory(cmd_context/extra_cmds) add_subdirectory(parsers/smt2) -add_subdirectory(qe/mbp) -add_subdirectory(qe/lite) add_subdirectory(solver/assertions) add_subdirectory(ast/pattern) add_subdirectory(math/lp) diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h index c1b045a43..36ddde9ff 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.h +++ b/src/ast/simplifiers/model_reconstruction_trail.h @@ -70,7 +70,7 @@ class model_reconstruction_trail { return true; if (m_subst) { for (auto const& [k, v] : m_subst->sub()) - if (free_vars.is_marked(k)) + if (free_vars.is_marked(to_app(k)->get_decl())) return true; } return false; @@ -88,8 +88,10 @@ class model_reconstruction_trail { void add_vars(expr* e, ast_mark& free_vars) { for (expr* t : subterms::all(expr_ref(e, m))) - if (is_app(t)) + if (is_app(t) && is_uninterp(t)) { + TRACE("simplifier", tout << "add var " << to_app(t)->get_decl()->get_name() << "\n"); free_vars.mark(to_app(t)->get_decl(), true); + } } void add_vars(dependent_expr const& d, ast_mark& free_vars) { diff --git a/src/sat/sat_solver/CMakeLists.txt b/src/sat/sat_solver/CMakeLists.txt index 725ca16f7..ad26aceab 100644 --- a/src/sat/sat_solver/CMakeLists.txt +++ b/src/sat/sat_solver/CMakeLists.txt @@ -1,7 +1,6 @@ z3_add_component(sat_solver SOURCES inc_sat_solver.cpp - sat_smt_preprocess.cpp sat_smt_solver.cpp COMPONENT_DEPENDENCIES aig_tactic diff --git a/src/sat/sat_solver/sat_smt_preprocess.cpp b/src/sat/sat_solver/sat_smt_preprocess.cpp deleted file mode 100644 index 02c6e88b4..000000000 --- a/src/sat/sat_solver/sat_smt_preprocess.cpp +++ /dev/null @@ -1,106 +0,0 @@ -/*++ -Copyright (c) 2022 Microsoft Corporation - -Module Name: - - sat_smt_preprocess.cpp - -Abstract: - - SAT pre-process - -Author: - - Nikolaj Bjorner (nbjorner) 2022-11-28 - ---*/ - - -#include "ast/rewriter/rewriter_def.h" -#include "ast/simplifiers/bit_blaster.h" -#include "ast/simplifiers/max_bv_sharing.h" -#include "ast/simplifiers/card2bv.h" -#include "ast/simplifiers/propagate_values.h" -#include "ast/simplifiers/rewriter_simplifier.h" -#include "ast/simplifiers/solve_eqs.h" -#include "ast/simplifiers/bv_slice.h" -#include "ast/simplifiers/eliminate_predicates.h" -#include "ast/simplifiers/elim_unconstrained.h" -#include "ast/simplifiers/pull_nested_quantifiers.h" -#include "ast/simplifiers/distribute_forall.h" -#include "ast/simplifiers/refine_inj_axiom.h" -#include "ast/simplifiers/elim_bounds.h" -#include "ast/simplifiers/bit2int.h" -#include "ast/simplifiers/bv_elim.h" -#include "ast/simplifiers/push_ite.h" -#include "ast/simplifiers/elim_term_ite.h" -#include "ast/simplifiers/flatten_clauses.h" -#include "ast/simplifiers/cnf_nnf.h" -#include "sat/sat_params.hpp" -#include "smt/params/smt_params.h" -#include "sat/sat_solver/sat_smt_preprocess.h" -#include "qe/lite/qe_lite.h" - -void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dependent_expr_state& st) { - - sat_params sp(p); - smt_params smtp(p); - if (sp.euf() || sp.smt()) { - s.add_simplifier(alloc(rewriter_simplifier, m, p, st)); - if (smtp.m_propagate_values) s.add_simplifier(alloc(propagate_values, m, p, st)); - if (smtp.m_solve_eqs) s.add_simplifier(alloc(euf::solve_eqs, m, st)); - if (smtp.m_elim_unconstrained) s.add_simplifier(alloc(elim_unconstrained, m, st)); - if (smtp.m_nnf_cnf) s.add_simplifier(alloc(cnf_nnf_simplifier, m, p, st)); - if (smtp.m_macro_finder || smtp.m_quasi_macros) s.add_simplifier(alloc(eliminate_predicates, m, st)); - if (smtp.m_qe_lite) s.add_simplifier(mk_qe_lite_simplifer(m, p, st)); - if (smtp.m_pull_nested_quantifiers) s.add_simplifier(alloc(pull_nested_quantifiers_simplifier, m, p, st)); - if (smtp.m_max_bv_sharing) s.add_simplifier(mk_max_bv_sharing(m, p, st)); - if (smtp.m_refine_inj_axiom) s.add_simplifier(alloc(refine_inj_axiom_simplifier, m, p, st)); - if (smtp.m_bv_size_reduce) s.add_simplifier(alloc(bv::slice, m, st)); - if (smtp.m_distribute_forall) s.add_simplifier(alloc(distribute_forall_simplifier, m, p, st)); - if (smtp.m_eliminate_bounds) s.add_simplifier(alloc(elim_bounds_simplifier, m, p, st)); - if (smtp.m_simplify_bit2int) s.add_simplifier(alloc(bit2int_simplifier, m, p, st)); - if (smtp.m_bb_quantifiers) s.add_simplifier(alloc(bv::elim_simplifier, m, p, st)); - if (smtp.m_eliminate_term_ite && smtp.m_lift_ite != lift_ite_kind::LI_FULL) s.add_simplifier(alloc(elim_term_ite_simplifier, m, p, st)); - if (smtp.m_lift_ite != lift_ite_kind::LI_NONE) s.add_simplifier(alloc(push_ite_simplifier, m, p, st, smtp.m_lift_ite == lift_ite_kind::LI_CONSERVATIVE)); - if (smtp.m_ng_lift_ite != lift_ite_kind::LI_NONE) s.add_simplifier(alloc(ng_push_ite_simplifier, m, p, st, smtp.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE)); - s.add_simplifier(alloc(flatten_clauses, m, p, st)); - - // - // add: - // euf_completion? - // - // add: make it externally programmable - // -#if 0 - if (!invoke(m_apply_quasi_macros)) return; -#endif - - } - else { - params_ref simp1_p = p; - simp1_p.set_bool("som", true); - simp1_p.set_bool("pull_cheap_ite", true); - simp1_p.set_bool("push_ite_bv", false); - simp1_p.set_bool("local_ctx", true); - simp1_p.set_uint("local_ctx_limit", 10000000); - simp1_p.set_bool("flat", true); // required by som - simp1_p.set_bool("hoist_mul", false); // required by som - simp1_p.set_bool("elim_and", true); - simp1_p.set_bool("blast_distinct", true); - simp1_p.set_bool("flat_and_or", false); - - params_ref simp2_p = p; - simp2_p.set_bool("flat", false); - simp2_p.set_bool("flat_and_or", false); - - s.add_simplifier(alloc(rewriter_simplifier, m, p, st)); - s.add_simplifier(alloc(propagate_values, m, p, st)); - s.add_simplifier(alloc(card2bv, m, p, st)); - s.add_simplifier(alloc(rewriter_simplifier, m, simp1_p, st)); - s.add_simplifier(mk_max_bv_sharing(m, p, st)); - s.add_simplifier(alloc(bit_blaster_simplifier, m, p, st)); - s.add_simplifier(alloc(rewriter_simplifier, m, simp2_p, st)); - } -} - diff --git a/src/sat/sat_solver/sat_smt_solver.cpp b/src/sat/sat_solver/sat_smt_solver.cpp index 4e5f8fd37..dbc2d9505 100644 --- a/src/sat/sat_solver/sat_smt_solver.cpp +++ b/src/sat/sat_solver/sat_smt_solver.cpp @@ -17,14 +17,10 @@ Author: Notes: - - add translation for preprocess state. - - If the pre-processors are stateful, they need to be properly translated. + - add back get_consequences, maybe or just have them handled by inc_sat_solver - could also port the layered solver used by smtfd and used by get_consequences to simplifiers - - port various pre-processing to simplifiers - - qe-lite, fm-elimination, ite-lifting, other from asserted_formulas - --*/ @@ -36,7 +32,7 @@ Notes: #include "model/model_smt2_pp.h" #include "model/model_evaluator.h" #include "sat/sat_solver.h" -#include "sat/sat_solver/sat_smt_preprocess.h" +#include "solver/simplifier_solver.h" #include "sat/sat_params.hpp" #include "sat/smt/euf_solver.h" #include "sat/tactic/goal2sat.h" @@ -47,54 +43,6 @@ Notes: // incremental SAT solver. class sat_smt_solver : public solver { - struct dep_expr_state : public dependent_expr_state { - sat_smt_solver& s; - model_reconstruction_trail m_reconstruction_trail; - dep_expr_state(sat_smt_solver& s):dependent_expr_state(s.m), s(s), m_reconstruction_trail(s.m, m_trail) {} - ~dep_expr_state() override {} - virtual unsigned qtail() const override { return s.m_fmls.size(); } - dependent_expr const& operator[](unsigned i) override { return s.m_fmls[i]; } - void update(unsigned i, dependent_expr const& j) override { SASSERT(j.fml()); s.m_fmls[i] = j; } - void add(dependent_expr const& j) override { s.m_fmls.push_back(j); } - bool inconsistent() override { return s.m_solver.inconsistent(); } - model_reconstruction_trail& model_trail() override { return m_reconstruction_trail; } - std::ostream& display(std::ostream& out) const override { - unsigned i = 0; - for (auto const& d : s.m_fmls) { - if (i > 0 && i == qhead()) - out << "---- head ---\n"; - out << d << "\n"; - ++i; - } - m_reconstruction_trail.display(out); - return out; - } - void append(generic_model_converter& mc) { model_trail().append(mc); } - void replay(unsigned qhead, expr_ref_vector& assumptions) { m_reconstruction_trail.replay(qhead, assumptions, *this); } - void flatten_suffix() override { - expr_mark seen; - unsigned j = qhead(); - for (unsigned i = qhead(); i < qtail(); ++i) { - expr* f = s.m_fmls[i].fml(); - if (seen.is_marked(f)) - continue; - seen.mark(f, true); - if (s.m.is_true(f)) - continue; - if (s.m.is_and(f)) { - auto* d = s.m_fmls[i].dep(); - for (expr* arg : *to_app(f)) - s.m_fmls.push_back(dependent_expr(s.m, arg, nullptr, d)); - continue; - } - if (i != j) - s.m_fmls[j] = s.m_fmls[i]; - ++j; - } - s.m_fmls.shrink(j); - } - }; - struct dependency2assumptions { ast_manager& m; trail_stack& m_trail; @@ -152,15 +100,12 @@ class sat_smt_solver : public solver { mutable sat::solver m_solver; params_ref m_params; - vector m_fmls; - dep_expr_state m_preprocess_state; - seq_simplifier m_preprocess; - trail_stack& m_trail; + trail_stack m_trail; dependency2assumptions m_dep; goal2sat m_goal2sat; - expr_ref_vector m_assumptions, m_core, m_ors, m_aux_fmls, m_internalized_fmls; + unsigned m_qhead = 0; + expr_ref_vector m_assumptions, m_core, m_ors, m_fmls, m_internalized_fmls; atom2bool_var m_map; - generic_model_converter_ref m_mc; mutable model_converter_ref m_cached_mc; mutable ref m_sat_mc; std::string m_unknown = "no reason given"; @@ -168,20 +113,16 @@ class sat_smt_solver : public solver { // this allows to access the internal state of the SAT solver and carry on partial results. bool m_internalized_converted = false; // have internalized formulas been converted back - bool is_internalized() const { return m_preprocess_state.qhead() == m_fmls.size(); } + bool is_internalized() const { return m_qhead == m_fmls.size(); } public: sat_smt_solver(ast_manager& m, params_ref const& p): solver(m), m_solver(p, m.limit()), - m_preprocess_state(*this), - m_preprocess(m, p, m_preprocess_state), - m_trail(m_preprocess_state.m_trail), m_dep(m, m_trail), - m_assumptions(m), m_core(m), m_ors(m), m_aux_fmls(m), m_internalized_fmls(m), + m_assumptions(m), m_core(m), m_ors(m), m_fmls(m), m_internalized_fmls(m), m_map(m) { updt_params(p); - init_preprocess(); m_solver.set_incremental(true); } @@ -203,13 +144,10 @@ public: } // TODO: copy preprocess state for (auto const& [k, v] : m_dep.m_dep2orig) result->m_dep.insert(tr(v), tr(k)); - for (dependent_expr const& f : m_fmls) result->m_fmls.push_back(dependent_expr(tr, f)); for (expr* f : m_assumptions) result->m_assumptions.push_back(tr(f)); for (auto & kv : m_map) result->m_map.insert(tr(kv.m_key), kv.m_value); for (expr* f : m_internalized_fmls) result->m_internalized_fmls.push_back(tr(f)); - if (m_mc) result->m_mc = dynamic_cast(m_mc->translate(tr)); result->m_dep.copy(tr, m_dep); - if (m_sat_mc) result->m_sat_mc = dynamic_cast(m_sat_mc->translate(tr)); result->m_internalized_converted = m_internalized_converted; return result; } @@ -234,8 +172,6 @@ public: expr_ref_vector assumptions(m); for (unsigned i = 0; i < sz; ++i) assumptions.push_back(ensure_literal(_assumptions[i])); - for (expr* a : assumptions) - m_preprocess_state.freeze(a); TRACE("sat", tout << assumptions << "\n";); lbool r = internalize_formulas(assumptions); if (r != l_true) @@ -284,17 +220,15 @@ public: m_solver.user_push(); m_goal2sat.user_push(); m_map.push(); - m_preprocess_state.push(); - m_preprocess.push(); + m_trail.push_scope(); m_trail.push(restore_vector(m_assumptions)); m_trail.push(restore_vector(m_fmls)); + m_trail.push(value_trail(m_qhead)); } void pop(unsigned n) override { n = std::min(n, m_trail.get_num_scopes()); // allow sat_smt_solver to take over for another solver. - - m_preprocess.pop(n); - m_preprocess_state.pop(n); + m_trail.pop_scope(n); m_map.pop(n); m_goal2sat.user_pop(n); m_solver.user_pop(n); @@ -345,18 +279,32 @@ public: return a; expr* new_dep = m.mk_fresh_const("dep", m.mk_bool_sort()); expr* fml = m.mk_iff(new_dep, a); - m_fmls.push_back(dependent_expr(m, fml, nullptr, nullptr)); + m_fmls.push_back(fml); m_dep.insert(a, new_dep); return new_dep; } void assert_expr_core2(expr * t, expr * a) override { - a = ensure_literal(a); - m_fmls.push_back(dependent_expr(m, t, nullptr, m.mk_leaf(a))); + m_ors.reset(); + m_ors.push_back(t); + if (m.is_and(a)) { + for (expr* arg : *to_app(a)) { + arg = ensure_literal(arg); + m_ors.push_back(mk_not(m, arg)); + m_assumptions.push_back(arg); + } + } + else { + a = ensure_literal(a); + m_assumptions.push_back(a); + m_ors.push_back(mk_not(m, a)); + } + flatten_or(m_ors); + m_fmls.push_back(mk_or(m_ors)); } void assert_expr_core(expr * t) override { - m_fmls.push_back(dependent_expr(m, t, nullptr, nullptr)); + m_fmls.push_back(t); } ast_manager& get_manager() const override { return m; } @@ -367,7 +315,6 @@ public: solver::collect_param_descrs(r); goal2sat::collect_param_descrs(r); sat::solver::collect_param_descrs(r); - m_preprocess.collect_param_descrs(r); } void updt_params(params_ref const & p) override { @@ -377,13 +324,11 @@ public: m_params.set_sym("pb.solver", sp.pb_solver()); m_solver.updt_params(m_params); m_solver.set_incremental(true); - m_preprocess.updt_params(m_params); if (sp.smt()) ensure_euf(); } void collect_statistics(statistics & st) const override { - m_preprocess.collect_statistics(st); m_solver.collect_statistics(st); } @@ -531,7 +476,7 @@ public: expr * get_assertion(unsigned idx) const override { if (is_internalized() && m_internalized_converted) return m_internalized_fmls[idx]; - return m_fmls[idx].fml(); + return m_fmls.get(idx); } unsigned get_num_assumptions() const override { @@ -549,7 +494,7 @@ public: return m_cached_mc; if (is_internalized() && m_internalized_converted) { if (m_sat_mc) m_sat_mc->flush_smc(m_solver, m_map); - m_cached_mc = concat(solver::get_model_converter().get(), m_mc.get(), m_sat_mc.get()); + m_cached_mc = concat(solver::get_model_converter().get(), m_sat_mc.get()); TRACE("sat", m_cached_mc->display(tout);); return m_cached_mc; } @@ -574,10 +519,6 @@ public: m_internalized_converted = true; } - void init_preprocess() { - ::init_preprocess(m, m_params, m_preprocess, m_preprocess_state); - } - euf::solver* get_euf() { return dynamic_cast(m_solver.get_extension()); } @@ -646,50 +587,20 @@ private: if (is_internalized() && assumptions.empty()) return l_true; - unsigned qhead = m_preprocess_state.qhead(); - TRACE("sat", tout << "qhead " << qhead << "\n"); + TRACE("sat", tout << "qhead " << m_qhead << "\n"); m_internalized_converted = false; - m_preprocess_state.replay(qhead, assumptions); - m_preprocess.reduce(); - if (!m.inc()) - return l_undef; - m_preprocess_state.advance_qhead(); - m_mc = alloc(generic_model_converter, m, "sat-model-converter"); - m_preprocess_state.append(*m_mc); m_solver.pop_to_base_level(); - m_aux_fmls.reset(); - for (; qhead < m_fmls.size(); ++qhead) - add_with_dependency(m_fmls[qhead]); init_goal2sat(); - m_goal2sat(m_aux_fmls.size(), m_aux_fmls.data()); + m_goal2sat(m_fmls.size() - m_qhead, m_fmls.data() + m_qhead); if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m); m_sat_mc->flush_smc(m_solver, m_map); + m_qhead = m_fmls.size(); return m.inc() ? l_true : l_undef; } - ptr_vector m_deps; - void add_with_dependency(dependent_expr const& de) { - if (!de.dep()) { - m_aux_fmls.push_back(de.fml()); - return; - } - m_deps.reset(); - m.linearize(de.dep(), m_deps); - m_ors.reset(); - m_ors.push_back(de.fml()); - flatten_or(m_ors); - for (expr* d : m_deps) { - SASSERT(m.is_bool(d)); - SASSERT(is_literal(d)); - m_assumptions.push_back(d); - m_ors.push_back(mk_not(m, d)); - } - m_aux_fmls.push_back(mk_or(m_ors)); - } - void extract_core() { m_core.reset(); if (m_dep.m_literals.empty()) @@ -720,7 +631,7 @@ private: mdl = nullptr; if (!m_solver.model_is_current()) return; - if (m_fmls.size() > m_preprocess_state.qhead()) + if (m_fmls.size() > m_qhead) return; TRACE("sat", m_solver.display_model(tout);); CTRACE("sat", m_sat_mc, m_sat_mc->display(tout);); @@ -751,7 +662,6 @@ private: if (m_sat_mc) (*m_sat_mc)(mdl); m_goal2sat.update_model(mdl); - TRACE("sat", model_smt2_pp(tout, m, *mdl, 0);); @@ -760,25 +670,24 @@ private: model_evaluator eval(*mdl); eval.set_model_completion(true); bool all_true = true; - for (dependent_expr const& d : m_fmls) { - if (has_quantifiers(d.fml())) + for (expr* f : m_fmls) { + if (has_quantifiers(f)) continue; expr_ref tmp(m); - eval(d.fml(), tmp); + eval(f, tmp); if (m.limit().is_canceled()) return; CTRACE("sat", !m.is_true(tmp), - tout << "Evaluation failed: " << mk_pp(d.fml(), m) << " to " << tmp << "\n"; + tout << "Evaluation failed: " << mk_pp(f, m) << " to " << tmp << "\n"; model_smt2_pp(tout, m, *(mdl.get()), 0);); if (m.is_false(tmp)) { - IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(d.fml(), m) << "\n"); + IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(f, m) << "\n"); IF_VERBOSE(0, verbose_stream() << "evaluated to " << tmp << "\n"); all_true = false; } } if (!all_true) { IF_VERBOSE(0, verbose_stream() << m_params << "\n"); - IF_VERBOSE(0, if (m_mc) m_mc->display(verbose_stream() << "mc0\n")); IF_VERBOSE(0, for (auto const& kv : m_map) verbose_stream() << mk_pp(kv.m_key, m) << " |-> " << kv.m_value << "\n"); exit(0); } @@ -786,13 +695,11 @@ private: IF_VERBOSE(1, verbose_stream() << "solution verified\n"); } } - TRACE("sat", m_mc->display(tout);); - (*m_mc)(mdl); } }; solver* mk_sat_smt_solver(ast_manager& m, params_ref const& p) { - return alloc(sat_smt_solver, m, p); + return mk_simplifier_solver(alloc(sat_smt_solver, m, p)); } diff --git a/src/solver/CMakeLists.txt b/src/solver/CMakeLists.txt index 3bea76dd0..088f2cbb2 100644 --- a/src/solver/CMakeLists.txt +++ b/src/solver/CMakeLists.txt @@ -5,15 +5,19 @@ z3_add_component(solver combined_solver.cpp mus.cpp parallel_tactical.cpp + simplifier_solver.cpp smt_logics.cpp solver.cpp solver_na2as.cpp solver_pool.cpp + solver_preprocess.cpp solver2tactic.cpp tactic2solver.cpp COMPONENT_DEPENDENCIES model tactic + smt_params + qe_lite PYG_FILES combined_solver_params.pyg parallel_params.pyg diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp new file mode 100644 index 000000000..17a39509e --- /dev/null +++ b/src/solver/simplifier_solver.cpp @@ -0,0 +1,317 @@ +/*++ +Copyright (c) 2023 Microsoft Corporation + +Module Name: + + simplifier_solver.cpp + +Abstract: + + Implements a solver with simplifying pre-processing. + +Author: + + Nikolaj Bjorner (nbjorner) 2023-01-30 + + Notes: + + - add translation for preprocess state. + - If the pre-processors are stateful, they need to be properly translated. + +--*/ +#include "util/params.h" +#include "ast/ast_util.h" +#include "ast/rewriter/expr_safe_replace.h" +#include "ast/simplifiers/dependent_expr_state.h" +#include "ast/simplifiers/seq_simplifier.h" +#include "solver/solver.h" +#include "solver/simplifier_solver.h" +#include "solver/solver_preprocess.h" + + +class simplifier_solver : public solver { + + + struct dep_expr_state : public dependent_expr_state { + simplifier_solver& s; + model_reconstruction_trail m_reconstruction_trail; + dep_expr_state(simplifier_solver& s) :dependent_expr_state(s.m), s(s), m_reconstruction_trail(s.m, m_trail) {} + ~dep_expr_state() override {} + virtual unsigned qtail() const override { return s.m_fmls.size(); } + dependent_expr const& operator[](unsigned i) override { return s.m_fmls[i]; } + void update(unsigned i, dependent_expr const& j) override { + SASSERT(j.fml()); + check_false(j.fml()); + s.m_fmls[i] = j; + } + void add(dependent_expr const& j) override { check_false(j.fml()); s.m_fmls.push_back(j); } + bool inconsistent() override { return s.m_inconsistent; } + model_reconstruction_trail& model_trail() override { return m_reconstruction_trail; } + std::ostream& display(std::ostream& out) const override { + unsigned i = 0; + for (auto const& d : s.m_fmls) { + if (i > 0 && i == qhead()) + out << "---- head ---\n"; + out << d << "\n"; + ++i; + } + m_reconstruction_trail.display(out); + return out; + } + void check_false(expr* f) { + if (s.m.is_false(f)) + s.set_inconsistent(); + } + void append(generic_model_converter& mc) { model_trail().append(mc); } + void replay(unsigned qhead, expr_ref_vector& assumptions) { m_reconstruction_trail.replay(qhead, assumptions, *this); } + void flatten_suffix() override { + expr_mark seen; + unsigned j = qhead(); + for (unsigned i = qhead(); i < qtail(); ++i) { + expr* f = s.m_fmls[i].fml(); + if (seen.is_marked(f)) + continue; + seen.mark(f, true); + if (s.m.is_true(f)) + continue; + if (s.m.is_and(f)) { + auto* d = s.m_fmls[i].dep(); + for (expr* arg : *to_app(f)) + add(dependent_expr(s.m, arg, nullptr, d)); + continue; + } + if (i != j) + s.m_fmls[j] = s.m_fmls[i]; + ++j; + } + s.m_fmls.shrink(j); + } + }; + + ast_manager& m; + scoped_ptr s; + vector m_fmls; + dep_expr_state m_preprocess_state; + seq_simplifier m_preprocess; + expr_ref_vector m_assumptions; + generic_model_converter_ref m_mc; + bool m_inconsistent = false; + + void flush(expr_ref_vector& assumptions) { + unsigned qhead = m_preprocess_state.qhead(); + if (qhead < m_fmls.size()) { + for (expr* a : assumptions) + m_preprocess_state.freeze(a); + TRACE("solver", tout << "qhead " << qhead << "\n"); + m_preprocess_state.replay(qhead, assumptions); + m_preprocess.reduce(); + if (!m.inc()) + return; + m_preprocess_state.advance_qhead(); + } + m_mc = alloc(generic_model_converter, m, "simplifier-model-converter"); + m_cached_mc = nullptr; + m_preprocess_state.append(*m_mc); + for (; qhead < m_fmls.size(); ++qhead) + add_with_dependency(m_fmls[qhead]); + } + + ptr_vector m_deps; + void add_with_dependency(dependent_expr const& de) { + if (!de.dep()) { + s->assert_expr(de.fml()); + return; + } + m_deps.reset(); + m.linearize(de.dep(), m_deps); + m_assumptions.reset(); + for (expr* d : m_deps) + m_assumptions.push_back(d); + s->assert_expr(de.fml(), mk_and(m_assumptions)); + } + + bool inconsistent() const { + return m_inconsistent; + } + + void set_inconsistent() { + if (!m_inconsistent) { + m_preprocess_state.m_trail.push(value_trail(m_inconsistent)); + m_inconsistent = true; + } + } + +public: + + simplifier_solver(solver* s) : + solver(s->get_manager()), + m(s->get_manager()), + s(s), + m_preprocess_state(*this), + m_preprocess(m, s->get_params(), m_preprocess_state), + m_assumptions(m), + m_proof(m) + { + init_preprocess(m, s->get_params(), m_preprocess, m_preprocess_state); + } + + void assert_expr_core2(expr* t, expr* a) override { + m_cached_model = nullptr; + m_cached_mc = nullptr; + proof* pr = m.proofs_enabled() ? m.mk_asserted(t) : nullptr; + m_fmls.push_back(dependent_expr(m, t, pr, m.mk_leaf(a))); + } + + void assert_expr_core(expr* t) override { + m_cached_model = nullptr; + m_cached_mc = nullptr; + proof* pr = m.proofs_enabled() ? m.mk_asserted(t) : nullptr; + m_fmls.push_back(dependent_expr(m, t, pr, nullptr)); + } + + void push() override { + expr_ref_vector none(m); + flush(none); + m_preprocess_state.push(); + m_preprocess.push(); + m_preprocess_state.m_trail.push(restore_vector(m_fmls)); + s->push(); + } + + void pop(unsigned n) override { + s->pop(n); + m_cached_model = nullptr; + m_preprocess.pop(n); + m_preprocess_state.pop(n); + } + + lbool check_sat_core(unsigned num_assumptions, expr* const* assumptions) override { + expr_ref_vector _assumptions(m, num_assumptions, assumptions); + flush(_assumptions); + return s->check_sat_core(num_assumptions, assumptions); + } + + void collect_statistics(statistics& st) const override { + s->collect_statistics(st); + m_preprocess.collect_statistics(st); + } + + model_ref m_cached_model; + void get_model_core(model_ref& m) override { + if (m_cached_model) { + m = m_cached_model; + return; + } + s->get_model(m); + if (m_mc) + (*m_mc)(m); + m_cached_model = m; + } + + proof_ref m_proof; + proof* get_proof_core() { + proof* p = s->get_proof(); + m_proof = p; + if (p) { + expr_ref tmp(p, m); + expr_safe_replace sub(m); + for (auto const& d : m_fmls) { + if (d.pr()) + sub.insert(m.mk_asserted(d.fml()), d.pr()); + } + sub(tmp); + SASSERT(is_app(tmp)); + m_proof = to_app(tmp); + } + return m_proof; + } + + solver* translate(ast_manager& m, params_ref const& p) override { + solver* new_s = s->translate(m, p); + ast_translation tr(get_manager(), m); + simplifier_solver* result = alloc(simplifier_solver, new_s); + for (dependent_expr const& f : m_fmls) + result->m_fmls.push_back(dependent_expr(tr, f)); + if (m_mc) + result->m_mc = dynamic_cast(m_mc->translate(tr)); + + // copy m_preprocess_state? + return result; + } + + void updt_params(params_ref const& p) override { + s->updt_params(p); + m_preprocess.updt_params(p); + } + + mutable model_converter_ref m_cached_mc; + model_converter_ref get_model_converter() const override { + if (!m_cached_mc) + m_cached_mc = concat(solver::get_model_converter().get(), m_mc.get(), s->get_model_converter().get()); + return m_cached_mc; + } + + unsigned get_num_assertions() const override { return s->get_num_assertions(); } + expr* get_assertion(unsigned idx) const override { return s->get_assertion(idx); } + std::string reason_unknown() const override { return s->reason_unknown(); } + void set_reason_unknown(char const* msg) override { s->set_reason_unknown(msg); } + void get_labels(svector& r) override { s->get_labels(r); } + void get_unsat_core(expr_ref_vector& r) { s->get_unsat_core(r); } + ast_manager& get_manager() const override { return s->get_manager(); } + void reset_params(params_ref const& p) override { s->reset_params(p); } + params_ref const& get_params() const override { return s->get_params(); } + void collect_param_descrs(param_descrs& r) override { s->collect_param_descrs(r); } + void push_params() override { s->push_params(); } + void pop_params() override { s->pop_params(); } + void set_produce_models(bool f) override { s->set_produce_models(f); } + void set_phase(expr* e) override { s->set_phase(e); } + void move_to_front(expr* e) override { s->move_to_front(e); } + phase* get_phase() override { return s->get_phase(); } + void set_phase(phase* p) override { s->set_phase(p); } + unsigned get_num_assumptions() const override { return s->get_num_assumptions(); } + expr* get_assumption(unsigned idx) const override { return s->get_assumption(idx); } + unsigned get_scope_level() const override { return s->get_scope_level(); } + lbool check_sat_cc(expr_ref_vector const& cube, vector const& clauses) override { return check_sat_cc(cube, clauses); } + void set_progress_callback(progress_callback* callback) override { s->set_progress_callback(callback); } + lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) override { + return s->get_consequences(asms, vars, consequences); + } + lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) override { return s->find_mutexes(vars, mutexes); } + lbool preferred_sat(expr_ref_vector const& asms, vector& cores) override { return s->preferred_sat(asms, cores); } + + expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override { return s->cube(vars, backtrack_level); } + expr* congruence_root(expr* e) override { return s->congruence_root(e); } + expr* congruence_next(expr* e) override { return s->congruence_next(e); } + std::ostream& display(std::ostream& out, unsigned n, expr* const* assumptions) const override { + return s->display(out, n, assumptions); + } + void get_units_core(expr_ref_vector& units) override { s->get_units_core(units); } + expr_ref_vector get_trail(unsigned max_level) override { return s->get_trail(max_level); } + void get_levels(ptr_vector const& vars, unsigned_vector& depth) override { s->get_levels(vars, depth); } + + void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause) override { + s->register_on_clause(ctx, on_clause); + } + + void user_propagate_init( + void* ctx, + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh) override { + s->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); + } + void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) override { s->user_propagate_register_fixed(fixed_eh); } + void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override { s->user_propagate_register_final(final_eh); } + void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override { s->user_propagate_register_eq(eq_eh); } + void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override { s->user_propagate_register_diseq(diseq_eh); } + void user_propagate_register_expr(expr* e) override { /*m_preprocess.user_propagate_register_expr(e); */ s->user_propagate_register_expr(e); } + void user_propagate_register_created(user_propagator::created_eh_t& r) override { s->user_propagate_register_created(r); } + // void user_propagate_clear() override { m_preprocess.user_propagate_clear(); s->user_propagate_clear(); } + + +}; + +solver* mk_simplifier_solver(solver* s) { + return alloc(simplifier_solver, s); +} + diff --git a/src/solver/simplifier_solver.h b/src/solver/simplifier_solver.h new file mode 100644 index 000000000..3d97a3869 --- /dev/null +++ b/src/solver/simplifier_solver.h @@ -0,0 +1,25 @@ +/*++ +Copyright (c) 2023 Microsoft Corporation + +Module Name: + + simplifier_solver.cpp + +Abstract: + + Implements a solver with simplifying pre-processing. + +Author: + + Nikolaj Bjorner (nbjorner) 2023-01-30 + +--*/ +#pragma once + +#include "util/params.h" + +class solver; +class solver_factory; + +solver * mk_simplifier_solver(solver * s); + diff --git a/src/solver/solver_preprocess.cpp b/src/solver/solver_preprocess.cpp new file mode 100644 index 000000000..71c6d975a --- /dev/null +++ b/src/solver/solver_preprocess.cpp @@ -0,0 +1,78 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + solver_preprocess.cpp + +Abstract: + + pre-process initialization module for solver + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-28 + +Notes: + + - port various pre-processing to simplifiers + - qe-lite, fm-elimination, ite-lifting, other from asserted_formulas +--*/ + + +#include "ast/rewriter/rewriter_def.h" +#include "ast/simplifiers/bit_blaster.h" +#include "ast/simplifiers/max_bv_sharing.h" +#include "ast/simplifiers/card2bv.h" +#include "ast/simplifiers/propagate_values.h" +#include "ast/simplifiers/rewriter_simplifier.h" +#include "ast/simplifiers/solve_eqs.h" +#include "ast/simplifiers/bv_slice.h" +#include "ast/simplifiers/eliminate_predicates.h" +#include "ast/simplifiers/elim_unconstrained.h" +#include "ast/simplifiers/pull_nested_quantifiers.h" +#include "ast/simplifiers/distribute_forall.h" +#include "ast/simplifiers/refine_inj_axiom.h" +#include "ast/simplifiers/elim_bounds.h" +#include "ast/simplifiers/bit2int.h" +#include "ast/simplifiers/bv_elim.h" +#include "ast/simplifiers/push_ite.h" +#include "ast/simplifiers/elim_term_ite.h" +#include "ast/simplifiers/flatten_clauses.h" +#include "ast/simplifiers/cnf_nnf.h" +#include "smt/params/smt_params.h" +#include "solver/solver_preprocess.h" +#include "qe/lite/qe_lite.h" + +void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dependent_expr_state& st) { + + smt_params smtp(p); + s.add_simplifier(alloc(rewriter_simplifier, m, p, st)); + if (smtp.m_propagate_values) s.add_simplifier(alloc(propagate_values, m, p, st)); + if (smtp.m_solve_eqs) s.add_simplifier(alloc(euf::solve_eqs, m, st)); + if (smtp.m_elim_unconstrained) s.add_simplifier(alloc(elim_unconstrained, m, st)); + if (smtp.m_nnf_cnf) s.add_simplifier(alloc(cnf_nnf_simplifier, m, p, st)); + if (smtp.m_macro_finder || smtp.m_quasi_macros) s.add_simplifier(alloc(eliminate_predicates, m, st)); + if (smtp.m_qe_lite) s.add_simplifier(mk_qe_lite_simplifer(m, p, st)); + if (smtp.m_pull_nested_quantifiers) s.add_simplifier(alloc(pull_nested_quantifiers_simplifier, m, p, st)); + if (smtp.m_max_bv_sharing) s.add_simplifier(mk_max_bv_sharing(m, p, st)); + if (smtp.m_refine_inj_axiom) s.add_simplifier(alloc(refine_inj_axiom_simplifier, m, p, st)); + if (smtp.m_bv_size_reduce) s.add_simplifier(alloc(bv::slice, m, st)); + if (smtp.m_distribute_forall) s.add_simplifier(alloc(distribute_forall_simplifier, m, p, st)); + if (smtp.m_eliminate_bounds) s.add_simplifier(alloc(elim_bounds_simplifier, m, p, st)); + if (smtp.m_simplify_bit2int) s.add_simplifier(alloc(bit2int_simplifier, m, p, st)); + if (smtp.m_bb_quantifiers) s.add_simplifier(alloc(bv::elim_simplifier, m, p, st)); + if (smtp.m_eliminate_term_ite && smtp.m_lift_ite != lift_ite_kind::LI_FULL) s.add_simplifier(alloc(elim_term_ite_simplifier, m, p, st)); + if (smtp.m_lift_ite != lift_ite_kind::LI_NONE) s.add_simplifier(alloc(push_ite_simplifier, m, p, st, smtp.m_lift_ite == lift_ite_kind::LI_CONSERVATIVE)); + if (smtp.m_ng_lift_ite != lift_ite_kind::LI_NONE) s.add_simplifier(alloc(ng_push_ite_simplifier, m, p, st, smtp.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE)); + s.add_simplifier(alloc(flatten_clauses, m, p, st)); + + // + // add: + // euf_completion? + // + // add: make it externally programmable + // + +} + diff --git a/src/sat/sat_solver/sat_smt_preprocess.h b/src/solver/solver_preprocess.h similarity index 94% rename from src/sat/sat_solver/sat_smt_preprocess.h rename to src/solver/solver_preprocess.h index e7b40a8a3..c0dfc42f3 100644 --- a/src/sat/sat_solver/sat_smt_preprocess.h +++ b/src/solver/solver_preprocess.h @@ -3,7 +3,7 @@ Copyright (c) 2022 Microsoft Corporation Module Name: - sat_smt_preprocess.h + solver_preprocess.h Abstract: