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

1 files changed, 0 insertions, 38 deletions

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;