add incremental version of value propagate

src/ast/simplifiers/CMakeLists.txt

@@ -6,6 +6,7 @@ z3_add_component(simplifiers
     euf_completion.cpp
     extract_eqs.cpp
     model_reconstruction_trail.cpp
+    propagate_values.cpp
     solve_context_eqs.cpp
     solve_eqs.cpp
   COMPONENT_DEPENDENCIES

src/ast/simplifiers/euf_completion.cpp

@@ -61,10 +61,6 @@ namespace euf {
     }
 
     void completion::reduce() {
-
-        propagate_values();
-        if (m_fmls.inconsistent())
-            return;
         m_has_new_eq = true;
         for (unsigned rounds = 0; m_has_new_eq && rounds <= 3 && !m_fmls.inconsistent(); ++rounds) {
             ++m_epoch;
@@ -76,81 +72,6 @@ namespace euf {
         }
     }
 
-    /**
-    * Propagate writes into values first. It is cheaper to propagate values directly than using
-    * the E-graph. The E-graph suffers from the following overhead: it prefers interpreted nodes
-    * as roots and therefore the "merge" function ignores the heuristic of choosing the node to appoint root
-    * as the one with the fewest parents. Merging a constant value with multiple terms then has a compounding
-    * quadratic time overhead since the parents of the value are removed and re-inserted into the congruence
-    * table repeatedly and with growing size (exceeding the n*log(n) overhead when choosing the root to 
-    * have the fewest parents).
-    */
-    void completion::propagate_values() {
-        shared_occs shared(m, true);
-        expr_substitution subst(m, true, false);
-        expr* x, * y;
-        expr_ref_buffer args(m);
-        auto add_shared = [&]() {
-            shared_occs_mark visited;
-            shared.reset();
-            for (unsigned i = 0; i < m_fmls.size(); ++i)
-                shared(m_fmls[i].fml(), visited);
-        };
-
-        auto add_sub = [&](dependent_expr const& de) {
-            auto const& [f, dep] = de();
-            if (m.is_not(f, x) && shared.is_shared(x))
-                subst.insert(x, m.mk_false(), dep);
-            else if (shared.is_shared(f))
-                subst.insert(f, m.mk_true(), dep);
-            if (m.is_eq(f, x, y) && m.is_value(x) && shared.is_shared(y))
-                subst.insert(y, x, dep);
-            else if (m.is_eq(f, x, y) && m.is_value(y) && shared.is_shared(x))
-                subst.insert(x, y, dep);
-        };
-
-        auto process_fml = [&](unsigned i) {
-            expr* f = m_fmls[i].fml();
-            expr_dependency* dep = m_fmls[i].dep();
-            expr_ref fml(m);
-            proof_ref pr(m);
-            m_rewriter(f, fml, pr);
-            if (fml != f) {
-                dep = m.mk_join(dep, m_rewriter.get_used_dependencies());
-                m_fmls.update(i, dependent_expr(m, fml, dep));
-                ++m_stats.m_num_rewrites;
-            }
-            m_rewriter.reset_used_dependencies();
-            add_sub(m_fmls[i]);
-        };
-
-        unsigned rw = m_stats.m_num_rewrites + 1;
-        for (unsigned r = 0; r < 4 && rw != m_stats.m_num_rewrites; ++r) {            
-            rw = m_stats.m_num_rewrites;
-            add_shared();
-            subst.reset();
-            m_rewriter.reset();
-            m_rewriter.set_substitution(&subst);
-            for (unsigned i = 0; i < m_qhead; ++i)
-                add_sub(m_fmls[i]);
-            for (unsigned i = m_qhead; i < m_fmls.size() && !m_fmls.inconsistent(); ++i)
-                process_fml(i);
-            add_shared();
-            subst.reset();
-            m_rewriter.reset();
-            m_rewriter.set_substitution(&subst);
-            for (unsigned i = 0; i < m_qhead; ++i)
-                add_sub(m_fmls[i]);
-            for (unsigned i = m_fmls.size(); i-- > m_qhead && !m_fmls.inconsistent();)
-                process_fml(i);
-            if (subst.empty())
-                break;
-        }
-
-        m_rewriter.set_substitution(nullptr);        
-        m_rewriter.reset();
-    }
-
     void completion::add_egraph() {
         m_nodes_to_canonize.reset();
         unsigned sz = m_fmls.size();

src/ast/simplifiers/euf_completion.h

@@ -46,7 +46,6 @@ namespace euf {
         bool is_new_eq(expr* a, expr* b);
         void update_has_new_eq(expr* g);
         expr_ref mk_and(expr* a, expr* b);
-        void propagate_values();
         void add_egraph();
         void map_canonical();
         void read_egraph();

src/ast/simplifiers/propagate_values.cpp

@@ -0,0 +1,115 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    propagate_values.h
+
+Abstract:
+
+    relatively cheap value propagation
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-24
+
+Notes:
+
+    Incremental version of propagate_values_tactic
+
+--*/
+
+#include "params/tactic_params.hpp"
+#include "ast/ast_pp.h"
+#include "ast/ast_util.h"
+#include "ast/shared_occs.h"
+#include "ast/simplifiers/propagate_values.h"
+
+propagate_values::propagate_values(ast_manager& m, dependent_expr_state& fmls):
+    dependent_expr_simplifier(m, fmls),
+    m_rewriter(m) {
+    m_rewriter.set_order_eq(true);
+    m_rewriter.set_flat_and_or(false);
+}
+
+void propagate_values::reduce() {
+    shared_occs shared(m, true);
+    expr_substitution subst(m, true, false);
+    expr* x, * y;
+    expr_ref_buffer args(m);
+    auto add_shared = [&]() {
+        shared_occs_mark visited;
+        shared.reset();
+        for (unsigned i = 0; i < m_fmls.size(); ++i)
+            shared(m_fmls[i].fml(), visited);
+    };
+
+    auto add_sub = [&](dependent_expr const& de) {
+        auto const& [f, dep] = de();
+        if (m.is_not(f, x) && shared.is_shared(x))
+            subst.insert(x, m.mk_false(), dep);
+        else if (shared.is_shared(f))
+            subst.insert(f, m.mk_true(), dep);
+        if (m.is_eq(f, x, y) && m.is_value(x) && shared.is_shared(y))
+            subst.insert(y, x, dep);
+        else if (m.is_eq(f, x, y) && m.is_value(y) && shared.is_shared(x))
+            subst.insert(x, y, dep);
+    };
+
+    auto process_fml = [&](unsigned i) {
+        expr* f = m_fmls[i].fml();
+        expr_dependency* dep = m_fmls[i].dep();
+        expr_ref fml(m);
+        proof_ref pr(m);
+        m_rewriter(f, fml, pr);
+        if (fml != f) {
+            dep = m.mk_join(dep, m_rewriter.get_used_dependencies());
+            m_fmls.update(i, dependent_expr(m, fml, dep));
+            ++m_stats.m_num_rewrites;
+        }
+        m_rewriter.reset_used_dependencies();
+        add_sub(m_fmls[i]);
+    };
+
+    unsigned rw = m_stats.m_num_rewrites + 1;
+    for (unsigned r = 0; r < m_max_rounds && rw != m_stats.m_num_rewrites; ++r) {            
+        rw = m_stats.m_num_rewrites;
+        add_shared();
+        subst.reset();
+        m_rewriter.reset();
+        m_rewriter.set_substitution(&subst);
+        for (unsigned i = 0; i < m_qhead; ++i)
+            add_sub(m_fmls[i]);
+        for (unsigned i = m_qhead; i < m_fmls.size() && !m_fmls.inconsistent(); ++i)
+            process_fml(i);
+        add_shared();
+        subst.reset();
+        m_rewriter.reset();
+        m_rewriter.set_substitution(&subst);
+        for (unsigned i = 0; i < m_qhead; ++i)
+            add_sub(m_fmls[i]);
+        for (unsigned i = m_fmls.size(); i-- > m_qhead && !m_fmls.inconsistent();)
+            process_fml(i);
+        if (subst.empty())
+            break;
+    }
+
+    m_rewriter.set_substitution(nullptr);        
+    m_rewriter.reset();
+
+    advance_qhead(m_fmls.size());
+}
+
+void propagate_values::collect_statistics(statistics& st) const {
+    st.update("propagate-values-rewrites", m_stats.m_num_rewrites);        
+}
+
+void propagate_values::updt_params(params_ref const& p) {
+    tactic_params tp(p);
+    m_max_rounds = p.get_uint("max_rounds", tp.propagate_values_max_rounds());
+}
+
+void propagate_values::collect_param_descrs(param_descrs& r) {
+    th_rewriter::get_param_descrs(r);
+    r.insert("max_rounds", CPK_UINT, "(default: 4) maximum number of rounds.");
+}

src/ast/simplifiers/propagate_values.h

@@ -0,0 +1,45 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    propagate_values.h
+
+Abstract:
+
+    relatively cheap value propagation
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-24
+
+Notes:
+    incremental version of propagate_values_tactic, to be replaced
+
+--*/
+
+#pragma once
+
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/rewriter/th_rewriter.h"
+
+
+class propagate_values : public dependent_expr_simplifier {
+
+    struct stats {
+        unsigned m_num_rewrites = 0;
+        void reset() { memset(this, 0, sizeof(*this)); }
+    };
+
+    th_rewriter            m_rewriter;
+    stats                  m_stats;
+    unsigned               m_max_rounds = 4;
+
+public:
+    propagate_values(ast_manager& m, dependent_expr_state& fmls);
+    void reduce() override;
+    void collect_statistics(statistics& st) const override;
+    void reset_statistics() override { m_stats.reset(); }
+    void updt_params(params_ref const& p) override;
+    void collect_param_descrs(param_descrs& r) override;
+};

src/tactic/core/CMakeLists.txt

@@ -45,6 +45,7 @@ z3_add_component(core_tactics
     occf_tactic.h
     pb_preprocess_tactic.h
     propagate_values_tactic.h
+    propagate_values2_tactic.h
     reduce_args_tactic.h
     simplify_tactic.h
     solve_eqs_tactic.h

src/tactic/core/elim_uncnstr2_tactic.h

@@ -20,7 +20,6 @@ Module Name:
 #include "tactic/tactic.h"
 #include "tactic/dependent_expr_state_tactic.h"
 #include "ast/simplifiers/elim_unconstrained.h"
-#include "ast/simplifiers/elim_unconstrained.h"
 
 class elim_uncnstr2_tactic_factory : public dependent_expr_simplifier_factory {
 public:

src/tactic/core/propagate_values2_tactic.h

@@ -0,0 +1,41 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    propagate_values2_tactic.h
+
+Abstract:
+
+    Tactic for propagating equalities (= t v) where v is a value
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-24
+
+--*/
+
+#include "util/params.h"
+#pragma once
+
+#include "util/params.h"
+#include "tactic/tactic.h"
+#include "tactic/dependent_expr_state_tactic.h"
+#include "ast/simplifiers/propagate_values.h"
+
+class propagate_values2_tactic_factory : public dependent_expr_simplifier_factory {
+public:
+    dependent_expr_simplifier* mk(ast_manager& m, params_ref const& p, dependent_expr_state& s) override {
+        return alloc(propagate_values, m, s);
+    }
+};
+
+inline tactic * mk_propagate_values2_tactic(ast_manager & m, params_ref const & p = params_ref()) {
+    return alloc(dependent_expr_state_tactic, m, p, alloc(propagate_values2_tactic_factory), "propagate-values2");
+}
+
+
+/*
+  ADD_TACTIC("propagate-valuesx2", "propagate constants.", "mk_propagate_values2_tactic(m, p)")
+*/
+