Moved is_int_expr into arith_recognizers

src/ast/arith_decl_plugin.cpp

@@ -638,6 +638,35 @@ bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int
     return true;
 }
 
+#define IS_INT_EXPR_DEPTH_LIMIT 100
+bool arith_recognizers::is_int_expr(expr const *e) const {
+    if (is_int(e)) return true;
+    if (is_uninterp(e)) return false;
+    ptr_buffer<const expr> todo;
+    todo.push_back(e);
+    rational r;
+    unsigned i = 0;
+    while (!todo.empty()) {
+        ++i;
+        if (i > IS_INT_EXPR_DEPTH_LIMIT) {return false;}
+        e = todo.back();
+        todo.pop_back();
+        if (is_to_real(e)) {
+            // pass
+        }
+        else if (is_numeral(e, r) && r.is_int()) {
+            // pass
+        }
+        else if (is_add(e) || is_mul(e)) {
+            todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
+        }
+        else {
+            return false;
+        }
+    }
+    return true;
+}
+
 arith_util::arith_util(ast_manager & m):
     arith_recognizers(m.mk_family_id("arith")),
     m_manager(m),

src/ast/arith_decl_plugin.h

@@ -244,6 +244,8 @@ public:
         return false;
     }
 
+    bool is_int_expr(expr const * e) const;
+
     bool is_le(expr const * n) const { return is_app_of(n, m_afid, OP_LE); }
     bool is_ge(expr const * n) const { return is_app_of(n, m_afid, OP_GE); }
     bool is_lt(expr const * n) const { return is_app_of(n, m_afid, OP_LT); }
@@ -533,4 +535,3 @@ inline app_ref operator>(app_ref const& x, app_ref const& y) {
 }
 
 #endif /* ARITH_DECL_PLUGIN_H_ */
-

src/smt/theory_arith_core.h

@@ -69,33 +69,7 @@ namespace smt {
 #if 0
         return m_util.is_int(e);
 #else
-        if (m_util.is_int(e)) return true;
-        if (is_uninterp(e)) return false;
-        m_todo.reset();
-        m_todo.push_back(e);
-        rational r;
-        unsigned i = 0;
-        while (!m_todo.empty()) {
-            ++i;
-            if (i > 100) {
-                return false;
-            }
-            e = m_todo.back();
-            m_todo.pop_back();
-            if (m_util.is_to_real(e)) {
-                // pass
-            }
-            else if (m_util.is_numeral(e, r) && r.is_int()) {
-                // pass
-            }
-            else if (m_util.is_add(e) || m_util.is_mul(e)) {
-                m_todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
-            }
-            else {
-                return false;
-            }
-        }
-        return true;
+        return m_util.is_int_expr(e);
 #endif
     }
 
@@ -3542,4 +3516,3 @@ namespace smt {
 };
 
 #endif /* THEORY_ARITH_CORE_H_ */
-