mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

fix #2502

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-08-21 11:11:22 +08:00
parent e08abb3213
commit eea041383d
2 changed files with 19 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/cmd_context/cmd_context.cpp
View file

@ -1674,6 +1674,7 @@ void cmd_context::display_model(model_ref& mdl) {
if (mdl) { if (mdl) {
if (m_mc0) (*m_mc0)(mdl); if (m_mc0) (*m_mc0)(mdl);
if (m_params.m_model_compress) mdl->compress(); if (m_params.m_model_compress) mdl->compress();
add_declared_functions(*mdl);
model_params p; model_params p;
if (p.v1() || p.v2()) { if (p.v1() || p.v2()) {
std::ostringstream buffer; std::ostringstream buffer;
@ -1687,6 +1688,23 @@ void cmd_context::display_model(model_ref& mdl) {
} }
} }
void cmd_context::add_declared_functions(model& mdl) {
for (auto const& kv : m_func_decls) {
func_decl* f = kv.m_value.first();
if (!mdl.has_interpretation(f)) {
expr* val = mdl.get_some_value(f->get_range());
if (f->get_arity() == 0) {
mdl.register_decl(f, val);
}
else {
func_interp* fi = alloc(func_interp, m(), f->get_arity());
fi->set_else(val);
mdl.register_decl(f, fi);
}
}
}
}
void cmd_context::display_sat_result(lbool r) { void cmd_context::display_sat_result(lbool r) {
switch (r) { switch (r) {
case l_true: case l_true:

1
src/cmd_context/cmd_context.h
View file

@ -273,6 +273,7 @@ protected:
void init_external_manager(); void init_external_manager();
void reset_cmds(); void reset_cmds();
void finalize_cmds(); void finalize_cmds();
void add_declared_functions(model& mdl);
void restore_func_decls(unsigned old_sz); void restore_func_decls(unsigned old_sz);
void restore_psort_decls(unsigned old_sz); void restore_psort_decls(unsigned old_sz);