Frequent lsb special case

src/math/polysat/simplify_clause.cpp

@@ -358,49 +358,78 @@ namespace polysat {
     }
     
     // 2^(k - d) * x = m * 2^(k - d)
+    // Special case [still seems to occur frequently]: -2^(k - 2) * x > 2^(k - 1) - TODO: Generalize [the obvious solution does not work] => lsb(x, 2) = 1
     bool simplify_clause::get_lsb(pdd lhs, pdd rhs, pdd& p, trailing_bits& info, bool pos) {
-        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;
-        
-        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);
+        SASSERT(rhs.is_univariate() && rhs.degree() <= 1);
 
-        auto it = p.begin();
+        if (rhs.is_zero()) { // equality
-        auto first = *it;
+            auto lhs_decomp = decouple_constant(lhs);
-        it++;
+
-        if (it == p.end()) {
+            lhs = lhs_decomp.first;
-            // 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
+            rhs = -lhs_decomp.second;
-            SASSERT(first.coeff.is_odd());
+
-            rational inv;
+            SASSERT(rhs.is_val());
-            VERIFY(first.coeff.mult_inverse(lhs.power_of_2(), inv));
+
-            p *= inv;
+            unsigned k = lhs.manager().power_of_2();
-            info.bits = mod2k(info.bits * inv, span);
+            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;
+            auto it = lhs.begin();
+            if (it == lhs.end())
+                return false;
+            if (it->vars.size() != 1)
+                return false;
+            rational coeff = it->coeff;
+            it++;
+            if (it != lhs.end())
+                return false;
+            if ((mod2k(-coeff, lhs.power_of_2())) != rational::power_of_two(lhs.power_of_2() - 2))
+                return false;
+            p = lhs.div(coeff);
+            SASSERT(p.is_var());
+            info.bits = 1;
+            info.length = 2;
+            info.positive = true; // this is a conjunction
+            return true;
         }
-        
-        info.length = span;
-        info.positive = pos;
-        return true;
     }
 
     // 2^k - 2^(k - i) <= x -> first i bits 1
     // 2^(k - i) > x -> first i bits 0
     bool simplify_clause::get_msb(pdd lhs, pdd rhs, pdd& p, leading_bits& info, bool pos) {
+        SASSERT(lhs.is_univariate() && lhs.degree() <= 1);
+        SASSERT(rhs.is_univariate() && rhs.degree() <= 1);
+
         if (lhs.is_var() && rhs.is_val()) {
             if (rhs.is_zero())
                 return false;
@@ -439,7 +468,10 @@ namespace polysat {
     // 2^(k - 1) <= 2^(k - i - 1) * x (original definition)
     // 2^(k - i - 1) * x + 2^(k - 1) <= 2^(k - 1) - 1 (rewritten)
     bool simplify_clause::get_bit(const pdd& lhs, const pdd& rhs, pdd& p, single_bit& bit, bool pos) {
+        SASSERT(lhs.is_univariate() && lhs.degree() <= 1);
+        SASSERT(rhs.is_univariate() && rhs.degree() <= 1);
         unsigned k = rhs.power_of_2();
+
         if (rhs.is_val()) {
             // 2^(k - i - 1) * x + 2^(k - 1) <= 2^(k - 1) - 1
             rational rhs_val = rhs.val() + 1;

src/test/polysat.cpp

@@ -698,6 +698,21 @@ namespace polysat {
             VERIFY(!s.m_viable.collect_bit_information(x.var(), false, fixed, justifications));
         }
 
+        // parity(x) >= 1 and bit_1(x)
+        static void test_fi_quickcheck3() {
+            scoped_solver s(__func__);
+            auto x = s.var(s.add_var(256));
+            signed_constraint c1 = s.eq(rational::power_of_two(255) * x);
+            signed_constraint c2 = s.ult(rational::power_of_two(255), -rational::power_of_two(254) * x);
+            s.add_clause(c1, false);
+            s.add_clause(c2, false);
+            s.m_viable.intersect(x.var(), c1);
+            s.m_viable.intersect(x.var(), c2);
+            svector<lbool> fixed;
+            vector<ptr_vector<viable::entry>> justifications;
+            VERIFY(!s.m_viable.collect_bit_information(x.var(), false, fixed, justifications));
+        }
+
         // 8 * x + 3 == 0 or 8 * x + 5 == 0 is unsat
         static void test_parity1() {
             scoped_solver s(__func__);
@@ -2069,6 +2084,8 @@ void tst_polysat() {
     
     RUN(test_polysat::test_fi_quickcheck1());
     RUN(test_polysat::test_fi_quickcheck2());
+    RUN(test_polysat::test_fi_quickcheck3());
+
     if (collect_test_records)
         test_records.display(std::cout);
 }