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

#7027

Browse source 
fix lossy function declaration inclusion functionality exposed when fixing a bug for incomplete model generation.
This commit is contained in:
Nikolaj Bjorner 2023-12-03 11:14:18 -08:00
parent a8f3396b24
commit 9cc2ce42f7
2 changed files with 9 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/sat/smt/dt_solver.cpp
View file

@ -554,12 +554,12 @@ namespace dt {
} }
// Assuming `app` is equal to a constructor term, return the constructor enode // Assuming `app` is equal to a constructor term, return the constructor enode
inline euf::enode* solver::oc_get_cstor(enode* app) { inline euf::enode* solver::oc_get_cstor(enode* app) const {
theory_var v = app->get_root()->get_th_var(get_id()); theory_var v = app->get_root()->get_th_var(get_id());
SASSERT(v != euf::null_theory_var); if (v == euf::null_theory_var)
return nullptr;
v = m_find.find(v); v = m_find.find(v);
var_data* d = m_var_data[v]; var_data* d = m_var_data[v];
SASSERT(d->m_constructor);
return d->m_constructor; return d->m_constructor;
} }
@ -783,7 +783,7 @@ namespace dt {
if (v == euf::null_theory_var) if (v == euf::null_theory_var)
return false; return false;
euf::enode* con = m_var_data[m_find.find(v)]->m_constructor; euf::enode* con = m_var_data[m_find.find(v)]->m_constructor;
CTRACE("dt", !con, display(tout) << ctx.bpp(n) << "\n";); TRACE("dt", display(tout) << ctx.bpp(n) << " con: " << ctx.bpp(con) << "\n";);
if (con->num_args() == 0) if (con->num_args() == 0)
dep.insert(n, nullptr); dep.insert(n, nullptr);
for (enode* arg : euf::enode_args(con)) for (enode* arg : euf::enode_args(con))
@ -794,16 +794,15 @@ namespace dt {
bool solver::include_func_interp(func_decl* f) const { bool solver::include_func_interp(func_decl* f) const {
if (!dt.is_accessor(f)) if (!dt.is_accessor(f))
return false; return false;
func_decl* con = dt.get_accessor_constructor(f); func_decl* con_decl = dt.get_accessor_constructor(f);
for (enode* app : ctx.get_egraph().enodes_of(f)) { for (enode* app : ctx.get_egraph().enodes_of(f)) {
enode* arg = app->get_arg(0)->get_root(); enode* con = oc_get_cstor(app->get_arg(0));
if (is_constructor(arg) && arg->get_decl() != con) if (con && is_constructor(con) && con->get_decl() != con_decl)
return true; return true;
} }
return false; return false;
} }
sat::literal solver::internalize(expr* e, bool sign, bool root) { sat::literal solver::internalize(expr* e, bool sign, bool root) {
if (!visit_rec(m, e, sign, root)) if (!visit_rec(m, e, sign, root))
return sat::null_literal; return sat::null_literal;

2
src/sat/smt/dt_solver.h
View file

@ -116,7 +116,7 @@ namespace dt {
void pop_core(unsigned n) override; void pop_core(unsigned n) override;
enode * oc_get_cstor(enode * n); enode * oc_get_cstor(enode * n) const;
bool occurs_check(enode * n); bool occurs_check(enode * n);
bool occurs_check_enter(enode * n); bool occurs_check_enter(enode * n);
void occurs_check_explain(enode * top, enode * root); void occurs_check_explain(enode * top, enode * root);