diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 52b21dd80..42e382790 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -128,6 +128,10 @@ namespace smt { return literal(v, lit.sign()); } + bool context::get_cancel_flag() { + return !m_manager.limit().inc(); + } + void context::copy(context& src_ctx, context& dst_ctx) { ast_manager& dst_m = dst_ctx.get_manager(); @@ -235,10 +239,8 @@ namespace smt { } // copy theory plugins - ptr_vector::iterator it2 = src.m_theory_set.begin(); - ptr_vector::iterator end2 = src.m_theory_set.end(); - for (; it2 != end2; ++it2) { - theory * new_th = (*it2)->mk_fresh(&dst); + for (theory* old_th : src.m_theory_set) { + theory * new_th = old_th->mk_fresh(&dst); dst.register_plugin(new_th); } } @@ -248,9 +250,7 @@ namespace smt { new_ctx->set_logic(l == 0 ? m_setup.get_logic() : *l); copy_plugins(*this, *new_ctx); return new_ctx; - } - - + } void context::init() { app * t = m_manager.mk_true(); @@ -2403,81 +2403,86 @@ namespace smt { */ unsigned context::pop_scope_core(unsigned num_scopes) { - 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);); - SASSERT(num_scopes > 0); - SASSERT(num_scopes <= m_scope_lvl); - SASSERT(m_scopes.size() == m_scope_lvl); - - unsigned new_lvl = m_scope_lvl - num_scopes; - - cache_generation(new_lvl); - 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("context", tout << "backtracking new_lvl: " << new_lvl << "\n";); - - 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]; - del_clauses(m_lemmas, bs.m_lemmas_lim); - m_simp_qhead = bs.m_simp_qhead_lim; - if (!bs.m_inconsistent) { - m_conflict = null_b_justification; - m_not_l = null_literal; - m_unsat_proof = 0; + try { + 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);); + SASSERT(num_scopes > 0); + SASSERT(num_scopes <= m_scope_lvl); + SASSERT(m_scopes.size() == m_scope_lvl); + + unsigned new_lvl = m_scope_lvl - num_scopes; + + cache_generation(new_lvl); + 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("context", tout << "backtracking new_lvl: " << new_lvl << "\n";); + + 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]; + del_clauses(m_lemmas, bs.m_lemmas_lim); + m_simp_qhead = bs.m_simp_qhead_lim; + if (!bs.m_inconsistent) { + m_conflict = null_b_justification; + 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; - m_not_l = null_literal; + else { + 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); - - 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); - - ptr_vector::iterator it = m_theory_set.begin(); - ptr_vector::iterator end = m_theory_set.end(); - for (; it != end; ++it) { - (*it)->pop_scope_eh(num_scopes); + catch (...) { + // throwing inside pop is just not cool. + UNREACHABLE(); + throw; } - - 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) { @@ -3418,10 +3423,9 @@ namespace smt { } void context::init_search() { - ptr_vector::iterator it = m_theory_set.begin(); - ptr_vector::iterator end = m_theory_set.end(); - for (; it != end; ++it) - (*it)->init_search_eh(); + for (theory* th : m_theory_set) { + th->init_search_eh(); + } m_qmanager->init_search_eh(); m_assumption_core.reset(); m_incomplete_theories.reset(); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 1aa3b385b..fecb42700 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -257,15 +257,7 @@ namespace smt { return m_params; } - bool get_cancel_flag() { - if (m_manager.limit().inc()) { - // get_simplifier().reset(); - return false; - } - else { - return true; - } - } + bool get_cancel_flag(); region & get_region() { return m_region; diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index f0f80b4ec..a1558e5e5 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -2106,6 +2106,7 @@ namespace smt { template void theory_arith::mutate_assignment() { + SASSERT(m_to_patch.empty()); remove_fixed_vars_from_base(); int num_vars = get_num_vars(); m_var_value_table.reset(); @@ -2131,12 +2132,9 @@ namespace smt { } if (candidates.empty()) return; - typename sbuffer::iterator it = candidates.begin(); - typename sbuffer::iterator end = candidates.end(); m_tmp_var_set.reset(); m_tmp_var_set2.reset(); - for (; it != end; ++it) { - theory_var v = *it; + for (theory_var v : candidates) { SASSERT(!is_fixed(v)); if (is_base(v)) { row & r = m_rows[get_var_row(v)]; diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index e10395d31..a30e51133 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -449,6 +449,7 @@ namespace smt { proof_ref pr(m); s(ante, s_ante, pr); + if (ctx.get_cancel_flag()) return; negated = m.is_not(s_ante, s_ante_n); if (negated) s_ante = s_ante_n; ctx.internalize(s_ante, false); @@ -456,6 +457,7 @@ namespace smt { if (negated) l_ante.neg(); s(conseq, s_conseq, pr); + if (ctx.get_cancel_flag()) return; negated = m.is_not(s_conseq, s_conseq_n); if (negated) s_conseq = s_conseq_n; ctx.internalize(s_conseq, false); @@ -1413,6 +1415,12 @@ namespace smt { final_check_status result = FC_DONE; final_check_status ok; 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";); switch (m_final_check_idx) { case 0: @@ -2307,7 +2315,7 @@ namespace smt { return false; } TRACE("arith_make_feasible_detail", display(tout);); - if (get_context().get_cancel_flag()) { + if (get_context().get_cancel_flag()) { return true; } }