From decaee83f39eb9eab57e4fc134cdead20c565e3d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Jan 2025 10:58:51 -0800 Subject: [PATCH] move from justified_expr to dependent_expr by aligning datatypes --- scripts/mk_project.py | 2 +- src/ast/justified_expr.h | 12 +++--- src/ast/macros/macro_manager.cpp | 2 +- src/ast/macros/quasi_macros.cpp | 14 +++---- src/ast/sls/sls_smt_plugin.h | 6 +-- src/ast/sls/sls_smt_solver.cpp | 4 +- src/solver/assertions/CMakeLists.txt | 1 + src/solver/assertions/asserted_formulas.cpp | 46 ++++++++++----------- src/solver/assertions/asserted_formulas.h | 16 +++---- 9 files changed, 52 insertions(+), 51 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 6399552e8..5d9a5ae69 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -53,7 +53,7 @@ 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('solver_assertions', ['pattern','smt_params','cmd_context','qe_lite'], 'solver/assertions') + add_lib('solver_assertions', ['pattern','smt_params','cmd_context','qe_lite', 'simplifiers', 'solver'], 'solver/assertions') add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic') add_lib('proto_model', ['model', 'rewriter', 'smt_params'], 'smt/proto_model') diff --git a/src/ast/justified_expr.h b/src/ast/justified_expr.h index a599ff5a1..2d2adf1b9 100644 --- a/src/ast/justified_expr.h +++ b/src/ast/justified_expr.h @@ -20,12 +20,12 @@ public: justified_expr& operator=(justified_expr const& other) { SASSERT(&m == &other.m); if (this != &other) { - m.inc_ref(other.get_fml()); - m.inc_ref(other.get_proof()); + m.inc_ref(other.fml()); + m.inc_ref(other.pr()); m.dec_ref(m_fml); m.dec_ref(m_proof); - m_fml = other.get_fml(); - m_proof = other.get_proof(); + m_fml = other.fml(); + m_proof = other.pr(); } return *this; } @@ -53,7 +53,7 @@ public: m_proof = nullptr; } - expr* get_fml() const { return m_fml; } + expr* fml() const { return m_fml; } - proof* get_proof() const { return m_proof; } + proof* pr() const { return m_proof; } }; diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp index 824573d46..d47072ebb 100644 --- a/src/ast/macros/macro_manager.cpp +++ b/src/ast/macros/macro_manager.cpp @@ -177,7 +177,7 @@ void macro_manager::mark_forbidden(unsigned n, justified_expr const * exprs) { expr_mark visited; macro_manager_ns::proc p(m_forbidden_set, m_forbidden); for (unsigned i = 0; i < n; i++) - for_each_expr(p, visited, exprs[i].get_fml()); + for_each_expr(p, visited, exprs[i].fml()); } diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp index b65daf063..254baa8b8 100644 --- a/src/ast/macros/quasi_macros.cpp +++ b/src/ast/macros/quasi_macros.cpp @@ -313,14 +313,14 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) { bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) { TRACE("quasi_macros", tout << "Finding quasi-macros in: " << std::endl; for (unsigned i = 0; i < n; i++) - tout << i << ": " << mk_pp(exprs[i].get_fml(), m) << std::endl; ); + tout << i << ": " << mk_pp(exprs[i].fml(), m) << std::endl; ); bool res = false; m_occurrences.reset(); // Find out how many non-ground appearances for each uninterpreted function there are for (unsigned i = 0 ; i < n ; i++) - find_occurrences(exprs[i].get_fml()); + find_occurrences(exprs[i].fml()); TRACE("quasi_macros", tout << "Occurrences: " << std::endl; for (auto kv : m_occurrences) @@ -331,9 +331,9 @@ bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) { app_ref a(m); expr_ref t(m); quantifier_ref macro(m); - if (is_quasi_macro(exprs[i].get_fml(), a, t) && - quasi_macro_to_macro(to_quantifier(exprs[i].get_fml()), a, t, macro)) { - TRACE("quasi_macros", tout << "Found quasi macro: " << mk_pp(exprs[i].get_fml(), m) << std::endl; + if (is_quasi_macro(exprs[i].fml(), a, t) && + quasi_macro_to_macro(to_quantifier(exprs[i].fml()), a, t, macro)) { + TRACE("quasi_macros", tout << "Found quasi macro: " << mk_pp(exprs[i].fml(), m) << std::endl; tout << "Macro: " << mk_pp(macro, m) << std::endl; ); proof * pr = nullptr; if (m.proofs_enabled()) @@ -377,9 +377,9 @@ void quasi_macros::apply_macros(unsigned n, justified_expr const* fmls, vectorbool_flip(); + sat::bool_var external_flip() override { + return m_ddfw->external_flip(); } bool is_external(sat::bool_var v) override { @@ -158,7 +158,7 @@ namespace sls { sat::clause_info const& get_clause(unsigned idx) const override { return m_ddfw->get_clause_info(idx); } ptr_iterator get_use_list(sat::literal lit) override { return m_ddfw->use_list(lit); } void flip(sat::bool_var v) override { - m_ddfw->flip(v); + m_ddfw->external_flip(v); } bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) override { return m_ddfw->try_rotate(v, rotated, budget); diff --git a/src/ast/sls/sls_smt_solver.cpp b/src/ast/sls/sls_smt_solver.cpp index 5a11e4dbb..cb2c895c4 100644 --- a/src/ast/sls/sls_smt_solver.cpp +++ b/src/ast/sls/sls_smt_solver.cpp @@ -88,8 +88,8 @@ namespace sls { vector const& clauses() const override { return m_ddfw.clauses(); } sat::clause_info const& get_clause(unsigned idx) const override { return m_ddfw.get_clause_info(idx); } ptr_iterator get_use_list(sat::literal lit) override { return m_ddfw.use_list(lit); } - void flip(sat::bool_var v) override { if (m_dirty) m_ddfw.reinit(), m_dirty = false; m_ddfw.flip(v); } - sat::bool_var bool_flip() override { if (m_dirty) m_ddfw.reinit(), m_dirty = false; return m_ddfw.bool_flip(); } + void flip(sat::bool_var v) override { if (m_dirty) m_ddfw.reinit(), m_dirty = false; m_ddfw.external_flip(v); } + sat::bool_var external_flip() override { if (m_dirty) m_ddfw.reinit(), m_dirty = false; return m_ddfw.external_flip(); } bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) override { if (m_dirty) m_ddfw.reinit(), m_dirty = false; return m_ddfw.try_rotate(v, rotated, budget); } double reward(sat::bool_var v) override { return m_ddfw.reward(v); } double get_weigth(unsigned clause_idx) override { return m_ddfw.get_clause_info(clause_idx).m_weight; } diff --git a/src/solver/assertions/CMakeLists.txt b/src/solver/assertions/CMakeLists.txt index 6deffd3a5..a1348fca2 100644 --- a/src/solver/assertions/CMakeLists.txt +++ b/src/solver/assertions/CMakeLists.txt @@ -5,4 +5,5 @@ z3_add_component(solver_assertions smt2parser smt_params qe_lite + solver ) diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp index 422adbf82..62f4c1970 100644 --- a/src/solver/assertions/asserted_formulas.cpp +++ b/src/solver/assertions/asserted_formulas.cpp @@ -184,7 +184,7 @@ void asserted_formulas::assert_expr(expr * e) { } void asserted_formulas::get_assertions(ptr_vector & result) const { - for (justified_expr const& je : m_formulas) result.push_back(je.get_fml()); + for (justified_expr const& je : m_formulas) result.push_back(je.fml()); } void asserted_formulas::push_scope() { @@ -258,7 +258,7 @@ void asserted_formulas::finalize() { bool asserted_formulas::check_well_sorted() const { for (justified_expr const& je : m_formulas) { - if (!is_well_sorted(m, je.get_fml())) return false; + if (!is_well_sorted(m, je.fml())) return false; } return true; } @@ -348,7 +348,7 @@ void asserted_formulas::display(std::ostream & out) const { for (unsigned i = 0; i < m_formulas.size(); i++) { if (i == m_qhead) out << "[HEAD] ==>\n"; - out << mk_pp(m_formulas[i].get_fml(), m) << "\n"; + out << mk_pp(m_formulas[i].fml(), m) << "\n"; } out << "inconsistent: " << inconsistent() << "\n"; } @@ -356,10 +356,10 @@ void asserted_formulas::display(std::ostream & out) const { void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) const { if (!m_formulas.empty()) { for (justified_expr const& f : m_formulas) - ast_def_ll_pp(out, m, f.get_fml(), pp_visited, true, false); + ast_def_ll_pp(out, m, f.fml(), pp_visited, true, false); out << "asserted formulas:\n"; for (justified_expr const& f : m_formulas) - out << "#" << f.get_fml()->get_id() << " "; + out << "#" << f.fml()->get_id() << " "; out << "\n"; } } @@ -400,7 +400,7 @@ void asserted_formulas::flatten_clauses() { unsigned sz = m_formulas.size(); for (unsigned i = m_qhead; i < sz; ++i) { auto const& j = m_formulas.get(i); - expr* f = j.get_fml(); + expr* f = j.fml(); bool decomposed = false; if (m.is_or(f, a, b) && m.is_not(b, b) && m.is_or(b) && (b->get_ref_count() == 1 || is_literal(a))) { decomposed = true; @@ -454,9 +454,9 @@ void asserted_formulas::nnf_cnf() { unsigned sz = m_formulas.size(); TRACE("nnf_bug", tout << "i: " << i << " sz: " << sz << "\n";); for (; i < sz; i++) { - expr * n = m_formulas[i].get_fml(); + expr * n = m_formulas[i].fml(); TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m) << "\n";); - proof_ref pr(m_formulas[i].get_proof(), m); + proof_ref pr(m_formulas[i].pr(), m); expr_ref r1(m); proof_ref pr1(m); push_todo.reset(); @@ -497,10 +497,10 @@ void asserted_formulas::simplify_fmls::operator()() { proof_ref result_pr(m); simplify(j, result, result_pr); if (m.proofs_enabled()) { - if (!result_pr) result_pr = m.mk_rewrite(j.get_fml(), result); - result_pr = m.mk_modus_ponens(j.get_proof(), result_pr); + if (!result_pr) result_pr = m.mk_rewrite(j.fml(), result); + result_pr = m.mk_modus_ponens(j.pr(), result_pr); } - if (j.get_fml() == result) { + if (j.fml() == result) { new_fmls.push_back(j); } else { @@ -530,7 +530,7 @@ void asserted_formulas::commit(unsigned new_qhead) { m_macro_manager.mark_forbidden(new_qhead - m_qhead, m_formulas.data() + m_qhead); for (unsigned i = m_qhead; i < new_qhead; ++i) { justified_expr const& j = m_formulas[i]; - update_substitution(j.get_fml(), j.get_proof()); + update_substitution(j.fml(), j.pr()); } m_qhead = new_qhead; } @@ -575,17 +575,17 @@ void asserted_formulas::propagate_values() { } unsigned asserted_formulas::propagate_values(unsigned i) { - expr_ref n(m_formulas[i].get_fml(), m); + expr_ref n(m_formulas[i].fml(), m); expr_ref new_n(m); proof_ref new_pr(m); m_rewriter(n, new_n, new_pr); if (m.proofs_enabled()) { - proof * pr = m_formulas[i].get_proof(); + proof * pr = m_formulas[i].pr(); new_pr = m.mk_modus_ponens(pr, new_pr); } justified_expr j(m, new_n, new_pr); m_formulas[i] = j; - if (m.is_false(j.get_fml())) { + if (m.is_false(j.fml())) { m_inconsistent = true; } update_substitution(new_n, new_pr); @@ -670,26 +670,26 @@ proof * asserted_formulas::get_inconsistency_proof() const { if (!m.inc()) return nullptr; for (justified_expr const& j : m_formulas) { - if (m.is_false(j.get_fml())) - return j.get_proof(); + if (m.is_false(j.fml())) + return j.pr(); } return nullptr; } void asserted_formulas::refine_inj_axiom_fn::simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { - expr* f = j.get_fml(); + expr* f = j.fml(); if (is_quantifier(f) && simplify_inj_axiom(m, to_quantifier(f), n)) { TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(f, m) << "\n" << n << "\n";); } else { - n = j.get_fml(); + n = j.fml(); } } void asserted_formulas::bv_size_reduce_fn::simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { bv_util bv(m); - expr* f = j.get_fml(); + expr* f = j.fml(); expr* a, *b, *x; unsigned lo, hi; rational r; @@ -699,7 +699,7 @@ void asserted_formulas::bv_size_reduce_fn::simplify(justified_expr const& j, exp // insert x -> x[0,lo-1] ++ n into sub new_term = bv.mk_concat(b, bv.mk_extract(lo - 1, 0, x)); m_sub.insert(x, new_term); - n = j.get_fml(); + n = j.fml(); return true; } return false; @@ -708,7 +708,7 @@ void asserted_formulas::bv_size_reduce_fn::simplify(justified_expr const& j, exp // done } else { - n = j.get_fml(); + n = j.fml(); m_sub(n); } } @@ -725,7 +725,7 @@ unsigned asserted_formulas::get_total_size() const { expr_mark visited; unsigned r = 0; for (justified_expr const& j : m_formulas) - r += get_num_exprs(j.get_fml(), visited); + r += get_num_exprs(j.fml(), visited); return r; } diff --git a/src/solver/assertions/asserted_formulas.h b/src/solver/assertions/asserted_formulas.h index 7af53e580..d0a748975 100644 --- a/src/solver/assertions/asserted_formulas.h +++ b/src/solver/assertions/asserted_formulas.h @@ -83,7 +83,7 @@ class asserted_formulas { class reduce_asserted_formulas_fn : public simplify_fmls { public: reduce_asserted_formulas_fn(asserted_formulas& af): simplify_fmls(af, "reduce-asserted") {} - void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { af.m_rewriter(j.get_fml(), n, p); } + void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { af.m_rewriter(j.fml(), n, p); } }; class find_macros_fn : public simplify_fmls { @@ -122,7 +122,7 @@ class asserted_formulas { distribute_forall m_functor; public: distribute_forall_fn(asserted_formulas& af): simplify_fmls(af, "distribute-forall"), m_functor(af.m) {} - void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_functor(j.get_fml(), n); } + void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_functor(j.fml(), n); } bool should_apply() const override { return af.m_smt_params.m_distribute_forall && af.has_quantifiers(); } void post_op() override { af.reduce_and_solve(); TRACE("asserted_formulas", af.display(tout);); } }; @@ -131,7 +131,7 @@ class asserted_formulas { pattern_inference_rw m_infer; public: pattern_inference_fn(asserted_formulas& af): simplify_fmls(af, "pattern-inference"), m_infer(af.m, af.m_smt_params) {} - void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_infer(j.get_fml(), n, p); } + void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_infer(j.fml(), n, p); } bool should_apply() const override { return af.m_smt_params.m_ematching && af.has_quantifiers(); } }; @@ -145,7 +145,7 @@ class asserted_formulas { class max_bv_sharing_fn : public simplify_fmls { public: max_bv_sharing_fn(asserted_formulas& af): simplify_fmls(af, "maximizing-bv-sharing") {} - void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { af.m_bv_sharing(j.get_fml(), n, p); } + void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { af.m_bv_sharing(j.fml(), n, p); } bool should_apply() const override { return af.m_smt_params.m_max_bv_sharing; } void post_op() override { af.m_reduce_asserted_formulas(); } }; @@ -164,7 +164,7 @@ class asserted_formulas { elim_term_ite_rw m_elim; public: elim_term_ite_fn(asserted_formulas& af): simplify_fmls(af, "elim-term-ite"), m_elim(af.m, af.m_defined_names) {} - void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_elim(j.get_fml(), n, p); } + void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_elim(j.fml(), n, p); } bool should_apply() const override { return af.m_smt_params.m_eliminate_term_ite && af.m_smt_params.m_lift_ite != lift_ite_kind::LI_FULL; } void post_op() override { af.m_formulas.append(m_elim.new_defs()); af.reduce_and_solve(); m_elim.reset(); } void push() { m_elim.push(); } @@ -186,7 +186,7 @@ class asserted_formulas { FUNCTOR m_functor; \ NAME(asserted_formulas& af):simplify_fmls(af, MSG), m_functor ARG {} \ virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { \ - m_functor(j.get_fml(), n, p); \ + m_functor(j.fml(), n, p); \ } \ virtual void post_op() { if (REDUCE) af.reduce_and_solve(); } \ virtual bool should_apply() const { return APP; } \ @@ -270,8 +270,8 @@ public: unsigned get_qhead() const { return m_qhead; } void commit(); void commit(unsigned new_qhead); - expr * get_formula(unsigned idx) const { return m_formulas[idx].get_fml(); } - proof * get_formula_proof(unsigned idx) const { return m_formulas[idx].get_proof(); } + expr * get_formula(unsigned idx) const { return m_formulas[idx].fml(); } + proof * get_formula_proof(unsigned idx) const { return m_formulas[idx].pr(); } params_ref const& get_params() const { return m_params; } void get_assertions(ptr_vector & result) const;