From a08a3ee32b01c87fd49e325db590231bd4a44834 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 13 Jan 2025 18:19:35 -0800
Subject: [PATCH] align reslimit with ddfw

---
 src/ast/sls/sls_arith_base.cpp   | 5 +++--
 src/ast/sls/sls_bv_lookahead.cpp | 2 +-
 src/ast/sls/sls_context.h        | 2 ++
 src/ast/sls/sls_smt_plugin.cpp   | 8 +++++++-
 src/ast/sls/sls_smt_plugin.h     | 2 ++
 src/ast/sls/sls_smt_solver.cpp   | 1 +
 6 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index 1d94927da..528cad536 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -2637,6 +2637,7 @@ namespace sls {
     }
     template<typename num_t>
     double arith_base<num_t>::lookahead(expr* t, bool update_score) {
+        ctx.rlimit().inc();
         SASSERT(a.is_int_real(t) || m.is_bool(t));
         double score = m_top_score;
         for (unsigned depth = m_min_depth; depth <= m_max_depth; ++depth) {
@@ -2955,7 +2956,7 @@ namespace sls {
         IF_VERBOSE(3, verbose_stream() << "lookahead-search moves:" << m_stats.m_moves << " max-moves:" << m_config.max_moves << "\n");
         TRACE("arith", display(tout));
 
-        while (m.inc() && m_stats.m_moves < m_config.max_moves) {
+        while (ctx.rlimit().inc() && m_stats.m_moves < m_config.max_moves) {
             m_stats.m_moves++;
             check_restart();
 
@@ -3015,7 +3016,7 @@ namespace sls {
         }
 
         m_last_atom = e;
-        CTRACE("arith", !e, "no candidate\n";);
+        CTRACE("arith", !e, tout << "no unsatisfiable candidate\n";);
         CTRACE("arith", e, 
             tout << "select " << mk_bounded_pp(e, m) << " ";
             for (auto v : get_fixable_exprs(e)) 
diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp
index 2d47cfb33..0d342287c 100644
--- a/src/ast/sls/sls_bv_lookahead.cpp
+++ b/src/ast/sls/sls_bv_lookahead.cpp
@@ -61,7 +61,7 @@ namespace sls {
         TRACE("bv", 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");
 
-        while (m.inc() && m_stats.m_moves < m_config.max_moves) {
+        while (ctx.rlimit().inc() && m_stats.m_moves < m_config.max_moves) {
             m_stats.m_moves++;
             check_restart();
 
diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h
index feccb9e09..ee3696d87 100644
--- a/src/ast/sls/sls_context.h
+++ b/src/ast/sls/sls_context.h
@@ -80,6 +80,7 @@ namespace sls {
         virtual void add_clause(unsigned n, sat::literal const* lits) = 0;
         virtual void force_restart() = 0;
         virtual std::ostream& display(std::ostream& out) = 0;
+        virtual reslimit& rlimit() = 0;
     };
     
     class context {
@@ -187,6 +188,7 @@ namespace sls {
         indexed_uint_set const& unsat() const { return s.unsat(); }
         unsigned rand() { return m_rand(); }
         unsigned rand(unsigned n) { return m_rand(n); }
+        reslimit& rlimit() { return s.rlimit(); }
         sat::literal_vector const& root_literals() const { return m_root_literals; }
         sat::literal_vector const& unit_literals() const { return m_unit_literals; }
         expr_ref_vector const& input_assertions() const { return m_input_assertions; }
diff --git a/src/ast/sls/sls_smt_plugin.cpp b/src/ast/sls/sls_smt_plugin.cpp
index b2b903985..0d039928e 100644
--- a/src/ast/sls/sls_smt_plugin.cpp
+++ b/src/ast/sls/sls_smt_plugin.cpp
@@ -47,6 +47,7 @@ namespace sls {
     void smt_plugin::check(expr_ref_vector const& fmls, vector <sat::literal_vector> const& clauses) {
         SASSERT(!m_ddfw);
         // set up state for local search theory_sls here
+
         m_result = l_undef;
         m_completed = false;
         m_units.reset();
@@ -109,9 +110,14 @@ namespace sls {
     }
 
     void smt_plugin::bounded_run(unsigned max_iterations) {
+        verbose_stream() << "bounded run " << max_iterations << "\n";
         m_ddfw->rlimit().reset_count();
         m_ddfw->rlimit().push(max_iterations);
-        run();
+        {
+            scoped_limits _sl(m.limit());
+            _sl.push_child(&m_ddfw->rlimit());
+            run();
+        }
         m_ddfw->rlimit().pop();
     }
     
diff --git a/src/ast/sls/sls_smt_plugin.h b/src/ast/sls/sls_smt_plugin.h
index f099fb264..711fec4d6 100644
--- a/src/ast/sls/sls_smt_plugin.h
+++ b/src/ast/sls/sls_smt_plugin.h
@@ -133,6 +133,8 @@ namespace sls {
 
         void on_rescale() override {}
 
+        reslimit& rlimit() override { return m_ddfw->rlimit(); }
+
         void smt_phase_to_sls();
         void smt_values_to_sls();
         void smt_units_to_sls();
diff --git a/src/ast/sls/sls_smt_solver.cpp b/src/ast/sls/sls_smt_solver.cpp
index 6036b9172..0258fc183 100644
--- a/src/ast/sls/sls_smt_solver.cpp
+++ b/src/ast/sls/sls_smt_solver.cpp
@@ -93,6 +93,7 @@ namespace sls {
         indexed_uint_set const& unsat() const override { return m_ddfw.unsat_set(); }
         sat::bool_var add_var() override { m_dirty = true;  return m_ddfw.add_var(); }  
         void add_input_assertion(expr* f) { m_context.add_input_assertion(f); }
+        reslimit& rlimit() { return m_ddfw.rlimit(); }
 
         void force_restart() override { m_ddfw.force_restart(); }