From bd0bd08ecf15c97a37cd17d021513a83255a37ff Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 8 Apr 2016 16:58:11 +0100 Subject: [PATCH] add is_considered_uninterpreted checks into acker_helper --- src/ackermannization/ackr_helper.h | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) diff --git a/src/ackermannization/ackr_helper.h b/src/ackermannization/ackr_helper.h index 5c572907e..70d6ab57b 100644 --- a/src/ackermannization/ackr_helper.h +++ b/src/ackermannization/ackr_helper.h @@ -33,19 +33,8 @@ class ackr_helper { which are not marked as uninterpreted but effectively are. */ inline bool should_ackermannize(app const * a) const { - if (a->get_family_id() == m_bvutil.get_family_id()) { - switch (a->get_decl_kind()) { - case OP_BSDIV0: - case OP_BUDIV0: - case OP_BSREM0: - case OP_BUREM0: - case OP_BSMOD0: - return true; - default: - return is_uninterp(a); - } - } - return (is_uninterp(a)); + decl_plugin * p = m_bvutil.get_manager().get_plugin(a->get_family_id()); + return p->is_considered_uninterpreted(a->get_decl()); } inline bv_util& bvutil() { return m_bvutil; }