This commit removes the CONST_INTEGER kind from nodes. This code comes from the branch arithmetic/remove_const_int.

14 files changed, 46 insertions, 175 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 16169c10a..15e0d8001 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -1004,10 +1004,10 @@ Type ValidityChecker::intType() {
 Type ValidityChecker::subrangeType(const Expr& l, const Expr& r) {
   bool noLowerBound = l.getType().isString() && l.getConst<string>() == "_NEGINF";
   bool noUpperBound = r.getType().isString() && r.getConst<string>() == "_POSINF";
-  CheckArgument(noLowerBound || l.getKind() == CVC4::kind::CONST_INTEGER, l);
-  CheckArgument(noUpperBound || r.getKind() == CVC4::kind::CONST_INTEGER, r);
-  CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst<Integer>());
-  CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst<Integer>());
+  CheckArgument(noLowerBound || (l.getKind() == CVC4::kind::CONST_RATIONAL && l.getConst<Rational>().isIntegral()), l);
+  CheckArgument(noUpperBound || (r.getKind() == CVC4::kind::CONST_RATIONAL && r.getConst<Rational>().isIntegral()), r);
+  CVC4::SubrangeBound bl = noLowerBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(l.getConst<Rational>().getNumerator());
+  CVC4::SubrangeBound br = noUpperBound ? CVC4::SubrangeBound() : CVC4::SubrangeBound(r.getConst<Rational>().getNumerator());
   return d_em->mkSubrangeType(CVC4::SubrangeBounds(bl, br));
 }
 
diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp
index f09c552d1..3d077502d 100644
--- a/src/expr/pickler.cpp
+++ b/src/expr/pickler.cpp
@@ -207,17 +207,11 @@ void PicklerPrivate::toCaseConstant(TNode n) {
     d_current << mkConstantHeader(k, 1);
     d_current << mkBlockBody(n.getConst<bool>());
     break;
-  case kind::CONST_INTEGER:
   case kind::CONST_RATIONAL: {
     std::string asString;
-    if(k == kind::CONST_INTEGER) {
-      const Integer& i = n.getConst<Integer>();
-      asString = i.toString(16);
-    } else {
-      Assert(k == kind::CONST_RATIONAL);
-      const Rational& q = n.getConst<Rational>();
-      asString = q.toString(16);
-    }
+    Assert(k == kind::CONST_RATIONAL);
+    const Rational& q = n.getConst<Rational>();
+    asString = q.toString(16);
     toCaseString(k, asString);
     break;
   }
@@ -357,16 +351,10 @@ Node PicklerPrivate::fromCaseConstant(Kind k, uint32_t constblocks) {
     bool b= val.d_body.d_data;
     return d_nm->mkConst<bool>(b);
   }
-  case kind::CONST_INTEGER:
   case kind::CONST_RATIONAL: {
     std::string s = fromCaseString(constblocks);
-    if(k == kind::CONST_INTEGER) {
-      Integer i(s, 16);
-      return d_nm->mkConst<Integer>(i);
-    } else {
-      Rational q(s, 16);
-      return d_nm->mkConst<Rational>(q);
-    }
+    Rational q(s, 16);
+    return d_nm->mkConst<Rational>(q);
   }
   case kind::BITVECTOR_EXTRACT_OP: {
     Block high = d_current.dequeue();
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index a39defd14..bdf5fe59e 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -171,7 +171,7 @@ public:
   static unsigned tokenToUnsigned( pANTLR3_COMMON_TOKEN token );
 
   /** Retrieve an Integer from the text of a token */
-  static Integer tokenToInteger( pANTLR3_COMMON_TOKEN token );
+  static Rational tokenToInteger( pANTLR3_COMMON_TOKEN token );
 
   /** Retrieve a Rational from the text of a token */
   static Rational tokenToRational(pANTLR3_COMMON_TOKEN token);
@@ -263,8 +263,8 @@ inline unsigned AntlrInput::tokenToUnsigned(pANTLR3_COMMON_TOKEN token) {
   return result;
 }
 
-inline Integer AntlrInput::tokenToInteger(pANTLR3_COMMON_TOKEN token) {
-  return Integer( tokenText(token) );
+inline Rational AntlrInput::tokenToInteger(pANTLR3_COMMON_TOKEN token) {
+  return Rational( tokenText(token) );
 }
 
 inline Rational AntlrInput::tokenToRational(pANTLR3_COMMON_TOKEN token) {
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 52d32606b..2da9f0f63 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1165,7 +1165,7 @@ parameterization[CVC4::parser::DeclarationCheck check,
 
 bound returns [CVC4::parser::cvc::mySubrangeBound bound]
   : UNDERSCORE { $bound = SubrangeBound(); }
-  | k=integer { $bound = SubrangeBound(k); }
+  | k=integer { $bound = SubrangeBound(k.getNumerator()); }
 ;
 
 typeLetDecl[CVC4::parser::DeclarationCheck check]
@@ -1991,7 +1991,7 @@ numeral returns [unsigned k = 0]
 /**
  * Similar to numeral but for arbitrary-precision, signed integer.
  */
-integer returns [CVC4::Integer k = 0]
+integer returns [CVC4::Rational k = 0]
   : INTEGER_LITERAL
     { $k = AntlrInput::tokenToInteger($INTEGER_LITERAL); }
   | MINUS_TOK INTEGER_LITERAL
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 857513fa3..1f147479d 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -94,18 +94,13 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
     case kind::CONST_RATIONAL: {
       const Rational& rat = n.getConst<Rational>();
-      if(rat.getDenominator() == 1) {
+      if(rat.isIntegral()) {
         out << rat.getNumerator();
       } else {
         out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')';
       }
       break;
     }
-    case kind::CONST_INTEGER: {
-      const Integer& num = n.getConst<Integer>();
-      out << num;
-      break;
-    }
     case kind::CONST_PSEUDOBOOLEAN: {
       const Pseudoboolean& num = n.getConst<Pseudoboolean>();
       out << num;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 03422c162..2b686441a 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -100,25 +100,16 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     case kind::BUILTIN:
       out << smtKindString(n.getConst<Kind>());
       break;
-    case kind::CONST_INTEGER: {
-      Integer i = n.getConst<Integer>();
-      if(i < 0) {
-        out << "(- " << -i << ')';
-      } else {
-        out << i;
-      }
-      break;
-    }
     case kind::CONST_RATIONAL: {
       Rational r = n.getConst<Rational>();
       if(r < 0) {
-        if(r.getDenominator() == 1) {
+        if(r.isIntegral()) {
           out << "(- " << -r << ')';
         } else {
           out << "(- (/ " << (-r).getNumerator() << ' ' << (-r).getDenominator() << "))";
         }
       } else {
-        if(r.getDenominator() == 1) {
+        if(r.isIntegral()) {
           out << r;
         } else {
           out << "(/ " << r.getNumerator() << ' ' << r.getDenominator() << ')';
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0acd81248..90d21c60d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -931,13 +931,13 @@ void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertion
       SubrangeBounds bounds = t.getSubrangeBounds();
       Trace("constrainSubtypes") << "constrainSubtypes(): got bounds " << bounds << endl;
       if(bounds.lower.hasBound()) {
-        Node c = NodeManager::currentNM()->mkConst(bounds.lower.getBound());
+        Node c = NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound()));
         Node lb = NodeManager::currentNM()->mkNode(kind::LEQ, c, n);
         Trace("constrainSubtypes") << "constrainSubtypes(): assert " << lb << endl;
         assertions.push_back(lb);
       }
       if(bounds.upper.hasBound()) {
-        Node c = NodeManager::currentNM()->mkConst(bounds.upper.getBound());
+        Node c = NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound()));
         Node ub = NodeManager::currentNM()->mkNode(kind::LEQ, n, c);
         Trace("constrainSubtypes") << "constrainSubtypes(): assert " << ub << endl;
         assertions.push_back(ub);
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 863eb5c31..d7a6c0443 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -40,9 +40,9 @@ bool ArithRewriter::isAtom(TNode n) {
 
 RewriteResponse ArithRewriter::rewriteConstant(TNode t){
   Assert(t.getMetaKind() == kind::metakind::CONSTANT);
-  Node val = coerceToRationalNode(t);
+  Assert(t.getKind() == kind::CONST_RATIONAL);
 
-  return RewriteResponse(REWRITE_DONE, val);
+  return RewriteResponse(REWRITE_DONE, t);
 }
 
 RewriteResponse ArithRewriter::rewriteVariable(TNode t){
@@ -91,27 +91,23 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
   }else if(t.getKind() == kind::UMINUS){
     return rewriteUMinus(t, true);
   }else if(t.getKind() == kind::DIVISION){
-    if(t[0].getKind()== kind::CONST_RATIONAL){
-      return rewriteDivByConstant(t, true);
-    }else{
-      return RewriteResponse(REWRITE_DONE, t);
-    }
+    return RewriteResponse(REWRITE_DONE, t); // wait until t[1] is rewritten
   }else if(t.getKind() == kind::PLUS){
     return preRewritePlus(t);
   }else if(t.getKind() == kind::MULT){
     return preRewriteMult(t);
   }else if(t.getKind() == kind::INTS_DIVISION){
-    Integer intOne(1);
-    if(t[1].getKind()== kind::CONST_INTEGER && t[1].getConst<Integer>() == intOne){
+    Rational intOne(1);
+    if(t[1].getKind()== kind::CONST_RATIONAL && t[1].getConst<Rational>() == intOne){
       return RewriteResponse(REWRITE_AGAIN, t[0]);
     }else{
       return RewriteResponse(REWRITE_DONE, t);
     }
   }else if(t.getKind() == kind::INTS_MODULUS){
-    Integer intOne(1);
-    if(t[1].getKind()== kind::CONST_INTEGER && t[1].getConst<Integer>() == intOne){
-      Integer intZero(0);
-      return RewriteResponse(REWRITE_AGAIN, mkIntegerNode(intZero));
+    Rational intOne(1);
+    if(t[1].getKind()== kind::CONST_RATIONAL && t[1].getConst<Rational>() == intOne){
+      Rational intZero(0);
+      return RewriteResponse(REWRITE_AGAIN, mkRationalNode(intZero));
     }else{
       return RewriteResponse(REWRITE_DONE, t);
     }
@@ -147,8 +143,6 @@ RewriteResponse ArithRewriter::preRewriteMult(TNode t){
   Assert(t.getKind()== kind::MULT);
 
   // Rewrite multiplications with a 0 argument and to 0
-  Integer intZero;
-
   Rational qZero(0);
 
   for(TNode::iterator i = t.begin(); i != t.end(); ++i) {
@@ -156,14 +150,6 @@ RewriteResponse ArithRewriter::preRewriteMult(TNode t){
       if((*i).getConst<Rational>() == qZero) {
         return RewriteResponse(REWRITE_DONE, mkRationalNode(qZero));
       }
-    } else if((*i).getKind() == kind::CONST_INTEGER) {
-      if((*i).getConst<Integer>() == intZero) {
-        if(t.getType().isInteger()) {
-          return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(intZero));
-        } else {
-          return RewriteResponse(REWRITE_DONE, mkRationalNode(qZero));
-        }
-      }
     }
   }
   return RewriteResponse(REWRITE_DONE, t);
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 8ecc3abdc..e88ec073d 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -152,10 +152,9 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
     }
     break;
   case CONST_RATIONAL:
-  case CONST_INTEGER:
     // Mark constants as minmax
-    d_minMap[n] = coerceToRational(n);
-    d_maxMap[n] = coerceToRational(n);
+    d_minMap[n] = n.getConst<Rational>();
+    d_maxMap[n] = n.getConst<Rational>();
     break;
   case OR: {
     // Look for things like "x = 0 OR x = 1" (that are defTrue) and
@@ -193,46 +192,6 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
       break;
     }
 
-    Integer k1, k2;
-    if(c1.getType().getConst<TypeConstant>() == INTEGER_TYPE) {
-      k1 = c1.getConst<Integer>();
-    } else {
-      Rational r = c1.getConst<Rational>();
-      if(r.getDenominator() == 1) {
-        k1 = r.getNumerator();
-      } else {
-        break;
-      }
-    }
-    if(c2.getType().getConst<TypeConstant>() == INTEGER_TYPE) {
-      k2 = c2.getConst<Integer>();
-    } else {
-      Rational r = c2.getConst<Rational>();
-      if(r.getDenominator() == 1) {
-        k2 = r.getNumerator();
-      } else {
-        break;
-      }
-    }
-    if(k1 > k2) {
-      swap(k1, k2);
-    }
-    if(k1 + 1 == k2) {
-      Debug("arith::static") << "==> found " << n << endl
-                             << "    which indicates " << var << " \\in { "
-                             << k1 << " , " << k2 << " }" << endl;
-      c1 = NodeManager::currentNM()->mkConst(k1);
-      c2 = NodeManager::currentNM()->mkConst(k2);
-      Node lhs = NodeBuilder<2>(kind::GEQ) << var << c1;
-      Node rhs = NodeBuilder<2>(kind::LEQ) << var << c2;
-      Node l = lhs && rhs;
-      Debug("arith::static") << "    learned: " << l << endl;
-      learned << l;
-      if(k1 == 0) {
-        Assert(k2 == 1);
-        replaceWithPseudoboolean(var);
-      }
-    }
     break;
   }
   default: // Do nothing
@@ -466,7 +425,7 @@ void ArithStaticLearner::addBound(TNode n) {
   NodeToMinMaxMap::iterator minFind = d_minMap.find(n[0]);
   NodeToMinMaxMap::iterator maxFind = d_maxMap.find(n[0]);
 
-  Rational constant = coerceToRational(n[1]);
+  Rational constant = n[1].getConst<Rational>();
   DeltaRational bound = constant;
 
   switch(Kind k = n.getKind()) {
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index af32c3f87..fb669cce4 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -41,50 +41,12 @@ inline Node mkRationalNode(const Rational& q){
   return NodeManager::currentNM()->mkConst<Rational>(q);
 }
 
-inline Node mkIntegerNode(const Integer& z){
-  return NodeManager::currentNM()->mkConst<Integer>(z);
-}
-
 inline Node mkBoolNode(bool b){
   return NodeManager::currentNM()->mkConst<bool>(b);
 }
 
 
 
-inline Rational coerceToRational(TNode constant){
-  switch(constant.getKind()){
-  case kind::CONST_INTEGER:
-    {
-      Rational q(constant.getConst<Integer>());
-      return q;
-    }
-  case kind::CONST_RATIONAL:
-    return constant.getConst<Rational>();
-  default:
-    Unreachable();
-  }
-  Rational unreachable(0,0);
-  return unreachable;
-}
-
-inline Node coerceToRationalNode(TNode constant){
-  switch(constant.getKind()){
-  case kind::CONST_INTEGER:
-    {
-      Rational q(constant.getConst<Integer>());
-      Node n = mkRationalNode(q);
-      return n;
-    }
-  case kind::CONST_RATIONAL:
-    return constant;
-  default:
-    Unreachable();
-  }
-  return Node::null();
-}
-
-
-
 /** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */
 inline bool isRelationOperator(Kind k){
   using namespace kind;
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 95d7d6ed1..e00d8dc5e 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -31,7 +31,7 @@ sort REAL_TYPE \
 sort INTEGER_TYPE \
     Cardinality::INTEGERS \
     well-founded \
-        "NodeManager::currentNM()->mkConst(Integer(0))" \
+        "NodeManager::currentNM()->mkConst(Rational(0))" \
         "expr/node_manager.h" \
     "Integer type"
 sort PSEUDOBOOLEAN_TYPE \
@@ -59,11 +59,7 @@ constant CONST_RATIONAL \
     ::CVC4::RationalHashStrategy \
     "util/rational.h" \
     "a multiple-precision rational constant"
-constant CONST_INTEGER \
-    ::CVC4::Integer \
-    ::CVC4::IntegerHashStrategy \
-    "util/integer.h" \
-    "a multiple-precision integer constant"
+
 constant CONST_PSEUDOBOOLEAN \
     ::CVC4::Pseudoboolean \
     ::CVC4::PseudobooleanHashStrategy \
@@ -83,7 +79,6 @@ typerule DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule
 typerule POW ::CVC4::theory::arith::ArithOperatorTypeRule
 
 typerule CONST_RATIONAL ::CVC4::theory::arith::ArithConstantTypeRule
-typerule CONST_INTEGER ::CVC4::theory::arith::ArithConstantTypeRule
 
 typerule LT ::CVC4::theory::arith::ArithPredicateTypeRule
 typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 434be42a2..d67cd46a9 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -232,7 +232,6 @@ public:
 
   // TODO: check if it's a theory leaf also
   static bool isMember(Node n) {
-    if (n.getKind() == kind::CONST_INTEGER) return false;
     if (n.getKind() == kind::CONST_RATIONAL) return false;
     if (isRelationOperator(n.getKind())) return false;
     return Theory::isLeafOf(n, theory::THEORY_ARITH);
@@ -283,7 +282,8 @@ public:
   bool isNormalForm() { return isMember(getNode()); }
 
   static Constant mkConstant(Node n) {
-    return Constant(coerceToRationalNode(n));
+    Assert(n.getKind() == kind::CONST_RATIONAL);
+    return Constant(n);
   }
 
   static Constant mkConstant(const Rational& rat) {
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index d660cb4cd..1bd3277cd 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1239,8 +1239,8 @@ Node TheoryArith::roundRobinBranch(){
     Integer floor_d = d.floor();
     Integer ceil_d = d.ceiling();
 
-    Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkIntegerNode(floor_d)));
-    Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, mkIntegerNode(ceil_d)));
+    Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkRationalNode(floor_d)));
+    Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, mkRationalNode(ceil_d)));
 
 
     Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq);
@@ -1436,9 +1436,6 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) {
 
   switch(n.getKind()) {
 
-  case kind::CONST_INTEGER:
-    return Rational(n.getConst<Integer>());
-
   case kind::CONST_RATIONAL:
     return n.getConst<Rational>();
 
@@ -1456,9 +1453,6 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) {
   case kind::MULT: { // 2+ args
     Assert(n.getNumChildren() == 2 && n[0].isConst());
     DeltaRational value(1);
-    if (n[0].getKind() == kind::CONST_INTEGER) {
-      return getDeltaValue(n[1]) * n[0].getConst<Integer>();
-    }
     if (n[0].getKind() == kind::CONST_RATIONAL) {
       return getDeltaValue(n[1]) * n[0].getConst<Rational>();
     }
@@ -1478,9 +1472,6 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) {
     if (n[1].getKind() == kind::CONST_RATIONAL) {
       return getDeltaValue(n[0]) / n[0].getConst<Rational>();
     }
-    if (n[1].getKind() == kind::CONST_INTEGER) {
-      return getDeltaValue(n[0]) / n[0].getConst<Integer>();
-    }
     Unreachable();
 
 
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 8d0d79f0a..69c98a255 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -32,8 +32,12 @@ class ArithConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
-    if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType();
-    return nodeManager->integerType();
+    Assert(n.getKind() == kind::CONST_RATIONAL);
+    if(n.getConst<Rational>().isIntegral()){
+      return nodeManager->integerType();
+    }else{
+      return nodeManager->realType();
+    }
   }
 };/* class ArithConstantTypeRule */
 
@@ -101,12 +105,12 @@ public:
 
     const SubrangeBounds& bounds = type.getConst<SubrangeBounds>();
     if(bounds.lower.hasBound()) {
-      return NodeManager::currentNM()->mkConst(bounds.lower.getBound());
+      return NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound()));
     }
     if(bounds.upper.hasBound()) {
-      return NodeManager::currentNM()->mkConst(bounds.upper.getBound());
+      return NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound()));
     }
-    return NodeManager::currentNM()->mkConst(Integer(0));
+    return NodeManager::currentNM()->mkConst(Rational(0));
   }
 };/* class SubrangeProperties */