From fa58a36b9f5cb13b27e9c48f03647b97e8cf8f2e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 5 Oct 2020 14:13:05 -0700 Subject: [PATCH] model refactor (#4723) * refactor model fixing Signed-off-by: Nikolaj Bjorner * missing cond macro Signed-off-by: Nikolaj Bjorner * file Signed-off-by: Nikolaj Bjorner * file Signed-off-by: Nikolaj Bjorner * add macros dependency Signed-off-by: Nikolaj Bjorner * deps and debug Signed-off-by: Nikolaj Bjorner * add dependency to normal forms Signed-off-by: Nikolaj Bjorner * na Signed-off-by: Nikolaj Bjorner * build issues Signed-off-by: Nikolaj Bjorner * compile Signed-off-by: Nikolaj Bjorner * fix leal regression * complete model fixer Signed-off-by: Nikolaj Bjorner * fold back private functionality to model_finder Signed-off-by: Nikolaj Bjorner * avoid duplicate fixed callbacks Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 4 +- src/CMakeLists.txt | 2 +- src/ast/euf/euf_egraph.cpp | 15 +- src/ast/euf/euf_egraph.h | 5 +- src/ast/euf/euf_etable.cpp | 6 +- src/ast/euf/euf_etable.h | 8 +- src/ast/fpa/bv2fpa_converter.h | 17 - src/ast/fpa/fpa2bv_converter.cpp | 2 +- src/ast/macros/CMakeLists.txt | 1 + src/ast/macros/cond_macro.h | 72 + src/ast/macros/quantifier_macro_info.cpp | 66 + src/ast/macros/quantifier_macro_info.h | 55 + src/model/CMakeLists.txt | 2 + src/model/model_core.cpp | 10 +- src/model/model_core.h | 1 + src/model/model_macro_solver.cpp | 593 +++++++ src/model/model_macro_solver.h | 308 ++++ src/sat/sat_extension.h | 4 +- src/sat/smt/CMakeLists.txt | 1 + src/sat/smt/array_solver.cpp | 2 +- src/sat/smt/ba_solver.cpp | 2 +- src/sat/smt/bv_solver.cpp | 2 +- src/sat/smt/euf_solver.cpp | 27 +- src/sat/smt/fpa_solver.cpp | 4 +- src/sat/smt/q_mbi.cpp | 15 +- src/sat/smt/q_mbi.h | 7 +- src/sat/smt/q_model_finder.cpp | 4 + src/sat/smt/q_model_finder.h | 14 + src/sat/smt/q_model_fixer.cpp | 198 +++ src/sat/smt/q_model_fixer.h | 78 + src/sat/smt/q_solver.cpp | 40 +- src/sat/smt/q_solver.h | 6 +- src/sat/smt/sat_th.cpp | 4 +- src/sat/smt/sat_th.h | 4 +- src/sat/smt/user_solver.cpp | 2 +- src/smt/smt_model_checker.h | 2 +- src/smt/smt_model_finder.cpp | 1933 ++++++---------------- src/smt/smt_model_finder.h | 18 +- src/smt/theory_fpa.cpp | 2 +- src/smt/user_propagator.cpp | 4 + src/smt/user_propagator.h | 2 + src/util/trail.h | 12 + 42 files changed, 2060 insertions(+), 1494 deletions(-) create mode 100644 src/ast/macros/cond_macro.h create mode 100644 src/ast/macros/quantifier_macro_info.cpp create mode 100644 src/ast/macros/quantifier_macro_info.h create mode 100644 src/model/model_macro_solver.cpp create mode 100644 src/model/model_macro_solver.h create mode 100644 src/sat/smt/q_model_fixer.cpp create mode 100644 src/sat/smt/q_model_fixer.h diff --git a/scripts/mk_project.py b/scripts/mk_project.py index d37574836..c1655d027 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -32,7 +32,7 @@ def init_project_def(): add_lib('rewriter', ['ast', 'polynomial', 'automata', 'params'], 'ast/rewriter') add_lib('macros', ['rewriter'], 'ast/macros') add_lib('normal_forms', ['rewriter'], 'ast/normal_forms') - add_lib('model', ['rewriter']) + add_lib('model', ['rewriter', 'macros']) add_lib('tactic', ['ast', 'model']) add_lib('substitution', ['ast', 'rewriter'], 'ast/substitution') add_lib('parser_util', ['ast'], 'parsers/util') @@ -49,7 +49,7 @@ def init_project_def(): add_lib('core_tactics', ['tactic', 'macros', 'normal_forms', 'rewriter', 'pattern'], 'tactic/core') add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith') - add_lib('sat_smt', ['sat', 'euf', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa'], 'sat/smt') + add_lib('sat_smt', ['sat', 'euf', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'normal_forms'], 'sat/smt') add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_smt'], 'sat/tactic') add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic') add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic') diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index b207a8bfc..736bfbdad 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -47,6 +47,7 @@ add_subdirectory(ast) add_subdirectory(params) add_subdirectory(ast/rewriter) add_subdirectory(ast/normal_forms) +add_subdirectory(ast/macros) add_subdirectory(model) add_subdirectory(tactic) add_subdirectory(ast/substitution) @@ -64,7 +65,6 @@ add_subdirectory(solver) add_subdirectory(cmd_context) add_subdirectory(cmd_context/extra_cmds) add_subdirectory(parsers/smt2) -add_subdirectory(ast/macros) add_subdirectory(ast/pattern) add_subdirectory(ast/rewriter/bit_blaster) add_subdirectory(smt/params) diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index a00795cb4..6c3cd58c1 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -107,6 +107,11 @@ namespace euf { enode* n = enode::mk(m_region, f, num_args, args); m_nodes.push_back(n); m_exprs.push_back(f); + if (is_app(f) && num_args > 0) { + unsigned id = to_app(f)->get_decl()->get_decl_id(); + m_decl2enodes.reserve(id+1); + m_decl2enodes[id].push_back(n); + } m_expr2enode.setx(f->get_id(), n, nullptr); push_node(n); for (unsigned i = 0; i < num_args; ++i) @@ -114,9 +119,15 @@ namespace euf { return n; } + enode_vector const& egraph::enodes_of(func_decl* f) { + unsigned id = f->get_decl_id(); + if (id < m_decl2enodes.size()) + return m_decl2enodes[id]; + return m_empty_enodes; + } + enode_bool_pair egraph::insert_table(enode* p) { auto rc = m_table.insert(p); - enode* p_other = rc.first; p->m_cg = rc.first; return rc; } @@ -338,6 +349,8 @@ namespace euf { m_expr2enode[e->get_id()] = nullptr; n->~enode(); + if (is_app(e) && n->num_args() > 0) + m_decl2enodes[to_app(e)->get_decl()->get_decl_id()].pop_back(); m_nodes.pop_back(); m_exprs.pop_back(); }; diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index 8e1f79864..d6cd8e430 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -141,7 +141,7 @@ namespace euf { tag(tag_t::is_value_assignment), r1(n), n1(nullptr), qhead(0) {} }; ast_manager& m; - svector m_to_merge; + svector m_to_merge; etable m_table; region m_region; svector m_updates; @@ -150,6 +150,8 @@ namespace euf { enode* m_tmp_eq { nullptr }; enode_vector m_nodes; expr_ref_vector m_exprs; + vector m_decl2enodes; + enode_vector m_empty_enodes; unsigned m_num_scopes { 0 }; bool m_inconsistent { false }; enode *m_n1 { nullptr }; @@ -214,6 +216,7 @@ namespace euf { ~egraph(); enode* find(expr* f) { return m_expr2enode.get(f->get_id(), nullptr); } enode* mk(expr* f, unsigned n, enode *const* args); + enode_vector const& enodes_of(func_decl* f); void push() { ++m_num_scopes; } void pop(unsigned num_scopes); diff --git a/src/ast/euf/euf_etable.cpp b/src/ast/euf/euf_etable.cpp index 3aaf6b75b..62dafdd68 100644 --- a/src/ast/euf/euf_etable.cpp +++ b/src/ast/euf/euf_etable.cpp @@ -22,7 +22,7 @@ namespace euf { // one table per func_decl implementation unsigned etable::cg_hash::operator()(enode * n) const { - SASSERT(decl(n)->is_flat_associative() || n->num_args() >= 3); + SASSERT(n->get_decl()->is_flat_associative() || n->num_args() >= 3); unsigned a, b, c; a = b = 0x9e3779b9; c = 11; @@ -50,7 +50,7 @@ namespace euf { } bool etable::cg_eq::operator()(enode * n1, enode * n2) const { - SASSERT(decl(n1) == decl(n2)); + SASSERT(n1->get_decl() == n2->get_decl()); unsigned num = n1->num_args(); if (num != n2->num_args()) { return false; @@ -96,7 +96,7 @@ namespace euf { } unsigned etable::set_table_id(enode * n) { - func_decl * f = decl(n); + func_decl * f = n->get_decl(); unsigned tid; decl_info d(f, n->num_args()); if (!m_func_decl2id.find(d, tid)) { diff --git a/src/ast/euf/euf_etable.h b/src/ast/euf/euf_etable.h index eef24184a..6e88cf9b9 100644 --- a/src/ast/euf/euf_etable.h +++ b/src/ast/euf/euf_etable.h @@ -24,8 +24,6 @@ namespace euf { // one table per function symbol - static func_decl* decl(enode* n) { return n->get_decl(); } - /** \brief Congruence table. @@ -45,7 +43,7 @@ namespace euf { bool operator()(enode * n1, enode * n2) const { SASSERT(n1->num_args() == 1); SASSERT(n2->num_args() == 1); - SASSERT(decl(n1) == decl(n2)); + SASSERT(n1->get_decl() == n2->get_decl()); return get_root(n1, 0) == get_root(n2, 0); } }; @@ -63,7 +61,7 @@ namespace euf { bool operator()(enode * n1, enode * n2) const { SASSERT(n1->num_args() == 2); SASSERT(n2->num_args() == 2); - SASSERT(decl(n1) == decl(n2)); + SASSERT(n1->get_decl() == n2->get_decl()); return get_root(n1, 0) == get_root(n2, 0) && get_root(n1, 1) == get_root(n2, 1); @@ -90,7 +88,7 @@ namespace euf { SASSERT(n1->num_args() == 2); SASSERT(n2->num_args() == 2); - SASSERT(decl(n1) == decl(n2)); + SASSERT(n1->get_decl() == n2->get_decl()); enode* c1_1 = get_root(n1, 0); enode* c1_2 = get_root(n1, 1); enode* c2_1 = get_root(n2, 0); diff --git a/src/ast/fpa/bv2fpa_converter.h b/src/ast/fpa/bv2fpa_converter.h index f533bcffc..87b98af59 100644 --- a/src/ast/fpa/bv2fpa_converter.h +++ b/src/ast/fpa/bv2fpa_converter.h @@ -70,21 +70,4 @@ public: array_model convert_array_func_interp(model_core * mc, func_decl * f, func_decl * bv_f); }; -template -class fpa2bv_conversion_trail_elem : public trail { - ast_manager& m; - obj_map& m_map; - expr_ref key; -public: - fpa2bv_conversion_trail_elem(ast_manager& m, obj_map& map, expr* e) : - m(m), m_map(map), key(e, m) { } - ~fpa2bv_conversion_trail_elem() override { } - void undo(T& s) override { - expr* val = m_map.find(key); - m_map.remove(key); - m.dec_ref(key); - m.dec_ref(val); - key = nullptr; - } -}; diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 6749773c3..4efaf3b00 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -32,11 +32,11 @@ Notes: fpa2bv_converter::fpa2bv_converter(ast_manager & m) : m(m), m_simp(m), - m_util(m), m_bv_util(m), m_arith_util(m), m_dt_util(m), m_seq_util(m), + m_util(m), m_mpf_manager(m_util.fm()), m_mpz_manager(m_mpf_manager.mpz_manager()), m_hi_fp_unspecified(true), diff --git a/src/ast/macros/CMakeLists.txt b/src/ast/macros/CMakeLists.txt index ec6d7e26c..12d4965a6 100644 --- a/src/ast/macros/CMakeLists.txt +++ b/src/ast/macros/CMakeLists.txt @@ -2,6 +2,7 @@ z3_add_component(macros SOURCES macro_finder.cpp macro_manager.cpp + quantifier_macro_info.cpp macro_util.cpp quasi_macros.cpp COMPONENT_DEPENDENCIES diff --git a/src/ast/macros/cond_macro.h b/src/ast/macros/cond_macro.h new file mode 100644 index 000000000..7e8064ac6 --- /dev/null +++ b/src/ast/macros/cond_macro.h @@ -0,0 +1,72 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + cond_macro.h + +Abstract: + + Class for maintaining conditional macros + +Author: + + Leonardo de Moura (leonardo) 2010-12-17. + +Revision History: + +--*/ +#pragma once +#include "ast/ast_ll_pp.h" + +class cond_macro { +protected: + func_decl * m_f; + expr_ref m_def; + expr_ref m_cond; + bool m_ineq; + bool m_satisfy_atom; + bool m_hint; + unsigned m_weight; +public: + cond_macro(ast_manager & m, func_decl * f, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, unsigned weight): + m_f(f), + m_def(def,m), + m_cond(cond, m), + m_ineq(ineq), + m_satisfy_atom(satisfy_atom), + m_hint(hint), + m_weight(weight) { + SASSERT(!m_hint || !m_cond); + } + + ~cond_macro() { + } + + func_decl * get_f() const { return m_f; } + + expr * get_def() const { return m_def; } + + expr * get_cond() const { return m_cond; } + + bool is_unconditional() const { return !m_cond || m_cond.m().is_true(m_cond); } + + bool satisfy_atom() const { return m_satisfy_atom; } + + bool is_hint() const { return m_hint; } + + bool is_equal(cond_macro const * other) const { + return m_f == other->m_f && m_def == other->m_def && m_cond == other->m_cond; + } + + std::ostream& display(std::ostream & out) const { + out << "[" << m_f->get_name() << " -> " << mk_bounded_pp(m_def, m_def.m(), 6); + if (m_hint) + out << " *hint*"; + else + out << " when " << mk_bounded_pp(m_cond, m_cond.m(), 6); + return out << "] weight: " << m_weight; + } + + unsigned get_weight() const { return m_weight; } +}; diff --git a/src/ast/macros/quantifier_macro_info.cpp b/src/ast/macros/quantifier_macro_info.cpp new file mode 100644 index 000000000..24e5a32e4 --- /dev/null +++ b/src/ast/macros/quantifier_macro_info.cpp @@ -0,0 +1,66 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + quantifier_macro_info.cpp + +Abstract: + + Macro solving utilities + +Author: + + Leonardo de Moura (leonardo) 2010-12-17. + +Revision History: + +--*/ +#include "ast/ast_pp.h" +#include "ast/macros/quantifier_macro_info.h" + +quantifier_macro_info::quantifier_macro_info(ast_manager& m, quantifier* q) : + m(m), + m_flat_q(q, m), + m_is_auf(true), + m_has_x_eq_y(false), + m_the_one(m) { + SASSERT(is_forall(q)); + collect_macro_candidates(q); +} + +void quantifier_macro_info::collect_macro_candidates(quantifier* q) { + macro_util mutil(m); + macro_util::macro_candidates candidates(m); + mutil.collect_macro_candidates(q, candidates); + unsigned num_candidates = candidates.size(); + for (unsigned i = 0; i < num_candidates; i++) { + cond_macro* mc = alloc(cond_macro, m, candidates.get_f(i), candidates.get_def(i), candidates.get_cond(i), + candidates.ineq(i), candidates.satisfy_atom(i), candidates.hint(i), q->get_weight()); + insert_macro(mc); + } +} + + +bool quantifier_macro_info::unary_function_fragment() const { + unsigned sz = m_ng_decls.size(); + if (sz > 1) + return false; + if (sz == 0) + return true; + func_decl* f = *(m_ng_decls.begin()); + return f->get_arity() == 1; +} + +std::ostream& quantifier_macro_info::display(std::ostream& out) const { + out << "info for quantifier:\n" << mk_pp(m_flat_q, m) << "\n"; + out << "IS_AUF: " << m_is_auf << ", has x=y: " << m_has_x_eq_y << "\n"; + out << "unary function fragment: " << unary_function_fragment() << "\n"; + out << "ng decls: "; + for (func_decl* f : m_ng_decls) + out << f->get_name() << " "; + out << "\nmacros:\n"; + for (cond_macro* cm : m_cond_macros) + cm->display(out << " ") << "\n"; + return out; +} diff --git a/src/ast/macros/quantifier_macro_info.h b/src/ast/macros/quantifier_macro_info.h new file mode 100644 index 000000000..82790e937 --- /dev/null +++ b/src/ast/macros/quantifier_macro_info.h @@ -0,0 +1,55 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + quantifier_macro_info.h + +Abstract: + + Macro solving utilities + +Author: + + Leonardo de Moura (leonardo) 2010-12-17. + +Revision History: + +--*/ +#pragma once +#include "util/scoped_ptr_vector.h" +#include "ast/ast_ll_pp.h" +#include "ast/macros/cond_macro.h" +#include "ast/macros/macro_util.h" +#include "ast/func_decl_dependencies.h" + +/** + \brief Store relevant information regarding a particular universal quantifier. + The information is used to (try to) build a model that satisfy the universal quantifier. +*/ +class quantifier_macro_info { +protected: + ast_manager& m; + quantifier_ref m_flat_q; // (flattened) quantifier + bool m_is_auf; + bool m_has_x_eq_y; + func_decl_set m_ng_decls; // declarations used in non-ground applications (basic_family operators are ignored here). + scoped_ptr_vector m_cond_macros; + func_decl_ref m_the_one; // the macro head used to satisfy the quantifier. this is useful for model checking + void collect_macro_candidates(quantifier* q); +public: + quantifier_macro_info(ast_manager& m, quantifier* q); + virtual ~quantifier_macro_info() {} + bool is_auf() const { return m_is_auf; } + quantifier* get_flat_q() const { return m_flat_q; } + bool has_cond_macros() const { return !m_cond_macros.empty(); } + scoped_ptr_vector const& macros() const { return m_cond_macros; } + void set_the_one(func_decl* f) { m_the_one = f; } + func_decl* get_the_one() const { return m_the_one; } + bool contains_ng_decl(func_decl* f) const { return m_ng_decls.contains(f); } + func_decl_set const& get_ng_decls() const { return m_ng_decls; } + virtual void reset_the_one() { m_the_one = nullptr; } + void insert_macro(cond_macro* m) { m_cond_macros.push_back(m); } + bool unary_function_fragment() const; + virtual std::ostream& display(std::ostream& out) const; +}; diff --git a/src/model/CMakeLists.txt b/src/model/CMakeLists.txt index b46a22e4e..9ba93b8e1 100644 --- a/src/model/CMakeLists.txt +++ b/src/model/CMakeLists.txt @@ -8,6 +8,7 @@ z3_add_component(model model.cpp model_evaluator.cpp model_implicant.cpp + model_macro_solver.cpp model_pp.cpp model_smt2_pp.cpp model_v2_pp.cpp @@ -16,6 +17,7 @@ z3_add_component(model value_factory.cpp COMPONENT_DEPENDENCIES rewriter + macros PYG_FILES model_evaluator_params.pyg model_params.pyg diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 97e74f49b..bfcd43f9f 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -74,9 +74,15 @@ void model_core::register_decl(func_decl * d, expr * v) { } void model_core::register_decl(func_decl * d, func_interp * fi) { + func_interp* old_fi = update_func_interp(d, fi); + dealloc(old_fi); +} + +func_interp* model_core::update_func_interp(func_decl* d, func_interp* fi) { TRACE("model", tout << "register " << d->get_name() << "\n";); SASSERT(d->get_arity() > 0); SASSERT(&fi->m() == &m); + func_interp* old_fi = nullptr; auto& value = m_finterp.insert_if_not_there(d, nullptr); if (value == nullptr) { // new entry @@ -87,10 +93,10 @@ void model_core::register_decl(func_decl * d, func_interp * fi) { } else { // replacing entry - if (fi != value) - dealloc(value); + old_fi = value; value = fi; } + return old_fi; } void model_core::unregister_decl(func_decl * d) { diff --git a/src/model/model_core.h b/src/model/model_core.h index 5b451dbb8..70c5e34d6 100644 --- a/src/model/model_core.h +++ b/src/model/model_core.h @@ -68,6 +68,7 @@ public: void register_decl(func_decl * d, expr * v); void register_decl(func_decl * f, func_interp * fi); void unregister_decl(func_decl * d); + func_interp* update_func_interp(func_decl* f, func_interp* fi); virtual expr * get_some_value(sort * s) = 0; virtual expr * get_fresh_value(sort * s) = 0; diff --git a/src/model/model_macro_solver.cpp b/src/model/model_macro_solver.cpp new file mode 100644 index 000000000..1d95f12cd --- /dev/null +++ b/src/model/model_macro_solver.cpp @@ -0,0 +1,593 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Abstract: + + Macro solving utilities + +Author: + + Leonardo de Moura (leonardo) 2010-12-17. + +--*/ + +#include "ast/for_each_expr.h" +#include "ast/ast_pp.h" +#include "model/model_macro_solver.h" +#include "model/model_core.h" + +void base_macro_solver::set_else_interp(func_decl* f, expr* f_else) { + SASSERT(f_else != nullptr); + func_interp* fi = m_model->get_func_interp(f); + if (fi == nullptr) { + fi = alloc(func_interp, m, f->get_arity()); + m_model->register_decl(f, fi); + } + fi->set_else(f_else); + TRACE("model_finder", tout << f->get_name() << " " << mk_pp(f_else, m) << "\n";); +} + +void base_macro_solver::operator()(model_core& m, ptr_vector& qs, ptr_vector& residue) { + m_model = &m; + ptr_vector curr_qs(qs), new_qs; + while (process(curr_qs, new_qs, residue)) { + curr_qs.swap(new_qs); + new_qs.reset(); + } + std::swap(qs, new_qs); +} + +/** + \brief Return true if \c f is in (qs\{q}) +*/ +bool simple_macro_solver::contains(func_decl* f, ptr_vector const& qs, quantifier* q) { + for (quantifier* other : qs) { + if (q == other) + continue; + quantifier_macro_info* other_qi = get_qinfo(other); + if (other_qi->contains_ng_decl(f)) + return true; + } + return false; +} + +bool simple_macro_solver::process(quantifier* q, ptr_vector const& qs) { + quantifier_macro_info* qi = get_qinfo(q); + for (cond_macro* m : qi->macros()) { + if (!m->satisfy_atom()) + continue; + func_decl* f = m->get_f(); + if (!contains(f, qs, q)) { + qi->set_the_one(f); + expr* f_else = m->get_def(); + SASSERT(f_else != nullptr); + // Remark: I can ignore the conditions of m because + // I know the (partial) interpretation of f satisfied the ground part. + // MBQI will force extra instantiations if the (partial) interpretation of f + // does not satisfy the quantifier. + // In all other cases the "else" of f will satisfy the quantifier. + set_else_interp(f, f_else); + TRACE("model_finder", tout << "satisfying the quantifier using simple macro:\n"; + m->display(tout); tout << "\n";); + return true; // satisfied quantifier + } + } + return false; +} + +bool simple_macro_solver::process(ptr_vector const& qs, ptr_vector& new_qs, ptr_vector& residue) { + bool removed = false; + for (quantifier* q : qs) { + if (process(q, qs)) + removed = true; + else + new_qs.push_back(q); + } + return removed; +} + + + +void hint_macro_solver::insert_q_f(quantifier* q, func_decl* f) { + SASSERT(!m_forbidden.contains(f)); + quantifier_set* s = nullptr; + if (!m_q_f.find(f, s)) { + s = alloc(quantifier_set); + m_q_f.insert(f, s); + m_qsets.push_back(s); + } + SASSERT(s != nullptr); + s->insert(q); +} + +void hint_macro_solver::insert_f2def(func_decl* f, expr* def) { + expr_set* s = nullptr; + if (!m_f2defs.find(f, s)) { + s = alloc(expr_set); + m_f2defs.insert(f, s); + m_esets.push_back(s); + } + SASSERT(s != nullptr); + s->insert(def); +} + +void hint_macro_solver::insert_q_f_def(quantifier* q, func_decl* f, expr* def) { + SASSERT(!m_forbidden.contains(f)); + quantifier_set* s = nullptr; + if (!m_q_f_def.find(f, def, s)) { + s = alloc(quantifier_set); + m_q_f_def.insert(f, def, s); + insert_f2def(f, def); + m_qsets.push_back(s); + } + SASSERT(s != nullptr); + s->insert(q); +} + + +hint_macro_solver::quantifier_set* hint_macro_solver::get_q_f_def(func_decl* f, expr* def) { + quantifier_set* s = nullptr; + m_q_f_def.find(f, def, s); + SASSERT(s != nullptr); + return s; +} + + +void hint_macro_solver::reset_q_fs() { + std::for_each(m_qsets.begin(), m_qsets.end(), delete_proc()); + std::for_each(m_esets.begin(), m_esets.end(), delete_proc()); + m_q_f.reset(); + m_q_f_def.reset(); + m_qsets.reset(); + m_f2defs.reset(); + m_esets.reset(); +} + + +bool hint_macro_solver::is_candidate(quantifier* q) const { + quantifier_macro_info* qi = get_qinfo(q); + for (cond_macro* m : qi->macros()) { + if (m->satisfy_atom() && !m_forbidden.contains(m->get_f())) + return true; + } + return false; +} + +void hint_macro_solver::register_decls_as_forbidden(quantifier* q) { + quantifier_macro_info* qi = get_qinfo(q); + func_decl_set const& ng_decls = qi->get_ng_decls(); + for (func_decl* f : ng_decls) { + m_forbidden.insert(f); + } +} + +void hint_macro_solver::preprocess(ptr_vector const& qs, ptr_vector& qcandidates, ptr_vector& non_qcandidates) { + ptr_vector curr(qs); + while (true) { + for (quantifier* q : curr) { + if (is_candidate(q)) { + qcandidates.push_back(q); + } + else { + register_decls_as_forbidden(q); + non_qcandidates.push_back(q); + } + } + if (curr.size() == qcandidates.size()) + return; + SASSERT(qcandidates.size() < curr.size()); + curr.swap(qcandidates); + qcandidates.reset(); + } +} + +void hint_macro_solver::mk_q_f_defs(ptr_vector const& qs) { + for (quantifier* q : qs) { + quantifier_macro_info* qi = get_qinfo(q); + func_decl_set const& ng_decls = qi->get_ng_decls(); + for (func_decl* f : ng_decls) { + if (!m_forbidden.contains(f)) + insert_q_f(q, f); + } + for (cond_macro* m : qi->macros()) { + if (m->satisfy_atom() && !m_forbidden.contains(m->get_f())) { + insert_q_f_def(q, m->get_f(), m->get_def()); + m_candidates.insert(m->get_f()); + } + } + } +} + +void hint_macro_solver::display_quantifier_set(std::ostream& out, quantifier_set const* s) { + for (quantifier* q : *s) { + out << q->get_qid() << " "; + } + out << "\n"; +} + +void hint_macro_solver::display_qcandidates(std::ostream& out, ptr_vector const& qcandidates) const { + for (quantifier* q : qcandidates) { + out << q->get_qid() << " ->\n" << mk_pp(q, m) << "\n"; + quantifier_macro_info* qi = get_qinfo(q); + qi->display(out); + out << "------\n"; + } + out << "Sets Q_f\n"; + for (auto const& kv : m_q_f) { + func_decl* f = kv.m_key; + quantifier_set* s = kv.m_value; + out << f->get_name() << " -> "; display_quantifier_set(out, s); + } + out << "Sets Q_{f = def}\n"; + for (auto const& kv : m_q_f_def) { + func_decl* f = kv.get_key1(); + expr* def = kv.get_key2(); + quantifier_set* s = kv.get_value(); + out << f->get_name() << " " << mk_pp(def, m) << " ->\n"; display_quantifier_set(out, s); + } +} + + +void hint_macro_solver::display_search_state(std::ostream& out) const { + out << "fs:\n"; + for (auto const& kv : m_fs) { + out << kv.m_key->get_name() << " "; + } + out << "\nsatisfied:\n"; + for (auto q : m_satisfied) { + out << q->get_qid() << " "; + } + out << "\nresidue:\n"; + for (auto q : m_residue) { + out << q->get_qid() << " "; + } + out << "\n"; +} + +bool hint_macro_solver::check_satisfied_residue_invariant() { + DEBUG_CODE( + for (quantifier* q : m_satisfied) { + SASSERT(!m_residue.contains(q)); + auto* qi = get_qinfo(q); + SASSERT(qi != nullptr); + SASSERT(qi->get_the_one() != nullptr); + }); + return true; +} + + +bool hint_macro_solver::update_satisfied_residue(func_decl* f, expr* def) { + bool useful = false; + SASSERT(check_satisfied_residue_invariant()); + quantifier_set* q_f = get_q_f(f); + quantifier_set* q_f_def = get_q_f_def(f, def); + for (quantifier* q : *q_f_def) { + if (!m_satisfied.contains(q)) { + useful = true; + m_residue.erase(q); + m_satisfied.insert(q); + quantifier_macro_info* qi = get_qinfo(q); + SASSERT(qi->get_the_one() == 0); + qi->set_the_one(f); // remark... event handler will reset it during backtracking. + } + } + if (!useful) + return false; + for (quantifier* q : *q_f) { + if (!m_satisfied.contains(q)) { + m_residue.insert(q); + } + } + SASSERT(check_satisfied_residue_invariant()); + return true; +} + +/** + \brief Extract from m_residue, func_decls that can be used as macros to satisfy it. + The candidates must not be elements of m_fs. +*/ +void hint_macro_solver::get_candidates_from_residue(func_decl_set& candidates) { + for (quantifier* q : m_residue) { + quantifier_macro_info* qi = get_qinfo(q); + for (cond_macro* m : qi->macros()) { + func_decl* f = m->get_f(); + if (m->satisfy_atom() && !m_forbidden.contains(f) && !m_fs.contains(f)) { + candidates.insert(f); + } + } + } +} + +#define GREEDY_MAX_DEPTH 10 /* to avoid too expensive search spaces */ + +/** + \brief Try to reduce m_residue using the macros of f. +*/ +void hint_macro_solver::greedy(func_decl* f, unsigned depth) { + if (depth >= GREEDY_MAX_DEPTH) + return; // failed + + TRACE("model_finder_hint", + tout << "greedy depth: " << depth << ", f: " << f->get_name() << "\n"; + display_search_state(tout);); + + expr_set* s = get_f_defs(f); + for (expr* def : *s) { + + SASSERT(!m_fs.contains(f)); + + m_satisfied.push_scope(); + m_residue.push_scope(); + TRACE("model_finder", tout << f->get_name() << " " << mk_pp(def, m) << "\n";); + m_fs.insert(f, def); + + if (update_satisfied_residue(f, def)) { + // update was useful + greedy(depth + 1); // greedy throws exception in case of success + // reachable iff greedy failed. + } + + m_satisfied.pop_scope(); + m_residue.pop_scope(); + m_fs.erase(f); + } +} + +/** + \brief check if satisfied subset introduces a cyclic dependency. + + f_1 = def_1(f_2), ..., f_n = def_n(f_1) + */ + +bool hint_macro_solver::is_cyclic() { + m_acyclic.reset(); + while (true) { + unsigned sz = m_acyclic.size(); + if (sz == m_fs.size()) return false; // there are no cyclic dependencies + for (auto const& kv : m_fs) { + func_decl* f = kv.m_key; + if (m_acyclic.contains(f)) continue; + if (is_acyclic(kv.m_value)) + m_acyclic.insert(f); + } + if (sz == m_acyclic.size()) return true; // no progress, so dependency cycle found. + } +} + +bool hint_macro_solver::is_acyclic(expr* def) { + m_visited.reset(); + occurs_check oc(*this); + try { + for_each_expr(oc, m_visited, def); + } + catch (const occurs&) { + return false; + } + return true; +} + +/** + \brief Try to reduce m_residue (if not empty) by selecting a function f + that is a macro in the residue. +*/ +void hint_macro_solver::greedy(unsigned depth) { + if (m_residue.empty()) { + if (is_cyclic()) return; + TRACE("model_finder_hint", + tout << "found subset that is satisfied by macros\n"; + display_search_state(tout);); + throw found_satisfied_subset(); + } + func_decl_set candidates; + get_candidates_from_residue(candidates); + + TRACE("model_finder_hint", tout << "candidates from residue:\n"; + for (func_decl* f : candidates) { + tout << f->get_name() << " "; + } + tout << "\n";); + + for (func_decl* f : candidates) { + greedy(f, depth); + } +} + +/** + \brief Try to find a set of quantifiers by starting to use the macros of f. + This is the "find" procedure in the comments above. + The set of satisfied quantifiers is in m_satisfied, and the remaining to be + satisfied in m_residue. When the residue becomes empty we throw the exception found_satisfied_subset. +*/ +void hint_macro_solver::process(func_decl* f) { + SASSERT(m_satisfied.empty()); + SASSERT(m_residue.empty()); + greedy(f, 0); +} + +/** + \brief Copy the quantifiers from qcandidates to new_qs that are not in m_satisfied. +*/ +void hint_macro_solver::copy_non_satisfied(ptr_vector const& qcandidates, ptr_vector& new_qs) { + for (quantifier* q : qcandidates) { + if (!m_satisfied.contains(q)) + new_qs.push_back(q); + } +} + +/** + \brief Use m_fs to set the interpretation of the function symbols that were used to satisfy the + quantifiers in m_satisfied. +*/ +void hint_macro_solver::set_interp() { + for (auto const& kv : m_fs) { + func_decl* f = kv.m_key; + expr* def = kv.m_value; + set_else_interp(f, def); + } +} + +void hint_macro_solver::reset() { + reset_q_fs(); + m_forbidden.reset(); + m_candidates.reset(); + m_satisfied.reset(); + m_residue.reset(); + m_fs.reset(); +} + +bool hint_macro_solver::process(ptr_vector const& qs, ptr_vector& new_qs, ptr_vector& residue) { + reset(); + ptr_vector qcandidates; + preprocess(qs, qcandidates, new_qs); + if (qcandidates.empty()) { + SASSERT(new_qs.size() == qs.size()); + return false; + } + mk_q_f_defs(qcandidates); + TRACE("model_finder_hint", tout << "starting hint-solver search using:\n"; display_qcandidates(tout, qcandidates);); + for (func_decl* f : m_candidates) { + try { + process(f); + } + catch (const found_satisfied_subset&) { + set_interp(); + copy_non_satisfied(qcandidates, new_qs); + return true; + } + } + // failed... copy everything to new_qs + new_qs.append(qcandidates); + return false; +} + +/** +\brief Satisfy clauses that are not in the AUF fragment but define conditional macros. +These clauses are eliminated even if the symbol being defined occurs in other quantifiers. +The auf_solver is ineffective in these clauses. + +\remark Full macros are used even if they are in the AUF fragment. +*/ + +bool non_auf_macro_solver::add_macro(func_decl* f, expr* f_else) { + TRACE("model_finder", tout << "trying to add macro for " << f->get_name() << "\n" << mk_pp(f_else, m) << "\n";); + func_decl_set* s = m_dependencies.mk_func_decl_set(); + m_dependencies.collect_ng_func_decls(f_else, s); + if (!m_dependencies.insert(f, s)) { + TRACE("model_finder", tout << "failed to add macro\n";); + return false; // cyclic dependency + } + set_else_interp(f, f_else); + return true; +} + +// Return true if r1 is a better macro than r2. +bool non_auf_macro_solver::is_better_macro(cond_macro* r1, cond_macro* r2) { + if (r2 == nullptr || !r1->is_hint()) + return true; + if (!r2->is_hint()) + return false; + SASSERT(r1->is_hint() && r2->is_hint()); + if (is_ground(r1->get_def()) && !is_ground(r2->get_def())) + return true; + return false; +} + +cond_macro* non_auf_macro_solver::get_macro_for(func_decl* f, quantifier* q) { + cond_macro* r = nullptr; + quantifier_macro_info* qi = get_qinfo(q); + for (cond_macro* m : qi->macros()) { + if (m->get_f() == f && !m->is_hint() && is_better_macro(m, r)) + r = m; + } + return r; +} + +typedef std::pair mq_pair; + +void non_auf_macro_solver::collect_candidates(ptr_vector const& qs, obj_map& full_macros, func_decl_set& cond_macros) { + for (quantifier* q : qs) { + quantifier_macro_info* qi = get_qinfo(q); + for (cond_macro* m : qi->macros()) { + if (!m->is_hint()) { + func_decl* f = m->get_f(); + TRACE("model_finder", tout << "considering macro for: " << f->get_name() << "\n"; + m->display(tout); tout << "\n";); + if (m->is_unconditional() && (!qi->is_auf() || m->get_weight() >= m_mbqi_force_template)) { + full_macros.insert(f, std::make_pair(m, q)); + cond_macros.erase(f); + } + else if (!full_macros.contains(f) && !qi->is_auf()) + cond_macros.insert(f); + } + } + } +} + +void non_auf_macro_solver::process_full_macros(obj_map const& full_macros, obj_hashtable& removed) { + for (auto const& kv : full_macros) { + func_decl* f = kv.m_key; + cond_macro* m = kv.m_value.first; + quantifier* q = kv.m_value.second; + SASSERT(m->is_unconditional()); + if (add_macro(f, m->get_def())) { + get_qinfo(q)->set_the_one(f); + removed.insert(q); + } + } +} + +void non_auf_macro_solver::process(func_decl* f, ptr_vector const& qs, obj_hashtable& removed) { + expr_ref fi_else(m); + ptr_buffer to_remove; + for (quantifier* q : qs) { + if (removed.contains(q)) + continue; + cond_macro* cm = get_macro_for(f, q); + if (!cm) + continue; + SASSERT(!cm->is_hint()); + if (cm->is_unconditional()) + return; // f is part of a full macro... ignoring it. + to_remove.push_back(q); + if (fi_else.get() == nullptr) { + fi_else = cm->get_def(); + } + else { + fi_else = m.mk_ite(cm->get_cond(), cm->get_def(), fi_else); + } + } + if (fi_else.get() != nullptr && add_macro(f, fi_else)) { + for (quantifier* q : to_remove) { + get_qinfo(q)->set_the_one(f); + removed.insert(q); + } + } +} + +void non_auf_macro_solver::process_cond_macros(func_decl_set const& cond_macros, ptr_vector const& qs, obj_hashtable& removed) { + for (func_decl* f : cond_macros) { + process(f, qs, removed); + } +} + +bool non_auf_macro_solver::process(ptr_vector const& qs, ptr_vector& new_qs, ptr_vector& residue) { + obj_map full_macros; + func_decl_set cond_macros; + obj_hashtable removed; + + // Possible improvement: sort full_macros & cond_macros using an user provided precedence function. + + collect_candidates(qs, full_macros, cond_macros); + process_full_macros(full_macros, removed); + process_cond_macros(cond_macros, qs, removed); + + for (quantifier* q : qs) { + if (removed.contains(q)) + continue; + new_qs.push_back(q); + residue.push_back(q); + } + return !removed.empty(); +} + + diff --git a/src/model/model_macro_solver.h b/src/model/model_macro_solver.h new file mode 100644 index 000000000..1c04f8ec1 --- /dev/null +++ b/src/model/model_macro_solver.h @@ -0,0 +1,308 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Abstract: + + Macro solving utilities + +Author: + + Leonardo de Moura (leonardo) 2010-12-17. + +--*/ + +#pragma once +#include "util/obj_pair_hashtable.h" +#include "util/backtrackable_set.h" +#include "ast/macros/quantifier_macro_info.h" +#include "model/model_core.h" + + +class quantifier2macro_infos { +public: + virtual ~quantifier2macro_infos() {} + virtual quantifier_macro_info* operator()(quantifier* q) = 0; +}; + +/** + \brief Base class for macro solvers. +*/ +class base_macro_solver { +protected: + ast_manager& m; + quantifier2macro_infos& m_q2info; + model_core* m_model; + + quantifier_macro_info* get_qinfo(quantifier* q) const { + return m_q2info(q); + } + + void set_else_interp(func_decl* f, expr* f_else); + + virtual bool process(ptr_vector const& qs, ptr_vector& new_qs, ptr_vector& residue) = 0; + +public: + base_macro_solver(ast_manager& m, quantifier2macro_infos& q2i) : + m(m), + m_q2info(q2i), + m_model(nullptr) { + } + + virtual ~base_macro_solver() {} + + /** + \brief Try to satisfy quantifiers in qs by using macro definitions. + Store in new_qs the quantifiers that were not satisfied. + Store in residue a subset of the quantifiers that were satisfied but contain information useful for the auf_solver. + */ + void operator()(model_core& m, ptr_vector& qs, ptr_vector& residue); +}; + +/** + \brief The simple macro solver satisfies quantifiers that contain + (conditional) macros for a function f that does not occur in any other quantifier. + + Since f does not occur in any other quantifier, I don't need to track the dependencies + of f. That is, recursive definition cannot be created. +*/ +class simple_macro_solver : public base_macro_solver { +protected: + /** + \brief Return true if \c f is in (qs\{q}) + */ + bool contains(func_decl* f, ptr_vector const& qs, quantifier* q); + + bool process(quantifier* q, ptr_vector const& qs); + + bool process(ptr_vector const& qs, ptr_vector& new_qs, ptr_vector& residue) override; + +public: + simple_macro_solver(ast_manager& m, quantifier2macro_infos& q2i) : + base_macro_solver(m, q2i) {} +}; + + +class hint_macro_solver : public base_macro_solver { + /* + This solver tries to satisfy quantifiers by using macros, cond_macros and hints. + The idea is to satisfy a set of quantifiers Q = Q_{f_1} union ... union Q_{f_n} + where Q_{f_i} is the set of quantifiers that contain the function f_i. + Let f_i = def_i be macros (in this solver conditions are ignored). + Let Q_{f_i = def_i} be the set of quantifiers where f_i = def_i is a macro. + Then, the set Q can be satisfied using f_1 = def_1 ... f_n = def_n + when + + Q_{f_1} union ... union Q_{f_n} = Q_{f_1 = def_1} ... Q_{f_n = def_n} (*) + + So, given a set of macros f_1 = def_1, ..., f_n = d_n, it is very easy to check + whether they can be used to satisfy all quantifiers that use f_1, ..., f_n in + non ground terms. + + We can find the sets of f_1 = def_1, ..., f_n = def_n that satisfy Q using + the following search procedure + find(Q) + for each f_i = def_i in Q + R = greedy(Q_{f_i = def_1}, Q_f_i \ Q_{f_i = def_i}, {f_i}, {f_i = def_i}) + if (R != empty-set) + return R + greedy(Satisfied, Residue, F, F_DEF) + if Residue = empty-set return F_DEF + for each f_j = def_j in Residue such that f_j not in F + New-Satisfied = Satisfied union Q_{f_j = def_j} + New-Residue = (Residue union Q_{f_j}) \ New-Satisfied + R = greedy(New-Satisfied, New-Residue, F \union {f_j}, F_DEF union {f_j = def_j}) + if (R != empty-set) + return R + + This search may be too expensive, and is exponential on the number of different function + symbols. + Some observations to prune the search space. + 1) If f_i occurs in a quantifier without macros, then f_i and any macro using it can be ignored during the search. + 2) If f_i = def_i is not a macro in a quantifier q, and there is no other f_j = def_j (i != j) in q, + then f_i = def_i can be ignored during the search. + */ + + typedef obj_hashtable quantifier_set; + typedef obj_map q_f; + typedef obj_pair_map q_f_def; + typedef obj_pair_hashtable f_def_set; + typedef obj_hashtable expr_set; + typedef obj_map f2defs; + + q_f m_q_f; + q_f_def m_q_f_def; + ptr_vector m_qsets; + f2defs m_f2defs; + ptr_vector m_esets; + + void insert_q_f(quantifier* q, func_decl* f); + + void insert_f2def(func_decl* f, expr* def); + void insert_q_f_def(quantifier* q, func_decl* f, expr* def); + + quantifier_set* get_q_f_def(func_decl* f, expr* def); + + expr_set* get_f_defs(func_decl* f) { return m_f2defs[f]; } + quantifier_set* get_q_f(func_decl* f) { return m_q_f[f]; } + + void reset_q_fs(); + + func_decl_set m_forbidden; + func_decl_set m_candidates; + + bool is_candidate(quantifier* q) const; + void register_decls_as_forbidden(quantifier* q); + + void preprocess(ptr_vector const& qs, ptr_vector& qcandidates, ptr_vector& non_qcandidates); + + void mk_q_f_defs(ptr_vector const& qs); + + static void display_quantifier_set(std::ostream& out, quantifier_set const* s); + + void display_qcandidates(std::ostream& out, ptr_vector const& qcandidates) const; + + // + // Search: main procedures + // + + struct ev_handler { + hint_macro_solver* m_owner; + + void operator()(quantifier* q, bool ins) { + quantifier_macro_info* qi = m_owner->get_qinfo(q); + qi->set_the_one(nullptr); + } + + ev_handler(hint_macro_solver* o) : + m_owner(o) { + } + }; + + + typedef backtrackable_set qset; + typedef backtrackable_set qsset; + typedef obj_map f2def; + + qset m_residue; + qsset m_satisfied; + f2def m_fs; // set of function symbols (and associated interpretation) that were used to satisfy the quantifiers in m_satisfied. + + struct found_satisfied_subset {}; + + void display_search_state(std::ostream& out) const; + bool check_satisfied_residue_invariant(); + + + bool update_satisfied_residue(func_decl* f, expr* def); + + /** + \brief Extract from m_residue, func_decls that can be used as macros to satisfy it. + The candidates must not be elements of m_fs. + */ + void get_candidates_from_residue(func_decl_set& candidates); + + /** + \brief Try to reduce m_residue using the macros of f. + */ + void greedy(func_decl* f, unsigned depth); + + /** + \brief check if satisfied subset introduces a cyclic dependency. + + f_1 = def_1(f_2), ..., f_n = def_n(f_1) + */ + + expr_mark m_visited; + obj_hashtable m_acyclic; + bool is_cyclic(); + struct occurs {}; + struct occurs_check { + hint_macro_solver& m_cls; + occurs_check(hint_macro_solver& hs) : m_cls(hs) {} + void operator()(app* n) { if (m_cls.m_fs.contains(n->get_decl()) && !m_cls.m_acyclic.contains(n->get_decl())) throw occurs(); } + void operator()(var* n) {} + void operator()(quantifier* n) {} + }; + bool is_acyclic(expr* def); + + /** + \brief Try to reduce m_residue (if not empty) by selecting a function f + that is a macro in the residue. + */ + void greedy(unsigned depth); + + /** + \brief Try to find a set of quantifiers by starting to use the macros of f. + This is the "find" procedure in the comments above. + The set of satisfied quantifiers is in m_satisfied, and the remaining to be + satisfied in m_residue. When the residue becomes empty we throw the exception found_satisfied_subset. + */ + void process(func_decl* f); + + /** + \brief Copy the quantifiers from qcandidates to new_qs that are not in m_satisfied. + */ + void copy_non_satisfied(ptr_vector const& qcandidates, ptr_vector& new_qs); + /** + \brief Use m_fs to set the interpretation of the function symbols that were used to satisfy the + quantifiers in m_satisfied. + */ + void set_interp(); + + void reset(); + + bool process(ptr_vector const& qs, ptr_vector& new_qs, ptr_vector& residue) override; + +public: + hint_macro_solver(ast_manager& m, quantifier2macro_infos& q2i) : + base_macro_solver(m, q2i), + m_satisfied(ev_handler(this)) { + } + + ~hint_macro_solver() override { + reset(); + } + +}; + +/** +\brief Satisfy clauses that are not in the AUF fragment but define conditional macros. +These clauses are eliminated even if the symbol being defined occurs in other quantifiers. +The auf_solver is ineffective in these clauses. + +\remark Full macros are used even if they are in the AUF fragment. +*/ + +class non_auf_macro_solver : public base_macro_solver { + func_decl_dependencies& m_dependencies; + unsigned m_mbqi_force_template{ 0 }; + + bool add_macro(func_decl* f, expr* f_else); + + // Return true if r1 is a better macro than r2. + bool is_better_macro(cond_macro* r1, cond_macro* r2); + + cond_macro* get_macro_for(func_decl* f, quantifier* q); + + typedef std::pair mq_pair; + + void collect_candidates(ptr_vector const& qs, obj_map& full_macros, func_decl_set& cond_macros); + + void process_full_macros(obj_map const& full_macros, obj_hashtable& removed); + + void process(func_decl* f, ptr_vector const& qs, obj_hashtable& removed); + + void process_cond_macros(func_decl_set const& cond_macros, ptr_vector const& qs, obj_hashtable& removed); + + bool process(ptr_vector const& qs, ptr_vector& new_qs, ptr_vector& residue) override; + +public: + non_auf_macro_solver(ast_manager& m, quantifier2macro_infos& q2i, func_decl_dependencies& d) : + base_macro_solver(m, q2i), + m_dependencies(d) { + } + + void set_mbqi_force_template(unsigned n) { m_mbqi_force_template = n; } +}; + + diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h index fd341059e..e8f40cdca 100644 --- a/src/sat/sat_extension.h +++ b/src/sat/sat_extension.h @@ -57,14 +57,16 @@ namespace sat { protected: bool m_drating { false }; int m_id { 0 }; + symbol m_name; solver* m_solver { nullptr }; public: - extension(int id): m_id(id) {} + extension(symbol const& name, int id): m_id(id), m_name(name) {} virtual ~extension() {} int get_id() const { return m_id; } void set_solver(solver* s) { m_solver = s; } solver& s() { return *m_solver; } solver const& s() const { return *m_solver; } + symbol const& name() const { return m_name; } virtual void set_lookahead(lookahead* s) {}; class scoped_drating { diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index 12c522a70..0b00b4f5a 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -26,6 +26,7 @@ z3_add_component(sat_smt fpa_solver.cpp q_mbi.cpp q_model_finder.cpp + q_model_fixer.cpp q_solver.cpp sat_dual_solver.cpp sat_th.cpp diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp index 7f01533b0..95cb52ff2 100644 --- a/src/sat/smt/array_solver.cpp +++ b/src/sat/smt/array_solver.cpp @@ -75,7 +75,7 @@ For example namespace array { solver::solver(euf::solver& ctx, theory_id id) : - th_euf_solver(ctx, id), + th_euf_solver(ctx, symbol("array"), id), a(m), m_sort2epsilon(m), m_sort2diag(m), diff --git a/src/sat/smt/ba_solver.cpp b/src/sat/smt/ba_solver.cpp index ba0553aa0..bc15b8a58 100644 --- a/src/sat/smt/ba_solver.cpp +++ b/src/sat/smt/ba_solver.cpp @@ -1363,7 +1363,7 @@ namespace sat { ba_solver(ctx.get_manager(), ctx.get_si(), id) {} ba_solver::ba_solver(ast_manager& m, sat::sat_internalizer& si, euf::theory_id id) - : euf::th_solver(m, id), + : euf::th_solver(m, symbol("ba"), id), si(si), m_pb(m), m_lookahead(nullptr), m_constraint_id(0), m_ba(*this), m_sort(m_ba) { diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index d09affb91..b1c9fcf2b 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -50,7 +50,7 @@ namespace bv { }; solver::solver(euf::solver& ctx, theory_id id) : - euf::th_euf_solver(ctx, id), + euf::th_euf_solver(ctx, symbol("bv"), id), bv(m), m_autil(m), m_ackerman(*this), diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 85bbd72e2..0be711400 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -29,7 +29,7 @@ Author: namespace euf { solver::solver(ast_manager& m, sat::sat_internalizer& si, params_ref const& p) : - extension(m.mk_family_id("euf")), + extension(symbol("euf"), m.mk_family_id("euf")), m(m), si(si), m_egraph(m), @@ -76,7 +76,7 @@ namespace euf { } th_solver* solver::quantifier2solver() { - family_id fid = m.mk_family_id(q::solver::name()); + family_id fid = m.mk_family_id(symbol("quant")); auto* ext = m_id2solver.get(fid, nullptr); if (ext) return ext; @@ -99,27 +99,18 @@ namespace euf { bv_util bvu(m); array_util au(m); fpa_util fpa(m); - if (pb.get_family_id() == fid) { + if (pb.get_family_id() == fid) ext = alloc(sat::ba_solver, *this, fid); - if (use_drat()) - s().get_drat().add_theory(fid, symbol("ba")); - } - else if (bvu.get_family_id() == fid) { + else if (bvu.get_family_id() == fid) ext = alloc(bv::solver, *this, fid); - if (use_drat()) - s().get_drat().add_theory(fid, symbol("bv")); - } - else if (au.get_family_id() == fid) { + else if (au.get_family_id() == fid) ext = alloc(array::solver, *this, fid); - if (use_drat()) - s().get_drat().add_theory(fid, symbol("array")); - } - else if (fpa.get_family_id() == fid) { + else if (fpa.get_family_id() == fid) ext = alloc(fpa::solver, *this); - if (use_drat()) - s().get_drat().add_theory(fid, symbol("fpa")); - } + if (ext) { + if (use_drat()) + s().get_drat().add_theory(fid, ext->name()); ext->set_solver(m_solver); ext->push_scopes(s().num_scopes()); add_solver(fid, ext); diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp index fefce8c9c..ceb36daf3 100644 --- a/src/sat/smt/fpa_solver.cpp +++ b/src/sat/smt/fpa_solver.cpp @@ -23,7 +23,7 @@ Revision History: namespace fpa { solver::solver(euf::solver& ctx) : - euf::th_euf_solver(ctx, ctx.get_manager().mk_family_id("fpa")), + euf::th_euf_solver(ctx, symbol("fpa"), ctx.get_manager().mk_family_id("fpa")), m_th_rw(ctx.get_manager()), m_converter(ctx.get_manager(), m_th_rw), m_rw(ctx.get_manager(), m_converter, params_ref()), @@ -65,7 +65,7 @@ namespace fpa { m.inc_ref(e); m.inc_ref(res); - ctx.push(fpa2bv_conversion_trail_elem(m, m_conversions, e)); + ctx.push(insert_ref2_map(m, m_conversions, e, res.get())); } return res; } diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index 4385c786f..eba177f1a 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -26,8 +26,13 @@ Author: namespace q { mbqi::mbqi(euf::solver& ctx, solver& s): - ctx(ctx), qs(s), m(s.get_manager()), m_model_finder(ctx), m_fresh_trail(m) {} - + ctx(ctx), + qs(s), + m(s.get_manager()), + m_model_fixer(ctx, qs), + m_model_finder(ctx), + m_fresh_trail(m) + {} void mbqi::restrict_to_universe(expr * sk, ptr_vector const & universe) { SASSERT(!universe.empty()); @@ -97,7 +102,7 @@ namespace q { if (r == l_false) return l_true; model_ref mdl0, mdl1; - m_solver->get_model(mdl0); + m_solver->get_model(mdl0); expr_ref proj(m); auto add_projection = [&](model& mdl, bool inv) { proj = project(mdl, q, vars, inv); @@ -222,4 +227,8 @@ namespace q { m_max_cex = ctx.get_config().m_mbqi_max_cexs; } + void mbqi::finalize_model(model& mdl) { + m_model_fixer(mdl); + } + } diff --git a/src/sat/smt/q_mbi.h b/src/sat/smt/q_mbi.h index da0565170..541de3fa5 100644 --- a/src/sat/smt/q_mbi.h +++ b/src/sat/smt/q_mbi.h @@ -19,7 +19,7 @@ Author: #include "solver/solver.h" #include "sat/smt/sat_th.h" #include "sat/smt/q_model_finder.h" - +#include "sat/smt/q_model_fixer.h" namespace euf { class solver; @@ -33,13 +33,14 @@ namespace q { euf::solver& ctx; solver& qs; ast_manager& m; + model_fixer m_model_fixer; model_finder m_model_finder; model_ref m_model; ref<::solver> m_solver; obj_map*> m_fresh; scoped_ptr_vector> m_values; expr_ref_vector m_fresh_trail; - unsigned m_max_cex{ 10 }; + unsigned m_max_cex{ 1 }; void restrict_to_universe(expr * sk, ptr_vector const & universe); void register_value(expr* e); @@ -58,6 +59,8 @@ namespace q { lbool operator()(); void init_search(); + + void finalize_model(model& mdl); }; } diff --git a/src/sat/smt/q_model_finder.cpp b/src/sat/smt/q_model_finder.cpp index ff326daa0..3777709f5 100644 --- a/src/sat/smt/q_model_finder.cpp +++ b/src/sat/smt/q_model_finder.cpp @@ -36,4 +36,8 @@ namespace q { } + void model_finder::adjust_model(model& mdl) { + + } + } diff --git a/src/sat/smt/q_model_finder.h b/src/sat/smt/q_model_finder.h index aec1bfd7a..f9ac8bdc0 100644 --- a/src/sat/smt/q_model_finder.h +++ b/src/sat/smt/q_model_finder.h @@ -37,9 +37,23 @@ namespace q { model_finder(euf::solver& ctx); + /** + * Compute an instantiation terms for the i'th bound variable in quantifier q. + */ expr_ref inv_term(model& mdl, quantifier* q, unsigned idx, expr* value, unsigned& generation); + /** + * Pre-restrict instantiations of vars, by adding constraints to solver s + */ void restrict_instantiations(::solver& s, model& mdl, quantifier* q, expr_ref_vector const& vars); + + /** + * Update model in order to best satisfy quantifiers. + * For the array property fragment, update the model + * such that the range of functions behaves monotonically + * based on regions over the inputs. + */ + void adjust_model(model& mdl); }; diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp new file mode 100644 index 000000000..177fa04e9 --- /dev/null +++ b/src/sat/smt/q_model_fixer.cpp @@ -0,0 +1,198 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + q_model_fixer.cpp + +Abstract: + + Model-based quantifier instantiation model-finder plugin + +Author: + + Nikolaj Bjorner (nbjorner) 2020-10-02 + +Notes: + + Derives from smt/smt_model_finder.cpp + +--*/ + + +#include "ast/for_each_expr.h" +#include "ast/arith_decl_plugin.h" +#include "ast/bv_decl_plugin.h" +#include "model/model_macro_solver.h" +#include "sat/smt/q_model_fixer.h" +#include "sat/smt/q_solver.h" +#include "sat/smt/euf_solver.h" + + +namespace q { + + template + static bool lt(U const& u, expr* x, expr* y) { + rational v1, v2; + if (u.is_numeral(x, v1) && u.is_numeral(y, v2)) + return v1 < v2; + else + return x->get_id() < y->get_id(); + } + + class arith_projection : public projection_function { + ast_manager& m; + arith_util a; + public: + bool operator()(expr* e1, expr* e2) const { return lt(a, e1, e2); } + arith_projection(ast_manager& m): m(m), a(m) {} + ~arith_projection() override {} + void sort(ptr_buffer& values) override { std::sort(values.begin(), values.end(), *this); } + expr* mk_lt(expr* x, expr* y) override { return a.mk_lt(x, y); } + }; + + class ubv_projection : public projection_function { + ast_manager& m; + bv_util bvu; + public: + bool operator()(expr* e1, expr* e2) const { return lt(bvu, e1, e2); } + ubv_projection(ast_manager& m): m(m), bvu(m) {} + ~ubv_projection() override {} + void sort(ptr_buffer& values) override { std::sort(values.begin(), values.end(), *this); } + expr* mk_lt(expr* x, expr* y) override { return m.mk_not(bvu.mk_ule(y, x)); } + }; + + model_fixer::model_fixer(euf::solver& ctx, q::solver& qs) : + ctx(ctx), m_qs(qs), m(ctx.get_manager()), m_dependencies(m) {} + + void model_fixer::operator()(model& mdl) { + ptr_vector univ; + for (sat::literal lit : m_qs.universal()) { + quantifier* q = to_quantifier(ctx.bool_var2expr(lit.var())); + if (ctx.is_relevant(q)) + univ.push_back(q); + } + if (univ.empty()) + return; + + m_dependencies.reset(); + ptr_vector residue; + + simple_macro_solver sms(m, *this); + sms(mdl, univ, residue); + + hint_macro_solver hms(m, *this); + hms(mdl, univ, residue); + + non_auf_macro_solver nas(m, *this, m_dependencies); + nas.set_mbqi_force_template(ctx.get_config().m_mbqi_force_template); + nas(mdl, univ, residue); + + univ.append(residue); + add_projection_functions(mdl, univ); + } + + quantifier_macro_info* model_fixer::operator()(quantifier* q) { + quantifier_macro_info* info = nullptr; + if (!m_q2info.find(q, info)) { + info = alloc(quantifier_macro_info, m, m_qs.flatten(q)); + m_q2info.insert(q, info); + ctx.push(new_obj_trail(info)); + ctx.push(insert_obj_map(m_q2info, q)); + } + return info; + } + + void model_fixer::add_projection_functions(model& mdl, ptr_vector const& qs) { + func_decl_set fns; + collect_partial_functions(qs, fns); + for (func_decl* f : fns) + add_projection_functions(mdl, f); + } + + void model_fixer::add_projection_functions(model& mdl, func_decl* f) { + // update interpretation of f so that the graph of f is fully determined by the + // ground values of its arguments. + func_interp* fi = mdl.get_func_interp(f); + if (!fi) + return; + if (fi->is_constant()) + return; + expr_ref_vector args(m); + for (unsigned i = 0; i < f->get_arity(); ++i) + args.push_back(add_projection_function(mdl, f, i)); + if (!fi->get_else() && fi->num_entries() > 0) + fi->set_else(fi->get_entry(ctx.s().rand()(fi->num_entries()))->get_result()); + bool has_projection = false; + for (expr* arg : args) + has_projection |= !is_var(arg); + if (!has_projection) + return; + func_interp* new_fi = alloc(func_interp, m, f->get_arity()); + func_decl* f_new = m.mk_fresh_func_decl(f->get_name(), symbol("aux"), f->get_arity(), f->get_domain(), f->get_range()); + new_fi->set_else(m.mk_app(f_new, args)); + mdl.update_func_interp(f, new_fi); + mdl.register_decl(f_new, fi); + } + + expr_ref model_fixer::add_projection_function(model& mdl, func_decl* f, unsigned idx) { + sort* srt = f->get_domain(idx); + projection_function* proj = get_projection(srt); + if (!proj) + return expr_ref(m.mk_var(idx, srt), m); + ptr_buffer values; + for (euf::enode* n : ctx.get_egraph().enodes_of(f)) + values.push_back(mdl(n->get_arg(idx)->get_expr())); + if (values.empty()) + return expr_ref(m.mk_var(idx, srt), m); + proj->sort(values); + unsigned j = 0; + for (unsigned i = 0; i < values.size(); ++i) + if (i == 0 || values[i-1] != values[i]) + values[j++] = values[i]; + values.shrink(j); + + unsigned sz = values.size(); + expr_ref var(m.mk_var(0, srt), m); + expr_ref pi(values.get(sz-1), m); + for (unsigned i = sz - 1; i >= 1; i--) { + expr* c = proj->mk_lt(var, values[i]); + pi = m.mk_ite(c, values[i - 1], pi); + } + func_interp* rpi = alloc(func_interp, m, 1); + rpi->set_else(pi); + func_decl * p = m.mk_fresh_func_decl(1, &srt, srt); + mdl.register_decl(p, rpi); + return expr_ref(m.mk_app(p, m.mk_var(idx, srt)), m); + } + + projection_function* model_fixer::get_projection(sort* srt) { + projection_function* proj = nullptr; + if (m_projections.find(srt, proj)) + return proj; + arith_util autil(m); + bv_util butil(m); + if (autil.is_real(srt) || autil.is_int(srt)) + proj = alloc(arith_projection, m); + else if (butil.is_bv_sort(srt)) + proj = alloc(ubv_projection, m); + // TBD: sbv_projection? FP, ADT projection? + if (!proj) + return nullptr; + m_projections.insert(srt, proj); + ctx.push(new_obj_trail(proj)); + ctx.push(insert_obj_map(m_projections, srt)); + return proj; + } + + void model_fixer::collect_partial_functions(ptr_vector const& qs, func_decl_set& fns) { + for (quantifier* q : qs) { + auto* info = (*this)(q); + quantifier* flat_q = info->get_flat_q(); + expr_ref body(flat_q->get_expr(), m); + for (expr* t : subterms(body)) + if (is_uninterp(t) && !to_app(t)->is_ground()) + fns.insert(to_app(t)->get_decl()); + } + } +} diff --git a/src/sat/smt/q_model_fixer.h b/src/sat/smt/q_model_fixer.h new file mode 100644 index 000000000..b10ef2551 --- /dev/null +++ b/src/sat/smt/q_model_fixer.h @@ -0,0 +1,78 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + q_model_fixer.h + +Abstract: + + Model-based quantifier instantiation model-finder plugin + +Author: + + Nikolaj Bjorner (nbjorner) 2020-10-02 + +Notes: + + Derives from smt/smt_model_finder.cpp + + Contains exclusively functionality that adjusts a model to make it + easier to satisfy relevant universally quantified literals. + +--*/ +#pragma once + +#include "sat/smt/sat_th.h" +#include "solver/solver.h" +#include "model/model_macro_solver.h" + +namespace euf { + class solver; +} + +namespace q { + + class solver; + + typedef obj_hashtable func_decl_set; + + class projection_function { + public: + virtual ~projection_function() {} + virtual void sort(ptr_buffer& values) = 0; + virtual expr* mk_lt(expr* a, expr* b) = 0; + }; + + class model_fixer : public quantifier2macro_infos { + euf::solver& ctx; + solver& m_qs; + ast_manager& m; + obj_map m_q2info; + func_decl_dependencies m_dependencies; + obj_map m_projections; + + void add_projection_functions(model& mdl, ptr_vector const& qs); + void add_projection_functions(model& mdl, func_decl* f); + expr_ref add_projection_function(model& mdl, func_decl* f, unsigned idx); + void collect_partial_functions(ptr_vector const& qs, func_decl_set& fns); + projection_function* get_projection(sort* srt); + + public: + + model_fixer(euf::solver& ctx, solver& qs); + ~model_fixer() override {} + + /** + * Update model in order to best satisfy quantifiers. + * For the array property fragment, update the model + * such that the range of functions behaves monotonically + * based on regions over the inputs. + */ + void operator()(model& mdl); + + quantifier_macro_info* operator()(quantifier* q); + + }; + +} diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index bded7ecc8..97adc6ae6 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -19,13 +19,14 @@ Author: #include "sat/smt/q_solver.h" #include "sat/smt/euf_solver.h" #include "sat/smt/sat_th.h" - +#include "ast/normal_forms/pull_quant.h" +#include "ast/well_sorted.h" namespace q { solver::solver(euf::solver& ctx): - th_euf_solver(ctx, ctx.get_manager().get_family_id(name())), - m_mbqi(ctx, *this) + th_euf_solver(ctx, symbol("quant"), ctx.get_manager().get_family_id(symbol("quant"))), + m_mbqi(ctx, *this) {} void solver::asserted(sat::literal l) { @@ -43,10 +44,12 @@ namespace q { } sat::check_result solver::check() { - switch (m_mbqi()) { - case l_true: return sat::check_result::CR_DONE; - case l_false: return sat::check_result::CR_CONTINUE; - case l_undef: return sat::check_result::CR_GIVEUP; + if (ctx.get_config().m_mbqi) { + switch (m_mbqi()) { + case l_true: return sat::check_result::CR_DONE; + case l_false: return sat::check_result::CR_CONTINUE; + case l_undef: return sat::check_result::CR_GIVEUP; + } } return sat::check_result::CR_GIVEUP; } @@ -117,4 +120,27 @@ namespace q { mk_var(ctx.get_egraph().find(e)); return lit; } + + void solver::finalize_model(model& mdl) { + m_mbqi.finalize_model(mdl); + } + + quantifier* solver::flatten(quantifier* q) { + quantifier* q_flat = nullptr; + if (!has_quantifiers(q->get_expr())) + return q; + if (m_flat.find(q, q_flat)) + return q_flat; + proof_ref pr(m); + expr_ref new_q(m); + pull_quant pull(m); + pull(q, new_q, pr); + SASSERT(is_well_sorted(m, new_q)); + q_flat = to_quantifier(new_q); + m.inc_ref(q_flat); + m.inc_ref(q); + m_flat.insert(q, q_flat); + ctx.push(insert_ref2_map(m, m_flat, q, q_flat)); + return q_flat; + } } diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h index e4662d6aa..58574544e 100644 --- a/src/sat/smt/q_solver.h +++ b/src/sat/smt/q_solver.h @@ -30,6 +30,7 @@ namespace q { class solver : public euf::th_euf_solver { typedef obj_map skolem_table; + typedef obj_map flat_table; friend class mbqi; struct stats { @@ -42,6 +43,7 @@ namespace q { mbqi m_mbqi; skolem_table m_skolems; + flat_table m_flat; sat::literal_vector m_universal; sat::literal skolemize(quantifier* q); @@ -51,7 +53,6 @@ namespace q { solver(euf::solver& ctx); ~solver() override {} - static char const* name() { return "quant"; } bool is_external(sat::bool_var v) override { return false; } void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override {} void asserted(sat::literal l) override; @@ -67,7 +68,10 @@ namespace q { void internalize(expr* e, bool redundant) override { UNREACHABLE(); } euf::theory_var mk_var(euf::enode* n) override; void init_search() override; + void finalize_model(model& mdl) override; ast_manager& get_manager() { return m; } + sat::literal_vector const& universal() const { return m_universal; } + quantifier* flatten(quantifier* q); }; } diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index 3406dc284..a9ddaa7d7 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -52,8 +52,8 @@ namespace euf { return true; } - th_euf_solver::th_euf_solver(euf::solver& ctx, euf::theory_id id): - th_solver(ctx.get_manager(), id), + th_euf_solver::th_euf_solver(euf::solver& ctx, symbol const& name, euf::theory_id id): + th_solver(ctx.get_manager(), name, id), ctx(ctx) {} diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 033ca85ac..48c80a8d3 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -97,7 +97,7 @@ namespace euf { protected: ast_manager & m; public: - th_solver(ast_manager& m, euf::theory_id id): extension(id), m(m) {} + th_solver(ast_manager& m, symbol const& name, euf::theory_id id): extension(name, id), m(m) {} virtual th_solver* clone(sat::solver* s, euf::solver& ctx) = 0; @@ -158,7 +158,7 @@ namespace euf { } public: - th_euf_solver(euf::solver& ctx, euf::theory_id id); + th_euf_solver(euf::solver& ctx, symbol const& name, euf::theory_id id); virtual ~th_euf_solver() {} virtual theory_var mk_var(enode * n); unsigned get_num_vars() const { return m_var2enode.size();} diff --git a/src/sat/smt/user_solver.cpp b/src/sat/smt/user_solver.cpp index f7fdb9364..c50b91ec2 100644 --- a/src/sat/smt/user_solver.cpp +++ b/src/sat/smt/user_solver.cpp @@ -21,7 +21,7 @@ Author: namespace user { solver::solver(euf::solver& ctx) : - th_euf_solver(ctx, ctx.get_manager().mk_family_id("user")) + th_euf_solver(ctx, symbol("user"), ctx.get_manager().mk_family_id("user")) {} solver::~solver() { diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h index 0c3097ef7..c6006bcb3 100644 --- a/src/smt/smt_model_checker.h +++ b/src/smt/smt_model_checker.h @@ -54,7 +54,7 @@ namespace smt { obj_map m_value2expr; expr_ref_vector m_fresh_exprs; - friend class instantiation_set; + friend class model_instantiation_set; void init_aux_context(); void init_value2expr(); diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 93837826b..9647bca81 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -24,12 +24,15 @@ Revision History: #include "ast/array_decl_plugin.h" #include "ast/normal_forms/pull_quant.h" #include "ast/rewriter/var_subst.h" +#include "ast/macros/cond_macro.h" +#include "ast/macros/quantifier_macro_info.h" #include "ast/for_each_expr.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "ast/well_sorted.h" #include "ast/ast_smt2_pp.h" #include "model/model_pp.h" +#include "model/model_macro_solver.h" #include "smt/smt_model_finder.h" #include "smt/smt_context.h" #include "tactic/tactic_exception.h" @@ -44,25 +47,10 @@ namespace smt { // // ----------------------------------- - // Append the new elements of v2 into v1. v2 should not be used after this operation, since it may suffer destructive updates. - template - void dappend(ptr_vector & v1, ptr_vector & v2) { - if (v2.empty()) - return; - if (v1.empty()) { - v1.swap(v2); - return; - } - for (T* t : v2) { - if (!v1.contains(t)) - v1.push_back(t); - } - v2.finalize(); - } class evaluator { public: - virtual expr * eval(expr * n, bool model_completion) = 0; + virtual expr* eval(expr* n, bool model_completion) = 0; }; // ----------------------------------- @@ -75,12 +63,12 @@ namespace smt { \brief Instantiation sets are the S_{k,j} sets in the Complete quantifier instantiation paper. */ class instantiation_set { - ast_manager & m; + ast_manager& m; obj_map m_elems; // and the associated generation - obj_map m_inv; + obj_map m_inv; expr_mark m_visited; public: - instantiation_set(ast_manager & m):m(m) {} + instantiation_set(ast_manager& m) :m(m) {} ~instantiation_set() { for (auto const& kv : m_elems) { @@ -89,9 +77,9 @@ namespace smt { m_elems.reset(); } - obj_map const & get_elems() const { return m_elems; } + obj_map const& get_elems() const { return m_elems; } - void insert(expr * n, unsigned generation) { + void insert(expr* n, unsigned generation) { if (m_elems.contains(n) || contains_model_value(n)) { return; } @@ -101,7 +89,7 @@ namespace smt { SASSERT(!m.is_model_value(n)); } - void remove(expr * n) { + void remove(expr* n) { // We can only remove n if it is in m_elems, AND m_inv was not initialized yet. SASSERT(m_elems.contains(n)); SASSERT(m_inv.empty()); @@ -110,7 +98,7 @@ namespace smt { m.dec_ref(n); } - void display(std::ostream & out) const { + void display(std::ostream& out) const { for (auto const& kv : m_elems) { out << mk_bounded_pp(kv.m_key, m) << " [" << kv.m_value << "]\n"; } @@ -120,28 +108,28 @@ namespace smt { } } - expr * get_inv(expr * v) const { - expr * t = nullptr; + expr* get_inv(expr* v) const { + expr* t = nullptr; m_inv.find(v, t); return t; } - unsigned get_generation(expr * t) const { + unsigned get_generation(expr* t) const { unsigned gen = 0; m_elems.find(t, gen); return gen; } - void mk_inverse(evaluator & ev) { + void mk_inverse(evaluator& ev) { for (auto const& kv : m_elems) { - expr * t = kv.m_key; + expr* t = kv.m_key; SASSERT(!contains_model_value(t)); unsigned gen = kv.m_value; - expr * t_val = ev.eval(t, true); + expr* t_val = ev.eval(t, true); if (!t_val) break; TRACE("model_finder", tout << mk_pp(t, m) << " " << mk_pp(t_val, m) << "\n";); - expr * old_t = nullptr; + expr* old_t = nullptr; if (m_inv.find(t_val, old_t)) { unsigned old_t_gen = 0; SASSERT(m_elems.contains(old_t)); @@ -156,12 +144,12 @@ namespace smt { } } - obj_map const & get_inv_map() const { + obj_map const& get_inv_map() const { return m_inv; } struct is_model_value {}; - void operator()(expr *n) { + void operator()(expr* n) { if (m.is_model_value(n)) { throw is_model_value(); } @@ -178,13 +166,14 @@ namespace smt { try { for_each_expr(*this, m_visited, n); } - catch (const is_model_value &) { + catch (const is_model_value&) { return true; } return false; } }; + /** During model construction time, we solve several constraints that impose restrictions @@ -195,58 +184,56 @@ namespace smt { these constraints. */ - // ----------------------------------- - // - // nodes - // - // ----------------------------------- - /** \brief Base class used to solve model construction constraints. */ class node { unsigned m_id; - node * m_find; - unsigned m_eqc_size; + node* m_find{ nullptr }; + unsigned m_eqc_size{ 1 }; - sort * m_sort; // sort of the elements in the instantiation set. + sort* m_sort; // sort of the elements in the instantiation set. - bool m_mono_proj; // relevant for integers & reals & bit-vectors - bool m_signed_proj; // relevant for bit-vectors. + bool m_mono_proj{ false }; // relevant for integers & reals & bit-vectors + bool m_signed_proj{ false }; // relevant for bit-vectors. ptr_vector m_avoid_set; ptr_vector m_exceptions; - instantiation_set * m_set; - - expr * m_else; - func_decl * m_proj; + scoped_ptr m_set; + expr* m_else{ nullptr }; + func_decl* m_proj{ nullptr }; + // Append the new elements of v2 into v1. v2 should not be used after this operation, since it may suffer destructive updates. + template + void dappend(ptr_vector& v1, ptr_vector& v2) { + if (v2.empty()) + return; + if (v1.empty()) { + v1.swap(v2); + return; + } + for (T* t : v2) { + if (!v1.contains(t)) + v1.push_back(t); + } + v2.finalize(); + } public: - node(unsigned id, sort * s): + node(unsigned id, sort* s) : m_id(id), - m_find(nullptr), - m_eqc_size(1), - m_sort(s), - m_mono_proj(false), - m_signed_proj(false), - m_set(nullptr), - m_else(nullptr), - m_proj(nullptr) { + m_sort(s) { } - ~node() { - if (m_set) - dealloc(m_set); - } + ~node() {} unsigned get_id() const { return m_id; } - sort * get_sort() const { return m_sort; } + sort* get_sort() const { return m_sort; } bool is_root() const { return m_find == nullptr; } - node * get_root() const { - node * curr = const_cast(this); + node* get_root() const { + node* curr = const_cast(this); while (!curr->is_root()) { curr = curr->m_find; } @@ -254,34 +241,34 @@ namespace smt { return curr; } - void merge(node * other) { - node * r1 = get_root(); - node * r2 = other->get_root(); - SASSERT(r1->m_set == nullptr); - SASSERT(r2->m_set == nullptr); + void merge(node* other) { + node* r1 = get_root(); + node* r2 = other->get_root(); + SASSERT(!r1->m_set); + SASSERT(!r2->m_set); SASSERT(r1->get_sort() == r2->get_sort()); if (r1 == r2) return; if (r1->m_eqc_size > r2->m_eqc_size) std::swap(r1, r2); - r1->m_find = r2; + r1->m_find = r2; r2->m_eqc_size += r1->m_eqc_size; if (r1->m_mono_proj) r2->m_mono_proj = true; if (r1->m_signed_proj) r2->m_signed_proj = true; - dappend(r2->m_avoid_set, r1->m_avoid_set); + dappend(r2->m_avoid_set, r1->m_avoid_set); dappend(r2->m_exceptions, r1->m_exceptions); } - void insert_avoid(node * n) { - ptr_vector & as = get_root()->m_avoid_set; + void insert_avoid(node* n) { + ptr_vector& as = get_root()->m_avoid_set; if (!as.contains(n)) as.push_back(n); } - void insert_exception(expr * n) { - ptr_vector & ex = get_root()->m_exceptions; + void insert_exception(expr* n) { + ptr_vector& ex = get_root()->m_exceptions; if (!ex.contains(n)) ex.push_back(n); } @@ -302,18 +289,18 @@ namespace smt { return get_root()->m_signed_proj; } - void mk_instantiation_set(ast_manager & m) { + void mk_instantiation_set(ast_manager& m) { SASSERT(is_root()); SASSERT(!m_set); m_set = alloc(instantiation_set, m); } - void insert(expr * n, unsigned generation) { + void insert(expr* n, unsigned generation) { SASSERT(is_ground(n)); get_root()->m_set->insert(n, generation); } - void display(std::ostream & out, ast_manager & m) const { + void display(std::ostream& out, ast_manager& m) const { if (is_root()) { out << "root node ------\n"; out << "@" << m_id << " mono: " << m_mono_proj << " signed: " << m_signed_proj << ", sort: " << mk_pp(m_sort, m) << "\n"; @@ -323,7 +310,7 @@ namespace smt { } out << "\n"; out << "exceptions: "; - for (expr * e : m_exceptions) { + for (expr* e : m_exceptions) { out << mk_bounded_pp(e, m) << " "; } out << "\n"; @@ -342,17 +329,17 @@ namespace smt { } } - instantiation_set const * get_instantiation_set() const { return get_root()->m_set; } + instantiation_set const* get_instantiation_set() const { return get_root()->m_set.get(); } - instantiation_set * get_instantiation_set() { return get_root()->m_set; } + instantiation_set* get_instantiation_set() { return get_root()->m_set.get(); } - ptr_vector const & get_exceptions() const { return get_root()->m_exceptions; } + ptr_vector const& get_exceptions() const { return get_root()->m_exceptions; } - ptr_vector const & get_avoid_set() const { return get_root()->m_avoid_set; } + ptr_vector const& get_avoid_set() const { return get_root()->m_avoid_set; } // return true if m_avoid_set.contains(this) bool must_avoid_itself() const { - node * r = get_root(); + node* r = get_root(); for (node* n : m_avoid_set) { if (r == n->get_root()) return true; @@ -360,29 +347,31 @@ namespace smt { return false; } - void set_else(expr * e) { + void set_else(expr* e) { SASSERT(!is_mono_proj()); SASSERT(get_root()->m_else == nullptr); get_root()->m_else = e; } - expr * get_else() const { + expr* get_else() const { return get_root()->m_else; } - void set_proj(func_decl * f) { + void set_proj(func_decl* f) { SASSERT(get_root()->m_proj == nullptr); get_root()->m_proj = f; } - func_decl * get_proj() const { + func_decl* get_proj() const { return get_root()->m_proj; } }; - typedef std::pair ast_idx_pair; + + typedef std::pair ast_idx_pair; typedef pair_hash, unsigned_hash> ast_idx_pair_hash; - typedef map > key2node; + typedef map > key2node; + /** \brief Auxiliary class for processing the "Almost uninterpreted fragment" described in the paper: @@ -391,31 +380,32 @@ namespace smt { The idea is to create node objects based on the information produced by the quantifier_analyzer. */ class auf_solver : public evaluator { - ast_manager & m; + ast_manager& m; arith_util m_arith; bv_util m_bv; array_util m_array; ptr_vector m_nodes; - unsigned m_next_node_id; + unsigned m_next_node_id{ 0 }; key2node m_uvars; key2node m_A_f_is; - random_gen m_rand; // Mapping from sort to auxiliary constant. // This auxiliary constant is used as a "witness" that is asserted as different from a // finite number of terms. // It is only safe to use this constant for infinite sorts. - obj_map m_sort2k; + obj_map m_sort2k; expr_ref_vector m_ks; // range of m_sort2k // Support for evaluating expressions in the current model. - proto_model * m_model; - obj_map m_eval_cache[2]; + proto_model* m_model{ nullptr }; + obj_map m_eval_cache[2]; expr_ref_vector m_eval_cache_range; ptr_vector m_root_nodes; - expr_ref_vector * m_new_constraints; + expr_ref_vector* m_new_constraints{ nullptr }; + random_gen m_rand; + void reset_sort2k() { m_sort2k.reset(); @@ -428,8 +418,8 @@ namespace smt { m_eval_cache_range.reset(); } - node * mk_node(key2node & map, ast * n, unsigned i, sort * s) { - node * r = nullptr; + node* mk_node(key2node& map, ast* n, unsigned i, sort* s) { + node* r = nullptr; ast_idx_pair k(n, i); if (map.find(k, r)) { SASSERT(r->get_sort() == s); @@ -442,20 +432,20 @@ namespace smt { return r; } - void display_key2node(std::ostream & out, key2node const & m) const { + void display_key2node(std::ostream& out, key2node const& m) const { for (auto const& kv : m) { - ast * a = kv.m_key.first; - unsigned i = kv.m_key.second; - node * n = kv.m_value; + ast* a = kv.m_key.first; + unsigned i = kv.m_key.second; + node* n = kv.m_value; out << "#" << a->get_id() << ":" << i << " -> @" << n->get_id() << "\n"; } } - void display_A_f_is(std::ostream & out) const { + void display_A_f_is(std::ostream& out) const { for (auto const& kv : m_A_f_is) { - func_decl * f = static_cast(kv.m_key.first); - unsigned i = kv.m_key.second; - node * n = kv.m_value; + func_decl* f = static_cast(kv.m_key.first); + unsigned i = kv.m_key.second; + node* n = kv.m_value; out << f->get_name() << ":" << i << " -> @" << n->get_id() << "\n"; } } @@ -465,16 +455,13 @@ namespace smt { } public: - auf_solver(ast_manager & m): + auf_solver(ast_manager& m) : m(m), m_arith(m), m_bv(m), m_array(m), - m_next_node_id(0), m_ks(m), - m_model(nullptr), m_eval_cache_range(m), - m_new_constraints(nullptr), m_rand(static_cast(m.limit().count())) { m.limit().inc(); } @@ -483,9 +470,9 @@ namespace smt { flush_nodes(); reset_eval_cache(); } - - ast_manager & get_manager() const { return m; } - + + ast_manager& get_manager() const { return m; } + void reset() { flush_nodes(); m_nodes.reset(); @@ -496,31 +483,31 @@ namespace smt { reset_sort2k(); } - void set_model(proto_model * m) { + void set_model(proto_model* m) { reset_eval_cache(); m_model = m; } - proto_model * get_model() const { + proto_model* get_model() const { SASSERT(m_model); return m_model; } - node * get_uvar(quantifier * q, unsigned i) { + node* get_uvar(quantifier* q, unsigned i) { SASSERT(i < q->get_num_decls()); - sort * s = q->get_decl_sort(q->get_num_decls() - i - 1); + sort* s = q->get_decl_sort(q->get_num_decls() - i - 1); return mk_node(m_uvars, q, i, s); } - node * get_A_f_i(func_decl * f, unsigned i) { + node* get_A_f_i(func_decl* f, unsigned i) { SASSERT(i < f->get_arity()); - sort * s = f->get_domain(i); + sort* s = f->get_domain(i); return mk_node(m_A_f_is, f, i, s); } - instantiation_set const * get_uvar_inst_set(quantifier * q, unsigned i) const { + instantiation_set const* get_uvar_inst_set(quantifier* q, unsigned i) const { ast_idx_pair k(q, i); - node * r = nullptr; + node* r = nullptr; if (m_uvars.find(k, r)) return r->get_instantiation_set(); return nullptr; @@ -538,14 +525,14 @@ namespace smt { ptr_vector to_delete; void cleanup_instantiation_sets() { - for (node * curr : m_nodes) { + for (node* curr : m_nodes) { if (curr->is_root()) { - instantiation_set * s = curr->get_instantiation_set(); + instantiation_set* s = curr->get_instantiation_set(); to_delete.reset(); - obj_map const & elems = s->get_elems(); + obj_map const& elems = s->get_elems(); for (auto const& kv : elems) { - expr * n = kv.m_key; - expr * n_val = eval(n, true); + expr* n = kv.m_key; + expr* n_val = eval(n, true); if (!n_val || (!m.is_value(n_val) && !m_array.is_array(n_val))) { to_delete.push_back(n); } @@ -557,7 +544,7 @@ namespace smt { } } - void display_nodes(std::ostream & out) const { + void display_nodes(std::ostream& out) const { display_key2node(out, m_uvars); display_A_f_is(out); for (node* n : m_nodes) { @@ -565,8 +552,8 @@ namespace smt { } } - expr * eval(expr * n, bool model_completion) override { - expr * r = nullptr; + expr* eval(expr* n, bool model_completion) override { + expr* r = nullptr; if (m_eval_cache[model_completion].find(n, r)) { return r; } @@ -589,18 +576,18 @@ namespace smt { \brief Collect the interpretations of n->get_exceptions() and the interpretations of the m_else of nodes in n->get_avoid_set() */ - void collect_exceptions_values(node * n, ptr_buffer & r) { + void collect_exceptions_values(node* n, ptr_buffer& r) { for (expr* e : n->get_exceptions()) { - expr * val = eval(e, true); + expr* val = eval(e, true); if (val) r.push_back(val); } for (node* a : n->get_avoid_set()) { - node * p = a->get_root(); + node* p = a->get_root(); if (!p->is_mono_proj() && p->get_else() != nullptr) { - expr * val = eval(p->get_else(), true); + expr* val = eval(p->get_else(), true); if (val) r.push_back(val); } @@ -614,16 +601,16 @@ namespace smt { Return 0 if such t does not exist. */ - expr * pick_instance_diff_exceptions(node * n, ptr_buffer const & ex_vals) { - instantiation_set const * s = n->get_instantiation_set(); - obj_map const & elems = s->get_elems(); + expr* pick_instance_diff_exceptions(node* n, ptr_buffer const& ex_vals) { + instantiation_set const* s = n->get_instantiation_set(); + obj_map const& elems = s->get_elems(); - expr * t_result = nullptr; + expr* t_result = nullptr; unsigned gen_result = UINT_MAX; for (auto const& kv : elems) { - expr * t = kv.m_key; + expr* t = kv.m_key; unsigned gen = kv.m_value; - expr * t_val = eval(t, true); + expr* t_val = eval(t, true); if (!t_val) return t_result; bool found = false; @@ -634,7 +621,7 @@ namespace smt { } } if (!found && (t_result == nullptr || gen < gen_result)) { - t_result = t; + t_result = t; gen_result = gen; } } @@ -642,15 +629,15 @@ namespace smt { } // we should not assume that uninterpreted sorts are infinite in benchmarks with quantifiers. - bool is_infinite(sort * s) const { return !m.is_uninterp(s) && s->is_infinite(); } + bool is_infinite(sort* s) const { return !m.is_uninterp(s) && s->is_infinite(); } /** \brief Return a fresh constant k that is used as a witness for elements that must be different from a set of values. */ - app * get_k_for(sort * s) { + app* get_k_for(sort* s) { SASSERT(is_infinite(s)); - app * r = nullptr; + app* r = nullptr; if (m_sort2k.find(s, r)) return r; r = m.mk_fresh_const("k", s); @@ -668,11 +655,11 @@ namespace smt { Remark: this method uses get_fresh_value, so it may fail. */ - expr * get_k_interp(app * k) { - sort * s = m.get_sort(k); + expr* get_k_interp(app* k) { + sort* s = m.get_sort(k); SASSERT(is_infinite(s)); - func_decl * k_decl = k->get_decl(); - expr * r = m_model->get_const_interp(k_decl); + func_decl* k_decl = k->get_decl(); + expr* r = m_model->get_const_interp(k_decl); if (r != nullptr) return r; r = m_model->get_fresh_value(s); @@ -689,14 +676,14 @@ namespace smt { It invokes get_k_interp that may fail. */ - bool assert_k_diseq_exceptions(app * k, ptr_vector const & exceptions) { + bool assert_k_diseq_exceptions(app* k, ptr_vector const& exceptions) { TRACE("assert_k_diseq_exceptions", tout << "assert_k_diseq_exceptions, " << "k: " << mk_pp(k, m) << "\nexceptions:\n"; - for (expr * e : exceptions) tout << mk_pp(e, m) << "\n";); - expr * k_interp = get_k_interp(k); + for (expr* e : exceptions) tout << mk_pp(e, m) << "\n";); + expr* k_interp = get_k_interp(k); if (k_interp == nullptr) return false; - for (expr * ex : exceptions) { - expr * ex_val = eval(ex, true); + for (expr* ex : exceptions) { + expr* ex_val = eval(ex, true); if (ex_val && !m.are_distinct(k_interp, ex_val)) { SASSERT(m_new_constraints); // This constraint cannot be asserted into m_context during model construction. @@ -707,27 +694,27 @@ namespace smt { return true; } - void set_projection_else(node * n) { + void set_projection_else(node* n) { TRACE("model_finder", n->display(tout, m);); SASSERT(n->is_root()); SASSERT(!n->is_mono_proj()); - instantiation_set const * s = n->get_instantiation_set(); - ptr_vector const & exceptions = n->get_exceptions(); - ptr_vector const & avoid_set = n->get_avoid_set(); - obj_map const & elems = s->get_elems(); + instantiation_set const* s = n->get_instantiation_set(); + ptr_vector const& exceptions = n->get_exceptions(); + ptr_vector const& avoid_set = n->get_avoid_set(); + obj_map const& elems = s->get_elems(); if (elems.empty()) return; if (!exceptions.empty() || !avoid_set.empty()) { ptr_buffer ex_vals; collect_exceptions_values(n, ex_vals); - expr * e = pick_instance_diff_exceptions(n, ex_vals); + expr* e = pick_instance_diff_exceptions(n, ex_vals); if (e != nullptr) { n->set_else(e); return; } - sort * s = n->get_sort(); + sort* s = n->get_sort(); TRACE("model_finder", tout << "trying to create k for " << mk_pp(s, m) << ", is_infinite: " << is_infinite(s) << "\n";); if (is_infinite(s)) { - app * k = get_k_for(s); + app* k = get_k_for(s); if (assert_k_diseq_exceptions(k, exceptions)) { n->insert(k, 0); // add k to the instantiation set n->set_else(k); @@ -736,7 +723,7 @@ namespace smt { } // TBD: add support for the else of bitvectors. // Idea: get the term t with the minimal interpretation and use t - 1. - } + } n->set_else((*(elems.begin())).m_key); } @@ -745,17 +732,17 @@ namespace smt { we must add e-1 and e+1 to the instantiation set. If sort->get_sort() is real, then we do nothing and hope for the best. */ - void add_mono_exceptions(node * n) { + void add_mono_exceptions(node* n) { SASSERT(n->is_mono_proj()); - sort * s = n->get_sort(); + sort* s = n->get_sort(); arith_rewriter arw(m); bv_rewriter brw(m); - ptr_vector const & exceptions = n->get_exceptions(); + ptr_vector const& exceptions = n->get_exceptions(); expr_ref e_minus_1(m), e_plus_1(m); if (m_arith.is_int(s)) { expr_ref one(m_arith.mk_int(1), m); arith_rewriter arith_rw(m); - for (expr * e : exceptions) { + for (expr* e : exceptions) { arith_rw.mk_sub(e, one, e_minus_1); arith_rw.mk_add(e, one, e_plus_1); TRACE("mf_simp_bug", tout << "e:\n" << mk_ismt2_pp(e, m) << "\none:\n" << mk_ismt2_pp(one, m) << "\n";); @@ -767,7 +754,7 @@ namespace smt { else if (m_bv.is_bv_sort(s)) { expr_ref one(m_bv.mk_numeral(rational(1), s), m); bv_rewriter bv_rw(m); - for (expr * e : exceptions) { + for (expr* e : exceptions) { bv_rw.mk_add(e, one, e_plus_1); bv_rw.mk_sub(e, one, e_minus_1); TRACE("mf_simp_bug", tout << "e:\n" << mk_ismt2_pp(e, m) << "\none:\n" << mk_ismt2_pp(one, m) << "\n";); @@ -781,28 +768,28 @@ namespace smt { } } - void get_instantiation_set_values(node * n, ptr_buffer & values) { - instantiation_set const * s = n->get_instantiation_set(); + void get_instantiation_set_values(node* n, ptr_buffer& values) { + instantiation_set const* s = n->get_instantiation_set(); obj_hashtable already_found; - obj_map const & elems = s->get_elems(); + obj_map const& elems = s->get_elems(); for (auto const& kv : elems) { - expr * t = kv.m_key; - expr * t_val = eval(t, true); + expr* t = kv.m_key; + expr* t_val = eval(t, true); if (t_val && !already_found.contains(t_val)) { values.push_back(t_val); already_found.insert(t_val); } } TRACE("model_finder_bug", tout << "values for the instantiation_set of @" << n->get_id() << "\n"; - for (expr * v : values) { - tout << mk_pp(v, m) << "\n"; - }); + for (expr* v : values) { + tout << mk_pp(v, m) << "\n"; + }); } template struct numeral_lt { T& m_util; - numeral_lt(T& a): m_util(a) {} + numeral_lt(T& a) : m_util(a) {} bool operator()(expr* e1, expr* e2) { rational v1, v2; if (m_util.is_numeral(e1, v1) && m_util.is_numeral(e2, v2)) { @@ -818,8 +805,8 @@ namespace smt { struct signed_bv_lt { bv_util& m_bv; unsigned m_bv_size; - signed_bv_lt(bv_util& bv, unsigned sz):m_bv(bv), m_bv_size(sz) {} - bool operator()(expr * e1, expr * e2) { + signed_bv_lt(bv_util& bv, unsigned sz) :m_bv(bv), m_bv_size(sz) {} + bool operator()(expr* e1, expr* e2) { rational v1, v2; if (m_bv.is_numeral(e1, v1) && m_bv.is_numeral(e2, v2)) { v1 = m_bv.norm(v1, m_bv_size, true); @@ -832,8 +819,8 @@ namespace smt { } }; - void sort_values(node * n, ptr_buffer & values) { - sort * s = n->get_sort(); + void sort_values(node* n, ptr_buffer& values) { + sort* s = n->get_sort(); if (m_arith.is_int(s) || m_arith.is_real(s)) { std::sort(values.begin(), values.end(), numeral_lt(m_arith)); } @@ -842,55 +829,55 @@ namespace smt { } else { std::sort(values.begin(), values.end(), signed_bv_lt(m_bv, m_bv.get_bv_size(s))); - } + } } - void mk_mono_proj(node * n) { + void mk_mono_proj(node* n) { add_mono_exceptions(n); ptr_buffer values; get_instantiation_set_values(n, values); if (values.empty()) return; sort_values(n, values); - sort * s = n->get_sort(); - bool is_arith = m_arith.is_int(s) || m_arith.is_real(s); + sort* s = n->get_sort(); + bool is_arith = m_arith.is_int(s) || m_arith.is_real(s); bool is_signed = n->is_signed_proj(); unsigned sz = values.size(); SASSERT(sz > 0); - expr * pi = values[sz - 1]; + expr* pi = values[sz - 1]; expr_ref var(m); var = m.mk_var(0, s); for (unsigned i = sz - 1; i >= 1; i--) { expr_ref c(m); - if (is_arith) + if (is_arith) c = m_arith.mk_lt(var, values[i]); else if (!is_signed) c = m.mk_not(m_bv.mk_ule(values[i], var)); else c = m.mk_not(m_bv.mk_sle(values[i], var)); - pi = m.mk_ite(c, values[i-1], pi); + pi = m.mk_ite(c, values[i - 1], pi); } - func_interp * rpi = alloc(func_interp, m, 1); + func_interp* rpi = alloc(func_interp, m, 1); rpi->set_else(pi); - func_decl * p = m.mk_fresh_func_decl(1, &s, s); + func_decl* p = m.mk_fresh_func_decl(1, &s, s); m_model->register_aux_decl(p, rpi); n->set_proj(p); TRACE("model_finder", n->display(tout << p->get_name() << "\n", m);); } - void mk_simple_proj(node * n) { + void mk_simple_proj(node* n) { set_projection_else(n); ptr_buffer values; get_instantiation_set_values(n, values); - sort * s = n->get_sort(); - func_decl * p = m.mk_fresh_func_decl(1, &s, s); - func_interp * pi = alloc(func_interp, m, 1); + sort* s = n->get_sort(); + func_decl* p = m.mk_fresh_func_decl(1, &s, s); + func_interp* pi = alloc(func_interp, m, 1); m_model->register_aux_decl(p, pi); if (n->get_else()) { - expr * else_val = eval(n->get_else(), true); - if (else_val) + expr* else_val = eval(n->get_else(), true); + if (else_val) pi->set_else(else_val); - } - for (expr * v : values) { + } + for (expr* v : values) { pi->insert_new_entry(&v, v); } n->set_proj(p); @@ -898,7 +885,7 @@ namespace smt { } void mk_projections() { - for (node * n : m_root_nodes) { + for (node* n : m_root_nodes) { SASSERT(n->is_root()); if (n->is_mono_proj()) mk_mono_proj(n); @@ -910,11 +897,11 @@ namespace smt { /** \brief Store in r the partial functions that have A_f_i nodes. */ - void collect_partial_funcs(func_decl_set & r) { + void collect_partial_funcs(func_decl_set& r) { for (auto const& kv : m_A_f_is) { - func_decl * f = to_func_decl(kv.m_key.first); + func_decl* f = to_func_decl(kv.m_key.first); if (!r.contains(f)) { - func_interp * fi = m_model->get_func_interp(f); + func_interp* fi = m_model->get_func_interp(f); if (fi == nullptr) { fi = alloc(func_interp, m, f->get_arity()); TRACE("model_finder", tout << "register " << f->get_name() << "\n";); @@ -936,10 +923,10 @@ namespace smt { for more details. */ void mk_sorts_finite() { - for (node * n : m_root_nodes) { + for (node* n : m_root_nodes) { SASSERT(n->is_root()); - sort * s = n->get_sort(); - if (m.is_uninterp(s) && + sort* s = n->get_sort(); + if (m.is_uninterp(s) && // Making all uninterpreted sorts finite. // n->must_avoid_itself() && !m_model->is_finite(s)) { @@ -951,18 +938,18 @@ namespace smt { void add_elem_to_empty_inst_sets() { obj_map sort2elems; ptr_vector need_fresh; - for (node * n : m_root_nodes) { + for (node* n : m_root_nodes) { SASSERT(n->is_root()); - instantiation_set const * s = n->get_instantiation_set(); + instantiation_set const* s = n->get_instantiation_set(); TRACE("model_finder", s->display(tout);); - obj_map const & elems = s->get_elems(); + obj_map const& elems = s->get_elems(); if (elems.empty()) { // The method get_some_value cannot be used if n->get_sort() is an uninterpreted sort or is a sort built using uninterpreted sorts // (e.g., (Array S S) where S is uninterpreted). The problem is that these sorts do not have a fixed interpretation. // Moreover, a model assigns an arbitrary interpretation to these sorts using "model_values" a model value. // If these module values "leak" inside the logical context, they may affect satisfiability. // - sort * ns = n->get_sort(); + sort* ns = n->get_sort(); if (m.is_fully_interp(ns)) { n->insert(m_model->get_some_value(ns), 0); } @@ -975,8 +962,8 @@ namespace smt { } } expr_ref_vector trail(m); - for (node * n : need_fresh) { - expr * e; + for (node* n : need_fresh) { + expr* e; sort* s = n->get_sort(); if (!sort2elems.find(s, e)) { e = m.mk_fresh_const("elem", s); @@ -993,7 +980,7 @@ namespace smt { */ void collect_root_nodes() { m_root_nodes.reset(); - for (node * n : m_nodes) { + for (node* n : m_nodes) { if (n->is_root()) m_root_nodes.push_back(n); } @@ -1015,8 +1002,8 @@ namespace smt { This is ok, because in the "limit" the "else" of the interpretation is irrelevant after the projections are applied. */ - func_decl * get_f_i_proj(func_decl * f, unsigned i) { - node * r = nullptr; + func_decl* get_f_i_proj(func_decl* f, unsigned i) { + node* r = nullptr; ast_idx_pair k(f, i); if (!m_A_f_is.find(k, r)) return nullptr; @@ -1027,21 +1014,21 @@ namespace smt { \brief Complete the interpretation of the functions that were collected in the beginning of fix_model(). */ - void complete_partial_funcs(func_decl_set const & partial_funcs) { - for (func_decl * f : partial_funcs) { + void complete_partial_funcs(func_decl_set const& partial_funcs) { + for (func_decl* f : partial_funcs) { // Complete the current interpretation m_model->complete_partial_func(f, true); - unsigned arity = f->get_arity(); - func_interp * fi = m_model->get_func_interp(f); + unsigned arity = f->get_arity(); + func_interp* fi = m_model->get_func_interp(f); if (fi->is_constant()) continue; // there is no point in using the projection for fi, since fi is the constant function. - + expr_ref_vector args(m); bool has_proj = false; for (unsigned i = 0; i < arity; i++) { - var * v = m.mk_var(i, f->get_domain(i)); - func_decl * pi = get_f_i_proj(f, i); + var* v = m.mk_var(i, f->get_domain(i)); + func_decl* pi = get_f_i_proj(f, i); if (pi != nullptr) { args.push_back(m.mk_app(pi, v)); has_proj = true; @@ -1052,20 +1039,20 @@ namespace smt { } if (has_proj) { // f_aux will be assigned to the old interpretation of f. - func_decl * f_aux = m.mk_fresh_func_decl(f->get_name(), symbol::null, arity, f->get_domain(), f->get_range()); - func_interp * new_fi = alloc(func_interp, m, arity); + func_decl* f_aux = m.mk_fresh_func_decl(f->get_name(), symbol::null, arity, f->get_domain(), f->get_range()); + func_interp* new_fi = alloc(func_interp, m, arity); new_fi->set_else(m.mk_app(f_aux, args.size(), args.c_ptr())); - TRACE("model_finder", tout << "Setting new interpretation for " << f->get_name() << "\n" << - mk_pp(new_fi->get_else(), m) << "\n"; - tout << "old interpretation: " << mk_pp(fi->get_interp(), m) << "\n";); + TRACE("model_finder", tout << "Setting new interpretation for " << f->get_name() << "\n" << + mk_pp(new_fi->get_else(), m) << "\n"; + tout << "old interpretation: " << mk_pp(fi->get_interp(), m) << "\n";); m_model->reregister_decl(f, new_fi, f_aux); } } } - void mk_inverse(node * n) { + void mk_inverse(node* n) { SASSERT(n->is_root()); - instantiation_set * s = n->get_instantiation_set(); + instantiation_set* s = n->get_instantiation_set(); s->mk_inverse(*this); } @@ -1079,7 +1066,7 @@ namespace smt { } public: - void fix_model(expr_ref_vector & new_constraints) { + void fix_model(expr_ref_vector& new_constraints) { cleanup_instantiation_sets(); m_new_constraints = &new_constraints; func_decl_set partial_funcs; @@ -1092,9 +1079,9 @@ namespace smt { mk_inverses(); complete_partial_funcs(partial_funcs); TRACE("model_finder", tout << "after auf_solver fixing the model\n"; - display_nodes(tout); - tout << "NEW MODEL:\n"; - model_pp(tout, *m_model);); + display_nodes(tout); + tout << "NEW MODEL:\n"; + model_pp(tout, *m_model);); } }; @@ -1121,66 +1108,66 @@ namespace smt { public: qinfo(ast_manager& m) :m(m) {} virtual ~qinfo() {} - virtual char const * get_kind() const = 0; - virtual bool is_equal(qinfo const * qi) const = 0; - virtual void display(std::ostream & out) const { out << "[" << get_kind() << "]"; } + virtual char const* get_kind() const = 0; + virtual bool is_equal(qinfo const* qi) const = 0; + virtual void display(std::ostream& out) const { out << "[" << get_kind() << "]"; } // AUF fragment solver - virtual void process_auf(quantifier * q, auf_solver & s, context * ctx) = 0; - virtual void populate_inst_sets(quantifier * q, auf_solver & s, context * ctx) = 0; + virtual void process_auf(quantifier* q, auf_solver& s, context* ctx) = 0; + virtual void populate_inst_sets(quantifier* q, auf_solver& s, context* ctx) = 0; // second pass... actually we may need to reach a fixpoint, but if it cannot be found // in two passes, the fixpoint is not finite. - virtual void populate_inst_sets2(quantifier * q, auf_solver & s, context * ctx) {} + virtual void populate_inst_sets2(quantifier* q, auf_solver& s, context* ctx) {} // Macro/Hint support - virtual void populate_inst_sets(quantifier * q, func_decl * mhead, ptr_vector & uvar_inst_sets, context * ctx) {} + virtual void populate_inst_sets(quantifier* q, func_decl* mhead, ptr_vector& uvar_inst_sets, context* ctx) {} }; class f_var : public qinfo { protected: - func_decl * m_f; + func_decl* m_f; unsigned m_arg_i; unsigned m_var_j; public: - f_var(ast_manager& m, func_decl * f, unsigned i, unsigned j): qinfo(m), m_f(f), m_arg_i(i), m_var_j(j) {} + f_var(ast_manager& m, func_decl* f, unsigned i, unsigned j) : qinfo(m), m_f(f), m_arg_i(i), m_var_j(j) {} ~f_var() override {} - char const * get_kind() const override { + char const* get_kind() const override { return "f_var"; } - bool is_equal(qinfo const * qi) const override { + bool is_equal(qinfo const* qi) const override { if (qi->get_kind() != get_kind()) return false; - f_var const * other = static_cast(qi); + f_var const* other = static_cast(qi); return m_f == other->m_f && m_arg_i == other->m_arg_i && m_var_j == other->m_var_j; } - void display(std::ostream & out) const override { + void display(std::ostream& out) const override { out << "(" << m_f->get_name() << ":" << m_arg_i << " -> v!" << m_var_j << ")"; } - void process_auf(quantifier * q, auf_solver & s, context * ctx) override { - node * n1 = s.get_A_f_i(m_f, m_arg_i); - node * n2 = s.get_uvar(q, m_var_j); + void process_auf(quantifier* q, auf_solver& s, context* ctx) override { + node* n1 = s.get_A_f_i(m_f, m_arg_i); + node* n2 = s.get_uvar(q, m_var_j); CTRACE("model_finder", n1->get_sort() != n2->get_sort(), - tout << "sort bug:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" << mk_ismt2_pp(q, m) << "\n"; - tout << "decl(0): " << q->get_decl_name(0) << "\n"; - tout << "f: " << m_f->get_name() << " i: " << m_arg_i << "\n"; - tout << "v: " << m_var_j << "\n"; - n1->get_root()->display(tout, m); - n2->get_root()->display(tout, m); - tout << "f signature: "; - for (unsigned i = 0; i < m_f->get_arity(); i++) tout << mk_pp(m_f->get_domain(i), m) << " "; - tout << "-> " << mk_pp(m_f->get_range(), m) << "\n"; - ); + tout << "sort bug:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" << mk_ismt2_pp(q, m) << "\n"; + tout << "decl(0): " << q->get_decl_name(0) << "\n"; + tout << "f: " << m_f->get_name() << " i: " << m_arg_i << "\n"; + tout << "v: " << m_var_j << "\n"; + n1->get_root()->display(tout, m); + n2->get_root()->display(tout, m); + tout << "f signature: "; + for (unsigned i = 0; i < m_f->get_arity(); i++) tout << mk_pp(m_f->get_domain(i), m) << " "; + tout << "-> " << mk_pp(m_f->get_range(), m) << "\n"; + ); n1->merge(n2); } - void populate_inst_sets(quantifier * q, auf_solver & s, context * ctx) override { - node * A_f_i = s.get_A_f_i(m_f, m_arg_i); - for (enode * n : ctx->enodes_of(m_f)) { + void populate_inst_sets(quantifier* q, auf_solver& s, context* ctx) override { + node* A_f_i = s.get_A_f_i(m_f, m_arg_i); + for (enode* n : ctx->enodes_of(m_f)) { if (ctx->is_relevant(n)) { // Remark: it is incorrect to use // n->get_arg(m_arg_i)->get_root() @@ -1191,26 +1178,26 @@ namespace smt { // classes are merged by accident. // So, using n->get_arg(m_arg_i)->get_root(), we may miss // a necessary instantiation. - enode * e_arg = n->get_arg(m_arg_i); - expr * arg = e_arg->get_owner(); + enode* e_arg = n->get_arg(m_arg_i); + expr* arg = e_arg->get_owner(); A_f_i->insert(arg, e_arg->get_generation()); } } } - void populate_inst_sets(quantifier * q, func_decl * mhead, ptr_vector & uvar_inst_sets, context * ctx) override { + void populate_inst_sets(quantifier* q, func_decl* mhead, ptr_vector& uvar_inst_sets, context* ctx) override { if (m_f != mhead) return; - uvar_inst_sets.reserve(m_var_j+1, 0); + uvar_inst_sets.reserve(m_var_j + 1, 0); if (uvar_inst_sets[m_var_j] == 0) uvar_inst_sets[m_var_j] = alloc(instantiation_set, ctx->get_manager()); - instantiation_set * s = uvar_inst_sets[m_var_j]; + instantiation_set* s = uvar_inst_sets[m_var_j]; SASSERT(s != nullptr); - for (enode * n : ctx->enodes_of(m_f)) { + for (enode* n : ctx->enodes_of(m_f)) { if (ctx->is_relevant(n)) { - enode * e_arg = n->get_arg(m_arg_i); - expr * arg = e_arg->get_owner(); + enode* e_arg = n->get_arg(m_arg_i); + expr* arg = e_arg->get_owner(); s->insert(arg, e_arg->get_generation()); } } @@ -1220,51 +1207,51 @@ namespace smt { class f_var_plus_offset : public f_var { expr_ref m_offset; public: - f_var_plus_offset(ast_manager & m, func_decl * f, unsigned i, unsigned j, expr * offset): + f_var_plus_offset(ast_manager& m, func_decl* f, unsigned i, unsigned j, expr* offset) : f_var(m, f, i, j), m_offset(offset, m) { } ~f_var_plus_offset() override {} - char const * get_kind() const override { + char const* get_kind() const override { return "f_var_plus_offset"; } - bool is_equal(qinfo const * qi) const override { + bool is_equal(qinfo const* qi) const override { if (qi->get_kind() != get_kind()) return false; - f_var_plus_offset const * other = static_cast(qi); + f_var_plus_offset const* other = static_cast(qi); return m_f == other->m_f && m_arg_i == other->m_arg_i && m_var_j == other->m_var_j && m_offset.get() == other->m_offset.get(); } - void display(std::ostream & out) const override { + void display(std::ostream& out) const override { out << "(" << m_f->get_name() << ":" << m_arg_i << " - " << mk_bounded_pp(m_offset.get(), m_offset.get_manager()) << " -> v!" << m_var_j << ")"; } - void process_auf(quantifier * q, auf_solver & s, context * ctx) override { + void process_auf(quantifier* q, auf_solver& s, context* ctx) override { // just create the nodes /* node * A_f_i = */ s.get_A_f_i(m_f, m_arg_i); /* node * S_j = */ s.get_uvar(q, m_var_j); } - void populate_inst_sets(quantifier * q, auf_solver & s, context * ctx) override { + void populate_inst_sets(quantifier* q, auf_solver& s, context* ctx) override { // S_j is not necessary equal to A_f_i. - node * A_f_i = s.get_A_f_i(m_f, m_arg_i)->get_root(); - node * S_j = s.get_uvar(q, m_var_j)->get_root(); + node* A_f_i = s.get_A_f_i(m_f, m_arg_i)->get_root(); + node* S_j = s.get_uvar(q, m_var_j)->get_root(); if (A_f_i == S_j) { // there is no finite fixpoint... we just copy the i-th arguments of A_f_i - m_offset // hope for the best... - node * S_j = s.get_uvar(q, m_var_j); - for (enode * n : ctx->enodes_of(m_f)) { + node* S_j = s.get_uvar(q, m_var_j); + for (enode* n : ctx->enodes_of(m_f)) { if (ctx->is_relevant(n)) { arith_rewriter arith_rw(m); bv_util bv(m); bv_rewriter bv_rw(m); - enode * e_arg = n->get_arg(m_arg_i); - expr * arg = e_arg->get_owner(); + enode* e_arg = n->get_arg(m_arg_i); + expr* arg = e_arg->get_owner(); expr_ref arg_minus_k(m); - if (bv.is_bv(arg)) + if (bv.is_bv(arg)) bv_rw.mk_sub(arg, m_offset, arg_minus_k); else arith_rw.mk_sub(arg, m_offset, arg_minus_k); @@ -1286,16 +1273,16 @@ namespace smt { } template - void copy_instances(node * from, node * to, auf_solver & s) { - instantiation_set const * from_s = from->get_instantiation_set(); - obj_map const & elems_s = from_s->get_elems(); + void copy_instances(node* from, node* to, auf_solver& s) { + instantiation_set const* from_s = from->get_instantiation_set(); + obj_map const& elems_s = from_s->get_elems(); arith_rewriter arith_rw(m_offset.get_manager()); bv_rewriter bv_rw(m_offset.get_manager()); bool is_bv = bv_util(m_offset.get_manager()).is_bv_sort(from->get_sort()); for (auto const& kv : elems_s) { - expr * n = kv.m_key; + expr* n = kv.m_key; expr_ref n_k(m_offset.get_manager()); if (PLUS) { if (is_bv) { @@ -1317,9 +1304,9 @@ namespace smt { } } - void populate_inst_sets2(quantifier * q, auf_solver & s, context * ctx) override { - node * A_f_i = s.get_A_f_i(m_f, m_arg_i)->get_root(); - node * S_j = s.get_uvar(q, m_var_j)->get_root(); + void populate_inst_sets2(quantifier* q, auf_solver& s, context* ctx) override { + node* A_f_i = s.get_A_f_i(m_f, m_arg_i)->get_root(); + node* S_j = s.get_uvar(q, m_var_j)->get_root(); // If A_f_i == S_j, then there is no finite fixpoint, so we do nothing here. if (A_f_i != S_j) { // enforce @@ -1330,7 +1317,7 @@ namespace smt { } } - void populate_inst_sets(quantifier * q, func_decl * mhead, ptr_vector & uvar_inst_sets, context * ctx) override { + void populate_inst_sets(quantifier* q, func_decl* mhead, ptr_vector& uvar_inst_sets, context* ctx) override { // ignored when in macro } @@ -1345,24 +1332,24 @@ namespace smt { Store in arrays, all enodes that match the pattern */ - void get_auf_arrays(app * auf_arr, context * ctx, ptr_buffer & arrays) { + void get_auf_arrays(app* auf_arr, context* ctx, ptr_buffer& arrays) { if (is_ground(auf_arr)) { if (ctx->e_internalized(auf_arr)) { - enode * e = ctx->get_enode(auf_arr); + enode* e = ctx->get_enode(auf_arr); if (ctx->is_relevant(e)) { arrays.push_back(e); } } } else { - app * nested_array = to_app(auf_arr->get_arg(0)); + app* nested_array = to_app(auf_arr->get_arg(0)); ptr_buffer nested_arrays; get_auf_arrays(nested_array, ctx, nested_arrays); - for (enode * curr : nested_arrays) { - enode_vector::iterator it2 = curr->begin_parents(); + for (enode* curr : nested_arrays) { + enode_vector::iterator it2 = curr->begin_parents(); enode_vector::iterator end2 = curr->end_parents(); for (; it2 != end2; ++it2) { - enode * p = *it2; + enode* p = *it2; if (ctx->is_relevant(p) && p->get_owner()->get_decl() == auf_arr->get_decl()) { arrays.push_back(p); } @@ -1374,74 +1361,74 @@ namespace smt { class select_var : public qinfo { protected: array_util m_array; - app * m_select; // It must satisfy is_auf_select... see bool is_auf_select(expr * t) const + app* m_select; // It must satisfy is_auf_select... see bool is_auf_select(expr * t) const unsigned m_arg_i; unsigned m_var_j; - app * get_array() const { return to_app(m_select->get_arg(0)); } + app* get_array() const { return to_app(m_select->get_arg(0)); } - func_decl * get_array_func_decl(app * ground_array, auf_solver & s) { + func_decl* get_array_func_decl(app* ground_array, auf_solver& s) { TRACE("model_evaluator", tout << expr_ref(ground_array, m) << "\n";); - expr * ground_array_interp = s.eval(ground_array, false); + expr* ground_array_interp = s.eval(ground_array, false); if (ground_array_interp && m_array.is_as_array(ground_array_interp)) return m_array.get_as_array_func_decl(ground_array_interp); return nullptr; } public: - select_var(ast_manager & m, app * s, unsigned i, unsigned j):qinfo(m), m_array(m), m_select(s), m_arg_i(i), m_var_j(j) {} + select_var(ast_manager& m, app* s, unsigned i, unsigned j) :qinfo(m), m_array(m), m_select(s), m_arg_i(i), m_var_j(j) {} ~select_var() override {} - char const * get_kind() const override { + char const* get_kind() const override { return "select_var"; } - bool is_equal(qinfo const * qi) const override { + bool is_equal(qinfo const* qi) const override { if (qi->get_kind() != get_kind()) return false; - select_var const * other = static_cast(qi); + select_var const* other = static_cast(qi); return m_select == other->m_select && m_arg_i == other->m_arg_i && m_var_j == other->m_var_j; } - void display(std::ostream & out) const override { + void display(std::ostream& out) const override { out << "(" << mk_bounded_pp(m_select, m) << ":" << m_arg_i << " -> v!" << m_var_j << ")"; } - void process_auf(quantifier * q, auf_solver & s, context * ctx) override { + void process_auf(quantifier* q, auf_solver& s, context* ctx) override { ptr_buffer arrays; get_auf_arrays(get_array(), ctx, arrays); TRACE("select_var", - tout << "enodes matching: "; display(tout); tout << "\n"; - for (enode* n : arrays) { - tout << "#" << n->get_owner()->get_id() << "\n" << mk_pp(n->get_owner(), m) << "\n"; - }); - node * n1 = s.get_uvar(q, m_var_j); + tout << "enodes matching: "; display(tout); tout << "\n"; for (enode* n : arrays) { - app * ground_array = n->get_owner(); - func_decl * f = get_array_func_decl(ground_array, s); + tout << "#" << n->get_owner()->get_id() << "\n" << mk_pp(n->get_owner(), m) << "\n"; + }); + node* n1 = s.get_uvar(q, m_var_j); + for (enode* n : arrays) { + app* ground_array = n->get_owner(); + func_decl* f = get_array_func_decl(ground_array, s); if (f) { SASSERT(m_arg_i >= 1); - node * n2 = s.get_A_f_i(f, m_arg_i - 1); + node* n2 = s.get_A_f_i(f, m_arg_i - 1); n1->merge(n2); } } } - void populate_inst_sets(quantifier * q, auf_solver & s, context * ctx) override { + void populate_inst_sets(quantifier* q, auf_solver& s, context* ctx) override { ptr_buffer arrays; get_auf_arrays(get_array(), ctx, arrays); - for (enode * curr : arrays) { - app * ground_array = curr->get_owner(); - func_decl * f = get_array_func_decl(ground_array, s); + for (enode* curr : arrays) { + app* ground_array = curr->get_owner(); + func_decl* f = get_array_func_decl(ground_array, s); if (f) { - node * A_f_i = s.get_A_f_i(f, m_arg_i - 1); - enode_vector::iterator it2 = curr->begin_parents(); + node* A_f_i = s.get_A_f_i(f, m_arg_i - 1); + enode_vector::iterator it2 = curr->begin_parents(); enode_vector::iterator end2 = curr->end_parents(); for (; it2 != end2; ++it2) { - enode * p = *it2; + enode* p = *it2; if (ctx->is_relevant(p) && p->get_owner()->get_decl() == m_select->get_decl()) { SASSERT(m_arg_i < p->get_owner()->get_num_args()); - enode * e_arg = p->get_arg(m_arg_i); + enode* e_arg = p->get_arg(m_arg_i); A_f_i->insert(e_arg->get_owner(), e_arg->get_generation()); } } @@ -1455,37 +1442,37 @@ namespace smt { unsigned m_var_i; unsigned m_var_j; public: - var_pair(ast_manager& m, unsigned i, unsigned j): qinfo(m), m_var_i(i), m_var_j(j) { + var_pair(ast_manager& m, unsigned i, unsigned j) : qinfo(m), m_var_i(i), m_var_j(j) { if (m_var_i > m_var_j) std::swap(m_var_i, m_var_j); } ~var_pair() override {} - bool is_equal(qinfo const * qi) const override { + bool is_equal(qinfo const* qi) const override { if (qi->get_kind() != get_kind()) return false; - var_pair const * other = static_cast(qi); + var_pair const* other = static_cast(qi); return m_var_i == other->m_var_i && m_var_j == other->m_var_j; } - void display(std::ostream & out) const override { + void display(std::ostream& out) const override { out << "(" << get_kind() << ":v!" << m_var_i << ":v!" << m_var_j << ")"; } - void populate_inst_sets(quantifier * q, auf_solver & s, context * ctx) override { + void populate_inst_sets(quantifier* q, auf_solver& s, context* ctx) override { // do nothing } }; class x_eq_y : public var_pair { public: - x_eq_y(ast_manager& m, unsigned i, unsigned j):var_pair(m, i, j) {} - char const * get_kind() const override { return "x_eq_y"; } + x_eq_y(ast_manager& m, unsigned i, unsigned j) :var_pair(m, i, j) {} + char const* get_kind() const override { return "x_eq_y"; } - void process_auf(quantifier * q, auf_solver & s, context * ctx) override { - node * n1 = s.get_uvar(q, m_var_i); - node * n2 = s.get_uvar(q, m_var_j); + void process_auf(quantifier* q, auf_solver& s, context* ctx) override { + node* n1 = s.get_uvar(q, m_var_i); + node* n2 = s.get_uvar(q, m_var_j); n1->insert_avoid(n2); if (n1 != n2) n2->insert_avoid(n1); @@ -1494,24 +1481,24 @@ namespace smt { class x_neq_y : public var_pair { public: - x_neq_y(ast_manager& m, unsigned i, unsigned j):var_pair(m, i, j) {} - char const * get_kind() const override { return "x_neq_y"; } + x_neq_y(ast_manager& m, unsigned i, unsigned j) :var_pair(m, i, j) {} + char const* get_kind() const override { return "x_neq_y"; } - void process_auf(quantifier * q, auf_solver & s, context * ctx) override { - node * n1 = s.get_uvar(q, m_var_i); - node * n2 = s.get_uvar(q, m_var_j); + void process_auf(quantifier* q, auf_solver& s, context* ctx) override { + node* n1 = s.get_uvar(q, m_var_i); + node* n2 = s.get_uvar(q, m_var_j); n1->merge(n2); } }; class x_leq_y : public var_pair { public: - x_leq_y(ast_manager& m, unsigned i, unsigned j):var_pair(m, i, j) {} - char const * get_kind() const override { return "x_leq_y"; } + x_leq_y(ast_manager& m, unsigned i, unsigned j) :var_pair(m, i, j) {} + char const* get_kind() const override { return "x_leq_y"; } - void process_auf(quantifier * q, auf_solver & s, context * ctx) override { - node * n1 = s.get_uvar(q, m_var_i); - node * n2 = s.get_uvar(q, m_var_j); + void process_auf(quantifier* q, auf_solver& s, context* ctx) override { + node* n1 = s.get_uvar(q, m_var_i); + node* n2 = s.get_uvar(q, m_var_j); n1->merge(n2); n1->set_mono_proj(); } @@ -1520,12 +1507,12 @@ namespace smt { // signed bit-vector comparison class x_sleq_y : public x_leq_y { public: - x_sleq_y(ast_manager& m, unsigned i, unsigned j):x_leq_y(m, i, j) {} - char const * get_kind() const override { return "x_sleq_y"; } + x_sleq_y(ast_manager& m, unsigned i, unsigned j) :x_leq_y(m, i, j) {} + char const* get_kind() const override { return "x_sleq_y"; } - void process_auf(quantifier * q, auf_solver & s, context * ctx) override { - node * n1 = s.get_uvar(q, m_var_i); - node * n2 = s.get_uvar(q, m_var_j); + void process_auf(quantifier* q, auf_solver& s, context* ctx) override { + node* n1 = s.get_uvar(q, m_var_i); + node* n2 = s.get_uvar(q, m_var_j); n1->merge(n2); n1->set_mono_proj(); n1->set_signed_proj(); @@ -1537,42 +1524,42 @@ namespace smt { unsigned m_var_i; expr_ref m_t; public: - var_expr_pair(ast_manager & m, unsigned i, expr * t): + var_expr_pair(ast_manager& m, unsigned i, expr* t) : qinfo(m), m_var_i(i), m_t(t, m) {} ~var_expr_pair() override {} - bool is_equal(qinfo const * qi) const override { + bool is_equal(qinfo const* qi) const override { if (qi->get_kind() != get_kind()) return false; - var_expr_pair const * other = static_cast(qi); + var_expr_pair const* other = static_cast(qi); return m_var_i == other->m_var_i && m_t.get() == other->m_t.get(); } - void display(std::ostream & out) const override { + void display(std::ostream& out) const override { out << "(" << get_kind() << ":v!" << m_var_i << ":" << mk_bounded_pp(m_t.get(), m) << ")"; } }; class x_eq_t : public var_expr_pair { public: - x_eq_t(ast_manager & m, unsigned i, expr * t): + x_eq_t(ast_manager& m, unsigned i, expr* t) : var_expr_pair(m, i, t) {} - char const * get_kind() const override { return "x_eq_t"; } + char const* get_kind() const override { return "x_eq_t"; } - void process_auf(quantifier * q, auf_solver & s, context * ctx) override { - node * n1 = s.get_uvar(q, m_var_i); + void process_auf(quantifier* q, auf_solver& s, context* ctx) override { + node* n1 = s.get_uvar(q, m_var_i); n1->insert_exception(m_t); } - void populate_inst_sets(quantifier * q, auf_solver & slv, context * ctx) override { + void populate_inst_sets(quantifier* q, auf_solver& slv, context* ctx) override { unsigned num_vars = q->get_num_decls(); - sort * s = q->get_decl_sort(num_vars - m_var_i - 1); + sort* s = q->get_decl_sort(num_vars - m_var_i - 1); if (m.is_uninterp(s)) { // For uninterpreted sorts, we add all terms in the context. // See Section 4.1 in the paper "Complete Quantifier Instantiation" - node * S_q_i = slv.get_uvar(q, m_var_i); - for (enode * n : ctx->enodes()) { + node* S_q_i = slv.get_uvar(q, m_var_i); + for (enode* n : ctx->enodes()) { if (ctx->is_relevant(n) && get_sort(n->get_owner()) == s) { S_q_i->insert(n->get_owner(), n->get_generation()); } @@ -1583,96 +1570,39 @@ namespace smt { class x_neq_t : public var_expr_pair { public: - x_neq_t(ast_manager & m, unsigned i, expr * t): + x_neq_t(ast_manager& m, unsigned i, expr* t) : var_expr_pair(m, i, t) {} - char const * get_kind() const override { return "x_neq_t"; } + char const* get_kind() const override { return "x_neq_t"; } - void process_auf(quantifier * q, auf_solver & s, context * ctx) override { + void process_auf(quantifier* q, auf_solver& s, context* ctx) override { // make sure that S_q_i is create. s.get_uvar(q, m_var_i); } - void populate_inst_sets(quantifier * q, auf_solver & s, context * ctx) override { - node * S_q_i = s.get_uvar(q, m_var_i); + void populate_inst_sets(quantifier* q, auf_solver& s, context* ctx) override { + node* S_q_i = s.get_uvar(q, m_var_i); S_q_i->insert(m_t, 0); } }; class x_gle_t : public var_expr_pair { public: - x_gle_t(ast_manager & m, unsigned i, expr * t): + x_gle_t(ast_manager& m, unsigned i, expr* t) : var_expr_pair(m, i, t) {} - char const * get_kind() const override { return "x_gle_t"; } + char const* get_kind() const override { return "x_gle_t"; } - void process_auf(quantifier * q, auf_solver & s, context * ctx) override { + void process_auf(quantifier* q, auf_solver& s, context* ctx) override { // make sure that S_q_i is create. - node * n1 = s.get_uvar(q, m_var_i); + node* n1 = s.get_uvar(q, m_var_i); n1->set_mono_proj(); } - void populate_inst_sets(quantifier * q, auf_solver & s, context * ctx) override { - node * S_q_i = s.get_uvar(q, m_var_i); + void populate_inst_sets(quantifier* q, auf_solver& s, context* ctx) override { + node* S_q_i = s.get_uvar(q, m_var_i); S_q_i->insert(m_t, 0); } }; - class cond_macro { - protected: - ast_manager & m; - func_decl * m_f; - expr * m_def; - expr * m_cond; - bool m_ineq; - bool m_satisfy_atom; - bool m_hint; - unsigned m_weight; - public: - cond_macro(ast_manager & m, func_decl * f, expr * def, expr * cond, bool ineq, bool satisfy_atom, bool hint, unsigned weight): - m(m), - m_f(f), - m_def(def), - m_cond(cond), - m_ineq(ineq), - m_satisfy_atom(satisfy_atom), - m_hint(hint), - m_weight(weight) { - m.inc_ref(m_def); - m.inc_ref(m_cond); - SASSERT(!m_hint || m_cond == 0); - } - - ~cond_macro() { - m.dec_ref(m_def); - m.dec_ref(m_cond); - } - - func_decl * get_f() const { return m_f; } - - expr * get_def() const { return m_def; } - - expr * get_cond() const { return m_cond; } - - bool is_unconditional() const { return m_cond == nullptr || m.is_true(m_cond); } - - bool satisfy_atom() const { return m_satisfy_atom; } - - bool is_hint() const { return m_hint; } - - bool is_equal(cond_macro const * other) const { - return m_f == other->m_f && m_def == other->m_def && m_cond == other->m_cond; - } - - void display(std::ostream & out) const { - out << "[" << m_f->get_name() << " -> " << mk_bounded_pp(m_def, m, 6); - if (m_hint) - out << " *hint*"; - else - out << " when " << mk_bounded_pp(m_cond, m, 6); - out << "] weight: " << m_weight; - } - - unsigned get_weight() const { return m_weight; } - }; // ----------------------------------- // @@ -1688,19 +1618,12 @@ namespace smt { The information is used to (try to) build a model that satisfy the universal quantifier (when it is marked as relevant in the end of the search). */ - class quantifier_info { - model_finder& m_mf; + class quantifier_info : public quantifier_macro_info { + model_finder& m_mf; quantifier_ref m_q; // original quantifier - quantifier_ref m_flat_q; // flat version of the quantifier - bool m_is_auf; - bool m_has_x_eq_y; + ptr_vector m_qinfo_vect; - func_decl_set m_ng_decls; // declarations used in non-ground applications (basic_family operators are ignored here). - ptr_vector m_cond_macros; - func_decl * m_the_one; // the macro head used to satisfy the quantifier. this is useful for model checking - // when the quantifier is satisfied by a macro/hint, it may not be processed by the AUF solver. - // in this case, the quantifier_info stores the instantiation sets. - ptr_vector * m_uvar_inst_sets; + ptr_vector* m_uvar_inst_sets; friend class quantifier_analyzer; @@ -1708,7 +1631,7 @@ namespace smt { m_mf.checkpoint("quantifier_info"); } - void insert_qinfo(qinfo * qi) { + void insert_qinfo(qinfo* qi) { // I'm assuming the number of qinfo's per quantifier is small. So, the linear search is not a big deal. scoped_ptr q(qi); for (qinfo* qi2 : m_qinfo_vect) { @@ -1721,140 +1644,89 @@ namespace smt { TRACE("model_finder", tout << "new quantifier qinfo: "; qi->display(tout); tout << "\n";); } - void insert_macro(cond_macro * m) { - m_cond_macros.push_back(m); - } - public: typedef ptr_vector::const_iterator macro_iterator; - quantifier_info(model_finder& mf, ast_manager & m, quantifier * q): - m_mf(mf), - m_q(q, m), - m_flat_q(m), - m_is_auf(true), - m_has_x_eq_y(false), - m_the_one(nullptr), - m_uvar_inst_sets(nullptr) { + static quantifier_ref mk_flat(ast_manager& m, quantifier* q) { if (has_quantifiers(q->get_expr()) && !m.is_lambda_def(q)) { proof_ref pr(m); expr_ref new_q(m); pull_quant pull(m); pull(q, new_q, pr); SASSERT(is_well_sorted(m, new_q)); - m_flat_q = to_quantifier(new_q); + return quantifier_ref(to_quantifier(new_q), m); } - else { - m_flat_q = q; - } - CTRACE("model_finder_bug", has_quantifiers(m_flat_q->get_expr()), - tout << mk_pp(q, m) << "\n" << mk_pp(m_flat_q, m) << "\n";); + else + return quantifier_ref(q, m); } - ~quantifier_info() { + quantifier_info(model_finder& mf, ast_manager& m, quantifier* q) : + quantifier_macro_info(m, mk_flat(m, q)), + m_mf(mf), + m_q(q, m), + m_uvar_inst_sets(nullptr) { + CTRACE("model_finder_bug", has_quantifiers(m_flat_q->get_expr()), + tout << mk_pp(q, m) << "\n" << mk_pp(m_flat_q, m) << "\n";); + } + + ~quantifier_info() override { std::for_each(m_qinfo_vect.begin(), m_qinfo_vect.end(), delete_proc()); - std::for_each(m_cond_macros.begin(), m_cond_macros.end(), delete_proc()); reset_the_one(); } - bool is_auf() const { return m_is_auf; } - - quantifier * get_flat_q() const { return m_flat_q; } - - bool unary_function_fragment() const { - unsigned sz = m_ng_decls.size(); - if (sz > 1) - return false; - if (sz == 0) - return true; - func_decl * f = *(m_ng_decls.begin()); - return f->get_arity() == 1; - } - - bool has_cond_macros() const { - return !m_cond_macros.empty(); - } - - ptr_vector const& macros() const { return m_cond_macros; } - - void set_the_one(func_decl * m) { - m_the_one = m; - } - - func_decl * get_the_one() const { - return m_the_one; - } - - bool contains_ng_decl(func_decl * f) const { - return m_ng_decls.contains(f); - } - - void display(std::ostream & out) const { - ast_manager & m = m_flat_q.get_manager(); - out << "info for (flat) quantifier:\n" << mk_pp(m_flat_q.get(), m) << "\n"; - out << "IS_AUF: " << m_is_auf << ", has x=y: " << m_has_x_eq_y << "\n"; - out << "unary function fragment: " << unary_function_fragment() << "\n"; - out << "ng decls: "; - for (func_decl * f : m_ng_decls) { - out << f->get_name() << " "; - } + std::ostream& display(std::ostream& out) const override { + quantifier_macro_info::display(out); out << "\ninfo bits:\n"; for (qinfo* qi : m_qinfo_vect) { out << " "; qi->display(out); out << "\n"; } - out << "\nmacros:\n"; - for (cond_macro* cm : m_cond_macros) { - out << " "; cm->display(out); out << "\n"; - } + return out; } - void process_auf(auf_solver & s, context * ctx) { + void process_auf(auf_solver& s, context* ctx) { for (unsigned i = 0; i < m_flat_q->get_num_decls(); i++) { // make sure a node exists for each variable. s.get_uvar(m_flat_q, i); } - for (qinfo * qi : m_qinfo_vect) { + for (qinfo* qi : m_qinfo_vect) { qi->process_auf(m_flat_q, s, ctx); } } - void populate_inst_sets(auf_solver & s, context * ctx) { - for (qinfo * qi : m_qinfo_vect) { + void populate_inst_sets(auf_solver& s, context* ctx) { + for (qinfo* qi : m_qinfo_vect) { qi->populate_inst_sets(m_flat_q, s, ctx); } // second pass - for (qinfo * qi : m_qinfo_vect) { + for (qinfo* qi : m_qinfo_vect) { checkpoint(); qi->populate_inst_sets2(m_flat_q, s, ctx); } } - func_decl_set const & get_ng_decls() const { - return m_ng_decls; - } - void populate_macro_based_inst_sets(context * ctx, evaluator & ev) { + void populate_macro_based_inst_sets(context* ctx, evaluator& ev) { SASSERT(m_the_one != 0); if (m_uvar_inst_sets != nullptr) return; m_uvar_inst_sets = alloc(ptr_vector); for (qinfo* qi : m_qinfo_vect) qi->populate_inst_sets(m_flat_q, m_the_one, *m_uvar_inst_sets, ctx); - for (instantiation_set * s : *m_uvar_inst_sets) { - if (s != nullptr) + for (instantiation_set* s : *m_uvar_inst_sets) { + if (s != nullptr) s->mk_inverse(ev); } } - instantiation_set * get_macro_based_inst_set(unsigned vidx, context * ctx, evaluator & ev) { + instantiation_set* get_macro_based_inst_set(unsigned vidx, context* ctx, evaluator& ev) { if (m_the_one == nullptr) return nullptr; populate_macro_based_inst_sets(ctx, ev); return m_uvar_inst_sets->get(vidx, 0); } - void reset_the_one() { - m_the_one = nullptr; + void reset_the_one() override { + quantifier_macro_info::reset_the_one(); if (m_uvar_inst_sets) { std::for_each(m_uvar_inst_sets->begin(), m_uvar_inst_sets->end(), delete_proc()); dealloc(m_uvar_inst_sets); @@ -1868,14 +1740,14 @@ namespace smt { fill the structure quantifier_info. */ class quantifier_analyzer { - model_finder& m_mf; - ast_manager & m; + model_finder& m_mf; + ast_manager& m; macro_util m_mutil; array_util m_array_util; arith_util m_arith_util; bv_util m_bv_util; - quantifier_info * m_info; + quantifier_info* m_info; typedef enum { POS, NEG } polarity; @@ -1883,64 +1755,64 @@ namespace smt { obj_hashtable m_pos_cache; obj_hashtable m_neg_cache; - typedef std::pair entry; + typedef std::pair entry; svector m_ftodo; ptr_vector m_ttodo; - void insert_qinfo(qinfo * qi) { + void insert_qinfo(qinfo* qi) { SASSERT(m_info); m_info->insert_qinfo(qi); } - bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t) { + bool is_var_plus_ground(expr* n, bool& inv, var*& v, expr_ref& t) { return m_mutil.is_var_plus_ground(n, inv, v, t); } - bool is_var_plus_ground(expr * n, var * & v, expr_ref & t) { + bool is_var_plus_ground(expr* n, var*& v, expr_ref& t) { bool inv; TRACE("is_var_plus_ground", tout << mk_pp(n, m) << "\n"; - tout << "is_var_plus_ground: " << is_var_plus_ground(n, inv, v, t) << "\n"; - tout << "inv: " << inv << "\n";); + tout << "is_var_plus_ground: " << is_var_plus_ground(n, inv, v, t) << "\n"; + tout << "inv: " << inv << "\n";); return is_var_plus_ground(n, inv, v, t) && !inv; } - bool is_add(expr * n) const { + bool is_add(expr* n) const { return m_mutil.is_add(n); } - bool is_zero(expr * n) const { + bool is_zero(expr* n) const { return m_mutil.is_zero_safe(n); } - bool is_times_minus_one(expr * n, expr * & arg) const { + bool is_times_minus_one(expr* n, expr*& arg) const { return m_mutil.is_times_minus_one(n, arg); } - bool is_le(expr * n) const { + bool is_le(expr* n) const { return m_mutil.is_le(n); } - bool is_le_ge(expr * n) const { + bool is_le_ge(expr* n) const { return m_mutil.is_le_ge(n); } - bool is_signed_le(expr * n) const { + bool is_signed_le(expr* n) const { return m_bv_util.is_bv_sle(n); } - expr * mk_one(sort * s) { + expr* mk_one(sort* s) { return m_bv_util.is_bv_sort(s) ? m_bv_util.mk_numeral(rational(1), s) : m_arith_util.mk_numeral(rational(1), s); } - void mk_sub(expr * t1, expr * t2, expr_ref & r) const { + void mk_sub(expr* t1, expr* t2, expr_ref& r) const { m_mutil.mk_sub(t1, t2, r); } - void mk_add(expr * t1, expr * t2, expr_ref & r) const { + void mk_add(expr* t1, expr* t2, expr_ref& r) const { m_mutil.mk_add(t1, t2, r); } - bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t, bool & inv) { + bool is_var_and_ground(expr* lhs, expr* rhs, var*& v, expr_ref& t, bool& inv) { inv = false; // true if invert the sign TRACE("is_var_and_ground", tout << "is_var_and_ground: " << mk_ismt2_pp(lhs, m) << " " << mk_ismt2_pp(rhs, m) << "\n";); if (is_var(lhs) && is_ground(rhs)) { @@ -1975,12 +1847,12 @@ namespace smt { return false; } - bool is_var_and_ground(expr * lhs, expr * rhs, var * & v, expr_ref & t) { + bool is_var_and_ground(expr* lhs, expr* rhs, var*& v, expr_ref& t) { bool inv; return is_var_and_ground(lhs, rhs, v, t, inv); } - - bool is_x_eq_t_atom(expr * n, var * & v, expr_ref & t) { + + bool is_x_eq_t_atom(expr* n, var*& v, expr_ref& t) { if (!is_app(n)) return false; if (m.is_eq(n)) @@ -1988,16 +1860,16 @@ namespace smt { return false; } - bool is_var_minus_var(expr * n, var * & v1, var * & v2) { + bool is_var_minus_var(expr* n, var*& v1, var*& v2) { if (!is_add(n)) return false; - expr * arg1 = to_app(n)->get_arg(0); - expr * arg2 = to_app(n)->get_arg(1); + expr* arg1 = to_app(n)->get_arg(0); + expr* arg2 = to_app(n)->get_arg(1); if (!is_var(arg1)) std::swap(arg1, arg2); if (!is_var(arg1)) return false; - expr * arg2_2; + expr* arg2_2; if (!is_times_minus_one(arg2, arg2_2)) return false; if (!is_var(arg2_2)) @@ -2007,7 +1879,7 @@ namespace smt { return true; } - bool is_var_and_var(expr * lhs, expr * rhs, var * & v1, var * & v2) { + bool is_var_and_var(expr* lhs, expr* rhs, var*& v1, var*& v2) { if (is_var(lhs) && is_var(rhs)) { v1 = to_var(lhs); v2 = to_var(rhs); @@ -2018,33 +1890,33 @@ namespace smt { (is_var_minus_var(rhs, v1, v2) && is_zero(lhs)); } - bool is_x_eq_y_atom(expr * n, var * & v1, var * & v2) { + bool is_x_eq_y_atom(expr* n, var*& v1, var*& v2) { return m.is_eq(n) && is_var_and_var(to_app(n)->get_arg(0), to_app(n)->get_arg(1), v1, v2); } - bool is_x_gle_y_atom(expr * n, var * & v1, var * & v2) { + bool is_x_gle_y_atom(expr* n, var*& v1, var*& v2) { return is_le_ge(n) && is_var_and_var(to_app(n)->get_arg(0), to_app(n)->get_arg(1), v1, v2); } - bool is_x_gle_t_atom(expr * atom, bool sign, var * & v, expr_ref & t) { + bool is_x_gle_t_atom(expr* atom, bool sign, var*& v, expr_ref& t) { if (!is_app(atom)) return false; if (sign) { bool r = is_le_ge(atom) && is_var_and_ground(to_app(atom)->get_arg(0), to_app(atom)->get_arg(1), v, t); CTRACE("is_x_gle_t", r, tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m) << "\n--->\n" - << mk_ismt2_pp(v, m) << " " << mk_ismt2_pp(t, m) << "\n"; - tout << "sign: " << sign << "\n";); + << mk_ismt2_pp(v, m) << " " << mk_ismt2_pp(t, m) << "\n"; + tout << "sign: " << sign << "\n";); return r; } else { if (is_le_ge(atom)) { expr_ref tmp(m); bool le = is_le(atom); - bool inv = false; + bool inv = false; if (is_var_and_ground(to_app(atom)->get_arg(0), to_app(atom)->get_arg(1), v, tmp, inv)) { if (inv) le = !le; - sort * s = m.get_sort(tmp); + sort* s = m.get_sort(tmp); expr_ref one(m); one = mk_one(s); if (le) @@ -2052,8 +1924,8 @@ namespace smt { else mk_sub(tmp, one, t); TRACE("is_x_gle_t", tout << "is_x_gle_t: " << mk_ismt2_pp(atom, m) << "\n--->\n" - << mk_ismt2_pp(v, m) << " " << mk_ismt2_pp(t, m) << "\n"; - tout << "sign: " << sign << "\n";); + << mk_ismt2_pp(v, m) << " " << mk_ismt2_pp(t, m) << "\n"; + tout << "sign: " << sign << "\n";); return true; } } @@ -2066,21 +1938,21 @@ namespace smt { m_neg_cache.reset(); } - obj_hashtable & get_cache(polarity pol) { + obj_hashtable& get_cache(polarity pol) { return pol == POS ? m_pos_cache : m_neg_cache; } - void visit_formula(expr * n, polarity pol) { + void visit_formula(expr* n, polarity pol) { if (is_ground(n)) return; // ground terms do not need to be visited. - obj_hashtable & c = get_cache(pol); + obj_hashtable& c = get_cache(pol); if (!c.contains(n)) { m_ftodo.push_back(entry(n, pol)); c.insert(n); } } - void visit_term(expr * n) { + void visit_term(expr* n) { // ground terms do not need to be visited. if (!is_ground(n) && !m_pos_cache.contains(n)) { m_ttodo.push_back(n); @@ -2091,17 +1963,17 @@ namespace smt { /** \brief Process uninterpreted applications. */ - void process_u_app(app * t) { + void process_u_app(app* t) { unsigned num_args = t->get_num_args(); for (unsigned i = 0; i < num_args; i++) { - expr * arg = t->get_arg(i); + expr* arg = t->get_arg(i); if (is_var(arg)) { SASSERT(t->get_decl()->get_domain(i) == to_var(arg)->get_sort()); insert_qinfo(alloc(f_var, m, t->get_decl(), i, to_var(arg)->get_idx())); continue; } - var * v; + var* v; expr_ref k(m); if (is_var_plus_ground(arg, v, k)) { insert_qinfo(alloc(f_var_plus_offset, m, t->get_decl(), i, v->get_idx(), k.get())); @@ -2122,13 +1994,13 @@ namespace smt { where a is ground or is_auf_select(a) == true and the indices are ground terms or variables. */ - bool is_auf_select(expr * t) const { + bool is_auf_select(expr* t) const { if (!m_array_util.is_select(t)) return false; - expr * a = to_app(t)->get_arg(0); + expr* a = to_app(t)->get_arg(0); if (!is_ground(a) && !is_auf_select(a)) return false; - for (expr * arg : *to_app(t)) { + for (expr* arg : *to_app(t)) { if (!is_ground(arg) && !is_var(arg)) return false; } @@ -2138,13 +2010,13 @@ namespace smt { /** \brief Process interpreted applications. */ - void process_i_app(app * t) { + void process_i_app(app* t) { if (is_auf_select(t)) { unsigned num_args = t->get_num_args(); - app * array = to_app(t->get_arg(0)); + app* array = to_app(t->get_arg(0)); visit_term(array); // array may be a nested array. for (unsigned i = 1; i < num_args; i++) { - expr * arg = t->get_arg(i); + expr* arg = t->get_arg(i); if (is_var(arg)) { insert_qinfo(alloc(select_var, m, t, i, to_var(arg)->get_idx())); } @@ -2154,13 +2026,13 @@ namespace smt { } } else { - for (expr * arg : *t) { + for (expr* arg : *t) { visit_term(arg); } } } - void process_app(app * t) { + void process_app(app* t) { SASSERT(!is_ground(t)); if (t->get_family_id() != m.get_basic_family_id()) { @@ -2177,7 +2049,7 @@ namespace smt { void process_terms_on_stack() { while (!m_ttodo.empty()) { - expr * curr = m_ttodo.back(); + expr* curr = m_ttodo.back(); m_ttodo.pop_back(); if (m.is_bool(curr)) { @@ -2194,12 +2066,12 @@ namespace smt { m_info->m_is_auf = false; // unexpected occurrence of variable. } else { - SASSERT(is_lambda(curr)); + SASSERT(is_lambda(curr)); } } } - void process_literal(expr * atom, bool sign) { + void process_literal(expr* atom, bool sign) { CTRACE("model_finder_bug", is_ground(atom), tout << mk_pp(atom, m) << "\n";); SASSERT(!is_ground(atom)); SASSERT(m.is_bool(atom)); @@ -2217,7 +2089,7 @@ namespace smt { } if (is_app(atom)) { - var * v, * v1, * v2; + var* v, * v1, * v2; expr_ref t(m); if (is_x_eq_t_atom(atom, v, t)) { if (sign) @@ -2252,23 +2124,23 @@ namespace smt { UNREACHABLE(); } - void process_literal(expr * atom, polarity pol) { + void process_literal(expr* atom, polarity pol) { process_literal(atom, pol == NEG); } - void process_and_or(app * n, polarity p) { + void process_and_or(app* n, polarity p) { for (expr* arg : *n) visit_formula(arg, p); } - void process_ite(app * n, polarity p) { + void process_ite(app* n, polarity p) { visit_formula(n->get_arg(0), p); visit_formula(n->get_arg(0), neg(p)); visit_formula(n->get_arg(1), p); visit_formula(n->get_arg(2), p); } - void process_iff(app * n) { + void process_iff(app* n) { visit_formula(n->get_arg(0), POS); visit_formula(n->get_arg(0), NEG); visit_formula(n->get_arg(1), POS); @@ -2282,8 +2154,8 @@ namespace smt { void process_formulas_on_stack() { while (!m_ftodo.empty()) { checkpoint(); - entry & e = m_ftodo.back(); - expr * curr = e.first; + entry& e = m_ftodo.back(); + expr* curr = e.first; polarity pol = e.second; m_ftodo.pop_back(); if (is_app(curr)) { @@ -2332,18 +2204,18 @@ namespace smt { } } - void process_formula(expr * n) { + void process_formula(expr* n) { SASSERT(m.is_bool(n)); visit_formula(n, POS); } - void process_clause(expr * cls) { + void process_clause(expr* cls) { SASSERT(is_clause(m, cls)); unsigned num_lits = get_clause_num_literals(m, cls); for (unsigned i = 0; i < num_lits; i++) { - expr * lit = get_clause_literal(m, cls, i); + expr* lit = get_clause_literal(m, cls, i); SASSERT(is_literal(m, lit)); - expr * atom; + expr* atom; bool sign; get_literal_atom_sign(m, lit, atom, sign); if (!is_ground(atom)) @@ -2351,40 +2223,29 @@ namespace smt { } } - void collect_macro_candidates(quantifier * q) { - macro_util::macro_candidates candidates(m); - m_mutil.collect_macro_candidates(q, candidates); - unsigned num_candidates = candidates.size(); - for (unsigned i = 0; i < num_candidates; i++) { - cond_macro * mc = alloc(cond_macro, m, candidates.get_f(i), candidates.get_def(i), candidates.get_cond(i), - candidates.ineq(i), candidates.satisfy_atom(i), candidates.hint(i), q->get_weight()); - m_info->insert_macro(mc); - } - } - public: - quantifier_analyzer(model_finder& mf, ast_manager & m): + quantifier_analyzer(model_finder& mf, ast_manager& m) : m_mf(mf), m(m), m_mutil(m), - m_array_util(m), + m_array_util(m), m_arith_util(m), m_bv_util(m), m_info(nullptr) { } - void operator()(quantifier_info * d) { + void operator()(quantifier_info* d) { m_info = d; - quantifier * q = d->get_flat_q(); + quantifier* q = d->get_flat_q(); if (m.is_lambda_def(q)) return; - expr * e = q->get_expr(); + expr* e = q->get_expr(); reset_cache(); if (!m.inc()) return; m_ttodo.reset(); m_ftodo.reset(); - + if (is_clause(m, e)) { process_clause(e); } @@ -2397,770 +2258,25 @@ namespace smt { process_terms_on_stack(); } - collect_macro_candidates(q); - m_info = nullptr; } }; + } - /** - \brief Base class for macro solvers. - */ - class base_macro_solver { - protected: - ast_manager & m; - obj_map const & m_q2info; - proto_model * m_model; - - quantifier_info * get_qinfo(quantifier * q) const { - return m_q2info[q]; - } - - void set_else_interp(func_decl * f, expr * f_else) { - SASSERT(f_else != nullptr); - func_interp * fi = m_model->get_func_interp(f); - if (fi == nullptr) { - fi = alloc(func_interp, m, f->get_arity()); - m_model->register_decl(f, fi); - } - fi->set_else(f_else); - TRACE("model_finder", tout << f->get_name() << " " << mk_pp(f_else, m) << "\n";); - } - - virtual bool process(ptr_vector const & qs, ptr_vector & new_qs, ptr_vector & residue) = 0; - - public: - base_macro_solver(ast_manager & m, obj_map const & q2i): - m(m), - m_q2info(q2i), - m_model(nullptr) { - } - - virtual ~base_macro_solver() {} - - /** - \brief Try to satisfy quantifiers in qs by using macro definitions. - Store in new_qs the quantifiers that were not satisfied. - Store in residue a subset of the quantifiers that were satisfied but contain information useful for the auf_solver. - */ - void operator()(proto_model * m, ptr_vector const & qs, ptr_vector & new_qs, ptr_vector & residue) { - m_model = m; - ptr_vector curr_qs(qs); - while (process(curr_qs, new_qs, residue)) { - curr_qs.swap(new_qs); - new_qs.reset(); - } - } - }; - - - /** - \brief The simple macro solver satisfies quantifiers that contain - (conditional) macros for a function f that does not occur in any other quantifier. - - Since f does not occur in any other quantifier, I don't need to track the dependencies - of f. That is, recursive definition cannot be created. - */ - class simple_macro_solver : public base_macro_solver { - protected: - /** - \brief Return true if \c f is in (qs\{q}) - */ - bool contains(func_decl * f, ptr_vector const & qs, quantifier * q) { - for (quantifier * other : qs) { - if (q == other) - continue; - quantifier_info * other_qi = get_qinfo(other); - if (other_qi->contains_ng_decl(f)) - return true; - } - return false; - } - - bool process(quantifier * q, ptr_vector const & qs) { - quantifier_info * qi = get_qinfo(q); - for (cond_macro* m : qi->macros()) { - if (!m->satisfy_atom()) - continue; - func_decl * f = m->get_f(); - if (!contains(f, qs, q)) { - qi->set_the_one(f); - expr * f_else = m->get_def(); - SASSERT(f_else != nullptr); - // Remark: I can ignore the conditions of m because - // I know the (partial) interpretation of f satisfied the ground part. - // MBQI will force extra instantiations if the (partial) interpretation of f - // does not satisfy the quantifier. - // In all other cases the "else" of f will satisfy the quantifier. - set_else_interp(f, f_else); - TRACE("model_finder", tout << "satisfying the quantifier using simple macro:\n"; - m->display(tout); tout << "\n";); - return true; // satisfied quantifier - } - } - return false; - } - - bool process(ptr_vector const & qs, ptr_vector & new_qs, ptr_vector & residue) override { - bool removed = false; - for (quantifier* q : qs) { - if (process(q, qs)) - removed = true; - else - new_qs.push_back(q); - } - return removed; - } - - public: - simple_macro_solver(ast_manager & m, obj_map const & q2i): - base_macro_solver(m, q2i) {} - }; - - - class hint_solver : public base_macro_solver { - /* - This solver tries to satisfy quantifiers by using macros, cond_macros and hints. - The idea is to satisfy a set of quantifiers Q = Q_{f_1} union ... union Q_{f_n} - where Q_{f_i} is the set of quantifiers that contain the function f_i. - Let f_i = def_i be macros (in this solver conditions are ignored). - Let Q_{f_i = def_i} be the set of quantifiers where f_i = def_i is a macro. - Then, the set Q can be satisfied using f_1 = def_1 ... f_n = def_n - when - - Q_{f_1} union ... union Q_{f_n} = Q_{f_1 = def_1} ... Q_{f_n = def_n} (*) - - So, given a set of macros f_1 = def_1, ..., f_n = d_n, it is very easy to check - whether they can be used to satisfy all quantifiers that use f_1, ..., f_n in - non ground terms. - - We can find the sets of f_1 = def_1, ..., f_n = def_n that satisfy Q using - the following search procedure - find(Q) - for each f_i = def_i in Q - R = greedy(Q_{f_i = def_1}, Q_f_i \ Q_{f_i = def_i}, {f_i}, {f_i = def_i}) - if (R != empty-set) - return R - greedy(Satisfied, Residue, F, F_DEF) - if Residue = empty-set return F_DEF - for each f_j = def_j in Residue such that f_j not in F - New-Satisfied = Satisfied union Q_{f_j = def_j} - New-Residue = (Residue union Q_{f_j}) \ New-Satisfied - R = greedy(New-Satisfied, New-Residue, F \union {f_j}, F_DEF union {f_j = def_j}) - if (R != empty-set) - return R - - This search may be too expensive, and is exponential on the number of different function - symbols. - Some observations to prune the search space. - 1) If f_i occurs in a quantifier without macros, then f_i and any macro using it can be ignored during the search. - 2) If f_i = def_i is not a macro in a quantifier q, and there is no other f_j = def_j (i != j) in q, - then f_i = def_i can be ignored during the search. - */ - - typedef obj_hashtable quantifier_set; - typedef obj_map q_f; - typedef obj_pair_map q_f_def; - typedef obj_pair_hashtable f_def_set; - typedef obj_hashtable expr_set; - typedef obj_map f2defs; - - q_f m_q_f; - q_f_def m_q_f_def; - ptr_vector m_qsets; - f2defs m_f2defs; - ptr_vector m_esets; - - void insert_q_f(quantifier * q, func_decl * f) { - SASSERT(!m_forbidden.contains(f)); - quantifier_set * s = nullptr; - if (!m_q_f.find(f, s)) { - s = alloc(quantifier_set); - m_q_f.insert(f, s); - m_qsets.push_back(s); - } - SASSERT(s != nullptr); - s->insert(q); - } - - void insert_f2def(func_decl * f, expr * def) { - expr_set * s = nullptr; - if (!m_f2defs.find(f, s)) { - s = alloc(expr_set); - m_f2defs.insert(f, s); - m_esets.push_back(s); - } - SASSERT(s != nullptr); - s->insert(def); - } - - void insert_q_f_def(quantifier * q, func_decl * f, expr * def) { - SASSERT(!m_forbidden.contains(f)); - quantifier_set * s = nullptr; - if (!m_q_f_def.find(f, def, s)) { - s = alloc(quantifier_set); - m_q_f_def.insert(f, def, s); - insert_f2def(f, def); - m_qsets.push_back(s); - } - SASSERT(s != nullptr); - s->insert(q); - } - - quantifier_set * get_q_f(func_decl * f) { return m_q_f[f]; } - - quantifier_set * get_q_f_def(func_decl * f, expr * def) { - quantifier_set * s = nullptr; - m_q_f_def.find(f, def, s); - SASSERT(s != nullptr); - return s; - } - - expr_set * get_f_defs(func_decl * f) { return m_f2defs[f]; } - - void reset_q_fs() { - std::for_each(m_qsets.begin(), m_qsets.end(), delete_proc()); - std::for_each(m_esets.begin(), m_esets.end(), delete_proc()); - m_q_f.reset(); - m_q_f_def.reset(); - m_qsets.reset(); - m_f2defs.reset(); - m_esets.reset(); - } - - func_decl_set m_forbidden; - func_decl_set m_candidates; - - bool is_candidate(quantifier * q) const { - quantifier_info * qi = get_qinfo(q); - for (cond_macro* m : qi->macros()) { - if (m->satisfy_atom() && !m_forbidden.contains(m->get_f())) - return true; - } - return false; - } - - void register_decls_as_forbidden(quantifier * q) { - quantifier_info * qi = get_qinfo(q); - func_decl_set const & ng_decls = qi->get_ng_decls(); - for (func_decl* f : ng_decls) { - m_forbidden.insert(f); - } - } - - void preprocess(ptr_vector const & qs, ptr_vector & qcandidates, ptr_vector & non_qcandidates) { - ptr_vector curr(qs); - while (true) { - for (quantifier * q : curr) { - if (is_candidate(q)) { - qcandidates.push_back(q); - } - else { - register_decls_as_forbidden(q); - non_qcandidates.push_back(q); - } - } - if (curr.size() == qcandidates.size()) - return; - SASSERT(qcandidates.size() < curr.size()); - curr.swap(qcandidates); - qcandidates.reset(); - } - } - - void mk_q_f_defs(ptr_vector const & qs) { - for (quantifier * q : qs) { - quantifier_info * qi = get_qinfo(q); - func_decl_set const & ng_decls = qi->get_ng_decls(); - for (func_decl* f : ng_decls) { - if (!m_forbidden.contains(f)) - insert_q_f(q, f); - } - for (cond_macro * m : qi->macros()) { - if (m->satisfy_atom() && !m_forbidden.contains(m->get_f())) { - insert_q_f_def(q, m->get_f(), m->get_def()); - m_candidates.insert(m->get_f()); - } - } - } - } - - static void display_quantifier_set(std::ostream & out, quantifier_set const * s) { - for (quantifier* q : *s) { - out << q->get_qid() << " "; - } - out << "\n"; - } - - void display_qcandidates(std::ostream & out, ptr_vector const & qcandidates) const { - for (quantifier * q : qcandidates) { - out << q->get_qid() << " ->\n" << mk_pp(q, m) << "\n"; - quantifier_info * qi = get_qinfo(q); - qi->display(out); - out << "------\n"; - } - out << "Sets Q_f\n"; - for (auto const& kv : m_q_f) { - func_decl * f = kv.m_key; - quantifier_set * s = kv.m_value; - out << f->get_name() << " -> "; display_quantifier_set(out, s); - } - out << "Sets Q_{f = def}\n"; - for (auto const& kv : m_q_f_def) { - func_decl * f = kv.get_key1(); - expr * def = kv.get_key2(); - quantifier_set * s = kv.get_value(); - out << f->get_name() << " " << mk_pp(def, m) << " ->\n"; display_quantifier_set(out, s); - } - } - - // - // Search: main procedures - // - - struct ev_handler { - hint_solver * m_owner; - - void operator()(quantifier * q, bool ins) { - quantifier_info * qi = m_owner->get_qinfo(q); - qi->set_the_one(nullptr); - } - - ev_handler(hint_solver * o): - m_owner(o) { - } - }; - - - typedef backtrackable_set qset; - typedef backtrackable_set qsset; - typedef obj_map f2def; - - qset m_residue; - qsset m_satisfied; - f2def m_fs; // set of function symbols (and associated interpretation) that were used to satisfy the quantifiers in m_satisfied. - - struct found_satisfied_subset {}; - - void display_search_state(std::ostream & out) const { - out << "fs:\n"; - for (auto const& kv : m_fs) { - out << kv.m_key->get_name() << " "; - } - out << "\nsatisfied:\n"; - for (auto q : m_satisfied) { - out << q->get_qid() << " "; - } - out << "\nresidue:\n"; - for (auto q : m_residue) { - out << q->get_qid() << " "; - } - out << "\n"; - } - - bool check_satisfied_residue_invariant() { - DEBUG_CODE( - for (quantifier * q : m_satisfied) { - SASSERT(!m_residue.contains(q)); - quantifier_info * qi = get_qinfo(q); - SASSERT(qi != nullptr); - SASSERT(qi->get_the_one() != nullptr); - }); - return true; - } - - - bool update_satisfied_residue(func_decl * f, expr * def) { - bool useful = false; - SASSERT(check_satisfied_residue_invariant()); - quantifier_set * q_f = get_q_f(f); - quantifier_set * q_f_def = get_q_f_def(f, def); - for (quantifier * q : *q_f_def) { - if (!m_satisfied.contains(q)) { - useful = true; - m_residue.erase(q); - m_satisfied.insert(q); - quantifier_info * qi = get_qinfo(q); - SASSERT(qi->get_the_one() == 0); - qi->set_the_one(f); // remark... event handler will reset it during backtracking. - } - } - if (!useful) - return false; - for (quantifier * q : *q_f) { - if (!m_satisfied.contains(q)) { - m_residue.insert(q); - } - } - SASSERT(check_satisfied_residue_invariant()); - return true; - } - - /** - \brief Extract from m_residue, func_decls that can be used as macros to satisfy it. - The candidates must not be elements of m_fs. - */ - void get_candidates_from_residue(func_decl_set & candidates) { - for (quantifier * q : m_residue) { - quantifier_info * qi = get_qinfo(q); - for (cond_macro * m : qi->macros()) { - func_decl * f = m->get_f(); - if (m->satisfy_atom() && !m_forbidden.contains(f) && !m_fs.contains(f)) { - candidates.insert(f); - } - } - } - } - -#define GREEDY_MAX_DEPTH 10 /* to avoid too expensive search spaces */ - - /** - \brief Try to reduce m_residue using the macros of f. - */ - void greedy(func_decl * f, unsigned depth) { - if (depth >= GREEDY_MAX_DEPTH) - return; // failed - - TRACE("model_finder_hint", - tout << "greedy depth: " << depth << ", f: " << f->get_name() << "\n"; - display_search_state(tout);); - - expr_set * s = get_f_defs(f); - for (expr * def : *s) { - - SASSERT(!m_fs.contains(f)); - - m_satisfied.push_scope(); - m_residue.push_scope(); - TRACE("model_finder", tout << f->get_name() << " " << mk_pp(def, m) << "\n";); - m_fs.insert(f, def); - - if (update_satisfied_residue(f, def)) { - // update was useful - greedy(depth + 1); // greedy throws exception in case of success - // reachable iff greedy failed. - } - - m_satisfied.pop_scope(); - m_residue.pop_scope(); - m_fs.erase(f); - } - } - - /** - \brief check if satisfied subset introduces a cyclic dependency. - - f_1 = def_1(f_2), ..., f_n = def_n(f_1) - */ - - expr_mark m_visited; - obj_hashtable m_acyclic; - bool is_cyclic() { - m_acyclic.reset(); - while (true) { - unsigned sz = m_acyclic.size(); - if (sz == m_fs.size()) return false; // there are no cyclic dependencies - for (auto const& kv : m_fs) { - func_decl * f = kv.m_key; - if (m_acyclic.contains(f)) continue; - if (is_acyclic(kv.m_value)) - m_acyclic.insert(f); - } - if (sz == m_acyclic.size()) return true; // no progress, so dependency cycle found. - } - } - - struct occurs {}; - struct occurs_check { - hint_solver& m_cls; - occurs_check(hint_solver& hs): m_cls(hs) {} - void operator()(app* n) { if (m_cls.m_fs.contains(n->get_decl()) && !m_cls.m_acyclic.contains(n->get_decl())) throw occurs(); } - void operator()(var* n) {} - void operator()(quantifier* n) {} - }; - bool is_acyclic(expr* def) { - m_visited.reset(); - occurs_check oc(*this); - try { - for_each_expr(oc, m_visited, def); - } - catch (const occurs &) { - return false; - } - return true; - } - - /** - \brief Try to reduce m_residue (if not empty) by selecting a function f - that is a macro in the residue. - */ - void greedy(unsigned depth) { - if (m_residue.empty()) { - if (is_cyclic()) return; - TRACE("model_finder_hint", - tout << "found subset that is satisfied by macros\n"; - display_search_state(tout);); - throw found_satisfied_subset(); - } - func_decl_set candidates; - get_candidates_from_residue(candidates); - - TRACE("model_finder_hint", tout << "candidates from residue:\n"; - for (func_decl * f : candidates) { - tout << f->get_name() << " "; - } - tout << "\n";); - - for (func_decl* f : candidates) { - greedy(f, depth); - } - } - - /** - \brief Try to find a set of quantifiers by starting to use the macros of f. - This is the "find" procedure in the comments above. - The set of satisfied quantifiers is in m_satisfied, and the remaining to be - satisfied in m_residue. When the residue becomes empty we throw the exception found_satisfied_subset. - */ - void process(func_decl * f) { - SASSERT(m_satisfied.empty()); - SASSERT(m_residue.empty()); - greedy(f, 0); - } - - /** - \brief Copy the quantifiers from qcandidates to new_qs that are not in m_satisfied. - */ - void copy_non_satisfied(ptr_vector const & qcandidates, ptr_vector & new_qs) { - for (quantifier * q : qcandidates) { - if (!m_satisfied.contains(q)) - new_qs.push_back(q); - } - } - - /** - \brief Use m_fs to set the interpretation of the function symbols that were used to satisfy the - quantifiers in m_satisfied. - */ - void set_interp() { - for (auto const& kv : m_fs) { - func_decl * f = kv.m_key; - expr * def = kv.m_value; - set_else_interp(f, def); - } - } - - void reset() { - reset_q_fs(); - m_forbidden.reset(); - m_candidates.reset(); - m_satisfied.reset(); - m_residue.reset(); - m_fs.reset(); - } - - bool process(ptr_vector const & qs, ptr_vector & new_qs, ptr_vector & residue) override { - reset(); - ptr_vector qcandidates; - preprocess(qs, qcandidates, new_qs); - if (qcandidates.empty()) { - SASSERT(new_qs.size() == qs.size()); - return false; - } - mk_q_f_defs(qcandidates); - TRACE("model_finder_hint", tout << "starting hint-solver search using:\n"; display_qcandidates(tout, qcandidates);); - for (func_decl * f : m_candidates) { - try { - process(f); - } - catch (const found_satisfied_subset &) { - set_interp(); - copy_non_satisfied(qcandidates, new_qs); - return true; - } - } - // failed... copy everything to new_qs - new_qs.append(qcandidates); - return false; - } - - public: - hint_solver(ast_manager & m, obj_map const & q2i): - base_macro_solver(m, q2i), - m_satisfied(ev_handler(this)) { - } - - ~hint_solver() override { - reset(); - } - - }; - - - /** - \brief Satisfy clauses that are not in the AUF fragment but define conditional macros. - These clauses are eliminated even if the symbol being defined occurs in other quantifiers. - The auf_solver is ineffective in these clauses. - - \remark Full macros are used even if they are in the AUF fragment. - */ - class non_auf_macro_solver : public base_macro_solver { - func_decl_dependencies & m_dependencies; - qi_params const * m_qi_params; - - bool add_macro(func_decl * f, expr * f_else) { - TRACE("model_finder", tout << "trying to add macro for " << f->get_name() << "\n" << mk_pp(f_else, m) << "\n";); - func_decl_set * s = m_dependencies.mk_func_decl_set(); - m_dependencies.collect_ng_func_decls(f_else, s); - if (!m_dependencies.insert(f, s)) { - TRACE("model_finder", tout << "failed to add macro\n";); - return false; // cyclic dependency - } - set_else_interp(f, f_else); - return true; - } - - // Return true if r1 is a better macro than r2. - bool is_better_macro(cond_macro * r1, cond_macro * r2) { - if (r2 == nullptr || !r1->is_hint()) - return true; - if (!r2->is_hint()) - return false; - SASSERT(r1->is_hint() && r2->is_hint()); - if (is_ground(r1->get_def()) && !is_ground(r2->get_def())) - return true; - return false; - } - - cond_macro * get_macro_for(func_decl * f, quantifier * q) { - cond_macro * r = nullptr; - quantifier_info * qi = get_qinfo(q); - for (cond_macro * m : qi->macros()) { - if (m->get_f() == f && !m->is_hint() && is_better_macro(m, r)) - r = m; - } - return r; - } - - typedef std::pair mq_pair; - - void collect_candidates(ptr_vector const & qs, obj_map & full_macros, func_decl_set & cond_macros) { - for (quantifier * q : qs) { - quantifier_info * qi = get_qinfo(q); - for (cond_macro * m : qi->macros()) { - if (!m->is_hint()) { - func_decl * f = m->get_f(); - TRACE("model_finder", tout << "considering macro for: " << f->get_name() << "\n"; - m->display(tout); tout << "\n";); - SASSERT(m_qi_params != nullptr); - if (m->is_unconditional() && (!qi->is_auf() || m->get_weight() >= m_qi_params->m_mbqi_force_template)) { - full_macros.insert(f, std::make_pair(m, q)); - cond_macros.erase(f); - } - else if (!full_macros.contains(f) && !qi->is_auf()) - cond_macros.insert(f); - } - } - } - } - - void process_full_macros(obj_map const & full_macros, obj_hashtable & removed) { - for (auto const& kv : full_macros) { - func_decl * f = kv.m_key; - cond_macro * m = kv.m_value.first; - quantifier * q = kv.m_value.second; - SASSERT(m->is_unconditional()); - if (add_macro(f, m->get_def())) { - get_qinfo(q)->set_the_one(f); - removed.insert(q); - } - } - } - - void process(func_decl * f, ptr_vector const & qs, obj_hashtable & removed) { - expr_ref fi_else(m); - ptr_buffer to_remove; - for (quantifier * q : qs) { - if (removed.contains(q)) - continue; - cond_macro * cm = get_macro_for(f, q); - if (!cm) - continue; - SASSERT(!cm->is_hint()); - if (cm->is_unconditional()) - return; // f is part of a full macro... ignoring it. - to_remove.push_back(q); - if (fi_else.get() == nullptr) { - fi_else = cm->get_def(); - } - else { - fi_else = m.mk_ite(cm->get_cond(), cm->get_def(), fi_else); - } - } - if (fi_else.get() != nullptr && add_macro(f, fi_else)) { - for (quantifier * q : to_remove) { - get_qinfo(q)->set_the_one(f); - removed.insert(q); - } - } - } - - void process_cond_macros(func_decl_set const & cond_macros, ptr_vector const & qs, obj_hashtable & removed) { - for (func_decl * f : cond_macros) { - process(f, qs, removed); - } - } - - bool process(ptr_vector const & qs, ptr_vector & new_qs, ptr_vector & residue) override { - obj_map full_macros; - func_decl_set cond_macros; - obj_hashtable removed; - - // Possible improvement: sort full_macros & cond_macros using an user provided precedence function. - - collect_candidates(qs, full_macros, cond_macros); - process_full_macros(full_macros, removed); - process_cond_macros(cond_macros, qs, removed); - - for (quantifier * q : qs) { - if (removed.contains(q)) - continue; - new_qs.push_back(q); - residue.push_back(q); - } - return !removed.empty(); - } - - public: - non_auf_macro_solver(ast_manager & m, obj_map const & q2i, func_decl_dependencies & d): - base_macro_solver(m, q2i), - m_dependencies(d), - m_qi_params(nullptr) { - } - - void set_params(qi_params const & p) { - SASSERT(m_qi_params == 0); - m_qi_params = &p; - } - }; - }; // ----------------------------------- // // model finder // // ----------------------------------- - - model_finder::model_finder(ast_manager & m): + + model_finder::model_finder(ast_manager& m) : m(m), m_context(nullptr), m_analyzer(alloc(quantifier_analyzer, *this, m)), m_auf_solver(alloc(auf_solver, m)), m_dependencies(m), - m_sm_solver(alloc(simple_macro_solver, m, m_q2info)), - m_hint_solver(alloc(hint_solver, m, m_q2info)), - m_nm_solver(alloc(non_auf_macro_solver, m, m_q2info, m_dependencies)), m_new_constraints(m) { } @@ -3177,7 +2293,7 @@ namespace smt { throw tactic_exception(m_context->get_manager().limit().get_cancel_msg()); } - mf::quantifier_info * model_finder::get_quantifier_info(quantifier * q) { + mf::quantifier_info* model_finder::get_quantifier_info(quantifier* q) { mf::quantifier_info* qi = nullptr; if (!m_q2info.find(q, qi)) { register_quantifier(q); @@ -3186,15 +2302,14 @@ namespace smt { return qi; } - void model_finder::set_context(context * ctx) { + void model_finder::set_context(context* ctx) { SASSERT(m_context == nullptr); m_context = ctx; - m_nm_solver->set_params(ctx->get_fparams()); } - void model_finder::register_quantifier(quantifier * q) { + void model_finder::register_quantifier(quantifier* q) { TRACE("model_finder", tout << "registering:\n" << q->get_id() << ": " << q << " " << &m_q2info << " " << mk_pp(q, m) << "\n";); - quantifier_info * new_info = alloc(quantifier_info, *this, m, q); + quantifier_info* new_info = alloc(quantifier_info, *this, m, q); m_q2info.insert(q, new_info); m_quantifiers.push_back(q); m_analyzer->operator()(new_info); @@ -3203,7 +2318,7 @@ namespace smt { void model_finder::push_scope() { m_scopes.push_back(scope()); - scope & s = m_scopes.back(); + scope& s = m_scopes.back(); s.m_quantifiers_lim = m_quantifiers.size(); } @@ -3211,9 +2326,9 @@ namespace smt { unsigned curr_size = m_quantifiers.size(); SASSERT(old_size <= curr_size); for (unsigned i = old_size; i < curr_size; i++) { - quantifier * q = m_quantifiers[i]; + quantifier* q = m_quantifiers[i]; SASSERT(m_q2info.contains(q)); - quantifier_info * info = get_quantifier_info(q); + quantifier_info* info = get_quantifier_info(q); m_q2info.erase(q); dealloc(info); } @@ -3221,10 +2336,10 @@ namespace smt { } void model_finder::pop_scope(unsigned num_scopes) { - unsigned lvl = m_scopes.size(); + unsigned lvl = m_scopes.size(); SASSERT(num_scopes <= lvl); - unsigned new_lvl = lvl - num_scopes; - scope & s = m_scopes[new_lvl]; + unsigned new_lvl = lvl - num_scopes; + scope& s = m_scopes[new_lvl]; restore_quantifiers(s.m_quantifiers_lim); m_scopes.shrink(new_lvl); } @@ -3241,62 +2356,64 @@ namespace smt { // do nothing in the current version } - void model_finder::collect_relevant_quantifiers(ptr_vector & qs) const { - for (quantifier * q : m_quantifiers) { + void model_finder::collect_relevant_quantifiers(ptr_vector& qs) const { + for (quantifier* q : m_quantifiers) { if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) qs.push_back(q); } } - void model_finder::process_auf(ptr_vector const & qs, proto_model * mdl) { + void model_finder::process_auf(ptr_vector const& qs, proto_model* mdl) { m_auf_solver->reset(); m_auf_solver->set_model(mdl); - for (quantifier * q : qs) { - quantifier_info * qi = get_quantifier_info(q); + for (quantifier* q : qs) { + quantifier_info* qi = get_quantifier_info(q); qi->process_auf(*(m_auf_solver.get()), m_context); } m_auf_solver->mk_instantiation_sets(); - for (quantifier * q : qs) { - quantifier_info * qi = get_quantifier_info(q); + for (quantifier* q : qs) { + quantifier_info* qi = get_quantifier_info(q); qi->populate_inst_sets(*(m_auf_solver.get()), m_context); } m_auf_solver->fix_model(m_new_constraints); TRACE("model_finder", - for (quantifier * q : qs) { - quantifier_info * qi = get_quantifier_info(q); - quantifier * fq = qi->get_flat_q(); - tout << "#" << fq->get_id() << " ->\n" << mk_pp(fq, m) << "\n"; - } - m_auf_solver->display_nodes(tout);); + for (quantifier* q : qs) { + quantifier_info* qi = get_quantifier_info(q); + quantifier* fq = qi->get_flat_q(); + tout << "#" << fq->get_id() << " ->\n" << mk_pp(fq, m) << "\n"; + } + m_auf_solver->display_nodes(tout);); } - void model_finder::process_simple_macros(ptr_vector & qs, ptr_vector & residue, proto_model * m) { - ptr_vector new_qs; - m_sm_solver->operator()(m, qs, new_qs, residue); - qs.swap(new_qs); - TRACE("model_finder", tout << "model after processing simple macros:\n"; model_pp(tout, *m);); + quantifier_macro_info* model_finder::operator()(quantifier* q) { + return m_q2info[q]; } - void model_finder::process_hint_macros(ptr_vector & qs, ptr_vector & residue, proto_model * m) { - ptr_vector new_qs; - m_hint_solver->operator()(m, qs, new_qs, residue); - qs.swap(new_qs); - TRACE("model_finder", tout << "model after processing simple macros:\n"; model_pp(tout, *m);); + void model_finder::process_simple_macros(ptr_vector& qs, ptr_vector& residue, proto_model* mdl) { + simple_macro_solver sms(m, *this); + sms(*mdl, qs, residue); + TRACE("model_finder", tout << "model after processing simple macros:\n"; model_pp(tout, *mdl);); } - void model_finder::process_non_auf_macros(ptr_vector & qs, ptr_vector & residue, proto_model * m) { - ptr_vector new_qs; - m_nm_solver->operator()(m, qs, new_qs, residue); - qs.swap(new_qs); - TRACE("model_finder", tout << "model after processing non auf macros:\n"; model_pp(tout, *m);); + void model_finder::process_hint_macros(ptr_vector& qs, ptr_vector& residue, proto_model* mdl) { + hint_macro_solver hms(m, *this); + hms(*mdl, qs, residue); + TRACE("model_finder", tout << "model after processing simple macros:\n"; model_pp(tout, *mdl);); + } + + void model_finder::process_non_auf_macros(ptr_vector& qs, ptr_vector& residue, proto_model* mdl) { + non_auf_macro_solver nas(m, *this, m_dependencies); + nas.set_mbqi_force_template(m_context->get_fparams().m_mbqi_force_template); + nas(*mdl, qs, residue); + TRACE("model_finder", tout << "model after processing non auf macros:\n"; model_pp(tout, *mdl);); } /** \brief Clean leftovers from previous invocations to fix_model. */ - void model_finder::cleanup_quantifier_infos(ptr_vector const & qs) { + void model_finder::cleanup_quantifier_infos(ptr_vector const& qs) { for (quantifier* q : qs) { get_quantifier_info(q)->reset_the_one(); } @@ -3306,7 +2423,7 @@ namespace smt { \brief Try to satisfy quantifiers by modifying the model while preserving the satisfiability of all ground formulas asserted into the logical context. */ - void model_finder::fix_model(proto_model * m) { + void model_finder::fix_model(proto_model* m) { if (m_quantifiers.empty()) return; ptr_vector qs; @@ -3325,8 +2442,8 @@ namespace smt { process_auf(qs, m); } - quantifier * model_finder::get_flat_quantifier(quantifier * q) { - quantifier_info * qinfo = get_quantifier_info(q); + quantifier* model_finder::get_flat_quantifier(quantifier* q) { + quantifier_info* qinfo = get_quantifier_info(q); return qinfo->get_flat_q(); } @@ -3335,19 +2452,19 @@ namespace smt { \remark q is the quantifier before flattening. */ - mf::instantiation_set const * model_finder::get_uvar_inst_set(quantifier * q, unsigned i) { - quantifier * flat_q = get_flat_quantifier(q); + mf::instantiation_set const* model_finder::get_uvar_inst_set(quantifier* q, unsigned i) { + quantifier* flat_q = get_flat_quantifier(q); SASSERT(flat_q->get_num_decls() >= q->get_num_decls()); - instantiation_set const * r = m_auf_solver->get_uvar_inst_set(flat_q, flat_q->get_num_decls() - q->get_num_decls() + i); - TRACE("model_finder", tout << "q: #" << q->get_id() << "\n" << mk_pp(q,m) << "\nflat_q: " << mk_pp(flat_q, m) - << "\ni: " << i << " " << flat_q->get_num_decls() - q->get_num_decls() + i << "\n";); + mf::instantiation_set const* r = m_auf_solver->get_uvar_inst_set(flat_q, flat_q->get_num_decls() - q->get_num_decls() + i); + TRACE("model_finder", tout << "q: #" << q->get_id() << "\n" << mk_pp(q, m) << "\nflat_q: " << mk_pp(flat_q, m) + << "\ni: " << i << " " << flat_q->get_num_decls() - q->get_num_decls() + i << "\n";); if (r != nullptr) return r; // quantifier was not processed by AUF solver... // it must have been satisfied by "macro"/"hint". - quantifier_info * qinfo = get_quantifier_info(q); + quantifier_info* qinfo = get_quantifier_info(q); SASSERT(qinfo); - return qinfo->get_macro_based_inst_set(i, m_context, *(m_auf_solver.get())); + return qinfo->get_macro_based_inst_set(i, m_context, *(m_auf_solver.get())); } /** @@ -3357,11 +2474,11 @@ namespace smt { Store in generation the generation of the result */ - expr * model_finder::get_inv(quantifier * q, unsigned i, expr * val, unsigned & generation) { - instantiation_set const * s = get_uvar_inst_set(q, i); + expr* model_finder::get_inv(quantifier* q, unsigned i, expr* val, unsigned& generation) { + instantiation_set const* s = get_uvar_inst_set(q, i); if (s == nullptr) return nullptr; - expr * t = s->get_inv(val); + expr* t = s->get_inv(val); if (t != nullptr) { generation = s->get_generation(t); } @@ -3376,28 +2493,28 @@ namespace smt { Return true if something was asserted. */ - bool model_finder::restrict_sks_to_inst_set(context * aux_ctx, quantifier * q, expr_ref_vector const & sks) { + bool model_finder::restrict_sks_to_inst_set(context* aux_ctx, quantifier* q, expr_ref_vector const& sks) { // Note: we currently add instances of q instead of flat_q. // If the user wants instances of flat_q, it should use PULL_NESTED_QUANTIFIERS=true. This option // will guarantee that q == flat_q. // // Since we only care about q (and its bindings), it only makes sense to restrict the variables of q. bool asserted_something = false; - unsigned num_decls = q->get_num_decls(); + unsigned num_decls = q->get_num_decls(); // Remark: sks were created for the flat version of q. SASSERT(get_flat_quantifier(q)->get_num_decls() == sks.size()); SASSERT(sks.size() >= num_decls); for (unsigned i = 0; i < num_decls; i++) { - expr * sk = sks.get(num_decls - i - 1); - instantiation_set const * s = get_uvar_inst_set(q, i); + expr* sk = sks.get(num_decls - i - 1); + instantiation_set const* s = get_uvar_inst_set(q, i); if (s == nullptr) continue; // nothing to do - obj_map const & inv = s->get_inv_map(); + obj_map const& inv = s->get_inv_map(); if (inv.empty()) continue; // nothing to do ptr_buffer eqs; for (auto const& kv : inv) { - expr * val = kv.m_key; + expr* val = kv.m_key; eqs.push_back(m.mk_eq(sk, val)); } expr_ref new_cnstr(m); @@ -3413,7 +2530,7 @@ namespace smt { unsigned sz = m_new_constraints.size(); if (sz > 0) { for (unsigned i = 0; i < sz; i++) { - expr * c = m_new_constraints.get(i); + expr* c = m_new_constraints.get(i); TRACE("model_finder_bug_detail", tout << "asserting new constraint: " << mk_pp(c, m) << "\n";); m_context->internalize(c, true); literal l(m_context->get_literal(c)); diff --git a/src/smt/smt_model_finder.h b/src/smt/smt_model_finder.h index bedbae79e..47fe10ab4 100644 --- a/src/smt/smt_model_finder.h +++ b/src/smt/smt_model_finder.h @@ -47,9 +47,12 @@ Revision History: #include "ast/ast.h" #include "ast/func_decl_dependencies.h" +#include "model/model_macro_solver.h" #include "smt/proto_model/proto_model.h" #include "tactic/tactic_exception.h" +class model_instantiation_set; + namespace smt { class context; @@ -59,17 +62,14 @@ namespace smt { class auf_solver; class simple_macro_solver; class hint_solver; - class non_auf_macro_solver; + class non_auf_macro_solver; class instantiation_set; }; - class model_finder { + class model_finder : public quantifier2macro_infos { typedef mf::quantifier_analyzer quantifier_analyzer; typedef mf::quantifier_info quantifier_info; typedef mf::auf_solver auf_solver; - typedef mf::simple_macro_solver simple_macro_solver; - typedef mf::hint_solver hint_solver; - typedef mf::non_auf_macro_solver non_auf_macro_solver; typedef mf::instantiation_set instantiation_set; ast_manager & m; @@ -79,9 +79,6 @@ namespace smt { obj_map m_q2info; ptr_vector m_quantifiers; func_decl_dependencies m_dependencies; - scoped_ptr m_sm_solver; - scoped_ptr m_hint_solver; - scoped_ptr m_nm_solver; struct scope { unsigned m_quantifiers_lim; @@ -105,7 +102,7 @@ namespace smt { public: model_finder(ast_manager & m); - ~model_finder(); + ~model_finder() override; void set_context(context * ctx); void register_quantifier(quantifier * q); @@ -122,6 +119,9 @@ namespace smt { void restart_eh(); void checkpoint(char const* component); + + quantifier_macro_info* operator()(quantifier* q); + }; }; diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 61ba1bff5..9f8e9c4b0 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -188,7 +188,7 @@ namespace smt { m_conversions.insert(e, res); m.inc_ref(e); m.inc_ref(res); - m_trail_stack.push(fpa2bv_conversion_trail_elem(m, m_conversions, e)); + m_trail_stack.push(insert_ref2_map(m, m_conversions, e, res.get())); } return res; diff --git a/src/smt/user_propagator.cpp b/src/smt/user_propagator.cpp index 22fa4e279..41e521952 100644 --- a/src/smt/user_propagator.cpp +++ b/src/smt/user_propagator.cpp @@ -78,6 +78,10 @@ void user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned num_lits, if (!m_fixed_eh) return; force_push(); + if (m_fixed.contains(v)) + return; + m_fixed.insert(v); + ctx.push_trail(insert_map(m_fixed, v)); m_id2justification.setx(v, literal_vector(num_lits, jlits), literal_vector()); m_fixed_eh(m_user_context, this, v, value); } diff --git a/src/smt/user_propagator.h b/src/smt/user_propagator.h index 544a9ed0e..e37dd751d 100644 --- a/src/smt/user_propagator.h +++ b/src/smt/user_propagator.h @@ -22,6 +22,7 @@ Notes: #pragma once +#include "util/uint_set.h" #include "smt/smt_theory.h" #include "solver/solver.h" @@ -57,6 +58,7 @@ namespace smt { solver::eq_eh_t m_diseq_eh; solver::context_obj* m_api_context { nullptr }; unsigned m_qhead { 0 }; + uint_set m_fixed; vector m_prop; unsigned_vector m_prop_lim; vector m_id2justification; diff --git a/src/util/trail.h b/src/util/trail.h index afe46f702..a2ce7a92a 100644 --- a/src/util/trail.h +++ b/src/util/trail.h @@ -192,6 +192,18 @@ public: virtual void undo(Ctx & ctx) { m_map.remove(m_obj); m.dec_ref(m_obj); } }; +template +class insert_ref2_map : public trail { + Mgr& m; + obj_map& m_map; + D* m_obj; + R* m_val; +public: + insert_ref2_map(Mgr& m, obj_map& t, D*o, R*r) : m(m), m_map(t), m_obj(o), m_val(r) {} + virtual ~insert_ref2_map() {} + virtual void undo(Ctx & ctx) { m_map.remove(m_obj); m.dec_ref(m_obj); m.dec_ref(m_val); } +}; + template class push_back_vector : public trail {