Final preparation for CONST_INTEGER (#8700)

With this PR, CI passes when using CONST_INTEGER instead of (all) integral CONST_RATIONAL.

This does not make this change yet, so CONST_RATIONAL is still used throughout.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index b5f0d463a12b57c122b9d298235170a080cf240f..d1146649b3382d27fcefdd753f29bcc656762649 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -2608,6 +2608,7 @@ const internal::Rational& getRational(const internal::Node& node)
   {
     case internal::Kind::CAST_TO_REAL:
       return node[0].getConst<internal::Rational>();
+    case internal::Kind::CONST_INTEGER:
     case internal::Kind::CONST_RATIONAL:
       return node.getConst<internal::Rational>();
     default:
@@ -2639,6 +2640,7 @@ bool checkReal64Bounds(const internal::Rational& r)
 bool isReal(const internal::Node& node)
 {
   return node.getKind() == internal::Kind::CONST_RATIONAL
+         || node.getKind() == internal::Kind::CONST_INTEGER
          || node.getKind() == internal::Kind::CAST_TO_REAL;
 }
 bool isReal32(const internal::Node& node)
@@ -2652,7 +2654,8 @@ bool isReal64(const internal::Node& node)
 
 bool isInteger(const internal::Node& node)
 {
-  return node.getKind() == internal::Kind::CONST_RATIONAL
+  return (node.getKind() == internal::Kind::CONST_RATIONAL
+          || node.getKind() == internal::Kind::CONST_INTEGER)
          && node.getConst<internal::Rational>().isIntegral();
 }
 bool isInt32(const internal::Node& node)
@@ -5242,12 +5245,10 @@ Term Solver::ensureTermSort(const Term& term, const Sort& sort) const
     // constructors. We do this cast using division with 1. This has the
     // advantage wrt using TO_REAL since (constant) division is always included
     // in the theory.
-    res = Term(
-        this,
-        d_nodeMgr->mkNode(extToIntKind(DIVISION),
-                          *res.d_node,
-                          d_nodeMgr->mkConst(internal::kind::CONST_RATIONAL,
-                                             internal::Rational(1))));
+    res = Term(this,
+               d_nodeMgr->mkNode(extToIntKind(DIVISION),
+                                 *res.d_node,
+                                 d_nodeMgr->mkConstInt(internal::Rational(1))));
   }
   Assert(res.getSort() == sort);
   return res;

diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp
index c27679b4f8f5d7cb4d5ed92db6aa938fd55ba777..dad48ba1ff102b7657e42c91bd11c8e9a012ab04 100644 (file)
--- a/src/expr/node_manager_template.cpp
+++ b/src/expr/node_manager_template.cpp
@@ -1304,6 +1304,7 @@ Node NodeManager::mkNode(TNode opNode, std::initializer_list<TNode> children)
 
 Node NodeManager::mkConstReal(const Rational& r)
 {
+  // works with (r.isIntegral() ? kind::CONST_INTEGER : kind::CONST_RATIONAL)
   return mkConst(kind::CONST_RATIONAL, r);
 }
 

diff --git a/src/theory/arith/arith_poly_norm.cpp b/src/theory/arith/arith_poly_norm.cpp
index 6da9653e4bbbc477b67af98e0b81094509b9887e..2226e94fc9277862bb03ddfdfbc678e0feef664c 100644 (file)
--- a/src/theory/arith/arith_poly_norm.cpp
+++ b/src/theory/arith/arith_poly_norm.cpp
@@ -158,7 +158,7 @@ std::vector<TNode> PolyNorm::getMonoVars(TNode m)
   if (!m.isNull())
   {
     Kind k = m.getKind();
-    Assert(k != CONST_RATIONAL);
+    Assert(k != CONST_RATIONAL && k != CONST_INTEGER);
     if (k == MULT || k == NONLINEAR_MULT)
     {
       vars.insert(vars.end(), m.begin(), m.end());
@@ -188,7 +188,7 @@ PolyNorm PolyNorm::mkPolyNorm(TNode n)
     Kind k = cur.getKind();
     if (it == visited.end())
     {
-      if (k == CONST_RATIONAL)
+      if (k == CONST_RATIONAL || k == CONST_INTEGER)
       {
         Rational r = cur.getConst<Rational>();
         if (r.sgn() == 0)
@@ -247,7 +247,8 @@ PolyNorm PolyNorm::mkPolyNorm(TNode n)
             }
           }
           break;
-        case CONST_RATIONAL: break;
+        case CONST_RATIONAL:
+        case CONST_INTEGER: break;
         default: Unhandled() << "Unhandled polynomial operation " << cur; break;
       }
     }

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 8920c51aa10c4a769dbaf903d09ca88314f48fe9..502b528b1eb60795e040969c48e0db31c29285a4 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -152,8 +152,8 @@ RewriteResponse ArithRewriter::postRewriteAtom(TNode atom)
   }
   // left |><| right
   Kind kind = atom.getKind();
-  Node left = removeToReal(atom[0]);
-  Node right = removeToReal(atom[1]);
+  Node left = rewriter::removeToReal(atom[0]);
+  Node right = rewriter::removeToReal(atom[1]);
 
   if (auto response = rewriter::tryEvaluateRelationReflexive(kind, left, right);
       response)
@@ -441,7 +441,7 @@ RewriteResponse ArithRewriter::postRewritePlus(TNode t)
     rewriter::addToSum(sum, child);
   }
   Node retSum = rewriter::collectSum(sum);
-  retSum = maybeEnsureReal(t.getType(), retSum);
+  retSum = rewriter::maybeEnsureReal(t.getType(), retSum);
   return RewriteResponse(REWRITE_DONE, retSum);
 }
 
@@ -452,7 +452,8 @@ RewriteResponse ArithRewriter::preRewriteMult(TNode node)
 
   if (auto res = rewriter::getZeroChild(node); res)
   {
-    return RewriteResponse(REWRITE_DONE, maybeEnsureReal(node.getType(), *res));
+    return RewriteResponse(REWRITE_DONE,
+                           rewriter::maybeEnsureReal(node.getType(), *res));
   }
   return RewriteResponse(REWRITE_DONE, node);
 }
@@ -466,7 +467,8 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){
 
   if (auto res = rewriter::getZeroChild(children); res)
   {
-    return RewriteResponse(REWRITE_DONE, maybeEnsureReal(t.getType(), *res));
+    return RewriteResponse(REWRITE_DONE,
+                           rewriter::maybeEnsureReal(t.getType(), *res));
   }
 
   Node ret;
@@ -489,7 +491,7 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){
         if (child.getConst<Rational>().isZero())
         {
           return RewriteResponse(REWRITE_DONE,
-                                 maybeEnsureReal(t.getType(), child));
+                                 rewriter::maybeEnsureReal(t.getType(), child));
         }
         ran *= child.getConst<Rational>();
       }
@@ -504,7 +506,7 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){
     }
     ret = rewriter::mkMultTerm(ran, std::move(leafs));
   }
-  ret = maybeEnsureReal(t.getType(), ret);
+  ret = rewriter::maybeEnsureReal(t.getType(), ret);
   return RewriteResponse(REWRITE_DONE, ret);
 }
 
@@ -513,8 +515,8 @@ RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre)
   Assert(t.getKind() == kind::DIVISION_TOTAL || t.getKind() == kind::DIVISION);
   Assert(t.getNumChildren() == 2);
 
-  Node left = removeToReal(t[0]);
-  Node right = removeToReal(t[1]);
+  Node left = rewriter::removeToReal(t[0]);
+  Node right = rewriter::removeToReal(t[1]);
   NodeManager* nm = NodeManager::currentNM();
   if (right.isConst())
   {
@@ -547,8 +549,8 @@ RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre)
     }
 
     Node result = nm->mkConstReal(den.inverse());
-    Node mult =
-        ensureReal(NodeManager::currentNM()->mkNode(kind::MULT, left, result));
+    Node mult = rewriter::ensureReal(
+        NodeManager::currentNM()->mkNode(kind::MULT, left, result));
     if (pre)
     {
       return RewriteResponse(REWRITE_DONE, mult);
@@ -562,20 +564,20 @@ RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre)
     // mkConst is applied to RAN in this block, which are always Real
     if (left.isConst())
     {
-      return RewriteResponse(
-          REWRITE_DONE,
-          ensureReal(rewriter::mkConst(left.getConst<Rational>() / den)));
+      return RewriteResponse(REWRITE_DONE,
+                             rewriter::ensureReal(rewriter::mkConst(
+                                 left.getConst<Rational>() / den)));
     }
     if (rewriter::isRAN(left))
     {
-      return RewriteResponse(
-          REWRITE_DONE,
-          ensureReal(rewriter::mkConst(rewriter::getRAN(left) / den)));
+      return RewriteResponse(REWRITE_DONE,
+                             rewriter::ensureReal(rewriter::mkConst(
+                                 rewriter::getRAN(left) / den)));
     }
 
     Node result = rewriter::mkConst(inverse(den));
-    Node mult =
-        ensureReal(NodeManager::currentNM()->mkNode(kind::MULT, left, result));
+    Node mult = rewriter::ensureReal(
+        NodeManager::currentNM()->mkNode(kind::MULT, left, result));
     if (pre)
     {
       return RewriteResponse(REWRITE_DONE, mult);
@@ -1124,40 +1126,6 @@ TrustNode ArithRewriter::expandDefinition(Node node)
   return ret;
 }
 
-TNode ArithRewriter::removeToReal(TNode t)
-{
-  return t.getKind() == kind::TO_REAL ? t[0] : t;
-}
-
-Node ArithRewriter::maybeEnsureReal(TypeNode tn, TNode t)
-{
-  // if we require being a real
-  if (!tn.isInteger())
-  {
-    // ensure that t has type real
-    Assert(tn.isReal());
-    return ensureReal(t);
-  }
-  return t;
-}
-
-Node ArithRewriter::ensureReal(TNode t)
-{
-  if (t.getType().isInteger())
-  {
-    if (t.isConst())
-    {
-      // short-circuit
-      Node ret = NodeManager::currentNM()->mkConstReal(t.getConst<Rational>());
-      Assert(ret.getType().isReal());
-      return ret;
-    }
-    Trace("arith-rewriter-debug") << "maybeEnsureReal: " << t << std::endl;
-    return NodeManager::currentNM()->mkNode(kind::TO_REAL, t);
-  }
-  return t;
-}
-
 RewriteResponse ArithRewriter::returnRewrite(TNode t, Node ret, Rewrite r)
 {
   Trace("arith-rewriter") << "ArithRewriter : " << t << " == " << ret << " by "

diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 3da45fead96001649dead5c5f04cc5592ac013b6..12f288d74ee7fc4ddb87ebfd84d6d075d4e17a5c 100644 (file)
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -94,17 +94,6 @@ class ArithRewriter : public TheoryRewriter
 
   /** return rewrite */
   static RewriteResponse returnRewrite(TNode t, Node ret, Rewrite r);
-  /**
-   * Remove TO_REAL from t, returns t[0] if t has kind TO_REAL.
-   */
-  static TNode removeToReal(TNode t);
-  /**
-   * Ensure that t has real type if tn is the real type. Do so by applying
-   * TO_REAL to t.
-   */
-  static Node maybeEnsureReal(TypeNode tn, TNode t);
-  /** Same as above, without a check for the type of tn. */
-  static Node ensureReal(TNode t);
   /** The operator elimination utility */
   OperatorElim& d_opElim;
 }; /* class ArithRewriter */

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 7f4398b9b1f5e6c4c9e0b58c0627e807cca20ea4..748703cf695d8856ed7bedd0c7ac1dd5537151cd 100644 (file)
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -38,10 +38,6 @@ typedef std::unordered_set<Node> NodeSet;
 typedef std::unordered_set<TNode> TNodeSet;
 typedef context::CDHashSet<Node> CDNodeSet;
 
-inline Node mkRationalNode(const Rational& q){
-  return NodeManager::currentNM()->mkConst(kind::CONST_RATIONAL, q);
-}
-
 inline Node mkBoolNode(bool b){
   return NodeManager::currentNM()->mkConst<bool>(b);
 }

diff --git a/src/theory/arith/linear/normal_form.cpp b/src/theory/arith/linear/normal_form.cpp
index ecbf10b1b9fb1ea1228567a9936db0ff50b12a03..f2c1b573600eada76b412bac52bab369796d7acd 100644 (file)
--- a/src/theory/arith/linear/normal_form.cpp
+++ b/src/theory/arith/linear/normal_form.cpp
@@ -29,8 +29,10 @@ namespace cvc5::internal {
 namespace theory {
 namespace arith::linear {
 
-Constant Constant::mkConstant(const Rational& rat) {
-  return Constant(mkRationalNode(rat));
+Constant Constant::mkConstant(const Rational& rat)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  return Constant(nm->mkConstReal(rat));
 }
 
 size_t Variable::getComplexity() const{

diff --git a/src/theory/arith/linear/theory_arith_private.cpp b/src/theory/arith/linear/theory_arith_private.cpp
index 0458a43ecb4040c8465f483101c674f69d583fda..793eb816a3a5f56788846cfac6d23fccdb986332 100644 (file)
--- a/src/theory/arith/linear/theory_arith_private.cpp
+++ b/src/theory/arith/linear/theory_arith_private.cpp
@@ -2041,7 +2041,7 @@ Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum){
     if(!vars.hasNode(x)){ return Node::null(); }
     Node xNode = vars.asNode(x);
     const Rational& q = sum[x];
-    Node mult = nm->mkNode(kind::MULT, mkRationalNode(q), xNode);
+    Node mult = nm->mkNode(kind::MULT, nm->mkConstReal(q), xNode);
     Trace("arith::toSumNode") << "toSumNode() " << x << " " << mult << endl;
     children.push_back(mult);
   }
@@ -4789,7 +4789,7 @@ bool TheoryArithPrivate::decomposeTerm(Node t,
   Polynomial poly = Polynomial::parsePolynomial(t);
   if(poly.isConstant()){
     c = poly.getHead().getConstant().getValue();
-    p = mkRationalNode(Rational(0));
+    p = NodeManager::currentNM()->mkConstReal(Rational(0));
     m = Rational(1);
     return true;
   }else if(poly.containsConstant()){
@@ -4838,22 +4838,6 @@ void TheoryArithPrivate::setToMin(int sgn, std::pair<Node, DeltaRational>& min,
   }
 }
 
-// std::pair<bool, Node> TheoryArithPrivate::entailmentUpperCheck(const Rational& lm, Node lp, const Rational& rm, Node rp, const DeltaRational& sep, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){
-
-//   Rational negRM = -rm;
-//   Node diff = NodeManager::currentNM()->mkNode(MULT, mkRationalConstan(lm), lp) + (negRM * rp);
-
-//   Rational diffm;
-//   Node diffp;
-//   decompose(diff, diffm, diffNode);
-
-
-//   std::pair<Node, DeltaRational> bestUbLeft, bestLbRight, bestUbDiff, tmp;
-//   bestUbLeft = bestLbRight = bestUbDiff = make_pair(Node::Null(), DeltaRational());
-
-//   return make_pair(false, Node::null());
-// }
-
 /**
  * Decomposes a literal into the form:
  *   dir*[lm*( lp )] k dir*[ [rm*( rp )] + sep ]

diff --git a/src/theory/arith/rewriter/node_utils.cpp b/src/theory/arith/rewriter/node_utils.cpp
index 3dfdff931670c56a65901ab8a798ddf18dd4c9b2..5285e29557e418949254adc29f3eac0211acf256 100644 (file)
--- a/src/theory/arith/rewriter/node_utils.cpp
+++ b/src/theory/arith/rewriter/node_utils.cpp
@@ -81,6 +81,37 @@ Node mkMultTerm(const RealAlgebraicNumber& multiplicity,
   return NodeManager::currentNM()->mkNode(Kind::NONLINEAR_MULT, monomial);
 }
 
+TNode removeToReal(TNode t) { return t.getKind() == kind::TO_REAL ? t[0] : t; }
+
+Node maybeEnsureReal(TypeNode tn, TNode t)
+{
+  // if we require being a real
+  if (!tn.isInteger())
+  {
+    // ensure that t has type real
+    Assert(tn.isReal());
+    return ensureReal(t);
+  }
+  return t;
+}
+
+Node ensureReal(TNode t)
+{
+  if (t.getType().isInteger())
+  {
+    if (t.isConst())
+    {
+      // short-circuit
+      Node ret = NodeManager::currentNM()->mkConstReal(t.getConst<Rational>());
+      Assert(ret.getType().isReal());
+      return ret;
+    }
+    Trace("arith-rewriter-debug") << "maybeEnsureReal: " << t << std::endl;
+    return NodeManager::currentNM()->mkNode(kind::TO_REAL, t);
+  }
+  return t;
+}
+
 }  // namespace rewriter
 }  // namespace arith
 }  // namespace theory

diff --git a/src/theory/arith/rewriter/node_utils.h b/src/theory/arith/rewriter/node_utils.h
index 54f8a16960ef4bb6dfb40ad2beddea3981919d79..71476b2d2aa26d059d1758b80b0111ab312c7c07 100644 (file)
--- a/src/theory/arith/rewriter/node_utils.h
+++ b/src/theory/arith/rewriter/node_utils.h
@@ -144,6 +144,18 @@ Node mkMultTerm(const RealAlgebraicNumber& multiplicity, TNode monomial);
 Node mkMultTerm(const RealAlgebraicNumber& multiplicity,
                 std::vector<Node>&& monomial);
 
+/**
+ * Remove TO_REAL from t, returns t[0] if t has kind TO_REAL.
+ */
+TNode removeToReal(TNode t);
+/**
+ * Ensure that t has real type if tn is the real type. Do so by applying
+ * TO_REAL to t.
+ */
+Node maybeEnsureReal(TypeNode tn, TNode t);
+/** Same as above, without a check for the type of tn. */
+Node ensureReal(TNode t);
+
 }  // namespace rewriter
 }  // namespace arith
 }  // namespace theory

diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp
index 6c6ce1fe36ee30c4c031e70941d6b18b1088fb45..388e2e4388d7271a978edd9291169a4652fae086 100644 (file)
--- a/test/unit/node/node_algorithm_black.cpp
+++ b/test/unit/node/node_algorithm_black.cpp
@@ -140,8 +140,8 @@ TEST_F(TestNodeBlackNodeAlgorithm, match)
 {
   TypeNode integer = d_nodeManager->integerType();
 
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
-  Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
+  Node two = d_nodeManager->mkConstInt(Rational(2));
 
   Node x = d_nodeManager->mkBoundVar(integer);
   Node a = d_skolemManager->mkDummySkolem("a", integer);

diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 039d591cd97c71bd75cd0e4098f5d60366d739a4..f0e8d0be83df0a940bd3cd18e389e81cc8dd798b 100644 (file)
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -737,15 +737,15 @@ TEST_F(TestNodeBlackNode, isConst)
   Node cons_1_nil =
       d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
                             cons,
-                            d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)),
+                            d_nodeManager->mkConstInt(Rational(1)),
                             d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil));
   Node cons_1_cons_2_nil = d_nodeManager->mkNode(
       APPLY_CONSTRUCTOR,
       cons,
-      d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)),
+      d_nodeManager->mkConstInt(Rational(1)),
       d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
                             cons,
-                            d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)),
+                            d_nodeManager->mkConstInt(Rational(2)),
                             d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)));
   ASSERT_TRUE(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst());
   ASSERT_FALSE(cons_x_nil.isConst());
@@ -754,8 +754,8 @@ TEST_F(TestNodeBlackNode, isConst)
 
   TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
                                                 d_nodeManager->integerType());
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+  Node zero = d_nodeManager->mkConstInt(Rational(0));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
   Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
   ASSERT_TRUE(storeAll.isConst());
 

diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp
index ec0ee24f9fe45d62bdc64cc5fe1f26ea5cf5b8d9..371bef1f08e5647d06464c0cb9bf231be395d6f7 100644 (file)
--- a/test/unit/node/node_manager_black.cpp
+++ b/test/unit/node/node_manager_black.cpp
@@ -140,7 +140,7 @@ TEST_F(TestNodeBlackNodeManager, mkConst_bool)
 TEST_F(TestNodeBlackNodeManager, mkConst_rational)
 {
   Rational r("3/2");
-  Node n = d_nodeManager->mkConst(CONST_RATIONAL, r);
+  Node n = d_nodeManager->mkConstReal(r);
   ASSERT_EQ(n.getConst<Rational>(), r);
 }
 

diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp
index c90625175190aada38ed1dca4182e54366ac5fb4..2c455a5dc3ca3c636c6b6228e336a147683ce204 100644 (file)
--- a/test/unit/node/node_manager_white.cpp
+++ b/test/unit/node/node_manager_white.cpp
@@ -34,8 +34,8 @@ class TestNodeWhiteNodeManager : public TestNode
 TEST_F(TestNodeWhiteNodeManager, mkConst_rational)
 {
   Rational i("3");
-  Node n = d_nodeManager->mkConst(CONST_RATIONAL, i);
-  Node m = d_nodeManager->mkConst(CONST_RATIONAL, i);
+  Node n = d_nodeManager->mkConstInt(i);
+  Node m = d_nodeManager->mkConstInt(i);
   ASSERT_EQ(n.getId(), m.getId());
 }
 

diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp
index edc9a28555206306b0fd9f8911f7e9806e316dec..3ace15512f181a4ffc9808437a7280268614face 100644 (file)
--- a/test/unit/node/node_white.cpp
+++ b/test/unit/node/node_white.cpp
@@ -49,7 +49,7 @@ TEST_F(TestNodeWhiteNode, iterators)
   Node x = d_nodeManager->mkVar("x", d_nodeManager->integerType());
   Node y = d_nodeManager->mkVar("y", d_nodeManager->integerType());
   Node x_plus_y = d_nodeManager->mkNode(ADD, x, y);
-  Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
+  Node two = d_nodeManager->mkConstInt(Rational(2));
   Node x_times_2 = d_nodeManager->mkNode(MULT, x, two);
 
   Node n = d_nodeManager->mkNode(ADD, x_times_2, x_plus_y, y);

diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp
index 83e74e07889f4474fea04fa321f0fc5c63f73ddc..b2a349ca0f3c3db79f980442f96c9bf53482c696 100644 (file)
--- a/test/unit/node/type_node_white.cpp
+++ b/test/unit/node/type_node_white.cpp
@@ -50,8 +50,8 @@ TEST_F(TestNodeWhiteTypeNode, sub_types)
   TypeNode bvType = d_nodeManager->mkBitVectorType(32);
 
   Node x = d_nodeManager->mkBoundVar("x", realType);
-  Node xPos = d_nodeManager->mkNode(
-      GT, x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
+  Node xPos =
+      d_nodeManager->mkNode(GT, x, d_nodeManager->mkConstInt(Rational(0)));
   TypeNode funtype = d_nodeManager->mkFunctionType(integerType, booleanType);
   Node lambda = d_nodeManager->mkVar("lambda", funtype);
   std::vector<Node> formals;

diff --git a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp
index e4e6c35f7e5ea5055825315dae8b23fd903d050b..84d6e8e3f522e49f3fa7e6b8f5b9c1f0d0ba12fd 100644 (file)
--- a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp
+++ b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp
@@ -35,7 +35,7 @@ TEST_F(TestPPWhiteForeignTheoryRewrite, simplify)
   std::cout << "len(x) >= 0 is simplified to true" << std::endl;
   Node x = d_nodeManager->mkVar("x", d_nodeManager->stringType());
   Node len_x = d_nodeManager->mkNode(kind::STRING_LENGTH, x);
-  Node zero = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, 0);
+  Node zero = d_nodeManager->mkConstInt(0);
   Node geq1 = d_nodeManager->mkNode(kind::GEQ, len_x, zero);
   Node tt = d_nodeManager->mkConst<bool>(true);
   Node simplified1 = ftr.foreignRewrite(geq1);

diff --git a/test/unit/theory/arith_poly_white.cpp b/test/unit/theory/arith_poly_white.cpp
index 4162ba611371a77cfa45a7038991e050c70815f5..44d3f39bbbc9ead183b3cb2664505fc136ae6809 100644 (file)
--- a/test/unit/theory/arith_poly_white.cpp
+++ b/test/unit/theory/arith_poly_white.cpp
@@ -40,9 +40,9 @@ class TestTheoryWhiteArithPolyNorm : public TestSmt
 TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_int)
 {
   TypeNode intType = d_nodeManager->integerType();
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
-  Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
+  Node zero = d_nodeManager->mkConstReal(Rational(0));
+  Node one = d_nodeManager->mkConstReal(Rational(1));
+  Node two = d_nodeManager->mkConstReal(Rational(2));
   Node x = d_nodeManager->mkVar("x", intType);
   Node y = d_nodeManager->mkVar("y", intType);
   Node z = d_nodeManager->mkVar("z", intType);
@@ -101,10 +101,10 @@ TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_int)
 TEST_F(TestTheoryWhiteArithPolyNorm, check_poly_norm_real)
 {
   TypeNode realType = d_nodeManager->realType();
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
-  Node half = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1) / Rational(2));
-  Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
+  Node zero = d_nodeManager->mkConstReal(Rational(0));
+  Node one = d_nodeManager->mkConstReal(Rational(1));
+  Node half = d_nodeManager->mkConstReal(Rational(1) / Rational(2));
+  Node two = d_nodeManager->mkConstReal(Rational(2));
   Node x = d_nodeManager->mkVar("x", realType);
   Node y = d_nodeManager->mkVar("y", realType);
 

diff --git a/test/unit/theory/evaluator_white.cpp b/test/unit/theory/evaluator_white.cpp
index 06106de2cc66f1cebdc40ed55fe543dd8aa9b9ff..5d480c7d46b4c3bed2a772af4f2155d945655cc8 100644 (file)
--- a/test/unit/theory/evaluator_white.cpp
+++ b/test/unit/theory/evaluator_white.cpp
@@ -103,8 +103,8 @@ TEST_F(TestTheoryWhiteEvaluator, strIdOf)
 {
   Node a = d_nodeManager->mkConst(String("A"));
   Node empty = d_nodeManager->mkConst(String(""));
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
-  Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
+  Node two = d_nodeManager->mkConstInt(Rational(2));
 
   std::vector<Node> args;
   std::vector<Node> vals;
@@ -150,14 +150,14 @@ TEST_F(TestTheoryWhiteEvaluator, code)
   {
     Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, a);
     Node r = eval.eval(n, args, vals);
-    ASSERT_EQ(r, d_nodeManager->mkConst(CONST_RATIONAL, Rational(65)));
+    ASSERT_EQ(r, d_nodeManager->mkConstInt(Rational(65)));
   }
 
   // (str.code "") ---> -1
   {
     Node n = d_nodeManager->mkNode(kind::STRING_TO_CODE, empty);
     Node r = eval.eval(n, args, vals);
-    ASSERT_EQ(r, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)));
+    ASSERT_EQ(r, d_nodeManager->mkConstInt(Rational(-1)));
   }
 }
 }  // namespace test

diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp
index 04c7d2502e98898cb17af51c58e0d8143e7b808c..e480db6ca6e14bb99824c85e1fc0053be7fc7e4b 100644 (file)
--- a/test/unit/theory/sequences_rewriter_white.cpp
+++ b/test/unit/theory/sequences_rewriter_white.cpp
@@ -94,11 +94,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_length_one)
   Node b = d_nodeManager->mkConst(String("B"));
   Node x = d_nodeManager->mkVar("x", strType);
   Node y = d_nodeManager->mkVar("y", strType);
-  Node negOne = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1));
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
-  Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
-  Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
+  Node negOne = d_nodeManager->mkConstInt(Rational(-1));
+  Node zero = d_nodeManager->mkConstInt(Rational(0));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
+  Node two = d_nodeManager->mkConstInt(Rational(2));
+  Node three = d_nodeManager->mkConstInt(Rational(3));
   Node i = d_nodeManager->mkVar("i", intType);
 
   ASSERT_TRUE(se.checkLengthOne(a));
@@ -129,7 +129,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_arith)
 
   Node z = d_nodeManager->mkVar("z", strType);
   Node n = d_nodeManager->mkVar("n", intType);
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
 
   // 1 >= (str.len (str.substr z n 1)) ---> true
   Node substr_z = d_nodeManager->mkNode(
@@ -151,8 +151,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption)
   Node y = d_nodeManager->mkVar("y", strType);
   Node z = d_nodeManager->mkVar("z", intType);
 
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+  Node zero = d_nodeManager->mkConstInt(Rational(0));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
 
   Node empty = d_nodeManager->mkConst(String(""));
   Node a = d_nodeManager->mkConst(String("A"));
@@ -185,8 +185,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption)
   ASSERT_TRUE(ae.checkWithAssumption(
       x_plus_slen_y_plus_slen_y_eq_zero, zero, x, false));
 
-  Node five = d_nodeManager->mkConst(CONST_RATIONAL, Rational(5));
-  Node six = d_nodeManager->mkConst(CONST_RATIONAL, Rational(6));
+  Node five = d_nodeManager->mkConstInt(Rational(5));
+  Node six = d_nodeManager->mkConstInt(Rational(6));
   Node x_plus_five = d_nodeManager->mkNode(kind::ADD, x, five);
   Node x_plus_five_lt_six =
       d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, six));
@@ -292,11 +292,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr)
   Node a = d_nodeManager->mkConst(String("A"));
   Node b = d_nodeManager->mkConst(String("B"));
   Node abcd = d_nodeManager->mkConst(String("ABCD"));
-  Node negone = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1));
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
-  Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
-  Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
+  Node negone = d_nodeManager->mkConstInt(Rational(-1));
+  Node zero = d_nodeManager->mkConstInt(Rational(0));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
+  Node two = d_nodeManager->mkConstInt(Rational(2));
+  Node three = d_nodeManager->mkConstInt(Rational(3));
 
   Node s = d_nodeManager->mkVar("s", strType);
   Node s2 = d_nodeManager->mkVar("s2", strType);
@@ -313,7 +313,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr)
       kind::STRING_SUBSTR,
       a,
       d_nodeManager->mkNode(
-          kind::ADD, x, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))),
+          kind::ADD, x, d_nodeManager->mkConstInt(Rational(1))),
       x);
   sameNormalForm(n, empty);
 
@@ -532,8 +532,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_concat)
 
   Node empty = d_nodeManager->mkConst(String(""));
   Node a = d_nodeManager->mkConst(String("A"));
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
+  Node zero = d_nodeManager->mkConstInt(Rational(0));
+  Node three = d_nodeManager->mkConstInt(Rational(3));
 
   Node i = d_nodeManager->mkVar("i", intType);
   Node s = d_nodeManager->mkVar("s", strType);
@@ -639,11 +639,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_indexOf)
   Node ccc = d_nodeManager->mkConst(String("CCC"));
   Node x = d_nodeManager->mkVar("x", strType);
   Node y = d_nodeManager->mkVar("y", strType);
-  Node negOne = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1));
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
-  Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
-  Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
+  Node negOne = d_nodeManager->mkConstInt(Rational(-1));
+  Node zero = d_nodeManager->mkConstInt(Rational(0));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
+  Node two = d_nodeManager->mkConstInt(Rational(2));
+  Node three = d_nodeManager->mkConstInt(Rational(3));
   Node i = d_nodeManager->mkVar("i", intType);
   Node j = d_nodeManager->mkVar("j", intType);
 
@@ -720,8 +720,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace)
   Node x = d_nodeManager->mkVar("x", strType);
   Node y = d_nodeManager->mkVar("y", strType);
   Node z = d_nodeManager->mkVar("z", strType);
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+  Node zero = d_nodeManager->mkConstInt(Rational(0));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
   Node n = d_nodeManager->mkVar("n", intType);
 
   // (str.replace (str.replace x "B" x) x "A") -->
@@ -1141,10 +1141,10 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
   Node z = d_nodeManager->mkVar("z", strType);
   Node n = d_nodeManager->mkVar("n", intType);
   Node m = d_nodeManager->mkVar("m", intType);
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
-  Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
-  Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
-  Node four = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
+  Node two = d_nodeManager->mkConstInt(Rational(2));
+  Node three = d_nodeManager->mkConstInt(Rational(3));
+  Node four = d_nodeManager->mkConstInt(Rational(4));
   Node t = d_nodeManager->mkConst(true);
   Node f = d_nodeManager->mkConst(false);
 
@@ -1567,9 +1567,9 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext)
   Node xxa = d_nodeManager->mkNode(kind::STRING_CONCAT, x, x, a);
   Node f = d_nodeManager->mkConst(false);
   Node n = d_nodeManager->mkVar("n", intType);
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
-  Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
+  Node zero = d_nodeManager->mkConstInt(Rational(0));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
+  Node three = d_nodeManager->mkConstInt(Rational(3));
 
   // Same normal form for:
   //

diff --git a/test/unit/theory/theory_arith_coverings_white.cpp b/test/unit/theory/theory_arith_coverings_white.cpp
index cdc8282fb0e19b591cb52a50194ef128c1f19136..912e21147cb94775dbc822b876c3b782e32fc569 100644 (file)
--- a/test/unit/theory/theory_arith_coverings_white.cpp
+++ b/test/unit/theory/theory_arith_coverings_white.cpp
@@ -205,15 +205,14 @@ TEST_F(TestTheoryWhiteArithCoverings, lazard_simp)
   Node a = d_nodeManager->mkVar(*d_realType);
   Node c = d_nodeManager->mkVar(*d_realType);
   Node orig = d_nodeManager->mkAnd(std::vector<Node>{
-      d_nodeManager->mkNode(
-          Kind::EQUAL, a, d_nodeManager->mkConst(CONST_RATIONAL, d_zero)),
+      d_nodeManager->mkNode(Kind::EQUAL, a, d_nodeManager->mkConstReal(d_zero)),
       d_nodeManager->mkNode(
           Kind::EQUAL,
           d_nodeManager->mkNode(
               Kind::ADD,
               d_nodeManager->mkNode(Kind::NONLINEAR_MULT, a, c),
-              d_nodeManager->mkConst(CONST_RATIONAL, d_one)),
-          d_nodeManager->mkConst(CONST_RATIONAL, d_zero))});
+              d_nodeManager->mkConstReal(d_one)),
+          d_nodeManager->mkConstReal(d_zero))});
 
   {
     Node rewritten = rewriter->rewrite(orig);
@@ -426,10 +425,10 @@ TEST_F(TestTheoryWhiteArithCoverings, test_cdcac_proof_1)
 TEST_F(TestTheoryWhiteArithCoverings, test_delta_one)
 {
   std::vector<Node> a;
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
-  Node mone = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1));
-  Node fifth = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 2));
+  Node zero = d_nodeManager->mkConstReal(Rational(0));
+  Node one = d_nodeManager->mkConstReal(Rational(1));
+  Node mone = d_nodeManager->mkConstReal(Rational(-1));
+  Node fifth = d_nodeManager->mkConstReal(Rational(1, 2));
   Node g = make_real_variable("g");
   Node l = make_real_variable("l");
   Node q = make_real_variable("q");
@@ -449,10 +448,10 @@ TEST_F(TestTheoryWhiteArithCoverings, test_delta_one)
 TEST_F(TestTheoryWhiteArithCoverings, test_delta_two)
 {
   std::vector<Node> a;
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
-  Node mone = d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1));
-  Node fifth = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 2));
+  Node zero = d_nodeManager->mkConstReal(Rational(0));
+  Node one = d_nodeManager->mkConstReal(Rational(1));
+  Node mone = d_nodeManager->mkConstReal(Rational(-1));
+  Node fifth = d_nodeManager->mkConstReal(Rational(1, 2));
   Node g = make_real_variable("g");
   Node l = make_real_variable("l");
   Node q = make_real_variable("q");

diff --git a/test/unit/theory/theory_arith_pow2_white.cpp b/test/unit/theory/theory_arith_pow2_white.cpp
index 1a60682bb1c1465b9dc2db9313f3bbb11c9e7beb..05576ff68a7d90737dd919b2519d09fc61886e17 100644 (file)
--- a/test/unit/theory/theory_arith_pow2_white.cpp
+++ b/test/unit/theory/theory_arith_pow2_white.cpp
@@ -36,11 +36,7 @@ class TestTheoryWhiteArithPow2 : public TestSmtNoFinishInit
     TestSmtNoFinishInit::SetUp();
     d_slvEngine->setOption("produce-models", "true");
     d_slvEngine->finishInit();
-    d_true = d_nodeManager->mkConst<bool>(true);
-    d_one = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, Rational(1));
   }
-  Node d_true;
-  Node d_one;
 };
 }  // namespace test
 }  // namespace cvc5::internal

diff --git a/test/unit/theory/theory_arith_rewriter_black.cpp b/test/unit/theory/theory_arith_rewriter_black.cpp
index ec6277c144806eb1b5af04976fbd5e7db9ac17e7..844d5f369688c72821240cffa21940cb48d27013 100644 (file)
--- a/test/unit/theory/theory_arith_rewriter_black.cpp
+++ b/test/unit/theory/theory_arith_rewriter_black.cpp
@@ -34,7 +34,7 @@ TEST_F(TestTheoryArithRewriterBlack, RealAlgebraicNumber)
   {
     RealAlgebraicNumber two({-8, 0, 0, 1}, 1, 3);
     Node n = d_nodeManager->mkRealAlgebraicNumber(two);
-    EXPECT_EQ(n.getKind(), Kind::CONST_RATIONAL);
+    EXPECT_EQ(n.isConst(), true);
     EXPECT_EQ(n.getConst<Rational>(), Rational(2));
   }
   {
@@ -51,7 +51,7 @@ TEST_F(TestTheoryArithRewriterBlack, RealAlgebraicNumber)
     Node n = d_nodeManager->mkRealAlgebraicNumber(sqrt2);
     n = d_nodeManager->mkNode(Kind::MULT, n, n);
     n = d_slvEngine->getRewriter()->rewrite(n);
-    EXPECT_EQ(n.getKind(), Kind::CONST_RATIONAL);
+    EXPECT_EQ(n.isConst(), true);
     EXPECT_EQ(n.getConst<Rational>(), Rational(2));
   }
   {
@@ -59,7 +59,7 @@ TEST_F(TestTheoryArithRewriterBlack, RealAlgebraicNumber)
     Node n = d_nodeManager->mkRealAlgebraicNumber(sqrt2);
     n = d_nodeManager->mkNode(Kind::SUB, n, n);
     n = d_slvEngine->getRewriter()->rewrite(n);
-    EXPECT_EQ(n.getKind(), Kind::CONST_RATIONAL);
+    EXPECT_EQ(n.isConst(), true);
     EXPECT_EQ(n.getConst<Rational>(), Rational(0));
   }
   {

diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp
index 8285c07e1442c369fa21e50796c2b0cfcae1a9bf..d9c8abbb7f11182cef287560c7f68cc5a7b63e23 100644 (file)
--- a/test/unit/theory/theory_arith_white.cpp
+++ b/test/unit/theory/theory_arith_white.cpp
@@ -68,7 +68,7 @@ class TestTheoryWhiteArith : public TestSmtNoFinishInit
 TEST_F(TestTheoryWhiteArith, assert)
 {
   Node x = d_nodeManager->mkVar(*d_realType);
-  Node c = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, d_zero);
+  Node c = d_nodeManager->mkConstReal(d_zero);
 
   Node gt = d_nodeManager->mkNode(GT, x, c);
   Node leq = Rewriter::rewrite(gt.notNode());
@@ -83,9 +83,9 @@ TEST_F(TestTheoryWhiteArith, int_normal_form)
 {
   Node x = d_nodeManager->mkVar(*d_intType);
   Node xr = d_nodeManager->mkVar(*d_realType);
-  Node c0 = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, d_zero);
-  Node c1 = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, d_one);
-  Node c2 = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, Rational(2));
+  Node c0 = d_nodeManager->mkConstReal(d_zero);
+  Node c1 = d_nodeManager->mkConstReal(d_one);
+  Node c2 = d_nodeManager->mkConstReal(Rational(2));
 
   Node geq0 = d_nodeManager->mkNode(GEQ, x, c0);
   Node geq1 = d_nodeManager->mkNode(GEQ, x, c1);

diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp
index 37222a589186a97efe8b7a772cefe421f9d99c2e..d144f1107a0699b6ad540f5831b09e31af1ecbbc 100644 (file)
--- a/test/unit/theory/theory_bags_normal_form_white.cpp
+++ b/test/unit/theory/theory_bags_normal_form_white.cpp
@@ -71,18 +71,15 @@ TEST_F(TestTheoryWhiteBagsNormalForm, empty_bag_normal_form)
 TEST_F(TestTheoryWhiteBagsNormalForm, mkBag_constant_element)
 {
   std::vector<Node> elements = getNStrings(1);
-  Node negative = d_nodeManager->mkBag(
-      d_nodeManager->stringType(),
-      elements[0],
-      d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)));
-  Node zero =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           elements[0],
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
-  Node positive =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           elements[0],
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+  Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                       elements[0],
+                                       d_nodeManager->mkConstInt(Rational(-1)));
+  Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                   elements[0],
+                                   d_nodeManager->mkConstInt(Rational(0)));
+  Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                       elements[0],
+                                       d_nodeManager->mkConstInt(Rational(1)));
   Node emptybag = d_nodeManager->mkConst(
       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
 
@@ -103,25 +100,19 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_count)
   // (bag.count "x" (bag.union_disjoint (bag "x" 4) (bag "y" 5)) = 4
   // (bag.count "x" (bag.union_disjoint (bag "y" 5) (bag "z" 5)) = 0
 
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node four = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4));
+  Node zero = d_nodeManager->mkConstInt(Rational(0));
+  Node four = d_nodeManager->mkConstInt(Rational(4));
   Node empty = d_nodeManager->mkConst(
       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
   Node x = d_nodeManager->mkConst(String("x"));
   Node y = d_nodeManager->mkConst(String("y"));
   Node z = d_nodeManager->mkConst(String("z"));
-  Node x_4 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
-  Node y_5 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           y,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
-  Node z_5 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           z,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
+  Node x_4 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
+  Node y_5 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(5)));
+  Node z_5 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(5)));
 
   Node input1 = d_nodeManager->mkNode(BAG_COUNT, x, empty);
   Node output1 = zero;
@@ -165,23 +156,15 @@ TEST_F(TestTheoryWhiteBagsNormalForm, duplicate_removal)
   Node x = d_nodeManager->mkConst(String("x"));
   Node y = d_nodeManager->mkConst(String("y"));
 
-  Node x_1 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
-  Node y_1 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           y,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
-
-  Node x_4 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
-  Node y_5 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           y,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
+  Node x_1 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1)));
+  Node y_1 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
+
+  Node x_4 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
+  Node y_5 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(5)));
 
   Node input2 = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, x_4);
   Node output2 = x_1;
@@ -208,26 +191,16 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_max)
   Node x = d_nodeManager->mkConst(String("x"));
   Node y = d_nodeManager->mkConst(String("y"));
   Node z = d_nodeManager->mkConst(String("z"));
-  Node x_4 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
-  Node x_3 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)));
-  Node x_7 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(7)));
-  Node z_2 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           z,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)));
-  Node y_1 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           y,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+  Node x_4 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
+  Node x_3 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(3)));
+  Node x_7 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(7)));
+  Node z_2 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(2)));
+  Node y_1 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
 
   Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2);
   Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1);
@@ -248,18 +221,15 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_disjoint1)
   std::vector<Node> elements = getNStrings(3);
   Node emptybag = d_nodeManager->mkConst(
       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
-  Node A =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           elements[0],
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)));
-  Node B =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           elements[1],
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)));
-  Node C =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           elements[2],
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
+  Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                elements[0],
+                                d_nodeManager->mkConstInt(Rational(2)));
+  Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                elements[1],
+                                d_nodeManager->mkConstInt(Rational(3)));
+  Node C = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                elements[2],
+                                d_nodeManager->mkConstInt(Rational(4)));
 
   Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
   // unionDisjointAB is already in a normal form
@@ -282,10 +252,9 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_disjoint1)
   ASSERT_EQ(unionDisjointA_BC, BagsUtils::evaluate(unionDisjointAB_C));
 
   Node unionDisjointAA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, A);
-  Node AA =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           elements[0],
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
+  Node AA = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                 elements[0],
+                                 d_nodeManager->mkConstInt(Rational(4)));
   ASSERT_FALSE(unionDisjointAA.isConst());
   ASSERT_TRUE(AA.isConst());
   ASSERT_EQ(AA, BagsUtils::evaluate(unionDisjointAA));
@@ -306,26 +275,16 @@ TEST_F(TestTheoryWhiteBagsNormalForm, union_disjoint2)
   Node x = d_nodeManager->mkConst(String("x"));
   Node y = d_nodeManager->mkConst(String("y"));
   Node z = d_nodeManager->mkConst(String("z"));
-  Node x_4 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
-  Node x_3 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)));
-  Node x_7 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(7)));
-  Node z_2 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           z,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)));
-  Node y_1 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           y,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+  Node x_4 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
+  Node x_3 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(3)));
+  Node x_7 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(7)));
+  Node z_2 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(2)));
+  Node y_1 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
 
   Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2);
   Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1);
@@ -354,26 +313,16 @@ TEST_F(TestTheoryWhiteBagsNormalForm, intersection_min)
   Node x = d_nodeManager->mkConst(String("x"));
   Node y = d_nodeManager->mkConst(String("y"));
   Node z = d_nodeManager->mkConst(String("z"));
-  Node x_4 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
-  Node x_3 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)));
-  Node x_7 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(7)));
-  Node z_2 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           z,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)));
-  Node y_1 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           y,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+  Node x_4 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
+  Node x_3 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(3)));
+  Node x_7 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(7)));
+  Node z_2 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(2)));
+  Node y_1 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
 
   Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2);
   Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1);
@@ -399,30 +348,18 @@ TEST_F(TestTheoryWhiteBagsNormalForm, difference_subtract)
   Node x = d_nodeManager->mkConst(String("x"));
   Node y = d_nodeManager->mkConst(String("y"));
   Node z = d_nodeManager->mkConst(String("z"));
-  Node x_1 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
-  Node x_4 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
-  Node x_3 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)));
-  Node x_7 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(7)));
-  Node z_2 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           z,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)));
-  Node y_1 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           y,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+  Node x_1 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1)));
+  Node x_4 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
+  Node x_3 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(3)));
+  Node x_7 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(7)));
+  Node z_2 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(2)));
+  Node y_1 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
 
   Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2);
   Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1);
@@ -448,30 +385,18 @@ TEST_F(TestTheoryWhiteBagsNormalForm, difference_remove)
   Node x = d_nodeManager->mkConst(String("x"));
   Node y = d_nodeManager->mkConst(String("y"));
   Node z = d_nodeManager->mkConst(String("z"));
-  Node x_1 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
-  Node x_4 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
-  Node x_3 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)));
-  Node x_7 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(7)));
-  Node z_2 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           z,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(2)));
-  Node y_1 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           y,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+  Node x_1 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1)));
+  Node x_4 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
+  Node x_3 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(3)));
+  Node x_7 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(7)));
+  Node z_2 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), z, d_nodeManager->mkConstInt(Rational(2)));
+  Node y_1 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
 
   Node A = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, z_2);
   Node B = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_3, y_1);
@@ -496,27 +421,23 @@ TEST_F(TestTheoryWhiteBagsNormalForm, bag_card)
   Node x = d_nodeManager->mkConst(String("x"));
   Node y = d_nodeManager->mkConst(String("y"));
   Node z = d_nodeManager->mkConst(String("z"));
-  Node x_4 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
-  Node y_1 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           y,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+  Node x_4 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
+  Node y_1 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
 
   Node input1 = d_nodeManager->mkNode(BAG_CARD, empty);
-  Node output1 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+  Node output1 = d_nodeManager->mkConstInt(Rational(0));
 
   ASSERT_EQ(output1, BagsUtils::evaluate(input1));
 
   Node input2 = d_nodeManager->mkNode(BAG_CARD, x_4);
-  Node output2 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4));
+  Node output2 = d_nodeManager->mkConstInt(Rational(4));
   ASSERT_EQ(output2, BagsUtils::evaluate(input2));
 
   Node union_disjoint = d_nodeManager->mkNode(BAG_UNION_DISJOINT, x_4, y_1);
   Node input3 = d_nodeManager->mkNode(BAG_CARD, union_disjoint);
-  Node output3 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(5));
+  Node output3 = d_nodeManager->mkConstInt(Rational(5));
   ASSERT_EQ(output3, BagsUtils::evaluate(input3));
 }
 
@@ -536,18 +457,12 @@ TEST_F(TestTheoryWhiteBagsNormalForm, is_singleton)
   Node x = d_nodeManager->mkConst(String("x"));
   Node y = d_nodeManager->mkConst(String("y"));
   Node z = d_nodeManager->mkConst(String("z"));
-  Node x_1 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
-  Node x_4 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
-  Node y_1 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           y,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+  Node x_1 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1)));
+  Node x_4 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
+  Node y_1 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
 
   Node input1 = d_nodeManager->mkNode(BAG_IS_SINGLETON, empty);
   Node output1 = falseNode;
@@ -590,14 +505,10 @@ TEST_F(TestTheoryWhiteBagsNormalForm, from_set)
   Node xSingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
   Node ySingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), y);
 
-  Node x_1 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
-  Node y_1 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           y,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+  Node x_1 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1)));
+  Node y_1 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(1)));
 
   Node input2 = d_nodeManager->mkNode(BAG_FROM_SET, xSingleton);
   Node output2 = x_1;
@@ -633,14 +544,10 @@ TEST_F(TestTheoryWhiteBagsNormalForm, to_set)
   Node xSingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), x);
   Node ySingleton = d_nodeManager->mkSingleton(d_nodeManager->stringType(), y);
 
-  Node x_4 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
-  Node y_5 =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           y,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
+  Node x_4 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(4)));
+  Node y_5 = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), y, d_nodeManager->mkConstInt(Rational(5)));
 
   Node input2 = d_nodeManager->mkNode(BAG_TO_SET, x_4);
   Node output2 = xSingleton;

diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp
index 121d26171827142ef8319c9c4efba467739842b7..934649755fc927d3e8086212c328a171bb5bb300 100644 (file)
--- a/test/unit/theory/theory_bags_rewriter_white.cpp
+++ b/test/unit/theory/theory_bags_rewriter_white.cpp
@@ -78,7 +78,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_equality)
   Node constantBag =
       d_nodeManager->mkBag(d_nodeManager->stringType(),
                            emptyString,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+                           d_nodeManager->mkConstInt(Rational(1)));
 
   // (= A A) = true where A is a bag
   Node n1 = A.eqNode(A);
@@ -107,18 +107,15 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_equality)
 TEST_F(TestTheoryWhiteBagsRewriter, mkBag_constant_element)
 {
   std::vector<Node> elements = getNStrings(1);
-  Node negative = d_nodeManager->mkBag(
-      d_nodeManager->stringType(),
-      elements[0],
-      d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)));
-  Node zero =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           elements[0],
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
-  Node positive =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           elements[0],
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+  Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                       elements[0],
+                                       d_nodeManager->mkConstInt(Rational(-1)));
+  Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                   elements[0],
+                                   d_nodeManager->mkConstInt(Rational(0)));
+  Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                       elements[0],
+                                       d_nodeManager->mkConstInt(Rational(1)));
   Node emptybag = d_nodeManager->mkConst(
       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
   RewriteResponse negativeResponse = d_rewriter->postRewrite(negative);
@@ -140,22 +137,18 @@ TEST_F(TestTheoryWhiteBagsRewriter, mkBag_variable_element)
 {
   Node skolem =
       d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
-  Node variable = d_nodeManager->mkBag(
-      d_nodeManager->stringType(),
-      skolem,
-      d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)));
-  Node negative = d_nodeManager->mkBag(
-      d_nodeManager->stringType(),
-      skolem,
-      d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)));
-  Node zero =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           skolem,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
-  Node positive =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           skolem,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+  Node variable = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                       skolem,
+                                       d_nodeManager->mkConstInt(Rational(-1)));
+  Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                       skolem,
+                                       d_nodeManager->mkConstInt(Rational(-1)));
+  Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                   skolem,
+                                   d_nodeManager->mkConstInt(Rational(0)));
+  Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                       skolem,
+                                       d_nodeManager->mkConstInt(Rational(1)));
   Node emptybag = d_nodeManager->mkConst(
       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
   RewriteResponse negativeResponse = d_rewriter->postRewrite(negative);
@@ -175,9 +168,9 @@ TEST_F(TestTheoryWhiteBagsRewriter, mkBag_variable_element)
 
 TEST_F(TestTheoryWhiteBagsRewriter, bag_count)
 {
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
-  Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
+  Node zero = d_nodeManager->mkConstInt(Rational(0));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
+  Node three = d_nodeManager->mkConstInt(Rational(3));
   Node skolem =
       d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
   Node emptyBag = d_nodeManager->mkConst(
@@ -203,18 +196,14 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_count)
 TEST_F(TestTheoryWhiteBagsRewriter, duplicate_removal)
 {
   Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
-  Node bag =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
+  Node bag = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(5)));
 
   // (bag.duplicate_removal (bag x n)) = (bag x 1)
   Node n = d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag);
   RewriteResponse response = d_rewriter->postRewrite(n);
-  Node noDuplicate =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+  Node noDuplicate = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(1)));
   ASSERT_TRUE(response.d_node == noDuplicate
               && response.d_status == REWRITE_AGAIN_FULL);
 }
@@ -225,14 +214,12 @@ TEST_F(TestTheoryWhiteBagsRewriter, union_max)
   std::vector<Node> elements = getNStrings(2);
   Node emptyBag = d_nodeManager->mkConst(
       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
-  Node A =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           elements[0],
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(n)));
-  Node B = d_nodeManager->mkBag(
-      d_nodeManager->stringType(),
-      elements[1],
-      d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1)));
+  Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                elements[0],
+                                d_nodeManager->mkConstInt(Rational(n)));
+  Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                elements[1],
+                                d_nodeManager->mkConstInt(Rational(n + 1)));
   Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B);
   Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A);
   Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
@@ -311,18 +298,15 @@ TEST_F(TestTheoryWhiteBagsRewriter, union_disjoint)
   std::vector<Node> elements = getNStrings(3);
   Node emptyBag = d_nodeManager->mkConst(
       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
-  Node A =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           elements[0],
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(n)));
-  Node B = d_nodeManager->mkBag(
-      d_nodeManager->stringType(),
-      elements[1],
-      d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1)));
-  Node C = d_nodeManager->mkBag(
-      d_nodeManager->stringType(),
-      elements[2],
-      d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 2)));
+  Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                elements[0],
+                                d_nodeManager->mkConstInt(Rational(n)));
+  Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                elements[1],
+                                d_nodeManager->mkConstInt(Rational(n + 1)));
+  Node C = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                elements[2],
+                                d_nodeManager->mkConstInt(Rational(n + 2)));
 
   Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
   Node unionDisjointBA = d_nodeManager->mkNode(BAG_UNION_DISJOINT, B, A);
@@ -375,14 +359,12 @@ TEST_F(TestTheoryWhiteBagsRewriter, intersection_min)
   std::vector<Node> elements = getNStrings(2);
   Node emptyBag = d_nodeManager->mkConst(
       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
-  Node A =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           elements[0],
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(n)));
-  Node B = d_nodeManager->mkBag(
-      d_nodeManager->stringType(),
-      elements[1],
-      d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1)));
+  Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                elements[0],
+                                d_nodeManager->mkConstInt(Rational(n)));
+  Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                elements[1],
+                                d_nodeManager->mkConstInt(Rational(n + 1)));
   Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B);
   Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A);
   Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
@@ -463,14 +445,12 @@ TEST_F(TestTheoryWhiteBagsRewriter, difference_subtract)
   std::vector<Node> elements = getNStrings(2);
   Node emptyBag = d_nodeManager->mkConst(
       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
-  Node A =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           elements[0],
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(n)));
-  Node B = d_nodeManager->mkBag(
-      d_nodeManager->stringType(),
-      elements[1],
-      d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1)));
+  Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                elements[0],
+                                d_nodeManager->mkConstInt(Rational(n)));
+  Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                elements[1],
+                                d_nodeManager->mkConstInt(Rational(n + 1)));
   Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B);
   Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A);
   Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
@@ -558,14 +538,12 @@ TEST_F(TestTheoryWhiteBagsRewriter, difference_remove)
   std::vector<Node> elements = getNStrings(2);
   Node emptyBag = d_nodeManager->mkConst(
       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
-  Node A =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           elements[0],
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(n)));
-  Node B = d_nodeManager->mkBag(
-      d_nodeManager->stringType(),
-      elements[1],
-      d_nodeManager->mkConst(CONST_RATIONAL, Rational(n + 1)));
+  Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                elements[0],
+                                d_nodeManager->mkConstInt(Rational(n)));
+  Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                elements[1],
+                                d_nodeManager->mkConstInt(Rational(n + 1)));
   Node unionMaxAB = d_nodeManager->mkNode(BAG_UNION_MAX, A, B);
   Node unionMaxBA = d_nodeManager->mkNode(BAG_UNION_MAX, B, A);
   Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
@@ -638,7 +616,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, difference_remove)
 TEST_F(TestTheoryWhiteBagsRewriter, choose)
 {
   Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
-  Node c = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
+  Node c = d_nodeManager->mkConstInt(Rational(3));
   Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
 
   // (bag.choose (bag x c)) = x where c is a constant > 0
@@ -653,18 +631,16 @@ TEST_F(TestTheoryWhiteBagsRewriter, bag_card)
   Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
   Node emptyBag = d_nodeManager->mkConst(
       EmptyBag(d_nodeManager->mkBagType(d_nodeManager->stringType())));
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node c = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
+  Node zero = d_nodeManager->mkConstInt(Rational(0));
+  Node c = d_nodeManager->mkConstInt(Rational(3));
   Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, c);
   std::vector<Node> elements = getNStrings(2);
-  Node A =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           elements[0],
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
-  Node B =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           elements[1],
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
+  Node A = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                elements[0],
+                                d_nodeManager->mkConstInt(Rational(4)));
+  Node B = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                elements[1],
+                                d_nodeManager->mkConstInt(Rational(5)));
   Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
 
   // (bag.card (as bag.empty (Bag String)) = 0
@@ -697,7 +673,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, is_singleton)
   // (bag.is_singleton (bag x c) = (c == 1)
   Node n2 = d_nodeManager->mkNode(BAG_IS_SINGLETON, bag);
   RewriteResponse response2 = d_rewriter->postRewrite(n2);
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
   Node equal = c.eqNode(one);
   ASSERT_TRUE(response2.d_node == equal
               && response2.d_status == REWRITE_AGAIN_FULL);
@@ -711,7 +687,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, from_set)
   // (bag.from_set (set.singleton (set.singleton_op Int) x)) = (bag x 1)
   Node n = d_nodeManager->mkNode(BAG_FROM_SET, singleton);
   RewriteResponse response = d_rewriter->postRewrite(n);
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
   Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(), x, one);
   ASSERT_TRUE(response.d_node == bag
               && response.d_status == REWRITE_AGAIN_FULL);
@@ -720,10 +696,8 @@ TEST_F(TestTheoryWhiteBagsRewriter, from_set)
 TEST_F(TestTheoryWhiteBagsRewriter, to_set)
 {
   Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->stringType());
-  Node bag =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           x,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(5)));
+  Node bag = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), x, d_nodeManager->mkConstInt(Rational(5)));
 
   // (bag.to_set (bag x n)) = (set.singleton (set.singleton_op T) x)
   Node n = d_nodeManager->mkNode(BAG_TO_SET, bag);
@@ -754,14 +728,10 @@ TEST_F(TestTheoryWhiteBagsRewriter, map)
   std::vector<Node> elements = getNStrings(2);
   Node a = d_nodeManager->mkConst(String("a"));
   Node b = d_nodeManager->mkConst(String("b"));
-  Node A =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           a,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(3)));
-  Node B =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           b,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(4)));
+  Node A = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), a, d_nodeManager->mkConstInt(Rational(3)));
+  Node B = d_nodeManager->mkBag(
+      d_nodeManager->stringType(), b, d_nodeManager->mkConstInt(Rational(4)));
   Node unionDisjointAB = d_nodeManager->mkNode(BAG_UNION_DISJOINT, A, B);
 
   ASSERT_TRUE(unionDisjointAB.isConst());
@@ -772,10 +742,9 @@ TEST_F(TestTheoryWhiteBagsRewriter, map)
   // (bag "" 7))
   Node n2 = d_nodeManager->mkNode(BAG_MAP, lambda, unionDisjointAB);
   Node rewritten = Rewriter::rewrite(n2);
-  Node bag =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           empty,
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(7)));
+  Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                  empty,
+                                  d_nodeManager->mkConstInt(Rational(7)));
   //  - (bag.map f (bag.union_disjoint K1 K2)) =
   //      (bag.union_disjoint (bag.map f K1) (bag.map f K2))
   Node k1 = d_skolemManager->mkDummySkolem("K1", A.getType());
@@ -796,10 +765,10 @@ TEST_F(TestTheoryWhiteBagsRewriter, fold)
   TypeNode bagIntegerType =
       d_nodeManager->mkBagType(d_nodeManager->integerType());
   Node emptybag = d_nodeManager->mkConst(EmptyBag(bagIntegerType));
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
-  Node ten = d_nodeManager->mkConst(CONST_RATIONAL, Rational(10));
-  Node n = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
+  Node zero = d_nodeManager->mkConstInt(Rational(0));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
+  Node ten = d_nodeManager->mkConstInt(Rational(10));
+  Node n = d_nodeManager->mkConstInt(Rational(2));
   Node x = d_nodeManager->mkBoundVar("x", d_nodeManager->integerType());
   Node y = d_nodeManager->mkBoundVar("y", d_nodeManager->integerType());
   Node xy = d_nodeManager->mkNode(BOUND_VAR_LIST, x, y);
@@ -828,7 +797,7 @@ TEST_F(TestTheoryWhiteBagsRewriter, fold)
   // (bag.fold (lambda ((x Int)(y Int)) (+ x y)) 1 (bag 10 2)) = 21
   bag = d_nodeManager->mkBag(d_nodeManager->integerType(), ten, n);
   Node node3 = d_nodeManager->mkNode(BAG_FOLD, f, one, bag);
-  Node result3 = d_nodeManager->mkConst(CONST_RATIONAL, Rational(21));
+  Node result3 = d_nodeManager->mkConstInt(Rational(21));
   Node response3 = Rewriter::rewrite(node3);
   ASSERT_TRUE(response3 == result3);
 

diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp
index e98b248a8748f26f1b7b00c963e839268306a6a6..7f280583baac42d2eab232d4c32bcbf4c12df83a 100644 (file)
--- a/test/unit/theory/theory_bags_type_rules_white.cpp
+++ b/test/unit/theory/theory_bags_type_rules_white.cpp
@@ -50,13 +50,12 @@ class TestTheoryWhiteBagsTypeRule : public TestSmt
 TEST_F(TestTheoryWhiteBagsTypeRule, count_operator)
 {
   std::vector<Node> elements = getNStrings(1);
-  Node bag = d_nodeManager->mkBag(
-      d_nodeManager->stringType(),
-      elements[0],
-      d_nodeManager->mkConst(CONST_RATIONAL, Rational(100)));
+  Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                  elements[0],
+                                  d_nodeManager->mkConstInt(Rational(100)));
 
   Node count = d_nodeManager->mkNode(BAG_COUNT, elements[0], bag);
-  Node node = d_nodeManager->mkConst(CONST_RATIONAL, Rational(10));
+  Node node = d_nodeManager->mkConstInt(Rational(10));
 
   // node of type Int is not compatible with bag of type (Bag String)
   ASSERT_THROW(d_nodeManager->mkNode(BAG_COUNT, node, bag).getType(true),
@@ -66,10 +65,9 @@ TEST_F(TestTheoryWhiteBagsTypeRule, count_operator)
 TEST_F(TestTheoryWhiteBagsTypeRule, duplicate_removal_operator)
 {
   std::vector<Node> elements = getNStrings(1);
-  Node bag = d_nodeManager->mkBag(
-      d_nodeManager->stringType(),
-      elements[0],
-      d_nodeManager->mkConst(CONST_RATIONAL, Rational(10)));
+  Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                  elements[0],
+                                  d_nodeManager->mkConstInt(Rational(10)));
   ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag));
   ASSERT_EQ(d_nodeManager->mkNode(BAG_DUPLICATE_REMOVAL, bag).getType(),
             bag.getType());
@@ -78,18 +76,15 @@ TEST_F(TestTheoryWhiteBagsTypeRule, duplicate_removal_operator)
 TEST_F(TestTheoryWhiteBagsTypeRule, mkBag_operator)
 {
   std::vector<Node> elements = getNStrings(1);
-  Node negative = d_nodeManager->mkBag(
-      d_nodeManager->stringType(),
-      elements[0],
-      d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1)));
-  Node zero =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           elements[0],
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
-  Node positive =
-      d_nodeManager->mkBag(d_nodeManager->stringType(),
-                           elements[0],
-                           d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)));
+  Node negative = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                       elements[0],
+                                       d_nodeManager->mkConstInt(Rational(-1)));
+  Node zero = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                   elements[0],
+                                   d_nodeManager->mkConstInt(Rational(0)));
+  Node positive = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                       elements[0],
+                                       d_nodeManager->mkConstInt(Rational(1)));
 
   // only positive multiplicity are constants
   ASSERT_FALSE(BagMakeTypeRule::computeIsConst(d_nodeManager, negative));
@@ -109,10 +104,9 @@ TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator)
 TEST_F(TestTheoryWhiteBagsTypeRule, to_set_operator)
 {
   std::vector<Node> elements = getNStrings(1);
-  Node bag = d_nodeManager->mkBag(
-      d_nodeManager->stringType(),
-      elements[0],
-      d_nodeManager->mkConst(CONST_RATIONAL, Rational(10)));
+  Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                  elements[0],
+                                  d_nodeManager->mkConstInt(Rational(10)));
   ASSERT_NO_THROW(d_nodeManager->mkNode(BAG_TO_SET, bag));
   ASSERT_TRUE(d_nodeManager->mkNode(BAG_TO_SET, bag).getType().isSet());
 }
@@ -120,10 +114,9 @@ TEST_F(TestTheoryWhiteBagsTypeRule, to_set_operator)
 TEST_F(TestTheoryWhiteBagsTypeRule, map_operator)
 {
   std::vector<Node> elements = getNStrings(1);
-  Node bag = d_nodeManager->mkBag(
-      d_nodeManager->stringType(),
-      elements[0],
-      d_nodeManager->mkConst(CONST_RATIONAL, Rational(10)));
+  Node bag = d_nodeManager->mkBag(d_nodeManager->stringType(),
+                                  elements[0],
+                                  d_nodeManager->mkConstInt(Rational(10)));
   Node set =
       d_nodeManager->mkSingleton(d_nodeManager->stringType(), elements[0]);
 
@@ -140,7 +133,7 @@ TEST_F(TestTheoryWhiteBagsTypeRule, map_operator)
   ASSERT_EQ(d_nodeManager->integerType(),
             mappedBag.getType().getBagElementType());
 
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
   Node x2 = d_nodeManager->mkBoundVar("x", d_nodeManager->integerType());
   std::vector<Node> args2;
   args2.push_back(x2);

diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp
index cd65445b846e811f7e77ed87c7d1d2cbe87d03a8..d53fd2a0a3252a7f3d45b136bea03cef4fa2fffd 100644 (file)
--- a/test/unit/theory/theory_black.cpp
+++ b/test/unit/theory/theory_black.cpp
@@ -41,8 +41,8 @@ TEST_F(TestTheoryBlack, array_const)
 {
   TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
                                                 d_nodeManager->integerType());
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+  Node zero = d_nodeManager->mkConstInt(Rational(0));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
   Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
   ASSERT_TRUE(storeAll.isConst());
 

diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp
index f1f3a42890ba04a6f9e02027c7f8300bce2ac16b..d28f74d34991a3fa048334b087acd3973cf6d0b4 100644 (file)
--- a/test/unit/theory/theory_bv_int_blaster_white.cpp
+++ b/test/unit/theory/theory_bv_int_blaster_white.cpp
@@ -39,11 +39,7 @@ class TestTheoryWhiteBvIntblaster : public TestSmtNoFinishInit
     TestSmtNoFinishInit::SetUp();
     d_slvEngine->setOption("produce-models", "true");
     d_slvEngine->finishInit();
-    d_true = d_nodeManager->mkConst<bool>(true);
-    d_one = d_nodeManager->mkConst<Rational>(CONST_RATIONAL, Rational(1));
   }
-  Node d_true;
-  Node d_one;
 };
 
 TEST_F(TestTheoryWhiteBvIntblaster, intblaster_constants)
@@ -63,7 +59,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_constants)
   env.d_logic.lock();
   IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1);
   Node result = intBlaster.translateNoChildren(bv7_4, lemmas, skolems);
-  Node seven = d_nodeManager->mkConst(CONST_RATIONAL, Rational(7));
+  Node seven = d_nodeManager->mkConstInt(Rational(7));
   ASSERT_EQ(seven, result);
 
   // translating integer constants should not change them

diff --git a/test/unit/theory/theory_engine_white.cpp b/test/unit/theory/theory_engine_white.cpp
index 6a54baa30ef140a3d0d4d632a42906332a5b9e57..d00da636a14df47e1c9dfcd89d4464477806479c 100644 (file)
--- a/test/unit/theory/theory_engine_white.cpp
+++ b/test/unit/theory/theory_engine_white.cpp
@@ -80,7 +80,7 @@ TEST_F(TestTheoryWhiteEngine, rewriter_simple)
   Node z = d_nodeManager->mkVar("z", d_nodeManager->integerType());
 
   // make the expression (ADD x y (MULT z 0))
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0"));
+  Node zero = d_nodeManager->mkConstInt(Rational("0"));
   Node zTimesZero = d_nodeManager->mkNode(MULT, z, zero);
   Node n = d_nodeManager->mkNode(ADD, x, y, zTimesZero);
 
@@ -111,8 +111,8 @@ TEST_F(TestTheoryWhiteEngine, rewriter_complex)
       "g",
       d_nodeManager->mkFunctionType(d_nodeManager->realType(),
                                     d_nodeManager->integerType()));
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational("1"));
-  Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational("2"));
+  Node one = d_nodeManager->mkConstInt(Rational("1"));
+  Node two = d_nodeManager->mkConstInt(Rational("2"));
 
   Node f1 = d_nodeManager->mkNode(APPLY_UF, f, one);
   Node f2 = d_nodeManager->mkNode(APPLY_UF, f, two);

diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp
index d6573f3a7b8fb40f03bbb2e26fe86d2d6a0e71b1..5d40a16a98b6f0e051ea3b5668b5f80c2a7fe126 100644 (file)
--- a/test/unit/theory/theory_int_opt_white.cpp
+++ b/test/unit/theory/theory_int_opt_white.cpp
@@ -44,8 +44,8 @@ class TestTheoryWhiteIntOpt : public TestSmtNoFinishInit
 
 TEST_F(TestTheoryWhiteIntOpt, max)
 {
-  Node ub = d_nodeManager->mkConst(CONST_RATIONAL, Rational("100"));
-  Node lb = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0"));
+  Node ub = d_nodeManager->mkConstInt(Rational("100"));
+  Node lb = d_nodeManager->mkConstInt(Rational("0"));
 
   // Objectives to be optimized max_cost is max objective
   Node max_cost = d_nodeManager->mkVar(*d_intType);
@@ -75,8 +75,8 @@ TEST_F(TestTheoryWhiteIntOpt, max)
 
 TEST_F(TestTheoryWhiteIntOpt, min)
 {
-  Node ub = d_nodeManager->mkConst(CONST_RATIONAL, Rational("100"));
-  Node lb = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0"));
+  Node ub = d_nodeManager->mkConstInt(Rational("100"));
+  Node lb = d_nodeManager->mkConstInt(Rational("0"));
 
   // Objectives to be optimized max_cost is max objective
   Node max_cost = d_nodeManager->mkVar(*d_intType);
@@ -106,8 +106,8 @@ TEST_F(TestTheoryWhiteIntOpt, min)
 
 TEST_F(TestTheoryWhiteIntOpt, result)
 {
-  Node ub = d_nodeManager->mkConst(CONST_RATIONAL, Rational("100"));
-  Node lb = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0"));
+  Node ub = d_nodeManager->mkConstInt(Rational("100"));
+  Node lb = d_nodeManager->mkConstInt(Rational("0"));
 
   // Objectives to be optimized max_cost is max objective
   Node max_cost = d_nodeManager->mkVar(*d_intType);
@@ -134,9 +134,9 @@ TEST_F(TestTheoryWhiteIntOpt, result)
 
 TEST_F(TestTheoryWhiteIntOpt, open_interval)
 {
-  Node ub1 = d_nodeManager->mkConst(CONST_RATIONAL, Rational("100"));
-  Node lb1 = d_nodeManager->mkConst(CONST_RATIONAL, Rational("0"));
-  Node lb2 = d_nodeManager->mkConst(CONST_RATIONAL, Rational("110"));
+  Node ub1 = d_nodeManager->mkConstInt(Rational("100"));
+  Node lb1 = d_nodeManager->mkConstInt(Rational("0"));
+  Node lb2 = d_nodeManager->mkConstInt(Rational("110"));
 
   Node cost1 = d_nodeManager->mkVar(*d_intType);
   Node cost2 = d_nodeManager->mkVar(*d_intType);

diff --git a/test/unit/theory/theory_sets_rewriter_white.cpp b/test/unit/theory/theory_sets_rewriter_white.cpp
index 8a1af26678030c35ebe6ddd4ddf1a3d297885130..91b246bb88df2ac164d4cacabb6e820772d28074 100644 (file)
--- a/test/unit/theory/theory_sets_rewriter_white.cpp
+++ b/test/unit/theory/theory_sets_rewriter_white.cpp
@@ -43,7 +43,7 @@ class TestTheoryWhiteSetsRewriter : public TestSmt
 
 TEST_F(TestTheoryWhiteSetsRewriter, map)
 {
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
   TypeNode stringType = d_nodeManager->stringType();
   TypeNode integerType = d_nodeManager->integerType();
   Node emptysetInteger =

diff --git a/test/unit/theory/theory_strings_skolem_cache_black.cpp b/test/unit/theory/theory_strings_skolem_cache_black.cpp
index 04742cfdb02341c7733310782efee37deba7a169..8a3c8d5dc90fb33283304e0bcc6c4560c50e5221 100644 (file)
--- a/test/unit/theory/theory_strings_skolem_cache_black.cpp
+++ b/test/unit/theory/theory_strings_skolem_cache_black.cpp
@@ -33,7 +33,7 @@ class TestTheoryBlackStringsSkolemCache : public TestSmt
 
 TEST_F(TestTheoryBlackStringsSkolemCache, mkSkolemCached)
 {
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+  Node zero = d_nodeManager->mkConstInt(Rational(0));
   Node n = d_skolemManager->mkDummySkolem("n", d_nodeManager->integerType());
   Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->stringType());
   Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->stringType());

diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp
index 745df9a41a2c3f1d2129d11c63909b74dc2d245c..0752038981079b386537aec544b42046ddb1d083 100644 (file)
--- a/test/unit/theory/type_enumerator_white.cpp
+++ b/test/unit/theory/type_enumerator_white.cpp
@@ -75,64 +75,64 @@ TEST_F(TestTheoryWhiteTypeEnumerator, arith)
 {
   TypeEnumerator te(d_nodeManager->integerType());
   ASSERT_FALSE(te.isFinished());
-  ASSERT_EQ(*te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
+  ASSERT_EQ(*te, d_nodeManager->mkConstInt(Rational(0)));
   for (int i = 1; i <= 100; ++i)
   {
     ASSERT_FALSE(te.isFinished());
-    ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(i)));
+    ASSERT_EQ(*++te, d_nodeManager->mkConstInt(Rational(i)));
     ASSERT_FALSE(te.isFinished());
-    ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-i)));
+    ASSERT_EQ(*++te, d_nodeManager->mkConstInt(Rational(-i)));
   }
   ASSERT_FALSE(te.isFinished());
 
   te = TypeEnumerator(d_nodeManager->realType());
   ASSERT_FALSE(te.isFinished());
-  ASSERT_EQ(*te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0, 1)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 1)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 1)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(2, 1)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-2, 1)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 2)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 2)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3, 1)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-3, 1)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 3)));
+  ASSERT_EQ(*te, d_nodeManager->mkConstReal(Rational(0, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(1, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-1, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(2, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-2, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(1, 2)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-1, 2)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(3, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-3, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(1, 3)));
   ASSERT_FALSE(te.isFinished());
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 3)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(4, 1)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-4, 1)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3, 2)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-3, 2)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(2, 3)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-2, 3)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 4)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 4)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5, 1)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-5, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-1, 3)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(4, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-4, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(3, 2)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-3, 2)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(2, 3)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-2, 3)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(1, 4)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-1, 4)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(5, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-5, 1)));
   ASSERT_FALSE(te.isFinished());
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 5)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 5)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(6, 1)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-6, 1)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5, 2)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-5, 2)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(4, 3)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-4, 3)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3, 4)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-3, 4)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(2, 5)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-2, 5)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 6)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(1, 5)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-1, 5)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(6, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-6, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(5, 2)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-5, 2)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(4, 3)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-4, 3)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(3, 4)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-3, 4)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(2, 5)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-2, 5)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(1, 6)));
   ASSERT_FALSE(te.isFinished());
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 6)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(7, 1)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-7, 1)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(5, 3)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-5, 3)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3, 5)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-3, 5)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1, 7)));
-  ASSERT_EQ(*++te, d_nodeManager->mkConst(CONST_RATIONAL, Rational(-1, 7)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-1, 6)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(7, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-7, 1)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(5, 3)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-5, 3)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(3, 5)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-3, 5)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(1, 7)));
+  ASSERT_EQ(*++te, d_nodeManager->mkConstReal(Rational(-1, 7)));
   ASSERT_FALSE(te.isFinished());
 }
 
@@ -265,26 +265,26 @@ TEST_F(TestTheoryWhiteTypeEnumerator, arrays_infinite)
   // ensure that certain items were found
   TypeNode arrayType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
                                                   d_nodeManager->integerType());
-  Node zeroes = d_nodeManager->mkConst(ArrayStoreAll(
-      arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))));
-  Node ones = d_nodeManager->mkConst(ArrayStoreAll(
-      arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(1))));
-  Node twos = d_nodeManager->mkConst(ArrayStoreAll(
-      arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(2))));
-  Node threes = d_nodeManager->mkConst(ArrayStoreAll(
-      arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(3))));
-  Node fours = d_nodeManager->mkConst(ArrayStoreAll(
-      arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(4))));
-  Node tens = d_nodeManager->mkConst(ArrayStoreAll(
-      arrayType, d_nodeManager->mkConst(CONST_RATIONAL, Rational(10))));
+  Node zeroes = d_nodeManager->mkConst(
+      ArrayStoreAll(arrayType, d_nodeManager->mkConstInt(Rational(0))));
+  Node ones = d_nodeManager->mkConst(
+      ArrayStoreAll(arrayType, d_nodeManager->mkConstInt(Rational(1))));
+  Node twos = d_nodeManager->mkConst(
+      ArrayStoreAll(arrayType, d_nodeManager->mkConstInt(Rational(2))));
+  Node threes = d_nodeManager->mkConst(
+      ArrayStoreAll(arrayType, d_nodeManager->mkConstInt(Rational(3))));
+  Node fours = d_nodeManager->mkConst(
+      ArrayStoreAll(arrayType, d_nodeManager->mkConstInt(Rational(4))));
+  Node tens = d_nodeManager->mkConst(
+      ArrayStoreAll(arrayType, d_nodeManager->mkConstInt(Rational(10))));
 
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
-  Node two = d_nodeManager->mkConst(CONST_RATIONAL, Rational(2));
-  Node three = d_nodeManager->mkConst(CONST_RATIONAL, Rational(3));
-  Node four = d_nodeManager->mkConst(CONST_RATIONAL, Rational(4));
-  Node five = d_nodeManager->mkConst(CONST_RATIONAL, Rational(5));
-  Node eleven = d_nodeManager->mkConst(CONST_RATIONAL, Rational(11));
+  Node zero = d_nodeManager->mkConstInt(Rational(0));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
+  Node two = d_nodeManager->mkConstInt(Rational(2));
+  Node three = d_nodeManager->mkConstInt(Rational(3));
+  Node four = d_nodeManager->mkConstInt(Rational(4));
+  Node five = d_nodeManager->mkConstInt(Rational(5));
+  Node eleven = d_nodeManager->mkConstInt(Rational(11));
 
   ASSERT_EQ(elts.find(d_nodeManager->mkNode(STORE, ones, zero, zero)),
             elts.end());

diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp
index 0f4016698d4f246e2d76b42e39097c7e76efdbfb..91e3e0d26f79327027ce4d3a57982111776e1d89 100644 (file)
--- a/test/unit/util/array_store_all_white.cpp
+++ b/test/unit/util/array_store_all_white.cpp
@@ -32,15 +32,15 @@ TEST_F(TestUtilWhiteArrayStoreAll, store_all)
   TypeNode usort = d_nodeManager->mkSort("U");
   ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(),
                                            d_nodeManager->realType()),
-                d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2)));
+                d_nodeManager->mkConstReal(Rational(9, 2)));
   ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkSort("U"), usort),
                 d_nodeManager->mkConst(UninterpretedSortValue(usort, 0)));
   ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8),
                                            d_nodeManager->realType()),
-                d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
+                d_nodeManager->mkConstInt(Rational(0)));
   ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8),
                                            d_nodeManager->integerType()),
-                d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)));
+                d_nodeManager->mkConstInt(Rational(0)));
 }
 
 TEST_F(TestUtilWhiteArrayStoreAll, type_errors)
@@ -49,14 +49,13 @@ TEST_F(TestUtilWhiteArrayStoreAll, type_errors)
                              d_nodeManager->mkConst(UninterpretedSortValue(
                                  d_nodeManager->mkSort("U"), 0))),
                IllegalArgumentException);
-  ASSERT_THROW(
-      ArrayStoreAll(d_nodeManager->integerType(),
-                    d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2))),
-      IllegalArgumentException);
+  ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(),
+                             d_nodeManager->mkConstReal(Rational(9, 2))),
+               IllegalArgumentException);
   ASSERT_THROW(
       ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->integerType(),
                                                d_nodeManager->mkSort("U")),
-                    d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2))),
+                    d_nodeManager->mkConstReal(Rational(9, 2))),
       IllegalArgumentException);
 }
 
@@ -71,13 +70,12 @@ TEST_F(TestUtilWhiteArrayStoreAll, const_error)
       ArrayStoreAll(d_nodeManager->integerType(),
                     d_nodeManager->mkVar("x", d_nodeManager->integerType())),
       IllegalArgumentException);
-  ASSERT_THROW(
-      ArrayStoreAll(d_nodeManager->integerType(),
-                    d_nodeManager->mkNode(
-                        kind::ADD,
-                        d_nodeManager->mkConst(CONST_RATIONAL, Rational(1)),
-                        d_nodeManager->mkConst(CONST_RATIONAL, Rational(0)))),
-      IllegalArgumentException);
+  ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(),
+                             d_nodeManager->mkNode(
+                                 kind::ADD,
+                                 d_nodeManager->mkConstInt(Rational(1)),
+                                 d_nodeManager->mkConstInt(Rational(0)))),
+               IllegalArgumentException);
 }
 }  // namespace test
 }  // namespace cvc5::internal

diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp
index da41b41e6688a991709741282acdedf52e00d4b1..ad7ccc0f49ccc5e573a17ad01908ecc4524dc514 100644 (file)
--- a/test/unit/util/datatype_black.cpp
+++ b/test/unit/util/datatype_black.cpp
@@ -255,7 +255,7 @@ TEST_F(TestUtilBlackDatatype, listIntUpdate)
   const DType& ldt = listType.getDType();
   Node updater = ldt[0][0].getUpdater();
   Node gt = d_nodeManager->mkGroundTerm(listType);
-  Node zero = d_nodeManager->mkConst(CONST_RATIONAL, Rational(0));
+  Node zero = d_nodeManager->mkConstInt(Rational(0));
   Node truen = d_nodeManager->mkConst(true);
   // construct an update term
   Node uterm = d_nodeManager->mkNode(kind::APPLY_UPDATER, updater, gt, zero);