mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #7102

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-01-27 17:05:48 -08:00
parent 2af1cff11f
commit f8a3b6f521
1 changed files with 20 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/model/model_evaluator.cpp
View file

@ -20,6 +20,7 @@ Revision History:
#include "ast/ast_util.h" #include "ast/ast_util.h"
#include "ast/for_each_expr.h" #include "ast/for_each_expr.h"
#include "ast/recfun_decl_plugin.h" #include "ast/recfun_decl_plugin.h"
#include "ast/polymorphism_util.h"
#include "ast/rewriter/rewriter_types.h" #include "ast/rewriter/rewriter_types.h"
#include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/bool_rewriter.h"
#include "ast/rewriter/arith_rewriter.h" #include "ast/rewriter/arith_rewriter.h"
@ -371,7 +372,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
bool get_macro(func_decl * f, expr * & def, quantifier * & , proof * &) { bool get_macro(func_decl * f, expr * & def, quantifier * & , proof * &) {
func_interp * fi = m_model.get_func_interp(f); func_interp * fi = m_model.get_func_interp(f);
def = nullptr; def = nullptr;
if (fi != nullptr) { if (fi) {
if (fi->is_partial()) { if (fi->is_partial()) {
if (m_model_completion) { if (m_model_completion) {
sort * s = f->get_range(); sort * s = f->get_range();
@ -384,6 +385,24 @@ struct evaluator_cfg : public default_rewriter_cfg {
def = fi->get_interp(); def = fi->get_interp();
SASSERT(def != nullptr); SASSERT(def != nullptr);
} }
else if (f->is_polymorphic() && (fi = m_model.get_func_interp(m.poly_root(f)))) {
if (fi->is_partial()) {
if (m_model_completion) {
sort * s = f->get_range();
expr * val = m_model.get_some_value(s);
fi->set_else(val);
}
else
return false;
}
def = fi->get_interp();
polymorphism::substitution subst(m);
polymorphism::util util(m);
util.unify(f, m.poly_root(f), subst);
def = subst(def);
SASSERT(def != nullptr);
}
else if (m_model_completion && else if (m_model_completion &&
(f->get_family_id() == null_family_id || (f->get_family_id() == null_family_id ||
m.get_plugin(f->get_family_id())->is_considered_uninterpreted(f))) { m.get_plugin(f->get_family_id())->is_considered_uninterpreted(f))) {