na

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

src/ast/sls/bv_sls_eval.cpp

@@ -1122,57 +1122,123 @@ namespace bv {
         for (unsigned i = 0; i < e.nw; ++i)
             m_tmp[i] = ~e.bits()[i];
         a.clear_overflow_bits(m_tmp);
-        return a.set_repair(random_bool(), m_tmp);       
+        return a.try_set(m_tmp);
     }
 
-    bool sls_eval::try_repair_bneg(bvval const& e, bvval& a) {
-        
+    bool sls_eval::try_repair_bneg(bvval const& e, bvval& a) {        
         e.set_sub(m_tmp, m_zero, e.bits()); 
-        return a.set_repair(random_bool(), m_tmp);        
+        return a.try_set(m_tmp);
     }
 
-    bool sls_eval::try_repair_ule(bool e, bvval& a, bvval const& b) {
-        return try_repair_ule(e, a, b.bits());       
-    }
-
-    bool sls_eval::try_repair_uge(bool e, bvval& a, bvval const& b) {
-        return try_repair_uge(e, a, b.bits());
-    }
 
     // a <=s b <-> a + p2 <=u b + p2
-
     // 
-    // to solve x for x <=s b:
-    // y := at most (b + p2) - p2
-    // x := random_at_most y
-    // or
-    // x := random_at_least y - p2 if y < p2
-    //
+    // NB: p2 = -p2
+    // 
     // to solve x for x >s b:
-    // infeasible if b + p2 = 0
-    // y := at least (b + 1 + p2) - p2
-    // TODO
+    // infeasible if b + 1 = p2
+    // solve for x >=s b + 1
     // 
     bool sls_eval::try_repair_sle(bool e, bvval& a, bvval const& b) {
-        a.set(m_tmp, b.bits());
-        if (e) {
-            return a.set_repair(true, m_tmp);
-        }
+        auto& p2 = m_b;
+        b.set_zero(p2);
+        p2.set(b.bw - 1, true);
+        p2.set_bw(b.bw);
+        bool r = false;
+        if (e) 
+            r = try_repair_sle(a, b.bits(), p2);        
         else {
-            a.set_add(m_tmp2, m_tmp, m_one);
-            return a.set_repair(false, m_tmp2);
+            auto& b1 = m_nexta;
+            a.set_add(b1, b.bits(), m_one);
+            if (p2 == b1)
+                r = false;
+            else
+                r = try_repair_sge(a, b1, p2);
         }
+        p2.set_bw(0);
+        return r;
     }
 
+    // to solve x for x <s b:
+    // infeasible if b = 0
+    // solve for x <=s b - 1
+    // 
     bool sls_eval::try_repair_sge(bool e, bvval& a, bvval const& b) {
-        a.set(m_tmp, b.bits());
-        if (e) {
-            return a.set_repair(false, m_tmp);
-        }
+        auto& p2 = m_b;
+        b.set_zero(p2);
+        p2.set(b.bw - 1, true);
+        p2.set_bw(b.bw);
+        bool r = false;
+        if (e)
+            r = try_repair_sge(a, b.bits(), p2);
+        else if (b.is_zero())
+            r = false;
         else {
-            a.set_sub(m_tmp2, m_tmp, m_one);
-            return a.set_repair(true, m_tmp2);
-        }        
+            auto& b1 = m_nexta;
+            a.set_sub(b1, b.bits(), m_one);
+            b1.set_bw(b.bw);
+            r = try_repair_sle(a, b1, p2);
+            b1.set_bw(0);
+        }
+        p2.set_bw(0);
+        return r;
+    }
+
+
+    // to solve x for x <=s b:
+    // let c := b + p2
+    // solve for
+    //    x + p2 <= c
+    // 
+    // x := random x <= b or x >= p2  if c >= p2 (b < p2)
+    // or
+    // x := random p2 <= x <= b       if c < p2  (b >= p2)
+    // 
+    bool sls_eval::try_repair_sle(bvval& a, bvect const& b, bvect const& p2) {
+        bool r = false;
+        if (b < p2) {
+            bool coin = m_rand() % 2 == 0;
+            if (coin)
+                r = a.set_random_at_least(p2, m_tmp3, m_rand);
+            if (!r)
+                r = a.set_random_at_most(b, m_tmp3, m_rand);
+            if (!coin && !r)
+                r = a.set_random_at_least(p2, m_tmp3, m_rand);
+        }
+        else 
+            r = a.set_random_in_range(p2, b, m_tmp3, m_rand);
+        return r;
+    }
+
+    // solve for x >=s b
+    // 
+    // d := b + p2
+    // 
+    // x := random b <= x < p2        if d >= p2 (b < p2)
+    // or
+    // x := random b <= x or x < p2   if d < p2
+    //  
+
+    bool sls_eval::try_repair_sge(bvval& a, bvect const& b, bvect const& p2) {
+        auto& p2_1 = m_tmp4;
+        a.set_sub(p2_1, p2, m_one);
+        p2_1.set_bw(a.bw);
+        bool r = false;
+        if (b < p2) 
+            // random b <= x < p2 
+            r = a.set_random_in_range(b, p2_1, m_tmp3, m_rand);        
+        else {
+            // random b <= x or x < p2
+            bool coin = m_rand() % 2 == 0;
+            if (coin)
+                r = a.set_random_at_most(p2_1, m_tmp3, m_rand);
+            if (!r)
+                r = a.set_random_at_least(b, m_tmp3, m_rand);
+            if (!r && !coin)
+                r = a.set_random_at_most(p2_1, m_tmp3, m_rand);
+        }
+        p2_1.set_bw(0);
+        return r;
     }
 
     void sls_eval::add_p2_1(bvval const& a, bvect& t) const {
@@ -1182,30 +1248,30 @@ namespace bv {
         a.clear_overflow_bits(t);
     }
 
-    bool sls_eval::try_repair_ule(bool e, bvval& a, bvect const& t) {
+    bool sls_eval::try_repair_ule(bool e, bvval& a, bvval const& b) {
         if (e) {
             // a <= t
-            return a.set_random_at_most(t, m_tmp, m_rand);
+            return a.set_random_at_most(b.bits(), m_tmp, m_rand);
         }
         else {
             // a > t
-            a.set_add(m_tmp, t, m_one);
+            a.set_add(m_tmp, b.bits(), m_one);
             if (a.is_zero(m_tmp))
                 return false;   
             return a.set_random_at_least(m_tmp, m_tmp2, m_rand);
         }           
     }
 
-    bool sls_eval::try_repair_uge(bool e, bvval& a, bvect const& t) {
+    bool sls_eval::try_repair_uge(bool e, bvval& a, bvval const& b) {
         if (e) {
             // a >= t
-            return a.set_random_at_least(t, m_tmp, m_rand);
+            return a.set_random_at_least(b.bits(), m_tmp, m_rand);
         }
         else {
             // a < t
-            if (a.is_zero(t))
+            if (b.is_zero())
                 return false;
-            a.set_sub(m_tmp, t, m_one);
+            a.set_sub(m_tmp, b.bits(), m_one);
             return a.set_random_at_most(m_tmp, m_tmp2, m_rand);
         }    
     }

src/ast/sls/bv_sls_eval.h

@@ -89,6 +89,8 @@ namespace bv {
         bool try_repair_uge(bool e, bvval& a, bvval const& b);
         bool try_repair_sle(bool e, bvval& a, bvval const& b);
         bool try_repair_sge(bool e, bvval& a, bvval const& b);
+        bool try_repair_sge(bvval& a, bvect const& b, bvect const& p2);
+        bool try_repair_sle(bvval& a, bvect const& b, bvect const& p2);
         bool try_repair_shl(bvval const& e, bvval& a, bvval& b, unsigned i);
         bool try_repair_ashr(bvval const& e, bvval& a, bvval& b, unsigned i);
         bool try_repair_lshr(bvval const& e, bvval& a, bvval& b, unsigned i);

src/ast/sls/sls_valuation.cpp

@@ -205,13 +205,9 @@ namespace bv {
         if (is_zero(tmp) || (0 == r() % 2))
             return try_set(tmp);
 
-        
+        set_random_below(tmp, r);
         // random value below tmp
-        auto msb_bit = msb(tmp);
-        for (unsigned i = 0; i < nw; ++i)
-            tmp[i] = (random_bits(r) & ~fixed[i]) | (fixed[i] & tmp[i]);
-        for (unsigned i = msb_bit; i < bw; ++i)
-            tmp.set(i, false);
+
         if (m_lo == m_hi || is_zero(m_lo) || m_lo <= tmp)
             return try_set(tmp);
 
@@ -226,10 +222,8 @@ namespace bv {
             return try_set(tmp);
 
         // random value at least tmp
-        auto msb_bit = msb(tmp);
-        for (unsigned i = 0; i < nw; ++i)
-            tmp[i] = (random_bits(r) & ~fixed[i]) | (fixed[i] & tmp[i]);
-        tmp.set(msb_bit, true);
+        set_random_above(tmp, r);
+       
         if (m_lo == m_hi || is_zero(m_hi) || m_hi > tmp)
             return try_set(tmp);
 
@@ -237,6 +231,71 @@ namespace bv {
         return get_at_least(src, tmp) && try_set(tmp);        
     }
 
+    bool sls_valuation::set_random_in_range(bvect const& lo, bvect const& hi, bvect& tmp, random_gen& r) {
+        if (0 == r() % 2) {
+            if (!get_at_least(lo, tmp))
+                return false;
+            SASSERT(in_range(tmp));
+            if (hi < tmp)
+                return false;
+
+            if (is_ones(tmp) || (0 == r() % 2))
+                return try_set(tmp);
+            set_random_above(tmp, r);
+            round_down(tmp, [&](bvect const& t) { return hi >= t && in_range(t); });
+            if (in_range(tmp) && lo <= tmp && hi >= tmp)
+                return try_set(tmp);
+            return get_at_least(lo, tmp) && hi >= tmp && try_set(tmp);
+        }
+        else {
+            if (!get_at_most(hi, tmp))
+                return false;
+            SASSERT(in_range(tmp));
+            if (lo > tmp)
+                return false;
+            if (is_zero(tmp) || (0 == r() % 2))
+                return try_set(tmp);
+            set_random_below(tmp, r);
+            round_up(tmp, [&](bvect const& t) { return lo <= t && in_range(t); });
+            if (in_range(tmp) && lo <= tmp && hi >= tmp)
+                return try_set(tmp);
+            return get_at_most(hi, tmp) && lo <= tmp && try_set(tmp);
+        }
+    }
+
+    void sls_valuation::round_down(bvect& dst, std::function<bool(bvect const&)> const& is_feasible) {      
+        for (unsigned i = bw; !is_feasible(dst) && i-- > 0; )
+            if (!fixed.get(i) && dst.get(i))
+                dst.set(i, false);        
+    }
+
+    void sls_valuation::round_up(bvect& dst, std::function<bool(bvect const&)> const& is_feasible) {
+        for (unsigned i = 0; !is_feasible(dst) && i < bw; ++i)
+            if (!fixed.get(i) && !dst.get(i))
+                dst.set(i, true);
+    }
+
+    void sls_valuation::set_random_above(bvect& dst, random_gen& r) {
+        for (unsigned i = 0; i < nw; ++i)
+            dst[i] = dst[i] | (random_bits(r) & ~fixed[i]);
+    }
+
+    void sls_valuation::set_random_below(bvect& dst, random_gen& r) {
+        if (is_zero(dst))
+            return;
+        unsigned n = 0, idx = UINT_MAX;
+        for (unsigned i = 0; i < bw; ++i)
+            if (dst.get(i) && !fixed.get(i) && (r() % ++n) == 0)
+                idx = i;                
+
+        if (idx == UINT_MAX)
+            return;
+        dst.set(idx, false);
+        for (unsigned i = 0; i < idx; ++i) 
+            if (!fixed.get(i))
+                dst.set(i, r() % 2 == 0);
+    }
+
     bool sls_valuation::set_repair(bool try_down, bvect& dst) {
         for (unsigned i = 0; i < nw; ++i)
             dst[i] = (~fixed[i] & dst[i]) | (fixed[i] & m_bits[i]);

src/ast/sls/sls_valuation.h

@@ -188,8 +188,13 @@ namespace bv {
 
         bool set_random_at_most(bvect const& src, bvect& tmp, random_gen& r);
         bool set_random_at_least(bvect const& src, bvect& tmp, random_gen& r);
+        bool set_random_in_range(bvect const& lo, bvect const& hi, bvect& tmp, random_gen& r);
 
         bool set_repair(bool try_down, bvect& dst);
+        void set_random_above(bvect& dst, random_gen& r);
+        void set_random_below(bvect& dst, random_gen& r);
+        void round_down(bvect& dst, std::function<bool(bvect const&)> const& is_feasible);
+        void round_up(bvect& dst, std::function<bool(bvect const&)> const& is_feasible);
 
 
         static digit_t random_bits(random_gen& r);