From b14499f2301cba4c47e7d8574ad094b148dc0282 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 21 Feb 2024 19:29:21 -0800
Subject: [PATCH] prepare for sls experiment

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/bv_sls.h       |  2 +
 src/sat/smt/sls_solver.cpp | 80 ++++++++++++++++++++++++++++++++------
 src/sat/smt/sls_solver.h   |  9 +++--
 3 files changed, 76 insertions(+), 15 deletions(-)

diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h
index e2030986d..be2e8feed 100644
--- a/src/ast/sls/bv_sls.h
+++ b/src/ast/sls/bv_sls.h
@@ -101,5 +101,7 @@ namespace bv {
         sls_valuation const& wval(expr* e) const { return m_eval.wval0(e); }
 
         model_ref get_model();
+
+        void cancel() { m.limit().cancel(); }
     };
 }
diff --git a/src/sat/smt/sls_solver.cpp b/src/sat/smt/sls_solver.cpp
index 1466b1b41..8feb9f83e 100644
--- a/src/sat/smt/sls_solver.cpp
+++ b/src/sat/smt/sls_solver.cpp
@@ -17,7 +17,7 @@ Author:
 
 #include "sat/smt/sls_solver.h"
 #include "sat/smt/euf_solver.h"
-#include "ast/sls/bv_sls.h"
+
 
 
 namespace sls {
@@ -26,8 +26,8 @@ namespace sls {
         th_euf_solver(ctx, symbol("sls"), ctx.get_manager().mk_family_id("sls")) {}
 
     solver::~solver() {
-        if (m_rlimit) {
-            m_rlimit->cancel();
+        if (m_bvsls) {
+            m_bvsls->cancel();            
             m_thread.join();
         }
     }
@@ -48,27 +48,83 @@ namespace sls {
         
 
     void solver::init_local_search() {
-        if (m_rlimit) {
-            m_rlimit->cancel();
+        if (m_bvsls) {
+            m_bvsls->cancel();
             m_thread.join();
+            if (m_result == l_true) {
+                verbose_stream() << "Found model using local search - INIT\n";
+                exit(1);
+            }
         }
         // set up state for local search solver here
-        auto* bvsls = alloc(bv::sls, m);
+
+        m_m = alloc(ast_manager, m);
+        ast_translation tr(m, *m_m);
+        
+        m_completed = false;
+        m_result = l_undef;
+        m_bvsls = alloc(bv::sls, *m_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());
+
+        unsigned trail_sz = s().trail_size();
+        for (unsigned i = 0; i < trail_sz; ++i) {
+            auto lit = s().trail_literal(i);
+            if (s().lvl(lit) > s().search_lvl())
+                break;
+            expr_ref fml = literal2expr(lit);
+            m_bvsls->assert_expr(tr(fml.get()));
+        }
+        unsigned num_vars = s().num_vars();
+        for (unsigned i = 0; i < 2*num_vars; ++i) {
+            auto l1 = ~sat::to_literal(i);
+            auto const& wlist = s().get_wlist(l1);
+            for (sat::watched const& w : wlist) {
+                if (!w.is_binary_non_learned_clause())
+                    continue;
+                sat::literal l2 = w.get_literal();
+                if (l1.index() > l2.index())
+                    continue;
+                expr_ref fml(m.mk_or(literal2expr(l1), literal2expr(l2)), m);
+                m_bvsls->assert_expr(tr(fml.get()));
+            }
+        }
+        for (auto clause : s().clauses()) {
+            expr_ref_vector cls(m);
+            for (auto lit : *clause)
+                cls.push_back(literal2expr(lit));
+            expr_ref fml(m.mk_or(cls), m);
+            m_bvsls->assert_expr(tr(fml.get()));
+        }
+
+        // use phase assignment from literals?
+        std::function<bool(expr*, unsigned)> eval = [&](expr* e, unsigned r) {
+            return false;
+        };
+
+        m_bvsls->init();
+        m_bvsls->init_eval(eval);
+        m_bvsls->updt_params(s().params());
+
+        m_thread = std::thread([this]() { run_local_search(); });        
     }
 
     void solver::sample_local_search() {
-    
+        if (m_completed) {
+            m_thread.join();
+            if (m_result == l_true) {
+                verbose_stream() << "Found model using local search\n";
+                exit(1);
+            }
+        }
     }
 
-    void solver::run_local_search(solver& s) {
-
+    void solver::run_local_search() {
+        lbool r = (*m_bvsls)();
+        m_result = r;
+        m_completed = true;
     }
 
 }
diff --git a/src/sat/smt/sls_solver.h b/src/sat/smt/sls_solver.h
index 2a8f07c0b..0c466d0cc 100644
--- a/src/sat/smt/sls_solver.h
+++ b/src/sat/smt/sls_solver.h
@@ -16,8 +16,10 @@ Author:
 --*/
 #pragma once
 
-#include "sat/smt/sat_th.h"
 #include "util/rlimit.h"
+#include "ast/sls/bv_sls.h"
+#include "sat/smt/sat_th.h"
+
 
 namespace euf {
     class solver;
@@ -29,9 +31,10 @@ namespace sls {
         std::atomic<lbool> m_result;
         std::atomic<bool> m_completed;
         std::thread m_thread;
-        scoped_ptr<reslimit> m_rlimit;
+        scoped_ptr<ast_manager> m_m;
+        scoped_ptr<bv::sls> m_bvsls;
 
-        void run_local_search(solver& s);
+        void run_local_search();
         void init_local_search();
         void sample_local_search();
     public: