reorg sls

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

src/ast/bv_decl_plugin.h

@@ -438,6 +438,7 @@ class bv_recognizers {
     MATCH_BINARY(is_bv_xor);
     MATCH_BINARY(is_bv_nand);
     MATCH_BINARY(is_bv_nor);
+    MATCH_BINARY(is_concat);
 
 
     MATCH_BINARY(is_bv_uremi);

src/ast/sls/bv_sls.cpp

@@ -56,18 +56,13 @@ namespace bv {
             }
         }
         for (auto* t : m_terms.terms()) {
-            if (t && !re_eval_is_correct(t)) 
+            if (t && !m_eval.re_eval_is_correct(t)) 
                 m_repair_roots.insert(t->get_id());            
         }
     }
 
     void sls::init_repair_goal(app* t) {
-        if (m.is_bool(t)) 
-            m_eval.set(t, m_eval.bval1(t));        
-        else if (bv.is_bv(t)) {
-            auto& v = m_eval.wval(t);
-            v.bits().copy_to(v.nw, v.eval);
-        }
+        m_eval.init_eval(t);
     }
 
     void sls::init_repair_candidates() {
@@ -149,7 +144,7 @@ namespace bv {
                 SASSERT(m_eval.bval0(e));
                 return { true, e };
             }
-            if (!re_eval_is_correct(e)) {
+            if (!m_eval.re_eval_is_correct(e)) {
                 init_repair_goal(e);
                 return { true, e };
             }
@@ -162,18 +157,16 @@ namespace bv {
     lbool sls::search1() {
         // init and init_eval were invoked
         unsigned n = 0;
-        for (; n < m_config.m_max_repairs && m.inc(); ) {
+        for (; n < m_config.m_max_repairs && m.inc(); ++n) {
             auto [down, e] = next_to_repair();
             if (!e)
                 return l_true;
 
             IF_VERBOSE(20, trace_repair(down, e));
 
             ++m_stats.m_moves;
-            if (down) {
-                try_repair_down(e);
-                ++n;
-            }
+            if (down) 
+                try_repair_down(e);            
             else
                 try_repair_up(e);            
         }
@@ -219,12 +212,7 @@ namespace bv {
     void sls::try_repair_down(app* e) {
         unsigned n = e->get_num_args();
         if (n == 0) {
-            if (m.is_bool(e)) {
-                m_eval.set(e, m_eval.bval1(e));
-            }
-            else {
-                VERIFY(m_eval.wval(e).commit_eval());
-            }
+            m_eval.commit_eval(e);
 
             IF_VERBOSE(3, verbose_stream() << "done\n");
             for (auto p : m_terms.parents(e))
@@ -271,44 +259,24 @@ namespace bv {
             m_repair_roots.insert(e->get_id());    
         else if (!m_eval.repair_up(e)) {
             IF_VERBOSE(2, verbose_stream() << "repair-up "; trace_repair(true, e));
-            init_repair();
+            if (m_rand(10) != 0) {
+                m_eval.set_random(e);
+
+                m_repair_roots.insert(e->get_id());
+            }
+            else
+                init_repair();
         }
         else {
-            if (!eval_is_correct(e)) {
+            if (!m_eval.eval_is_correct(e)) {
                 verbose_stream() << "incorrect eval #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
             }
-            SASSERT(eval_is_correct(e));
+            SASSERT(m_eval.eval_is_correct(e));
             for (auto p : m_terms.parents(e))
                 m_repair_up.insert(p->get_id());
         }
     }
 
-    bool sls::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.wval(e);
-            return v.eval == v.bits();
-        }
-        UNREACHABLE();
-        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() {
         if (m_engine_model)
@@ -317,24 +285,17 @@ namespace bv {
         model_ref mdl = alloc(model, m);         
         auto& terms = m_eval.sort_assertions(m_terms.assertions());
         for (expr* e : terms) {
-            if (!re_eval_is_correct(to_app(e))) {
+            if (!m_eval.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);
-                    verbose_stream() << v << "\n" << v.eval << "\n";
-                }
+                m_eval.display_value(verbose_stream(), e) << "\n";
             }
             if (!is_uninterp_const(e))
                 continue;
 
             auto f = to_app(e)->get_decl();
-            if (m.is_bool(e))
-                mdl->register_decl(f, m.mk_bool_val(m_eval.bval0(e)));
-            else if (bv.is_bv(e)) {
-                auto const& v = m_eval.wval(e);
-                rational n = v.get_value();
-                mdl->register_decl(f, bv.mk_numeral(n, v.bw));
-            }
+            auto v = m_eval.get_value(to_app(e));
+            if (v)
+                mdl->register_decl(f, v);
         }
         terms.reset();
         return mdl;
@@ -350,10 +311,7 @@ namespace bv {
                 out << "u ";
             if (m_repair_roots.contains(e->get_id()))
                 out << "r ";
-            if (bv.is_bv(e))
-                out << m_eval.wval(e);
-            else if (m.is_bool(e))
-                out << (m_eval.bval0(e)?"T":"F");
+            m_eval.display_value(out, e);
             out << "\n";
         }
         terms.reset();
@@ -372,12 +330,10 @@ namespace bv {
     }
 
     std::ostream& sls::trace_repair(bool down, expr* e) {
-            verbose_stream() << (down ? "d #" : "u #")
+        verbose_stream() << (down ? "d #" : "u #")
             << e->get_id() << ": "
             << mk_bounded_pp(e, m, 1) << " ";
-        if (bv.is_bv(e)) verbose_stream() << m_eval.wval(e) << " " << (m_eval.is_fixed0(e) ? "fixed " : " ");
-        if (m.is_bool(e)) verbose_stream() << m_eval.bval0(e) << " ";
-        verbose_stream() << "\n";
+        m_eval.display_value(verbose_stream(), e) << "\n";
         return verbose_stream();
     }
 

src/ast/sls/bv_sls.h

@@ -56,8 +56,6 @@ namespace bv {
 
         std::pair<bool, app*> next_to_repair();
 
-        bool eval_is_correct(app* e);
-        bool re_eval_is_correct(app* e);
         void init_repair_goal(app* e);
         void try_repair_down(app* e);
         void try_repair_up(app* e);