Initial cut at distinguishing uses of CONST_RATIONAL (#7682)

diff --git a/src/expr/bound_var_manager.cpp b/src/expr/bound_var_manager.cpp
index 53c87fb970def06254f2980053379299cd5d8e22..450b2358fc76a354ab26a5c23da4f339803f6214 100644 (file)
--- a/src/expr/bound_var_manager.cpp
+++ b/src/expr/bound_var_manager.cpp
@@ -53,7 +53,7 @@ Node BoundVarManager::getCacheValue(TNode cv1, TNode cv2, size_t i)
 
 Node BoundVarManager::getCacheValue(size_t i)
 {
-  return NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(i));
+  return NodeManager::currentNM()->mkConstInt(Rational(i));
 }
 
 Node BoundVarManager::getCacheValue(TNode cv, size_t i)

diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 5b2503454b543b8ac3f7a3b3199b34a96dbb892f..4902b1562496cb2a752543353baf38a13fda9e54 100644 (file)
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -867,7 +867,7 @@ Node DType::getSharedSelector(TypeNode dtt, TypeNode t, size_t index) const
   ss << "sel_" << index;
   SkolemManager* sm = nm->getSkolemManager();
   TypeNode stype = nm->mkSelectorType(dtt, t);
-  Node nindex = nm->mkConst(CONST_RATIONAL, Rational(index));
+  Node nindex = nm->mkConstInt(Rational(index));
   s = sm->mkSkolemFunction(SkolemFunId::SHARED_SELECTOR, stype, nindex);
   d_sharedSel[dtt][t][index] = s;
   Trace("dt-shared-sel") << "Made " << s << " of type " << dtt << " -> " << t

diff --git a/src/expr/nary_term_util.cpp b/src/expr/nary_term_util.cpp
index a872c64c787a0d7ae04fd211d4a53079a7313d2c..03ce637e47d29f117143484df2137571bb565618 100644 (file)
--- a/src/expr/nary_term_util.cpp
+++ b/src/expr/nary_term_util.cpp
@@ -119,10 +119,10 @@ Node getNullTerminator(Kind k, TypeNode tn)
     case OR: nullTerm = nm->mkConst(false); break;
     case AND:
     case SEP_STAR: nullTerm = nm->mkConst(true); break;
-    case PLUS: nullTerm = nm->mkConst(CONST_RATIONAL, Rational(0)); break;
+    case PLUS: nullTerm = nm->mkConstRealOrInt(tn, Rational(0)); break;
     case MULT:
     case NONLINEAR_MULT:
-      nullTerm = nm->mkConst(CONST_RATIONAL, Rational(1));
+      nullTerm = nm->mkConstRealOrInt(tn, Rational(1));
       break;
     case STRING_CONCAT:
       // handles strings and sequences

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 6435c488a96981f9132c5780fab341b5f23965d6..b2682661e8608568da3034034305fc31b551f56d 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -579,6 +579,12 @@ class NodeManager
    */
   Node mkConstInt(const Rational& r);
 
+  /**
+   * Make constant real or int, which calls one of the above methods based
+   * on the type tn.
+   */
+  Node mkConstRealOrInt(const TypeNode& tn, const Rational& r);
+
   /** Create a node with children. */
   TypeNode mkTypeNode(Kind kind, TypeNode child1);
   TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2);

diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp
index b00d793225c1f9163448742aad5c7574a3a88244..4f235a53a5b50c4aec54b8f2b2f66156fd9cc32b 100644 (file)
--- a/src/expr/node_manager_template.cpp
+++ b/src/expr/node_manager_template.cpp
@@ -1298,4 +1298,15 @@ Node NodeManager::mkConstInt(const Rational& r)
   return mkConst(kind::CONST_RATIONAL, r);
 }
 
+Node NodeManager::mkConstRealOrInt(const TypeNode& tn, const Rational& r)
+{
+  Assert(tn.isRealOrInt()) << "Expected real or int for mkConstRealOrInt, got "
+                           << tn;
+  if (tn.isReal())
+  {
+    return mkConstReal(r);
+  }
+  return mkConstInt(r);
+}
+
 }  // namespace cvc5

diff --git a/src/expr/term_context_node.cpp b/src/expr/term_context_node.cpp
index 3be9faad0223a700eb0128d3db7b22e78219d48b..91e6dbfd3c9d3b43fd2bd5569c1aeb244e7eb12f 100644 (file)
--- a/src/expr/term_context_node.cpp
+++ b/src/expr/term_context_node.cpp
@@ -54,7 +54,7 @@ Node TCtxNode::getNodeHash() const { return computeNodeHash(d_node, d_val); }
 Node TCtxNode::computeNodeHash(Node n, uint32_t val)
 {
   NodeManager* nm = NodeManager::currentNM();
-  return nm->mkNode(kind::SEXPR, n, nm->mkConst(CONST_RATIONAL, Rational(val)));
+  return nm->mkNode(kind::SEXPR, n, nm->mkConstInt(Rational(val)));
 }
 
 Node TCtxNode::decomposeNodeHash(Node h, uint32_t& val)

diff --git a/src/expr/term_context_node.h b/src/expr/term_context_node.h
index ac89b0d71ef3cae19e00154bdfdbb35bee189aa3..9e4fe90de68b9019a7eccb6d1bfc5cce5f5d2ed9 100644 (file)
--- a/src/expr/term_context_node.h
+++ b/src/expr/term_context_node.h
@@ -54,7 +54,7 @@ class TCtxNode
   Node getNodeHash() const;
   /**
    * Get node hash, which is a unique node representation of the pair (n, val).
-   * In particular, this returns (SEXPR n (CONST_RATIONAL val)).
+   * In particular, this returns (SEXPR n (CONST_INTEGER val)).
    */
   static Node computeNodeHash(Node n, uint32_t val);
   /**

diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index e6b5a4bcab68b19ec95f109cec57348ab6f948c8..2ff45aef0009bb4cd78a078785851f01fa12a13c 100644 (file)
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -235,25 +235,19 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache)
       }
       else if (current.isConst())
       {
-        switch (current.getKind())
+        if (current.getType().isInteger())
         {
-          case kind::CONST_RATIONAL:
+          Rational constant = current.getConst<Rational>();
+          Assert (constant.isIntegral());
+          BitVector bv(size, constant.getNumerator());
+          if (bv.toSignedInteger() != constant.getNumerator())
           {
-            Rational constant = current.getConst<Rational>();
-            if (constant.isIntegral()) {
-              BitVector bv(size, constant.getNumerator());
-              if (bv.toSignedInteger() != constant.getNumerator())
-              {
-                throw TypeCheckingExceptionPrivate(
-                    current,
-                    string("Not enough bits for constant in intToBV: ")
-                        + current.toString());
-              }
-              result = nm->mkConst(bv);
-            }
-            break;
+            throw TypeCheckingExceptionPrivate(
+                current,
+                string("Not enough bits for constant in intToBV: ")
+                    + current.toString());
           }
-          default: break;
+          result = nm->mkConst(bv);
         }
       }
       else

diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 66646b76697ad9c5a56c6d7a367bb1400a7e88e7..1be5ee81b7320e786b5e7a03464a26c2c33fb51f 100644 (file)
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -213,8 +213,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
 
   NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = nm->getSkolemManager();
-  Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)),
-       one = nm->mkConst(CONST_RATIONAL, Rational(1));
+  Node zero = nm->mkConstInt(Rational(0)), one = nm->mkConstInt(Rational(1));
   Node trueNode = nm->mkConst(true);
 
   unordered_map<TNode, Node> intVars;
@@ -276,10 +275,8 @@ PreprocessingPassResult MipLibTrick::applyInternal(
         break;
       }
       if ((*j1)[1].getKind() != kind::EQUAL
-          || !(((*j1)[1][0].isVar()
-                && (*j1)[1][1].getKind() == kind::CONST_RATIONAL)
-               || ((*j1)[1][0].getKind() == kind::CONST_RATIONAL
-                   && (*j1)[1][1].isVar())))
+          || !(((*j1)[1][0].isVar() && (*j1)[1][1].isConst())
+               || ((*j1)[1][0].isConst() && (*j1)[1][1].isVar())))
       {
         eligible = false;
         Debug("miplib") << "  -- INELIGIBLE -- (=> (and X X) X)" << endl;
@@ -332,14 +329,11 @@ PreprocessingPassResult MipLibTrick::applyInternal(
         }
         sort(posv.begin(), posv.end());
         const Node pos = NodeManager::currentNM()->mkNode(kind::AND, posv);
-        const TNode var = ((*j1)[1][0].getKind() == kind::CONST_RATIONAL)
-                              ? (*j1)[1][1]
-                              : (*j1)[1][0];
+        const TNode var = ((*j1)[1][0].isConst()) ? (*j1)[1][1] : (*j1)[1][0];
         const pair<Node, Node> pos_var(pos, var);
-        const Rational& constant =
-            ((*j1)[1][0].getKind() == kind::CONST_RATIONAL)
-                ? (*j1)[1][0].getConst<Rational>()
-                : (*j1)[1][1].getConst<Rational>();
+        const Rational& constant = ((*j1)[1][0].isConst())
+                                       ? (*j1)[1][0].getConst<Rational>()
+                                       : (*j1)[1][1].getConst<Rational>();
         uint64_t mark = 0;
         unsigned countneg = 0, thepos = 0;
         for (unsigned ii = 0; ii < pos.getNumChildren(); ++ii)
@@ -406,14 +400,11 @@ PreprocessingPassResult MipLibTrick::applyInternal(
         const bool xneg = (x.getKind() == kind::NOT);
         x = xneg ? x[0] : x;
         Debug("miplib") << "  x:" << x << "  " << xneg << endl;
-        const TNode var = ((*j1)[1][0].getKind() == kind::CONST_RATIONAL)
-                              ? (*j1)[1][1]
-                              : (*j1)[1][0];
+        const TNode var = ((*j1)[1][0].isConst()) ? (*j1)[1][1] : (*j1)[1][0];
         const pair<Node, Node> x_var(x, var);
-        const Rational& constant =
-            ((*j1)[1][0].getKind() == kind::CONST_RATIONAL)
-                ? (*j1)[1][0].getConst<Rational>()
-                : (*j1)[1][1].getConst<Rational>();
+        const Rational& constant = ((*j1)[1][0].isConst())
+                                       ? (*j1)[1][0].getConst<Rational>()
+                                       : (*j1)[1][1].getConst<Rational>();
         unsigned mark = (xneg ? 0 : 1);
         if ((marks[x_var] & (1u << mark)) != 0)
         {
@@ -573,17 +564,15 @@ PreprocessingPassResult MipLibTrick::applyInternal(
             NodeBuilder sumb(kind::PLUS);
             for (size_t jj = 0; jj < pos.getNumChildren(); ++jj)
             {
-              sumb << nm->mkNode(kind::MULT,
-                                 nm->mkConst(CONST_RATIONAL, coef[pos_var][jj]),
-                                 newVars[jj]);
+              sumb << nm->mkNode(
+                  kind::MULT, nm->mkConstInt(coef[pos_var][jj]), newVars[jj]);
             }
             sum = sumb;
           }
           else
           {
-            sum = nm->mkNode(kind::MULT,
-                             nm->mkConst(CONST_RATIONAL, coef[pos_var][0]),
-                             newVars[0]);
+            sum = nm->mkNode(
+                kind::MULT, nm->mkConstInt(coef[pos_var][0]), newVars[0]);
           }
           Debug("miplib") << "vars[] " << var << endl
                           << "    eq " << rewrite(sum) << endl;

diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp
index 6c93eba153a5391664e6c77861a0e72f20c79849..0e7ac9c79e74b7fc04ccd8eb76e1256583a0a674 100644 (file)
--- a/src/preprocessing/passes/pseudo_boolean_processor.cpp
+++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp
@@ -66,7 +66,7 @@ bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated)
   Node l = assertion[0];
   Node r = assertion[1];
 
-  if (r.getKind() != kind::CONST_RATIONAL)
+  if (!r.isConst())
   {
     Debug("pbs::rewrites") << "not rhs constant" << assertion << std::endl;
     return false;
@@ -216,7 +216,7 @@ void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion,
   Node l = assertion[0];
   Node r = assertion[1];
 
-  if (r.getKind() == kind::CONST_RATIONAL)
+  if (r.isConst())
   {
     const Rational& rc = r.getConst<Rational>();
     if (isIntVar(l))
@@ -233,8 +233,7 @@ void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion,
     else if (l.getKind() == kind::MULT && l.getNumChildren() == 2)
     {
       Node c = l[0], v = l[1];
-      if (c.getKind() == kind::CONST_RATIONAL
-          && c.getConst<Rational>().isNegativeOne())
+      if (c.isConst() && c.getConst<Rational>().isNegativeOne())
       {
         if (isIntVar(v))
         {

diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index 5c453980816c36b8466fc5cf3ea5f960283cc3b3..d2cde7b46d3fe659c92c3792cdf5f83e4d67c875 100644 (file)
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -78,8 +78,7 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
               if (!c.isNull())
               {
                 Assert(c.isConst());
-                coeffs.push_back(NodeManager::currentNM()->mkConst(
-                    CONST_RATIONAL,
+                coeffs.push_back(nm->mkConstInt(
                     Rational(c.getConst<Rational>().getDenominator())));
               }
             }
@@ -134,15 +133,10 @@ Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& va
             }
             Node sumt =
                 sum.empty()
-                    ? NodeManager::currentNM()->mkConst(CONST_RATIONAL,
-                                                        Rational(0))
-                    : (sum.size() == 1
-                           ? sum[0]
-                           : NodeManager::currentNM()->mkNode(kind::PLUS, sum));
-            ret = NodeManager::currentNM()->mkNode(
-                ret_lit.getKind(),
-                sumt,
-                NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0)));
+                    ? nm->mkConstInt(Rational(0))
+                    : (sum.size() == 1 ? sum[0] : nm->mkNode(kind::PLUS, sum));
+            ret = nm->mkNode(
+                ret_lit.getKind(), sumt, nm->mkConstInt(Rational(0)));
             if (!ret_pol)
             {
               ret = ret.negate();

diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index ae05d6b871fa1cf1094481bd0feb9e3725300ae1..027be232ba36d65f1b913dfc5201fa2a8f32a307 100644 (file)
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -515,9 +515,9 @@ void UnconstrainedSimplifier::processUnconstrained()
             if (current.getType().isInteger())
             {
               // div/mult by 1 should have been simplified
-              Assert(other != nm->mkConst(CONST_RATIONAL, Rational(1)));
+              Assert(other != nm->mkConstInt(Rational(1)));
               // div by -1 should have been simplified
-              if (other != nm->mkConst(CONST_RATIONAL, Rational(-1)))
+              if (other != nm->mkConstInt(Rational(-1)))
               {
                 break;
               }

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index 6eab9b0368832427d327844578f6a4c5ed3f16f5..5af1c2b7e347cd8bcef90aa7e858be8bbafff909 100644 (file)
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -89,7 +89,7 @@ Node LfscNodeConverter::postConvert(Node n)
     }
     // bound variable v is (bvar x T)
     TypeNode intType = nm->integerType();
-    Node x = nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(n)));
+    Node x = nm->mkConstInt(Rational(getOrAssignIndexForVar(n)));
     Node tc = typeAsNode(convertType(tn));
     TypeNode ftype = nm->mkFunctionType({intType, d_sortType}, tn);
     Node bvarOp = getSymbolInternal(k, ftype, "bvar");
@@ -136,8 +136,7 @@ Node LfscNodeConverter::postConvert(Node n)
     TypeNode intType = nm->integerType();
     TypeNode varType = nm->mkFunctionType({intType, d_sortType}, tn);
     Node var = mkInternalSymbol("var", varType);
-    Node index =
-        nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(n)));
+    Node index = nm->mkConstInt(Rational(getOrAssignIndexForVar(n)));
     Node tc = typeAsNode(convertType(tn));
     return nm->mkNode(APPLY_UF, var, index, tc);
   }
@@ -176,7 +175,7 @@ Node LfscNodeConverter::postConvert(Node n)
     Node hconstf = getSymbolInternal(k, tnh, "apply");
     return nm->mkNode(APPLY_UF, hconstf, n[0], n[1]);
   }
-  else if (k == CONST_RATIONAL || k == CAST_TO_REAL)
+  else if (k == CONST_RATIONAL || k == CONST_INTEGER || k == CAST_TO_REAL)
   {
     if (k == CAST_TO_REAL)
     {
@@ -184,8 +183,9 @@ Node LfscNodeConverter::postConvert(Node n)
       do
       {
         n = n[0];
-        Assert(n.getKind() == APPLY_UF || n.getKind() == CONST_RATIONAL);
-      } while (n.getKind() != CONST_RATIONAL);
+        Assert(n.getKind() == APPLY_UF || n.getKind() == CONST_RATIONAL
+               || n.getKind() == CONST_INTEGER);
+      } while (n.getKind() != CONST_RATIONAL && n.getKind() != CONST_INTEGER);
     }
     TypeNode tnv = nm->mkFunctionType(tn, tn);
     Node rconstf;
@@ -198,7 +198,7 @@ Node LfscNodeConverter::postConvert(Node n)
       {
         // use LFSC syntax for mpz negation
         Node mpzn = getSymbolInternal(k, nm->mkFunctionType(tn, tn), "~");
-        arg = nm->mkNode(APPLY_UF, mpzn, nm->mkConst(CONST_RATIONAL, r.abs()));
+        arg = nm->mkNode(APPLY_UF, mpzn, nm->mkConstInt(r.abs()));
       }
       else
       {
@@ -344,8 +344,8 @@ Node LfscNodeConverter::postConvert(Node n)
     Node rop = getSymbolInternal(
         k, relType, printer::smt2::Smt2Printer::smtKindString(k));
     RegExpLoop op = n.getOperator().getConst<RegExpLoop>();
-    Node n1 = nm->mkConst(CONST_RATIONAL, Rational(op.d_loopMinOcc));
-    Node n2 = nm->mkConst(CONST_RATIONAL, Rational(op.d_loopMaxOcc));
+    Node n1 = nm->mkConstInt(Rational(op.d_loopMinOcc));
+    Node n2 = nm->mkConstInt(Rational(op.d_loopMaxOcc));
     return nm->mkNode(APPLY_UF, nm->mkNode(APPLY_UF, rop, n1, n2), n[0]);
   }
   else if (k == MATCH)
@@ -485,16 +485,14 @@ TypeNode LfscNodeConverter::postConvertType(TypeNode tn)
   else if (k == BITVECTOR_TYPE)
   {
     tnn = d_typeKindToNodeCons[k];
-    Node w = nm->mkConst(CONST_RATIONAL, Rational(tn.getBitVectorSize()));
+    Node w = nm->mkConstInt(Rational(tn.getBitVectorSize()));
     tnn = nm->mkNode(APPLY_UF, tnn, w);
   }
   else if (k == FLOATINGPOINT_TYPE)
   {
     tnn = d_typeKindToNodeCons[k];
-    Node e = nm->mkConst(CONST_RATIONAL,
-                         Rational(tn.getFloatingPointExponentSize()));
-    Node s = nm->mkConst(CONST_RATIONAL,
-                         Rational(tn.getFloatingPointSignificandSize()));
+    Node e = nm->mkConstInt(Rational(tn.getFloatingPointExponentSize()));
+    Node s = nm->mkConstInt(Rational(tn.getFloatingPointSignificandSize()));
     tnn = nm->mkNode(APPLY_UF, tnn, e, s);
   }
   else if (tn.getNumChildren() == 0)
@@ -723,8 +721,7 @@ void LfscNodeConverter::getCharVectorInternal(Node c, std::vector<Node>& chars)
   Node aconstf = getSymbolInternal(CONST_STRING, tnc, "char");
   for (unsigned i = 0, size = vec.size(); i < size; i++)
   {
-    Node cc = nm->mkNode(
-        APPLY_UF, aconstf, nm->mkConst(CONST_RATIONAL, Rational(vec[i])));
+    Node cc = nm->mkNode(APPLY_UF, aconstf, nm->mkConstInt(Rational(vec[i])));
     chars.push_back(cc);
   }
 }
@@ -747,42 +744,36 @@ std::vector<Node> LfscNodeConverter::getOperatorIndices(Kind k, Node n)
     case BITVECTOR_EXTRACT:
     {
       BitVectorExtract p = n.getConst<BitVectorExtract>();
-      indices.push_back(nm->mkConst(CONST_RATIONAL, Rational(p.d_high)));
-      indices.push_back(nm->mkConst(CONST_RATIONAL, Rational(p.d_low)));
+      indices.push_back(nm->mkConstInt(Rational(p.d_high)));
+      indices.push_back(nm->mkConstInt(Rational(p.d_low)));
       break;
     }
     case BITVECTOR_REPEAT:
-      indices.push_back(
-          nm->mkConst(CONST_RATIONAL,
-                      Rational(n.getConst<BitVectorRepeat>().d_repeatAmount)));
+      indices.push_back(nm->mkConstInt(
+          Rational(n.getConst<BitVectorRepeat>().d_repeatAmount)));
       break;
     case BITVECTOR_ZERO_EXTEND:
-      indices.push_back(nm->mkConst(
-          CONST_RATIONAL,
+      indices.push_back(nm->mkConstInt(
           Rational(n.getConst<BitVectorZeroExtend>().d_zeroExtendAmount)));
       break;
     case BITVECTOR_SIGN_EXTEND:
-      indices.push_back(nm->mkConst(
-          CONST_RATIONAL,
+      indices.push_back(nm->mkConstInt(
           Rational(n.getConst<BitVectorSignExtend>().d_signExtendAmount)));
       break;
     case BITVECTOR_ROTATE_LEFT:
-      indices.push_back(nm->mkConst(
-          CONST_RATIONAL,
+      indices.push_back(nm->mkConstInt(
           Rational(n.getConst<BitVectorRotateLeft>().d_rotateLeftAmount)));
       break;
     case BITVECTOR_ROTATE_RIGHT:
-      indices.push_back(nm->mkConst(
-          CONST_RATIONAL,
+      indices.push_back(nm->mkConstInt(
           Rational(n.getConst<BitVectorRotateRight>().d_rotateRightAmount)));
       break;
     case INT_TO_BITVECTOR:
-      indices.push_back(nm->mkConst(
-          CONST_RATIONAL, Rational(n.getConst<IntToBitVector>().d_size)));
+      indices.push_back(
+          nm->mkConstInt(Rational(n.getConst<IntToBitVector>().d_size)));
       break;
     case IAND:
-      indices.push_back(
-          nm->mkConst(CONST_RATIONAL, Rational(n.getConst<IntAnd>().d_size)));
+      indices.push_back(nm->mkConstInt(Rational(n.getConst<IntAnd>().d_size)));
       break;
     case APPLY_TESTER:
     {
@@ -1023,7 +1014,7 @@ Node LfscNodeConverter::getOperatorOfClosure(Node q, bool macroApply)
 Node LfscNodeConverter::getOperatorOfBoundVar(Node cop, Node v)
 {
   NodeManager* nm = NodeManager::currentNM();
-  Node x = nm->mkConst(CONST_RATIONAL, Rational(getOrAssignIndexForVar(v)));
+  Node x = nm->mkConstInt(Rational(getOrAssignIndexForVar(v)));
   Node tc = typeAsNode(convertType(v.getType()));
   return nm->mkNode(APPLY_UF, cop, x, tc);
 }

diff --git a/src/proof/lfsc/lfsc_util.cpp b/src/proof/lfsc/lfsc_util.cpp
index 06bedb8952b01dae8be39b099a1244f0d6298002..aca884ddcd0afe5e7aea8660f7c276b68786fd2c 100644 (file)
--- a/src/proof/lfsc/lfsc_util.cpp
+++ b/src/proof/lfsc/lfsc_util.cpp
@@ -68,8 +68,8 @@ LfscRule getLfscRule(Node n)
 
 Node mkLfscRuleNode(LfscRule r)
 {
-  return NodeManager::currentNM()->mkConst(CONST_RATIONAL,
-                                           Rational(static_cast<uint32_t>(r)));
+  return NodeManager::currentNM()->mkConstInt(
+      Rational(static_cast<uint32_t>(r)));
 }
 
 bool LfscProofLetifyTraverseCallback::shouldTraverse(const ProofNode* pn)

diff --git a/src/proof/method_id.cpp b/src/proof/method_id.cpp
index 9567590a80553d536f0d968cab88717cc89b3309..042df92bbae52ba3f1d03e8015a3441b56e08f16 100644 (file)
--- a/src/proof/method_id.cpp
+++ b/src/proof/method_id.cpp
@@ -51,8 +51,8 @@ std::ostream& operator<<(std::ostream& out, MethodId id)
 
 Node mkMethodId(MethodId id)
 {
-  return NodeManager::currentNM()->mkConst(CONST_RATIONAL,
-                                           Rational(static_cast<uint32_t>(id)));
+  return NodeManager::currentNM()->mkConstInt(
+      Rational(static_cast<uint32_t>(id)));
 }
 
 bool getMethodId(TNode n, MethodId& i)

diff --git a/src/proof/proof_checker.cpp b/src/proof/proof_checker.cpp
index 5289d77ffd700e947e34099d260ddbf248936783..b688a28f3389de537d18dbaabe342cf7dfa60157 100644 (file)
--- a/src/proof/proof_checker.cpp
+++ b/src/proof/proof_checker.cpp
@@ -74,8 +74,8 @@ Node ProofRuleChecker::mkKindNode(Kind k)
     // UNDEFINED_KIND is negative, hence return null to avoid cast
     return Node::null();
   }
-  return NodeManager::currentNM()->mkConst(CONST_RATIONAL,
-                                           Rational(static_cast<uint32_t>(k)));
+  return NodeManager::currentNM()->mkConstInt(
+      Rational(static_cast<uint32_t>(k)));
 }
 
 ProofCheckerStatistics::ProofCheckerStatistics()

diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index 61a1a298c0305b0318e289dd024cde5cd5b8d689..b5542ab357c241253fb13d5b88867b9e173c0163 100644 (file)
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -173,7 +173,7 @@ void ProofCnfStream::convertAndAssertAnd(TNode node, bool negated)
     for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i)
     {
       // Create a proof step for each n_i
-      Node iNode = nm->mkConst<Rational>(CONST_RATIONAL, i);
+      Node iNode = nm->mkConstInt(i);
       d_proof.addStep(node[i], PfRule::AND_ELIM, {node}, {iNode});
       Trace("cnf") << "ProofCnfStream::convertAndAssertAnd: AND_ELIM " << i
                    << " added norm " << node[i] << "\n";
@@ -232,7 +232,7 @@ void ProofCnfStream::convertAndAssertOr(TNode node, bool negated)
     for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i)
     {
       // Create a proof step for each (not n_i)
-      Node iNode = nm->mkConst<Rational>(CONST_RATIONAL, i);
+      Node iNode = nm->mkConstInt(i);
       d_proof.addStep(
           node[i].notNode(), PfRule::NOT_OR_ELIM, {node.notNode()}, {iNode});
       Trace("cnf") << "ProofCnfStream::convertAndAssertOr: NOT_OR_ELIM " << i
@@ -687,7 +687,7 @@ SatLiteral ProofCnfStream::handleAnd(TNode node)
     if (added)
     {
       Node clauseNode = nm->mkNode(kind::OR, node.notNode(), node[i]);
-      Node iNode = nm->mkConst<Rational>(CONST_RATIONAL, i);
+      Node iNode = nm->mkConstInt(i);
       d_proof.addStep(clauseNode, PfRule::CNF_AND_POS, {}, {node, iNode});
       Trace("cnf") << "ProofCnfStream::handleAnd: CNF_AND_POS " << i
                    << " added " << clauseNode << "\n";
@@ -747,7 +747,7 @@ SatLiteral ProofCnfStream::handleOr(TNode node)
     if (added)
     {
       Node clauseNode = nm->mkNode(kind::OR, node, node[i].notNode());
-      Node iNode = nm->mkConst<Rational>(CONST_RATIONAL, i);
+      Node iNode = nm->mkConstInt(i);
       d_proof.addStep(clauseNode, PfRule::CNF_OR_NEG, {}, {node, iNode});
       Trace("cnf") << "ProofCnfStream::handleOr: CNF_OR_NEG " << i << " added "
                    << clauseNode << "\n";

diff --git a/src/smt/difficulty_post_processor.cpp b/src/smt/difficulty_post_processor.cpp
index 31797ba5e88a45d9bf4645a9b11b65176978eb66..6d1882a4e517e83d8ff5efb61aa0402d6e5e6aac 100644 (file)
--- a/src/smt/difficulty_post_processor.cpp
+++ b/src/smt/difficulty_post_processor.cpp
@@ -69,7 +69,7 @@ void DifficultyPostprocessCallback::getDifficultyMap(
   NodeManager* nm = NodeManager::currentNM();
   for (const std::pair<const Node, uint64_t>& d : d_accMap)
   {
-    dmap[d.first] = nm->mkConst(CONST_RATIONAL, Rational(d.second));
+    dmap[d.first] = nm->mkConstInt(Rational(d.second));
   }
 }
 

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index a292fec8f588f4169ea468dd9d4d1d755517c5f8..90f0a48bffcadfa76c994398318140ba19cd4f3f 100644 (file)
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -855,7 +855,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
         for (size_t j = 0, nchildi = children[i].getNumChildren(); j < nchildi;
              j++)
         {
-          Node nodej = nm->mkConst(CONST_RATIONAL, Rational(j));
+          Node nodej = nm->mkConstInt(Rational(j));
           cdp->addStep(
               children[i][j], PfRule::AND_ELIM, {children[i]}, {nodej});
         }
@@ -1086,8 +1086,10 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
       TNode child = children[i];
       TNode scalar = args[i];
       bool isPos = scalar.getConst<Rational>() > 0;
-      Node scalarCmp = nm->mkNode(
-          isPos ? GT : LT, scalar, nm->mkConst(CONST_RATIONAL, Rational(0)));
+      Node scalarCmp =
+          nm->mkNode(isPos ? GT : LT,
+                     scalar,
+                     nm->mkConstRealOrInt(scalar.getType(), Rational(0)));
       // (= scalarCmp true)
       Node scalarCmpOrTrue = steps.tryStep(PfRule::EVALUATE, {}, {scalarCmp});
       Assert(!scalarCmpOrTrue.isNull());

diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index b5278a353ebf6a6639a1341fa1645aae33f799f5..c661dab4bc02b4b6271935b209918e795798b7b5 100644 (file)
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -47,9 +47,9 @@ IAndSolver::IAndSolver(Env& env,
   NodeManager* nm = NodeManager::currentNM();
   d_false = nm->mkConst(false);
   d_true = nm->mkConst(true);
-  d_zero = nm->mkConst(CONST_RATIONAL, Rational(0));
-  d_one = nm->mkConst(CONST_RATIONAL, Rational(1));
-  d_two = nm->mkConst(CONST_RATIONAL, Rational(2));
+  d_zero = nm->mkConstInt(Rational(0));
+  d_one = nm->mkConstInt(Rational(1));
+  d_two = nm->mkConstInt(Rational(2));
 }
 
 IAndSolver::~IAndSolver() {}

diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp
index 8af1a38fb5f41f028f987b21821173558442fdb9..700eb6de9fe30040c13283fd9aa1a8ddbdadf3c6 100644 (file)
--- a/src/theory/arith/nl/iand_utils.cpp
+++ b/src/theory/arith/nl/iand_utils.cpp
@@ -38,7 +38,7 @@ Node pow2(uint64_t k)
 {
   Assert(k >= 0);
   NodeManager* nm = NodeManager::currentNM();
-  return nm->mkConst(CONST_RATIONAL, Rational(intpow2(k)));
+  return nm->mkConstInt(Rational(intpow2(k)));
 }
 
 bool oneBitAnd(bool a, bool b) { return (a && b); }
@@ -60,9 +60,9 @@ Node intExtract(Node x, uint64_t i, uint64_t size)
 IAndUtils::IAndUtils()
 {
   NodeManager* nm = NodeManager::currentNM();
-  d_zero = nm->mkConst(CONST_RATIONAL, Rational(0));
-  d_one = nm->mkConst(CONST_RATIONAL, Rational(1));
-  d_two = nm->mkConst(CONST_RATIONAL, Rational(2));
+  d_zero = nm->mkConstInt(Rational(0));
+  d_one = nm->mkConstInt(Rational(1));
+  d_two = nm->mkConstInt(Rational(2));
 }
 
 Node IAndUtils::createITEFromTable(
@@ -80,8 +80,7 @@ Node IAndUtils::createITEFromTable(
   Assert(table.size() == 1 + ((uint64_t)(num_of_values * num_of_values)));
   // start with the default, most common value.
   // this value is represented in the table by (-1, -1).
-  Node ite =
-      nm->mkConst(CONST_RATIONAL, Rational(table.at(std::make_pair(-1, -1))));
+  Node ite = nm->mkConstInt(Rational(table.at(std::make_pair(-1, -1))));
   for (uint64_t i = 0; i < num_of_values; i++)
   {
     for (uint64_t j = 0; j < num_of_values; j++)
@@ -94,13 +93,10 @@ Node IAndUtils::createITEFromTable(
       // append the current value to the ite.
       ite = nm->mkNode(
           kind::ITE,
-          nm->mkNode(
-              kind::AND,
-              nm->mkNode(
-                  kind::EQUAL, x, nm->mkConst(CONST_RATIONAL, Rational(i))),
-              nm->mkNode(
-                  kind::EQUAL, y, nm->mkConst(CONST_RATIONAL, Rational(j)))),
-          nm->mkConst(CONST_RATIONAL, Rational(table.at(std::make_pair(i, j)))),
+          nm->mkNode(kind::AND,
+                     nm->mkNode(kind::EQUAL, x, nm->mkConstInt(Rational(i))),
+                     nm->mkNode(kind::EQUAL, y, nm->mkConstInt(Rational(j)))),
+          nm->mkConstInt(Rational(table.at(std::make_pair(i, j)))),
           ite);
     }
   }
@@ -139,7 +135,7 @@ Node IAndUtils::createSumNode(Node x,
   // number of elements in the sum expression
   uint64_t sumSize = bvsize / granularity;
   // initialize the sum
-  Node sumNode = nm->mkConst(CONST_RATIONAL, Rational(0));
+  Node sumNode = nm->mkConstInt(Rational(0));
   // compute the table for the current granularity if needed
   if (d_bvandTable.find(granularity) == d_bvandTable.end())
   {
@@ -264,7 +260,7 @@ Node IAndUtils::twoToK(unsigned k) const
 {
   // could be faster
   NodeManager* nm = NodeManager::currentNM();
-  return nm->mkNode(kind::POW, d_two, nm->mkConst(CONST_RATIONAL, Rational(k)));
+  return nm->mkNode(kind::POW, d_two, nm->mkConstInt(Rational(k)));
 }
 
 Node IAndUtils::twoToKMinusOne(unsigned k) const

diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp
index 4428d03508fa8fc99c9821be498889834d22ba4f..80ccd6707ebb65e991464a268b712368dd1bcf9f 100644 (file)
--- a/src/theory/bags/bag_solver.cpp
+++ b/src/theory/bags/bag_solver.cpp
@@ -42,8 +42,8 @@ BagSolver::BagSolver(Env& env,
       d_termReg(tr),
       d_mapCache(userContext())
 {
-  d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
-  d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
+  d_zero = NodeManager::currentNM()->mkConstInt(Rational(0));
+  d_one = NodeManager::currentNM()->mkConstInt(Rational(1));
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
 }

diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp
index 7667318060c336ac24701ef44cd83a0dca6a0e9d..a5fb206aaafc9b179f5b477733ce98bbaff82024 100644 (file)
--- a/src/theory/bags/bags_rewriter.cpp
+++ b/src/theory/bags/bags_rewriter.cpp
@@ -45,8 +45,8 @@ BagsRewriter::BagsRewriter(HistogramStat<Rewrite>* statistics)
     : d_statistics(statistics)
 {
   d_nm = NodeManager::currentNM();
-  d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0));
-  d_one = d_nm->mkConst(CONST_RATIONAL, Rational(1));
+  d_zero = d_nm->mkConstInt(Rational(0));
+  d_one = d_nm->mkConstInt(Rational(1));
 }
 
 RewriteResponse BagsRewriter::postRewrite(TNode n)

diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp
index a433ceb2dd36e555cfd8e35a90e536fccee5348d..cb6a3ea7092b7812dd15af32b5173fe49cc214ed 100644 (file)
--- a/src/theory/bags/inference_generator.cpp
+++ b/src/theory/bags/inference_generator.cpp
@@ -36,8 +36,8 @@ InferenceGenerator::InferenceGenerator(SolverState* state, InferenceManager* im)
   d_nm = NodeManager::currentNM();
   d_sm = d_nm->getSkolemManager();
   d_true = d_nm->mkConst(true);
-  d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0));
-  d_one = d_nm->mkConst(CONST_RATIONAL, Rational(1));
+  d_zero = d_nm->mkConstInt(Rational(0));
+  d_one = d_nm->mkConstInt(Rational(1));
 }
 
 InferInfo InferenceGenerator::nonNegativeCount(Node n, Node e)

diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp
index 9a510c6f5b938ab8e4461e16b9a436c144502f48..6cf26d357df4f28f2e676ae1a54b28f7a491a43e 100644 (file)
--- a/src/theory/bags/normal_form.cpp
+++ b/src/theory/bags/normal_form.cpp
@@ -201,14 +201,10 @@ Node NormalForm::constructConstantBagFromElements(
   }
   TypeNode elementType = t.getBagElementType();
   std::map<Node, Rational>::const_reverse_iterator it = elements.rbegin();
-  Node bag = nm->mkBag(elementType,
-                       it->first,
-                       nm->mkConst<Rational>(CONST_RATIONAL, it->second));
+  Node bag = nm->mkBag(elementType, it->first, nm->mkConstInt(it->second));
   while (++it != elements.rend())
   {
-    Node n = nm->mkBag(elementType,
-                       it->first,
-                       nm->mkConst<Rational>(CONST_RATIONAL, it->second));
+    Node n = nm->mkBag(elementType, it->first, nm->mkConstInt(it->second));
     bag = nm->mkNode(BAG_UNION_DISJOINT, n, bag);
   }
   return bag;
@@ -261,10 +257,10 @@ Node NormalForm::evaluateBagCount(TNode n)
   NodeManager* nm = NodeManager::currentNM();
   if (it != elements.end())
   {
-    Node count = nm->mkConst(CONST_RATIONAL, it->second);
+    Node count = nm->mkConstInt(it->second);
     return count;
   }
-  return nm->mkConst(CONST_RATIONAL, Rational(0));
+  return nm->mkConstInt(Rational(0));
 }
 
 Node NormalForm::evaluateDuplicateRemoval(TNode n)
@@ -592,7 +588,7 @@ Node NormalForm::evaluateCard(TNode n)
   }
 
   NodeManager* nm = NodeManager::currentNM();
-  Node sumNode = nm->mkConst(CONST_RATIONAL, sum);
+  Node sumNode = nm->mkConstInt(sum);
   return sumNode;
 }
 

diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index 61b4ebcbf18280905ff39849d15467380d5fd85a..522f6749c42b82ea6481cd08c6478642bff7cf52 100644 (file)
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -134,7 +134,7 @@ TrustNode TheoryBags::expandChooseOperator(const Node& node,
   Node emptyBag = nm->mkConst(EmptyBag(bagType));
   Node isEmpty = A.eqNode(emptyBag);
   Node count = nm->mkNode(BAG_COUNT, x, A);
-  Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
+  Node one = nm->mkConstInt(Rational(1));
   Node geqOne = nm->mkNode(GEQ, count, one);
   Node geqOneAndEqual = geqOne.andNode(equal);
   Node ite = nm->mkNode(ITE, isEmpty, equal, geqOneAndEqual);

diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp
index 58a1b3291f3672e90dc4655c3ec177e42123c25b..0bfef55d249b2bdf619cd17f57434bf62818ffab 100644 (file)
--- a/src/theory/bags/theory_bags_type_enumerator.cpp
+++ b/src/theory/bags/theory_bags_type_enumerator.cpp
@@ -57,7 +57,7 @@ Node BagEnumerator::operator*()
 BagEnumerator& BagEnumerator::operator++()
 {
   // increase the multiplicity by one
-  Node one = d_nodeManager->mkConst(CONST_RATIONAL, Rational(1));
+  Node one = d_nodeManager->mkConstInt(Rational(1));
   TypeNode elementType = d_elementTypeEnumerator.getType();
   Node singleton = d_nodeManager->mkBag(elementType, d_element, one);
   if (d_currentBag.getKind() == kind::BAG_EMPTY)

diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index 9190f423fbe121352551513e1e7789b6ff3c5587..60ded97b6f98c23d7e20deb61546b9cbaa992ef2 100644 (file)
--- a/src/theory/booleans/proof_circuit_propagator.cpp
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -31,9 +31,9 @@ namespace {
 
 /** Shorthand to create a Node from a constant number */
 template <typename T>
-Node mkRat(T val)
+Node mkInt(T val)
 {
-  return NodeManager::currentNM()->mkConst<Rational>(CONST_RATIONAL, val);
+  return NodeManager::currentNM()->mkConstInt(Rational(val));
 }
 
 /**
@@ -356,7 +356,7 @@ std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::andTrue(
     return nullptr;
   }
   return mkProof(
-      PfRule::AND_ELIM, {assume(d_parent)}, {mkRat(i - d_parent.begin())});
+      PfRule::AND_ELIM, {assume(d_parent)}, {mkInt(i - d_parent.begin())});
 }
 
 std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::orFalse(
@@ -368,7 +368,7 @@ std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::orFalse(
   }
   return mkNot(mkProof(PfRule::NOT_OR_ELIM,
                        {assume(d_parent.notNode())},
-                       {mkRat(i - d_parent.begin())}));
+                       {mkInt(i - d_parent.begin())}));
 }
 
 std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteC(bool c)
@@ -463,7 +463,7 @@ std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::andOneFalse()
   auto it = std::find(d_parent.begin(), d_parent.end(), d_child);
   return mkResolution(
       mkProof(
-          PfRule::CNF_AND_POS, {}, {d_parent, mkRat(it - d_parent.begin())}),
+          PfRule::CNF_AND_POS, {}, {d_parent, mkInt(it - d_parent.begin())}),
       d_child,
       true);
 }
@@ -476,7 +476,7 @@ std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::orOneTrue()
   }
   auto it = std::find(d_parent.begin(), d_parent.end(), d_child);
   return mkNot(mkResolution(
-      mkProof(PfRule::CNF_OR_NEG, {}, {d_parent, mkRat(it - d_parent.begin())}),
+      mkProof(PfRule::CNF_OR_NEG, {}, {d_parent, mkInt(it - d_parent.begin())}),
       d_child,
       false));
 }

diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 9d11b9f7df476af551271bcc3b75161c1b3d422a..1c714b856830067853473cd42a0742e62f2239fe 100644 (file)
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -405,8 +405,8 @@ bool BuiltinProofRuleChecker::getTheoryId(TNode n, TheoryId& tid)
 
 Node BuiltinProofRuleChecker::mkTheoryIdNode(TheoryId tid)
 {
-  return NodeManager::currentNM()->mkConst(
-      CONST_RATIONAL, Rational(static_cast<uint32_t>(tid)));
+  return NodeManager::currentNM()->mkConstInt(
+      Rational(static_cast<uint32_t>(tid)));
 }
 
 }  // namespace builtin

diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
index 60bb0a9bc7d92f211f2bdc44c48b10a3369fce7f..71ce13c69e167928c7565ea6288a8458bc384701 100644 (file)
--- a/src/theory/bv/int_blaster.cpp
+++ b/src/theory/bv/int_blaster.cpp
@@ -59,8 +59,8 @@ IntBlaster::IntBlaster(Env& env,
       d_context(userContext())
 {
   d_nm = NodeManager::currentNM();
-  d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0));
-  d_one = d_nm->mkConst(CONST_RATIONAL, Rational(1));
+  d_zero = d_nm->mkConstInt(0);
+  d_one = d_nm->mkConstInt(1);
 };
 
 IntBlaster::~IntBlaster() {}
@@ -106,18 +106,18 @@ Node IntBlaster::maxInt(uint64_t k)
 {
   Assert(k > 0);
   Rational max_value = intpow2(k) - 1;
-  return d_nm->mkConst(CONST_RATIONAL, max_value);
+  return d_nm->mkConstInt(max_value);
 }
 
 Node IntBlaster::pow2(uint64_t k)
 {
   Assert(k >= 0);
-  return d_nm->mkConst(CONST_RATIONAL, intpow2(k));
+  return d_nm->mkConstInt(intpow2(k));
 }
 
 Node IntBlaster::modpow2(Node n, uint64_t exponent)
 {
-  Node p2 = d_nm->mkConst(CONST_RATIONAL, intpow2(exponent));
+  Node p2 = d_nm->mkConstInt(intpow2(exponent));
   return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, n, p2);
 }
 
@@ -720,7 +720,7 @@ Node IntBlaster::translateNoChildren(Node original,
       BitVector constant(original.getConst<BitVector>());
       Integer c = constant.toInteger();
       Rational r = Rational(c, Integer(1));
-      translation = d_nm->mkConst(CONST_RATIONAL, r);
+      translation = d_nm->mkConstInt(r);
     }
     else
     {

diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index adb067045efb96d6228ab869384a6b18245b1ef8..fd300fe4148d6c502ee349e13eb99b7cdd82f768 100644 (file)
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -467,7 +467,7 @@ Node eliminateBv2Nat(TNode node)
 {
   const unsigned size = utils::getSize(node[0]);
   NodeManager* const nm = NodeManager::currentNM();
-  const Node z = nm->mkConst(CONST_RATIONAL, Rational(0));
+  const Node z = nm->mkConstInt(Rational(0));
   const Node bvone = utils::mkOne(1);
 
   Integer i = 1;
@@ -478,8 +478,8 @@ Node eliminateBv2Nat(TNode node)
         nm->mkNode(kind::EQUAL,
                    nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), node[0]),
                    bvone);
-    children.push_back(nm->mkNode(
-        kind::ITE, cond, nm->mkConst(CONST_RATIONAL, Rational(i)), z));
+    children.push_back(
+        nm->mkNode(kind::ITE, cond, nm->mkConstInt(Rational(i)), z));
   }
   // avoid plus with one child
   return children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children);
@@ -496,11 +496,11 @@ Node eliminateInt2Bv(TNode node)
   Integer i = 2;
   while (v.size() < size)
   {
-    Node cond = nm->mkNode(kind::GEQ,
-                           nm->mkNode(kind::INTS_MODULUS_TOTAL,
-                                      node[0],
-                                      nm->mkConst(CONST_RATIONAL, Rational(i))),
-                           nm->mkConst(CONST_RATIONAL, Rational(i, 2)));
+    Node cond = nm->mkNode(
+        kind::GEQ,
+        nm->mkNode(
+            kind::INTS_MODULUS_TOTAL, node[0], nm->mkConstInt(Rational(i))),
+        nm->mkConstInt(Rational(i, 2)));
     v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero));
     i *= 2;
   }

diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index b475d51e7a22309c3c83997158cec0f992f2f903..196b4f01dfbce5d475b51a22b14fe6aed63566df 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -78,7 +78,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in)
       const DType& dt = utils::datatypeOf(constructor);
       const DTypeConstructor& c = dt[constructorIndex];
       unsigned weight = c.getWeight();
-      children.push_back(nm->mkConst(CONST_RATIONAL, Rational(weight)));
+      children.push_back(nm->mkConstInt(Rational(weight)));
       Node res =
           children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children);
       Trace("datatypes-rewrite")
@@ -104,9 +104,8 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in)
             res = nm->mkConst(false);
             break;
           }
-          children.push_back(nm->mkNode(kind::DT_HEIGHT_BOUND,
-                                        in[0][i],
-                                        nm->mkConst(CONST_RATIONAL, rmo)));
+          children.push_back(
+              nm->mkNode(kind::DT_HEIGHT_BOUND, in[0][i], nm->mkConstInt(rmo)));
         }
       }
       if (res.isNull())

diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index 7ca58905f2d796b6fb5080152f3fc1171a909e93..4ed6e3da94ebd26acb0f715b0ed31557622502df 100644 (file)
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -108,7 +108,7 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
         }
         if (argSuccess)
         {
-          narg = nm->mkConst(CONST_RATIONAL, Rational(i));
+          narg = nm->mkConstInt(Rational(i));
           break;
         }
       }
@@ -141,7 +141,7 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
         if (n >= 0)
         {
           Node t = exp[0];
-          Node nn = nm->mkConst(CONST_RATIONAL, Rational(n));
+          Node nn = nm->mkConstInt(Rational(n));
           Node eq = exp.eqNode(conc);
           cdp->addStep(eq, PfRule::DT_INST, {}, {t, nn});
           cdp->addStep(conc, PfRule::EQ_RESOLVE, {exp, eq}, {});

diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 5324e1c79d4be1d81e5fe5c92b8470d6fb231f8f..ee42add6b2500bce314c984ce44239db4dcbeea7 100644 (file)
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -107,10 +107,10 @@ operator DT_SIZE_BOUND 2 "datatypes height bound"
 typerule DT_SIZE_BOUND ::cvc5::theory::datatypes::DtBoundTypeRule
 
 operator DT_SYGUS_BOUND 2 "datatypes sygus bound"
-typerule DT_SYGUS_BOUND ::cvc5::theory::datatypes::DtSygusBoundTypeRule
+typerule DT_SYGUS_BOUND ::cvc5::theory::datatypes::DtBoundTypeRule
 
 operator DT_SYGUS_EVAL 1: "datatypes sygus evaluation function"
-typerule DT_SYGUS_EVAL ::cvc5::theory::datatypes::DtSyguEvalTypeRule
+typerule DT_SYGUS_EVAL ::cvc5::theory::datatypes::DtSygusEvalTypeRule
 
 
 # Kinds for match terms. For example, the match term

diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 88a3e43d7a7e1dc43e6a9458bd9089f2ab478f6b..90511112c1c5e1d0058d5fb0c55032b7b65c2ad9 100644 (file)
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -57,7 +57,7 @@ SygusExtension::SygusExtension(Env& env,
       d_active_terms(context()),
       d_currTermSize(context())
 {
-  d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+  d_zero = NodeManager::currentNM()->mkConstInt(Rational(0));
   d_true = NodeManager::currentNM()->mkConst(true);
 }
 
@@ -1772,8 +1772,8 @@ Node SygusExtension::SygusSizeDecisionStrategy::getOrMkMeasureValue()
     NodeManager* nm = NodeManager::currentNM();
     SkolemManager* sm = nm->getSkolemManager();
     d_measure_value = sm->mkDummySkolem("mt", nm->integerType());
-    Node mtlem = nm->mkNode(
-        kind::GEQ, d_measure_value, nm->mkConst(CONST_RATIONAL, Rational(0)));
+    Node mtlem =
+        nm->mkNode(kind::GEQ, d_measure_value, nm->mkConstInt(Rational(0)));
     d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS);
   }
   return d_measure_value;
@@ -1787,8 +1787,7 @@ Node SygusExtension::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue(
     NodeManager* nm = NodeManager::currentNM();
     SkolemManager* sm = nm->getSkolemManager();
     Node new_mt = sm->mkDummySkolem("mt", nm->integerType());
-    Node mtlem =
-        nm->mkNode(kind::GEQ, new_mt, nm->mkConst(CONST_RATIONAL, Rational(0)));
+    Node mtlem = nm->mkNode(kind::GEQ, new_mt, nm->mkConstInt(Rational(0)));
     d_measure_value_active = new_mt;
     d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS);
   }
@@ -1817,8 +1816,7 @@ Node SygusExtension::SygusSizeDecisionStrategy::mkLiteral(unsigned s)
   NodeManager* nm = NodeManager::currentNM();
   Trace("sygus-engine") << "******* Sygus : allocate size literal " << s
                         << " for " << d_this << std::endl;
-  return nm->mkNode(
-      DT_SYGUS_BOUND, d_this, nm->mkConst(CONST_RATIONAL, Rational(s)));
+  return nm->mkNode(DT_SYGUS_BOUND, d_this, nm->mkConstInt(Rational(s)));
 }
 
 int SygusExtension::getGuardStatus( Node g ) {

diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp
index 1b5e37bc3e7742765d72a9f57d023b1abf04e67d..4826e87bcecc0c648690d630309d8ecce25248a2 100644 (file)
--- a/src/theory/datatypes/sygus_simple_sym.cpp
+++ b/src/theory/datatypes/sygus_simple_sym.cpp
@@ -245,7 +245,7 @@ bool SygusSimpleSymBreak::considerArgKind(
           rt.d_children[0].d_req_kind = PLUS;
           rt.d_children[0].d_children[0].d_req_type = dt[c].getArgType(1);
           rt.d_children[0].d_children[1].d_req_const =
-              NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
+              NodeManager::currentNM()->mkConstInt(Rational(1));
           rt.d_children[1].d_req_type = dt[c].getArgType(0);
         }
         else if (k == LT || k == GEQ)
@@ -256,7 +256,7 @@ bool SygusSimpleSymBreak::considerArgKind(
           rt.d_children[1].d_req_kind = PLUS;
           rt.d_children[1].d_children[0].d_req_type = dt[c].getArgType(0);
           rt.d_children[1].d_children[1].d_req_const =
-              NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
+              NodeManager::currentNM()->mkConstInt(Rational(1));
         }
       }
       else if (pk == BITVECTOR_NOT)

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 3f11ab1da7bf05e39f2737671df467ae7c6a01f5..3f13886ed1d2adfcf0791160cb52677cc777abc4 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -68,7 +68,7 @@ TheoryDatatypes::TheoryDatatypes(Env& env,
 {
 
   d_true = NodeManager::currentNM()->mkConst( true );
-  d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+  d_zero = NodeManager::currentNM()->mkConstInt(Rational(0));
   d_dtfCounter = 0;
 
   // indicate we are using the default theory state object

diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp
index 78bc67868b3d1e50acae9f6dfcdda7dc270de40f..422af1731ab8582bb2393bfbb6cf3ba1b9f2420c 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_type_rules.cpp
+++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp
@@ -322,10 +322,10 @@ TypeNode DtBoundTypeRule::computeType(NodeManager* nodeManager,
       throw TypeCheckingExceptionPrivate(
           n, "expecting datatype bound term to have datatype argument.");
     }
-    if (n[1].getKind() != kind::CONST_RATIONAL)
+    if (!n[1].isConst() || !n[1].getType().isInteger())
     {
-      throw TypeCheckingExceptionPrivate(n,
-                                         "datatype bound must be a constant");
+      throw TypeCheckingExceptionPrivate(
+          n, "datatype bound must be a constant integer");
     }
     if (n[1].getConst<Rational>().getNumerator().sgn() == -1)
     {
@@ -336,34 +336,9 @@ TypeNode DtBoundTypeRule::computeType(NodeManager* nodeManager,
   return nodeManager->booleanType();
 }
 
-TypeNode DtSygusBoundTypeRule::computeType(NodeManager* nodeManager,
-                                           TNode n,
-                                           bool check)
-{
-  if (check)
-  {
-    if (!n[0].getType().isDatatype())
-    {
-      throw TypeCheckingExceptionPrivate(
-          n, "datatype sygus bound takes a datatype");
-    }
-    if (n[1].getKind() != kind::CONST_RATIONAL)
-    {
-      throw TypeCheckingExceptionPrivate(
-          n, "datatype sygus bound must be a constant");
-    }
-    if (n[1].getConst<Rational>().getNumerator().sgn() == -1)
-    {
-      throw TypeCheckingExceptionPrivate(
-          n, "datatype sygus bound must be non-negative");
-    }
-  }
-  return nodeManager->booleanType();
-}
-
-TypeNode DtSyguEvalTypeRule::computeType(NodeManager* nodeManager,
-                                         TNode n,
-                                         bool check)
+TypeNode DtSygusEvalTypeRule::computeType(NodeManager* nodeManager,
+                                          TNode n,
+                                          bool check)
 {
   TypeNode headType = n[0].getType(check);
   if (!headType.isDatatype())

diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 7cf98aa747e378ff6c9a59cc9cb664e2527f8c7a..3b1276221cda7603022be97d4d8c62c6d98904fb 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -64,12 +64,7 @@ class DtBoundTypeRule {
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
-class DtSygusBoundTypeRule {
- public:
-  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
-};
-
-class DtSyguEvalTypeRule
+class DtSygusEvalTypeRule
 {
  public:
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);

diff --git a/src/theory/difficulty_manager.cpp b/src/theory/difficulty_manager.cpp
index d50d10d9f87cc57e05593c323dc32c61151e3a82..7714abfa98af1ef81a1849bc43a312a6603b516a 100644 (file)
--- a/src/theory/difficulty_manager.cpp
+++ b/src/theory/difficulty_manager.cpp
@@ -44,7 +44,7 @@ void DifficultyManager::getDifficultyMap(std::map<Node, Node>& dmap)
   NodeManager* nm = NodeManager::currentNM();
   for (const std::pair<const Node, uint64_t> p : d_dfmap)
   {
-    dmap[p.first] = nm->mkConst(CONST_RATIONAL, Rational(p.second));
+    dmap[p.first] = nm->mkConstInt(Rational(p.second));
   }
 }
 

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 5a4e8e7bca88272cf948c82c4505e5eb3f2ba697..d4fc32197b4ca984f447ab8559c7e9c8d34fac8a 100644 (file)
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -469,8 +469,8 @@ std::ostream& operator<<(std::ostream& out, InferenceId i)
 
 Node mkInferenceIdNode(InferenceId i)
 {
-  return NodeManager::currentNM()->mkConst(CONST_RATIONAL,
-                                           Rational(static_cast<uint32_t>(i)));
+  return NodeManager::currentNM()->mkConstInt(
+      Rational(static_cast<uint32_t>(i)));
 }
 
 bool getInferenceId(TNode n, InferenceId& i)

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index ec33fe5fd55a029960e9ec9489bd3e830e9e01ca..81ae18f4fa257350c898d82f9706a8d75c6dc8ee 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -163,8 +163,8 @@ void SolvedForm::push_back(Node pv, Node n, TermProperties& pv_prop)
   }
   else
   {
-    Assert(new_theta.getKind() == CONST_RATIONAL);
-    Assert(pv_prop.d_coeff.getKind() == CONST_RATIONAL);
+    Assert(new_theta.isConst());
+    Assert(pv_prop.d_coeff.isConst());
     NodeManager* nm = NodeManager::currentNM();
     new_theta = nm->mkConst(CONST_RATIONAL,
                             Rational(new_theta.getConst<Rational>()
@@ -1165,8 +1165,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
           Node nn = NodeManager::currentNM()->mkNode(
               MULT,
               subs[i],
-              NodeManager::currentNM()->mkConst(
-                  CONST_RATIONAL,
+              NodeManager::currentNM()->mkConstReal(
                   Rational(1) / prop[i].d_coeff.getConst<Rational>()));
           nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn );
           nn = rewrite(nn);
@@ -1214,10 +1213,9 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node
           for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
             Node c_coeff;
             if( !msum_coeff[it->first].isNull() ){
-              c_coeff = rewrite(NodeManager::currentNM()->mkConst(
-                  CONST_RATIONAL,
+              c_coeff = rewrite(NodeManager::currentNM()->mkConstReal(
                   pv_prop.d_coeff.getConst<Rational>()
-                      / msum_coeff[it->first].getConst<Rational>()));
+                  / msum_coeff[it->first].getConst<Rational>()));
             }else{
               c_coeff = pv_prop.d_coeff;
             }
@@ -1283,7 +1281,7 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >&
       }else{
         atom_lhs = nm->mkNode(MINUS, atom[0], atom[1]);
         atom_lhs = rewrite(atom_lhs);
-        atom_rhs = nm->mkConst(CONST_RATIONAL, Rational(0));
+        atom_rhs = nm->mkConstRealOrInt(atom_lhs.getType(), Rational(0));
       }
       //must be an eligible term
       if( isEligible( atom_lhs ) ){

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index e08f892181bd53d64eaac7ae9604ab0036aa3652..2555ff6377ade2bd899582b707f543f436fd5188 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -58,8 +58,8 @@ InstStrategyCegqi::InstStrategyCegqi(Env& env,
       d_added_cbqi_lemma(userContext()),
       d_vtsCache(new VtsTermCache(env, qim)),
       d_bv_invert(nullptr),
-      d_small_const_multiplier(NodeManager::currentNM()->mkConst(
-          CONST_RATIONAL, Rational(1) / Rational(1000000))),
+      d_small_const_multiplier(NodeManager::currentNM()->mkConstReal(
+          Rational(1) / Rational(1000000))),
       d_small_const(d_small_const_multiplier)
 {
   d_check_vts_lemma_lc = false;
@@ -435,6 +435,7 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
     }
     d_curr_quant = Node::null();
   }else if( e==1 ){
+    NodeManager* nm = NodeManager::currentNM();
     //minimize the free delta heuristically on demand
     if( d_check_vts_lemma_lc ){
       Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl;
@@ -453,12 +454,10 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
       d_vtsCache->getVtsTerms(inf, true, false, false);
       for( unsigned i=0; i<inf.size(); i++ ){
         Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
-        Node inf_lem_lb = NodeManager::currentNM()->mkNode(
+        Node inf_lem_lb = nm->mkNode(
             GT,
             inf[i],
-            NodeManager::currentNM()->mkConst(
-                CONST_RATIONAL,
-                Rational(1) / d_small_const.getConst<Rational>()));
+            nm->mkConstReal(Rational(1) / d_small_const.getConst<Rational>()));
         d_qim.lemma(inf_lem_lb, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF);
       }
     }

diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
index f405da34573d73c1a27c9877bb2d9018f08559b3..058b6a8bf301063af21ba8920c81883c0660e7d7 100644 (file)
--- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
@@ -31,7 +31,6 @@ namespace quantifiers {
 VtsTermCache::VtsTermCache(Env& env, QuantifiersInferenceManager& qim)
     : EnvObj(env), d_qim(qim)
 {
-  d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
 }
 
 void VtsTermCache::getVtsTerms(std::vector<Node>& t,
@@ -71,7 +70,8 @@ Node VtsTermCache::getVtsDelta(bool isFree, bool create)
           sm->mkDummySkolem("delta_free",
                             nm->realType(),
                             "free delta for virtual term substitution");
-      Node delta_lem = nm->mkNode(GT, d_vts_delta_free, d_zero);
+      Node zero = nm->mkConstReal(Rational(0));
+      Node delta_lem = nm->mkNode(GT, d_vts_delta_free, zero);
       d_qim.lemma(delta_lem, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA);
     }
     if (d_vts_delta.isNull())
@@ -216,13 +216,17 @@ Node VtsTermCache::rewriteVtsSymbols(Node n)
               {
                 nlit = nm->mkConst(false);
               }
-              else if (res == 1)
-              {
-                nlit = nm->mkNode(GEQ, d_zero, slv);
-              }
               else
               {
-                nlit = nm->mkNode(GT, slv, d_zero);
+                Node zero = nm->mkConstRealOrInt(slv.getType(), Rational(0));
+                if (res == 1)
+                {
+                  nlit = nm->mkNode(GEQ, zero, slv);
+                }
+                else
+                {
+                  nlit = nm->mkNode(GT, slv, zero);
+                }
               }
             }
           }

diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.h b/src/theory/quantifiers/cegqi/vts_term_cache.h
index 60c8f28f3a1ef89594feea336b4a6c6c6ef5db20..7ae16aec8a4a63b9ad52ed3c39b60ca0ffeeb7fa 100644 (file)
--- a/src/theory/quantifiers/cegqi/vts_term_cache.h
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.h
@@ -127,8 +127,6 @@ class VtsTermCache : protected EnvObj
  private:
   /** Reference to the quantifiers inference manager */
   QuantifiersInferenceManager& d_qim;
-  /** constants */
-  Node d_zero;
   /** The virtual term substitution delta */
   Node d_vts_delta;
   /** The virtual term substitution "free delta" */

diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp
index 9933eb6c99c24fc79846a903e654742dde927866..e4d7436c87e5175dc59ba07ec12bda6d7a39de3b 100644 (file)
--- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp
+++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp
@@ -678,8 +678,7 @@ Node PatternTermSelector::getInversion(Node n, Node x)
           Assert(nc.isConst());
           if (x.getType().isInteger())
           {
-            Node coeff =
-                nm->mkConst(CONST_RATIONAL, nc.getConst<Rational>().abs());
+            Node coeff = nm->mkConstInt(nc.getConst<Rational>().abs());
             if (!nc.getConst<Rational>().abs().isOne())
             {
               x = nm->mkNode(INTS_DIVISION_TOTAL, x, coeff);
@@ -691,8 +690,7 @@ Node PatternTermSelector::getInversion(Node n, Node x)
           }
           else
           {
-            Node coeff = nm->mkConst(CONST_RATIONAL,
-                                     Rational(1) / nc.getConst<Rational>());
+            Node coeff = nm->mkConstReal(Rational(1) / nc.getConst<Rational>());
             x = nm->mkNode(MULT, x, coeff);
           }
         }

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 4ed918b43fd9231188b0616d13576ffd746dae02..1152267e8c9681af32f28fca284ac702cfaee7f7 100644 (file)
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -49,7 +49,7 @@ ExtendedRewriter::ExtendedRewriter(Rewriter& rew, bool aggr)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
-  d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+  d_intZero = NodeManager::currentNM()->mkConstInt(Rational(0));
 }
 
 void ExtendedRewriter::setCache(Node n, Node ret) const
@@ -1723,7 +1723,7 @@ Node ExtendedRewriter::extendedRewriteStrings(Node node) const
     strings::ArithEntail aent(&d_rew);
     // (str.substr s x y) --> "" if x < len(s) |= 0 >= y
     Node n1_lt_tot_len = d_rew.rewrite(nm->mkNode(LT, node[1], tot_len));
-    if (aent.checkWithAssumption(n1_lt_tot_len, d_zero, node[2], false))
+    if (aent.checkWithAssumption(n1_lt_tot_len, d_intZero, node[2], false))
     {
       Node ret = strings::Word::mkEmptyWord(node.getType());
       debugExtendedRewrite(node, ret, "SS_START_ENTAILS_ZERO_LEN");
@@ -1731,7 +1731,7 @@ Node ExtendedRewriter::extendedRewriteStrings(Node node) const
     }
 
     // (str.substr s x y) --> "" if 0 < y |= x >= str.len(s)
-    Node non_zero_len = d_rew.rewrite(nm->mkNode(LT, d_zero, node[2]));
+    Node non_zero_len = d_rew.rewrite(nm->mkNode(LT, d_intZero, node[2]));
     if (aent.checkWithAssumption(non_zero_len, node[1], tot_len, false))
     {
       Node ret = strings::Word::mkEmptyWord(node.getType());
@@ -1739,8 +1739,8 @@ Node ExtendedRewriter::extendedRewriteStrings(Node node) const
       return ret;
     }
     // (str.substr s x y) --> "" if x >= 0 |= 0 >= str.len(s)
-    Node geq_zero_start = d_rew.rewrite(nm->mkNode(GEQ, node[1], d_zero));
-    if (aent.checkWithAssumption(geq_zero_start, d_zero, tot_len, false))
+    Node geq_zero_start = d_rew.rewrite(nm->mkNode(GEQ, node[1], d_intZero));
+    if (aent.checkWithAssumption(geq_zero_start, d_intZero, tot_len, false))
     {
       Node ret = strings::Word::mkEmptyWord(node.getType());
       debugExtendedRewrite(node, ret, "SS_GEQ_ZERO_START_ENTAILS_EMP_S");

diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index 1b9d0dae4513575ba617652591ca5713d826b3d0..bf5829e03c46ed02b7ae6dc095b86107e1ff8aea 100644 (file)
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -262,7 +262,7 @@ class ExtendedRewriter
   /** Common constant nodes */
   Node d_true;
   Node d_false;
-  Node d_zero;
+  Node d_intZero;
 };
 
 }  // namespace quantifiers

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index b5b9e7d887ed3f0f07cc0d2b55b1e3318da9c78c..18a63d245c7f3ad1bfd12a7b20d0b14063ff8f36 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -59,7 +59,7 @@ BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic(
 Node BoundedIntegers::IntRangeDecisionHeuristic::mkLiteral(unsigned n)
 {
   NodeManager* nm = NodeManager::currentNM();
-  Node cn = nm->mkConst(CONST_RATIONAL, Rational(n == 0 ? 0 : n - 1));
+  Node cn = nm->mkConstInt(Rational(n == 0 ? 0 : n - 1));
   return nm->mkNode(n == 0 ? LT : LEQ, d_proxy_range, cn);
 }
 
@@ -84,10 +84,9 @@ Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma()
   Node lem = nm->mkNode(
       EQUAL,
       currLit,
-      nm->mkNode(
-          curr == 0 ? LT : LEQ,
-          d_range,
-          nm->mkConst(CONST_RATIONAL, Rational(curr == 0 ? 0 : curr - 1))));
+      nm->mkNode(curr == 0 ? LT : LEQ,
+                 d_range,
+                 nm->mkConstInt(Rational(curr == 0 ? 0 : curr - 1))));
   return lem;
 }
 
@@ -693,8 +692,7 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
       }
       choices.pop_back();
       Node bvl = nm->mkNode(BOUND_VAR_LIST, choice_i);
-      Node cMinCard =
-          nm->mkNode(LEQ, srCardN, nm->mkConst(CONST_RATIONAL, Rational(i)));
+      Node cMinCard = nm->mkNode(LEQ, srCardN, nm->mkConstInt(Rational(i)));
       choice_i = nm->mkNode(WITNESS, bvl, nm->mkNode(OR, cMinCard, cBody));
       d_setm_choice[sro].push_back(choice_i);
     }
@@ -818,8 +816,8 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node
         Node range = rewrite(nm->mkNode(MINUS, u, l));
         // 9999 is an arbitrary range past which we do not do exhaustive
         // bounded instantation, based on the check below.
-        Node ra = rewrite(nm->mkNode(
-            LEQ, range, nm->mkConst(CONST_RATIONAL, Rational(9999))));
+        Node ra =
+            rewrite(nm->mkNode(LEQ, range, nm->mkConstInt(Rational(9999))));
         Node tl = l;
         Node tu = u;
         getBounds( q, v, rsi, tl, tu );
@@ -830,8 +828,7 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node
           Trace("bound-int-rsi")  << "Actual bound range is " << rr << std::endl;
           for (long k = 0; k < rr; k++)
           {
-            Node t =
-                nm->mkNode(PLUS, tl, nm->mkConst(CONST_RATIONAL, Rational(k)));
+            Node t = nm->mkNode(PLUS, tl, nm->mkConstInt(Rational(k)));
             t = rewrite(t);
             elements.push_back( t );
           }

diff --git a/src/theory/quantifiers/quant_bound_inference.cpp b/src/theory/quantifiers/quant_bound_inference.cpp
index af72e2a7c0e1f18fc99adda7bc3c335d9561322f..dfffe64cfdace252403311bcb53ab50e4a394796 100644 (file)
--- a/src/theory/quantifiers/quant_bound_inference.cpp
+++ b/src/theory/quantifiers/quant_bound_inference.cpp
@@ -61,10 +61,9 @@ bool QuantifiersBoundInference::mayComplete(TypeNode tn, unsigned maxCard)
     if (!c.isLargeFinite())
     {
       NodeManager* nm = NodeManager::currentNM();
-      Node card =
-          nm->mkConst(CONST_RATIONAL, Rational(c.getFiniteCardinality()));
+      Node card = nm->mkConstInt(Rational(c.getFiniteCardinality()));
       // check if less than fixed upper bound
-      Node oth = nm->mkConst(CONST_RATIONAL, Rational(maxCard));
+      Node oth = nm->mkConstInt(Rational(maxCard));
       Node eq = nm->mkNode(LEQ, card, oth);
       eq = Rewriter::rewrite(eq);
       mc = eq.isConst() && eq.getConst<bool>();

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 9522a4b9b5d60c7b0ccecf58b814d74d00b7f17c..d39212ddc26d9c478504b74aefef7a01d92ae2b9 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -721,7 +721,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
                   break;
                 }
               }else{
-                Node z = p->getZero( k );
+                Node z = p->getZero(d_vars[index].getType(), k);
                 if( !z.isNull() ){
                   Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl;
                   assigned.push_back( vn );
@@ -744,7 +744,7 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign
           if( slv_v!=-1 ){
             Node lhs;
             if( children.empty() ){
-              lhs = p->getZero( k );
+              lhs = p->getZero(d_vars[index].getType(), k);
             }else if( children.size()==1 ){
               lhs = children[0];
             }else{
@@ -2280,18 +2280,20 @@ QuantConflictFind::Statistics::Statistics()
 {
 }
 
-TNode QuantConflictFind::getZero( Kind k ) {
-  std::map< Kind, Node >::iterator it = d_zero.find( k );
-  if( it==d_zero.end() ){
+TNode QuantConflictFind::getZero(TypeNode tn, Kind k)
+{
+  std::pair<TypeNode, Kind> key(tn, k);
+  std::map<std::pair<TypeNode, Kind>, Node>::iterator it = d_zero.find(key);
+  if (it == d_zero.end())
+  {
     Node nn;
     if( k==PLUS ){
-      nn = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+      nn = NodeManager::currentNM()->mkConstRealOrInt(tn, Rational(0));
     }
-    d_zero[k] = nn;
+    d_zero[key] = nn;
     return nn;
-  }else{
-    return it->second;
   }
+  return it->second;
 }
 
 std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e) {

diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index d14e281fbdb9c9c8f4e6877930e2c54a50ed18e0..82a925d3b76b795c9b25d35444dc4ac80662d2c4 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -195,7 +195,7 @@ class QuantConflictFind : public QuantifiersModule
 
  private:
   context::CDO< bool > d_conflict;
-  std::map< Kind, Node > d_zero;
+  std::map<std::pair<TypeNode, Kind>, Node> d_zero;
   //for storing nodes created during t-constraint solving (prevents memory leaks)
   std::vector< Node > d_tempCache;
   //optimization: list of quantifiers that depend on ground function applications
@@ -209,8 +209,9 @@ private:
 public:  //for ground terms
   Node d_true;
   Node d_false;
-  TNode getZero( Kind k );
-private:
+  TNode getZero(TypeNode tn, Kind k);
+
+ private:
   std::map< Node, QuantInfo > d_qinfo;
 private:  //for equivalence classes
   // type -> list(eqc)

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 2002c73dbb3114cdb282e307ae4d08bf081ad42d..c53809d6eb4b755cee4bd580e91fa28b059bbd50 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -920,7 +920,7 @@ bool QuantifiersRewriter::getVarElimLit(Node body,
       for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++)
       {
         TypeNode tn = tspec[j];
-        Node rn = nm->mkConst(CONST_RATIONAL, Rational(j));
+        Node rn = nm->mkConstInt(Rational(j));
         Node cacheVal = BoundVarManager::getCacheValue(body, lit, rn);
         Node v = bvm->mkBoundVar<QRewDtExpandAttribute>(cacheVal, tn);
         newChildren.push_back(v);

diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index 9f2f9c91c568e4271248c5f73c9edbd4634e2dfb..6399340aa59a1754678f6f3158e7ba226242d8eb 100644 (file)
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -285,11 +285,10 @@ Node Skolemize::mkSkolemizedBody(Node f,
     }
     else if (options::intWfInduction() && tn.isInteger())
     {
-      Node icond = nm->mkNode(GEQ, k, nm->mkConst(CONST_RATIONAL, Rational(0)));
+      Node icond = nm->mkNode(GEQ, k, nm->mkConstInt(Rational(0)));
       Node iret =
-          ret.substitute(
-                 ind_vars[0],
-                 nm->mkNode(MINUS, k, nm->mkConst(CONST_RATIONAL, Rational(1))))
+          ret.substitute(ind_vars[0],
+                         nm->mkNode(MINUS, k, nm->mkConstInt(Rational(1))))
               .negate();
       n_str_ind = nm->mkNode(OR, icond.negate(), iret);
       n_str_ind = nm->mkNode(AND, icond, n_str_ind);

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index be80992eaa0cec7921a0109aa014371f026cb244..c9706b40fb1e0a11398ce090d3fb1786b4121d18 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -480,7 +480,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
       std::set<TypeNode> unresolvedTypes;
       unresolvedTypes.insert(u);
       std::vector<TypeNode> cargsEmpty;
-      Node cr = nm->mkConst(CONST_RATIONAL, Rational(1));
+      Node cr = nm->mkConstInt(Rational(1));
       sdt.addConstructor(cr, "1", cargsEmpty);
       std::vector<TypeNode> cargsPlus;
       cargsPlus.push_back(u);
@@ -503,8 +503,8 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
     if (pow_two > 0)
     {
       Node size_ve = nm->mkNode(DT_SIZE, d_virtual_enum);
-      Node fair_lemma = nm->mkNode(
-          GEQ, size_ve, nm->mkConst(CONST_RATIONAL, Rational(pow_two - 1)));
+      Node fair_lemma =
+          nm->mkNode(GEQ, size_ve, nm->mkConstInt(Rational(pow_two - 1)));
       fair_lemma = nm->mkNode(OR, newLit, fair_lemma);
       Trace("cegis-unif-enum-lemma")
           << "CegisUnifEnum::lemma, fairness size:" << fair_lemma << "\n";

diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index 674183b20cb8f2f709614ca61cce311b576f2636..711d390f83d7ad1e54881df7dab95fc5fb7d98d3 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -257,7 +257,7 @@ void SygusEnumerator::TermCache::initialize(SygusStatistics* s,
         // more aggressive merging of constructor classes. On the negative side,
         // this adds another level of indirection to remember which argument
         // positions the argument types occur in, for each constructor.
-        Node n = nm->mkConst(CONST_RATIONAL, Rational(i));
+        Node n = nm->mkConstInt(Rational(i));
         nToC[n] = i;
         tnit.add(n, argTypes[i]);
       }

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 95d3a5ab5b834bb1558524f0f7c0fa7e0f5636c2..7227b71848473b1a1654701847770e6d3d451712 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -85,11 +85,12 @@ void CegGrammarConstructor::collectTerms(
         Node c = cur;
         if (tn.isRealOrInt())
         {
-          c = nm->mkConst(CONST_RATIONAL, c.getConst<Rational>().abs());
+          c = nm->mkConstRealOrInt(tn, c.getConst<Rational>().abs());
         }
         consts[tn].insert(c);
         if (tn.isInteger())
         {
+          c = nm->mkConstReal(c.getConst<Rational>().abs());
           TypeNode rtype = nm->realType();
           consts[rtype].insert(c);
         }
@@ -410,8 +411,8 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
   NodeManager* nm = NodeManager::currentNM();
   if (type.isRealOrInt())
   {
-    ops.push_back(nm->mkConst(CONST_RATIONAL, Rational(0)));
-    ops.push_back(nm->mkConst(CONST_RATIONAL, Rational(1)));
+    ops.push_back(nm->mkConstRealOrInt(type, Rational(0)));
+    ops.push_back(nm->mkConstRealOrInt(type, Rational(1)));
   }
   else if (type.isBitVector())
   {
@@ -556,7 +557,7 @@ Node CegGrammarConstructor::createLambdaWithZeroArg(
   Assert(bArgType.isRealOrInt() || bArgType.isBitVector());
   if (bArgType.isRealOrInt())
   {
-    zarg = nm->mkConst(CONST_RATIONAL, Rational(0));
+    zarg = nm->mkConstRealOrInt(bArgType, Rational(0));
   }
   else
   {
@@ -800,7 +801,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
         Trace("sygus-grammar-def") << "\t...add for 1 to Pos_Int\n";
         std::vector<TypeNode> cargsEmpty;
         sdts.back().addConstructor(
-            nm->mkConst(CONST_RATIONAL, Rational(1)), "1", cargsEmpty);
+            nm->mkConstInt(Rational(1)), "1", cargsEmpty);
         /* Add operator PLUS */
         Kind kind = PLUS;
         Trace("sygus-grammar-def") << "\t...add for PLUS to Pos_Int\n";
@@ -1150,7 +1151,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     {
       const SygusDatatypeConstructor& sdc = sdti.getConstructor(k);
       Node sop = sdc.d_op;
-      bool isBuiltinArithOp = (sop.getKind() == CONST_RATIONAL);
+      bool isBuiltinArithOp = (sop.getType().isRealOrInt() && sop.isConst());
       bool hasExternalType = false;
       for (unsigned j = 0, nargs = sdc.d_argTypes.size(); j < nargs; j++)
       {

diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 89cee0145264f3394dc61232f02b8f59d1c4bb30..1402c845c47e013e8a2f4ef5f3b394828a40f5ab 100644 (file)
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -589,14 +589,14 @@ Node SygusSampler::getRandomValue(TypeNode tn)
       std::vector<Node> sum;
       for (unsigned j = 0, size = vec.size(); j < size; j++)
       {
-        Node digit = nm->mkConst(CONST_RATIONAL, Rational(vec[j]) * curr);
+        Node digit = nm->mkConstInt(Rational(vec[j]) * curr);
         sum.push_back(digit);
         curr = curr * baser;
       }
       Node ret;
       if (sum.empty())
       {
-        ret = nm->mkConst(CONST_RATIONAL, Rational(0));
+        ret = nm->mkConstInt(Rational(0));
       }
       else if (sum.size() == 1)
       {
@@ -631,7 +631,7 @@ Node SygusSampler::getRandomValue(TypeNode tn)
       }
       else
       {
-        return nm->mkConst(CONST_RATIONAL, sr / rr);
+        return nm->mkConstReal(sr / rr);
       }
     }
   }

diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 1dfcc044ebfa652736d26d6c87c0a3d1ebfce727..18f9ec7e234bf9414622b419facba6ee121861fb 100644 (file)
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -332,7 +332,7 @@ Node TermUtil::mkTypeValue(TypeNode tn, int32_t val)
   if (tn.isRealOrInt())
   {
     Rational c(val);
-    n = NodeManager::currentNM()->mkConst(CONST_RATIONAL, c);
+    n = NodeManager::currentNM()->mkConstRealOrInt(tn, c);
   }
   else if (tn.isBitVector())
   {

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index e2181b4c6d6aa96a94b049d274458da6721f91c7..7bb752acd0db3b87d065e19fb90aae79854abcc5 100644 (file)
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -47,7 +47,7 @@ CardinalityExtension::CardinalityExtension(Env& env,
       d_finite_type_constants_processed(false)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
-  d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+  d_zero = NodeManager::currentNM()->mkConstInt(Rational(0));
 }
 
 void CardinalityExtension::reset()
@@ -134,7 +134,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t)
   if (finiteType)
   {
     Node typeCardinality =
-        nm->mkConst(CONST_RATIONAL, Rational(card.getFiniteCardinality()));
+        nm->mkConstInt(Rational(card.getFiniteCardinality()));
     Node cardUniv = nm->mkNode(kind::SET_CARD, proxy);
     Node leq = nm->mkNode(kind::LEQ, cardUniv, typeCardinality);
 
@@ -980,8 +980,8 @@ void CardinalityExtension::checkMinCard()
     }
     if (!members.empty())
     {
-      Node conc = nm->mkNode(
-          GEQ, cardTerm, nm->mkConst(CONST_RATIONAL, Rational(members.size())));
+      Node conc =
+          nm->mkNode(GEQ, cardTerm, nm->mkConstInt(Rational(members.size())));
       Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
       d_im.assertInference(conc, InferenceId::SETS_CARD_MINIMAL, expn, 1);
     }

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index f065802920e88f54552b463a596f3eed016e6469..a08c051f664d8433e05fab5b8c6b36687848b339 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -59,7 +59,7 @@ TheorySetsPrivate::TheorySetsPrivate(Env& env,
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
-  d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+  d_zero = NodeManager::currentNM()->mkConstInt(Rational(0));
 }
 
 TheorySetsPrivate::~TheorySetsPrivate()
@@ -1289,7 +1289,7 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
     case kind::RELATION_JOIN_IMAGE:
     {
       // these are logic exceptions, not type checking exceptions
-      if (node[1].getKind() != kind::CONST_RATIONAL)
+      if (!node[1].isConst())
       {
         throw LogicException(
             "JoinImage cardinality constraint must be a constant");

diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index d603946c48d317f30c7cbd442afc42dc99351f86..cb9b2673185fd256f341d01a10b9a28066ae3fdb 100644 (file)
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -272,13 +272,12 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
   {
     if(node[0].isConst()) {
       std::set<Node> elements = NormalForm::getElementsFromNormalConstant(node[0]);
-      return RewriteResponse(
-          REWRITE_DONE, nm->mkConst(CONST_RATIONAL, Rational(elements.size())));
+      return RewriteResponse(REWRITE_DONE,
+                             nm->mkConstInt(Rational(elements.size())));
     }
     else if (node[0].getKind() == kind::SET_SINGLETON)
     {
-      return RewriteResponse(REWRITE_DONE,
-                             nm->mkConst(CONST_RATIONAL, Rational(1)));
+      return RewriteResponse(REWRITE_DONE, nm->mkConstInt(Rational(1)));
     }
     else if (node[0].getKind() == kind::SET_UNION)
     {

diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp
index 8eaa503541e87546ab2bf79c79eed6fbed58fd59..19f1bc97df52bdc8e69cb1963c6f1ffe50428f1d 100644 (file)
--- a/src/theory/strings/arith_entail.cpp
+++ b/src/theory/strings/arith_entail.cpp
@@ -32,7 +32,7 @@ namespace strings {
 
 ArithEntail::ArithEntail(Rewriter* r) : d_rr(r)
 {
-  d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+  d_zero = NodeManager::currentNM()->mkConstInt(Rational(0));
 }
 
 Node ArithEntail::rewrite(Node a) { return d_rr->rewrite(a); }
@@ -76,11 +76,10 @@ bool ArithEntail::check(Node a, bool strict)
     return a.getConst<Rational>().sgn() >= (strict ? 1 : 0);
   }
 
-  Node ar = strict ? NodeManager::currentNM()->mkNode(
-                kind::MINUS,
-                a,
-                NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1)))
-                   : a;
+  Node ar =
+      strict ? NodeManager::currentNM()->mkNode(
+          kind::MINUS, a, NodeManager::currentNM()->mkConstInt(Rational(1)))
+             : a;
   ar = d_rr->rewrite(ar);
 
   if (ar.getAttribute(StrCheckEntailArithComputedAttr()))
@@ -133,7 +132,7 @@ bool ArithEntail::checkApprox(Node ar)
         << "Get approximations " << v << "..." << std::endl;
     if (v.isNull())
     {
-      Node mn = c.isNull() ? nm->mkConst(CONST_RATIONAL, Rational(1)) : c;
+      Node mn = c.isNull() ? nm->mkConstInt(Rational(1)) : c;
       aarSum.push_back(mn);
     }
     else
@@ -496,8 +495,8 @@ void ArithEntail::getArithApproximations(Node a,
           {
             // x >= 0 implies
             //   x+1 >= len( int.to.str( x ) )
-            approx.push_back(nm->mkNode(
-                PLUS, nm->mkConst(CONST_RATIONAL, Rational(1)), a[0][0]));
+            approx.push_back(
+                nm->mkNode(PLUS, nm->mkConstInt(Rational(1)), a[0][0]));
           }
         }
       }
@@ -507,7 +506,7 @@ void ArithEntail::getArithApproximations(Node a,
         {
           // x >= 0 implies
           //   len( int.to.str( x ) ) >= 1
-          approx.push_back(nm->mkConst(CONST_RATIONAL, Rational(1)));
+          approx.push_back(nm->mkConstInt(Rational(1)));
         }
         // other crazy things are possible here, e.g.
         // len( int.to.str( len( y ) + 10 ) ) >= 2
@@ -541,7 +540,7 @@ void ArithEntail::getArithApproximations(Node a,
       // ...hard to test, runs risk of non-termination
 
       // -1 <= indexof( x, y, n )
-      approx.push_back(nm->mkConst(CONST_RATIONAL, Rational(-1)));
+      approx.push_back(nm->mkConstInt(Rational(-1)));
     }
   }
   else if (ak == STRING_STOI)
@@ -556,7 +555,7 @@ void ArithEntail::getArithApproximations(Node a,
     else
     {
       // -1 <= str.to.int( x )
-      approx.push_back(nm->mkConst(CONST_RATIONAL, Rational(-1)));
+      approx.push_back(nm->mkConstInt(Rational(-1)));
     }
   }
   Trace("strings-ent-approx-debug") << "Return " << approx.size() << std::endl;
@@ -661,9 +660,8 @@ bool ArithEntail::checkWithAssumption(Node assumption,
       // (not (>= s t)) --> (>= (t - 1) s)
       Assert(assumption.getKind() == kind::NOT
              && assumption[0].getKind() == kind::GEQ);
-      x = nm->mkNode(kind::MINUS,
-                     assumption[0][1],
-                     nm->mkConst(CONST_RATIONAL, Rational(1)));
+      x = nm->mkNode(
+          kind::MINUS, assumption[0][1], nm->mkConstInt(Rational(1)));
       y = assumption[0][0];
     }
 
@@ -866,7 +864,7 @@ Node ArithEntail::getConstantBoundLength(TNode s, bool isLower) const
   if (s.isConst())
   {
     size_t len = Word::getLength(s);
-    ret = nm->mkConst(CONST_RATIONAL, Rational(len));
+    ret = nm->mkConstInt(Rational(len));
   }
   else if (s.getKind() == STRING_CONCAT)
   {
@@ -885,12 +883,12 @@ Node ArithEntail::getConstantBoundLength(TNode s, bool isLower) const
         success = false;
         break;
       }
-      Assert(b.getKind() == CONST_RATIONAL);
+      Assert(b.isConst());
       sum = sum + b.getConst<Rational>();
     }
     if (success && (!isLower || sum.sgn() != 0))
     {
-      ret = nm->mkConst(CONST_RATIONAL, sum);
+      ret = nm->mkConstInt(sum);
     }
   }
   if (ret.isNull() && isLower)

diff --git a/src/theory/strings/array_solver.cpp b/src/theory/strings/array_solver.cpp
index 65ff4cde461d1d8f498789d69be61f55a7fcd992..c04bfe9184c3865a2b86a9035a3f0acbcdb09f7c 100644 (file)
--- a/src/theory/strings/array_solver.cpp
+++ b/src/theory/strings/array_solver.cpp
@@ -44,7 +44,7 @@ ArraySolver::ArraySolver(Env& env,
       d_eqProc(context())
 {
   NodeManager* nm = NodeManager::currentNM();
-  d_zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+  d_zero = nm->mkConstInt(Rational(0));
 }
 
 ArraySolver::~ArraySolver() {}

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 69d50a7d98ef0b8ff4527dacdb1d540b82b23758..2d25a0d1eeb6270143c75efd8548e8f7a3ed2947 100644 (file)
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -604,8 +604,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn,
     if (lr.isConst())
     {
       // if constant, compare
-      Node cmp =
-          nm->mkNode(GEQ, lr, nm->mkConst(CONST_RATIONAL, Rational(card_need)));
+      Node cmp = nm->mkNode(GEQ, lr, nm->mkConstInt(Rational(card_need)));
       cmp = rewrite(cmp);
       needsSplit = !cmp.getConst<bool>();
     }
@@ -619,7 +618,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn,
       bool success = true;
       while (r < card_need && success)
       {
-        Node rr = nm->mkConst(CONST_RATIONAL, Rational(r));
+        Node rr = nm->mkConstInt(Rational(r));
         if (d_state.areDisequal(rr, lr))
         {
           r++;
@@ -669,7 +668,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn,
                           << std::endl;
     if (int_k + 1 > ei->d_cardinalityLemK.get())
     {
-      Node k_node = nm->mkConst(CONST_RATIONAL, Rational(int_k));
+      Node k_node = nm->mkConstInt(Rational(int_k));
       // add cardinality lemma
       Node dist = nm->mkNode(DISTINCT, cols[i]);
       std::vector<Node> expn;

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 46f75bd10c724db24738112e3259e1fdfa70d646..ab214c9ceaceee8daaca4bf3ce74ee224beeaa5b 100644 (file)
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -50,9 +50,9 @@ CoreSolver::CoreSolver(Env& env,
       d_nfPairs(context()),
       d_extDeq(userContext())
 {
-  d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
-  d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
-  d_neg_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(-1));
+  d_zero = NodeManager::currentNM()->mkConstInt(Rational(0));
+  d_one = NodeManager::currentNM()->mkConstInt(Rational(1));
+  d_neg_one = NodeManager::currentNM()->mkConstInt(Rational(-1));
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
 }
@@ -776,12 +776,12 @@ Node CoreSolver::getConclusion(Node x,
     {
       // we can assume its length is greater than zero
       Node emp = Word::mkEmptyWord(sk1.getType());
-      conc = nm->mkNode(AND,
-                        conc,
-                        sk1.eqNode(emp).negate(),
-                        nm->mkNode(GT,
-                                   nm->mkNode(STRING_LENGTH, sk1),
-                                   nm->mkConst(CONST_RATIONAL, Rational(0))));
+      conc = nm->mkNode(
+          AND,
+          conc,
+          sk1.eqNode(emp).negate(),
+          nm->mkNode(
+              GT, nm->mkNode(STRING_LENGTH, sk1), nm->mkConstInt(Rational(0))));
     }
   }
   else if (rule == PfRule::CONCAT_CSPLIT)

diff --git a/src/theory/strings/eager_solver.cpp b/src/theory/strings/eager_solver.cpp
index ac8e815df64a2d414f0588430787f6fa244b75d7..0e5c1965825bed4db1fce07b17611fa2616b5207 100644 (file)
--- a/src/theory/strings/eager_solver.cpp
+++ b/src/theory/strings/eager_solver.cpp
@@ -227,7 +227,7 @@ bool EagerSolver::addArithmeticBound(EqcInfo* e, Node t, bool isLower)
   Assert(e != nullptr);
   Assert(!t.isNull());
   Node tb = t.isConst() ? t : getBoundForLength(t, isLower);
-  Assert(!tb.isNull() && tb.getKind() == CONST_RATIONAL)
+  Assert(!tb.isNull() && tb.isConst() && tb.getType().isInteger())
       << "Unexpected bound " << tb << " from " << t;
   Rational br = tb.getConst<Rational>();
   Node prev = isLower ? e->d_firstBound : e->d_secondBound;
@@ -236,7 +236,7 @@ bool EagerSolver::addArithmeticBound(EqcInfo* e, Node t, bool isLower)
   {
     // convert to bound
     Node prevb = prev.isConst() ? prev : getBoundForLength(prev, isLower);
-    Assert(!prevb.isNull() && prevb.getKind() == CONST_RATIONAL);
+    Assert(!prevb.isNull() && prevb.isConst() && prevb.getType().isInteger());
     Rational prevbr = prevb.getConst<Rational>();
     if (prevbr == br || (br < prevbr) == isLower)
     {
@@ -251,7 +251,8 @@ bool EagerSolver::addArithmeticBound(EqcInfo* e, Node t, bool isLower)
   {
     // are we in conflict?
     Node prevob = prevo.isConst() ? prevo : getBoundForLength(prevo, !isLower);
-    Assert(!prevob.isNull() && prevob.getKind() == CONST_RATIONAL);
+    Assert(!prevob.isNull() && prevob.isConst()
+           && prevob.getType().isInteger());
     Rational prevobr = prevob.getConst<Rational>();
     if (prevobr != br && (prevobr < br) == isLower)
     {

diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index edfb91c64686cc829a8a697931a916d94f76ef9d..81da5006277c4dd349da0f8586b6fae6a540fa2f 100644 (file)
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -499,7 +499,7 @@ void InferProofCons::convert(InferenceId infer,
         {
           // it should be the case that lenConstraint => lenReq
           lenReq = nm->mkNode(STRING_LENGTH, t0)
-                       .eqNode(nm->mkConst(CONST_RATIONAL, Rational(0)))
+                       .eqNode(nm->mkConstInt(Rational(0)))
                        .notNode();
           lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
           rule = PfRule::CONCAT_CSPLIT;
@@ -530,7 +530,7 @@ void InferProofCons::convert(InferenceId infer,
         {
           // it should be the case that lenConstraint => lenReq
           lenReq = nm->mkNode(STRING_LENGTH, t0)
-                       .eqNode(nm->mkConst(CONST_RATIONAL, Rational(0)))
+                       .eqNode(nm->mkConstInt(Rational(0)))
                        .notNode();
           lenSuccess = convertLengthPf(lenReq, lenConstraint, psb);
           rule = PfRule::CONCAT_CPROP;
@@ -837,7 +837,7 @@ void InferProofCons::convert(InferenceId infer,
             std::vector<Node> childrenAE;
             childrenAE.push_back(eunf);
             std::vector<Node> argsAE;
-            argsAE.push_back(nm->mkConst(CONST_RATIONAL, Rational(0)));
+            argsAE.push_back(nm->mkConstInt(Rational(0)));
             Node eunfAE = psb.tryStep(PfRule::AND_ELIM, childrenAE, argsAE);
             Trace("strings-ipc-prefix")
                 << "--- and elim to " << eunfAE << std::endl;

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 5247e222d4ed9e6227abaae0b908438cbba23dc9..c7020869ff9c476dcd99a832b8f4fb1ead4f5774 100644 (file)
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -51,8 +51,8 @@ InferenceManager::InferenceManager(Env& env,
                  : nullptr)
 {
   NodeManager* nm = NodeManager::currentNM();
-  d_zero = nm->mkConst(CONST_RATIONAL, Rational(0));
-  d_one = nm->mkConst(CONST_RATIONAL, Rational(1));
+  d_zero = nm->mkConstInt(Rational(0));
+  d_one = nm->mkConstInt(Rational(1));
   d_true = nm->mkConst(true);
   d_false = nm->mkConst(false);
 }

diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index edb38e70266088994f751d684aa2784f27c882eb..dc01bb6d7ca0f3e736a45e96e65ad3c991168487 100644 (file)
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -212,8 +212,8 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
     else if (id == PfRule::CONCAT_CSPLIT)
     {
       Assert(children.size() == 2);
-      Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
-      Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
+      Node zero = nm->mkConstInt(Rational(0));
+      Node one = nm->mkConstInt(Rational(1));
       if (children[1].getKind() != NOT || children[1][0].getKind() != EQUAL
           || children[1][0][0].getKind() != STRING_LENGTH
           || children[1][0][0][0] != t0 || children[1][0][1] != zero)
@@ -240,7 +240,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
     else if (id == PfRule::CONCAT_CPROP)
     {
       Assert(children.size() == 2);
-      Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+      Node zero = nm->mkConstInt(Rational(0));
 
       Trace("pfcheck-strings-cprop")
           << "CONCAT_PROP, isRev=" << isRev << std::endl;
@@ -352,7 +352,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
     {
       return Node::null();
     }
-    Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+    Node zero = nm->mkConstInt(Rational(0));
     Node clen = nm->mkNode(STRING_LENGTH, nemp[0][0]);
     return clen.eqNode(zero).notNode();
   }
@@ -462,7 +462,7 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
            && args[1].getType().isStringLike());
     Node c1 = nm->mkNode(STRING_TO_CODE, args[0]);
     Node c2 = nm->mkNode(STRING_TO_CODE, args[1]);
-    Node eqNegOne = c1.eqNode(nm->mkConst(CONST_RATIONAL, Rational(-1)));
+    Node eqNegOne = c1.eqNode(nm->mkConstInt(Rational(-1)));
     Node deq = c1.eqNode(c2).negate();
     Node eqn = args[0].eqNode(args[1]);
     return nm->mkNode(kind::OR, eqNegOne, deq, eqn);

diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index 8a96e22d2f0bc658c87b2933c87c6a1432f6c639..477533beeeeb7595bf193fe7335fc3c39aa69d8d 100644 (file)
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -98,7 +98,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
   Node x = atom[0];
   Node lenx = nm->mkNode(STRING_LENGTH, x);
   Node re = atom[1];
-  Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+  Node zero = nm->mkConstInt(Rational(0));
   std::vector<Node> children;
   utils::getConcat(re, children);
 
@@ -252,10 +252,8 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
       if (gap_minsize[i] > 0)
       {
         // the gap to this child is at least gap_minsize[i]
-        prev_end =
-            nm->mkNode(PLUS,
-                       prev_end,
-                       nm->mkConst(CONST_RATIONAL, Rational(gap_minsize[i])));
+        prev_end = nm->mkNode(
+            PLUS, prev_end, nm->mkConstInt(Rational(gap_minsize[i])));
       }
       prev_ends.push_back(prev_end);
       Node sc = sep_children[i];
@@ -280,8 +278,8 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
           }
           // if the gap after this one is strict, we need a non-greedy find
           // thus, we add a symbolic constant
-          Node cacheVal = BoundVarManager::getCacheValue(
-              atom, nm->mkConst(CONST_RATIONAL, Rational(i)));
+          Node cacheVal =
+              BoundVarManager::getCacheValue(atom, nm->mkConstInt(Rational(i)));
           TypeNode intType = nm->integerType();
           Node k =
               bvm->mkBoundVar<ReElimConcatIndexAttribute>(cacheVal, intType);
@@ -289,8 +287,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
           prev_end = nm->mkNode(PLUS, prev_end, k);
         }
         Node curr = nm->mkNode(STRING_INDEXOF, x, sc, prev_end);
-        Node idofFind =
-            curr.eqNode(nm->mkConst(CONST_RATIONAL, Rational(-1))).negate();
+        Node idofFind = curr.eqNode(nm->mkConstInt(Rational(-1))).negate();
         conj.push_back(idofFind);
         prev_end = nm->mkNode(PLUS, curr, lensc);
       }
@@ -305,7 +302,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
       // then the last indexof/substr constraint entails the following
       // constraint, so it is not necessary to add.
       // Below, we may write "A" for (str.to.re "A") and _ for re.allchar:
-      Node cEnd = nm->mkConst(CONST_RATIONAL, Rational(gap_minsize_end));
+      Node cEnd = nm->mkConstInt(Rational(gap_minsize_end));
       if (gap_exact_end)
       {
         Assert(!sep_children.empty());
@@ -477,8 +474,8 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
       }
       else
       {
-        Node cacheVal = BoundVarManager::getCacheValue(
-            atom, nm->mkConst(CONST_RATIONAL, Rational(i)));
+        Node cacheVal =
+            BoundVarManager::getCacheValue(atom, nm->mkConstInt(Rational(i)));
         TypeNode intType = nm->integerType();
         k = bvm->mkBoundVar<ReElimConcatIndexAttribute>(cacheVal, intType);
         Node bound =
@@ -541,7 +538,7 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg)
   Node x = atom[0];
   Node lenx = nm->mkNode(STRING_LENGTH, x);
   Node re = atom[1];
-  Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+  Node zero = nm->mkConstInt(Rational(0));
   // for regular expression star,
   // if the period is a fixed constant, we can turn it into a bounded
   // quantifier
@@ -561,8 +558,8 @@ Node RegExpElimination::eliminateStar(Node atom, bool isAgg)
   std::vector<Node> char_constraints;
   TypeNode intType = nm->integerType();
   Node index = bvm->mkBoundVar<ReElimStarIndexAttribute>(atom, intType);
-  Node substr_ch = nm->mkNode(
-      STRING_SUBSTR, x, index, nm->mkConst(CONST_RATIONAL, Rational(1)));
+  Node substr_ch =
+      nm->mkNode(STRING_SUBSTR, x, index, nm->mkConstInt(Rational(1)));
   substr_ch = Rewriter::rewrite(substr_ch);
   // handle the case where it is purely characters
   for (const Node& r : disj)

diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp
index 645dc05cd36ce7dabbddc050519fbc50d2fa15b6..4c4540366cb1c0f34d4f183c6bb5c50c20481b30 100644 (file)
--- a/src/theory/strings/regexp_entail.cpp
+++ b/src/theory/strings/regexp_entail.cpp
@@ -584,7 +584,7 @@ bool RegExpEntail::testConstStringInRegExp(cvc5::String& s,
               }
               else
               {
-                Node num2 = nm->mkConst(CONST_RATIONAL, cvc5::Rational(u - 1));
+                Node num2 = nm->mkConstInt(cvc5::Rational(u - 1));
                 Node r2 = nm->mkNode(REGEXP_LOOP, r[0], r[1], num2);
                 if (testConstStringInRegExp(s, index_start + len, r2))
                 {
@@ -616,7 +616,7 @@ bool RegExpEntail::testConstStringInRegExp(cvc5::String& s,
             cvc5::String t = s.substr(index_start, len);
             if (testConstStringInRegExp(t, 0, r[0]))
             {
-              Node num2 = nm->mkConst(CONST_RATIONAL, cvc5::Rational(l - 1));
+              Node num2 = nm->mkConstInt(cvc5::Rational(l - 1));
               Node r2 = nm->mkNode(REGEXP_LOOP, r[0], num2, num2);
               if (testConstStringInRegExp(s, index_start + len, r2))
               {
@@ -668,7 +668,7 @@ Node RegExpEntail::getFixedLengthForRegexp(TNode n)
   }
   else if (k == REGEXP_ALLCHAR || k == REGEXP_RANGE)
   {
-    return nm->mkConst(CONST_RATIONAL, Rational(1));
+    return nm->mkConstInt(Rational(1));
   }
   else if (k == REGEXP_UNION || k == REGEXP_INTER)
   {

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index a7ba37b183d8b8a2fa658ecb72696b806457b219..eb6d2d3551dd50529692df7a2422538bd3933fa2 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -37,10 +37,8 @@ RegExpOpr::RegExpOpr(Env& env, SkolemCache* sc)
       d_false(NodeManager::currentNM()->mkConst(false)),
       d_emptyRegexp(NodeManager::currentNM()->mkNode(kind::REGEXP_NONE,
                                                      std::vector<Node>{})),
-      d_zero(NodeManager::currentNM()->mkConst(CONST_RATIONAL,
-                                               ::cvc5::Rational(0))),
-      d_one(NodeManager::currentNM()->mkConst(CONST_RATIONAL,
-                                              ::cvc5::Rational(1))),
+      d_zero(NodeManager::currentNM()->mkConstInt(Rational(0))),
+      d_one(NodeManager::currentNM()->mkConstInt(Rational(1))),
       d_sigma(NodeManager::currentNM()->mkNode(kind::REGEXP_ALLCHAR,
                                                std::vector<Node>{})),
       d_sigma_star(
@@ -911,7 +909,7 @@ Node RegExpOpr::reduceRegExpNeg(Node mem)
   Node r = mem[0][1];
   NodeManager* nm = NodeManager::currentNM();
   Kind k = r.getKind();
-  Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+  Node zero = nm->mkConstInt(Rational(0));
   Node conc;
   if (k == REGEXP_CONCAT)
   {
@@ -955,7 +953,7 @@ Node RegExpOpr::reduceRegExpNegConcatFixed(Node mem, Node reLen, size_t index)
   Node r = mem[0][1];
   NodeManager* nm = NodeManager::currentNM();
   Assert(r.getKind() == REGEXP_CONCAT);
-  Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+  Node zero = nm->mkConstInt(Rational(0));
   // The following simplification states that
   //    ~( s in R1 ++ R2 ++... ++ Rn )
   // is equivalent to
@@ -1040,7 +1038,7 @@ Node RegExpOpr::reduceRegExpPos(Node mem,
       }
       else
       {
-        Node ivalue = nm->mkConst(CONST_RATIONAL, Rational(i));
+        Node ivalue = nm->mkConstInt(Rational(i));
         Node sk = sm->mkSkolemFunction(SkolemFunId::RE_UNFOLD_POS_COMPONENT,
                                        s.getType(),
                                        {mem[0], mem[1], ivalue});
@@ -1321,10 +1319,8 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node >
             rt = itr2->second;
           } else {
             std::map< PairNodes, Node > cache2(cache);
-            cache2[p] = NodeManager::currentNM()->mkNode(
-                kind::REGEXP_RV,
-                NodeManager::currentNM()->mkConst(CONST_RATIONAL,
-                                                  cvc5::Rational(cnt)));
+            cache2[p] =
+                nm->mkNode(kind::REGEXP_RV, nm->mkConstInt(Rational(cnt)));
             rt = intersectInternal(r1l, r2l, cache2, cnt+1);
             cacheX[ pp ] = rt;
           }

diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 1d82f9abd2bd5de8177627d815685d413501b8b1..7670c0b70439f6635fd8b7cc876a5ae3ead12716 100644 (file)
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -352,7 +352,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
       }
       else if (ne.getKind() == STRING_SUBSTR)
       {
-        Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+        Node zero = nm->mkConstInt(Rational(0));
 
         if (d_arithEntail.check(ne[1], false)
             && d_arithEntail.check(ne[2], true))
@@ -586,8 +586,7 @@ Node SequencesRewriter::rewriteLength(Node node)
   Kind nk0 = node[0].getKind();
   if (node[0].isConst())
   {
-    Node retNode =
-        nm->mkConst(CONST_RATIONAL, Rational(Word::getLength(node[0])));
+    Node retNode = nm->mkConstInt(Rational(Word::getLength(node[0])));
     return returnRewrite(node, retNode, Rewrite::LEN_EVAL);
   }
   else if (nk0 == kind::STRING_CONCAT)
@@ -600,8 +599,8 @@ Node SequencesRewriter::rewriteLength(Node node)
       {
         if (tmpNode[i].isConst())
         {
-          node_vec.push_back(nm->mkConst(
-              CONST_RATIONAL, Rational(Word::getLength(tmpNode[i]))));
+          node_vec.push_back(
+              nm->mkConstInt(Rational(Word::getLength(tmpNode[i]))));
         }
         else
         {
@@ -634,7 +633,7 @@ Node SequencesRewriter::rewriteLength(Node node)
   }
   else if (nk0 == SEQ_UNIT)
   {
-    Node retNode = nm->mkConst(CONST_RATIONAL, Rational(1));
+    Node retNode = nm->mkConstInt(Rational(1));
     return returnRewrite(node, retNode, Rewrite::LEN_SEQ_UNIT);
   }
   return node;
@@ -1311,7 +1310,7 @@ Node SequencesRewriter::rewriteMembership(TNode node)
   }
   else if (r.getKind() == kind::REGEXP_ALLCHAR)
   {
-    Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
+    Node one = nm->mkConstInt(Rational(1));
     Node retNode = one.eqNode(nm->mkNode(STRING_LENGTH, x));
     return returnRewrite(node, retNode, Rewrite::RE_IN_SIGMA);
   }
@@ -1344,7 +1343,7 @@ Node SequencesRewriter::rewriteMembership(TNode node)
       Node flr = RegExpEntail::getFixedLengthForRegexp(r[0]);
       if (!flr.isNull())
       {
-        Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
+        Node one = nm->mkConstInt(Rational(1));
         if (flr == one)
         {
           NodeBuilder nb(AND);
@@ -1430,7 +1429,7 @@ Node SequencesRewriter::rewriteMembership(TNode node)
       if (constStr.isNull())
       {
         // x in re.++(_*, _, _) ---> str.len(x) >= 2
-        Node num = nm->mkConst(CONST_RATIONAL, Rational(allSigmaMinSize));
+        Node num = nm->mkConstInt(Rational(allSigmaMinSize));
         Node lenx = nm->mkNode(STRING_LENGTH, x);
         Node retNode = nm->mkNode(allSigmaStrict ? EQUAL : GEQ, lenx, num);
         return returnRewrite(node, retNode, Rewrite::RE_CONCAT_PURE_ALLCHAR);
@@ -1722,10 +1721,9 @@ TrustNode SequencesRewriter::expandDefinition(Node node)
     Node s = node[0];
     Node n = node[1];
     // seq.nth(s, n) --> ite(0 <= n < len(s), seq.nth_total(s,n), Uf(s, n))
-    Node cond =
-        nm->mkNode(AND,
-                   nm->mkNode(LEQ, nm->mkConst(CONST_RATIONAL, Rational(0)), n),
-                   nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s)));
+    Node cond = nm->mkNode(AND,
+                           nm->mkNode(LEQ, nm->mkConstInt(Rational(0)), n),
+                           nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s)));
     Node ss = nm->mkNode(SEQ_NTH_TOTAL, s, n);
     Node uf = SkolemCache::mkSkolemSeqNth(s.getType(), "Uf");
     Node u = nm->mkNode(APPLY_UF, uf, s, n);
@@ -1776,7 +1774,7 @@ Node SequencesRewriter::rewriteCharAt(Node node)
 {
   Assert(node.getKind() == STRING_CHARAT);
   NodeManager* nm = NodeManager::currentNM();
-  Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
+  Node one = nm->mkConstInt(Rational(1));
   Node retNode = nm->mkNode(STRING_SUBSTR, node[0], node[1], one);
   return returnRewrite(node, retNode, Rewrite::CHARAT_ELIM);
 }
@@ -1854,7 +1852,7 @@ Node SequencesRewriter::rewriteSubstr(Node node)
       }
     }
   }
-  Node zero = nm->mkConst(CONST_RATIONAL, cvc5::Rational(0));
+  Node zero = nm->mkConstInt(cvc5::Rational(0));
 
   // if entailed non-positive length or negative start point
   if (d_arithEntail.check(zero, node[1], true))
@@ -2453,7 +2451,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
   if (node[2].isConst() && node[2].getConst<Rational>().sgn() < 0)
   {
     // z<0  implies  str.indexof( x, y, z ) --> -1
-    Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1));
+    Node negone = nm->mkConstInt(Rational(-1));
     return returnRewrite(node, negone, Rewrite::IDOF_NEG);
   }
 
@@ -2471,7 +2469,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
       // We know that, due to limitations on the size of string constants
       // in our implementation, that accessing a position greater than
       // rMaxInt is guaranteed to be out of bounds.
-      Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1));
+      Node negone = nm->mkConstInt(Rational(-1));
       return returnRewrite(node, negone, Rewrite::IDOF_MAX);
     }
     Assert(node[2].getConst<Rational>().sgn() >= 0);
@@ -2482,13 +2480,12 @@ Node SequencesRewriter::rewriteIndexof(Node node)
     std::size_t ret = Word::find(s, t, start);
     if (ret != std::string::npos)
     {
-      Node retv =
-          nm->mkConst(CONST_RATIONAL, Rational(static_cast<unsigned>(ret)));
+      Node retv = nm->mkConstInt(Rational(static_cast<unsigned>(ret)));
       return returnRewrite(node, retv, Rewrite::IDOF_FIND);
     }
     else if (children0.size() == 1)
     {
-      Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1));
+      Node negone = nm->mkConstInt(Rational(-1));
       return returnRewrite(node, negone, Rewrite::IDOF_NFIND);
     }
   }
@@ -2500,14 +2497,14 @@ Node SequencesRewriter::rewriteIndexof(Node node)
       if (node[2].getConst<Rational>().sgn() == 0)
       {
         // indexof( x, x, 0 ) --> 0
-        Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+        Node zero = nm->mkConstInt(Rational(0));
         return returnRewrite(node, zero, Rewrite::IDOF_EQ_CST_START);
       }
     }
     if (d_arithEntail.check(node[2], true))
     {
       // y>0  implies  indexof( x, x, y ) --> -1
-      Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1));
+      Node negone = nm->mkConstInt(Rational(-1));
       return returnRewrite(node, negone, Rewrite::IDOF_EQ_NSTART);
     }
     Node emp = Word::mkEmptyWord(stype);
@@ -2538,7 +2535,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
   if (d_arithEntail.check(len1, len0m2, true))
   {
     // len(x)-z < len(y)  implies  indexof( x, y, z ) ----> -1
-    Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1));
+    Node negone = nm->mkConstInt(Rational(-1));
     return returnRewrite(node, negone, Rewrite::IDOF_LEN);
   }
 
@@ -2620,7 +2617,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
     else
     {
       // str.contains( x, y ) --> false  implies  str.indexof(x,y,z) --> -1
-      Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1));
+      Node negone = nm->mkConstInt(Rational(-1));
       return returnRewrite(node, negone, Rewrite::IDOF_NCTN);
     }
   }
@@ -2675,12 +2672,12 @@ Node SequencesRewriter::rewriteIndexofRe(Node node)
   Node s = node[0];
   Node r = node[1];
   Node n = node[2];
-  Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+  Node zero = nm->mkConstInt(Rational(0));
   Node slen = nm->mkNode(STRING_LENGTH, s);
 
   if (d_arithEntail.check(zero, n, true) || d_arithEntail.check(n, slen, true))
   {
-    Node ret = nm->mkConst(CONST_RATIONAL, Rational(-1));
+    Node ret = nm->mkConstInt(Rational(-1));
     return returnRewrite(node, ret, Rewrite::INDEXOF_RE_INVALID_INDEX);
   }
 
@@ -2695,15 +2692,14 @@ Node SequencesRewriter::rewriteIndexofRe(Node node)
         // We know that, due to limitations on the size of string constants
         // in our implementation, that accessing a position greater than
         // rMaxInt is guaranteed to be out of bounds.
-        Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1));
+        Node negone = nm->mkConstInt(Rational(-1));
         return returnRewrite(node, negone, Rewrite::INDEXOF_RE_MAX_INDEX);
       }
 
       uint32_t start = nrat.getNumerator().toUnsignedInt();
       Node rem = nm->mkConst(s.getConst<String>().substr(start));
       std::pair<size_t, size_t> match = firstMatch(rem, r);
-      Node ret = nm->mkConst(
-          CONST_RATIONAL,
+      Node ret = nm->mkConstInt(
           Rational(match.first == string::npos
                        ? -1
                        : static_cast<int64_t>(start + match.first)));
@@ -2967,8 +2963,8 @@ Node SequencesRewriter::rewriteReplace(Node node)
         nm->mkNode(kind::STRING_LENGTH, utils::mkConcat(children1, stype));
     Node maxLen1 = nm->mkNode(kind::PLUS, partLen1, lastChild1[2]);
 
-    Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
-    Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
+    Node zero = nm->mkConstInt(Rational(0));
+    Node one = nm->mkConstInt(Rational(1));
     Node len0 = nm->mkNode(kind::STRING_LENGTH, node[0]);
     Node len0_1 = nm->mkNode(kind::PLUS, len0, one);
     // Check len(t) + j > len(x) + 1
@@ -3491,8 +3487,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n)
   Node val;
   if (isPrefix)
   {
-    val =
-        NodeManager::currentNM()->mkConst(CONST_RATIONAL, ::cvc5::Rational(0));
+    val = NodeManager::currentNM()->mkConstInt(::cvc5::Rational(0));
   }
   else
   {
@@ -3527,7 +3522,7 @@ Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype)
   NodeManager* nm = NodeManager::currentNM();
 
   Node res;
-  if (len.getKind() == CONST_RATIONAL)
+  if (len.isConst())
   {
     // c -> "A" repeated c times
     Rational ratLen = len.getConst<Rational>();

diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index eb09ff187ecdb17c6042048cf13fbe1dd84154ac..03c9f9375c0c3a262e65246c4e353a9888b39864 100644 (file)
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -54,7 +54,7 @@ SkolemCache::SkolemCache(Rewriter* rr) : d_rr(rr)
 {
   NodeManager* nm = NodeManager::currentNM();
   d_strType = nm->stringType();
-  d_zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+  d_zero = nm->mkConstInt(Rational(0));
 }
 
 Node SkolemCache::mkSkolemCached(Node a, Node b, SkolemId id, const char* c)
@@ -217,27 +217,26 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
   {
     // SK_ID_VC_SPT(x, y) ---> SK_SUFFIX_REM(x, 1)
     id = SK_SUFFIX_REM;
-    b = nm->mkConst(CONST_RATIONAL, Rational(1));
+    b = nm->mkConstInt(Rational(1));
   }
   else if (id == SK_ID_VC_SPT_REV)
   {
     // SK_ID_VC_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) 1))
     id = SK_PREFIX;
-    b = nm->mkNode(MINUS,
-                   nm->mkNode(STRING_LENGTH, a),
-                   nm->mkConst(CONST_RATIONAL, Rational(1)));
+    b = nm->mkNode(
+        MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkConstInt(Rational(1)));
   }
   else if (id == SK_ID_DC_SPT)
   {
     // SK_ID_DC_SPT(x, y) ---> SK_PREFIX(x, 1)
     id = SK_PREFIX;
-    b = nm->mkConst(CONST_RATIONAL, Rational(1));
+    b = nm->mkConstInt(Rational(1));
   }
   else if (id == SK_ID_DC_SPT_REM)
   {
     // SK_ID_DC_SPT_REM(x, y) ---> SK_SUFFIX_REM(x, 1)
     id = SK_SUFFIX_REM;
-    b = nm->mkConst(CONST_RATIONAL, Rational(1));
+    b = nm->mkConstInt(Rational(1));
   }
   else if (id == SK_ID_DEQ_X)
   {

diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 045347cbb6fdc87ff04e78559d24e4f9fb03e48e..6b7fc699bdce2df8e75dbbf879ad5c011c8af18c 100644 (file)
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -34,7 +34,7 @@ SolverState::SolverState(Env& env, Valuation& v)
       d_pendingConflictSet(env.getContext(), false),
       d_pendingConflict(InferenceId::UNKNOWN)
 {
-  d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
+  d_zero = NodeManager::currentNM()->mkConstInt(Rational(0));
   d_false = NodeManager::currentNM()->mkConst(false);
 }
 

diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp
index 6e4ba25a564de19a68db71a6bba36e8bf5326ddd..952a1a36bd55905afea1951831039e37acde0dbe 100644 (file)
--- a/src/theory/strings/strings_entail.cpp
+++ b/src/theory/strings/strings_entail.cpp
@@ -123,7 +123,7 @@ bool StringsEntail::stripSymbolicLength(std::vector<Node>& n1,
   Assert(dir == 1 || dir == -1);
   Assert(nr.empty());
   NodeManager* nm = NodeManager::currentNM();
-  Node zero = nm->mkConst(CONST_RATIONAL, cvc5::Rational(0));
+  Node zero = nm->mkConstInt(cvc5::Rational(0));
   bool ret = false;
   bool success = true;
   unsigned sindex = 0;
@@ -145,7 +145,7 @@ bool StringsEntail::stripSymbolicLength(std::vector<Node>& n1,
           Assert(d_arithEntail.check(curr, true));
           Node s = n1[sindex_use];
           size_t slen = Word::getLength(s);
-          Node ncl = nm->mkConst(CONST_RATIONAL, cvc5::Rational(slen));
+          Node ncl = nm->mkConstInt(cvc5::Rational(slen));
           Node next_s = nm->mkNode(MINUS, lowerBound, ncl);
           next_s = d_rr->rewrite(next_s);
           Assert(next_s.isConst());
@@ -461,7 +461,7 @@ bool StringsEntail::componentContainsBase(
               {
                 n1rb = nm->mkNode(STRING_SUBSTR,
                                   n2[0],
-                                  nm->mkConst(CONST_RATIONAL, Rational(0)),
+                                  nm->mkConstInt(Rational(0)),
                                   start_pos);
               }
               if (dir != 1)
@@ -714,7 +714,7 @@ bool StringsEntail::checkNonEmpty(Node a)
 bool StringsEntail::checkLengthOne(Node s, bool strict)
 {
   NodeManager* nm = NodeManager::currentNM();
-  Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
+  Node one = nm->mkConstInt(Rational(1));
   Node len = nm->mkNode(STRING_LENGTH, s);
   len = d_rr->rewrite(len);
   return d_arithEntail.check(one, len)

diff --git a/src/theory/strings/strings_fmf.cpp b/src/theory/strings/strings_fmf.cpp
index 2951c86a2108449c9e8f81d0adabd9c7e672d1be..a3ae03099e8ffe6d8e206e441b54db14ffea9f00 100644 (file)
--- a/src/theory/strings/strings_fmf.cpp
+++ b/src/theory/strings/strings_fmf.cpp
@@ -85,8 +85,7 @@ Node StringsFmf::StringSumLengthDecisionStrategy::mkLiteral(unsigned i)
     return Node::null();
   }
   NodeManager* nm = NodeManager::currentNM();
-  Node lit = nm->mkNode(
-      LEQ, d_inputVarLsum.get(), nm->mkConst(CONST_RATIONAL, Rational(i)));
+  Node lit = nm->mkNode(LEQ, d_inputVarLsum.get(), nm->mkConstInt(Rational(i)));
   Trace("strings-fmf") << "StringsFMF::mkLiteral: " << lit << std::endl;
   return lit;
 }

diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp
index e4b91d4d81d1083c2b81ff987e2629d53d903b3c..2ff7598b5d3f087fe6a9cd531de08527024eeab1 100644 (file)
--- a/src/theory/strings/strings_rewriter.cpp
+++ b/src/theory/strings/strings_rewriter.cpp
@@ -100,11 +100,11 @@ Node StringsRewriter::rewriteStrToInt(Node node)
     String s = node[0].getConst<String>();
     if (s.isNumber())
     {
-      ret = nm->mkConst(CONST_RATIONAL, s.toNumber());
+      ret = nm->mkConstInt(s.toNumber());
     }
     else
     {
-      ret = nm->mkConst(CONST_RATIONAL, Rational(-1));
+      ret = nm->mkConstInt(Rational(-1));
     }
     return returnRewrite(node, ret, Rewrite::STOI_EVAL);
   }
@@ -117,7 +117,7 @@ Node StringsRewriter::rewriteStrToInt(Node node)
         String t = nc.getConst<String>();
         if (!t.isNumber())
         {
-          Node ret = nm->mkConst(CONST_RATIONAL, Rational(-1));
+          Node ret = nm->mkConstInt(Rational(-1));
           return returnRewrite(node, ret, Rewrite::STOI_CONCAT_NONNUM);
         }
       }
@@ -303,11 +303,11 @@ Node StringsRewriter::rewriteStringToCode(Node n)
     {
       std::vector<unsigned> vec = s.getVec();
       Assert(vec.size() == 1);
-      ret = nm->mkConst(CONST_RATIONAL, Rational(vec[0]));
+      ret = nm->mkConstInt(Rational(vec[0]));
     }
     else
     {
-      ret = nm->mkConst(CONST_RATIONAL, Rational(-1));
+      ret = nm->mkConstInt(Rational(-1));
     }
     return returnRewrite(n, ret, Rewrite::TO_CODE_EVAL);
   }
@@ -320,10 +320,9 @@ Node StringsRewriter::rewriteStringIsDigit(Node n)
   NodeManager* nm = NodeManager::currentNM();
   // eliminate str.is_digit(s) ----> 48 <= str.to_code(s) <= 57
   Node t = nm->mkNode(STRING_TO_CODE, n[0]);
-  Node retNode =
-      nm->mkNode(AND,
-                 nm->mkNode(LEQ, nm->mkConst(CONST_RATIONAL, Rational(48)), t),
-                 nm->mkNode(LEQ, t, nm->mkConst(CONST_RATIONAL, Rational(57))));
+  Node retNode = nm->mkNode(AND,
+                            nm->mkNode(LEQ, nm->mkConstInt(Rational(48)), t),
+                            nm->mkNode(LEQ, t, nm->mkConstInt(Rational(57))));
   return returnRewrite(n, retNode, Rewrite::IS_DIGIT_ELIM);
 }
 

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 85027370ea5048583f1466cd88c7f21edaf05cbc..d2d72327646cbb7d3910f855bc80cc4d17d79835 100644 (file)
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -60,9 +60,9 @@ TermRegistry::TermRegistry(Env& env,
               : nullptr)
 {
   NodeManager* nm = NodeManager::currentNM();
-  d_zero = nm->mkConst(CONST_RATIONAL, Rational(0));
-  d_one = nm->mkConst(CONST_RATIONAL, Rational(1));
-  d_negOne = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(-1));
+  d_zero = nm->mkConstInt(Rational(0));
+  d_one = nm->mkConstInt(Rational(1));
+  d_negOne = NodeManager::currentNM()->mkConstInt(Rational(-1));
   Assert(options().strings.stringsAlphaCard <= String::num_codes());
   d_alphaCard = options().strings.stringsAlphaCard;
 }
@@ -81,13 +81,12 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard)
   if (tk == STRING_TO_CODE)
   {
     // ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 )
-    Node code_len =
-        utils::mkNLength(t[0]).eqNode(nm->mkConst(CONST_RATIONAL, Rational(1)));
-    Node code_eq_neg1 = t.eqNode(nm->mkConst(CONST_RATIONAL, Rational(-1)));
-    Node code_range = nm->mkNode(
-        AND,
-        nm->mkNode(GEQ, t, nm->mkConst(CONST_RATIONAL, Rational(0))),
-        nm->mkNode(LT, t, nm->mkConst(CONST_RATIONAL, Rational(alphaCard))));
+    Node code_len = utils::mkNLength(t[0]).eqNode(nm->mkConstInt(Rational(1)));
+    Node code_eq_neg1 = t.eqNode(nm->mkConstInt(Rational(-1)));
+    Node code_range =
+        nm->mkNode(AND,
+                   nm->mkNode(GEQ, t, nm->mkConstInt(Rational(0))),
+                   nm->mkNode(LT, t, nm->mkConstInt(Rational(alphaCard))));
     lemma = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
   }
   else if (tk == STRING_INDEXOF || tk == STRING_INDEXOF_RE)
@@ -98,17 +97,16 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard)
     //
     // where f in { str.indexof, str.indexof_re }
     Node l = nm->mkNode(STRING_LENGTH, t[0]);
-    lemma = nm->mkNode(
-        AND,
-        nm->mkNode(OR,
-                   t.eqNode(nm->mkConst(CONST_RATIONAL, Rational(-1))),
-                   nm->mkNode(GEQ, t, t[2])),
-        nm->mkNode(LEQ, t, l));
+    lemma = nm->mkNode(AND,
+                       nm->mkNode(OR,
+                                  t.eqNode(nm->mkConstInt(Rational(-1))),
+                                  nm->mkNode(GEQ, t, t[2])),
+                       nm->mkNode(LEQ, t, l));
   }
   else if (tk == STRING_STOI)
   {
     // (>= (str.to_int x) (- 1))
-    lemma = nm->mkNode(GEQ, t, nm->mkConst(CONST_RATIONAL, Rational(-1)));
+    lemma = nm->mkNode(GEQ, t, nm->mkConstInt(Rational(-1)));
   }
   else if (tk == STRING_CONTAINS)
   {
@@ -126,7 +124,7 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc, uint32_t alphaCard)
 Node TermRegistry::lengthPositive(Node t)
 {
   NodeManager* nm = NodeManager::currentNM();
-  Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
+  Node zero = nm->mkConstInt(Rational(0));
   Node emp = Word::mkEmptyWord(t.getType());
   Node tlen = nm->mkNode(STRING_LENGTH, t);
   Node tlenEqZero = tlen.eqNode(zero);
@@ -416,7 +414,7 @@ TrustNode TermRegistry::getRegisterTermLemma(Node n)
   }
   else if (n.isConst())
   {
-    lsum = nm->mkConst(CONST_RATIONAL, Rational(Word::getLength(n)));
+    lsum = nm->mkConstInt(Rational(Word::getLength(n)));
   }
   Assert(!lsum.isNull());
   d_proxyVarToLength[sk] = lsum;
@@ -486,7 +484,7 @@ bool TermRegistry::isHandledUpdate(Node n)
   {
     lenN = nm->mkNode(STRING_LENGTH, n[2]);
   }
-  Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
+  Node one = nm->mkConstInt(Rational(1));
   return d_aent.checkEq(lenN, one);
 }
 

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 4ed754b16a6b6339dfa178b717fe6d62918f3f60..8b496b725006e7717932dbe31ba851d320d9f202 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -84,9 +84,9 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
 {
   d_termReg.finishInit(&d_im);
 
-  d_zero = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(0));
-  d_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(1));
-  d_neg_one = NodeManager::currentNM()->mkConst(CONST_RATIONAL, Rational(-1));
+  d_zero = NodeManager::currentNM()->mkConstInt(Rational(0));
+  d_one = NodeManager::currentNM()->mkConstInt(Rational(1));
+  d_neg_one = NodeManager::currentNM()->mkConstInt(Rational(-1));
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
 
@@ -425,7 +425,7 @@ bool TheoryStrings::collectModelInfoType(
           lvalue++;
         }
         Trace("strings-model") << "*** Decide to make length of " << lvalue << std::endl;
-        lts_values[i] = nm->mkConst(CONST_RATIONAL, Rational(lvalue));
+        lts_values[i] = nm->mkConstInt(Rational(lvalue));
         values_used[lvalue] = Node::null();
       }
       Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes ";
@@ -1071,8 +1071,7 @@ TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
     SkolemCache* sc = d_termReg.getSkolemCache();
     Node k = sc->mkSkolemCached(atom, SkolemCache::SK_PURIFY, "kFromCode");
     Node t = atom[0];
-    Node card = nm->mkConst(CONST_RATIONAL,
-                            Rational(d_termReg.getAlphabetCardinality()));
+    Node card = nm->mkConstInt(Rational(d_termReg.getAlphabetCardinality()));
     Node cond =
         nm->mkNode(AND, nm->mkNode(LEQ, d_zero, t), nm->mkNode(LT, t, card));
     Node emp = Word::mkEmptyWord(atom.getType());

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 4f27371ffad7ceb916ad0d281ac5f05fcc5ef590..4c2319b4e4eb58f9d7cb6ccc5227de6c4d4150f8 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -53,9 +53,9 @@ Node StringsPreprocess::reduce(Node t,
       << "StringsPreprocess::reduce: " << t << std::endl;
   Node retNode = t;
   NodeManager* nm = NodeManager::currentNM();
-  Node zero = nm->mkConst(CONST_RATIONAL, Rational(0));
-  Node one = nm->mkConst(CONST_RATIONAL, Rational(1));
-  Node negOne = nm->mkConst(CONST_RATIONAL, Rational(-1));
+  Node zero = nm->mkConstInt(Rational(0));
+  Node one = nm->mkConstInt(Rational(1));
+  Node negOne = nm->mkConstInt(Rational(-1));
 
   if( t.getKind() == kind::STRING_SUBSTR ) {
     // processing term:  substr( s, n, m )
@@ -184,7 +184,7 @@ Node StringsPreprocess::reduce(Node t,
     Node skk = sc->mkTypedSkolemCached(
         nm->integerType(), t, SkolemCache::SK_PURIFY, "iok");
 
-    Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1));
+    Node negone = nm->mkConstInt(Rational(-1));
 
     // substr( x, n, len( x ) - n )
     Node st = nm->mkNode(STRING_SUBSTR,
@@ -364,7 +364,7 @@ Node StringsPreprocess::reduce(Node t,
     Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0")));
     Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0);
 
-    Node ten = nm->mkConst(CONST_RATIONAL, Rational(10));
+    Node ten = nm->mkConstInt(Rational(10));
     Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux)));
     Node leadingZeroPos =
         nm->mkNode(AND, x.eqNode(zero), nm->mkNode(GT, leni, one));
@@ -431,7 +431,7 @@ Node StringsPreprocess::reduce(Node t,
         MINUS,
         nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, s, k, one)),
         c0);
-    Node ten = nm->mkConst(CONST_RATIONAL, Rational(10));
+    Node ten = nm->mkConstInt(Rational(10));
     Node kc3 = nm->mkNode(
         OR, nm->mkNode(LT, codeSk, zero), nm->mkNode(GEQ, codeSk, ten));
     conc1.push_back(nm->mkNode(OR, sEmpty, nm->mkNode(AND, kc1, kc2, kc3)));
@@ -865,12 +865,11 @@ Node StringsPreprocess::reduce(Node t,
     Node ci = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, x, i, one));
     Node ri = nm->mkNode(STRING_TO_CODE, nm->mkNode(STRING_SUBSTR, r, i, one));
 
-    Node lb = nm->mkConst(CONST_RATIONAL,
-                          Rational(t.getKind() == STRING_TOUPPER ? 97 : 65));
-    Node ub = nm->mkConst(CONST_RATIONAL,
-                          Rational(t.getKind() == STRING_TOUPPER ? 122 : 90));
-    Node offset = nm->mkConst(
-        CONST_RATIONAL, Rational(t.getKind() == STRING_TOUPPER ? -32 : 32));
+    Node lb = nm->mkConstInt(Rational(t.getKind() == STRING_TOUPPER ? 97 : 65));
+    Node ub =
+        nm->mkConstInt(Rational(t.getKind() == STRING_TOUPPER ? 122 : 90));
+    Node offset =
+        nm->mkConstInt(Rational(t.getKind() == STRING_TOUPPER ? -32 : 32));
 
     Node res = nm->mkNode(
         ITE,

diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index a133babba2f00b14557b6cc7a59882c7262af04d..0ee2e906d074037b8685a93f75ca3c019137c95a 100644 (file)
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -165,8 +165,7 @@ Node mkNLength(Node t)
 Node mkPrefix(Node t, Node n)
 {
   NodeManager* nm = NodeManager::currentNM();
-  return nm->mkNode(
-      STRING_SUBSTR, t, nm->mkConst(CONST_RATIONAL, Rational(0)), n);
+  return nm->mkNode(STRING_SUBSTR, t, nm->mkConstInt(Rational(0)), n);
 }
 
 Node mkSuffix(Node t, Node n)