mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

add missing lambda defs per #5509

Browse source 
the result is now unknown because the nested expression contains exists, which doesn't get replaced by universal quantifier which is assumed by the legacy core.
The legacy core should not depend on universal quantifiers only, but fixing this is a risk. Workaround is to rewrite goals using forall only (replace exists by de-Morgan dual).
This commit is contained in:
Nikolaj Bjorner 2021-08-27 11:57:26 -07:00
parent 9790a8aa43
commit 09696e989e
3 changed files with 22 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/model/model_core.cpp
View file

@ -125,3 +125,16 @@ void model_core::unregister_decl(func_decl * d) {
dealloc(v);
}
}
void model_core::add_lambda_defs() {
unsigned sz = get_num_decls();
for (unsigned i = sz; i-- > 0; ) {
func_decl* f = get_decl(i);
quantifier* q = m.is_lambda_def(f);
if (!q)
continue;
func_interp* fi = alloc(func_interp, m, f->get_arity());
fi->set_else(q);
register_decl(f, fi);
}
}

2
src/model/model_core.h
View file

@ -72,6 +72,8 @@ public:
void unregister_decl(func_decl * d);
func_interp* update_func_interp(func_decl* f, func_interp* fi);
void add_lambda_defs();
virtual expr * get_some_value(sort * s) = 0;
virtual expr * get_fresh_value(sort * s) = 0;
virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) = 0;

8
src/smt/smt_model_checker.cpp
View file

@ -423,8 +423,14 @@ namespace smt {
m_value2expr.reset();
TRACE("model_checker", tout << "MODEL_CHECKER INVOKED\n";
tout << "model:\n"; model_pp(tout, *m_curr_model););
tout << "model:\n"; model_pp(tout, *m_curr_model););
for (quantifier* q : *m_qm)
if (m.is_lambda_def(q)) {
md->add_lambda_defs();
break;
}
md->compress();
TRACE("model_checker", tout << "MODEL_CHECKER INVOKED\n";