summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/strings/regexp_operation.cpp5
-rw-r--r--src/theory/strings/regexp_operation.h1
-rw-r--r--src/theory/strings/theory_strings.cpp7
-rw-r--r--src/theory/strings/theory_strings.h1
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp6
-rw-r--r--src/util/regexp.cpp6
6 files changed, 10 insertions, 16 deletions
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<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 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<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 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<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 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<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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback