enable concurrent sls with new solver core

allow using sls engine (for bit-vectors) with the new core.

Examples

z3 sat.smt=true tactic.default_tactic=smt /v:1 smt.sls.enable=true smt.bv.solver=0 /st C:\QF_BV_SAT\bench_10.smt2
z3 sat.smt=true tactic.default_tactic=smt /v:1 smt.sls.enable=true smt.bv.solver=2 /st C:\QF_BV_SAT\bench_10.smt2
z3 C:\QF_BV_SAT\bench_11100.smt2 sat.smt=true tactic.default_tactic=smt /v:1 smt.sls.enable=true smt.bv.solver=2 /st

src/ast/sls/bv_sls.cpp

@@ -93,6 +93,18 @@ namespace bv {
 
         if (m_to_repair.empty())
             return;
+
+        // add fresh units, if any
+        bool new_assertion = false;
+        while (m_get_unit) {
+            auto e = m_get_unit();
+            if (!e)
+                break;
+            new_assertion = true;
+            assert_expr(e);
+        }
+        if (new_assertion) 
+            init();        
 
         std::function<bool(expr*, unsigned)> eval = [&](expr* e, unsigned i) {
             unsigned id = e->get_id();
@@ -212,9 +224,7 @@ namespace bv {
     void sls::try_repair_down(app* e) {
         unsigned n = e->get_num_args();
         if (n == 0) {
-            m_eval.commit_eval(e);
-
-            IF_VERBOSE(3, verbose_stream() << "done\n");
+            m_eval.commit_eval(e);           
             for (auto p : m_terms.parents(e))
                 m_repair_up.insert(p->get_id());
 

src/ast/sls/bv_sls.h

@@ -53,6 +53,7 @@ namespace bv {
         sls_engine          m_engine;
         bool                m_engine_model = false;
         bool                m_engine_init = false;
+        std::function<expr_ref()> m_get_unit;
 
         std::pair<bool, app*> next_to_repair();
 
@@ -81,7 +82,6 @@ namespace bv {
 
         /*
         * Invoke init after all expressions are asserted. 
-        * No other expressions can be asserted after init.
         */
         void init();
 
@@ -91,6 +91,11 @@ namespace bv {
         */
         void init_eval(std::function<bool(expr*, unsigned)>& eval);
 
+        /**
+        * add callback to retrieve new units
+        */
+        void init_unit(std::function<expr_ref()> get_unit) { m_get_unit = get_unit; }
+
         /**
         * Run (bounded) local search to find feasible assignments.
         */

src/ast/sls/bv_sls_fixed.cpp

@@ -58,16 +58,16 @@ namespace bv {
         expr* t, * s;
         rational v;
         if (bv.is_concat(e, t, s)) {
-            auto& val = wval(s);
-            if (val.lo() != val.hi() && (val.lo() < val.hi() || val.hi() == 0))
+            auto& vals = wval(s);
+            if (vals.lo() != vals.hi() && (vals.lo() < vals.hi() || vals.hi() == 0))
                 // lo <= e
-                add_range(e, val.lo(), rational::zero(), false);
+                add_range(e, vals.lo(), rational::zero(), false);
             auto valt = wval(t);
-#if 0
-            if (val.lo() < val.hi())
-                // e < (2^|s|) * hi
-                add_range(e, rational::zero(), val.hi() * rational::power_of_two(bv.get_bv_size(s)), false);
-#endif
+            if (valt.lo() != valt.hi() && (valt.lo() < valt.hi() || valt.hi() == 0)) {
+                // (2^|s|) * lo <= e < (2^|s|) * hi
+                auto p = rational::power_of_two(bv.get_bv_size(s));
+                add_range(e, valt.lo() * p, valt.hi() * p, false);
+            }
         }        
         else if (bv.is_bv_add(e, s, t) && bv.is_numeral(s, v)) {
             auto& val = wval(t);

src/ast/sls/bv_sls_terms.cpp

@@ -206,13 +206,15 @@ namespace bv {
                 m_todo.push_back(arg);
         }       
         // populate parents
+        m_parents.reset();
         m_parents.reserve(m_terms.size());
         for (expr* e : m_terms) {
             if (!e || !is_app(e))
                 continue;
             for (expr* arg : *to_app(e))
                 m_parents[arg->get_id()].push_back(e);                
         }
+        m_assertion_set.reset();
         for (auto a : m_assertions)
             m_assertion_set.insert(a->get_id());
     }

src/ast/sls/sls_valuation.cpp

@@ -245,6 +245,7 @@ namespace bv {
     }
 
     bool sls_valuation::set_random_at_most(bvect const& src, random_gen& r) {
+        m_tmp.set_bw(bw);
         if (!get_at_most(src, m_tmp))
             return false;
 
@@ -639,6 +640,14 @@ namespace bv {
 
         if (has_range() && !in_range(m_bits)) 
             m_bits = m_lo;
+
+        if (mod(lo() + 1, rational::power_of_two(bw)) == hi())
+            for (unsigned i = 0; i < nw; ++i)
+                fixed[i] = ~0;      
+        if (lo() < hi() && hi() < rational::power_of_two(bw - 1))
+            for (unsigned i = 0; i < bw; ++i)
+                if (hi() < rational::power_of_two(i))
+                    fixed.set(i, true);
 
         SASSERT(well_formed());
     }

src/sat/sat_solver.cpp

@@ -1314,7 +1314,7 @@ namespace sat {
     }
 
     bool solver::should_cancel() {
-        if (limit_reached() || memory_exceeded()) {
+        if (limit_reached() || memory_exceeded() || m_solver_canceled) {
             return true;
         }
         if (m_config.m_restart_max <= m_restarts) {
@@ -1959,6 +1959,7 @@ namespace sat {
 
     void solver::init_search() {
         m_model_is_current        = false;
+        m_solver_canceled         = false;
         m_phase_counter           = 0;
         m_search_state            = s_unsat;
         m_search_unsat_conflicts  = m_config.m_search_unsat_conflicts;

src/sat/sat_solver.h

@@ -177,6 +177,7 @@ namespace sat {
         clause_wrapper_vector   m_clauses_to_reinit;
         std::string             m_reason_unknown;
         bool                    m_trim = false;
+        bool                    m_solver_canceled = false;
 
         visit_helper            m_visited;
 
@@ -287,6 +288,7 @@ namespace sat {
         random_gen& rand() { return m_rand; }
 
         void set_trim() { m_trim = true; }
+        void set_canceled() { m_solver_canceled = true; }
 
     protected:
         void reset_var(bool_var v, bool ext, bool dvar);

src/sat/sat_solver/sat_smt_solver.cpp

@@ -197,10 +197,16 @@ class sat_smt_solver : public solver {
         case l_false:
             extract_core();
             break;
-        default:
+        default: {
+            auto* ext = get_euf();
+            if (ext && ext->get_sls_model()) {
+                r = l_true;
+                break;
+            }
             set_reason_unknown(m_solver.get_reason_unknown());
             break;
         }
+        }
         return r;
     }
 
@@ -576,6 +582,7 @@ class sat_smt_solver : public solver {
     void add_assumption(expr* a) {
         init_goal2sat();
         m_dep.insert(a, m_goal2sat.internalize(a));
+        get_euf()->add_assertion(a);
     }
 
     void internalize_assumptions(expr_ref_vector const& asms) {     
@@ -632,6 +639,11 @@ class sat_smt_solver : public solver {
     void get_model_core(model_ref & mdl) override {
         TRACE("sat", tout << "retrieve model " << (m_solver.model_is_current()?"present":"absent") << "\n";);
         mdl = nullptr;
+        auto ext = get_euf();
+        if (ext)
+            mdl = ext->get_sls_model();
+        if (mdl)
+            return;
         if (!m_solver.model_is_current()) 
             return;
         if (m_fmls.size() > m_qhead)

src/sat/smt/euf_internalize.cpp

@@ -525,4 +525,8 @@ namespace euf {
         return n;
     }
 
+    void solver::add_assertion(expr* f) {
+        m_assertions.push_back(f);
+        m_trail.push(push_back_vector(m_assertions));
+    }
 }

src/sat/smt/euf_model.cpp

@@ -18,6 +18,7 @@ Module Name:
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "sat/smt/euf_solver.h"
+#include "sat/smt/sls_solver.h"
 #include "model/value_factory.h"
 
 namespace euf {
@@ -67,6 +68,14 @@ namespace euf {
         m_qmodel = mdl;
     }
 
+    model_ref solver::get_sls_model() {
+        model_ref mdl;
+        auto s = get_solver(m.mk_family_id("sls"), nullptr);
+        if (s)
+            mdl = dynamic_cast<sls::solver*>(s)->get_model();
+        return mdl;
+    }
+
     void solver::update_model(model_ref& mdl, bool validate) {
         TRACE("model", tout << "create model\n";);
         if (m_qmodel) {

src/sat/smt/euf_solver.cpp

@@ -28,6 +28,7 @@ Module Name:
 #include "sat/smt/q_solver.h"
 #include "sat/smt/fpa_solver.h"
 #include "sat/smt/dt_solver.h"
+#include "sat/smt/sls_solver.h"
 #include "sat/smt/recfun_solver.h"
 #include "sat/smt/specrel_solver.h"
 
@@ -54,6 +55,7 @@ namespace euf {
         m_smt_proof_checker(m, p),
         m_clause(m),       
         m_expr_args(m),
+        m_assertions(m),
         m_values(m)
     {
         updt_params(p);
@@ -77,6 +79,7 @@ namespace euf {
             };
             m_egraph.set_on_merge(on_merge);
         }
+
     }
 
     void solver::updt_params(params_ref const& p) {
@@ -185,7 +188,9 @@ namespace euf {
         IF_VERBOSE(0, verbose_stream() << mk_pp(f, m) << " not handled\n");
     }
 
-    void solver::init_search() {        
+    void solver::init_search() {   
+        if (get_config().m_sls_enable)
+            add_solver(alloc(sls::solver, *this));
         TRACE("before_search", s().display(tout););
         m_reason_unknown.clear();
         for (auto* s : m_solvers)
@@ -217,7 +222,7 @@ namespace euf {
         mark_relevant(lit);
         s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), idx));
     }
-
+    
     lbool solver::resolve_conflict() {
         for (auto* s : m_solvers) {
             lbool r = s->resolve_conflict();
@@ -664,7 +669,9 @@ namespace euf {
         if (give_up)
             return sat::check_result::CR_GIVEUP;  
         if (m_qsolver && m_config.m_arith_ignore_int)
-            return sat::check_result::CR_GIVEUP;            
+            return sat::check_result::CR_GIVEUP; 
+        for (auto s : m_solvers)
+            s->finalize();
         return sat::check_result::CR_DONE;
     }
 

src/sat/smt/euf_solver.h

@@ -154,6 +154,7 @@ namespace euf {
         svector<scope>                   m_scopes;
         scoped_ptr_vector<th_solver>     m_solvers;
         ptr_vector<th_solver>            m_id2solver;
+
 
         constraint* m_conflict = nullptr;
         constraint* m_eq = nullptr;
@@ -173,6 +174,7 @@ namespace euf {
         symbol                           m_smt = symbol("smt");            
         expr_ref_vector                  m_clause;
         expr_ref_vector                  m_expr_args;
+        expr_ref_vector                  m_assertions;
 
 
         // internalization
@@ -482,6 +484,10 @@ namespace euf {
         bool enable_ackerman_axioms(expr* n) const;
         bool is_fixed(euf::enode* n, expr_ref& val, sat::literal_vector& explain);
 
+        void add_assertion(expr* f);
+        expr_ref_vector const& get_assertions() { return m_assertions; }
+        model_ref get_sls_model();
+
         // relevancy
 
         bool relevancy_enabled() const { return m_relevancy.enabled(); }

src/sat/smt/sat_th.h

@@ -148,6 +148,8 @@ namespace euf {
 
         virtual void set_bounds(enode* n) {}
 
+        virtual void finalize() {}
+
     };
 
     class th_proof_hint : public sat::proof_hint {
@@ -225,6 +227,7 @@ namespace euf {
         void push() override { m_num_scopes++; }
         void pop(unsigned n) override;
 
+
         unsigned random();
     };