From 114e7b73e5846a85588a6032ee7d82e22869cff1 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Wed, 19 Jul 2023 12:51:35 +0200
Subject: [PATCH] move callback into member function

---
 src/ast/euf/euf_egraph.h     | 20 ++++++++++----------
 src/math/polysat/slicing.cpp | 35 ++++++++++++++---------------------
 src/math/polysat/slicing.h   |  2 ++
 3 files changed, 26 insertions(+), 31 deletions(-)

diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
index 1b5b47734..7c34184e8 100644
--- a/src/ast/euf/euf_egraph.h
+++ b/src/ast/euf/euf_egraph.h
@@ -191,11 +191,11 @@ namespace euf {
         uint64_t               m_congruence_timestamp = 0;
 
         std::vector<std::function<void(enode*,enode*)>> m_on_merge;
-        std::function<void(enode*, enode*)>    m_on_propagate_literal;
-        std::function<void(enode*)>            m_on_make;
-        std::function<void(expr*,expr*,expr*)> m_used_eq;
-        std::function<void(app*,app*)>         m_used_cc;  
-        std::function<void(std::ostream&, void*)>   m_display_justification;
+        std::function<void(enode*,enode*)>              m_on_propagate_literal;
+        std::function<void(enode*)>                     m_on_make;
+        std::function<void(expr*,expr*,expr*)>          m_used_eq;
+        std::function<void(app*,app*)>                  m_used_cc;
+        std::function<void(std::ostream&,void*)>        m_display_justification;
 
         void push_eq(enode* r1, enode* n1, unsigned r2_num_parents) {
             m_updates.push_back(update_record(r1, n1, r2_num_parents));
@@ -301,11 +301,11 @@ namespace euf {
         void set_relevant(enode* n);
         void set_default_relevant(bool b) { m_default_relevant = b; }
 
-        void set_on_merge(std::function<void(enode* root,enode* other)>& on_merge) { m_on_merge.push_back(on_merge); }
-        void set_on_propagate(std::function<void(enode* lit,enode* ante)>& on_propagate) { m_on_propagate_literal = on_propagate; }
-        void set_on_make(std::function<void(enode* n)>& on_make) { m_on_make = on_make; }
-        void set_used_eq(std::function<void(expr*,expr*,expr*)>& used_eq) { m_used_eq = used_eq; }
-        void set_used_cc(std::function<void(app*,app*)>& used_cc) { m_used_cc = used_cc; }
+        void set_on_merge(std::function<void(enode* root,enode* other)> on_merge) { m_on_merge.push_back(std::move(on_merge)); }
+        void set_on_propagate(std::function<void(enode* lit,enode* ante)> on_propagate) { m_on_propagate_literal = std::move(on_propagate); }
+        void set_on_make(std::function<void(enode* n)> on_make) { m_on_make = std::move(on_make); }
+        void set_used_eq(std::function<void(expr*,expr*,expr*)> used_eq) { m_used_eq = std::move(used_eq); }
+        void set_used_cc(std::function<void(app*,app*)> used_cc) { m_used_cc = std::move(used_cc); }
         void set_display_justification(std::function<void(std::ostream&, void*)> d) { m_display_justification = std::move(d); }
 
         void begin_explain();
diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index 2254eded7..13ab9ad2d 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -106,27 +106,7 @@ namespace polysat {
         reg_decl_plugins(m_ast);
         m_bv = alloc(bv_util, m_ast);
         m_egraph.set_display_justification(display_dep);
-        std::function<void(enode* lit, enode* ante)> propagate_negation = [&](enode* lit, enode* ante) {
-            // LOG("lit: " << lit->get_id() << " value=" << lit->value());
-            // if (ante)
-            //     LOG("ante: " << ante->get_id() << " value=" << ante->value());
-            // else
-            //     LOG("ante: <null>");
-            // LOG(m_egraph);
-            // ante may be set when symmetric equality is added by congruence
-            if (ante)
-                return;
-            // on_propagate may be called before set_value
-            if (lit->value() == l_undef)
-                return;
-            SASSERT(lit->is_equality());
-            SASSERT_EQ(lit->value(), l_false);
-            SASSERT(lit->get_lit_justification().is_external());
-            // LOG("lit: id=" << lit->get_id() << " value=" << lit->value() << " dep=" << decode_dep(lit->get_lit_justification().ext<void>()));
-            m_disequality_conflict = lit;
-        };
-        m_egraph.set_on_propagate(propagate_negation);
-
+        m_egraph.set_on_propagate([&](enode* lit, enode* ante) { egraph_on_propagate(lit, ante); });
     }
 
     slicing::slice_info& slicing::info(euf::enode* n) {
@@ -520,6 +500,19 @@ namespace polysat {
         end_explain();
     }
 
+    void slicing::egraph_on_propagate(enode* lit, enode* ante) {
+        // ante may be set when symmetric equality is added by congruence
+        if (ante)
+            return;
+        // on_propagate may be called before set_value
+        if (lit->value() == l_undef)
+            return;
+        SASSERT(lit->is_equality());
+        SASSERT_EQ(lit->value(), l_false);
+        SASSERT(lit->get_lit_justification().is_external());
+        m_disequality_conflict = lit;
+    }
+
     bool slicing::can_propagate() const {
         return !m_needs_congruence.empty() || m_egraph.can_propagate();
     }
diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h
index 0efd66b5a..a360f5025 100644
--- a/src/math/polysat/slicing.h
+++ b/src/math/polysat/slicing.h
@@ -168,6 +168,8 @@ namespace polysat {
         // (i.e., x and y have the same base, but are not necessarily in the same equivalence class)
         void explain_equal(enode* x, enode* y, sat::literal_vector& out_lits, unsigned_vector& out_vars);
 
+        void egraph_on_propagate(enode* lit, enode* ante);
+
         // Merge equivalence classes of two base slices.
         // Returns true if merge succeeded without conflict.
         [[nodiscard]] bool merge_base(enode* s1, enode* s2, dep_t dep);