ps

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/smt/polysat/CMakeLists.txt

@@ -6,6 +6,7 @@ z3_add_component(polysat
     fixed_bits.cpp
     forbidden_intervals.cpp
     op_constraint.cpp
+    saturation.cpp
     ule_constraint.cpp
     umul_ovfl_constraint.cpp
     viable.cpp

src/sat/smt/polysat/core.cpp

@@ -204,13 +204,6 @@ namespace polysat {
         return true;
     }
 
-    signed_constraint core::get_constraint(unsigned idx, bool sign) {
-        auto sc = m_constraint_index[idx].sc;
-        if (sign)
-            sc = ~sc;
-        return sc;
-    }
-
     void core::propagate_assignment(constraint_id idx) { 
         auto [sc, dep, value] = m_constraint_index[idx.id];
         SASSERT(value != l_undef);
@@ -252,7 +245,6 @@ namespace polysat {
             bool swapped = false;
             for (unsigned i = vars.size(); i-- > 2; ) {
                 if (!is_assigned(vars[i])) {
-                    verbose_stream() << "watch instead " << vars[i] << " instead of " << vars[0] << " for " << idx << "\n";
                     add_watch(idx, vars[i]);
                     std::swap(vars[i], vars[0]);
                     swapped = true;

src/sat/smt/polysat/core.h

@@ -87,8 +87,6 @@ namespace polysat {
 
         void add_watch(unsigned idx, unsigned var);
 
-        signed_constraint get_constraint(unsigned idx, bool sign);
-
         lbool eval(signed_constraint const& sc);
         dependency_vector explain_eval(signed_constraint const& sc);
 

src/sat/smt/polysat/op_constraint.cpp

@@ -313,22 +313,12 @@ namespace polysat {
     }
 
     void op_constraint::activate_ashr(core& c, dependency const& d) {
-        //
-        // if q = k & p >= 0 -> r*2^k + 
-        // if q = k & p < 0  -> (p / 2^k) - 1 + 2^{N-k}
-        //
-
         auto& m = p.manager();
         unsigned const N = m.power_of_2();
-
         auto& C = c.cs();
         c.add_clause("q >= N & p < 0 -> p << q = -1", {~C.uge(q, N), ~C.slt(p, 0), C.eq(r, m.max_value())}, false);
         c.add_clause("q >= N & p >= 0 -> p << q = 0", {~C.uge(q, N), ~C.sge(p, 0), C.eq(r)}, false);
         c.add_clause("q = 0 -> p << q = p", { ~C.eq(q), C.eq(r, p) }, false);
-        for (unsigned k = 0; k < N; ++k) {
-//            c.add_clause("q = k & p >= 0 -> p << q = p / 2^k", {~C.eq(q, k), ~C.sge(p, 0), ... }, true);
-//            c.add_clause("q = k & p < 0 -> p << q = (p / 2^k) -1 + 2^{N-k}", {~C.eq(q, k), ~C.slt(p, 0), ... }, true);
-        }
     }
 
 
@@ -361,7 +351,43 @@ namespace polysat {
     }   
 
     void op_constraint::propagate_ashr(core& c, dependency const& dep) {
-
+        //
+        // Suppose q = k, p >= 0:
+        // p = ab, where b has length k, a has length N - k
+        // r = 0a, where 0 has length k, a has length N - k
+        // r*2^k = a0
+        // ab - a0 = 0b = p - r*2^k < 2^k
+        // r < 2^{N-k}
+        // 
+        // Suppose q = k, p < 0
+        // p = ab
+        // r = 111a where 111 has length k
+        // r*2^k = a0
+        // ab - a0 = 0b = p - r*2^k < 2^k
+        // r >= 1110
+        // example:
+        //    1100 = 12 = 16 - 4 = 2^4 - 2^2 = 2^N - 2^k
+        // 
+        // Succinct:
+        // if q = k & p >= 0 -> r*2^k + p < 2^{N-k} && r < 2^k
+        // if q = k & p < 0  -> (p / 2^k) - 2^N + 2^{N-k}
+        //
+        auto& m = p.manager();
+        auto N = m.power_of_2();
+        auto qv = c.subst(q);
+        if (qv.is_val() && 1 <= qv.val() && qv.val() < N) {
+            auto pv = c.subst(p);
+            auto rv = c.subst(r);
+            auto& C = c.cs();
+            unsigned k = qv.val().get_unsigned();
+            rational twoN = rational::power_of_two(N);
+            rational twoK = rational::power_of_two(k);
+            rational twoNk = rational::power_of_two(N - k);
+            auto eqK = C.eq(q, k);
+            c.add_clause("q = k -> r*2^k + p < 2^k", { ~eqK, C.ult(p - r * twoK, twoK) }, true);
+            c.add_clause("q = k & p >= 0 -> r < 2^{N-k}", { ~eqK, ~C.ule(0, p), C.ult(r, twoNk) }, true);            
+            c.add_clause("q = k & p < 0 -> r >= 2^N - 2^{N-k}", { ~eqK, ~C.slt(p, 0), C.uge(r, twoN - twoNk) }, true);
+        }
     }
 
 

src/sat/smt/polysat/saturation.cpp

@@ -34,6 +34,7 @@ namespace polysat {
 
     saturation::saturation(core& c) : c(c), C(c.cs()) {}
 
+#if 0
     void saturation::perform(pvar v) {
         for (signed_constraint c : core)
             perform(v, sc, core);
@@ -2187,4 +2188,6 @@ namespace polysat {
         }
     }
 
+#endif
+
 }

src/sat/smt/polysat/saturation.h

@@ -13,7 +13,7 @@ Author:
 --*/
 #pragma once
 
-#include "math/polysat/constraints.h"
+#include "sat/smt/polysat/constraints.h"
 
 namespace polysat {