Use uniform length limit for String constants (#2381)

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 3faa63df5df0ffb4590ebb8b302e10043fdbc664..f53f82cc49e120c7a02e91e5446591256b10bf5c 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -34,7 +34,6 @@ RegExpOpr::RegExpOpr()
                                                      std::vector<Node>{})),
       d_zero(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))),
       d_one(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))),
-      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 +1136,7 @@ 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>() <= d_rMaxInt,
+    Assert(n[0].getConst<Rational>() <= Rational(String::maxSize()),
            "Exceeded UINT32_MAX in RegExpOpr::containC2");
     unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt();
     return cnt == y;
@@ -1179,7 +1178,7 @@ 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>() <= d_rMaxInt,
+    Assert(n[0].getConst<Rational>() <= Rational(String::maxSize()),
            "Exceeded UINT32_MAX in RegExpOpr::convert2");
     unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt();
     r1 = d_emptySingleton;

diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 298c88e8c3a4d8d75e6f65d9e635031f7f0d41b2..57e68abfbc527b267899d495754940015f5e1a82 100644 (file)
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -48,7 +48,6 @@ class RegExpOpr {
   Node d_emptyRegexp;
   Node d_zero;
   Node d_one;
-  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 25e07d7aede6682df2d920ca00f4b375cf4f6428..72e82edcaf6cabbc2a554822dc335e2e8e50ecbd 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -103,7 +103,6 @@ TheoryStrings::TheoryStrings(context::Context* c,
                              Valuation valuation,
                              const LogicInfo& logicInfo)
     : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
-      d_rMaxInt(UINT32_MAX),
       d_notify(*this),
       d_equalityEngine(d_notify, c, "theory::strings", true),
       d_conflict(c, false),
@@ -536,7 +535,7 @@ 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>() <= d_rMaxInt,
+      Assert(lts[i].getConst<Rational>() <= Rational(String::maxSize()),
              "Exceeded UINT32_MAX in string model");
       unsigned lvalue = lts[i].getConst<Rational>().getNumerator().toUnsignedInt();
       values_used[ lvalue ] = true;
@@ -546,7 +545,7 @@ 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>() <= d_rMaxInt,
+        Assert(v.getConst<Rational>() <= Rational(String::maxSize()),
                "Exceeded UINT32_MAX in string model");
         unsigned lvalue =  v.getConst<Rational>().getNumerator().toUnsignedInt();
         values_used[ lvalue ] = true;
@@ -623,7 +622,7 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
       Trace("strings-model") << std::endl;
 
       //use type enumerator
-      Assert(lts_values[i].getConst<Rational>() <= d_rMaxInt,
+      Assert(lts_values[i].getConst<Rational>() <= Rational(String::maxSize()),
              "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 2c899988fbcaf3064a2d88d18f1e1598ccb5fc04..2c0cb42aafddc76fba000b3ede65eecd22683bd4 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -234,7 +234,6 @@ private:
   Node d_zero;
   Node d_one;
   Node d_neg_one;
-  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 72567b2b39433b2b70cbb6ba115f96fac06cff43..1c68097ae1de16e664b0988895ba741d9b7ac0e2 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -653,7 +653,7 @@ Node TheoryStringsRewriter::rewriteLoopRegExp(TNode node)
   }
   TNode n1 = node[1];
   NodeManager* nm = NodeManager::currentNM();
-  CVC4::Rational rMaxInt(UINT32_MAX);
+  CVC4::Rational rMaxInt(String::maxSize());
   AlwaysAssert(n1.isConst(), "re.loop contains non-constant integer (1).");
   AlwaysAssert(n1.getConst<Rational>().sgn() >= 0,
                "Negative integer in string REGEXP_LOOP (1)");
@@ -1216,7 +1216,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
     if (node[1].isConst() && node[2].isConst())
     {
       CVC4::String s = node[0].getConst<String>();
-      CVC4::Rational rMaxInt(UINT32_MAX);
+      CVC4::Rational rMaxInt(String::maxSize());
       uint32_t start;
       if (node[1].getConst<Rational>() > rMaxInt)
       {
@@ -2641,7 +2641,7 @@ 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(UINT32_MAX));
+              Assert(lbr < Rational(String::maxSize()));
               curr = Rewriter::rewrite(NodeManager::currentNM()->mkNode(
                   kind::MINUS, curr, lowerBound));
               uint32_t lbsize = lbr.getNumerator().toUnsignedInt();

diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index 8d68d4e868269f9dd3a764afd2f2a56eff7cc754..34175a7751ac45a030b97c0dbd7c769fa0629233 100644 (file)
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -442,10 +442,8 @@ bool String::isDigit(unsigned character)
   return c >= '0' && c <= '9';
 }
 
-size_t String::maxSize()
-{
-  return std::numeric_limits<size_t>::max();
-}
+size_t String::maxSize() { return std::numeric_limits<uint32_t>::max(); }
+
 Rational String::toNumber() const
 {
   // when smt2 standard for strings is set, this may change, based on the