mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

mbc: moved code under get_subst()

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-04 16:11:27 -07:00
parent e860e4d045
commit 478d7c790e
1 changed files with 19 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

45
src/muz/spacer/spacer_mbc.cpp
View file

@ -30,45 +30,38 @@ public:
m_parts(parts), m_current_part(UINT_MAX)
{m_mev.set_model_completion(true);}
br_status reduce_app(func_decl *f, unsigned num, expr * const * args,
expr_ref &result, proof_ref & result_pr) {
bool get_subst(expr *s, expr * & t, proof * & t_pr) {
if (!is_app(s)) return false;
unsigned part = UINT_MAX;
// not a constant
if (num != 0) return BR_FAILED;
// not in partition map
if (!m_pmap.find(f, part)) return BR_FAILED;
if (!m_pmap.find (to_app(s)->get_decl(), part)) return false;
// first part element, remember it
if (!found_partition()) {
set_partition(part);
return BR_FAILED;
return false;
}
// already in our substitution map
expr *tmp = nullptr;
if (m_subs.find(s, tmp)) {
t = tmp;
return true;
}
// decide value based on model
expr_ref e(m), val(m);
e = m.mk_app(f, num, args);
// already in our substitution map
expr *t = nullptr;
if (m_subs.find(e, t)) {
result = t;
return BR_DONE;
}
expr_ref val(m);
// eval in the model
m_mev.eval(e, val, true);
m_mev.eval(s, val, true);
// store decided equality
m_parts[part].push_back(m.mk_eq(e, val));
// store decided equality (also keeps ref to s and val
m_parts[part].push_back(m.mk_eq(s, val));
// store substitution
m_subs.insert(e, val);
result = val;
return BR_DONE;
}
bool get_subst(expr * s, expr * & t, proof * & t_pr) {
return m_subs.find(s, t);
m_subs.insert(s, val);
t = val;
return true;
}
void reset_partition() {m_current_part = UINT_MAX;}