From d567d3b7f251c214f9dcf0ccc6171a3ae5417df0 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 18 Aug 2023 17:11:46 +0200
Subject: [PATCH] rename to try_congruence and add conditions

---
 src/math/polysat/saturation.cpp | 18 ++++++++++++------
 src/math/polysat/saturation.h   |  2 +-
 2 files changed, 13 insertions(+), 7 deletions(-)

diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index 6123cf4c2..921114bf9 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -76,7 +76,7 @@ namespace polysat {
             return false;
         if (try_nonzero_upper_extract(v, core, i))
             prop = true;
-        if (try_ugt_eq(v, core, i))
+        if (try_congruence(v, core, i))
             prop = true;
         if (try_mul_bounds(v, core, i))
             prop = true;
@@ -111,20 +111,26 @@ namespace polysat {
         return prop;
     }
 
-    bool saturation::try_ugt_eq(pvar x, conflict& core, inequality const& i) {
-        set_rule("egraph(x == y) & p(x,y) > q(x,y) ==> p(y,y) > q(y,y)");
-        if (!i.is_strict())
-            return false;
+    bool saturation::try_congruence(pvar x, conflict& core, inequality const& i) {
+        set_rule("egraph(x == y) & C(x,y) ==> C(y,y)");
+        // TODO: generalize to other constraint types?
+        // if (!i.is_strict())
+        //     return false;
         // if (!core.vars().contains(x))
         //     return false;
         if (!i.as_signed_constraint().contains_var(x))
             return false;
         for (pvar y : s.m_slicing.equivalent_vars(x)) {
+            if (x == y)
+                continue;
+            if (!s.is_assigned(y))
+                continue;
             if (!core.vars().contains(y))
                 continue;
             if (!i.as_signed_constraint().contains_var(y))
                 continue;
-            // does inequality become false by plugging in x = y?
+            SASSERT_EQ(s.get_level(y), s.get_level(x));  // propagated by slicing egraph since they are equivalent
+            SASSERT(s.m_search.get_pvar_index(y) < s.m_search.get_pvar_index(x));  // y was the earlier one since we are currently resolving x
             pdd const lhs = i.lhs().subst_pdd(x, s.var(y));
             pdd const rhs = i.rhs().subst_pdd(x, s.var(y));
             signed_constraint c = ineq(true, lhs, rhs);
diff --git a/src/math/polysat/saturation.h b/src/math/polysat/saturation.h
index 3d870faaf..7759b2394 100644
--- a/src/math/polysat/saturation.h
+++ b/src/math/polysat/saturation.h
@@ -122,7 +122,7 @@ namespace polysat {
         bool try_div_monotonicity(conflict& core);
 
         bool try_nonzero_upper_extract(pvar v, conflict& core, inequality const& i);
-        bool try_ugt_eq(pvar v, conflict& core, inequality const& i);
+        bool try_congruence(pvar v, conflict& core, inequality const& i);
 
 
         rational round(rational const& M, rational const& x);