na

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

src/ast/sls/bv_sls.cpp

@@ -70,7 +70,7 @@ namespace bv {
     void sls::reinit_eval() {
         std::function<bool(expr*, unsigned)> eval = [&](expr* e, unsigned i) {
             auto should_keep = [&]() {
-                return m_rand() % 100 >= 98;
+                return m_rand() % 100 <= 92;
             };
             if (m.is_bool(e)) {
                 if (m_eval.is_fixed0(e) || should_keep())
@@ -127,11 +127,12 @@ namespace bv {
             if (!e)
                 return l_true;
 
-            ++m_stats.m_moves;
 
             trace_repair(down, e);
 
-            if (down)
+            ++m_stats.m_moves;
+
+            if (down) 
                 try_repair_down(e);
             else
                 try_repair_up(e);            

src/ast/sls/bv_sls_eval.cpp

@@ -30,7 +30,7 @@ namespace bv {
                 continue;
             app* a = to_app(e);
             if (bv.is_bv(e)) 
-                add_bit_vector(e);
+                add_bit_vector(a);
             if (a->get_family_id() == basic_family_id)
                 init_eval_basic(a);
             else if (a->get_family_id() == bv.get_family_id())
@@ -40,7 +40,7 @@ namespace bv {
                     auto& v = wval(e);
                     for (unsigned i = 0; i < v.bw; ++i)
                         m_tmp.set(i, eval(e, i));
-                    v.set(m_tmp);
+                    v.set_repair(random_bool(), m_tmp);
                 }
                 else if (m.is_bool(e))
                     m_eval.setx(e->get_id(), eval(e, 0), false);
@@ -78,16 +78,21 @@ namespace bv {
         return m_todo;
     }
 
-    bool sls_eval::add_bit_vector(expr* e) {
-        auto bw = bv.get_bv_size(e);
+    bool sls_eval::add_bit_vector(app* e) {
         m_values.reserve(e->get_id() + 1);
         if (m_values.get(e->get_id()))
             return false;
-        m_values.set(e->get_id(), alloc_valuation(bw));
+        auto v = alloc_valuation(e);
+        m_values.set(e->get_id(), v);
+        if (bv.is_sign_ext(e)) {
+            unsigned p = e->get_parameter(0).get_int();
+            v->set_signed(p);
+        }
         return true;
     }
 
-    sls_valuation* sls_eval::alloc_valuation(unsigned bit_width) {
+    sls_valuation* sls_eval::alloc_valuation(app* e) {
+        auto bit_width = bv.get_bv_size(e);
         auto* r = alloc(sls_valuation, bit_width);
         while (m_tmp.size() < 2 * r->nw) {
             m_tmp.push_back(0);
@@ -905,8 +910,14 @@ namespace bv {
     }
 
     bool sls_eval::try_repair_eq(bool is_true, bvval& a, bvval const& b) {
-        if (is_true)
-            return a.try_set(b.bits());
+        if (is_true) {
+            if (m_rand() % 20 != 0) 
+                if (a.try_set(b.bits()))
+                    return true;
+            
+            a.get_variant(m_tmp, m_rand);
+            return a.set_repair(random_bool(), m_tmp);
+        }
         else {
             bool try_above = m_rand() % 2 == 0;
             if (try_above) {
@@ -1004,22 +1015,26 @@ namespace bv {
     // If this fails, set a to a random value
     // 
     bool sls_eval::try_repair_add(bvect const& e, bvval& a, bvval const& b) {
-        a.set_sub(m_tmp, e, b.bits());
-        if (a.try_set(m_tmp))
-            return true;
+        if (m_rand() % 20 != 0) {
+            a.set_sub(m_tmp, e, b.bits());
+            if (a.try_set(m_tmp))
+                return true;
+        }
         a.get_variant(m_tmp, m_rand);
         return a.set_repair(random_bool(), m_tmp);          
     }
 
     bool sls_eval::try_repair_sub(bvect const& e, bvval& a, bvval & b, unsigned i) {
-        if (i == 0) 
-            // e = a - b -> a := e + b
-            a.set_add(m_tmp, e, b.bits());        
-        else 
-            // b := a - e
-            b.set_sub(m_tmp, a.bits(), e);       
-        if (a.try_set(m_tmp))
-            return true;
+        if (m_rand() % 20 != 0) {
+            if (i == 0) 
+                // e = a - b -> a := e + b
+                a.set_add(m_tmp, e, b.bits());        
+            else 
+                // b := a - e
+                b.set_sub(m_tmp, a.bits(), e);       
+            if (a.try_set(m_tmp))
+                return true;
+        }
         // fall back to a random value
         a.get_variant(m_tmp, m_rand);
         return a.set_repair(random_bool(), m_tmp);
@@ -1045,6 +1060,11 @@ namespace bv {
             return a.set_repair(random_bool(), m_tmp);            
         }      
 
+        if (m_rand() % 20 == 0) {
+            a.get_variant(m_tmp, m_rand);
+            return a.set_repair(random_bool(), m_tmp);            
+        }
+
 #if 0
         verbose_stream() << "solve for " << e << "\n";
 
@@ -1125,7 +1145,11 @@ namespace bv {
         if (parity_e > 0 && parity_b > 0)
             b.shift_right(m_tmp2, std::min(parity_b, parity_e));
         a.set_mul(m_tmp, tb, m_tmp2);
-        return a.set_repair(random_bool(), m_tmp);      
+        if (a.set_repair(random_bool(), m_tmp))
+            return true;
+
+        a.get_variant(m_tmp, m_rand);
+        return a.set_repair(random_bool(), m_tmp);
     }
 
     bool sls_eval::try_repair_bnot(bvect const& e, bvval& a) {

src/ast/sls/bv_sls_eval.h

@@ -59,8 +59,8 @@ namespace bv {
         * Register e as a bit-vector. 
         * Return true if not already registered, false if already registered.
         */
-        bool add_bit_vector(expr* e);
-        sls_valuation* alloc_valuation(unsigned bit_width);
+        bool add_bit_vector(app* e);
+        sls_valuation* alloc_valuation(app* e);
 
         bool bval1_basic(app* e) const;
         bool bval1_bv(app* e) const;  
@@ -143,7 +143,7 @@ namespace bv {
 
         sls_valuation& wval(expr* e) const;
 
-        bool is_fixed0(expr* e) const { return m_fixed[e->get_id()]; }
+        bool is_fixed0(expr* e) const { return m_fixed.get(e->get_id(), false); }
 
         /**
          * Retrieve evaluation based on immediate children.         

src/ast/sls/sls_valuation.cpp

@@ -307,18 +307,21 @@ namespace bv {
     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);        
+                dst.set(i, false);      
+        repair_sign_bits(dst);
     }
 
     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);
+        repair_sign_bits(dst);
     }
 
     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]);
+        repair_sign_bits(dst);
     }
 
     void sls_valuation::set_random_below(bvect& dst, random_gen& r) {
@@ -335,12 +338,14 @@ namespace bv {
         for (unsigned i = 0; i < idx; ++i) 
             if (!fixed.get(i))
                 dst.set(i, r() % 2 == 0);
+        repair_sign_bits(dst);
     }
 
     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]);
 
+        repair_sign_bits(dst);
         if (in_range(dst)) {
             set(eval, dst);
             return true;
@@ -363,6 +368,7 @@ namespace bv {
                 if (!fixed.get(i) && dst.get(i))
                     dst.set(i, false);
         }
+        repair_sign_bits(dst);
         if (in_range(dst)) {
             set(eval, dst);
             repaired = true;
@@ -378,6 +384,7 @@ namespace bv {
             for (unsigned i = 0; i < nw; ++i)
                 out[i] = fixed[i] & m_bits[i];
         }
+        repair_sign_bits(out);
         SASSERT(!has_overflow(out));
     }
 
@@ -390,6 +397,7 @@ namespace bv {
             for (unsigned i = 0; i < nw; ++i)
                 out[i] = ~fixed[i] | m_bits[i];
         }
+        repair_sign_bits(out);
         SASSERT(!has_overflow(out));
     }
 
@@ -421,9 +429,28 @@ namespace bv {
     void sls_valuation::get_variant(bvect& dst, random_gen& r) const {
         for (unsigned i = 0; i < nw; ++i)
             dst[i] = (random_bits(r) & ~fixed[i]) | (fixed[i] & m_bits[i]);
+        repair_sign_bits(dst);
         clear_overflow_bits(dst);
     }
 
+    void sls_valuation::repair_sign_bits(bvect& dst) const {
+        if (m_signed_prefix == 0)
+            return;
+        bool sign = dst.get(bw - 1);
+        for (unsigned i = bw; i-- >= bw - m_signed_prefix; ) {
+            if (dst.get(i) != sign) {
+                if (fixed.get(i)) {
+                    for (unsigned i = bw; i-- >= bw - m_signed_prefix; )
+                        if (!fixed.get(i))
+                            dst.set(i, !sign);
+                    return;
+                }
+                else
+                    dst.set(i, sign);
+            }
+        }
+    }
+
     //
     // new_bits != bits => ~fixed
     // 0 = (new_bits ^ bits) & fixed

src/ast/sls/sls_valuation.h

@@ -96,11 +96,14 @@ namespace bv {
     protected:
         bvect m_bits;
         bvect m_lo, m_hi;        // range assignment to bit-vector, as wrap-around interval
+        unsigned m_signed_prefix = 0;
 
         unsigned mask;
         bool round_up(bvect& dst) const;
         bool round_down(bvect& dst) const;
 
+        void repair_sign_bits(bvect& dst) const;
+
 
     public:
         unsigned bw;                     // bit-width
@@ -111,6 +114,7 @@ namespace bv {
         sls_valuation(unsigned bw);
 
         void set_bw(unsigned bw);
+        void set_signed(unsigned prefix) { m_signed_prefix = prefix; }
 
         unsigned num_bytes() const { return (bw + 7) / 8; }