This commit removes the CONST_INTEGER kind from nodes. This code comes from the branc...

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 16169c10a4b141edf195c32f92c20fa01c0a4f87..15e0d8001945583dc376d601c9652cf2983319f5 100644 (file)
--- 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 f09c552d1ae6ea522cd4026bd4eda0d00b7cbc97..3d077502d320e2a22192ca418449750cd3062236 100644 (file)
--- 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 a39defd14d01ead448ede75a69ad2dcdaf3f25ee..bdf5fe59ee0e97df9892ddb36a72f4ef99779fee 100644 (file)
--- 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 52d32606b2517489d2dc45dcc82969d76b9c70ac..2da9f0f638fdfbd3331fcaa5a691eba0157145b1 100644 (file)
--- 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 857513fa3fb376e63116eb348878c77c1efd46ad..1f147479ddbfa9b0006fc10b1368daf22b45a8ef 100644 (file)
--- 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 03422c1625165504af9174283c4d2da051f179b8..2b686441ab37e755716290c44cd30d1ace5ef381 100644 (file)
--- 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 0acd812489cb7cb094d88b7ceab410b77c714ad4..90d21c60d5afbee6853828ab49578d1fd6bb94df 100644 (file)
--- 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 863eb5c319b1323baaeb77449765a5b847a75bb5..d7a6c0443a59e7ca88b92c620292feeb34a47e07 100644 (file)
--- 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 8ecc3abdcbf46a248417b501acb142bdd602b61e..e88ec073d97b1abd23567d3f86bc3d1df03d3dcf 100644 (file)
--- 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 af32c3f8766a6ede16d753870142d3b9f0021396..fb669cce437c3f7b80fd2b9caf447215c087b7af 100644 (file)
--- 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 95d7d6ed1e04140faff882f54149ab9a5a492c01..e00d8dc5eac6c3daee09cac3a2bf4056d7ea35fb 100644 (file)
--- 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 434be42a20f710d70d1361865a26b78f20400697..d67cd46a94ae13ede36e829cb96c3ce8cde2aee9 100644 (file)
--- 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 d660cb4cd1fa76ccd53230b8debeb2634c86172a..1bd3277cde8d9a6f09616922149fc12007ae35d3 100644 (file)
--- 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 8d0d79f0a013839095e4cfe6f7ac87be7b690a83..69c98a25548c788ed028deaa35fb0db2580d1ea7 100644 (file)
--- 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 */
 

diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index 853d0086bd7d52e1b6cea18c1c0a0f1c90025f3b..491f995840b332e3546f8e5881419e7577dbc911 100644 (file)
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -66,8 +66,8 @@ public:
       d_apply_fun_bool = new Expr(d_em->mkExpr(APPLY_UF, *fun_op, *a_bool));
       null = new Expr;
 
-      i1 = new Expr(d_em->mkConst(Integer("0")));
-      i2 = new Expr(d_em->mkConst(Integer(23)));
+      i1 = new Expr(d_em->mkConst(Rational("0")));
+      i2 = new Expr(d_em->mkConst(Rational(23)));
       r1 = new Expr(d_em->mkConst(Rational(1, 5)));
       r2 = new Expr(d_em->mkConst(Rational("0")));
     } catch(Exception e) {
@@ -218,8 +218,8 @@ public:
     TS_ASSERT(d_apply_fun_bool->getKind() == APPLY_UF);
     TS_ASSERT(null->getKind() == NULL_EXPR);
 
-    TS_ASSERT(i1->getKind() == CONST_INTEGER);
-    TS_ASSERT(i2->getKind() == CONST_INTEGER);
+    TS_ASSERT(i1->getKind() == CONST_RATIONAL);
+    TS_ASSERT(i2->getKind() == CONST_RATIONAL);
     TS_ASSERT(r1->getKind() == CONST_RATIONAL);
     TS_ASSERT(r2->getKind() == CONST_RATIONAL);
   }
@@ -292,8 +292,8 @@ public:
     TS_ASSERT(d_apply_fun_bool->toString() == "(APPLY_UF f a)");
     TS_ASSERT(null->toString() == "null");
 
-    TS_ASSERT(i1->toString() == "(CONST_INTEGER 0)");
-    TS_ASSERT(i2->toString() == "(CONST_INTEGER 23)");
+    TS_ASSERT(i1->toString() == "(CONST_RATIONAL 0)");
+    TS_ASSERT(i2->toString() == "(CONST_RATIONAL 23)");
     TS_ASSERT(r1->toString() == "(CONST_RATIONAL 1/5)");
     TS_ASSERT(r2->toString() == "(CONST_RATIONAL 0)");
   }
@@ -324,8 +324,8 @@ public:
     TS_ASSERT(sd.str() == "(APPLY_UF f a)");
     TS_ASSERT(snull.str() == "null");
 
-    TS_ASSERT(si1.str() == "(CONST_INTEGER 0)");
-    TS_ASSERT(si2.str() == "(CONST_INTEGER 23)");
+    TS_ASSERT(si1.str() == "(CONST_RATIONAL 0)");
+    TS_ASSERT(si2.str() == "(CONST_RATIONAL 23)");
     TS_ASSERT(sr1.str() == "(CONST_RATIONAL 1/5)");
     TS_ASSERT(sr2.str() == "(CONST_RATIONAL 0)");
   }
@@ -362,14 +362,14 @@ public:
     TS_ASSERT_THROWS(b_bool->getConst<Kind>(), IllegalArgumentException);
     TS_ASSERT_THROWS(c_bool_and->getConst<Kind>(), IllegalArgumentException);
     TS_ASSERT(and_op->getConst<Kind>() == AND);
-    TS_ASSERT_THROWS(and_op->getConst<Integer>(), IllegalArgumentException);
+    TS_ASSERT_THROWS(and_op->getConst<Rational>(), IllegalArgumentException);
     TS_ASSERT(plus_op->getConst<Kind>() == PLUS);
     TS_ASSERT_THROWS(plus_op->getConst<Rational>(), IllegalArgumentException);
     TS_ASSERT_THROWS(d_apply_fun_bool->getConst<Kind>(), IllegalArgumentException);
     TS_ASSERT_THROWS(null->getConst<Kind>(), IllegalArgumentException);
 
-    TS_ASSERT(i1->getConst<Integer>() == 0);
-    TS_ASSERT(i2->getConst<Integer>() == 23);
+    TS_ASSERT(i1->getConst<Rational>() == 0);
+    TS_ASSERT(i2->getConst<Rational>() == 23);
     TS_ASSERT(r1->getConst<Rational>() == Rational(1, 5));
     TS_ASSERT(r2->getConst<Rational>() == Rational("0"));
 

diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index c30e4badb9bb669f2ca64a163c4ace3d6a0e5735..cca2ff4fcfdbab43354ce8846e6502ace26a91c1 100644 (file)
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -168,13 +168,6 @@ public:
     TS_ASSERT_EQUALS(ff.getConst<bool>(),false);
   }
 
-
-  void testMkConstInt() {
-    Integer i("3");
-    Node n = d_nodeManager->mkConst(i);
-    TS_ASSERT_EQUALS(n.getConst<Integer>(),i);
-  }
-
   void testMkConstRat() {
     Rational r("3/2");
     Node n = d_nodeManager->mkConst(r);

diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index 735fe2ac842f915c7c2705d5f28ed6e605b36544..15a178b5c3fa81b4d3f8a110d435e7ecc9369b61 100644 (file)
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -50,8 +50,8 @@ public:
     delete d_ctxt;
   }
 
-  void testMkConstInt() {
-    Integer i("3");
+  void testMkConstRational() {
+    Rational i("3");
     Node n = d_nm->mkConst(i);
     Node m = d_nm->mkConst(i);
     TS_ASSERT_EQUALS(n.getId(), m.getId());

diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index ce67004c6db3518470b70fa60a59a6ec4fdacb4f..a042b17529df388a5450fd4f5962a7a8591fbd70 100644 (file)
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -73,7 +73,7 @@ public:
     Node x = d_nm->mkVar("x", d_nm->integerType());
     Node y = d_nm->mkVar("y", d_nm->integerType());
     Node x_plus_y = d_nm->mkNode(PLUS, x, y);
-    Node two = d_nm->mkConst(Integer(2));
+    Node two = d_nm->mkConst(Rational(2));
     Node x_times_2 = d_nm->mkNode(MULT, x, two);
 
     Node n = d_nm->mkNode(PLUS, x_times_2, x_plus_y, y);