From: Andres Noetzli Date: Sun, 26 Aug 2018 21:31:16 +0000 (-0700) Subject: Use uniform length limit for String constants (#2381) X-Git-Tag: cvc5-1.0.0~4718 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9f9f8d29c9428289492e421fc1c464a51a06977e;p=cvc5.git 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 3faa63df5..f53f82cc4 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -34,7 +34,6 @@ RegExpOpr::RegExpOpr() std::vector{})), 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{})), 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() <= d_rMaxInt, + Assert(n[0].getConst() <= Rational(String::maxSize()), "Exceeded UINT32_MAX in RegExpOpr::containC2"); unsigned y = n[0].getConst().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() <= d_rMaxInt, + Assert(n[0].getConst() <= Rational(String::maxSize()), "Exceeded UINT32_MAX in RegExpOpr::convert2"); unsigned y = n[0].getConst().getNumerator().toUnsignedInt(); r1 = d_emptySingleton; diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 298c88e8c..57e68abfb 100644 --- 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 25e07d7ae..72e82edca 100644 --- 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() <= d_rMaxInt, + Assert(lts[i].getConst() <= Rational(String::maxSize()), "Exceeded UINT32_MAX in string model"); unsigned lvalue = lts[i].getConst().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() <= d_rMaxInt, + Assert(v.getConst() <= Rational(String::maxSize()), "Exceeded UINT32_MAX in string model"); unsigned lvalue = v.getConst().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() <= d_rMaxInt, + Assert(lts_values[i].getConst() <= Rational(String::maxSize()), "Exceeded UINT32_MAX in string model"); StringEnumeratorLength sel(lts_values[i].getConst().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 2c899988f..2c0cb42aa 100644 --- 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 72567b2b3..1c68097ae 100644 --- 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().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(); - CVC4::Rational rMaxInt(UINT32_MAX); + CVC4::Rational rMaxInt(String::maxSize()); uint32_t start; if (node[1].getConst() > rMaxInt) { @@ -2641,7 +2641,7 @@ bool TheoryStringsRewriter::stripSymbolicLength(std::vector& 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 8d68d4e86..34175a775 100644 --- 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::max(); -} +size_t String::maxSize() { return std::numeric_limits::max(); } + Rational String::toNumber() const { // when smt2 standard for strings is set, this may change, based on the