From: Andrew Reynolds Date: Sun, 26 Aug 2018 05:22:57 +0000 (-0500) Subject: Fix unsigned integer type issues in strings (#2380) X-Git-Tag: cvc5-1.0.0~4719 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=28867b06a05fc13d0257093fcd28caa5907317b6;p=cvc5.git 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 477e99b9b..3faa63df5 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -34,7 +34,7 @@ RegExpOpr::RegExpOpr() std::vector{})), 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{})), 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() <= RMAXINT, "Exceeded LONG_MAX in RegExpOpr::containC2"); + Assert(n[0].getConst() <= d_rMaxInt, + "Exceeded UINT32_MAX in RegExpOpr::containC2"); unsigned y = n[0].getConst().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() <= RMAXINT, "Exceeded LONG_MAX in RegExpOpr::convert2"); + Assert(n[0].getConst() <= d_rMaxInt, + "Exceeded UINT32_MAX in RegExpOpr::convert2"); unsigned y = n[0].getConst().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 a646f0e6f..298c88e8c 100644 --- 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 ce0100686..25e07d7ae 100644 --- 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() <= RMAXINT, "Exceeded LONG_MAX in string model"); + Assert(lts[i].getConst() <= d_rMaxInt, + "Exceeded UINT32_MAX in string model"); unsigned lvalue = lts[i].getConst().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() <= RMAXINT, "Exceeded LONG_MAX in string model"); + Assert(v.getConst() <= d_rMaxInt, + "Exceeded UINT32_MAX in string model"); unsigned lvalue = v.getConst().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() <= RMAXINT, "Exceeded LONG_MAX in string model"); + Assert(lts_values[i].getConst() <= d_rMaxInt, + "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 de505f262..2c899988f 100644 --- 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 9a0fad7d8..72567b2b3 100644 --- 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().sgn() >= 0, "Negative integer in string REGEXP_LOOP (1)"); - Assert(n1.getConst() <= RMAXINT, - "Exceeded LONG_MAX in string REGEXP_LOOP (1)"); - unsigned l = n1.getConst().getNumerator().toUnsignedInt(); + Assert(n1.getConst() <= rMaxInt, + "Exceeded UINT32_MAX in string REGEXP_LOOP (1)"); + uint32_t l = n1.getConst().getNumerator().toUnsignedInt(); std::vector 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().sgn() >= 0, "Negative integer in string REGEXP_LOOP (2)"); - Assert(n2.getConst() <= RMAXINT, - "Exceeded LONG_MAX in string REGEXP_LOOP (2)"); - unsigned u = n2.getConst().getNumerator().toUnsignedInt(); + Assert(n2.getConst() <= rMaxInt, + "Exceeded UINT32_MAX in string REGEXP_LOOP (2)"); + uint32_t u = n2.getConst().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().getNumerator().toUnsignedInt(); + uint32_t l = r[1].getConst().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().getNumerator().toUnsignedInt(); + uint32_t u = r[2].getConst().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(); - CVC4::Rational RMAXINT(LONG_MAX); - unsigned start; - if (node[1].getConst() > RMAXINT) + CVC4::Rational rMaxInt(UINT32_MAX); + uint32_t start; + if (node[1].getConst() > 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() > RMAXINT) + if (node[2].getConst() > 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().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() > RMAXINT) + CVC4::Rational rMaxInt(CVC4::String::maxSize()); + if (node[2].getConst() > 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().sgn() >= 0); - unsigned start = + uint32_t start = node[2].getConst().getNumerator().toUnsignedInt(); CVC4::String s = children0[0].getConst(); CVC4::String t = node[1].getConst(); @@ -2641,10 +2641,10 @@ 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(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) {