mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

fix #3786

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-06 13:03:41 -07:00
parent 07413cc928
commit 5acf4b5968
1 changed files with 24 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

50
src/muz/transforms/dl_mk_scale.cpp
View file

@ -45,34 +45,32 @@ namespace datalog {
for (auto const& kv : m_new2old) { for (auto const& kv : m_new2old) {
func_decl* old_p = kv.m_value; func_decl* old_p = kv.m_value;
func_decl* new_p = kv.m_key; func_decl* new_p = kv.m_key;
func_interp* old_fi = alloc(func_interp, m, old_p->get_arity()); func_interp* new_fi = md->get_func_interp(new_p);
expr_ref_vector subst(m);
var_subst vs(m, false);
expr_ref tmp(m);
if (new_p->get_arity() == 0) { if (!new_fi) {
old_fi->set_else(md->get_const_interp(new_p)); TRACE("dl", tout << new_p->get_name() << " has no value in the current model\n";);
} continue;
else { }
func_interp* new_fi = md->get_func_interp(new_p); for (unsigned i = 0; i < old_p->get_arity(); ++i) {
expr_ref_vector subst(m); subst.push_back(m.mk_var(i, old_p->get_domain(i)));
var_subst vs(m, false); }
expr_ref tmp(m); subst.push_back(a.mk_numeral(rational(1), a.mk_real()));
if (!new_fi) { SASSERT(!new_fi->is_partial() && new_fi->num_entries() == 0);
TRACE("dl", tout << new_p->get_name() << " has no value in the current model\n";); tmp = vs(new_fi->get_else(), subst.size(), subst.c_ptr());
dealloc(old_fi); if (old_p->get_arity() == 0) {
continue; old_model->register_decl(old_p, tmp);
} }
for (unsigned i = 0; i < old_p->get_arity(); ++i) { else {
subst.push_back(m.mk_var(i, old_p->get_domain(i))); func_interp* old_fi = alloc(func_interp, m, old_p->get_arity());
} // Hedge that we don't have to handle the general case for models produced
subst.push_back(a.mk_numeral(rational(1), a.mk_real())); // by Horn clause solvers.
old_fi->set_else(tmp);
// Hedge that we don't have to handle the general case for models produced old_model->register_decl(old_p, old_fi);
// by Horn clause solvers. }
SASSERT(!new_fi->is_partial() && new_fi->num_entries() == 0);
tmp = vs(new_fi->get_else(), subst.size(), subst.c_ptr());
old_fi->set_else(tmp);
old_model->register_decl(old_p, old_fi);
}
} }
// register values that have not been scaled. // register values that have not been scaled.