fixup repairs

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/ast/sls/bv_sls_eval.cpp

@@ -777,8 +777,8 @@ namespace bv {
             return try_repair_zero_ext(assign_value(e), wval(e, 0));
         case OP_SIGN_EXT:
             return try_repair_sign_ext(assign_value(e), wval(e, 0));
-        case OP_CONCAT:
-            return try_repair_concat(assign_value(e), wval(e, 0), wval(e, 1), i);
+        case OP_CONCAT: 
+            return try_repair_concat(e, i);        
         case OP_EXTRACT: {
             unsigned hi, lo;
             expr* arg;
@@ -1218,18 +1218,18 @@ namespace bv {
         a.set_sub(p2_1, p2, m_one);
         p2_1.set_bw(a.bw);
         bool r = false;
-        if (p2 < b) 
+        if (b < p2) 
             // random b <= x < p2 
             r = a.set_random_in_range(b, p2_1, 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_rand);
+                r = a.set_random_at_most(p2_1, m_rand);
             if (!r)
-                r = a.set_random_at_least(b,  m_rand);
+                r = a.set_random_at_least(b, m_rand);
             if (!r && !coin)
-                r = a.set_random_at_most(p2_1,  m_rand);
+                r = a.set_random_at_most(p2_1, m_rand);
         }
         p2_1.set_bw(0);
         return r;
@@ -1790,21 +1790,16 @@ namespace bv {
         return a.try_set(m_tmp);
     }
 
-    bool sls_eval::try_repair_concat(bvect const& e, bvval& a, bvval& b, unsigned idx) {
-        bool r = false;
-        if (idx == 0) {
-            for (unsigned i = 0; i < a.bw; ++i)
-                m_tmp.set(i, e.get(i + b.bw));
-            a.clear_overflow_bits(m_tmp);
-            r = a.try_set(m_tmp);
-        }
-        else {
-            for (unsigned i = 0; i < b.bw; ++i)
-                m_tmp.set(i, e.get(i));
-            b.clear_overflow_bits(m_tmp);
-            r = b.try_set(m_tmp);
-        }       
-        return r;
+    bool sls_eval::try_repair_concat(app* e, unsigned idx) {
+        unsigned bw = 0;
+        auto& ve = assign_value(e);
+        for (unsigned j = 0; j < idx; ++j)
+            bw += bv.get_bv_size(e->get_arg(j));
+        auto& a = wval(e, idx);
+        for (unsigned i = 0; i < a.bw; ++i)
+            m_tmp.set(i, ve.get(i + bw));
+        a.clear_overflow_bits(m_tmp);
+        return a.try_set(m_tmp);
     }
 
     //

src/ast/sls/bv_sls_eval.h

@@ -104,7 +104,7 @@ namespace bv {
         bool try_repair_umul_ovfl(bool e, bvval& a, bvval& b, unsigned i);
         bool try_repair_zero_ext(bvect const& e, bvval& a);
         bool try_repair_sign_ext(bvect const& e, bvval& a);
-        bool try_repair_concat(bvect const& e, bvval& a, bvval& b, unsigned i);
+        bool try_repair_concat(app* e, unsigned i);
         bool try_repair_extract(bvect const& e, bvval& a, unsigned lo);
         bool try_repair_comp(bvect const& e, bvval& a, bvval& b, unsigned i);
         bool try_repair_eq(bool is_true, bvval& a, bvval const& b);

src/ast/sls/sls_valuation.cpp

@@ -279,29 +279,23 @@ namespace bv {
             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);
+            if (in_range(tmp) || get_at_least(lo, tmp))
+                return lo <= tmp && tmp <= hi && 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);
+            if (in_range(tmp) || get_at_most(hi, tmp))
+                return lo <= tmp && tmp <= hi && try_set(tmp);
         }
+        return false;
     }
 
     void sls_valuation::round_down(bvect& dst, std::function<bool(bvect const&)> const& is_feasible) {