mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

use independent completion flag for sls to avoid conflating with genuine cancelation

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-10-26 14:48:13 -07:00
parent 646eacd2aa
commit c6f5e3232c
3 changed files with 12 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_context.cpp
View file

@ -104,6 +104,8 @@ namespace smt {
*/ */
bool context::get_cancel_flag() { bool context::get_cancel_flag() {
if (l_true == m_sls_completed)
return true;
if (m.limit().inc()) if (m.limit().inc())
return false; return false;
m_last_search_failure = CANCELED; m_last_search_failure = CANCELED;
@ -3507,10 +3509,11 @@ namespace smt {
if (r == l_true && get_cancel_flag()) { if (r == l_true && get_cancel_flag()) {
r = l_undef; r = l_undef;
} }
if (r == l_undef && get_cancel_flag() && has_sls_model()) { if (r == l_undef && m_sls_completed == l_true && has_sls_model()) {
m.limit().reset_cancel(); m.limit().reset_cancel();
r = l_true; r = l_true;
} }
m_sls_completed = l_false;
if (r == l_true && gparams::get_value("model_validate") == "true") { if (r == l_true && gparams::get_value("model_validate") == "true") {
recfun::util u(m); recfun::util u(m);
if (u.get_rec_funs().empty() && m_proto_model) { if (u.get_rec_funs().empty() && m_proto_model) {
@ -3750,6 +3753,7 @@ namespace smt {
m_phase_default = false; m_phase_default = false;
m_case_split_queue ->init_search_eh(); m_case_split_queue ->init_search_eh();
m_next_progress_sample = 0; m_next_progress_sample = 0;
m_sls_completed = l_undef;
if (m.has_type_vars() && !m_theories.get_plugin(poly_family_id)) if (m.has_type_vars() && !m_theories.get_plugin(poly_family_id))
register_plugin(alloc(theory_polymorphism, *this)); register_plugin(alloc(theory_polymorphism, *this));
TRACE("literal_occ", display_literal_num_occs(tout);); TRACE("literal_occ", display_literal_num_occs(tout););

6
src/smt/smt_context.h
View file

@ -128,6 +128,7 @@ namespace smt {
class parallel* m_par = nullptr; class parallel* m_par = nullptr;
unsigned m_par_index = 0; unsigned m_par_index = 0;
bool m_internalizing_assertions = false; bool m_internalizing_assertions = false;
lbool m_sls_completed = l_undef;
// ----------------------------------- // -----------------------------------
@ -288,6 +289,11 @@ namespace smt {
bool get_cancel_flag(); bool get_cancel_flag();
void set_sls_completed() {
if (m_sls_completed == l_undef)
m_sls_completed = l_true;
}
region & get_region() { region & get_region() {
return m_region; return m_region;
} }

2
src/smt/theory_sls.cpp
View file

@ -58,7 +58,7 @@ namespace smt {
} }
void theory_sls::set_finished() { void theory_sls::set_finished() {
m.limit().cancel(); ctx.set_sls_completed();
} }
unsigned theory_sls::get_num_bool_vars() const { unsigned theory_sls::get_num_bool_vars() const {