From e8b4875a1742aec6548670f2d0df591015050446 Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <Clemens.Eisenhofer@tuwien.ac.at>
Date: Sat, 18 Feb 2023 14:15:51 +0100
Subject: [PATCH] Multiply by inverse to detect more parity constraints

---
 src/math/polysat/simplify_clause.cpp      | 22 +++++++++++++++++-----
 src/math/polysat/variable_elimination.cpp |  7 +++----
 src/math/polysat/viable.cpp               |  1 +
 3 files changed, 21 insertions(+), 9 deletions(-)

diff --git a/src/math/polysat/simplify_clause.cpp b/src/math/polysat/simplify_clause.cpp
index bde128e88..4b53290f1 100644
--- a/src/math/polysat/simplify_clause.cpp
+++ b/src/math/polysat/simplify_clause.cpp
@@ -349,7 +349,7 @@ namespace polysat {
     }
 
     // decomposes into a plain constant and a part containing variables. e.g., 2*x*y + 3*z - 2 gets { 2*x*y + 3*z, -2 }
-    static std::pair<pdd, pdd> decompose_constant(const pdd& p) {
+    static std::pair<pdd, pdd> decouple_constant(const pdd& p) {
         for (const auto& m : p) {
             if (m.vars.empty())
                 return { p - m.coeff, p.manager().mk_val(m.coeff) };
@@ -358,10 +358,9 @@ namespace polysat {
     }
     
     // 2^(k - d) * x = m * 2^(k - d)
-    // TODO: Factor out constant factors from x and put them to the rhs 
     bool simplify_clause::get_trailing_mask(pdd lhs, pdd rhs, pdd& p, trailing_bits& mask, bool pos) {
-        auto lhs_decomp = decompose_constant(lhs);
-        auto rhs_decomp = decompose_constant(rhs);
+        auto lhs_decomp = decouple_constant(lhs);
+        auto rhs_decomp = decouple_constant(rhs);
         
         lhs = lhs_decomp.first - rhs_decomp.first;
         rhs = rhs_decomp.second - lhs_decomp.second;
@@ -371,7 +370,7 @@ namespace polysat {
         unsigned k = lhs.manager().power_of_2(); 
         unsigned d = lhs.max_pow2_divisor();
         unsigned span = k - d;
-        if (span == 0)
+        if (span == 0 || lhs.is_val())
             return false;
         
         p = lhs.div(rational::power_of_two(d));
@@ -379,6 +378,19 @@ namespace polysat {
         mask.bits = rhs_val / rational::power_of_two(d);
         if (!mask.bits.is_int())
             return false;
+        
+        auto it = p.begin();
+        auto first = *it;
+        it++;
+        if (it == p.end()) {
+            // if the lhs contains only one monomial it is of the form: odd * x = mask. We can multiply by the inverse to get the mask for x
+            SASSERT(first.coeff.is_odd());
+            rational inv;
+            VERIFY(first.coeff.mult_inverse(lhs.power_of_2(), inv));
+            p *= inv;
+            mask.bits *= inv;
+        }
+        
         mask.length = span;
         mask.positive = pos;
         return true;
diff --git a/src/math/polysat/variable_elimination.cpp b/src/math/polysat/variable_elimination.cpp
index 245d2047b..9d2b816f5 100644
--- a/src/math/polysat/variable_elimination.cpp
+++ b/src/math/polysat/variable_elimination.cpp
@@ -764,9 +764,9 @@ namespace polysat {
         
         if (a_parity > 0) {
             shift = s.lshr(a1, a1.manager().mk_val(a_parity));
-            signed_constraint least_parity = s.parity_at_least(a1, a_parity);
-            signed_constraint shift_right_left = s.eq(rational::power_of_two(a_parity) * shift, a1);
-            s.add_clause(~least_parity, shift_right_left, true);
+            //signed_constraint least_parity = s.parity_at_least(a1, a_parity);
+            //signed_constraint shift_right_left = s.eq(rational::power_of_two(a_parity) * shift, a1);
+            //s.add_clause(~least_parity, shift_right_left, true);
             // s.add_clause(~shift_right_left, least_parity, true); Might be interesting as well [although not needed]; needs to consider special case 0
             // [nsb cr: this pre-condition is already implied from the parity explanations]
             // precondition.insert_eval(~shift_right_left);
@@ -778,7 +778,6 @@ namespace polysat {
         LOG("pseudo inverse: " << a_pi);
         LOG("-b: " << (-b));
         LOG("shifted a" << shift);
-        LOG("Forced elimination: " << a_pi * (-b) * shift + b1);
         return { a_pi * (-b) * shift + b1, true };
 #endif
     }
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 96854cb8b..b844894b6 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -913,6 +913,7 @@ namespace {
         
         do {
             if (e->src.size() != 1) {
+                // We just consider the ordinary constraints and not already contracted ones 
                 e = e->next();
                 continue;
             }