Functions to extract fixed bits for slicing

src/math/polysat/fixed_bits.cpp

@@ -18,30 +18,59 @@ Author:
 namespace polysat {
 
     /**
-     * Constraint lhs <= rhs.
+     * 2^k * x = 2^k * b
-     *
+     * ==> x[N-k-1:0] = b[N-k-1:0]
-     * 2^(k - d) * x = 2^(k - d) * c
-     * ==> x[|d|:0] = c[|d|:0]
-     *
-     * -2^(k - 2) * x > 2^(k - 1)
-     * <=> 2 + x[1:0] > 2  (mod 4)
-     * ==> x[1:0] = 1
-     *    -- TODO: Generalize [the obvious solution does not work]
-     */
-
-    /**
-     * 2^(k - d) * x = 2^(k - d) * c
-     * ==> x[|d|:0] = c[|d|:0]
      */
     bool get_eq_fixed_lsb(pdd const& p, fixed_bits& out) {
+        SASSERT(!p.is_val());
+        unsigned const N = p.power_of_2();
+        // Recognize p = 2^k * a * x - 2^k * b
         if (!p.hi().is_val())
             return false;
-        // TODO:
+        if (!p.lo().is_val())
-        return false;
+            return false;
+        // p = c * x - d
+        rational const c = p.hi().val();
+        rational const d = (-p.lo()).val();
+        SASSERT(!c.is_zero());
+#if 1
+        // NOTE: ule_constraint::simplify removes odd factors of the leading term
+        unsigned k;
+        VERIFY(c.is_power_of_two(k));
+        if (d.parity(N) < k)
+            return false;
+        rational const b = machine_div2k(d, k);
+        out = fixed_bits(N - k - 1, 0, b);
+        SASSERT_EQ(d, b * rational::power_of_two(k));
+        SASSERT_EQ(p, (p.manager().mk_var(p.var()) - out.value) * rational::power_of_two(k));
+        return true;
+#else
+        // branch if we want to support non-simplifed constraints (not recommended)
+        //
+        // 2^k * a * x = 2^k * b
+        // ==> x[N-k-1:0] = a^-1 * b[N-k-1:0]
+        // for odd a
+        unsigned k = c.parity(N);
+        if (d.parity(N) < k)
+            return false;
+        rational const a = machine_div2k(c, k);
+        SASSERT(a.is_odd());
+        SASSERT(a.is_one());  // TODO: ule-simplify will multiply with a_inv already, so we can drop the check here.
+        rational a_inv;
+        VERIFY(a.mult_inverse(N, a_inv));
+        rational const b = machine_div2k(d, k);
+        out.hi = N - k - 1;
+        out.lo = 0;
+        out.value = a_inv * b;
+        SASSERT_EQ(p, (p.manager().mk_var(p.var()) - out.value) * a * rational::power_of_two(k));
+        return true;
+#endif
     }
 
     bool get_eq_fixed_bits(pdd const& p, fixed_bits& out) {
-        return get_eq_fixed_lsb(p, out);
+        if (get_eq_fixed_lsb(p, out))
+            return true;
+        return false;
     }
 
     /**
@@ -56,7 +85,53 @@ namespace polysat {
         return false;
     }
 
+    /**
+     * Constraint lhs <= rhs.
+     *
+     * x <= 2^k - 1  ==>  x[N-1:k] = 0
+     * x <  2^k      ==>  x[N-1:k] = 0
+     */
+    bool get_ule_fixed_msb(pdd const& p, pdd const& q, bool is_positive, fixed_bits& out) {
+        SASSERT(!q.is_zero());  // equalities are handled elsewhere
+        unsigned const N = p.power_of_2();
+        pdd const& lhs = is_positive ? p : q;
+        pdd const& rhs = is_positive ? q : p;
+        bool const is_strict = !is_positive;
+        if (lhs.is_var() && rhs.is_val()) {
+            // x <= c
+            // find smallest k such that c <= 2^k - 1, i.e., c+1 <= 2^k
+            // ==>  x <= 2^k - 1  ==> x[N-1:k] = 0
+            //
+            // x < c
+            // find smallest k such that c <= 2^k
+            // ==>  x < 2^k  ==> x[N-1:k] = 0
+            rational const c = is_strict ? rhs.val() : (rhs.val() + 1);
+            unsigned const k = c.next_power_of_two();
+            if (k < N) {
+                out.hi = N - 1;
+                out.lo = k;
+                out.value = 0;
+                return true;
+            }
+        }
+        return false;
+    }
+
+    // 2^(N-1) <= 2^(N-1-i) * x
+    bool get_ule_fixed_bit(pdd const& p, pdd const& q, bool is_positive, fixed_bits& out) {
+        return false;
+    }
+
     bool get_ule_fixed_bits(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_bits& out) {
+        SASSERT(ule_constraint::is_simplified(lhs, rhs));
+        if (rhs.is_zero())
+            return is_positive ? get_eq_fixed_bits(lhs, out) : false;
+        if (get_ule_fixed_msb(lhs, rhs, is_positive, out))
+            return true;
+        if (get_ule_fixed_lsb(lhs, rhs, is_positive, out))
+            return true;
+        if (get_ule_fixed_bit(lhs, rhs, is_positive, out))
+            return true;
         return false;
     }
 
@@ -79,44 +154,6 @@ namespace polysat {
         SASSERT(lhs.is_univariate() && lhs.degree() <= 1);
         SASSERT(rhs.is_univariate() && rhs.degree() <= 1);
 
-        if (rhs.is_zero()) { // equality
-            auto lhs_decomp = decouple_constant(lhs);
-
-            lhs = lhs_decomp.first;
-            rhs = -lhs_decomp.second;
-
-            SASSERT(rhs.is_val());
-
-            unsigned k = lhs.manager().power_of_2();
-            unsigned d = lhs.max_pow2_divisor();
-            unsigned span = k - d;
-            if (span == 0 || lhs.is_val())
-                return false;
-
-            p = lhs.div(rational::power_of_two(d));
-            rational rhs_val = rhs.val();
-            info.bits = rhs_val / rational::power_of_two(d);
-            if (!info.bits.is_int())
-                return false;
-
-            SASSERT(lhs.is_univariate() && lhs.degree() <= 1);
-
-            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;
-                info.bits = mod2k(info.bits * inv, span);
-            }
-
-            info.length = span;
-            info.positive = pos;
-            return true;
-        }
         else { // inequality - check for special case
             if (pos || lhs.power_of_2() < 3)
                 return false;

src/math/polysat/fixed_bits.h

@@ -3,7 +3,7 @@ Copyright (c) 2022 Microsoft Corporation
 
 Module Name:
 
-    Extract fixed bits from (univariate) constraints
+    Extract fixed bits of variables from univariate constraints
 
 Author:
 
@@ -35,6 +35,8 @@ namespace polysat {
     bool get_eq_fixed_bits(pdd const& p, fixed_bits& out);
 
     bool get_ule_fixed_lsb(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_bits& out);
+    bool get_ule_fixed_msb(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_bits& out);
+    bool get_ule_fixed_bit(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_bits& out);
     bool get_ule_fixed_bits(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_bits& out);
     bool get_fixed_bits(signed_constraint c, fixed_bits& out);