mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-12 14:10:54 +00:00
Code Activity

address inconsistent states encountered when cancelling, #1197

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-13 13:40:30 -07:00
parent 19bb55e396
commit 00742566fb
4 changed files with 99 additions and 97 deletions
Download patch file Download diff file Expand all files Collapse all files

170
src/smt/smt_context.cpp
View file

@ -128,6 +128,10 @@ namespace smt {
return literal(v, lit.sign()); return literal(v, lit.sign());
} }
bool context::get_cancel_flag() {
return !m_manager.limit().inc();
}
void context::copy(context& src_ctx, context& dst_ctx) { void context::copy(context& src_ctx, context& dst_ctx) {
ast_manager& dst_m = dst_ctx.get_manager(); ast_manager& dst_m = dst_ctx.get_manager();
@ -235,10 +239,8 @@ namespace smt {
} }
// copy theory plugins // copy theory plugins
ptr_vector<theory>::iterator it2 = src.m_theory_set.begin(); for (theory* old_th : src.m_theory_set) {
ptr_vector<theory>::iterator end2 = src.m_theory_set.end(); theory * new_th = old_th->mk_fresh(&dst);
for (; it2 != end2; ++it2) {
theory * new_th = (*it2)->mk_fresh(&dst);
dst.register_plugin(new_th); dst.register_plugin(new_th);
} }
} }
@ -248,9 +250,7 @@ namespace smt {
new_ctx->set_logic(l == 0 ? m_setup.get_logic() : *l); new_ctx->set_logic(l == 0 ? m_setup.get_logic() : *l);
copy_plugins(*this, *new_ctx); copy_plugins(*this, *new_ctx);
return new_ctx; return new_ctx;
} }
void context::init() { void context::init() {
app * t = m_manager.mk_true(); app * t = m_manager.mk_true();
@ -2403,81 +2403,86 @@ namespace smt {
*/ */
unsigned context::pop_scope_core(unsigned num_scopes) { unsigned context::pop_scope_core(unsigned num_scopes) {
if (m_manager.has_trace_stream()) try {
m_manager.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n"; if (m_manager.has_trace_stream())
m_manager.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n";
TRACE("context", tout << "backtracking: " << num_scopes << " from " << m_scope_lvl << "\n";);
TRACE("pop_scope_detail", display(tout);); TRACE("context", tout << "backtracking: " << num_scopes << " from " << m_scope_lvl << "\n";);
SASSERT(num_scopes > 0); TRACE("pop_scope_detail", display(tout););
SASSERT(num_scopes <= m_scope_lvl); SASSERT(num_scopes > 0);
SASSERT(m_scopes.size() == m_scope_lvl); SASSERT(num_scopes <= m_scope_lvl);
SASSERT(m_scopes.size() == m_scope_lvl);
unsigned new_lvl = m_scope_lvl - num_scopes;
unsigned new_lvl = m_scope_lvl - num_scopes;
cache_generation(new_lvl);
m_qmanager->pop(num_scopes); cache_generation(new_lvl);
m_case_split_queue->pop_scope(num_scopes); m_qmanager->pop(num_scopes);
m_case_split_queue->pop_scope(num_scopes);
TRACE("pop_scope", tout << "backtracking: " << num_scopes << ", new_lvl: " << new_lvl << "\n";);
scope & s = m_scopes[new_lvl]; TRACE("pop_scope", tout << "backtracking: " << num_scopes << ", new_lvl: " << new_lvl << "\n";);
TRACE("context", tout << "backtracking new_lvl: " << new_lvl << "\n";); scope & s = m_scopes[new_lvl];
TRACE("context", tout << "backtracking new_lvl: " << new_lvl << "\n";);
unsigned units_to_reassert_lim = s.m_units_to_reassert_lim;
unsigned units_to_reassert_lim = s.m_units_to_reassert_lim;
if (new_lvl < m_base_lvl) {
base_scope & bs = m_base_scopes[new_lvl]; if (new_lvl < m_base_lvl) {
del_clauses(m_lemmas, bs.m_lemmas_lim); base_scope & bs = m_base_scopes[new_lvl];
m_simp_qhead = bs.m_simp_qhead_lim; del_clauses(m_lemmas, bs.m_lemmas_lim);
if (!bs.m_inconsistent) { m_simp_qhead = bs.m_simp_qhead_lim;
m_conflict = null_b_justification; if (!bs.m_inconsistent) {
m_not_l = null_literal; m_conflict = null_b_justification;
m_unsat_proof = 0; m_not_l = null_literal;
m_unsat_proof = 0;
}
m_base_scopes.shrink(new_lvl);
} }
m_base_scopes.shrink(new_lvl); else {
} m_conflict = null_b_justification;
else { m_not_l = null_literal;
m_conflict = null_b_justification; }
m_not_l = null_literal; del_clauses(m_aux_clauses, s.m_aux_clauses_lim);
m_relevancy_propagator->pop(num_scopes);
m_fingerprints.pop_scope(num_scopes);
unassign_vars(s.m_assigned_literals_lim);
undo_trail_stack(s.m_trail_stack_lim);
for (theory* th : m_theory_set) {
th->pop_scope_eh(num_scopes);
}
del_justifications(m_justifications, s.m_justifications_lim);
m_asserted_formulas.pop_scope(num_scopes);
m_eq_propagation_queue.reset();
m_th_eq_propagation_queue.reset();
m_th_diseq_propagation_queue.reset();
m_atom_propagation_queue.reset();
m_region.pop_scope(num_scopes);
m_scopes.shrink(new_lvl);
m_scope_lvl = new_lvl;
if (new_lvl < m_base_lvl) {
m_base_lvl = new_lvl;
m_search_lvl = new_lvl; // Remark: not really necessary
}
unsigned num_bool_vars = get_num_bool_vars();
// any variable >= num_bool_vars was deleted during backtracking.
reinit_clauses(num_scopes, num_bool_vars);
reassert_units(units_to_reassert_lim);
TRACE("pop_scope_detail", tout << "end of pop_scope: \n"; display(tout););
CASSERT("context", check_invariant());
return num_bool_vars;
} }
del_clauses(m_aux_clauses, s.m_aux_clauses_lim); catch (...) {
// throwing inside pop is just not cool.
m_relevancy_propagator->pop(num_scopes); UNREACHABLE();
throw;
m_fingerprints.pop_scope(num_scopes);
unassign_vars(s.m_assigned_literals_lim);
undo_trail_stack(s.m_trail_stack_lim);
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end; ++it) {
(*it)->pop_scope_eh(num_scopes);
} }
del_justifications(m_justifications, s.m_justifications_lim);
m_asserted_formulas.pop_scope(num_scopes);
m_eq_propagation_queue.reset();
m_th_eq_propagation_queue.reset();
m_th_diseq_propagation_queue.reset();
m_atom_propagation_queue.reset();
m_region.pop_scope(num_scopes);
m_scopes.shrink(new_lvl);
m_scope_lvl = new_lvl;
if (new_lvl < m_base_lvl) {
m_base_lvl = new_lvl;
m_search_lvl = new_lvl; // Remark: not really necessary
}
unsigned num_bool_vars = get_num_bool_vars();
// any variable >= num_bool_vars was deleted during backtracking.
reinit_clauses(num_scopes, num_bool_vars);
reassert_units(units_to_reassert_lim);
TRACE("pop_scope_detail", tout << "end of pop_scope: \n"; display(tout););
CASSERT("context", check_invariant());
return num_bool_vars;
} }
void context::pop_scope(unsigned num_scopes) { void context::pop_scope(unsigned num_scopes) {
@ -3418,10 +3423,9 @@ namespace smt {
} }
void context::init_search() { void context::init_search() {
ptr_vector<theory>::iterator it = m_theory_set.begin(); for (theory* th : m_theory_set) {
ptr_vector<theory>::iterator end = m_theory_set.end(); th->init_search_eh();
for (; it != end; ++it) }
(*it)->init_search_eh();
m_qmanager->init_search_eh(); m_qmanager->init_search_eh();
m_assumption_core.reset(); m_assumption_core.reset();
m_incomplete_theories.reset(); m_incomplete_theories.reset();

10
src/smt/smt_context.h
View file

@ -257,15 +257,7 @@ namespace smt {
return m_params; return m_params;
} }
bool get_cancel_flag() { bool get_cancel_flag();
if (m_manager.limit().inc()) {
// get_simplifier().reset();
return false;
}
else {
return true;
}
}
region & get_region() { region & get_region() {
return m_region; return m_region;

6
src/smt/theory_arith_aux.h
View file

@ -2106,6 +2106,7 @@ namespace smt {
template<typename Ext> template<typename Ext>
void theory_arith<Ext>::mutate_assignment() { void theory_arith<Ext>::mutate_assignment() {
SASSERT(m_to_patch.empty());
remove_fixed_vars_from_base(); remove_fixed_vars_from_base();
int num_vars = get_num_vars(); int num_vars = get_num_vars();
m_var_value_table.reset(); m_var_value_table.reset();
@ -2131,12 +2132,9 @@ namespace smt {
} }
if (candidates.empty()) if (candidates.empty())
return; return;
typename sbuffer<theory_var>::iterator it = candidates.begin();
typename sbuffer<theory_var>::iterator end = candidates.end();
m_tmp_var_set.reset(); m_tmp_var_set.reset();
m_tmp_var_set2.reset(); m_tmp_var_set2.reset();
for (; it != end; ++it) { for (theory_var v : candidates) {
theory_var v = *it;
SASSERT(!is_fixed(v)); SASSERT(!is_fixed(v));
if (is_base(v)) { if (is_base(v)) {
row & r = m_rows[get_var_row(v)]; row & r = m_rows[get_var_row(v)];

10
src/smt/theory_arith_core.h
View file

@ -449,6 +449,7 @@ namespace smt {
proof_ref pr(m); proof_ref pr(m);
s(ante, s_ante, pr); s(ante, s_ante, pr);
if (ctx.get_cancel_flag()) return;
negated = m.is_not(s_ante, s_ante_n); negated = m.is_not(s_ante, s_ante_n);
if (negated) s_ante = s_ante_n; if (negated) s_ante = s_ante_n;
ctx.internalize(s_ante, false); ctx.internalize(s_ante, false);
@ -456,6 +457,7 @@ namespace smt {
if (negated) l_ante.neg(); if (negated) l_ante.neg();
s(conseq, s_conseq, pr); s(conseq, s_conseq, pr);
if (ctx.get_cancel_flag()) return;
negated = m.is_not(s_conseq, s_conseq_n); negated = m.is_not(s_conseq, s_conseq_n);
if (negated) s_conseq = s_conseq_n; if (negated) s_conseq = s_conseq_n;
ctx.internalize(s_conseq, false); ctx.internalize(s_conseq, false);
@ -1413,6 +1415,12 @@ namespace smt {
final_check_status result = FC_DONE; final_check_status result = FC_DONE;
final_check_status ok; final_check_status ok;
do { do {
if (get_context().get_cancel_flag()) {
return FC_GIVEUP;
}
SASSERT(m_to_patch.empty());
TRACE("arith", tout << "m_final_check_idx: " << m_final_check_idx << ", result: " << result << "\n";); TRACE("arith", tout << "m_final_check_idx: " << m_final_check_idx << ", result: " << result << "\n";);
switch (m_final_check_idx) { switch (m_final_check_idx) {
case 0: case 0:
@ -2307,7 +2315,7 @@ namespace smt {
return false; return false;
} }
TRACE("arith_make_feasible_detail", display(tout);); TRACE("arith_make_feasible_detail", display(tout););
if (get_context().get_cancel_flag()) { if (get_context().get_cancel_flag()) {
return true; return true;
} }
} }