na

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

src/ast/sls/bv_sls.cpp

@@ -138,6 +138,8 @@ namespace bv {
     void sls::try_repair_down(app* e) {
 
         if (eval_is_correct(e)) {
+//            if (bv.is_bv(e))
+//                verbose_stream() << mk_pp(e, m) << " := " << m_eval.wval(e) << "\n";
             m_repair_roots.remove(m_repair_root);
             m_repair_root = UINT_MAX;
             return;
@@ -147,7 +149,6 @@ namespace bv {
         if (n == 0) {
             auto& v = m_eval.wval(e);
             v.commit_eval();
-            verbose_stream() << mk_pp(e, m) << " := " << v << "\n";
             for (auto p : m_terms.parents(e))
                 m_repair_up.insert(p->get_id());
             m_repair_roots.remove(m_repair_root);
@@ -193,11 +194,25 @@ namespace bv {
         return false;
     }
 
+
+    bool sls::re_eval_is_correct(app* e) {
+        if (!m_eval.can_eval1(e))
+            return false;
+        if (m.is_bool(e))
+            return m_eval.bval0(e) == m_eval.bval1(e);
+        if (bv.is_bv(e)) {
+            auto const& v = m_eval.eval(e);
+            return v.eval == v.bits();
+        }
+        UNREACHABLE();
+        return false;
+    }
+
     model_ref sls::get_model() {
         model_ref mdl = alloc(model, m);
         auto& terms = m_eval.sort_assertions(m_terms.assertions());
         for (expr* e : terms) {
-            if (!eval_is_correct(to_app(e))) {
+            if (!re_eval_is_correct(to_app(e))) {
                 verbose_stream() << "missed evaluation #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
                 if (bv.is_bv(e)) {
                     auto const& v = m_eval.wval(e);

src/ast/sls/bv_sls.h

@@ -54,6 +54,7 @@ namespace bv {
         std::pair<bool, app*> next_to_repair();
         
         bool eval_is_correct(app* e);
+        bool re_eval_is_correct(app* e);
         void try_repair_down(app* e);
         void try_repair_up(app* e);
         void set_repair_down(expr* e) { m_repair_down = e->get_id(); }

src/ast/sls/bv_sls_eval.cpp

@@ -299,7 +299,6 @@ namespace bv {
     sls_valuation& sls_eval::eval(app* e) const {
         auto& val = *m_values[e->get_id()];        
         eval(e, val);
-        verbose_stream() << "eval " << mk_pp(e, m) << " := " << val << " " << val.eval << "\n";
         return val;        
     }
 
@@ -1021,7 +1020,6 @@ namespace bv {
         unsigned parity_e = b.parity(e);
         unsigned parity_b = b.parity(b.bits());
 
-        verbose_stream() << e << " := " << a << " * " << b << "\n";
         if (b.is_zero(e)) {
             a.get_variant(m_tmp, m_rand);
             for (unsigned i = 0; i < b.bw - parity_b; ++i)
@@ -1092,6 +1090,8 @@ namespace bv {
         y.set_bw(0);
         // x*a + y*b = 1
     
+        tb.set_bw(b.bw);
+        tb.set_bw(0);
 #if Z3DEBUG
         b.get(y);
         if (parity_b > 0)
@@ -1099,7 +1099,7 @@ namespace bv {
         a.set_mul(m_tmp, tb, y);
         SASSERT(a.is_one(m_tmp));
 #endif
-        b.get(m_tmp2);
+        e.copy_to(b.nw, m_tmp2);
         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);

src/ast/sls/sls_valuation.cpp

@@ -338,10 +338,8 @@ namespace bv {
     }
 
     void sls_valuation::min_feasible(bvect& out) const {
-        if (m_lo < m_hi) {
+        if (m_lo < m_hi) 
-            for (unsigned i = 0; i < nw; ++i)
+            m_lo.copy_to(nw, out);        
-                out[i] = m_lo[i];
-        }
         else {
             for (unsigned i = 0; i < nw; ++i)
                 out[i] = fixed[i] & m_bits[i];
@@ -351,8 +349,7 @@ namespace bv {
 
     void sls_valuation::max_feasible(bvect& out) const {
         if (m_lo < m_hi) {
-            for (unsigned i = 0; i < nw; ++i)
+            m_hi.copy_to(nw, out);
-                out[i] = m_hi[i];
             sub1(out);
         }
         else {
@@ -386,8 +383,7 @@ namespace bv {
     }
 
     void sls_valuation::get(bvect& dst) const {
-        for (unsigned i = 0; i < nw; ++i)
+        m_bits.copy_to(nw, dst);
-            dst[i] = m_bits[i];
     }
 
     digit_t sls_valuation::random_bits(random_gen& rand) {

src/ast/sls/sls_valuation.h

@@ -37,6 +37,12 @@ namespace bv {
         bvect(unsigned sz) : svector(sz, (unsigned)0) {}
         void set_bw(unsigned bw);
 
+        void copy_to(unsigned nw, bvect & dst) const {
+            SASSERT(nw <= this->size());
+            for (unsigned i = 0; i < nw; ++i)
+                dst[i] = (*this)[i];
+        }
+
         void set(unsigned bit_idx, bool val) {
             auto _val = static_cast<digit_t>(0 - static_cast<digit_t>(val));
             get_bit_word(bit_idx) ^= (_val ^ get_bit_word(bit_idx)) & get_pos_mask(bit_idx);
@@ -282,8 +288,11 @@ namespace bv {
 
         std::ostream& display(std::ostream& out) const {
             out << m_bits;
-            out << " fix:";
+            out << " ev: " << eval;
-            out << fixed;
+            if (!is_zero(fixed)) {
+                out << " fix:";
+                out << fixed;
+            }
             if (m_lo != m_hi) 
                 out << " [" << m_lo << ", " << m_hi << "[";            
             return out;