summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/strings/regexp_operation.cpp8
-rw-r--r--src/theory/strings/regexp_operation.h2
-rw-r--r--src/theory/strings/theory_strings.cpp11
-rw-r--r--src/theory/strings/theory_strings.h2
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp40
5 files changed, 34 insertions, 29 deletions
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<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 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<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 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<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)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback