updates

src/ast/sls/bv_sls.cpp

@@ -40,8 +40,6 @@ namespace bv {
         m_eval.init_eval(m_terms.assertions(), eval);
         m_eval.tighten_range(m_terms.assertions());
         init_repair();
-        display(verbose_stream());
-        exit(0);
     }
 
     void sls::init_repair() {

src/ast/sls/bv_sls_eval.cpp

@@ -1598,7 +1598,7 @@ namespace bv {
             b.clear_overflow_bits(m_tmp);
             r = b.try_set(m_tmp);
         }
-        verbose_stream() << e << " := " << a << " " << b << "\n";
+        //verbose_stream() << e << " := " << a << " " << b << "\n";
         return r;
     }
 
@@ -1625,7 +1625,12 @@ namespace bv {
             a.get(m_tmp);
         for (unsigned i = 0; i < e.bw; ++i)
             m_tmp.set(i + lo, e.get(i));
-        return a.try_set(m_tmp);
+        if (a.try_set(m_tmp))
+            return true;
+        a.get_variant(m_tmp, m_rand);       
+        bool res = a.set_repair(random_bool(), m_tmp);
+        // verbose_stream() << "try set " << res << " " << m_tmp[0] << " " << a << "\n";
+        return res;
     }
 
     void sls_eval::set_div(bvect const& a, bvect const& b, unsigned bw,
@@ -1660,19 +1665,22 @@ namespace bv {
         }
         if (bv.is_bv(e)) {
             auto& v = eval(to_app(e));
+            // verbose_stream() << "committing: " << v << "\n";
             for (unsigned i = 0; i < v.nw; ++i)
                 if (0 != (v.fixed[i] & (v.bits()[i] ^ v.eval[i]))) {
                     v.bits().copy_to(v.nw, v.eval);
                     return false;
                 }
-            v.commit_eval();
-            return true;
+            if (v.commit_eval())
+                return true;
+            v.bits().copy_to(v.nw, v.eval);
+            return false;
         }
         return false;
     }
 
     sls_valuation& sls_eval::wval(expr* e) const { 
-        if (!m_values[e->get_id()]) verbose_stream() << mk_bounded_pp(e, m) << "\n";  
+        // if (!m_values[e->get_id()]) verbose_stream() << mk_bounded_pp(e, m) << "\n";  
         return *m_values[e->get_id()]; 
     }
 

src/ast/sls/bv_sls_fixed.cpp

@@ -25,7 +25,6 @@ namespace bv {
     {}
 
     void sls_fixed::init(expr_ref_vector const& es) {
-        init_ranges(es);
         ev.sort_assertions(es);
         for (expr* e : ev.m_todo) {
             if (!is_app(e))
@@ -40,6 +39,7 @@ namespace bv {
                 ;
         }
         ev.m_todo.reset();
+        init_ranges(es);
     }
 
 
@@ -185,7 +185,6 @@ 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.tighten_range();
         }
     }
 
@@ -420,6 +419,5 @@ namespace bv {
             UNREACHABLE();
             break;
         }      
-        v.tighten_range();
     }
 }

src/ast/sls/sls_valuation.cpp

@@ -99,6 +99,8 @@ namespace bv {
         for (unsigned i = 0; i < nw; ++i)
             if (0 != (fixed[i] & (m_bits[i] ^ eval[i])))
                 return false;        
+        if (!in_range(eval))
+            return false;
         for (unsigned i = 0; i < nw; ++i) 
             m_bits[i] = eval[i]; 
         SASSERT(well_formed()); 
@@ -110,6 +112,7 @@ namespace bv {
         auto c = m.compare(m_lo.data(), nw, m_hi.data(), nw);
         SASSERT(!has_overflow(bits));
         // full range
+
         if (c == 0)
             return true;
         // lo < hi: then lo <= bits & bits < hi
@@ -328,13 +331,35 @@ namespace bv {
     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]);
-        bool ok = try_down ? round_down(dst) : round_up(dst);
-        if (!ok)
-            VERIFY(try_down ? round_up(dst) : round_down(dst));
-        DEBUG_CODE(SASSERT(0 == (mask & (fixed[nw-1] & (m_bits[nw-1] ^ dst[nw-1])))); for (unsigned i = 0; i + 1 < nw; ++i) SASSERT(0 == (fixed[i] & (m_bits[i] ^ dst[i]))););
-        set(eval, dst);
-        SASSERT(well_formed());
-        return true;
+
+        if (in_range(dst)) {
+            set(eval, dst);
+            return true;
+        }
+        bool repaired = false;
+        dst.set_bw(bw);
+        if (m_lo < m_hi) {
+            for (unsigned i = bw; m_hi <= dst && !in_range(dst) && i-- > 0; )
+                if (!fixed.get(i) && dst.get(i))
+                    dst.set(i, false);
+            for (unsigned i = 0; i < bw && dst < m_lo && !in_range(dst); ++i)
+                if (!fixed.get(i) && !dst.get(i))
+                    dst.set(i, true);        
+        }
+        else {
+            for (unsigned i = 0; !in_range(dst); ++i)
+                if (!fixed.get(i) && !dst.get(i))
+                    dst.set(i, true);
+            for (unsigned i = bw; !in_range(dst) && i-- > 0;)
+                if (!fixed.get(i) && dst.get(i))
+                    dst.set(i, false);
+        }
+        if (in_range(dst)) {
+            set(eval, dst);
+            repaired = true;
+        }
+        dst.set_bw(0);
+        return repaired;
     }
 
     void sls_valuation::min_feasible(bvect& out) const {
@@ -406,6 +431,7 @@ namespace bv {
     //
     bool sls_valuation::can_set(bvect const& new_bits) const {
         SASSERT(!has_overflow(new_bits));
+        // verbose_stream() << "can set " << bw << " " << new_bits[0] << " " << in_range(new_bits) << "\n";
         for (unsigned i = 0; i < nw; ++i)
             if (0 != ((new_bits[i] ^ m_bits[i]) & fixed[i]))
                 return false;
@@ -446,10 +472,8 @@ namespace bv {
         if (h == l)
             return;
 
-        verbose_stream() << "[" << l << ", " << h << "[\n";
-        verbose_stream() << *this << "\n";
-
-        SASSERT(is_zero(fixed)); // ranges can only be added before fixed bits are set.
+        //verbose_stream() << "[" << l << ", " << h << "[\n";
+        //verbose_stream() << *this << "\n";
 
         if (m_lo == m_hi) {
             set_value(m_lo, l);
@@ -481,13 +505,14 @@ namespace bv {
 
         SASSERT(!has_overflow(m_lo));
         SASSERT(!has_overflow(m_hi));
-        if (!in_range(m_bits)) 
-            set(m_bits, m_lo);
+
+        tighten_range();
         SASSERT(well_formed());
-        verbose_stream() << *this << "\n";
+        // verbose_stream() << *this << "\n";
     }
 
     //
+    // update bits based on ranges
     // tighten lo/hi based on fixed bits.
     //   lo[bit_i] != fixedbit[bit_i] 
     //     let bit_i be most significant bit position of disagreement.
@@ -502,35 +527,19 @@ namespace bv {
     //
     void sls_valuation::tighten_range() {
 
-        verbose_stream() << "tighten " << *this << "\n";
+        // verbose_stream() << "tighten " << *this << "\n";
         if (m_lo == m_hi)
             return;
-        for (unsigned i = bw; i-- > 0; ) {
-            if (!fixed.get(i))
-                continue;
-            if (m_bits.get(i) == m_lo.get(i))
-                continue;
-            if (m_bits.get(i)) {
-                m_lo.set(i, true);
-                for (unsigned j = i; j-- > 0; )
-                    m_lo.set(j, fixed.get(j) && m_bits.get(j));
-            }
-            else {
-                for (unsigned j = bw; j-- > 0; )
-                    m_lo.set(j, fixed.get(j) && m_bits.get(j));
-            }
-            break;
-        }
 
         if (!in_range(m_bits)) {
-            verbose_stream() << "not in range\n";
+            // 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";
-
+                compatible = 0 == (fixed[i] & (m_bits[i] ^ m_lo[i]));
+            //verbose_stream() << (fixed[0] & (m_bits[0] ^ m_lo[0])) << "\n";
+            //verbose_stream() << bw << " " << m_lo[0] << " " << m_bits[0] << "\n";
             if (compatible) {
-                verbose_stream() << "compatible\n";
+                //verbose_stream() << "compatible\n";
                 set(m_bits, m_lo);
             }
             else {
@@ -561,6 +570,24 @@ namespace bv {
                 set(m_bits, tmp);
             }
         }
+        // update lo, hi to be feasible.
+
+        for (unsigned i = bw; i-- > 0; ) {
+            if (!fixed.get(i))
+                continue;
+            if (m_bits.get(i) == m_lo.get(i))
+                continue;
+            if (m_bits.get(i)) {
+                m_lo.set(i, true);
+                for (unsigned j = i; j-- > 0; )
+                    m_lo.set(j, fixed.get(j) && m_bits.get(j));
+            }
+            else {
+                for (unsigned j = bw; j-- > 0; )
+                    m_lo.set(j, fixed.get(j) && m_bits.get(j));
+            }
+            break;
+        }
 
         SASSERT(well_formed());
     }

src/tactic/core/simplify_tactic.cpp

@@ -42,6 +42,10 @@ struct simplify_tactic::imp {
         m_num_steps = 0;
     }
 
+    void collect_statistics(statistics& st) {
+        st.update("rewriter.steps", m_num_steps);
+    }
+
     void operator()(goal & g) {
         tactic_report report("simplifier", g);
         m_num_steps = 0;
@@ -108,6 +112,11 @@ void simplify_tactic::cleanup() {
     new (m_imp) imp(m, p);
 }
 
+void simplify_tactic::collect_statistics(statistics& st) const {
+    if (m_imp)
+        m_imp->collect_statistics(st);
+}
+
 unsigned simplify_tactic::get_num_steps() const {
     return m_imp->get_num_steps();
 }

src/tactic/core/simplify_tactic.h

@@ -81,6 +81,8 @@ class simplify_tactic : public tactic {
     static void get_param_descrs(param_descrs & r);
 
     void collect_param_descrs(param_descrs & r) override { get_param_descrs(r); }
+
+    void collect_statistics(statistics& st) const override;
 
     void operator()(goal_ref const & in, goal_ref_buffer & result) override;
 

src/tactic/dependent_expr_state_tactic.h

@@ -62,7 +62,7 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
         if (m_simp)
             pop(1);
     }
-
+    
     /**
     * size(), [](), update() and inconsistent() implement the abstract interface of dependent_expr_state
     */
@@ -140,6 +140,12 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
         cleanup();
     }
 
+    void collect_statistics(statistics& st) const override {
+        if (m_simp)
+            m_simp->collect_statistics(st);
+        st.copy(m_st);
+    }
+
     void cleanup() override {
         if (m_simp) {
             m_simp->collect_statistics(m_st);
@@ -151,13 +157,6 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
         m_dep = dependent_expr(m, m.mk_true(), nullptr, nullptr);
     }
 
-    void collect_statistics(statistics& st) const override {
-        if (m_simp)
-            m_simp->collect_statistics(st);
-        else
-            st.copy(m_st);
-    }
-
     void reset_statistics() override {
         if (m_simp)
             m_simp->reset_statistics();

src/tactic/tactic.h

@@ -62,7 +62,7 @@ class tactic : public user_propagator::core {
     */
     virtual void operator()(goal_ref const & in, goal_ref_buffer& result) = 0;
 
-    virtual void collect_statistics(statistics & st) const { }
+    virtual void collect_statistics(statistics& st) const {  }
     virtual void reset_statistics() {}
     virtual void cleanup() = 0;
     virtual void reset() { cleanup(); }
@@ -130,6 +130,7 @@ class skip_tactic : public tactic {
     void cleanup() override {}
     tactic * translate(ast_manager & m) override { return this; } 
     char const* name() const override { return "skip"; }
+    void collect_statistics(statistics& st) const override {}
 };
 
 tactic * mk_skip_tactic();

src/tactic/tactical.cpp

@@ -1190,6 +1190,9 @@ class fail_if_tactic : public tactic {
     tactic * translate(ast_manager & m) override {
         return this;
     }
+
+    void collect_statistics(statistics& st) const override {
+    }
 };
 
 tactic * fail_if(probe * p) {
@@ -1216,6 +1219,7 @@ class if_no_proofs_tactical : public unary_tactical {
     }
 
     tactic * translate(ast_manager & m) override { return translate_core<if_no_proofs_tactical>(m); }
+
 };
 
 class if_no_unsat_cores_tactical : public unary_tactical {