mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix mbqi value caching issue raised by Clemens and Martin
This commit is contained in:
parent
d5fde2e578
commit
dde5218b29
|
@ -82,22 +82,18 @@ namespace smt {
|
|||
app* fresh_term;
|
||||
if (is_app(val) && to_app(val)->get_num_args() > 0) {
|
||||
ptr_buffer<expr> args;
|
||||
for (expr* arg : *to_app(val)) {
|
||||
for (expr* arg : *to_app(val))
|
||||
args.push_back(get_type_compatible_term(arg));
|
||||
}
|
||||
fresh_term = m.mk_app(to_app(val)->get_decl(), args.size(), args.data());
|
||||
}
|
||||
else {
|
||||
expr * sk_term = get_term_from_ctx(val);
|
||||
if (sk_term != nullptr) {
|
||||
if (sk_term != nullptr)
|
||||
return sk_term;
|
||||
}
|
||||
|
||||
for (expr* f : m_fresh_exprs) {
|
||||
if (f->get_sort() == val->get_sort()) {
|
||||
for (expr* f : m_fresh_exprs)
|
||||
if (f->get_sort() == val->get_sort())
|
||||
return f;
|
||||
}
|
||||
}
|
||||
fresh_term = m.mk_fresh_const("sk", val->get_sort());
|
||||
}
|
||||
m_fresh_exprs.push_back(fresh_term);
|
||||
|
@ -106,13 +102,16 @@ namespace smt {
|
|||
}
|
||||
|
||||
void model_checker::init_value2expr() {
|
||||
|
||||
if (m_value2expr.empty()) {
|
||||
// populate m_value2expr
|
||||
for (auto const& kv : *m_root2value) {
|
||||
enode * n = kv.m_key;
|
||||
expr * val = kv.m_value;
|
||||
n = n->get_eq_enode_with_min_gen();
|
||||
m_value2expr.insert(val, n->get_expr());
|
||||
expr* e = n->get_expr();
|
||||
if (!m.is_value(e))
|
||||
m_value2expr.insert(val, e);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
@ -330,27 +330,32 @@ namespace smt {
|
|||
enode * n = curr.get_enode();
|
||||
SASSERT(n->get_root() == n);
|
||||
TRACE("mg_top_sort", tout << curr << "\n";);
|
||||
dependencies.reset();
|
||||
dependency_values.reset();
|
||||
model_value_proc * proc = root2proc[n];
|
||||
SASSERT(proc);
|
||||
proc->get_dependencies(dependencies);
|
||||
for (model_value_dependency const& d : dependencies) {
|
||||
if (d.is_fresh_value()) {
|
||||
CTRACE("mg_top_sort", !d.get_value()->get_value(),
|
||||
tout << "#" << n->get_owner_id() << " " << mk_pp(n->get_expr(), m) << " -> " << d << "\n";);
|
||||
SASSERT(d.get_value()->get_value());
|
||||
dependency_values.push_back(d.get_value()->get_value());
|
||||
}
|
||||
else {
|
||||
enode * child = d.get_enode();
|
||||
TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_expr(), m) << "): "
|
||||
<< mk_pp(child->get_expr(), m) << " " << mk_pp(child->get_root()->get_expr(), m) << "\n";);
|
||||
child = child->get_root();
|
||||
dependency_values.push_back(m_root2value[child]);
|
||||
app* val = nullptr;
|
||||
if (m.is_value(n->get_expr()))
|
||||
val = to_app(n->get_expr());
|
||||
else {
|
||||
dependencies.reset();
|
||||
dependency_values.reset();
|
||||
model_value_proc * proc = root2proc[n];
|
||||
SASSERT(proc);
|
||||
proc->get_dependencies(dependencies);
|
||||
for (model_value_dependency const& d : dependencies) {
|
||||
if (d.is_fresh_value()) {
|
||||
CTRACE("mg_top_sort", !d.get_value()->get_value(),
|
||||
tout << "#" << n->get_owner_id() << " " << mk_pp(n->get_expr(), m) << " -> " << d << "\n";);
|
||||
SASSERT(d.get_value()->get_value());
|
||||
dependency_values.push_back(d.get_value()->get_value());
|
||||
}
|
||||
else {
|
||||
enode * child = d.get_enode();
|
||||
TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_expr(), m) << "): "
|
||||
<< mk_pp(child->get_expr(), m) << " " << mk_pp(child->get_root()->get_expr(), m) << "\n";);
|
||||
child = child->get_root();
|
||||
dependency_values.push_back(m_root2value[child]);
|
||||
}
|
||||
}
|
||||
val = proc->mk_value(*this, dependency_values);
|
||||
}
|
||||
app * val = proc->mk_value(*this, dependency_values);
|
||||
register_value(val);
|
||||
m_asts.push_back(val);
|
||||
m_root2value.insert(n, val);
|
||||
|
|
Loading…
Reference in a new issue