na

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

src/ast/sls/bv_sls.cpp

@@ -38,8 +38,10 @@ namespace bv {
 
     void sls::init_eval(std::function<bool(expr*, unsigned)>& eval) {
         m_eval.init_eval(m_terms.assertions(), eval);
-        m_eval.init_fixed(m_terms.assertions());
+        m_eval.tighten_range(m_terms.assertions());
         init_repair();
+        display(verbose_stream());
+        exit(0);
     }
 
     void sls::init_repair() {
@@ -160,8 +162,11 @@ namespace bv {
 
         unsigned n = e->get_num_args();
         if (n == 0) {
-            auto& v = m_eval.wval(e);
-            VERIFY(v.commit_eval());
+            if (m.is_bool(e)) 
+                m_eval.set(e, m_eval.bval1(e));                            
+            else 
+                VERIFY(m_eval.wval(e).commit_eval());
+            
             for (auto p : m_terms.parents(e))
                 m_repair_up.insert(p->get_id());
             return;

src/ast/sls/bv_sls_eval.cpp

@@ -643,11 +643,21 @@ namespace bv {
             mk_rotate_left(val.bw - n.get_unsigned());
             break;
         }
+        case OP_BCOMP: {
+            auto const& a = wval(e->get_arg(0));
+            auto const& b = wval(e->get_arg(1));
+            if (a.bits() == b.bits())
+                val.set(val.eval, 1);
+            else
+                val.set(val.eval, 0);
+            break;
+        }
         case OP_BREDAND:
         case OP_BREDOR:
         case OP_BXNOR:
         case OP_INT2BV:
-        case OP_BCOMP:
+
+            verbose_stream() << mk_bounded_pp(e, m) << "\n";
             NOT_IMPLEMENTED_YET();
             break;
         case OP_BIT2BOOL:
@@ -829,8 +839,10 @@ namespace bv {
             return try_repair_umul_ovfl(!bval0(e), wval(e, 0), wval(e, 1), i);
         case OP_BUMUL_OVFL:
             return try_repair_umul_ovfl(bval0(e), wval(e, 0), wval(e, 1), i);
+        case OP_BCOMP:
+            return try_repair_comp(eval_value(e), wval(e, 0), wval(e, 1), i);
         case OP_BUADD_OVFL:
-        case OP_BCOMP:            
+         
         case OP_BNAND:
         case OP_BREDAND:
         case OP_BREDOR:
@@ -887,29 +899,33 @@ namespace bv {
         else if (bv.is_bv(child)) {
             auto & a = wval(e->get_arg(i));
             auto & b = wval(e->get_arg(1 - i));
-            if (is_true) 
-                return a.try_set(b.bits());
-            else {
-                bool try_above = m_rand() % 2 == 0;
-                if (try_above) {
-                    a.set_add(m_tmp, b.bits(), m_one);
-                    if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand))
-                        return true;
-                }
-                a.set_sub(m_tmp, b.bits(), m_one);
-                if (!a.is_zero(m_tmp) && a.set_random_at_most(m_tmp, m_tmp2, m_rand))
-                    return true;
-                if (!try_above) {
-                    a.set_add(m_tmp, b.bits(), m_one);
-                    if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand))
-                        return true;
-                }
-                return false;
-            }
+            return try_repair_eq(is_true, a, b);
         }
         return false;
     }
 
+    bool sls_eval::try_repair_eq(bool is_true, bvval& a, bvval const& b) {
+        if (is_true)
+            return a.try_set(b.bits());
+        else {
+            bool try_above = m_rand() % 2 == 0;
+            if (try_above) {
+                a.set_add(m_tmp, b.bits(), m_one);
+                if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand))
+                    return true;
+            }
+            a.set_sub(m_tmp, b.bits(), m_one);
+            if (!a.is_zero(m_tmp) && a.set_random_at_most(m_tmp, m_tmp2, m_rand))
+                return true;
+            if (!try_above) {
+                a.set_add(m_tmp, b.bits(), m_one);
+                if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand))
+                    return true;
+            }
+            return false;
+        }
+    }
+
     bool sls_eval::try_repair_xor(app* e, unsigned i) {
         bool ev = bval0(e);
         bool bv = bval0(e->get_arg(1 - i));
@@ -1285,6 +1301,7 @@ namespace bv {
                     m_tmp.set(i, e.get(sh + i));
                 for (unsigned i = a.bw - sh; i < a.bw; ++i)
                     m_tmp.set(i, a.get_bit(i));
+                a.clear_overflow_bits(m_tmp);
                 return a.try_set(m_tmp);
             }
         }
@@ -1335,6 +1352,12 @@ namespace bv {
         return try_repair_ashr(e, a, b, i);
     }
 
+    bool sls_eval::try_repair_comp(bvect const& e, bvval& a, bvval& b, unsigned i) {
+        SASSERT(e[0] == 0 || e[0] == 1);
+        SASSERT(e.bw == 1);
+        return try_repair_eq(e[0] == 1, i == 0 ? a : b, i == 0 ? b : a);
+    }
+
     // e = a udiv b
     // e = 0 => a != ones
     // b = 0 => e = -1        // nothing to repair on a
@@ -1368,7 +1391,8 @@ namespace bv {
             while (b.bits() < m_tmp2)
                 m_tmp2.set(b.msb(m_tmp2), false);
             while (a.set_add(m_tmp3, m_tmp, m_tmp2)) 
-                m_tmp2.set(b.msb(m_tmp2), false);            
+                m_tmp2.set(b.msb(m_tmp2), false);       
+            a.clear_overflow_bits(m_tmp3);
             return a.set_repair(true, m_tmp3);
         }
         else {
@@ -1561,18 +1585,21 @@ namespace bv {
     }
 
     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);
-            return a.try_set(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);
-            return b.try_set(m_tmp);
+            r = b.try_set(m_tmp);
         }
+        verbose_stream() << e << " := " << a << " " << b << "\n";
+        return r;
     }
 
     //
@@ -1644,6 +1671,11 @@ namespace bv {
         return false;
     }
 
+    sls_valuation& sls_eval::wval(expr* e) const { 
+        if (!m_values[e->get_id()]) verbose_stream() << mk_bounded_pp(e, m) << "\n";  
+        return *m_values[e->get_id()]; 
+    }
+
     std::ostream& sls_eval::display(std::ostream& out, expr_ref_vector const& es) {
         auto& terms = sort_assertions(es);
         for (expr* e : terms) {

src/ast/sls/bv_sls_eval.h

@@ -106,6 +106,8 @@ namespace bv {
         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_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);
         void add_p2_1(bvval const& a, bvect& t) const;
 
         bool add_overflow_on_fixed(bvval const& a, bvect const& t);
@@ -127,7 +129,7 @@ namespace bv {
 
         void init_eval(expr_ref_vector const& es, std::function<bool(expr*, unsigned)> const& eval);
 
-        void init_fixed(expr_ref_vector const& es) { m_fix.init(es); }
+        void tighten_range(expr_ref_vector const& es) { m_fix.init(es); }
 
         ptr_vector<expr>& sort_assertions(expr_ref_vector const& es);
 
@@ -139,7 +141,7 @@ namespace bv {
         
         bool bval0(expr* e) const { return m_eval[e->get_id()]; }
 
-        sls_valuation& wval(expr* e) const { return *m_values[e->get_id()]; }
+        sls_valuation& wval(expr* e) const;
 
         bool is_fixed0(expr* e) const { return m_fixed[e->get_id()]; }
 

src/ast/sls/bv_sls_fixed.cpp

@@ -112,7 +112,7 @@ namespace bv {
             auto& val = wval(s);
             val.try_set_bit(idx, !sign);
             val.fixed.set(idx, true);
-            val.init_fixed();
+            val.tighten_range();
         }
     }
 
@@ -185,7 +185,7 @@ namespace bv {
             auto& val_el = wval(e->get_arg(2));
             for (unsigned i = 0; i < val.nw; ++i)
                 val.fixed[i] = val_el.fixed[i] & val_th.fixed[i] & ~(val_el.bits(i) ^ val_th.bits(i));
-            val.init_fixed();
+            val.tighten_range();
         }
     }
 
@@ -420,6 +420,6 @@ namespace bv {
             UNREACHABLE();
             break;
         }      
-        v.init_fixed();
+        v.tighten_range();
     }
 }

src/ast/sls/sls_valuation.cpp

@@ -446,8 +446,8 @@ namespace bv {
         if (h == l)
             return;
 
-        //verbose_stream() << "[" << l << ", " << h << "[\n";
-        //verbose_stream() << *this << "\n";
+        verbose_stream() << "[" << l << ", " << h << "[\n";
+        verbose_stream() << *this << "\n";
 
         SASSERT(is_zero(fixed)); // ranges can only be added before fixed bits are set.
 
@@ -481,9 +481,10 @@ namespace bv {
 
         SASSERT(!has_overflow(m_lo));
         SASSERT(!has_overflow(m_hi));
-        if (!in_range(m_bits))
+        if (!in_range(m_bits)) 
             set(m_bits, m_lo);
         SASSERT(well_formed());
+        verbose_stream() << *this << "\n";
     }
 
     //
@@ -499,7 +500,9 @@ namespace bv {
     //  lo + 1 = hi -> set bits = lo
     //  lo < hi, set most significant bits based on hi
     //
-    void sls_valuation::init_fixed() {
+    void sls_valuation::tighten_range() {
+
+        verbose_stream() << "tighten " << *this << "\n";
         if (m_lo == m_hi)
             return;
         for (unsigned i = bw; i-- > 0; ) {
@@ -518,56 +521,47 @@ namespace bv {
             }
             break;
         }
-        bvect hi1(nw + 1);
-        bvect one(nw + 1);
-        one[0] = 1;
-        digit_t c;
-        mpn_manager().sub(m_hi.data(), nw, one.data(), nw, hi1.data(), &c);
-        clear_overflow_bits(hi1);
-        for (unsigned i = bw; i-- > 0; ) {
-            if (!fixed.get(i))
-                continue;
-            if (m_bits.get(i) == hi1.get(i))
-                continue;
-            if (hi1.get(i)) {
-                hi1.set(i, false);
-                for (unsigned j = i; j-- > 0; )
-                    hi1.set(j, !fixed.get(j) || m_bits.get(j));
+
+        if (!in_range(m_bits)) {
+            verbose_stream() << "not in range\n";
+            bool compatible = true;
+            for (unsigned i = 0; i < nw && compatible; ++i)
+                compatible = 0 == (fixed[i] && (m_bits[i] ^ m_lo[i]));
+            verbose_stream() << (fixed[0] && (m_bits[0] ^ m_lo[0])) << "\n";
+
+            if (compatible) {
+                verbose_stream() << "compatible\n";
+                set(m_bits, m_lo);
             }
             else {
-                for (unsigned j = bw; j-- > 0; )
-                    hi1.set(j, fixed.get(j) && m_bits.get(j));
+                bvect tmp(m_bits.nw);
+                tmp.set_bw(bw);
+                set(tmp, m_lo);
+                unsigned max_diff = bw;
+                for (unsigned i = 0; i < bw; ++i) {
+                    if (fixed.get(i) && (m_bits.get(i) ^ m_lo.get(i))) {
+                        tmp.set(i, m_bits.get(i));
+                        max_diff = i;
+                    }
+                }
+                SASSERT(max_diff != bw);
+
+                for (unsigned i = 0; i <= max_diff; ++i)
+                    tmp.set(i, fixed.get(i) && m_bits.get(i));
+
+                bool found0 = false;
+                for (unsigned i = max_diff + 1; i < bw; ++i) {
+                    if (found0 || m_lo.get(i) || fixed.get(i))
+                        tmp.set(i, m_lo.get(i) && fixed.get(i));
+                    else {
+                        tmp.set(i, true);
+                        found0 = true;
+                    }
+                }
+                set(m_bits, tmp);
             }
-            mpn_manager().add(hi1.data(), nw, one.data(), nw, m_hi.data(), nw + 1, &c);
-            clear_overflow_bits(m_hi);
-            break;
         }
 
-        // set fixed bits based on bounds
-        auto set_fixed_bit = [&](unsigned i, bool b) {
-            if (!fixed.get(i)) {
-                fixed.set(i, true);
-                eval.set(i, b);
-            }
-            };
-
-        // set most significant bits
-        if (m_lo < m_hi) {
-            unsigned i = bw;
-            for (; i-- > 0 && !m_hi.get(i); )
-                set_fixed_bit(i, false);
-
-            if (is_power_of2(m_hi))
-                set_fixed_bit(i, false);
-        }
-
-        // lo + 1 = hi: then bits = lo
-        mpn_manager().add(m_lo.data(), nw, one.data(), nw, hi1.data(), nw + 1, &c);
-        clear_overflow_bits(hi1);
-        if (m_hi == hi1) {
-            for (unsigned i = 0; i < bw; ++i)
-                set_fixed_bit(i, m_lo.get(i));
-        }
         SASSERT(well_formed());
     }
 

src/ast/sls/sls_valuation.h

@@ -140,7 +140,7 @@ namespace bv {
         void get(bvect& dst) const;
         void add_range(rational lo, rational hi);
         bool has_range() const { return m_lo != m_hi; }
-        void init_fixed();
+        void tighten_range();
 
         void clear_overflow_bits(bvect& bits) const {
             SASSERT(nw > 0);
@@ -156,11 +156,10 @@ namespace bv {
 
         bool is_zero() const { return is_zero(m_bits); }
         bool is_zero(bvect const& a) const { 
-            SASSERT(!has_overflow(a));
-            for (unsigned i = 0; i < nw; ++i)
+            for (unsigned i = 0; i < nw - 1; ++i)
                 if (a[i] != 0)
                     return false;
-            return true;
+            return (a[nw - 1] & mask) == 0;          
         }
 
         bool is_ones() const { return is_ones(m_bits); }