From 8e3b9f6686acd5676eb475f155976d9ca536d2dd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Nov 2024 21:43:26 -0800 Subject: [PATCH] add sequential option for SLS, fixes to import/export methods SLS<->SMT --- src/ast/sls/sat_ddfw.cpp | 3 +- src/ast/sls/sat_ddfw.h | 4 +- src/ast/sls/sls_arith_base.cpp | 8 +- src/ast/sls/sls_smt_plugin.cpp | 110 +++++++++++++++++++-------- src/ast/sls/sls_smt_plugin.h | 23 ++++-- src/ast/sls/sls_smt_solver.cpp | 4 - src/sat/smt/sls_solver.cpp | 2 +- src/sat/smt/sls_solver.h | 5 +- src/smt/params/smt_params.cpp | 1 + src/smt/params/smt_params.h | 1 + src/smt/params/smt_params_helper.pyg | 1 + src/smt/smt_context.h | 4 +- src/smt/theory_seq.cpp | 19 +++++ src/smt/theory_seq.h | 1 + src/smt/theory_sls.cpp | 73 +++++++++++++++--- src/smt/theory_sls.h | 28 ++++++- 16 files changed, 224 insertions(+), 63 deletions(-) diff --git a/src/ast/sls/sat_ddfw.cpp b/src/ast/sls/sat_ddfw.cpp index 5129c2caf..1a87524c0 100644 --- a/src/ast/sls/sat_ddfw.cpp +++ b/src/ast/sls/sat_ddfw.cpp @@ -57,7 +57,6 @@ namespace sat { } void ddfw::check_with_plugin() { - m_plugin->init_search(); unsigned steps = 0; if (m_min_sz <= m_unsat.size()) save_best_values(); @@ -77,7 +76,6 @@ namespace sat { IF_VERBOSE(0, verbose_stream() << "Exception: " << ex.what() << "\n"); throw; } - m_plugin->finish_search(); } void ddfw::log() { @@ -246,6 +244,7 @@ namespace sat { void ddfw::flip(bool_var v) { ++m_flips; + m_limit.inc(); literal lit = literal(v, !value(v)); literal nlit = ~lit; SASSERT(is_true(lit)); diff --git a/src/ast/sls/sat_ddfw.h b/src/ast/sls/sat_ddfw.h index a00a196c9..468178981 100644 --- a/src/ast/sls/sat_ddfw.h +++ b/src/ast/sls/sat_ddfw.h @@ -36,8 +36,8 @@ namespace sat { class local_search_plugin { public: virtual ~local_search_plugin() {} - virtual void init_search() = 0; - virtual void finish_search() = 0; + //virtual void init_search() = 0; + //virtual void finish_search() = 0; virtual void on_rescale() = 0; virtual void on_save_model() = 0; virtual void on_restart() = 0; diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp index ecc48fdca..24ba4935a 100644 --- a/src/ast/sls/sls_arith_base.cpp +++ b/src/ast/sls/sls_arith_base.cpp @@ -2016,9 +2016,13 @@ namespace sls { w = mk_term(e); num_t n; - if (!is_num(v, n)) + try { + if (!is_num(v, n)) + return false; + } + catch (overflow_exception const&) { return false; - // verbose_stream() << "set value " << w << " " << mk_bounded_pp(e, m) << " " << n << " " << value(w) << "\n"; + } if (n == value(w)) return true; return update(w, n); diff --git a/src/ast/sls/sls_smt_plugin.cpp b/src/ast/sls/sls_smt_plugin.cpp index 2b704fa3f..5912bb44f 100644 --- a/src/ast/sls/sls_smt_plugin.cpp +++ b/src/ast/sls/sls_smt_plugin.cpp @@ -19,6 +19,8 @@ Author: #include "ast/sls/sls_smt_plugin.h" #include "ast/for_each_expr.h" #include "ast/bv_decl_plugin.h" +#include "ast/ast_pp.h" +#include "smt/params/smt_params_helper.hpp" namespace sls { @@ -29,6 +31,8 @@ namespace sls { m_sync(), m_smt2sync_tr(m, m_sync), m_smt2sls_tr(m, m_sls), + m_sls2sync_tr(m_sls, m_sync), + m_sls2smt_tr(m_sls, m), m_sync_uninterp(m_sync), m_sls_uninterp(m_sls), m_sync_values(m_sync), @@ -85,7 +89,10 @@ namespace sls { add_shared_term(t); } - m_thread = std::thread([this]() { run(); }); + if (ctx.parallel_mode()) + m_thread = std::thread([this]() { run(); }); + else + m_completed = true; } void smt_plugin::run() { @@ -94,8 +101,19 @@ namespace sls { m_result = m_ddfw->check(0, nullptr); m_ddfw->collect_statistics(m_st); IF_VERBOSE(1, 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); + } m_completed = true; } + + void smt_plugin::bounded_run(unsigned max_iterations) { + m_ddfw->rlimit().reset_count(); + m_ddfw->rlimit().push(max_iterations); + run(); + m_ddfw->rlimit().pop(); + } void smt_plugin::finalize(model_ref& mdl, ::statistics& st) { auto* d = m_ddfw; @@ -191,13 +209,47 @@ namespace sls { for (auto v : m_shared_bool_vars) { auto w = m_smt_bool_var2sls_bool_var[v]; if (m_sat_phase[v] != is_true(sat::literal(w, false))) - flip(w); + flip(w); m_ddfw->bias(w) = m_sat_phase[v] ? 1 : -1; } + smt_phase_to_sls(); m_has_new_sat_phase = false; return true; } + void smt_plugin::smt_phase_to_sls() { + for (auto v : m_shared_bool_vars) { + auto w = m_smt_bool_var2sls_bool_var[v]; + auto phase = ctx.get_best_phase(v); + if (phase != is_true(sat::literal(w, false))) + flip(w); + m_ddfw->bias(w) = phase ? 1 : -1; + } + } + + void smt_plugin::smt_values_to_sls() { + for (auto const& [t, t_sync] : m_smt2sync_uninterp) { + expr_ref val_t(m); + if (!ctx.get_value(t, val_t)) + continue; + expr* t_sls = m_smt2sls_tr(t); + auto val_sls = expr_ref(m_smt2sls_tr(val_t.get()), m_sls); + m_context.set_value(t_sls, val_sls); + } + } + + void smt_plugin::sls_phase_to_smt() { + IF_VERBOSE(2, verbose_stream() << "SLS -> SMT phase\n"); + for (auto v : m_shared_bool_vars) + ctx.force_phase(sat::literal(v, !m_sls_phase[v])); + } + + void smt_plugin::sls_activity_to_smt() { + IF_VERBOSE(2, verbose_stream() << "SLS -> SMT activity\n"); + for (auto v : m_shared_bool_vars) + ctx.inc_activity(v, 200 * m_rewards[v]); + } + bool smt_plugin::export_units_to_sls() { if (!m_has_units) return false; @@ -225,65 +277,63 @@ namespace sls { if (unsat().size() > m_min_unsat_size) return; m_min_unsat_size = unsat().size(); - std::lock_guard lock(m_mutex); + export_phase_from_sls(); + export_values_from_sls(); + } + + void smt_plugin::export_phase_from_sls() { + std::lock_guard lock(m_mutex); 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); - //verbose_stream() << v << " " << w << "\n"; VERIFY(m_ddfw->get_model().size() > w); VERIFY(m_sls_phase.size() > v); - m_sls_phase[v] = l_true == m_ddfw->get_model()[w]; - m_has_new_sls_phase = true; + m_sls_phase[v] = l_true == m_ddfw->get_model()[w]; } - // export_values_from_sls(); + m_has_new_sls_phase = true; } void smt_plugin::export_values_from_sls() { - IF_VERBOSE(3, verbose_stream() << "import values from sls\n"); + IF_VERBOSE(3, verbose_stream() << "export values from sls\n"); std::lock_guard lock(m_mutex); for (auto const& [t, t_sync] : m_sls2sync_uninterp) { - expr_ref val_t = m_context.get_value(t_sync); - m_sync_values.set(t_sync->get_id(), val_t.get()); + expr_ref val_t = m_context.get_value(t); + auto sync_val = m_sls2sync_tr(val_t.get()); + m_sync_values.setx(t_sync->get_id(), sync_val); } m_has_new_sls_values = true; } void smt_plugin::import_from_sls() { export_activity_to_smt(); - export_values_to_smt(); - export_phase_to_smt(); + if (m_has_new_sls_values) { + std::lock_guard lock(m_mutex); + sls_values_to_smt(); + m_has_new_sls_values = false; + } + if (m_has_new_sls_phase) { + std::lock_guard lock(m_mutex); + sls_phase_to_smt(); + m_has_new_sls_phase = false; + } } void smt_plugin::export_activity_to_smt() { } - void smt_plugin::export_values_to_smt() { + void smt_plugin::sls_values_to_smt() { if (!m_has_new_sls_values) return; - IF_VERBOSE(3, verbose_stream() << "SLS -> SMT values\n"); - std::lock_guard lock(m_mutex); + IF_VERBOSE(2, verbose_stream() << "SLS -> SMT values\n"); ast_translation tr(m_sync, m); for (auto const& [t, t_sync] : m_smt2sync_uninterp) { expr* sync_val = m_sync_values.get(t_sync->get_id(), nullptr); if (!sync_val) continue; expr_ref val(tr(sync_val), m); - ctx.initialize_value(t, val); + ctx.set_value(t, val); } - m_has_new_sls_values = false; - } - - void smt_plugin::export_phase_to_smt() { - if (!m_has_new_sls_phase) - return; - std::lock_guard lock(m_mutex); - IF_VERBOSE(3, verbose_stream() << "SLS -> SMT phase\n"); - for (auto v : m_shared_bool_vars) { - auto w = m_smt_bool_var2sls_bool_var[v]; - ctx.force_phase(sat::literal(w, m_sls_phase[v])); - } - m_has_new_sls_phase = false; } void smt_plugin::add_shared_term(expr* t) { @@ -310,6 +360,6 @@ namespace sls { m_ddfw->reinit(); m_new_clause_added = false; } - // export_from_sls(); + export_from_sls(); } } diff --git a/src/ast/sls/sls_smt_plugin.h b/src/ast/sls/sls_smt_plugin.h index 0ad28d6dc..073e5bc96 100644 --- a/src/ast/sls/sls_smt_plugin.h +++ b/src/ast/sls/sls_smt_plugin.h @@ -30,13 +30,16 @@ namespace sls { virtual ~smt_context() {} virtual ast_manager& get_manager() = 0; virtual params_ref get_params() = 0; - virtual void initialize_value(expr* t, expr* v) = 0; + virtual void set_value(expr* t, expr* v) = 0; virtual void force_phase(sat::literal lit) = 0; virtual void set_has_new_best_phase(bool b) = 0; + virtual bool get_value(expr* v, expr_ref& val) = 0; virtual bool get_best_phase(sat::bool_var v) = 0; virtual expr* bool_var2expr(sat::bool_var v) = 0; + virtual void inc_activity(sat::bool_var v, double inc) = 0; virtual void set_finished() = 0; virtual unsigned get_num_bool_vars() const = 0; + virtual bool parallel_mode() const = 0; }; @@ -50,7 +53,7 @@ namespace sls { ast_manager& m; ast_manager m_sls; ast_manager m_sync; - ast_translation m_smt2sync_tr, m_smt2sls_tr; + ast_translation m_smt2sync_tr, m_smt2sls_tr, m_sls2sync_tr, m_sls2smt_tr; expr_ref_vector m_sync_uninterp, m_sls_uninterp; expr_ref_vector m_sync_values; sat::ddfw* m_ddfw = nullptr; @@ -63,6 +66,7 @@ namespace sls { sat::literal_vector m_units; model_ref m_sls_model; ::statistics m_st; + bool m_new_clause_added = false; unsigned m_min_unsat_size = UINT_MAX; obj_map m_sls2sync_uninterp; // hashtable from sls-uninterp to sync uninterp @@ -78,6 +82,7 @@ namespace sls { bool is_shared(sat::literal lit); void run(); + void add_shared_term(expr* t); void add_uninterp(expr* smt_t); void add_shared_var(sat::bool_var v, sat::bool_var w); @@ -85,12 +90,12 @@ namespace sls { void import_phase_from_smt(); void import_values_from_sls(); void export_values_from_sls(); + void export_phase_from_sls(); void import_activity_from_sls(); bool export_phase_to_sls(); bool export_units_to_sls(); void export_values_to_smt(); void export_activity_to_smt(); - void export_phase_to_smt(); void export_from_sls(); @@ -106,9 +111,12 @@ namespace sls { void updt_params(params_ref& p) {} std::ostream& display(std::ostream& out) override; + void bounded_run(unsigned max_iterations); + bool export_to_sls(); void import_from_sls(); bool completed() { return m_completed; } + lbool result() { return m_result; } void add_unit(sat::literal lit); // local_search_plugin: @@ -124,12 +132,13 @@ namespace sls { m_sls_model = mdl; } - void init_search() override {} - - void finish_search() override {} - void on_rescale() override {} + void smt_phase_to_sls(); + void smt_values_to_sls(); + void sls_phase_to_smt(); + void sls_values_to_smt(); + void sls_activity_to_smt(); // sat_solver_context: diff --git a/src/ast/sls/sls_smt_solver.cpp b/src/ast/sls/sls_smt_solver.cpp index 09efea199..0960ba6bd 100644 --- a/src/ast/sls/sls_smt_solver.cpp +++ b/src/ast/sls/sls_smt_solver.cpp @@ -42,10 +42,6 @@ namespace sls { m.limit().pop_child(&m_ddfw.rlimit()); } - void init_search() override {} - - void finish_search() override {} - void on_rescale() override {} void on_restart() override { diff --git a/src/sat/smt/sls_solver.cpp b/src/sat/smt/sls_solver.cpp index 0eb01ff85..45b4c5951 100644 --- a/src/sat/smt/sls_solver.cpp +++ b/src/sat/smt/sls_solver.cpp @@ -40,7 +40,7 @@ namespace sls { return s().params(); } - void solver::initialize_value(expr* t, expr* v) { + void solver::set_value(expr* t, expr* v) { ctx.user_propagate_initialize_value(t, v); } diff --git a/src/sat/smt/sls_solver.h b/src/sat/smt/sls_solver.h index 35f4e1b7d..0378f5845 100644 --- a/src/sat/smt/sls_solver.h +++ b/src/sat/smt/sls_solver.h @@ -92,13 +92,16 @@ namespace sls { ast_manager& get_manager() override { return m; } params_ref get_params() override; - void initialize_value(expr* t, expr* v) override; + void set_value(expr* t, expr* v) override; void force_phase(sat::literal lit) override; void set_has_new_best_phase(bool b) override; bool get_best_phase(sat::bool_var v) override; expr* bool_var2expr(sat::bool_var v) override; void set_finished() override; + void inc_activity(sat::bool_var v, double inc) override {} unsigned get_num_bool_vars() const override; + bool parallel_mode() const override { return false; } + bool get_value(expr* v, expr_ref& value) override { return false; } }; diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 71587b5cc..bfa310866 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -50,6 +50,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_threads_cube_frequency = p.threads_cube_frequency(); m_core_validate = p.core_validate(); m_sls_enable = p.sls_enable(); + m_sls_parallel = p.sls_parallel(); m_logic = _p.get_sym("logic", m_logic); m_string_solver = p.string_solver(); m_up_persist_clauses = p.up_persist_clauses(); diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 0ef063e4a..7a14aa1da 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -115,6 +115,7 @@ struct smt_params : public preprocessor_params, bool m_clause_proof = false; symbol m_proof_log; bool m_sls_enable = false; + bool m_sls_parallel = true; // ----------------------------------- // diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 1ef795e4b..23ea55af6 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -137,6 +137,7 @@ def_module_params(module_name='smt', ('str.fixed_length_refinement', BOOL, False, 'use abstraction refinement in fixed-length equation solver (Z3str3 only)'), ('str.fixed_length_naive_cex', BOOL, True, 'construct naive counterexamples when fixed-length model construction fails for a given length assignment (Z3str3 only)'), ('sls.enable', BOOL, False, 'enable sls co-processor with SMT engine'), + ('sls.parallel', BOOL, True, 'use sls co-processor in parallel or sequential with SMT engine'), ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'), ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'), ('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'), diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index f1d880930..2358ebedf 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1193,9 +1193,9 @@ namespace smt { void rescale_bool_var_activity(); public: - void inc_bvar_activity(bool_var v) { + void inc_bvar_activity(bool_var v, double inc = 1.0) { double & act = m_activity[v]; - act += m_bvar_inc; + act += m_bvar_inc * inc; if (act > ACTIVITY_LIMIT) rescale_bool_var_activity(); m_case_split_queue->activity_increased_eh(v); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 0d16120b1..caecc628b 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1494,6 +1494,11 @@ bool theory_seq::internalize_term(app* term) { bool_var bv = ctx.mk_bool_var(term); ctx.set_var_theory(bv, get_id()); ctx.mark_as_relevant(bv); +#if 1 + // experiment + if (m_util.str.is_contains(term)) + init_length_limit_for_contains(term); +#endif } enode* e = nullptr; @@ -1533,6 +1538,20 @@ void theory_seq::add_length(expr* l) { m_trail_stack.push(insert_obj_trail(m_has_length, e)); } + +void theory_seq::init_length_limit_for_contains(expr* c) { + if (ctx.is_searching()) + return; + expr* x, *y; + VERIFY(m_util.str.is_contains(c, x, y)); + unsigned min_y = m_util.str.min_length(y); + if (min_y > 0) { + unsigned old_min_y = 0; + m_length_limit_map.find(x, old_min_y); + add_length_limit(x, old_min_y + min_y, false); + } +} + /** Add length limit restrictions to sequence s. */ diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index d469097d8..a6539bded 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -562,6 +562,7 @@ namespace smt { void enforce_length_coherence(enode* n1, enode* n2); void add_length_limit(expr* s, unsigned k, bool is_searching); + void init_length_limit_for_contains(expr* c); // model-check the functions that convert integers to strings and the other way. void add_int_string(expr* e); diff --git a/src/smt/theory_sls.cpp b/src/smt/theory_sls.cpp index d0b0378bd..0fac7cace 100644 --- a/src/smt/theory_sls.cpp +++ b/src/smt/theory_sls.cpp @@ -37,13 +37,12 @@ namespace smt { return ctx.get_params(); } - void theory_sls::initialize_value(expr* t, expr* v) { - //ctx.user_propagate_initialize_value(t, v); + void theory_sls::set_value(expr* t, expr* v) { + ctx.user_propagate_initialize_value(t, v); } void theory_sls::force_phase(sat::literal lit) { - // - // ctx.force_phase(lit); + ctx.force_phase(lit); } void theory_sls::set_has_new_best_phase(bool b) { @@ -51,7 +50,7 @@ namespace smt { } bool theory_sls::get_best_phase(sat::bool_var v) { - return false; + return ctx.get_assignment(v) == l_true; } expr* theory_sls::bool_var2expr(sat::bool_var v) { @@ -61,6 +60,15 @@ namespace smt { void theory_sls::set_finished() { ctx.set_sls_completed(); } + + bool theory_sls::get_value(expr* v, expr_ref& value) { + auto* n = ctx.get_enode(v); + return n && ctx.get_value(n, value); + } + + void theory_sls::inc_activity(sat::bool_var v, double inc) { + ctx.inc_bvar_activity(v, inc); + } unsigned theory_sls::get_num_bool_vars() const { return ctx.get_num_bool_vars(); @@ -85,7 +93,7 @@ namespace smt { m_smt_plugin->check(fmls, clauses); return; } - if (!m_smt_plugin) + if (!m_smt_plugin || !m_parallel_mode) return; if (!m_smt_plugin->completed()) return; @@ -103,18 +111,20 @@ namespace smt { for (; m_trail_lim < lits.size() && ctx.get_assign_level(lits[m_trail_lim]) == scope_lvl; ++m_trail_lim) m_smt_plugin->add_unit(lits[m_trail_lim]); } + + ++m_difference_score; // blindly assume we backtrack over initial clauses. #if 0 if (ctx.has_new_best_phase()) m_smt_plugin->import_phase_from_smt(); -#endif - - // m_smt_plugin->import_from_sls(); +#endif } void theory_sls::init() { if (m_smt_plugin) finalize(); + smt_params p(ctx.get_fparams()); + m_parallel_mode = p.m_sls_parallel; m_smt_plugin = alloc(sls::smt_plugin, *this); m_checking = false; } @@ -123,11 +133,52 @@ namespace smt { st.copy(m_st); } - void theory_sls::display(std::ostream& out) const { - out << "theory-sls\n"; + void theory_sls::restart_eh() { + if (m_parallel_mode || !m_smt_plugin) + return; + + if (ctx.m_stats.m_num_restarts >= m_threshold + 5) { + m_threshold *= 2; + bounded_run(m_restart_ls_steps); + m_smt_plugin->sls_activity_to_smt(); + } + m_difference_score = 0; + m_difference_score_threshold = 1; } + void theory_sls::bounded_run(unsigned num_steps) { + m_smt_plugin->bounded_run(num_steps); + if (m_smt_plugin->result() == l_true) { + m_smt_plugin->finalize(m_model, m_st); + m_smt_plugin = nullptr; + } + } + final_check_status theory_sls::final_check_eh() { + if (m_parallel_mode || !m_smt_plugin) + return FC_DONE; + if (m_difference_score < m_difference_score_threshold + 100) + return FC_DONE; + + ++m_difference_score_threshold; + m_difference_score = 0; + ++m_num_guided_sls; + + m_smt_plugin->smt_phase_to_sls(); + m_smt_plugin->smt_values_to_sls(); + bounded_run(m_final_check_ls_steps); + dec_final_check_ls_steps(); + m_smt_plugin->sls_phase_to_smt(); + m_smt_plugin->sls_values_to_smt(); + if (m_num_guided_sls % 20 == 0) + m_smt_plugin->sls_activity_to_smt(); + + return FC_DONE; + } + + void theory_sls::display(std::ostream& out) const { + out << "theory-sls\n"; + } #endif } diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h index 581d7d460..d57b35945 100644 --- a/src/smt/theory_sls.h +++ b/src/smt/theory_sls.h @@ -54,9 +54,30 @@ namespace smt { sls::smt_plugin* m_smt_plugin = nullptr; unsigned m_trail_lim = 0; bool m_checking = false; + bool m_parallel_mode = true; + unsigned m_threshold = 1; + unsigned m_restart_sls_count = 0; + unsigned m_difference_score = 0; + unsigned m_difference_score_threshold = 0; + unsigned m_num_guided_sls = 0; + unsigned m_restart_ls_steps = 100000; + unsigned m_restart_ls_steps_inc = 10000; + unsigned m_restart_ls_steps_max = 300000; + unsigned m_final_check_ls_steps = 30000; + unsigned m_final_check_ls_steps_dec = 10000; + unsigned m_final_check_ls_steps_min = 10000; ::statistics m_st; void finalize(); + void bounded_run(unsigned num_steps); + void inc_restart_ls_steps() { + if (m_restart_ls_steps < m_restart_ls_steps_max) + m_restart_ls_steps += m_restart_ls_steps_inc; + } + void dec_final_check_ls_steps() { + if (m_final_check_ls_steps > m_final_check_ls_steps_min) + m_final_check_ls_steps -= m_final_check_ls_steps_dec; + } public: theory_sls(context& ctx); @@ -75,17 +96,22 @@ namespace smt { bool internalize_term(app* term) override { return false; } void new_eq_eh(theory_var v1, theory_var v2) override {} void new_diseq_eh(theory_var v1, theory_var v2) override {} + void restart_eh() override; + final_check_status final_check_eh() override; // sls::smt_context interface ast_manager& get_manager() override { return m; } params_ref get_params() override; - void initialize_value(expr* t, expr* v) override; + void set_value(expr* t, expr* v) override; void force_phase(sat::literal lit) override; void set_has_new_best_phase(bool b) override; bool get_best_phase(sat::bool_var v) override; expr* bool_var2expr(sat::bool_var v) override; void set_finished() override; unsigned get_num_bool_vars() const override; + void inc_activity(sat::bool_var v, double inc) override; + bool parallel_mode() const { return m_parallel_mode; } + bool get_value(expr* v, expr_ref& value) override; }; }