mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

add is_considered_uninterpreted checks into acker_helper

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-04-08 16:58:11 +01:00
parent 0597b579b1
commit bd0bd08ecf
1 changed files with 2 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/ackermannization/ackr_helper.h
View file

@ -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; }