align reslimit with ddfw

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)) 

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();
 

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; }

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();
     }
     

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();

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(); }