fix incrementality bug for pre-processing: replay has to be invoked on every push regardless.

Author: NikolajBjorner

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);

src/ast/simplifiers/model_reconstruction_trail.cpp

@@ -20,13 +20,28 @@ Module Name:
 #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.
 
 void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumptions, dependent_expr_state& st) {
 
     if (m_trail.empty())
         return;
+    if (qhead == st.qtail())
+        return;
 
     ast_mark free_vars;
     m_intersects_with_model = false;

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);

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)