From 943d881340fc77496dcfc75d9ba65a617a51475e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 12 Jan 2025 16:59:27 -0800
Subject: [PATCH] fixes to hybrid mode

---
 src/ast/sls/sls_arith_base.cpp | 27 +++++++++++++++++++--------
 src/ast/sls/sls_context.cpp    |  1 -
 src/ast/sls/sls_smt_plugin.cpp |  6 ++++--
 3 files changed, 23 insertions(+), 11 deletions(-)

diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index 17b441c25..1d94927da 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -2479,6 +2479,20 @@ namespace sls {
             if (get_bool_value(a) != ctx.is_true(v))
                 ctx.flip(v);
         }
+#if 0
+        for (auto idx : ctx.unsat()) {
+            auto const& cl = ctx.get_clause(idx);
+            verbose_stream() << "clause " << cl << "\n";
+            for (auto lit : cl) {
+                auto a = ctx.atom(lit.var());
+                if (a)
+                    verbose_stream() << lit << " " << mk_bounded_pp(a, m) << " " << get_bool_value(a) << " " << ctx.is_true(lit) << "\n";
+                else
+                    verbose_stream() << lit << " " << ctx.is_true(lit) << "\n";
+            }
+        }
+#endif
+
     }
 
     template<typename num_t>
@@ -2938,24 +2952,22 @@ namespace sls {
         rescore();
         m_config.max_moves = m_stats.m_moves + m_config.max_moves_base;
         TRACE("arith", tout << "search " << m_stats.m_moves << " " << m_config.max_moves << "\n";);
-        IF_VERBOSE(1, verbose_stream() << "lookahead-search moves:" << m_stats.m_moves << " max-moves:" << m_config.max_moves << "\n");
+        IF_VERBOSE(3, verbose_stream() << "lookahead-search moves:" << m_stats.m_moves << " max-moves:" << m_config.max_moves << "\n");
         TRACE("arith", display(tout));
-        bool loop_again = true;
 
         while (m.inc() && m_stats.m_moves < m_config.max_moves) {
-            loop_again = false;
             m_stats.m_moves++;
             check_restart();
 
             auto t = get_candidate_unsat();
 
-            if (!t)
+            if (!t) 
                 break;
-
+            
             auto& vars = get_fixable_exprs(t);
 
             if (vars.empty()) 
-                return;            
+                break;            
 
             if (ctx.rand(2047) < m_config.wp && apply_move(t, vars, arith_move_type::random_inc_dec))
                 continue;
@@ -2965,9 +2977,8 @@ namespace sls {
 
             if (apply_move(t, vars, arith_move_type::random_update))
                 recalibrate_weights();
-            loop_again = true;
         }
-        if (loop_again)
+        if (m_stats.m_moves >= m_config.max_moves)
             m_config.max_moves_base += 100;
         finalize_bool_assignment();
     }
diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp
index e9481984f..25700126b 100644
--- a/src/ast/sls/sls_context.cpp
+++ b/src/ast/sls/sls_context.cpp
@@ -123,7 +123,6 @@ namespace sls {
 
             propagate_boolean_assignment();
 
-
             // verbose_stream() << "propagate " << unsat().size() << " " << m_new_constraint << "\n";
 
             if (m_new_constraint || !unsat().empty())
diff --git a/src/ast/sls/sls_smt_plugin.cpp b/src/ast/sls/sls_smt_plugin.cpp
index f8e0c200b..b2b903985 100644
--- a/src/ast/sls/sls_smt_plugin.cpp
+++ b/src/ast/sls/sls_smt_plugin.cpp
@@ -55,6 +55,7 @@ namespace sls {
         m_ddfw = alloc(sat::ddfw);
         m_ddfw->set_plugin(this);
         m_ddfw->updt_params(ctx.get_params());
+        m_context.updt_params(ctx.get_params());
 
         for (auto const& clause : clauses) {
             m_ddfw->add(clause.size(), clause.data());
@@ -72,7 +73,7 @@ namespace sls {
         }
 
         for (auto fml : fmls) 
-            m_context.add_constraint(m_smt2sls_tr(fml));     
+            m_context.add_input_assertion(m_smt2sls_tr(fml));     
 
         for (unsigned v = 0; v < ctx.get_num_bool_vars(); ++v) {
             expr* e = ctx.bool_var2expr(v);
@@ -99,7 +100,7 @@ namespace sls {
         if (!m_ddfw)
             return;
         m_result = m_ddfw->check(0, nullptr);
-        IF_VERBOSE(1, verbose_stream() << "sls-result " << m_result << "\n");
+        IF_VERBOSE(2, verbose_stream() << "sls-result " << m_result << "\n");
         for (auto v : m_shared_bool_vars) {
             auto w = m_smt_bool_var2sls_bool_var[v];
             m_rewards[v] = m_ddfw->get_reward_avg(w);
@@ -127,6 +128,7 @@ namespace sls {
         SASSERT(m_completed);
         mdl = nullptr;
         m_ddfw->collect_statistics(st);
+        m_context.collect_statistics(st);
         if (m_result == l_true && m_sls_model) {
             ast_translation tr(m_sls, m);
             mdl = m_sls_model->translate(tr);