Fix unsigned integer type issues in strings (#2380)

* Fix unsigned integer types in strings.

* Format

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 477e99b9b6b43ea20a4a299d2ff7f32edaf1c826..3faa63df5df0ffb4590ebb8b302e10043fdbc664 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -34,7 +34,7 @@ RegExpOpr::RegExpOpr()
                                                      std::vector<Node>{})),
       d_zero(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))),
       d_one(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))),
-      RMAXINT(LONG_MAX),
+      d_rMaxInt(UINT32_MAX),
       d_sigma(NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA,
                                                std::vector<Node>{})),
       d_sigma_star(NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, d_sigma))
@@ -1137,7 +1137,8 @@ bool RegExpOpr::isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2) {
 
 bool RegExpOpr::containC2(unsigned cnt, Node n) {
   if(n.getKind() == kind::REGEXP_RV) {
-    Assert(n[0].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in RegExpOpr::containC2");
+    Assert(n[0].getConst<Rational>() <= d_rMaxInt,
+           "Exceeded UINT32_MAX in RegExpOpr::containC2");
     unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt();
     return cnt == y;
   } else if(n.getKind() == kind::REGEXP_CONCAT) {
@@ -1178,7 +1179,8 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) {
     r1 = d_emptySingleton;
     r2 = d_emptySingleton;
   } else if(n.getKind() == kind::REGEXP_RV) {
-    Assert(n[0].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in RegExpOpr::convert2");
+    Assert(n[0].getConst<Rational>() <= d_rMaxInt,
+           "Exceeded UINT32_MAX in RegExpOpr::convert2");
     unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt();
     r1 = d_emptySingleton;
     if(cnt == y) {

diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index a646f0e6f8cae3719b03bcf9938cce390596b069..298c88e8c3a4d8d75e6f65d9e635031f7f0d41b2 100644 (file)
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -48,7 +48,7 @@ class RegExpOpr {
   Node d_emptyRegexp;
   Node d_zero;
   Node d_one;
-  CVC4::Rational RMAXINT;
+  CVC4::Rational d_rMaxInt;
 
   Node d_sigma;
   Node d_sigma_star;

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ce01006863a933d42742b8a23b7e9933a1830d8c..25e07d7aede6682df2d920ca00f4b375cf4f6428 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -103,7 +103,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
                              Valuation valuation,
                              const LogicInfo& logicInfo)
     : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
-      RMAXINT(LONG_MAX),
+      d_rMaxInt(UINT32_MAX),
       d_notify(*this),
       d_equalityEngine(d_notify, c, "theory::strings", true),
       d_conflict(c, false),
@@ -536,7 +536,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
     Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl;
     if( lts[i].isConst() ) {
       lts_values.push_back( lts[i] );
-      Assert(lts[i].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model");
+      Assert(lts[i].getConst<Rational>() <= d_rMaxInt,
+             "Exceeded UINT32_MAX in string model");
       unsigned lvalue = lts[i].getConst<Rational>().getNumerator().toUnsignedInt();
       values_used[ lvalue ] = true;
     }else{
@@ -545,7 +546,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
         Node v = d_valuation.getModelValue(lts[i]);
         Trace("strings-model") << "Model value for " << lts[i] << " is " << v << std::endl;
         lts_values.push_back( v );
-        Assert(v.getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model");
+        Assert(v.getConst<Rational>() <= d_rMaxInt,
+               "Exceeded UINT32_MAX in string model");
         unsigned lvalue =  v.getConst<Rational>().getNumerator().toUnsignedInt();
         values_used[ lvalue ] = true;
       }else{
@@ -621,7 +623,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
       Trace("strings-model") << std::endl;
 
       //use type enumerator
-      Assert(lts_values[i].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model");
+      Assert(lts_values[i].getConst<Rational>() <= d_rMaxInt,
+             "Exceeded UINT32_MAX in string model");
       StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt());
       for (const Node& eqc : pure_eq)
       {

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index de505f262193a2d82a3b464e911d62edeca5d1cf..2c899988fbcaf3064a2d88d18f1e1598ccb5fc04 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -234,7 +234,7 @@ private:
   Node d_zero;
   Node d_one;
   Node d_neg_one;
-  CVC4::Rational RMAXINT;
+  CVC4::Rational d_rMaxInt;
   unsigned d_card_size;
   // Helper functions
   Node getRepresentative( Node t );

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 9a0fad7d822b52c02b01ec522df7a2cbd709d271..72567b2b39433b2b70cbb6ba115f96fac06cff43 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -653,13 +653,13 @@ Node TheoryStringsRewriter::rewriteLoopRegExp(TNode node)
   }
   TNode n1 = node[1];
   NodeManager* nm = NodeManager::currentNM();
-  CVC4::Rational RMAXINT(LONG_MAX);
+  CVC4::Rational rMaxInt(UINT32_MAX);
   AlwaysAssert(n1.isConst(), "re.loop contains non-constant integer (1).");
   AlwaysAssert(n1.getConst<Rational>().sgn() >= 0,
                "Negative integer in string REGEXP_LOOP (1)");
-  Assert(n1.getConst<Rational>() <= RMAXINT,
-         "Exceeded LONG_MAX in string REGEXP_LOOP (1)");
-  unsigned l = n1.getConst<Rational>().getNumerator().toUnsignedInt();
+  Assert(n1.getConst<Rational>() <= rMaxInt,
+         "Exceeded UINT32_MAX in string REGEXP_LOOP (1)");
+  uint32_t l = n1.getConst<Rational>().getNumerator().toUnsignedInt();
   std::vector<Node> vec_nodes;
   for (unsigned i = 0; i < l; i++)
   {
@@ -675,9 +675,9 @@ Node TheoryStringsRewriter::rewriteLoopRegExp(TNode node)
     AlwaysAssert(n2.isConst(), "re.loop contains non-constant integer (2).");
     AlwaysAssert(n2.getConst<Rational>().sgn() >= 0,
                  "Negative integer in string REGEXP_LOOP (2)");
-    Assert(n2.getConst<Rational>() <= RMAXINT,
-           "Exceeded LONG_MAX in string REGEXP_LOOP (2)");
-    unsigned u = n2.getConst<Rational>().getNumerator().toUnsignedInt();
+    Assert(n2.getConst<Rational>() <= rMaxInt,
+           "Exceeded UINT32_MAX in string REGEXP_LOOP (2)");
+    uint32_t u = n2.getConst<Rational>().getNumerator().toUnsignedInt();
     if (u <= l)
     {
       retNode = n;
@@ -838,7 +838,7 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i
       }
     }
     case kind::REGEXP_LOOP: {
-      unsigned l = r[1].getConst<Rational>().getNumerator().toUnsignedInt();
+      uint32_t l = r[1].getConst<Rational>().getNumerator().toUnsignedInt();
       if(s.size() == index_start) {
         return l==0? true : testConstStringInRegExp(s, index_start, r[0]);
       } else if(l==0 && r[1]==r[2]) {
@@ -847,7 +847,7 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i
         Assert(r.getNumChildren() == 3, "String rewriter error: LOOP has 2 children");
         if(l==0) {
           //R{0,u}
-          unsigned u = r[2].getConst<Rational>().getNumerator().toUnsignedInt();
+          uint32_t u = r[2].getConst<Rational>().getNumerator().toUnsignedInt();
           for(unsigned len=s.size() - index_start; len>=1; len--) {
             CVC4::String t = s.substr(index_start, len);
             if(testConstStringInRegExp(t, 0, r[0])) {
@@ -1216,9 +1216,9 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
     if (node[1].isConst() && node[2].isConst())
     {
       CVC4::String s = node[0].getConst<String>();
-      CVC4::Rational RMAXINT(LONG_MAX);
-      unsigned start;
-      if (node[1].getConst<Rational>() > RMAXINT)
+      CVC4::Rational rMaxInt(UINT32_MAX);
+      uint32_t start;
+      if (node[1].getConst<Rational>() > rMaxInt)
       {
         // start beyond the maximum size of strings
         // thus, it must be beyond the end point of this string
@@ -1241,7 +1241,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
           return returnRewrite(node, ret, "ss-const-start-oob");
         }
       }
-      if (node[2].getConst<Rational>() > RMAXINT)
+      if (node[2].getConst<Rational>() > rMaxInt)
       {
         // take up to the end of the string
         Node ret = nm->mkConst(::CVC4::String(s.suffix(s.size() - start)));
@@ -1254,7 +1254,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
       }
       else
       {
-        unsigned len =
+        uint32_t len =
             node[2].getConst<Rational>().getNumerator().toUnsignedInt();
         if (start + len > s.size())
         {
@@ -1743,17 +1743,17 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
   getConcat(node[0], children0);
   if (children0[0].isConst() && node[1].isConst() && node[2].isConst())
   {
-    CVC4::Rational RMAXINT(CVC4::String::maxSize());
-    if (node[2].getConst<Rational>() > RMAXINT)
+    CVC4::Rational rMaxInt(CVC4::String::maxSize());
+    if (node[2].getConst<Rational>() > rMaxInt)
     {
       // 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.
+      // rMaxInt is guaranteed to be out of bounds.
       Node negone = nm->mkConst(Rational(-1));
       return returnRewrite(node, negone, "idof-max");
     }
     Assert(node[2].getConst<Rational>().sgn() >= 0);
-    unsigned start =
+    uint32_t start =
         node[2].getConst<Rational>().getNumerator().toUnsignedInt();
     CVC4::String s = children0[0].getConst<String>();
     CVC4::String t = node[1].getConst<String>();
@@ -2641,10 +2641,10 @@ bool TheoryStringsRewriter::stripSymbolicLength(std::vector<Node>& n1,
               // we can remove part of the constant
               // lower bound minus the length of a concrete string is negative,
               // hence lowerBound cannot be larger than long max
-              Assert(lbr < Rational(LONG_MAX));
+              Assert(lbr < Rational(UINT32_MAX));
               curr = Rewriter::rewrite(NodeManager::currentNM()->mkNode(
                   kind::MINUS, curr, lowerBound));
-              unsigned lbsize = lbr.getNumerator().toUnsignedInt();
+              uint32_t lbsize = lbr.getNumerator().toUnsignedInt();
               Assert(lbsize < s.size());
               if (dir == 1)
               {