From 488ae3f42d9d3e06978e11a42d1d47e76072f797 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Tue, 15 May 2012 19:01:19 +0000
Subject: This commit removes the CONST_INTEGER kind from nodes. This code
 comes from the branch arithmetic/remove_const_int.

---
 src/theory/arith/kinds | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

(limited to 'src/theory/arith/kinds')

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
-- 
cgit v1.2.3