From 5a5e39ae74f6f22324a7b31fd99e96de11801d78 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 Oct 2024 12:18:09 -0700 Subject: [PATCH] fix incrementality bug for pre-processing: replay has to be invoked on every push regardless. --- src/ast/simplifiers/elim_unconstrained.cpp | 8 ++++---- .../simplifiers/model_reconstruction_trail.cpp | 15 +++++++++++++++ src/ast/simplifiers/model_reconstruction_trail.h | 12 ++---------- src/solver/simplifier_solver.cpp | 10 +++++----- 4 files changed, 26 insertions(+), 19 deletions(-) diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp index 818800d99..44b1ee091 100644 --- a/src/ast/simplifiers/elim_unconstrained.cpp +++ b/src/ast/simplifiers/elim_unconstrained.cpp @@ -80,7 +80,7 @@ void elim_unconstrained::eliminate() { continue; } expr* e = get_parent(v); - IF_VERBOSE(11, for (expr* p : n.m_parents) verbose_stream() << "parent " << mk_bounded_pp(p, m) << " @ " << get_node(p).m_refcount << "\n";); + TRACE("elim_unconstrained", for (expr* p : n.m_parents) verbose_stream() << "parent " << mk_bounded_pp(p, m) << " @ " << get_node(p).m_refcount << "\n";); if (!e || !is_app(e) || !is_ground(e)) { n.m_refcount = 0; continue; @@ -107,13 +107,13 @@ void elim_unconstrained::eliminate() { n.m_refcount = 0; m_args.shrink(sz); if (!inverted) { - IF_VERBOSE(11, verbose_stream() << "not inverted " << mk_bounded_pp(e, m) << "\n"); + TRACE("elim_unconstrained", tout << "not inverted " << mk_bounded_pp(e, m) << "\n"); continue; } - IF_VERBOSE(11, verbose_stream() << "replace " << mk_pp(t, m) << " / " << rr << " -> " << r << "\n"); + IF_VERBOSE(11, verbose_stream() << "replace " << mk_pp(t, m) << " : " << rr << " -> " << r << "\n"); - TRACE("elim_unconstrained", tout << mk_pp(t, m) << " / " << rr << " -> " << r << "\n"); + TRACE("elim_unconstrained", tout << mk_pp(t, m) << " : " << rr << " -> " << r << "\n"); SASSERT(r->get_sort() == t->get_sort()); m_stats.m_num_eliminated++; m_trail.push_back(r); diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp index 47ebea525..1f3c74ea2 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.cpp +++ b/src/ast/simplifiers/model_reconstruction_trail.cpp @@ -20,6 +20,19 @@ Author: #include "ast/converters/generic_model_converter.h" +void model_reconstruction_trail::add_vars(expr* e, ast_mark& free_vars) { + for (expr* t : subterms::all(expr_ref(e, m))) { + if (is_app(t) && is_uninterp(t)) { + func_decl* f = to_app(t)->get_decl(); + TRACE("simplifier", tout << "add var " << f->get_name() << "\n"); + free_vars.mark(f, true); + if (m_model_vars.is_marked(f)) + m_intersects_with_model = true; + } + } +} + + // accumulate a set of dependent exprs, updating m_trail to exclude loose // substitutions that use variables from the dependent expressions. @@ -27,6 +40,8 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt if (m_trail.empty()) return; + if (qhead == st.qtail()) + return; ast_mark free_vars; m_intersects_with_model = false; diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h index c2d8b0001..4c064124a 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.h +++ b/src/ast/simplifiers/model_reconstruction_trail.h @@ -101,6 +101,7 @@ class model_reconstruction_trail { */ void add_model_var(func_decl* f) { if (!m_model_vars.is_marked(f)) { + verbose_stream() << "add model var " << f->get_name() << "\n"; m_model_vars_trail.push_back(f); m_model_vars.mark(f, true); m_trail_stack.push(undo_model_var(*this)); @@ -112,16 +113,7 @@ class model_reconstruction_trail { * record if there is an intersection with the model_vars that are * registered when updates are added to the trail. */ - void add_vars(expr* e, ast_mark& free_vars) { - for (expr* t : subterms::all(expr_ref(e, m))) - if (is_app(t) && is_uninterp(t)) { - func_decl* f = to_app(t)->get_decl(); - TRACE("simplifier", tout << "add var " << f->get_name() << "\n"); - free_vars.mark(f, true); - if (m_model_vars.is_marked(f)) - m_intersects_with_model = true; - } - } + void add_vars(expr* e, ast_mark& free_vars); void add_vars(dependent_expr const& d, ast_mark& free_vars) { add_vars(d.fml(), free_vars); diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp index ae1d6b8a2..b114f364f 100644 --- a/src/solver/simplifier_solver.cpp +++ b/src/solver/simplifier_solver.cpp @@ -130,6 +130,10 @@ class simplifier_solver : public solver { unsigned qhead = m_preprocess_state.qhead(); expr_ref_vector orig_assumptions(assumptions); m_core_replace.reset(); + m_preprocess_state.replay(qhead, assumptions); + for (unsigned i = 0; i < assumptions.size(); ++i) + m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i)); + if (qhead < m_fmls.size()) { m_preprocess.reduce(); if (!m.inc()) @@ -138,11 +142,7 @@ class simplifier_solver : public solver { m_preprocess_state.display(tout)); m_preprocess_state.advance_qhead(); } - if (!assumptions.empty()) { - m_preprocess_state.replay(m_preprocess_state.qhead(), assumptions); - for (unsigned i = 0; i < assumptions.size(); ++i) - m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i)); - } + m_mc = m_preprocess_state.model_trail().get_model_converter(); m_cached_mc = nullptr; for (; qhead < m_fmls.size(); ++qhead)