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

Fixed inconsistent state upon solver interruption. Partially fixes #951.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-07-21 17:42:48 +01:00
parent 943dc8118a
commit faa19117e4
4 changed files with 38 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/smt/cached_var_subst.cpp
View file

@ -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);
}

36
src/smt/qi_queue.cpp
View file

@ -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<float>(stat->get_size());
m_vals[DEPTH] = static_cast<float>(stat->get_depth());
m_vals[GENERATION] = static_cast<float>(generation);
m_vals[QUANT_GENERATION] = static_cast<float>(stat->get_generation());
m_vals[QUANT_GENERATION] = static_cast<float>(stat->get_generation());
m_vals[WEIGHT] = static_cast<float>(q->get_weight());
m_vals[VARS] = static_cast<float>(q->get_num_decls());
m_vals[PATTERN_WIDTH] = pat ? static_cast<float>(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<unsigned>(r);
}
void qi_queue::insert(fingerprint * f, app * pat, unsigned generation, unsigned min_top_generation, unsigned max_top_generation) {
quantifier * q = static_cast<quantifier*>(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<quantifier*>(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<quantifier*>(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<quantifier*>(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
}
};

4
src/smt/smt_quantifier.cpp
View file

@ -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 {

4
src/smt/smt_quantifier.h
View file

@ -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<enode, app *> const & root2value);
@ -167,7 +167,7 @@ namespace smt {
virtual void push() = 0;
virtual void pop(unsigned num_scopes) = 0;
};
};