bugfixes, adding plugin solver

Author: NikolajBjorner

src/ast/sls/bv_sls.cpp

@@ -91,7 +91,7 @@ namespace bv {
 
     lbool sls::search() {
         // init and init_eval were invoked
-        unsigned n = 0;  
+        unsigned n = 0;
         for (; n++ < m_config.m_max_repairs && m.inc(); ) {
             ++m_stats.m_moves;
             auto [down, e] = next_to_repair();
@@ -164,7 +164,7 @@ namespace bv {
         return was_repaired;
     }
 
-    void sls::try_repair_up(app* e) {
+    void sls::try_repair_up(app* e) {       
         m_repair_up.remove(e->get_id());
         if (m_terms.is_assertion(e) || !m_eval.repair_up(e)) 
             m_repair_down.insert(e->get_id());        

src/ast/sls/bv_sls_eval.cpp

@@ -130,7 +130,7 @@ namespace bv {
     void sls_eval::init_eval_bv(app* e) {
         if (bv.is_bv(e)) {
             auto& v = wval0(e);
-            v.set(wval1(e));
+            v.set(wval1(e).bits);
         }
         else if (m.is_bool(e)) 
             m_eval.setx(e->get_id(), bval1_bv(e), false);        
@@ -299,10 +299,10 @@ namespace bv {
         return bval0(e); 
     }
 
-    svector<digit_t>& sls_eval::wval1(app* e) const {
+    sls_valuation& sls_eval::wval1(app* e) const {
         auto& val = *m_values1[e->get_id()];
         wval1(e, val);
-        return val.bits;
+        return val;        
     }
 
     void sls_eval::wval1(app* e, sls_valuation& val) const {
@@ -429,8 +429,6 @@ namespace bv {
             break;
         }
         case OP_CONCAT: {
-            if (e->get_num_args() != 2)
-                verbose_stream() << mk_bounded_pp(e, m) << "\n";
             SASSERT(e->get_num_args() == 2);
             auto const& a = wval0(e->get_arg(0));
             auto const& b = wval0(e->get_arg(1));
@@ -1005,8 +1003,8 @@ namespace bv {
         }
         else {
             // b := a - e
-            a.set_sub(m_tmp, a.bits, e.bits);
-            a.set_repair(random_bool(), m_tmp);
+            b.set_sub(m_tmp, a.bits, e.bits);
+            b.set_repair(random_bool(), m_tmp);
         }
         return true;
     }
@@ -1186,7 +1184,6 @@ namespace bv {
             if (a.is_zero(m_tmp2))
                 return false;
             if (!a.get_at_least(m_tmp2, m_tmp)) {
-                verbose_stream() << "could not get at least\n";                    
                 return false;
             }
         }
@@ -1571,7 +1568,7 @@ namespace bv {
             return true;
         }
         if (bv.is_bv(e))
-            return wval0(e).try_set(wval1(to_app(e)));
+            return wval0(e).try_set(wval1(to_app(e)).bits);
         return false;
     }
 }

src/ast/sls/bv_sls_eval.h

@@ -136,8 +136,8 @@ namespace bv {
          */
         bool bval1(app* e) const;
         bool can_eval1(app* e) const;
-
-        svector<digit_t>& wval1(app* e) const;
+        
+        sls_valuation& wval1(app* e) const;
 
         /**
          * Override evaluaton.

src/ast/sls/sls_valuation.h

@@ -202,6 +202,7 @@ namespace bv {
         }
 
         std::ostream& display(std::ostream& out) const {
+            out << "V:";
             out << std::hex;
             auto print_bits = [&](svector<digit_t> const& v) {
                 bool nz = false;
@@ -215,7 +216,7 @@ namespace bv {
             };
 
             print_bits(bits);
-            out << " ";
+            out << " fix:";
             print_bits(fixed);
 
             if (!eq(lo, hi)) {

src/sat/smt/CMakeLists.txt

@@ -46,6 +46,7 @@ z3_add_component(sat_smt
     q_solver.cpp
     recfun_solver.cpp
     sat_th.cpp
+    sls_solver.cpp
     specrel_solver.cpp
     tseitin_theory_checker.cpp
     user_solver.cpp

src/sat/smt/sls_solver.cpp

@@ -0,0 +1,74 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    sls_solver
+
+Abstract:
+
+    Interface to Concurrent SLS solver
+    
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2024-02-21
+
+--*/
+
+#include "sat/smt/sls_solver.h"
+#include "sat/smt/euf_solver.h"
+#include "ast/sls/bv_sls.h"
+
+
+namespace sls {
+
+    solver::solver(euf::solver& ctx):
+        th_euf_solver(ctx, symbol("sls"), ctx.get_manager().mk_family_id("sls")) {}
+
+    solver::~solver() {
+        if (m_rlimit) {
+            m_rlimit->cancel();
+            m_thread.join();
+        }
+    }
+
+    void solver::push_core() {
+        if (s().scope_lvl() == s().search_lvl() + 1)
+            init_local_search();
+    }
+    
+    void solver::pop_core(unsigned n) {
+        if (s().scope_lvl() - n <= s().search_lvl())
+            sample_local_search();
+    }
+
+    void solver::simplify() {
+    
+    }
+        
+
+    void solver::init_local_search() {
+        if (m_rlimit) {
+            m_rlimit->cancel();
+            m_thread.join();
+        }
+        // set up state for local search solver here
+        auto* bvsls = alloc(bv::sls, m);
+        // walk clauses, add them
+        // walk trail stack until search level, add units
+        // encapsulate bvsls within the arguments of run-local-search.
+        // ensure bvsls does not touch ast-manager.
+        m_thread = std::thread([this]() { run_local_search(*this); });
+        m_rlimit = alloc(reslimit);
+        m_rlimit->push_child(&s().rlimit());
+    }
+
+    void solver::sample_local_search() {
+    
+    }
+
+    void solver::run_local_search(solver& s) {
+
+    }
+
+}

src/sat/smt/sls_solver.h

@@ -0,0 +1,59 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    sls_solver
+
+Abstract:
+
+    Interface to Concurrent SLS solver
+    
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2024-02-21
+
+--*/
+#pragma once
+
+#include "sat/smt/sat_th.h"
+#include "util/rlimit.h"
+
+namespace euf {
+    class solver;
+}
+
+namespace sls {
+
+    class solver : public euf::th_euf_solver {
+        std::atomic<lbool> m_result;
+        std::atomic<bool> m_completed;
+        std::thread m_thread;
+        scoped_ptr<reslimit> m_rlimit;
+
+        void run_local_search(solver& s);
+        void init_local_search();
+        void sample_local_search();
+    public:
+        solver(euf::solver& ctx);
+        ~solver();
+
+        void push_core() override;
+        void pop_core(unsigned n) override;
+        void simplify() override;
+
+        sat::literal internalize(expr* e, bool sign, bool root) override { UNREACHABLE();  return sat::null_literal; }
+        void internalize(expr* e) override { UNREACHABLE(); }
+        th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); }
+       
+
+        bool unit_propagate() override { return false; }
+        void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override { UNREACHABLE(); }
+        sat::check_result check() override { return sat::check_result::CR_DONE; }
+        std::ostream & display(std::ostream & out) const override { return out; }
+        std::ostream & display_justification(std::ostream & out, sat::ext_justification_idx idx) const override { UNREACHABLE(); return out; }
+        std::ostream & display_constraint(std::ostream & out, sat::ext_constraint_idx idx) const override { UNREACHABLE(); return out; }
+        
+    };
+
+}