Add lemma: y = x[h:l] & y != 0 ==> x >= 2^l

src/math/polysat/saturation.cpp

@@ -47,6 +47,7 @@ namespace polysat {
     }
 
     void saturation::perform(pvar v, conflict& core) {
+        LOG_H1("Saturation for v" << v << ", core: " << core);
         IF_VERBOSE(2, verbose_stream() << "v" << v << " " << core << "\n");
         for (signed_constraint c : core)
             perform(v, c, core);
@@ -73,6 +74,8 @@ namespace polysat {
         bool prop = false;
         if (s.size(v) != i.lhs().power_of_2())
             return false;
+        if (try_nonzero_upper_extract(v, core, i))
+            prop = true;
         if (try_mul_bounds(v, core, i))
             prop = true;
         if (try_parity(v, core, i))
@@ -106,6 +109,44 @@ namespace polysat {
         return prop;
     }
 
+    bool saturation::try_nonzero_upper_extract(pvar y, conflict& core, inequality const& i) {
+        set_rule("y = x[h:l] & y != 0 ==> x >= 2^l");
+        if (!s.m_justification[y].is_propagation_by_slicing())
+            return false;
+        if (!s.get_value(y).is_zero())
+            return false;
+        if (!is_nonzero_by(y, i))
+            return false;
+        for (pvar x : core.vars()) {
+            if (!s.get_value(x).is_zero())
+                continue;
+            unsigned hi, lo;
+            if (!s.m_slicing.is_extract(y, x, hi, lo))  // TODO: generalize; use is_equal to check this and if yes, extract the explanation. otherwise it will only work in very limited cases.
+                continue;
+            if (propagate(y, core, i, s.ule(rational::power_of_two(lo), s.var(x))))
+                return true;
+        }
+        return false;
+    }
+
+    // TODO: can be generalized
+    bool saturation::is_nonzero_by(pvar x, inequality const& i) {
+        if (i.is_strict() && i.lhs().is_zero()) {
+            // 0 < p
+            pdd const& p = i.rhs();
+            if (p.is_val())
+                return false;
+            if (!p.lo().is_zero())
+                return false;
+            if (!p.hi().is_val())
+                return false;
+            SASSERT(!p.hi().is_zero());
+            // 0 < a*x for a != 0
+            return true;
+        }
+        return false;
+    }
+
     bool saturation::try_umul_ovfl(pvar v, signed_constraint c, conflict& core) {
         SASSERT(c->is_umul_ovfl());
         bool prop = false;
@@ -526,8 +567,8 @@ namespace polysat {
         return false;
     }
 
-    bool saturation::is_forced_diseq(pdd const& p, int i, signed_constraint& c) {
-        c = s.eq(p, i);
+    bool saturation::is_forced_diseq(pdd const& p, rational const& val, signed_constraint& c) {
+        c = s.eq(p, val);
         return is_forced_false(c);
     }
 

src/math/polysat/saturation.h

@@ -121,6 +121,8 @@ namespace polysat {
         bool try_infer_parity_equality(pvar x, conflict& core, inequality const& a_l_b);
         bool try_div_monotonicity(conflict& core);
 
+        bool try_nonzero_upper_extract(pvar v, conflict& core, inequality const& i);
+
         rational round(rational const& M, rational const& x);
         bool eval_round(rational const& M, pdd const& p, rational& r);
         bool extract_linear_form(pdd const& q, pvar& y, rational& a, rational& b);
@@ -199,6 +201,9 @@ namespace polysat {
 
         bool has_lower_bound(pvar x, conflict& core, rational& bound, vector<signed_constraint>& x_le_bound);
 
+        // inequality i implies x != 0
+        bool is_nonzero_by(pvar x, inequality const& i);
+
         // determine min/max parity of polynomial
         unsigned min_parity(pdd const& p, vector<signed_constraint>& explain);
         unsigned max_parity(pdd const& p, vector<signed_constraint>& explain);
@@ -210,7 +215,8 @@ namespace polysat {
         bool is_forced_eq(pdd const& p, rational const& val);
         bool is_forced_eq(pdd const& p, int i) { return is_forced_eq(p, rational(i)); }
         
-        bool is_forced_diseq(pdd const& p, int i, signed_constraint& c);
+        bool is_forced_diseq(pdd const& p, rational const& val, signed_constraint& c);
+        bool is_forced_diseq(pdd const& p, int i, signed_constraint& c) { return is_forced_diseq(p, rational(i), c); }
 
         bool is_forced_odd(pdd const& p, signed_constraint& c);
 

src/math/polysat/slicing.cpp

@@ -834,6 +834,10 @@ namespace polysat {
         }
     }
 
+    bool slicing::is_extract(pvar x, pvar src, unsigned& out_hi, unsigned& out_lo) {
+        return find_range_in_ancestor(var2slice(x), var2slice(src), out_hi, out_lo);
+    }
+
     void slicing::egraph_on_merge(enode* root, enode* other) {
         SASSERT(!is_value(other));  // by convention, interpreted nodes are always chosen as root
         if (is_value(root)) {

src/math/polysat/slicing.h

@@ -320,6 +320,9 @@ namespace polysat {
         pvar mk_concat(unsigned num_args, pvar const* args) { return mk_concat(num_args, args, null_var); }
         pvar mk_concat(std::initializer_list<pvar> args);
 
+        // Find hi, lo such that x = src[hi:lo].
+        bool is_extract(pvar x, pvar src, unsigned& out_hi, unsigned& out_lo);
+
         // Track value assignments to variables (and propagate to subslices)
         // (could generalize to fixed bits, then we need a way to merge interpreted enodes)
         void add_value(pvar v, rational const& value);