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

update func_interp code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-04-18 17:30:52 -07:00
parent cff843ca59
commit 3a6218ac21
1 changed files with 4 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/model/func_interp.cpp
View file

@ -107,25 +107,23 @@ void func_interp::reset_interp_cache() {
bool func_interp::is_fi_entry_expr(expr * e, ptr_vector<expr> & args) { bool func_interp::is_fi_entry_expr(expr * e, ptr_vector<expr> & args) {
args.reset(); args.reset();
expr* c, *t, *f; expr* c, *t, *f, *a0, *a1;
if (!m().is_ite(e, c, t, f)) { if (!m().is_ite(e, c, t, f)) {
return false; return false;
} }
if ((m_arity == 0) || if ((m_arity == 0) ||
(m_arity == 1 && (!m().is_eq(c) || to_app(c)->get_num_args() != 2)) || (m_arity == 1 && !m().is_eq(c, a1, a2)) ||
(m_arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != m_arity))) (m_arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != m_arity)))
return false; return false;
args.resize(m_arity, 0); args.resize(m_arity, 0);
for (unsigned i = 0; i < m_arity; i++) { for (unsigned i = 0; i < m_arity; i++) {
expr * ci = (m_arity == 1 && i == 0) ? to_app(c) : to_app(c)->get_arg(i); expr * ci = (m_arity == 1 && i == 0) ? c : to_app(c)->get_arg(i);
if (!m().is_eq(ci) || to_app(ci)->get_num_args() != 2) if (!m().is_eq(ci, a0, a1))
return false; return false;
expr * a0 = to_app(ci)->get_arg(0);
expr * a1 = to_app(ci)->get_arg(1);
if (is_var(a0) && to_var(a0)->get_idx() == i) if (is_var(a0) && to_var(a0)->get_idx() == i)
args[i] = a1; args[i] = a1;
else if (is_var(a1) && to_var(a1)->get_idx() == i) else if (is_var(a1) && to_var(a1)->get_idx() == i)