Skip to content

Commit

Permalink
align reslimit with ddfw
Browse files Browse the repository at this point in the history
NikolajBjorner committed Jan 14, 2025
1 parent 3c5b8bd commit a08a3ee
Showing 6 changed files with 16 additions and 4 deletions.
5 changes: 3 additions & 2 deletions src/ast/sls/sls_arith_base.cpp
Original file line number Diff line number Diff line change
@@ -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))
2 changes: 1 addition & 1 deletion src/ast/sls/sls_bv_lookahead.cpp
Original file line number Diff line number Diff line change
@@ -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();

2 changes: 2 additions & 0 deletions src/ast/sls/sls_context.h
Original file line number Diff line number Diff line change
@@ -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; }
8 changes: 7 additions & 1 deletion src/ast/sls/sls_smt_plugin.cpp
Original file line number Diff line number Diff line change
@@ -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();
}

2 changes: 2 additions & 0 deletions src/ast/sls/sls_smt_plugin.h
Original file line number Diff line number Diff line change
@@ -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();
1 change: 1 addition & 0 deletions src/ast/sls/sls_smt_solver.cpp
Original file line number Diff line number Diff line change
@@ -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(); }

0 comments on commit a08a3ee

Please sign in to comment.