updates to sls

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

Author: NikolajBjorner

src/ast/simplifiers/solve_eqs.cpp

@@ -329,6 +329,7 @@ namespace euf {
         m_config.m_context_solve = p.get_bool("context_solve", tp.solve_eqs_context_solve());
         for (auto* ex : m_extract_plugins)
             ex->updt_params(p);
+        m_rewriter.updt_params(p);
     }
 
     void solve_eqs::collect_param_descrs(param_descrs& r) {

src/ast/sls/bv_sls.cpp

@@ -25,12 +25,15 @@ Module Name:
 
 namespace bv {
 
-    sls::sls(ast_manager& m): 
+    sls::sls(ast_manager& m, params_ref const& p): 
         m(m), 
         bv(m),
         m_terms(m),
-        m_eval(m)
-    {}
+        m_eval(m),
+        m_engine(m, p)
+    {
+        updt_params(p);
+    }
 
     void sls::init() {
         m_terms.init(); 
@@ -67,20 +70,48 @@ namespace bv {
         }
     }
 
+    void sls::init_repair_candidates() {
+        m_to_repair.reset();
+        ptr_vector<expr> todo;
+        expr_fast_mark1 mark;
+        for (auto index : m_repair_roots) 
+            todo.push_back(m_terms.term(index));
+        for (unsigned i = 0; i < todo.size(); ++i) {
+            expr* e = todo[i];
+            if (mark.is_marked(e))
+                continue;
+            mark.mark(e);
+            if (!is_app(e))
+                continue;
+            for (expr* arg : *to_app(e))
+                todo.push_back(arg);
+
+            if (is_uninterp_const(e))
+                m_to_repair.insert(e->get_id());
+
+        }
+    }
+
+
     void sls::reinit_eval() {
+        init_repair_candidates();
+
+        if (m_to_repair.empty())
+            return;
+           
         std::function<bool(expr*, unsigned)> eval = [&](expr* e, unsigned i) {
-            auto should_keep = [&]() {
-                return m_rand() % 100 <= 92;
-            };
-            if (m.is_bool(e)) {
-                if (m_eval.is_fixed0(e) || should_keep())
-                    return m_eval.bval0(e);
-            }
+            unsigned id = e->get_id();
+            bool keep = (m_rand() % 100 <= 50) || !m_to_repair.contains(id);
+            if (m.is_bool(e) && (m_eval.is_fixed0(e) || keep))
+                return m_eval.bval0(e);
             else if (bv.is_bv(e)) {
                 auto& w = m_eval.wval(e);
-                if (w.fixed.get(i) || should_keep())
-                    return w.get_bit(i);                
-            }
+                if (w.fixed.get(i) || keep)
+                    return w.get_bit(i);
+                //auto const& z = m_engine.get_value(e);
+                //return rational(z).get_bit(i);
+            }            
+            
             return m_rand() % 2 == 0;
         };
         m_eval.init_eval(m_terms.assertions(), eval);
@@ -119,15 +150,14 @@ namespace bv {
         return { false, nullptr };
     }
 
-    lbool sls::search() {
+    lbool sls::search1() {
         // init and init_eval were invoked
         unsigned n = 0;
         for (; n++ < m_config.m_max_repairs && m.inc(); ) {
             auto [down, e] = next_to_repair();
             if (!e)
                 return l_true;
 
-
             trace_repair(down, e);
 
             ++m_stats.m_moves;
@@ -140,16 +170,32 @@ namespace bv {
         return l_undef;
     }
 
+    lbool sls::search2() {
+        lbool res = l_undef;
+        if (m_stats.m_restarts == 0)
+            res = m_engine();
+        else if (m_stats.m_restarts % 1000 == 0)
+            res = m_engine.search_loop();
+        if (res != l_undef) 
+            m_engine_model = true;          
+        return res;
+    }
+
 
     lbool sls::operator()() {
         lbool res = l_undef;
         m_stats.reset();
         m_stats.m_restarts = 0;
+        m_engine_model = false;
+
         do {
-            res = search();
+            res = search1();
             if (res != l_undef)
                 break;
             trace();
+            res = search2();
+            if (res != l_undef)
+                break;
             reinit_eval();
         } 
         while (m.inc() && m_stats.m_restarts++ < m_config.m_max_restarts);
@@ -158,34 +204,60 @@ 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 
+            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;
         }        
 
-        unsigned s = m_rand(n);
-        for (unsigned i = 0; i < n; ++i) {
-            auto j = (i + s) % n;
-            if (m_eval.try_repair(e, j)) {
-                set_repair_down(e->get_arg(j));
+        if (n == 2) {
+            auto d1 = get_depth(e->get_arg(0));
+            auto d2 = get_depth(e->get_arg(1));
+            unsigned s = m_rand(d1 + d2 + 2);
+            if (s <= d1 && m_eval.try_repair(e, 0)) {
+                set_repair_down(e->get_arg(0));
+                return;
+            }
+            if (m_eval.try_repair(e, 1)) {
+                set_repair_down(e->get_arg(1));
+                return;
+            }
+            if (m_eval.try_repair(e, 0)) {
+                set_repair_down(e->get_arg(0));
                 return;
             }
         }
-        // search a new root / random walk to repair        
+        else {
+            unsigned s = m_rand(n);
+            for (unsigned i = 0; i < n; ++i) {
+                auto j = (i + s) % n;
+                if (m_eval.try_repair(e, j)) {
+                    set_repair_down(e->get_arg(j));
+                    return;
+                }
+            }
+        }
+        // repair was not successful, so reset the state to find a different way to repair
+        init_repair();
     }
 
     void sls::try_repair_up(app* e) {       
 
-        if (m_terms.is_assertion(e) || !m_eval.repair_up(e)) 
-            m_repair_roots.insert(e->get_id());        
+        if (m_terms.is_assertion(e)) 
+            m_repair_roots.insert(e->get_id());    
+        else if (!m_eval.repair_up(e)) {
+            //m_repair_roots.insert(e->get_id());
+            init_repair();
+        }
         else {
             if (!eval_is_correct(e)) {
                 verbose_stream() << "incorrect eval #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
@@ -224,7 +296,10 @@ namespace bv {
     }
 
     model_ref sls::get_model() {
-        model_ref mdl = alloc(model, m);
+        if (m_engine_model)
+            return m_engine.get_model();
+
+        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))) {
@@ -273,7 +348,12 @@ namespace bv {
     void sls::updt_params(params_ref const& _p) {
         sls_params p(_p);
         m_config.m_max_restarts = p.max_restarts();
+        m_config.m_max_repairs = p.max_repairs();
         m_rand.set_seed(p.random_seed());
+        m_terms.updt_params(_p);
+        params_ref q = _p;
+        q.set_uint("max_restarts", 10);
+        m_engine.updt_params(q);
     }
 
     void sls::trace_repair(bool down, expr* e) {

src/ast/sls/bv_sls.h

@@ -26,6 +26,7 @@ Module Name:
 #include "ast/sls/sls_valuation.h"
 #include "ast/sls/bv_sls_terms.h"
 #include "ast/sls/bv_sls_eval.h"
+#include "ast/sls/sls_engine.h"
 #include "ast/bv_decl_plugin.h"
 #include "model/model.h"
 
@@ -49,6 +50,8 @@ namespace bv {
         ptr_vector<expr>    m_todo;
         random_gen          m_rand;
         config              m_config;
+        sls_engine          m_engine;
+        bool                m_engine_model = false;
 
         std::pair<bool, app*> next_to_repair();
 
@@ -59,19 +62,23 @@ namespace bv {
         void try_repair_up(app* e);
         void set_repair_down(expr* e) { m_repair_down = e->get_id(); }
 
-        lbool search();
+        lbool search1();
+        lbool search2();
         void reinit_eval();
         void init_repair();
         void trace();
         void trace_repair(bool down, expr* e);
 
+        indexed_uint_set m_to_repair;
+        void init_repair_candidates();
+
     public:
-        sls(ast_manager& m);
+        sls(ast_manager& m, params_ref const& p);
 
         /**
         * Add constraints
         */
-        void assert_expr(expr* e) { m_terms.assert_expr(e); }
+        void assert_expr(expr* e) { m_terms.assert_expr(e); m_engine.assert_expr(e); }
 
         /*
         * Invoke init after all expressions are asserted. 
@@ -91,10 +98,10 @@ namespace bv {
         lbool operator()();
 
         void updt_params(params_ref const& p);
-        void collect_statistics(statistics & st) const { m_stats.collect_statistics(st); }
-        void reset_statistics() { m_stats.reset(); }
+        void collect_statistics(statistics& st) const { m_stats.collect_statistics(st); m_engine.collect_statistics(st); }
+        void reset_statistics() { m_stats.reset(); m_engine.reset_statistics(); }
 
-        sls_stats const& get_stats() const { return m_stats; }
+        unsigned get_num_moves() { return m_stats.m_moves + m_engine.get_stats().m_moves; }
 
         std::ostream& display(std::ostream& out);
 

src/ast/sls/bv_sls_eval.cpp

@@ -24,8 +24,8 @@ namespace bv {
     {}   
 
     void sls_eval::init_eval(expr_ref_vector const& es, std::function<bool(expr*, unsigned)> const& eval) {
-        sort_assertions(es);
-        for (expr* e : m_todo) {
+        auto& terms = sort_assertions(es);
+        for (expr* e : terms) {
             if (!is_app(e))
                 continue;
             app* a = to_app(e);
@@ -49,7 +49,7 @@ namespace bv {
                 TRACE("sls", tout << "Unhandled expression " << mk_pp(e, m) << "\n");
             }
         }
-        m_todo.reset();
+        terms.reset();
     }
 
     /**
@@ -1698,7 +1698,7 @@ 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);

src/ast/sls/bv_sls_fixed.cpp

@@ -108,6 +108,13 @@ namespace bv {
             else if (bv.is_numeral(t, a))
                 init_range(s, -a, nullptr, rational(0), false);
         }
+        else if (sign && m.is_eq(e, s, t)) {
+            if (bv.is_numeral(s, a))
+                // 1 <= t - a
+                init_range(nullptr, rational(1), t, -a, false);
+            else if (bv.is_numeral(t, a))
+                init_range(nullptr, rational(1), s, -a, false);
+        }
         else if (bv.is_bit2bool(e, s, idx)) {
             auto& val = wval(s);
             val.try_set_bit(idx, !sign);
@@ -157,7 +164,6 @@ namespace bv {
             else
                 v.add_range(-b, -a);
         }
-        
     }
 
     void sls_fixed::get_offset(expr* e, expr*& x, rational& offset) {