mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

#5417

Browse source 
more gracefully handle non-implemented theories
This commit is contained in:
Nikolaj Bjorner 2021-07-19 13:50:20 -07:00
parent 0a34eef470
commit 4388ab2e3e
1 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/sat/smt/euf_model.cpp
View file

@ -178,6 +178,10 @@ namespace euf {
mbS->add_value(n, *mdl, m_values); mbS->add_value(n, *mdl, m_values);
else if (auto* mbE = expr2solver(e)) else if (auto* mbE = expr2solver(e))
mbE->add_value(n, *mdl, m_values); mbE->add_value(n, *mdl, m_values);
else if (is_app(e) && to_app(e)->get_family_id() != m.get_basic_family_id()) {
m_values.set(id, e);
IF_VERBOSE(1, verbose_stream() << "creating self-value for " << mk_pp(e, m) << "\n");
}
else { else {
IF_VERBOSE(1, verbose_stream() << "no model values created for " << mk_pp(e, m) << "\n"); IF_VERBOSE(1, verbose_stream() << "no model values created for " << mk_pp(e, m) << "\n");
} }
@ -212,9 +216,10 @@ namespace euf {
args.reset(); args.reset();
for (expr* arg : *a) { for (expr* arg : *a) {
enode* earg = get_enode(arg); enode* earg = get_enode(arg);
args.push_back(m_values.get(earg->get_root_id())); expr* val = m_values.get(earg->get_root_id());
CTRACE("euf", !args.back(), tout << "no value for " << bpp(earg) << "\n";); args.push_back(val);
SASSERT(args.back()); CTRACE("euf", !val, tout << "no value for " << bpp(earg) << "\n";);
SASSERT(val);
} }
SASSERT(args.size() == arity); SASSERT(args.size() == arity);
if (!fi->get_entry(args.data())) if (!fi->get_entry(args.data()))