Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk allows linearization of div,mod,/ by a constant.

9 files changed, 325 insertions, 27 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index aa5049ed4..247c09294 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -29,7 +29,8 @@ namespace theory {
 namespace arith {
 
 bool ArithRewriter::isAtom(TNode n) {
-  return arith::isRelationOperator(n.getKind());
+  Kind k = n.getKind();
+  return arith::isRelationOperator(k) || k == kind::IS_INTEGER || k == kind::DIVISIBLE;
 }
 
 RewriteResponse ArithRewriter::rewriteConstant(TNode t){
@@ -98,11 +99,28 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
       return preRewritePlus(t);
     case kind::MULT:
       return preRewriteMult(t);
-    //case kind::INTS_DIVISION:
-    //case kind::INTS_MODULUS:
+    case kind::INTS_DIVISION:
+    case kind::INTS_MODULUS:
+      return RewriteResponse(REWRITE_DONE, t);
     case kind::INTS_DIVISION_TOTAL:
     case kind::INTS_MODULUS_TOTAL:
       return rewriteIntsDivModTotal(t,true);
+    case kind::ABS:
+      if(t[0].isConst()) {
+        const Rational& rat = t[0].getConst<Rational>();
+        if(rat >= 0) {
+          return RewriteResponse(REWRITE_DONE, t[0]);
+        } else {
+          return RewriteResponse(REWRITE_DONE,
+                                 NodeManager::currentNM()->mkConst(-rat));
+        }
+      }
+      return RewriteResponse(REWRITE_DONE, t);
+    case kind::IS_INTEGER:
+    case kind::TO_INTEGER:
+      return RewriteResponse(REWRITE_DONE, t);
+    case kind::TO_REAL:
+      return RewriteResponse(REWRITE_DONE, t[0]);
     default:
       Unhandled(k);
     }
@@ -126,11 +144,44 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
       return postRewritePlus(t);
     case kind::MULT:
       return postRewriteMult(t);
-      //case kind::INTS_DIVISION:
-      //case kind::INTS_MODULUS:
+    case kind::INTS_DIVISION:
+    case kind::INTS_MODULUS:
+      return RewriteResponse(REWRITE_DONE, t);
     case kind::INTS_DIVISION_TOTAL:
     case kind::INTS_MODULUS_TOTAL:
       return rewriteIntsDivModTotal(t, false);
+    case kind::ABS:
+      if(t[0].isConst()) {
+        const Rational& rat = t[0].getConst<Rational>();
+        if(rat >= 0) {
+          return RewriteResponse(REWRITE_DONE, t[0]);
+        } else {
+          return RewriteResponse(REWRITE_DONE,
+                                 NodeManager::currentNM()->mkConst(-rat));
+        }
+      }
+    case kind::TO_REAL:
+      return RewriteResponse(REWRITE_DONE, t[0]);
+    case kind::TO_INTEGER:
+      if(t[0].isConst()) {
+        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(Rational(t[0].getConst<Rational>().floor())));
+      }
+      if(t[0].getType().isInteger()) {
+        return RewriteResponse(REWRITE_DONE, t[0]);
+      }
+      //Unimplemented("TO_INTEGER, nonconstant");
+      //return rewriteToInteger(t);
+      return RewriteResponse(REWRITE_DONE, t);
+    case kind::IS_INTEGER:
+      if(t[0].isConst()) {
+        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(t[0].getConst<Rational>().getDenominator() == 1));
+      }
+      if(t[0].getType().isInteger()) {
+        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
+      }
+      //Unimplemented("IS_INTEGER, nonconstant");
+      //return rewriteIsInteger(t);
+      return RewriteResponse(REWRITE_DONE, t);
     default:
       Unreachable();
     }
@@ -190,6 +241,25 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){
 }
 
 RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){
+  if(atom.getKind() == kind::IS_INTEGER) {
+    if(atom[0].isConst()) {
+      return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(atom[0].getConst<Rational>().isIntegral()));
+    }
+    if(atom[0].getType().isInteger()) {
+      return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
+    }
+    // not supported, but this isn't the right place to complain
+    return RewriteResponse(REWRITE_DONE, atom);
+  } else if(atom.getKind() == kind::DIVISIBLE) {
+    if(atom[0].isConst()) {
+      return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(bool((atom[0].getConst<Rational>() / atom.getOperator().getConst<Divisible>().k).isIntegral())));
+    }
+    if(atom.getOperator().getConst<Divisible>().k.isOne()) {
+      return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
+    }
+    return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkNode(kind::EQUAL, NodeManager::currentNM()->mkNode(kind::INTS_MODULUS_TOTAL, atom[0], NodeManager::currentNM()->mkConst(Rational(atom.getOperator().getConst<Divisible>().k))), NodeManager::currentNM()->mkConst(Rational(0))));
+  }
+
   // left |><| right
   TNode left = atom[0];
   TNode right = atom[1];
@@ -217,6 +287,14 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){
   }else if(atom.getKind() == kind::LT){
     Node geq = currNM->mkNode(kind::GEQ, atom[0], atom[1]);
     return RewriteResponse(REWRITE_DONE, currNM->mkNode(kind::NOT, geq));
+  }else if(atom.getKind() == kind::IS_INTEGER){
+    if(atom[0].getType().isInteger()){
+      return RewriteResponse(REWRITE_DONE, currNM->mkConst(true));
+    }
+  }else if(atom.getKind() == kind::DIVISIBLE){
+    if(atom.getOperator().getConst<Divisible>().k.isOne()){
+      return RewriteResponse(REWRITE_DONE, currNM->mkConst(true));
+    }
   }
 
   return RewriteResponse(REWRITE_DONE, atom);
@@ -329,6 +407,13 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){
       Assert(k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL);
       return RewriteResponse(REWRITE_AGAIN, n);
     }
+  }else if(dIsConstant && d.getConst<Rational>().isNegativeOne()){
+    if(k == kind::INTS_MODULUS || k == kind::INTS_MODULUS_TOTAL){
+      return RewriteResponse(REWRITE_DONE, mkRationalNode(0));
+    }else{
+      Assert(k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL);
+      return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkNode(kind::UMINUS, n));
+    }
   }else if(dIsConstant && n.getKind() == kind::CONST_RATIONAL){
     Assert(d.getConst<Rational>().isIntegral());
     Assert(n.getConst<Rational>().isIntegral());
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 07cfcc9e5..a8a4047ca 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -23,8 +23,16 @@ operator INTS_DIVISION 2 "ints division (user symbol)"
 operator INTS_DIVISION_TOTAL 2 "ints division with interpreted division by 0 (internal symbol)"
 operator INTS_MODULUS 2 "ints modulus (user symbol)"
 operator INTS_MODULUS_TOTAL 2 "ints modulus with interpreted division by 0 (internal symbol)"
+operator ABS 1 "absolute value"
+parameterized DIVISIBLE DIVISIBLE_OP 1 "divisibility-by-k predicate"
 operator POW 2 "arithmetic power"
 
+constant DIVISIBLE_OP \
+        ::CVC4::Divisible \
+        ::CVC4::DivisibleHashFunction \
+        "util/divisible.h" \
+        "operator for the divisibility-by-k predicate"
+
 sort REAL_TYPE \
     Cardinality::REALS \
     well-founded \
@@ -72,6 +80,10 @@ operator LEQ 2 "less than or equal, x <= y"
 operator GT 2 "greater than, x > y"
 operator GEQ 2 "greater than or equal, x >= y"
 
+operator IS_INTEGER 1 "term is integer"
+operator TO_INTEGER 1 "cast term to integer"
+operator TO_REAL 1 "cast term to real"
+
 typerule PLUS ::CVC4::theory::arith::ArithOperatorTypeRule
 typerule MULT ::CVC4::theory::arith::ArithOperatorTypeRule
 typerule MINUS ::CVC4::theory::arith::ArithOperatorTypeRule
@@ -86,11 +98,17 @@ typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule
 typerule GT ::CVC4::theory::arith::ArithPredicateTypeRule
 typerule GEQ ::CVC4::theory::arith::ArithPredicateTypeRule
 
-typerule INTS_DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule INTS_MODULUS ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule IS_INTEGER ::CVC4::theory::arith::ArithUnaryPredicateTypeRule
+
+typerule ABS ::CVC4::theory::arith::IntOperatorTypeRule
+typerule INTS_DIVISION ::CVC4::theory::arith::IntOperatorTypeRule
+typerule INTS_MODULUS ::CVC4::theory::arith::IntOperatorTypeRule
+typerule DIVISIBLE ::CVC4::theory::arith::IntUnaryPredicateTypeRule
 
 typerule DIVISION_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule INTS_DIVISION_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule INTS_MODULUS_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule
+typerule INTS_DIVISION_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule
+typerule INTS_MODULUS_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule
 
 endtheory
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index c6af7010f..1dddb5a5b 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -241,6 +241,11 @@ public:
     case kind::INTS_MODULUS_TOTAL:
     case kind::DIVISION_TOTAL:
       return isDivMember(n);
+    case kind::ABS:
+    case kind::TO_INTEGER:
+      // Treat to_int as a variable; it is replaced in early preprocessing
+      // by a variable.
+      return true;
     default:
       return (!isRelationOperator(k)) &&
         (Theory::isLeafOf(n, theory::THEORY_ARITH));
diff --git a/src/theory/arith/options b/src/theory/arith/options
index 7d92f5351..57ef3d1b9 100644
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@ -100,5 +100,7 @@ option arithPropAsLemmaLength --arith-prop-clauses uint16_t :default 8 :read-wri
 option soiQuickExplain --soi-qe bool :default false :read-write
  Use quick explain to minimize the sum of infeasibility conflicts.
 
+option rewriteDivk rewrite-divk --rewrite-divk bool :default false
+ rewrite division and mod when by a constant into linear terms
 
 endmodule
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index c0442da90..120ac0154 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -47,6 +47,7 @@ void TheoryArith::addSharedTerm(TNode n){
 }
 
 Node TheoryArith::ppRewrite(TNode atom) {
+  CodeTimer timer(d_ppRewriteTimer);
   return d_internal->ppRewrite(atom);
 }
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 10c79b293..6b9fd5515 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -42,6 +42,7 @@ private:
 
   TheoryArithPrivate* d_internal;
 
+  KEEP_STATISTIC(TimerStat, d_ppRewriteTimer, "theory::arith::ppRewriteTimer");
 
 public:
   TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index dd5e404c6..a01397973 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -737,19 +737,142 @@ void TheoryArithPrivate::addSharedTerm(TNode n){
   }
 }
 
+namespace attr {
+  struct ToIntegerTag { };
+  struct LinearIntDivTag { };
+}/* CVC4::theory::arith::attr namespace */
+
+/**
+ * This attribute maps the child of a to_int / is_int to the
+ * corresponding integer skolem.
+ */
+typedef expr::Attribute<attr::ToIntegerTag, Node> ToIntegerAttr;
+
+/**
+ * This attribute maps division-by-constant-k terms to a variable
+ * used to eliminate them.
+ */
+typedef expr::Attribute<attr::LinearIntDivTag, Node> LinearIntDivAttr;
+
+Node TheoryArithPrivate::ppRewriteTerms(TNode n) {
+  if(Theory::theoryOf(n) != THEORY_ARITH) {
+    return n;
+  }
+
+  NodeManager* nm = NodeManager::currentNM();
+
+  switch(Kind k = n.getKind()) {
+
+  case kind::TO_INTEGER:
+  case kind::IS_INTEGER: {
+    Node intVar;
+    if(!n[0].getAttribute(ToIntegerAttr(), intVar)) {
+      intVar = nm->mkSkolem("toInt", nm->integerType(), "a conversion of a Real term to its Integer part");
+      n[0].setAttribute(ToIntegerAttr(), intVar);
+      d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LT, nm->mkNode(kind::MINUS, n[0], nm->mkConst(Rational(1))), intVar), nm->mkNode(kind::LEQ, intVar, n[0])));
+    }
+    if(n.getKind() == kind::TO_INTEGER) {
+      Node node = intVar;
+      return node;
+    } else {
+      Node node = nm->mkNode(kind::EQUAL, node[0], intVar);
+      return node;
+    }
+    Unreachable();
+  }
+
+  case kind::INTS_DIVISION:
+  case kind::INTS_DIVISION_TOTAL: {
+    if(!options::rewriteDivk()) {
+      return n;
+    }
+    Node num = Rewriter::rewrite(n[0]);
+    Node den = Rewriter::rewrite(n[1]);
+    if(den.isConst()) {
+      const Rational& rat = den.getConst<Rational>();
+      Assert(!num.isConst());
+      if(rat != 0) {
+        Node intVar;
+        Node rw = nm->mkNode(k, num, den);
+        if(!rw.getAttribute(LinearIntDivAttr(), intVar)) {
+          intVar = nm->mkSkolem("linearIntDiv", nm->integerType(), "the result of an intdiv-by-k term");
+          rw.setAttribute(LinearIntDivAttr(), intVar);
+          if(rat > 0) {
+            d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(1)))))));
+          } else {
+            d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(-1)))))));
+          }
+        }
+        return intVar;
+      }
+    }
+    break;
+  }
+
+  case kind::INTS_MODULUS:
+  case kind::INTS_MODULUS_TOTAL: {
+    if(!options::rewriteDivk()) {
+      return n;
+    }
+    Node num = Rewriter::rewrite(n[0]);
+    Node den = Rewriter::rewrite(n[1]);
+    if(den.isConst()) {
+      const Rational& rat = den.getConst<Rational>();
+      Assert(!num.isConst());
+      if(rat != 0) {
+        Node intVar;
+        Node rw = nm->mkNode(k, num, den);
+        if(!rw.getAttribute(LinearIntDivAttr(), intVar)) {
+          intVar = nm->mkSkolem("linearIntDiv", nm->integerType(), "the result of an intdiv-by-k term");
+          rw.setAttribute(LinearIntDivAttr(), intVar);
+          if(rat > 0) {
+            d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(1)))))));
+          } else {
+            d_containing.d_out->lemma(nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, nm->mkNode(kind::MULT, den, intVar), num), nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(-1)))))));
+          }
+        }
+        Node node = nm->mkNode(kind::MINUS, num, nm->mkNode(kind::MULT, den, intVar));
+        return node;
+      }
+    }
+    break;
+  }
+
+  default:
+    ;
+  }
+
+  for(TNode::const_iterator i = n.begin(); i != n.end(); ++i) {
+    Node rewritten = ppRewriteTerms(*i);
+    if(rewritten != *i) {
+      NodeBuilder<> b(n.getKind());
+      b.append(n.begin(), i);
+      b << rewritten;
+      for(++i; i != n.end(); ++i) {
+        b << ppRewriteTerms(*i);
+      }
+      rewritten = b;
+      return rewritten;
+    }
+  }
+
+  return n;
+}
+
 Node TheoryArithPrivate::ppRewrite(TNode atom) {
   Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
 
-
   if (atom.getKind() == kind::EQUAL  && options::arithRewriteEq()) {
     Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
     Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
+    leq = ppRewriteTerms(leq);
+    geq = ppRewriteTerms(geq);
     Node rewritten = Rewriter::rewrite(leq.andNode(geq));
     Debug("arith::preprocess") << "arith::preprocess() : returning "
                                << rewritten << endl;
     return rewritten;
   } else {
-    return atom;
+    return ppRewriteTerms(atom);
   }
 }
 
@@ -902,7 +1025,7 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){
     // vl is the product of at least 2 variables
     // vl : (* v1 v2 ...)
     if(getLogicInfo().isLinear()){
-      throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
+      throw LogicException("A non-linear fact was asserted to arithmetic in a linear logic.");
     }
 
     setIncomplete();
@@ -939,7 +1062,7 @@ void TheoryArithPrivate::setupDivLike(const Variable& v){
   Assert(v.isDivLike());
 
   if(getLogicInfo().isLinear()){
-    throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
+    throw LogicException("A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic;\nif you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.");
   }
 
   Node vnode = v.getNode();
@@ -1161,16 +1284,22 @@ void TheoryArithPrivate::setupAtom(TNode atom) {
 void TheoryArithPrivate::preRegisterTerm(TNode n) {
   Debug("arith::preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl;
 
-  if(isRelationOperator(n.getKind())){
-    if(!isSetup(n)){
-      setupAtom(n);
+  try {
+    if(isRelationOperator(n.getKind())){
+      if(!isSetup(n)){
+        setupAtom(n);
+      }
+      Constraint c = d_constraintDatabase.lookup(n);
+      Assert(c != NullConstraint);
+  
+      Debug("arith::preregister") << "setup constraint" << c << endl;
+      Assert(!c->canBePropagated());
+      c->setPreregistered();
     }
-    Constraint c = d_constraintDatabase.lookup(n);
-    Assert(c != NullConstraint);
-
-    Debug("arith::preregister") << "setup constraint" << c << endl;
-    Assert(!c->canBePropagated());
-    c->setPreregistered();
+  } catch(LogicException& le) {
+    std::stringstream ss;
+    ss << le.getMessage() << endl << "The fact in question: " << n << endl;
+    throw LogicException(ss.str());
   }
 
   Debug("arith::preregister") << "end arith::preRegisterTerm("<< n <<")" << endl;
@@ -1187,7 +1316,10 @@ ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool slack){
   //TODO : The VarList trick is good enough?
   Assert(isLeaf(x) || VarList::isMember(x) || x.getKind() == PLUS);
   if(getLogicInfo().isLinear() && Variable::isDivMember(x)){
-    throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
+    stringstream ss;
+    ss << "A non-linear fact (involving div/mod/divisibility) was asserted to arithmetic in a linear logic: " << x << endl
+       << "if you only use division (or modulus) by a constant value, or if you only use the divisibility-by-k predicate, try using the --rewrite-divk option.";
+    throw LogicException(ss.str());
   }
   Assert(!d_partialModel.hasArithVar(x));
   Assert(x.getType().isReal()); // real or integer
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 86c8e213e..7370cfc15 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -346,7 +346,8 @@ private:
   Node axiomIteForTotalDivision(Node div_tot);
   Node axiomIteForTotalIntDivision(Node int_div_like);
 
-
+  // handle linear /, div, mod, and also is_int, to_int
+  Node ppRewriteTerms(TNode atom);
 
 public:
   TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index cc8451f8b..45e18fe0d 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -62,12 +62,37 @@ public:
         }
       }
     }
-    Kind k = n.getKind();
-    bool isDivision = k == kind::DIVISION || k == kind::DIVISION_TOTAL;
-    return (isInteger && !isDivision ? integerType : realType);
+    switch(Kind k = n.getKind()) {
+      case kind::TO_REAL:
+        return realType;
+      case kind::TO_INTEGER:
+        return integerType;
+      default: {
+        bool isDivision = k == kind::DIVISION || k == kind::DIVISION_TOTAL;
+        return (isInteger && !isDivision ? integerType : realType);
+      }
+    }
   }
 };/* class ArithOperatorTypeRule */
 
+class IntOperatorTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    TNode::iterator child_it = n.begin();
+    TNode::iterator child_it_end = n.end();
+    if(check) {
+      for(; child_it != child_it_end; ++child_it) {
+        TypeNode childType = (*child_it).getType(check);
+        if (!childType.isInteger()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting an integer subterm");
+        }
+      }
+    }
+    return nodeManager->integerType();
+  }
+};/* class IntOperatorTypeRule */
+
 class ArithPredicateTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
@@ -87,6 +112,34 @@ public:
   }
 };/* class ArithPredicateTypeRule */
 
+class ArithUnaryPredicateTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    if( check ) {
+      TypeNode t = n[0].getType(check);
+      if (!t.isReal()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};/* class ArithUnaryPredicateTypeRule */
+
+class IntUnaryPredicateTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    if( check ) {
+      TypeNode t = n[0].getType(check);
+      if (!t.isInteger()) {
+        throw TypeCheckingExceptionPrivate(n, "expecting an integer term");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+};/* class IntUnaryPredicateTypeRule */
+
 class SubrangeProperties {
 public:
   inline static Cardinality computeCardinality(TypeNode type) {