From f09d37f93fbfe17055d56f247a6bfdf0b89f292b Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 6 Nov 2023 14:17:28 +0100
Subject: [PATCH] slicing: fix dependency tracking for values

---
 src/math/polysat/slicing.cpp | 31 ++++++++++++++++++-------------
 src/math/polysat/slicing.h   |  2 +-
 src/math/polysat/solver.cpp  |  2 ++
 3 files changed, 21 insertions(+), 14 deletions(-)

diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp
index df17cc029..f4cca2a62 100644
--- a/src/math/polysat/slicing.cpp
+++ b/src/math/polysat/slicing.cpp
@@ -899,30 +899,35 @@ namespace polysat {
         SASSERT_EQ(root, root->get_root());
         SASSERT_EQ(root, other->get_root());
 
-        enode* v1 = info(root).value_node;   // root is the root
-        enode* v2 = info(other).value_node;  // 'other' was its own root before the merge
+        enode* const v1 = info(root).value_node;   // root is the root
+        enode* const v2 = info(other).value_node;  // 'other' was its own root before the merge
         if (v1 && v2 && get_value(v1) != get_value(v2)) {
             // we have a conflict. add interpreted enodes to make the egraph realize it.
-            enode* i1 = mk_interpreted_value_node(v1);
-            enode* i2 = mk_interpreted_value_node(v2);
+            enode* const i1 = mk_interpreted_value_node(v1);
+            enode* const i2 = mk_interpreted_value_node(v2);
             m_egraph.merge(i1, v1, dep_t().encode());
             m_egraph.merge(i2, v2, dep_t().encode());
             SASSERT(is_conflict());
             return;
         }
 
-        if (v1 || v2) {
-            if (!v1) set_value_node(root, v2);
-            if (!v2) set_value_node(other, v1);
-            rational const val = get_value(v1 ? v1 : v2);
+        enode* const v = v1 ? v1 : v2;
+        if (v && !(v1 && v2)) {
+            // exactly one node has a value
+            rational const val = get_value(v);
             for (enode* n : euf::enode_class(other)) {
-                pvar const v = slice2var(n);
-                if (v == null_var)
-                    continue;
-                if (m_solver.is_assigned(v))
+                pvar const var = slice2var(n);
+                if (var != null_var && m_solver.is_assigned(var))
+                    continue;  // TODO: could try to detect possible conflicts by checking value
+
+                enode* const vn = get_value_node(n);
+                if (!vn)
+                    set_value_node(n, v);
+
+                if (var == null_var)
                     continue;
                 LOG("on_merge: v" << v << " := " << val);
-                m_solver.assign_propagate_by_slicing(v, val);
+                m_solver.assign_propagate_by_slicing(var, val);
             }
         }
     }
diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h
index 5c21d73d6..92b9a1e74 100644
--- a/src/math/polysat/slicing.h
+++ b/src/math/polysat/slicing.h
@@ -154,7 +154,7 @@ namespace polysat {
 
         enode* parent(enode* s) const { return info(s).parent; }
 
-        enode* get_value_node(enode* s) const { return info(s->get_root()).value_node; }
+        enode* get_value_node(enode* s) const { return info(s).value_node; }
         void set_value_node(enode* s, enode* value_node);
 
         unsigned get_cut(enode* s) const { return info(s).cut; }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index b8d4d4c3e..a5bf031d8 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1007,11 +1007,13 @@ namespace polysat {
     }
 
     void solver::revert_decision(pvar v) {
+        LOG("revert_decision: v" << v);
         unsigned max_jump_level = get_level(v) - 1;
         backjump_and_learn(max_jump_level, false);
     }
 
     void solver::revert_bool_decision(sat::literal const lit) {
+        LOG("revert_bool_decision: " << lit_pp(*this, lit));
         unsigned max_jump_level = m_bvars.level(lit) - 1;
         backjump_and_learn(max_jump_level, true);
         // NOTE: happens in 42448.smt2; but does not seem to be a bug.