diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index c488a6269..9d894627a 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -3,6 +3,7 @@ z3_add_component(simplifiers bit_blaster.cpp bv_slice.cpp card2bv.cpp + dependent_expr_state.cpp elim_unconstrained.cpp eliminate_predicates.cpp euf_completion.cpp diff --git a/src/ast/simplifiers/bit_blaster.cpp b/src/ast/simplifiers/bit_blaster.cpp index dc086c628..72ee19eca 100644 --- a/src/ast/simplifiers/bit_blaster.cpp +++ b/src/ast/simplifiers/bit_blaster.cpp @@ -37,7 +37,7 @@ void bit_blaster::reduce() { expr_ref new_curr(m); proof_ref new_pr(m); bool change = false; - for (unsigned idx = m_fmls.qhead(); idx < m_fmls.size(); idx++) { + for (unsigned idx = qhead(); idx < qtail(); idx++) { if (m_fmls.inconsistent()) break; auto [curr, d] = m_fmls[idx](); diff --git a/src/ast/simplifiers/bv_slice.cpp b/src/ast/simplifiers/bv_slice.cpp index 14d6edb99..cc8b4fd85 100644 --- a/src/ast/simplifiers/bv_slice.cpp +++ b/src/ast/simplifiers/bv_slice.cpp @@ -27,7 +27,7 @@ namespace bv { } void slice::process_eqs() { - for (unsigned i = m_fmls.qhead(); i < m_fmls.size(); ++i) { + for (unsigned i = qhead(); i < qtail(); ++i) { auto const [f, d] = m_fmls[i](); process_eq(f); } @@ -136,7 +136,7 @@ namespace bv { expr_ref_vector cache(m), pin(m); ptr_vector todo, args; expr* c; - for (unsigned i = m_fmls.qhead(); i < m_fmls.size(); ++i) { + for (unsigned i = qhead(); i < qtail(); ++i) { auto const [f, d] = m_fmls[i](); todo.push_back(f); pin.push_back(f); diff --git a/src/ast/simplifiers/card2bv.cpp b/src/ast/simplifiers/card2bv.cpp index 3feb86474..d20b4a6c5 100644 --- a/src/ast/simplifiers/card2bv.cpp +++ b/src/ast/simplifiers/card2bv.cpp @@ -29,7 +29,7 @@ void card2bv::reduce() { expr_ref new_f1(m), new_f2(m); proof_ref new_pr(m); - for (unsigned idx = m_fmls.qhead(); !m_fmls.inconsistent() && idx < m_fmls.size(); idx++) { + for (unsigned idx = qhead(); !m_fmls.inconsistent() && idx < qtail(); idx++) { auto [f, d] = m_fmls[idx](); rw1(f, new_f1); rw2(false, new_f1, new_f2, new_pr); diff --git a/src/ast/simplifiers/dependent_expr_state.cpp b/src/ast/simplifiers/dependent_expr_state.cpp new file mode 100644 index 000000000..5219d25da --- /dev/null +++ b/src/ast/simplifiers/dependent_expr_state.cpp @@ -0,0 +1,109 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + dependent_expr_state.cpp + +Author: + + Nikolaj Bjorner (nbjorner) 2022-11-2. + +--*/ + +#include "ast/simplifiers/dependent_expr_state.h" +#include "ast/recfun_decl_plugin.h" +#include "ast/for_each_ast.h" + +unsigned dependent_expr_state::num_exprs() { + expr_fast_mark1 visited; + unsigned r = 0; + for (unsigned i = 0; i < qtail(); i++) + r += get_num_exprs((*this)[i].fml(), visited); + return r; +} + +void dependent_expr_state::freeze(func_decl* f) { + if (m_frozen.is_marked(f)) + return; + m_frozen_trail.push_back(f); + m_frozen.mark(f, true); +} + +void dependent_expr_state::freeze(expr* term) { + if (is_app(term)) + freeze(to_app(term)->get_decl()); +} + +/** +* Freeze functions appearing as sub-expressions of 'e'. +* The only_as_array flag indicates whether to only freeze occurrences of as-array +* from elimination. +*/ +void dependent_expr_state::freeze_terms(expr* e, bool only_as_array, ast_mark& visited) { + auto& m = m_frozen_trail.get_manager(); + struct proc { + bool only_as_array; + array_util a; + dependent_expr_state& st; + proc(ast_manager& m, bool o, dependent_expr_state& d) : + only_as_array(o), a(m), st(d) {} + void operator()(func_decl* f) { + if (!only_as_array) + st.freeze(f); + if (a.is_as_array(f, f) && is_uninterp(f)) + st.freeze(f); + } + void operator()(ast* s) {} + }; + proc proc(m, only_as_array, *this); + for_each_ast(proc, visited, e); +} + +/** +* Freeze all functions used in recursive definitions +*/ + +void dependent_expr_state::freeze_recfun() { + if (m_recfun_frozen) + return; + m_recfun_frozen = true; + auto& m = m_frozen_trail.get_manager(); + recfun::util rec(m); + ast_mark visited; + for (func_decl* f : rec.get_rec_funs()) + freeze_terms(rec.get_def(f).get_rhs(), false, visited); +} + +/** +* The current qhead is to be updated to qtail. +* Before this update, freeze all functions appearing in formulas. +*/ +void dependent_expr_state::freeze_prefix() { + ast_mark visited; + for (unsigned i = qhead(); i < qtail(); ++i) + freeze_terms((*this)[i].fml(), false, visited); +} + +/** +* Freeze functions in the unprocessed suffix that appear in dependencies and in as-array. +*/ +void dependent_expr_state::freeze_suffix() { + if (m_suffix_frozen) + return; + m_suffix_frozen = true; + auto& m = m_frozen_trail.get_manager(); + freeze_recfun(); + ast_mark visited; + ptr_vector es; + for (unsigned i = qhead(); i < qtail(); ++i) { + auto d = (*this)[i]; + if (d.dep()) { + es.reset(); + m.linearize(d.dep(), es); + for (expr* e : es) + freeze_terms(e, false, visited); + } + freeze_terms(d.fml(), true, visited); + } +} diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h index a65492a58..4c9b21f0a 100644 --- a/src/ast/simplifiers/dependent_expr_state.h +++ b/src/ast/simplifiers/dependent_expr_state.h @@ -42,27 +42,54 @@ Author: */ class dependent_expr_state { unsigned m_qhead = 0; + bool m_suffix_frozen = false; + bool m_recfun_frozen = false; + ast_mark m_frozen; + func_decl_ref_vector m_frozen_trail; + void freeze_prefix(); + void freeze_recfun(); + void freeze_terms(expr* term, bool only_as_array, ast_mark& visited); + void freeze(expr* term); + void freeze(func_decl* f); + struct thaw : public trail { + unsigned sz; + dependent_expr_state& st; + thaw(dependent_expr_state& st) : sz(st.m_frozen_trail.size()), st(st) {} + void undo() override { + for (unsigned i = st.m_frozen_trail.size(); i-- > sz; ) + st.m_frozen.mark(st.m_frozen_trail.get(i), false); + st.m_frozen_trail.shrink(sz); + } + }; public: + dependent_expr_state(ast_manager& m) : m_frozen_trail(m) {} virtual ~dependent_expr_state() {} - virtual unsigned size() const = 0; + unsigned qhead() const { return m_qhead; } + virtual unsigned qtail() const = 0; virtual dependent_expr const& operator[](unsigned i) = 0; virtual void update(unsigned i, dependent_expr const& j) = 0; virtual void add(dependent_expr const& j) = 0; virtual bool inconsistent() = 0; virtual model_reconstruction_trail& model_trail() = 0; + virtual void flatten_suffix() {} trail_stack m_trail; - void push() { m_trail.push_scope(); } - void pop(unsigned n) { m_trail.pop_scope(n); } - unsigned qhead() const { return m_qhead; } - void advance_qhead() { if (m_trail.get_num_scopes() > 0) m_trail.push(value_trail(m_qhead)); m_qhead = size(); } - unsigned num_exprs() { - expr_fast_mark1 visited; - unsigned r = 0; - for (unsigned i = 0; i < size(); i++) - r += get_num_exprs((*this)[i].fml(), visited); - return r; + void push() { + m_trail.push_scope(); + m_trail.push(value_trail(m_qhead)); + m_trail.push(thaw(*this)); } + void pop(unsigned n) { m_trail.pop_scope(n); } + + void advance_qhead() { freeze_prefix(); m_suffix_frozen = false; m_qhead = qtail(); } + unsigned num_exprs(); + + /** + * Freeze internal functions + */ + bool frozen(func_decl* f) const { return m_frozen.is_marked(f); } + bool frozen(expr* f) const { return is_app(f) && m_frozen.is_marked(to_app(f)->get_decl()); } + void freeze_suffix(); }; /** @@ -76,6 +103,9 @@ protected: unsigned num_scopes() const { return m_trail.get_num_scopes(); } + unsigned qhead() const { return m_fmls.qhead(); } + unsigned qtail() const { return m_fmls.qtail(); } + public: dependent_expr_simplifier(ast_manager& m, dependent_expr_state& s) : m(m), m_fmls(s), m_trail(s.m_trail) {} virtual ~dependent_expr_simplifier() {} diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp index 93a84dba6..41305b745 100644 --- a/src/ast/simplifiers/elim_unconstrained.cpp +++ b/src/ast/simplifiers/elim_unconstrained.cpp @@ -48,7 +48,7 @@ Author: elim_unconstrained::elim_unconstrained(ast_manager& m, dependent_expr_state& fmls) : dependent_expr_simplifier(m, fmls), m_inverter(m), m_lt(*this), m_heap(1024, m_lt), m_trail(m) { std::function is_var = [&](expr* e) { - return is_uninterp_const(e) && !m_frozen.is_marked(e) && get_node(e).m_refcount <= 1; + return is_uninterp_const(e) && !m_fmls.frozen(e) && get_node(e).m_refcount <= 1; }; m_inverter.set_is_var(is_var); } @@ -121,12 +121,14 @@ expr* elim_unconstrained::get_parent(unsigned n) const { * initialize node structure */ void elim_unconstrained::init_nodes() { + + m_fmls.freeze_suffix(); + expr_ref_vector terms(m); - for (unsigned i = 0; i < m_fmls.size(); ++i) + for (unsigned i = qhead(); i < qtail(); ++i) terms.push_back(m_fmls[i].fml()); m_trail.append(terms); m_heap.reset(); - m_frozen.reset(); m_root.reset(); // initialize nodes for terms in the original goal @@ -135,23 +137,6 @@ void elim_unconstrained::init_nodes() { // top-level terms have reference count > 0 for (expr* e : terms) inc_ref(e); - - // freeze subterms before the already processed head - terms.reset(); - for (unsigned i = 0; i < m_fmls.qhead(); ++i) - terms.push_back(m_fmls[i].fml()); - for (expr* e : subterms::all(terms)) - m_frozen.mark(e, true); - - // freeze subterms that occur with recursive function definitions - recfun::util rec(m); - if (rec.has_rec_defs()) { - for (func_decl* f : rec.get_rec_funs()) { - expr* rhs = rec.get_def(f).get_rhs(); - for (expr* t : subterms::all(expr_ref(rhs, m))) - m_frozen.mark(t); - } - } } /** @@ -216,7 +201,7 @@ void elim_unconstrained::gc(expr* t) { */ void elim_unconstrained::reconstruct_terms() { expr_ref_vector terms(m); - for (unsigned i = m_fmls.qhead(); i < m_fmls.size(); ++i) + for (unsigned i = qhead(); i < qtail(); ++i) terms.push_back(m_fmls[i].fml()); for (expr* e : subterms_postorder::all(terms)) { @@ -249,8 +234,8 @@ void elim_unconstrained::reconstruct_terms() { void elim_unconstrained::assert_normalized(vector& old_fmls) { - unsigned sz = m_fmls.size(); - for (unsigned i = m_fmls.qhead(); i < sz; ++i) { + unsigned sz = qtail(); + for (unsigned i = qhead(); i < sz; ++i) { auto [f, d] = m_fmls[i](); node& n = get_node(f); expr* g = n.m_term; diff --git a/src/ast/simplifiers/elim_unconstrained.h b/src/ast/simplifiers/elim_unconstrained.h index b66d0b727..9da0f3fc2 100644 --- a/src/ast/simplifiers/elim_unconstrained.h +++ b/src/ast/simplifiers/elim_unconstrained.h @@ -45,7 +45,6 @@ class elim_unconstrained : public dependent_expr_simplifier { heap m_heap; expr_ref_vector m_trail; ptr_vector m_args; - expr_mark m_frozen; stats m_stats; unsigned_vector m_root; diff --git a/src/ast/simplifiers/eliminate_predicates.cpp b/src/ast/simplifiers/eliminate_predicates.cpp index fa615048f..d71d2180a 100644 --- a/src/ast/simplifiers/eliminate_predicates.cpp +++ b/src/ast/simplifiers/eliminate_predicates.cpp @@ -109,7 +109,7 @@ bool eliminate_predicates::can_be_macro_head(expr* _head, unsigned num_bound) { return false; app* head = to_app(_head); func_decl* f = head->get_decl(); - if (m_disable_macro.is_marked(f)) + if (m_fmls.frozen(f)) return false; if (m_is_macro.is_marked(f)) return false; @@ -157,7 +157,7 @@ expr_ref eliminate_predicates::bind_free_variables_in_def(clause& cl, app* head, * (or (not (head x)) (def x)) */ bool eliminate_predicates::try_find_binary_definition(func_decl* p, app_ref& head, expr_ref& def, expr_dependency_ref& dep) { - if (m_disable_macro.is_marked(p)) + if (m_fmls.frozen(p)) return false; expr_mark binary_pos, binary_neg; obj_map deps; @@ -501,7 +501,7 @@ void eliminate_predicates::reduce_definitions() { for (auto const& [k, v] : m_macros) macro_expander.insert(v->m_head, v->m_def, v->m_dep); - for (unsigned i = m_fmls.qhead(); i < m_fmls.size(); ++i) { + for (unsigned i = qhead(); i < qtail(); ++i) { auto [f, d] = m_fmls[i](); expr_ref fml(f, m), new_fml(m); expr_dependency_ref dep(m); @@ -524,7 +524,7 @@ void eliminate_predicates::reduce_definitions() { void eliminate_predicates::try_resolve(func_decl* p) { if (m_disable_elimination.is_marked(p)) return; - if (m_disable_macro.is_marked(p)) + if (m_fmls.frozen(p)) return; unsigned num_pos = 0, num_neg = 0; @@ -717,30 +717,20 @@ void eliminate_predicates::try_resolve() { /** * Process the terms m_to_exclude, walk all subterms. * Uninterpreted function declarations in these terms are added to 'exclude_set' -* Uninterpreted function declarations from as-array terms are added to 'm_disable_macro' */ void eliminate_predicates::process_to_exclude(ast_mark& exclude_set) { ast_mark visited; - array_util a(m); - struct proc { - array_util& a; ast_mark& to_exclude; - ast_mark& to_disable; - proc(array_util& a, ast_mark& f, ast_mark& d) : - a(a), to_exclude(f), to_disable(d) {} + proc(ast_mark& f) : + to_exclude(f) {} void operator()(func_decl* f) { if (is_uninterp(f)) to_exclude.mark(f, true); } - void operator()(app* e) { - func_decl* f; - if (a.is_as_array(e, f) && is_uninterp(f)) - to_disable.mark(f, true); - } void operator()(ast* s) {} }; - proc proc(a, exclude_set, m_disable_macro); + proc proc(exclude_set); for (expr* e : m_to_exclude) for_each_ast(proc, visited, e); @@ -779,16 +769,10 @@ eliminate_predicates::clause* eliminate_predicates::init_clause(expr* f, expr_de * eliminations. */ void eliminate_predicates::init_clauses() { - for (unsigned i = 0; i < m_fmls.qhead(); ++i) - m_to_exclude.push_back(m_fmls[i].fml()); - recfun::util rec(m); - if (rec.has_rec_defs()) - for (auto& d : rec.get_rec_funs()) - m_to_exclude.push_back(rec.get_def(d).get_rhs()); - - process_to_exclude(m_disable_macro); - for (unsigned i = m_fmls.qhead(); i < m_fmls.size(); ++i) { + m_fmls.freeze_suffix(); + + for (unsigned i = qhead(); i < qtail(); ++i) { clause* cl = init_clause(i); add_use_list(*cl); m_clauses.push_back(cl); @@ -821,7 +805,6 @@ void eliminate_predicates::reset() { m_predicates.reset(); m_predicate_decls.reset(); m_to_exclude.reset(); - m_disable_macro.reset(); m_disable_elimination.reset(); m_is_macro.reset(); for (auto const& [k, v] : m_macros) diff --git a/src/ast/simplifiers/eliminate_predicates.h b/src/ast/simplifiers/eliminate_predicates.h index ca4110e99..a8d4fff48 100644 --- a/src/ast/simplifiers/eliminate_predicates.h +++ b/src/ast/simplifiers/eliminate_predicates.h @@ -88,7 +88,7 @@ private: }; scoped_ptr_vector m_clauses; - ast_mark m_disable_elimination, m_disable_macro, m_predicate_decls, m_is_macro; + ast_mark m_disable_elimination, m_predicate_decls, m_is_macro; ptr_vector m_predicates; ptr_vector m_to_exclude; stats m_stats; diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp index f077f1918..78be41c1a 100644 --- a/src/ast/simplifiers/euf_completion.cpp +++ b/src/ast/simplifiers/euf_completion.cpp @@ -74,13 +74,13 @@ namespace euf { void completion::add_egraph() { m_nodes_to_canonize.reset(); - unsigned sz = m_fmls.size(); + unsigned sz = qtail(); auto add_children = [&](enode* n) { for (auto* ch : enode_args(n)) m_nodes_to_canonize.push_back(ch); }; - for (unsigned i = m_fmls.qhead(); i < sz; ++i) { + for (unsigned i = qhead(); i < sz; ++i) { expr* x, * y; auto [f, d] = m_fmls[i](); if (m.is_eq(f, x, y)) { @@ -113,8 +113,8 @@ namespace euf { return; } - unsigned sz = m_fmls.size(); - for (unsigned i = m_fmls.qhead(); i < sz; ++i) { + unsigned sz = qtail(); + for (unsigned i = qhead(); i < sz; ++i) { auto [f, d] = m_fmls[i](); expr_dependency_ref dep(d, m); diff --git a/src/ast/simplifiers/extract_eqs.cpp b/src/ast/simplifiers/extract_eqs.cpp index d65f9b167..fdb889ee3 100644 --- a/src/ast/simplifiers/extract_eqs.cpp +++ b/src/ast/simplifiers/extract_eqs.cpp @@ -258,7 +258,7 @@ namespace euf { if (!m_enabled) return; m_nonzero.reset(); - for (unsigned i = 0; i < fmls.size(); ++i) + for (unsigned i = 0; i < fmls.qtail(); ++i) add_pos(fmls[i].fml()); } diff --git a/src/ast/simplifiers/max_bv_sharing.cpp b/src/ast/simplifiers/max_bv_sharing.cpp index 4744c473c..3ac27302a 100644 --- a/src/ast/simplifiers/max_bv_sharing.cpp +++ b/src/ast/simplifiers/max_bv_sharing.cpp @@ -255,7 +255,7 @@ public: void reduce() override { expr_ref new_curr(m); proof_ref new_pr(m); - for (unsigned idx = m_fmls.qhead(); idx < m_fmls.size() && !m_fmls.inconsistent(); idx++) { + for (unsigned idx = qhead(); idx < qtail() && !m_fmls.inconsistent(); idx++) { auto [curr, d] = m_fmls[idx](); m_rw(curr, new_curr, new_pr); // Proof reconstruction: new_pr = m.mk_modus_ponens(old_pr, new_pr); diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp index 19c7d9381..18af7449f 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.cpp +++ b/src/ast/simplifiers/model_reconstruction_trail.cpp @@ -26,7 +26,7 @@ Author: void model_reconstruction_trail::replay(unsigned qhead, dependent_expr_state& st) { ast_mark free_vars; scoped_ptr rp = mk_default_expr_replacer(m, false); - for (unsigned i = qhead; i < st.size(); ++i) + for (unsigned i = qhead; i < st.qtail(); ++i) add_vars(st[i], free_vars); for (auto& t : m_trail) { @@ -64,7 +64,7 @@ void model_reconstruction_trail::replay(unsigned qhead, dependent_expr_state& st dependent_expr de(m, t->m_def, t->m_dep); add_vars(de, free_vars); - for (unsigned i = qhead; i < st.size(); ++i) { + for (unsigned i = qhead; i < st.qtail(); ++i) { auto [f, dep1] = st[i](); expr_ref g(m); expr_dependency_ref dep2(m); @@ -77,7 +77,7 @@ void model_reconstruction_trail::replay(unsigned qhead, dependent_expr_state& st rp->set_substitution(t->m_subst.get()); // rigid entries: // apply substitution to added in case of rigid model convertions - for (unsigned i = qhead; i < st.size(); ++i) { + for (unsigned i = qhead; i < st.qtail(); ++i) { auto [f, dep1] = st[i](); auto [g, dep2] = rp->replace_with_dep(f); dependent_expr d(m, g, m.mk_join(dep1, dep2)); diff --git a/src/ast/simplifiers/propagate_values.cpp b/src/ast/simplifiers/propagate_values.cpp index 2572cc310..928e8a787 100644 --- a/src/ast/simplifiers/propagate_values.cpp +++ b/src/ast/simplifiers/propagate_values.cpp @@ -41,7 +41,7 @@ void propagate_values::reduce() { auto add_shared = [&]() { shared_occs_mark visited; shared.reset(); - for (unsigned i = 0; i < m_fmls.size(); ++i) + for (unsigned i = 0; i < qtail(); ++i) shared(m_fmls[i].fml(), visited); }; @@ -78,7 +78,7 @@ void propagate_values::reduce() { subst.reset(); m_rewriter.reset(); m_rewriter.set_substitution(&subst); - for (unsigned i = 0; i < m_fmls.qhead(); ++i) + for (unsigned i = 0; i < qhead(); ++i) add_sub(m_fmls[i]); }; @@ -86,10 +86,10 @@ void propagate_values::reduce() { for (unsigned r = 0; r < m_max_rounds && rw != m_stats.m_num_rewrites; ++r) { rw = m_stats.m_num_rewrites; init_sub(); - for (unsigned i = m_fmls.qhead(); i < m_fmls.size() && !m_fmls.inconsistent(); ++i) + for (unsigned i = qhead(); i < qtail() && !m_fmls.inconsistent(); ++i) process_fml(i); init_sub(); - for (unsigned i = m_fmls.size(); i-- > m_fmls.qhead() && !m_fmls.inconsistent();) + for (unsigned i = qtail(); i-- > qhead() && !m_fmls.inconsistent();) process_fml(i); if (subst.empty()) break; diff --git a/src/ast/simplifiers/rewriter_simplifier.h b/src/ast/simplifiers/rewriter_simplifier.h index f956ec808..bb9fd0d22 100644 --- a/src/ast/simplifiers/rewriter_simplifier.h +++ b/src/ast/simplifiers/rewriter_simplifier.h @@ -40,7 +40,7 @@ public: m_num_steps = 0; expr_ref new_curr(m); proof_ref new_pr(m); - for (unsigned idx = m_fmls.qhead(); idx < m_fmls.size(); idx++) { + for (unsigned idx = qhead(); idx < qtail(); idx++) { if (m_fmls.inconsistent()) break; auto d = m_fmls[idx]; diff --git a/src/ast/simplifiers/seq_simplifier.h b/src/ast/simplifiers/seq_simplifier.h index 0fa5990dd..326b3d09e 100644 --- a/src/ast/simplifiers/seq_simplifier.h +++ b/src/ast/simplifiers/seq_simplifier.h @@ -70,6 +70,7 @@ public: break; collect_stats _cs(*s); s->reduce(); + m_fmls.flatten_suffix(); } } diff --git a/src/ast/simplifiers/solve_context_eqs.cpp b/src/ast/simplifiers/solve_context_eqs.cpp index 7eaa8ad2f..e87381825 100644 --- a/src/ast/simplifiers/solve_context_eqs.cpp +++ b/src/ast/simplifiers/solve_context_eqs.cpp @@ -42,7 +42,7 @@ namespace euf { bool solve_context_eqs::is_safe_eq(expr* e) { m_and_pos.reset(); m_and_neg.reset(); m_or_pos.reset(); m_or_neg.reset(); - for (unsigned i = 0; i < m_fmls.size(); ++i) + for (unsigned i = 0; i < m_fmls.qtail(); ++i) if (!is_safe_eq(m_fmls[i].fml(), e)) return false; return true; @@ -147,7 +147,7 @@ namespace euf { void solve_context_eqs::collect_nested_equalities(dep_eq_vector& eqs) { expr_mark visited; - unsigned sz = m_fmls.size(); + unsigned sz = m_fmls.qtail(); for (unsigned i = m_fmls.qhead(); i < sz; ++i) collect_nested_equalities(m_fmls[i], visited, eqs); diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp index f6055af50..e2fbc0c9a 100644 --- a/src/ast/simplifiers/solve_eqs.cpp +++ b/src/ast/simplifiers/solve_eqs.cpp @@ -34,7 +34,7 @@ namespace euf { void solve_eqs::get_eqs(dep_eq_vector& eqs) { for (extract_eq* ex : m_extract_plugins) - for (unsigned i = m_fmls.qhead(); i < m_fmls.size(); ++i) + for (unsigned i = qhead(); i < qtail(); ++i) ex->get_eqs(m_fmls[i], eqs); } @@ -187,7 +187,7 @@ namespace euf { scoped_ptr rp = mk_default_expr_replacer(m, false); rp->set_substitution(m_subst.get()); - for (unsigned i = m_fmls.qhead(); i < m_fmls.size() && !m_fmls.inconsistent(); ++i) { + for (unsigned i = qhead(); i < qtail() && !m_fmls.inconsistent(); ++i) { auto [f, d] = m_fmls[i](); auto [new_f, new_dep] = rp->replace_with_dep(f); m_rewriter(new_f); diff --git a/src/sat/sat_solver/sat_smt_solver.cpp b/src/sat/sat_solver/sat_smt_solver.cpp index 91a2bfec2..69cc7ed17 100644 --- a/src/sat/sat_solver/sat_smt_solver.cpp +++ b/src/sat/sat_solver/sat_smt_solver.cpp @@ -17,9 +17,6 @@ Author: Notes: - - proper handling of dependencies + pre-processing - - literals used in dependencies should not be eliminated by pre-processing routines - This has to be enforced. - add translation for preprocess state. - If the pre-processors are stateful, they need to be properly translated. - add back get_consequences, maybe or just have them handled by inc_sat_solver @@ -55,9 +52,9 @@ class sat_smt_solver : public solver { struct dep_expr_state : public dependent_expr_state { sat_smt_solver& s; model_reconstruction_trail m_reconstruction_trail; - dep_expr_state(sat_smt_solver& s):s(s), m_reconstruction_trail(s.m, m_trail) {} + dep_expr_state(sat_smt_solver& s):dependent_expr_state(s.m), s(s), m_reconstruction_trail(s.m, m_trail) {} ~dep_expr_state() override {} - virtual unsigned size() const override { return s.m_fmls.size(); } + virtual unsigned qtail() const override { return s.m_fmls.size(); } dependent_expr const& operator[](unsigned i) override { return s.m_fmls[i]; } void update(unsigned i, dependent_expr const& j) override { s.m_fmls[i] = j; } void add(dependent_expr const& j) override { s.m_fmls.push_back(j); } @@ -65,6 +62,28 @@ class sat_smt_solver : public solver { model_reconstruction_trail& model_trail() override { return m_reconstruction_trail; } void append(generic_model_converter& mc) { model_trail().append(mc); } void replay(unsigned qhead) { m_reconstruction_trail.replay(qhead, *this); } + void flatten_suffix() override { + expr_mark seen; + unsigned j = qhead(); + for (unsigned i = qhead(); i < qtail(); ++i) { + expr* f = s.m_fmls[i].fml(); + if (seen.is_marked(f)) + continue; + seen.mark(f, true); + if (s.m.is_true(f)) + continue; + if (s.m.is_and(f)) { + auto* d = s.m_fmls[i].dep(); + for (expr* arg : *to_app(f)) + s.m_fmls.push_back(dependent_expr(s.m, arg, d)); + continue; + } + if (i != j) + s.m_fmls[j] = s.m_fmls[i]; + ++j; + } + s.m_fmls.shrink(j); + } }; struct dependency2assumptions { @@ -253,7 +272,6 @@ public: } void push_internal() { - m_trail.push_scope(); m_solver.user_push(); m_goal2sat.user_push(); m_map.push(); @@ -272,7 +290,6 @@ public: m_map.pop(n); m_goal2sat.user_pop(n); m_solver.user_pop(n); - m_trail.pop_scope(n); m_mc->shrink(m_mc_size); } diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h index dda114c24..3afc0fc9f 100644 --- a/src/tactic/dependent_expr_state_tactic.h +++ b/src/tactic/dependent_expr_state_tactic.h @@ -42,6 +42,7 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state { public: dependent_expr_state_tactic(ast_manager& m, params_ref const& p, dependent_expr_simplifier_factory* f): + dependent_expr_state(m), m(m), m_params(p), m_factory(f), @@ -52,7 +53,7 @@ public: /** * size(), [](), update() and inconsisent() implement the abstract interface of dependent_expr_state */ - unsigned size() const override { return m_goal->size(); } + unsigned qtail() const override { return m_goal->size(); } dependent_expr const& operator[](unsigned i) override { m_dep = dependent_expr(m, m_goal->form(i), m_goal->dep(i)); @@ -60,11 +61,15 @@ public: } void update(unsigned i, dependent_expr const& j) override { + if (inconsistent()) + return; auto [f, d] = j(); m_goal->update(i, f, nullptr, d); } void add(dependent_expr const& j) override { + if (inconsistent()) + return; auto [f, d] = j(); m_goal->assert_expr(f, nullptr, d); }