From d3bf25ce856f3ea316b69e82dd762f907dbd8e4b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 26 Jan 2025 14:16:43 -0800
Subject: [PATCH] throttle value smt -> sls

---
 src/ast/sls/sat_ddfw.cpp       | 2 +-
 src/ast/sls/sat_ddfw.h         | 1 +
 src/ast/sls/sls_arith_base.cpp | 4 ++--
 src/ast/sls/sls_smt_plugin.cpp | 6 ++++--
 src/sat/smt/sls_solver.cpp     | 5 -----
 5 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/src/ast/sls/sat_ddfw.cpp b/src/ast/sls/sat_ddfw.cpp
index d030cdec2f1..da6d567f883 100644
--- a/src/ast/sls/sat_ddfw.cpp
+++ b/src/ast/sls/sat_ddfw.cpp
@@ -430,7 +430,7 @@ namespace sat {
         for (unsigned i = 0; i < num_vars(); ++i) 
             m_model[i] = to_lbool(value(i));
         save_priorities();
-        if (m_plugin && !m_in_external_flip && m_restart_count == 0)
+        if (m_plugin && !m_in_external_flip && m_restart_count == 0 && m_model_save_count++ % 10 == 0)
             m_plugin->on_restart(); // import values if there are any updated ones.
         if (m_plugin && !m_in_external_flip)
             m_last_result = m_plugin->on_save_model();
diff --git a/src/ast/sls/sat_ddfw.h b/src/ast/sls/sat_ddfw.h
index c3a493ed4f7..81bbb6fbe6b 100644
--- a/src/ast/sls/sat_ddfw.h
+++ b/src/ast/sls/sat_ddfw.h
@@ -97,6 +97,7 @@ namespace sat {
         uint64_t         m_last_flips_for_shift = 0;
         unsigned         m_num_non_binary_clauses = 0;
         unsigned         m_restart_count = 0, m_reinit_count = 0;
+        unsigned         m_model_save_count = 0;
         uint64_t         m_restart_next = 0, m_reinit_next = 0;
         uint64_t         m_flips = 0, m_last_flips = 0, m_shifts = 0;
         unsigned         m_logs = 0;
diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index 35ceb02ffa5..13a7895a1c8 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -1571,8 +1571,8 @@ namespace sls {
                 todo.push_back(op.m_arg1);
                 todo.push_back(op.m_arg2);
             }
-            if (m_vars[u].is_if_op()) {
-                auto const& ui = m_vars[u];
+            auto const& ui = m_vars[u];
+            if (ui.is_if_op()) {
                 expr* c = nullptr, * th = nullptr, * el = nullptr;
                 VERIFY(m.is_ite(ui.m_expr, c, th, el));
                 todo.push_back(mk_var(th));
diff --git a/src/ast/sls/sls_smt_plugin.cpp b/src/ast/sls/sls_smt_plugin.cpp
index 952515264f6..fe09b2f010d 100644
--- a/src/ast/sls/sls_smt_plugin.cpp
+++ b/src/ast/sls/sls_smt_plugin.cpp
@@ -212,7 +212,7 @@ namespace sls {
             m_sat_phase[v] = ctx.get_best_phase(v);
     }
 
-    bool smt_plugin::export_to_sls() {     
+    bool smt_plugin::export_to_sls() {    
         bool updated = false;
         if (m_has_units) {            
             std::lock_guard<std::mutex> lock(m_mutex);
@@ -274,7 +274,7 @@ namespace sls {
 
     void smt_plugin::smt_values_to_sls() {
 
-        if (ctx.parallel_mode()) {
+        if (true || ctx.parallel_mode()) {
             std::scoped_lock lock(m_mutex);
             m_sync_var_values.reset();
             for (auto const& [t, t_sync] : m_smt2sync_uninterp) {
@@ -310,9 +310,11 @@ namespace sls {
     void smt_plugin::sls_phase_to_smt() {
         if (!m_has_new_sls_phase)
             return;
+#if 0
         IF_VERBOSE(2, verbose_stream() << "SLS -> SMT phase. unsat size: " << m_min_unsat_size << "\n");
         for (auto v : m_shared_bool_vars) 
             ctx.force_phase(sat::literal(v, !m_sls_phase[v]));
+#endif
         m_has_new_sls_phase = false;
     }
 
diff --git a/src/sat/smt/sls_solver.cpp b/src/sat/smt/sls_solver.cpp
index 45b4c5951cd..15e73fbaa8d 100644
--- a/src/sat/smt/sls_solver.cpp
+++ b/src/sat/smt/sls_solver.cpp
@@ -105,11 +105,6 @@ namespace sls {
                 m_smt_plugin->add_unit(lit);
             }
         }
-#if 0
-        if (ctx.has_new_best_phase())
-            m_smt_plugin->import_phase_from_smt();
-
-#endif
 
         m_smt_plugin->import_from_sls();
     }