mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

fix #1681

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-18 21:53:45 -07:00
parent b4aac1ab55
commit 86c39c971d
4 changed files with 15 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/smt/proto_model/proto_model.cpp
View file

@ -342,10 +342,16 @@ void proto_model::compress() {
\brief Complete the interpretation fi of f if it is partial.
If f does not have an interpretation in the given model, then this is a noop.
*/
void proto_model::complete_partial_func(func_decl * f) {
void proto_model::complete_partial_func(func_decl * f, bool use_fresh) {
func_interp * fi = get_func_interp(f);
if (fi && fi->is_partial()) {
expr * else_value = fi->get_max_occ_result();
expr * else_value;
if (use_fresh) {
else_value = get_fresh_value(f->get_range());
}
else {
else_value = fi->get_max_occ_result();
}
if (else_value == nullptr)
else_value = get_some_value(f->get_range());
fi->set_else(else_value);
@ -355,14 +361,14 @@ void proto_model::complete_partial_func(func_decl * f) {
/**
\brief Set the (else) field of function interpretations...
*/
void proto_model::complete_partial_funcs() {
void proto_model::complete_partial_funcs(bool use_fresh) {
if (m_model_partial)
return;
// m_func_decls may be "expanded" when we invoke get_some_value.
// So, we must not use iterators to traverse it.
for (unsigned i = 0; i < m_func_decls.size(); i++) {
complete_partial_func(m_func_decls[i]);
for (func_decl* f : m_func_decls) {
complete_partial_func(f, use_fresh);
}
}

4
src/smt/proto_model/proto_model.h
View file

@ -100,8 +100,8 @@ public:
//
// Complete partial function interps
//
void complete_partial_func(func_decl * f);
void complete_partial_funcs();
void complete_partial_func(func_decl * f, bool use_fresh);
void complete_partial_funcs(bool use_fresh);
//
// Create final model object.

2
src/smt/smt_context.cpp
View file

@ -4364,7 +4364,7 @@ namespace smt {
m_proto_model = m_model_generator->mk_model();
m_qmanager->adjust_model(m_proto_model.get());
TRACE("mbqi_bug", tout << "before complete_partial_funcs:\n"; model_pp(tout, *m_proto_model););
m_proto_model->complete_partial_funcs();
m_proto_model->complete_partial_funcs(false);
TRACE("mbqi_bug", tout << "before cleanup:\n"; model_pp(tout, *m_proto_model););
m_proto_model->cleanup();
if (m_fparams.m_model_compact)

2
src/smt/smt_model_finder.cpp
View file

@ -1028,7 +1028,7 @@ namespace smt {
void complete_partial_funcs(func_decl_set const & partial_funcs) {
for (func_decl * f : partial_funcs) {
// Complete the current interpretation
m_model->complete_partial_func(f);
m_model->complete_partial_func(f, true);
unsigned arity = f->get_arity();
func_interp * fi = m_model->get_func_interp(f);