diff --git a/src/ast/sls/sls_smt_plugin.cpp b/src/ast/sls/sls_smt_plugin.cpp index 6d0cb0e0a45..85227190cba 100644 --- a/src/ast/sls/sls_smt_plugin.cpp +++ b/src/ast/sls/sls_smt_plugin.cpp @@ -106,7 +106,6 @@ namespace sls { m_rewards[v] = m_ddfw->get_reward_avg(w); } m_completed = true; - m_min_unsat_size = UINT_MAX; } void smt_plugin::bounded_run(unsigned max_iterations) { @@ -140,6 +139,20 @@ namespace sls { // m_ddfw owns the pointer to smt_plugin and destructs it. dealloc(d); } + + void smt_plugin::get_shared_clauses(vector& _clauses) { + _clauses.reset(); + for (auto const& clause : clauses()) { + if (!all_of(clause.m_clause, [&](sat::literal lit) { + return m_sls_bool_var2smt_bool_var.get(lit.var(), sat::null_bool_var) != sat::null_bool_var; + })) + continue; + sat::literal_vector cl; + for (auto lit : clause) + cl.push_back(sat::literal(m_sls_bool_var2smt_bool_var[lit.var()], lit.sign())); + _clauses.push_back(cl); + } + } std::ostream& smt_plugin::display(std::ostream& out) { m_ddfw->display(out); diff --git a/src/ast/sls/sls_smt_plugin.h b/src/ast/sls/sls_smt_plugin.h index 616fd801c01..2e74b793fc9 100644 --- a/src/ast/sls/sls_smt_plugin.h +++ b/src/ast/sls/sls_smt_plugin.h @@ -107,6 +107,7 @@ namespace sls { // interface to calling solver: void check(expr_ref_vector const& fmls, vector const& clauses); void finalize(model_ref& md, ::statistics& st); + void get_shared_clauses(vector& clauses); void updt_params(params_ref& p) {} std::ostream& display(std::ostream& out) override; diff --git a/src/smt/theory_sls.cpp b/src/smt/theory_sls.cpp index ee9a8d9f3c2..0127c229c70 100644 --- a/src/smt/theory_sls.cpp +++ b/src/smt/theory_sls.cpp @@ -84,21 +84,23 @@ namespace smt { } void theory_sls::propagate() { - if (m_smt_plugin && !m_checking) { + if (!m_smt_plugin) + return; + if (!m_checking) { expr_ref_vector fmls(m); for (unsigned i = 0; i < ctx.get_num_asserted_formulas(); ++i) fmls.push_back(ctx.get_asserted_formula(i)); m_checking = true; vector clauses; m_smt_plugin->check(fmls, clauses); - return; + m_smt_plugin->get_shared_clauses(m_shared_clauses); + } + else if (!m_parallel_mode) + propagate_local_search(); + else if (m_smt_plugin->completed()) { + m_smt_plugin->finalize(m_model, m_st); + m_smt_plugin = nullptr; } - if (!m_smt_plugin || !m_parallel_mode) - return; - if (!m_smt_plugin->completed()) - return; - m_smt_plugin->finalize(m_model, m_st); - m_smt_plugin = nullptr; } void theory_sls::pop_scope_eh(unsigned n) { @@ -111,14 +113,67 @@ namespace smt { m_smt_plugin->add_unit(lits[m_trail_lim]); } - ++m_difference_score; // blindly assume we backtrack over initial clauses. + check_for_unassigned_clause_after_resolve(); #if 0 if (ctx.has_new_best_phase()) m_smt_plugin->import_phase_from_smt(); -#endif +#endif } + // + // hybrid-smt uses a heuristic to determine when to restart local search. + // it is based on when the assignment to shared clauses has a change in literal assignment. + // + void theory_sls::check_for_unassigned_clause_after_resolve() { + if (m_has_unassigned_clause_after_resolve) { + m_after_resolve_decide_count = 0; + if (m_after_resolve_decide_gap >= 16) + m_after_resolve_decide_gap /= 4; + } + else if (!shared_clauses_are_true()) { + m_resolve_count++; + if (m_resolve_count > m_resolve_gap) { + m_resolve_gap++; + m_has_unassigned_clause_after_resolve = true; + m_resolve_count = 0; + m_after_resolve_decide_count = 0; + m_after_resolve_decide_gap = 4; + } + } + } + + void theory_sls::propagate_local_search() { + if (!m_has_unassigned_clause_after_resolve) + return; + if (m_parallel_mode || !m_smt_plugin) + return; + ++m_after_resolve_decide_count; + if (100 + m_after_resolve_decide_gap > m_after_resolve_decide_count) + return; + m_after_resolve_decide_gap *= 2; + if (!shared_clauses_are_true()) + return; + m_resolve_count = 0; + m_has_unassigned_clause_after_resolve = false; + run_guided_sls(); + } + + void theory_sls::run_guided_sls() { + ++m_num_guided_sls; + m_smt_plugin->smt_phase_to_sls(); + m_smt_plugin->smt_units_to_sls(); + m_smt_plugin->smt_values_to_sls(); + bounded_run(m_final_check_ls_steps); + dec_final_check_ls_steps(); + if (m_smt_plugin) { + 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(); + } + } + void theory_sls::init() { if (m_smt_plugin) finalize(); @@ -158,27 +213,21 @@ namespace smt { 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) + ++m_after_resolve_decide_count; + if (m_after_resolve_decide_gap > m_after_resolve_decide_count) 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_units_to_sls(); - m_smt_plugin->smt_values_to_sls(); - bounded_run(m_final_check_ls_steps); - dec_final_check_ls_steps(); - if (m_smt_plugin) { - 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(); - } + m_after_resolve_decide_gap *= 2; + run_guided_sls(); return FC_DONE; } + bool theory_sls::shared_clauses_are_true() const { + for (auto const& cl : m_shared_clauses) + if (all_of(cl, [this](sat::literal lit) { return ctx.get_assignment(lit) != l_true; })) + return false; + return true; + } + void theory_sls::display(std::ostream& out) const { out << "theory-sls\n"; } diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h index d7e3c7ba176..65b4aef0743 100644 --- a/src/smt/theory_sls.h +++ b/src/smt/theory_sls.h @@ -65,7 +65,13 @@ namespace smt { unsigned m_final_check_ls_steps = 30000; unsigned m_final_check_ls_steps_dec = 10000; unsigned m_final_check_ls_steps_min = 10000; + bool m_has_unassigned_clause_after_resolve = false; + unsigned m_after_resolve_decide_gap = 4; + unsigned m_after_resolve_decide_count = 0; + unsigned m_resolve_count = 0; + unsigned m_resolve_gap = 0; ::statistics m_st; + vector m_shared_clauses; void finalize(); void bounded_run(unsigned num_steps); @@ -78,6 +84,12 @@ namespace smt { m_final_check_ls_steps -= m_final_check_ls_steps_dec; } + bool shared_clauses_are_true() const; + void check_for_unassigned_clause_after_resolve(); + void propagate_local_search(); + + void run_guided_sls(); + public: theory_sls(context& ctx); ~theory_sls() override;