From faa19117e40fa6850318fa777f884e65a68aae1a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 21 Jul 2017 17:42:48 +0100 Subject: [PATCH] Fixed inconsistent state upon solver interruption. Partially fixes #951. --- src/smt/cached_var_subst.cpp | 25 ++++++++++++++++--------- src/smt/qi_queue.cpp | 36 ++++++++++++++++++------------------ src/smt/smt_quantifier.cpp | 4 ++-- src/smt/smt_quantifier.h | 4 ++-- 4 files changed, 38 insertions(+), 31 deletions(-) diff --git a/src/smt/cached_var_subst.cpp b/src/smt/cached_var_subst.cpp index 1db3aa0a6..c36eb6dd2 100644 --- a/src/smt/cached_var_subst.cpp +++ b/src/smt/cached_var_subst.cpp @@ -23,7 +23,7 @@ bool cached_var_subst::key_eq_proc::operator()(cached_var_subst::key * k1, cache return false; if (k1->m_num_bindings != k2->m_num_bindings) return false; - for (unsigned i = 0; i < k1->m_num_bindings; i++) + for (unsigned i = 0; i < k1->m_num_bindings; i++) if (k1->m_bindings[i] != k2->m_bindings[i]) return false; return true; @@ -49,9 +49,9 @@ void cached_var_subst::operator()(quantifier * qa, unsigned num_bindings, smt::e new_key->m_qa = qa; new_key->m_num_bindings = num_bindings; - for (unsigned i = 0; i < num_bindings; i++) + for (unsigned i = 0; i < num_bindings; i++) new_key->m_bindings[i] = bindings[i]->get_owner(); - + instances::entry * entry = m_instances.insert_if_not_there2(new_key, 0); if (entry->get_data().m_key != new_key) { SASSERT(entry->get_data().m_value != 0); @@ -60,20 +60,27 @@ void cached_var_subst::operator()(quantifier * qa, unsigned num_bindings, smt::e result = entry->get_data().m_value; return; } - - m_proc(qa->get_expr(), new_key->m_num_bindings, new_key->m_bindings, result); + + SASSERT(entry->get_data().m_value == 0); + try { + m_proc(qa->get_expr(), new_key->m_num_bindings, new_key->m_bindings, result); + } + catch (...) { + // CMW: The var_subst reducer was interrupted and m_instances is + // in an inconsistent state; we need to remove (new_key, 0). + m_instances.remove(new_key); + throw; // Throw on to smt::qi_queue/smt::solver. + } + // cache result entry->get_data().m_value = result; // remove key from cache m_new_keys[num_bindings] = 0; - + // increment reference counters m_refs.push_back(qa); for (unsigned i = 0; i < new_key->m_num_bindings; i++) m_refs.push_back(new_key->m_bindings[i]); m_refs.push_back(result); } - - - diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index 530d0ec88..70a3041d2 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -41,7 +41,7 @@ namespace smt { init_parser_vars(); m_vals.resize(15, 0.0f); } - + qi_queue::~qi_queue() { } @@ -50,7 +50,7 @@ namespace smt { if (!m_parser.parse_string(m_params.m_qi_cost.c_str(), m_cost_function)) { // it is not reasonable to abort here during the creation of smt::context just because an invalid option was provided. // throw default_exception("invalid cost function %s", m_params.m_qi_cost.c_str()); - + // using warning message instead warning_msg("invalid cost function '%s', switching to default one", m_params.m_qi_cost.c_str()); // Trying again with default function @@ -107,7 +107,7 @@ namespace smt { m_vals[SIZE] = static_cast(stat->get_size()); m_vals[DEPTH] = static_cast(stat->get_depth()); m_vals[GENERATION] = static_cast(generation); - m_vals[QUANT_GENERATION] = static_cast(stat->get_generation()); + m_vals[QUANT_GENERATION] = static_cast(stat->get_generation()); m_vals[WEIGHT] = static_cast(q->get_weight()); m_vals[VARS] = static_cast(q->get_num_decls()); m_vals[PATTERN_WIDTH] = pat ? static_cast(pat->get_num_args()) : 1.0f; @@ -118,7 +118,7 @@ namespace smt { TRACE("qi_queue_detail", for (unsigned i = 0; i < m_vals.size(); i++) { tout << m_vals[i] << " "; } tout << "\n";); return stat; } - + float qi_queue::get_cost(quantifier * q, app * pat, unsigned generation, unsigned min_top_generation, unsigned max_top_generation) { quantifier_stat * stat = set_values(q, pat, generation, min_top_generation, max_top_generation, 0); float r = m_evaluator(m_cost_function, m_vals.size(), m_vals.c_ptr()); @@ -132,11 +132,11 @@ namespace smt { float r = m_evaluator(m_new_gen_function, m_vals.size(), m_vals.c_ptr()); return static_cast(r); } - + void qi_queue::insert(fingerprint * f, app * pat, unsigned generation, unsigned min_top_generation, unsigned max_top_generation) { quantifier * q = static_cast(f->get_data()); float cost = get_cost(q, pat, generation, min_top_generation, max_top_generation); - TRACE("qi_queue_detail", + TRACE("qi_queue_detail", tout << "new instance of " << q->get_qid() << ", weight " << q->get_weight() << ", generation: " << generation << ", scope_level: " << m_context.get_scope_level() << ", cost: " << cost << "\n"; for (unsigned i = 0; i < f->get_num_args(); i++) { @@ -157,7 +157,7 @@ namespace smt { quantifier * qa = static_cast(f->get_data()); if (curr.m_cost <= m_eager_cost_threshold) { - instantiate(curr); + instantiate(curr); } else if (m_params.m_qi_promote_unsat && m_checker.is_unsat(qa->get_expr(), f->get_num_args(), f->get_args())) { // do not delay instances that produce a conflict. @@ -193,7 +193,7 @@ namespace smt { // This nasty side-effect may change the behavior of Z3. m_manager.trace_stream() << " #" << bindings[i]->get_owner_id(); } - + #endif if (m_manager.proofs_enabled()) m_manager.trace_stream() << " #" << proof_id; @@ -233,7 +233,7 @@ namespace smt { if (m_manager.is_true(s_instance)) { TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m_manager);); - if (m_manager.has_trace_stream()) + if (m_manager.has_trace_stream()) m_manager.trace_stream() << "[end-of-instance]\n"; return; @@ -278,7 +278,7 @@ namespace smt { pr1 = m_manager.mk_modus_ponens(qi_pr, rw); } else { - app * bare_s_lemma = m_manager.mk_or(m_manager.mk_not(q), s_instance); + app * bare_s_lemma = m_manager.mk_or(m_manager.mk_not(q), s_instance); proof * prs[1] = { pr.get() }; proof * cg = m_manager.mk_congruence(bare_lemma, bare_s_lemma, 1, prs); proof * rw = m_manager.mk_rewrite(bare_s_lemma, lemma); @@ -331,13 +331,13 @@ namespace smt { s.m_instances_lim = m_instances.size(); s.m_instantiated_trail_lim = m_instantiated_trail.size(); } - + void qi_queue::pop_scope(unsigned num_scopes) { unsigned new_lvl = m_scopes.size() - num_scopes; scope & s = m_scopes[new_lvl]; unsigned old_sz = s.m_instantiated_trail_lim; unsigned sz = m_instantiated_trail.size(); - for (unsigned i = old_sz; i < sz; i++) + for (unsigned i = old_sz; i < sz; i++) m_delayed_entries[m_instantiated_trail[i]].m_instantiated = false; m_instantiated_trail.shrink(old_sz); m_delayed_entries.shrink(s.m_delayed_entries_lim); @@ -359,7 +359,7 @@ namespace smt { } bool qi_queue::final_check_eh() { - TRACE("qi_queue", display_delayed_instances_stats(tout); tout << "lazy threshold: " << m_params.m_qi_lazy_threshold + TRACE("qi_queue", display_delayed_instances_stats(tout); tout << "lazy threshold: " << m_params.m_qi_lazy_threshold << ", scope_level: " << m_context.get_scope_level() << "\n";); if (m_params.m_qi_conservative_final_check) { bool init = false; @@ -379,7 +379,7 @@ namespace smt { entry & e = m_delayed_entries[i]; TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); if (!e.m_instantiated && e.m_cost <= min_cost) { - TRACE("qi_queue", + TRACE("qi_queue", tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); result = false; m_instantiated_trail.push_back(i); @@ -389,13 +389,13 @@ namespace smt { } return result; } - + bool result = true; for (unsigned i = 0; i < m_delayed_entries.size(); i++) { entry & e = m_delayed_entries[i]; TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold) { - TRACE("qi_queue", + TRACE("qi_queue", tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";); result = false; m_instantiated_trail.push_back(i); @@ -443,7 +443,7 @@ namespace smt { quantifier * qa = *it2; delayed_qa_info info; qa2info.find(qa, info); - out << qa->get_qid() << ": " << info.m_num << " [" << info.m_min_cost << ", " << info.m_max_cost << "]\n"; + out << qa->get_qid() << ": " << info.m_num << " [" << info.m_min_cost << ", " << info.m_max_cost << "]\n"; } } @@ -482,6 +482,6 @@ namespace smt { } #endif } - + }; diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 10e2df988..1c8f94edf 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -135,7 +135,7 @@ namespace smt { m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO m_num_instances++; } - TRACE("quantifier", + TRACE("quantifier", tout << mk_pp(q, m()) << " "; for (unsigned i = 0; i < num_bindings; ++i) { tout << mk_pp(bindings[i]->get_owner(), m()) << " "; @@ -372,7 +372,7 @@ namespace smt { quantifier_manager_plugin * plugin = m_imp->m_plugin->mk_fresh(); m_imp->~imp(); m_imp = new (m_imp) imp(*this, ctx, p, plugin); - plugin->set_manager(*this); + plugin->set_manager(*this); } void quantifier_manager::display(std::ostream & out) const { diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index 6dcf20583..96af9909a 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -75,7 +75,7 @@ namespace smt { }; bool model_based() const; - bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier? + bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier? void adjust_model(proto_model * m); check_model_result check_model(proto_model * m, obj_map const & root2value); @@ -167,7 +167,7 @@ namespace smt { virtual void push() = 0; virtual void pop(unsigned num_scopes) = 0; - + }; };