From addbe558233349f32cc5419abb71d6b4c954e307 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Apr 2020 19:55:40 -0700 Subject: [PATCH] fix #3846, another bug in eq2bv-tactic Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/eq2bv_tactic.cpp | 18 ++++---- src/tactic/bv/bv_bounds_tactic.cpp | 74 ------------------------------ 2 files changed, 9 insertions(+), 83 deletions(-) diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp index d0dbbc90c..aafee26f0 100644 --- a/src/tactic/arith/eq2bv_tactic.cpp +++ b/src/tactic/arith/eq2bv_tactic.cpp @@ -152,7 +152,7 @@ public: obj_map m_fd; obj_map m_max; expr_mark m_nonfd; - ast_mark m_has_eq; + expr_mark m_has_eq; ptr_vector m_todo; eq2bv_tactic(ast_manager & _m): @@ -203,7 +203,7 @@ public: for (unsigned i = 0; !g->inconsistent() && i < g->size(); i++) { expr_ref new_curr(m); proof_ref new_pr(m); - expr_ref var(m); + app_ref var(m); if (is_bound(g->form(i), var) && !m_has_eq.is_marked(var)) { if (m.proofs_enabled()) { new_pr = m.mk_rewrite(g->form(i), m.mk_true()); @@ -312,42 +312,42 @@ public: } } - bool is_upper(expr* f, expr_ref& var) { + bool is_upper(expr* f, app_ref& var) { expr* e1, *e2; unsigned k; if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) && is_var_const_pair(e1, e2, k)) { SASSERT(m_bounds.has_upper(e1)); - var = e1; + var = to_app(e1); return true; } return false; } - bool is_lower(expr* f, expr_ref& var) { + bool is_lower(expr* f, app_ref& var) { expr* e1, *e2; unsigned k; if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) && is_var_const_pair(e2, e1, k)) { SASSERT(m_bounds.has_lower(e2)); - var = e2; + var = to_app(e2); return true; } return false; } - bool is_bound(expr* f, expr_ref& var) { + bool is_bound(expr* f, app_ref& var) { return is_lower(f, var) || is_upper(f, var); } void mark_has_eq(expr* e) { if (is_uninterp_const(e)) { - m_has_eq.mark(to_app(e)->get_decl(), true); + m_has_eq.mark(e, true); } } void collect_fd(expr* f) { m_trail.push_back(f); - expr_ref var(m); + app_ref var(m); if (is_bound(f, var)) return; m_todo.push_back(f); while (!m_todo.empty()) { diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 92454727d..5a9819b69 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -241,64 +241,6 @@ namespace { return false; } -#if 0 - expr_set* get_expr_vars(expr* t) { - unsigned id = t->get_id(); - m_expr_vars.reserve(id + 1); - expr_set*& entry = m_expr_vars[id]; - if (entry) - return entry; - - expr_set* set = alloc(expr_set); - entry = set; - - if (!m_bv.is_numeral(t)) - set->insert(t, true); - - if (!is_app(t)) - return set; - - app* a = to_app(t); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - expr_set* set_arg = get_expr_vars(a->get_arg(i)); - for (expr_set::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) { - set->insert(I->m_key, true); - } - } - return set; - } -#endif - -#if 0 - expr_cnt* get_expr_bounds(expr* t) { - unsigned id = t->get_id(); - m_bound_exprs.reserve(id + 1); - expr_cnt*& entry = m_bound_exprs[id]; - if (entry) - return entry; - - expr_cnt* set = alloc(expr_cnt); - entry = set; - - if (!is_app(t)) - return set; - - interval b; - expr* e; - if (is_bound(t, e, b)) { - set->insert_if_not_there2(e, 0)->get_data().m_value++; - } - - app* a = to_app(t); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - expr_cnt* set_arg = get_expr_bounds(a->get_arg(i)); - for (expr_cnt::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) { - set->insert_if_not_there2(I->m_key, 0)->get_data().m_value += I->m_value; - } - } - return set; - } -#endif public: bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) { @@ -475,15 +417,6 @@ namespace { if (contains(t, v.m_key)) return true; } -#if 0 - expr_set* used_exprs = get_expr_vars(t); - for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) { - if (contains(t, I->m_key)) return true; - if (I->m_value.is_singleton() && used_exprs->contains(I->m_key)) - return true; - } -#endif - expr* t1; interval b; // skip common case: single bound constraint without any context for simplification @@ -494,13 +427,6 @@ namespace { if (contains_bound(t)) { return true; } -#if 0 - expr_cnt* bounds = get_expr_bounds(t); - for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) { - if (I->m_value > 1 || m_bound.contains(I->m_key)) - return true; - } -#endif return false; }