diff options
Diffstat (limited to 'src/theory/strings/regexp_operation.cpp')
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index b20e2f3ad..aaf1c864f 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -281,7 +281,7 @@ int RegExpOpr::delta( Node r, Node &exp ) { // 0-unknown, 1-yes, 2-no int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) { - Assert( c.size() < 2 ); + Assert(c.size() < 2); Trace("regexp-derive") << "RegExp-derive starts with /" << mkString( r ) << "/, c=" << c << std::endl; int ret = 1; @@ -522,7 +522,7 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) { } Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { - Assert( c.size() < 2 ); + Assert(c.size() < 2); Trace("regexp-derive") << "RegExp-derive starts with /" << mkString( r ) << "/, c=" << c << std::endl; Node retNode = d_emptyRegexp; PairNodeStr dv = std::make_pair( r, c ); @@ -1249,8 +1249,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>() <= Rational(String::maxSize()), - "Exceeded UINT32_MAX in RegExpOpr::containC2"); + 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; } else if(n.getKind() == kind::REGEXP_CONCAT) { @@ -1291,8 +1291,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>() <= Rational(String::maxSize()), - "Exceeded UINT32_MAX in RegExpOpr::convert2"); + 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; if(cnt == y) { @@ -1503,7 +1503,7 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > } Node RegExpOpr::removeIntersection(Node r) { - Assert( checkConstRegExp(r) ); + Assert(checkConstRegExp(r)); std::map < Node, Node >::const_iterator itr = d_rm_inter_cache.find(r); if(itr != d_rm_inter_cache.end()) { return itr->second; |