diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-10-21 23:10:35 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-10-21 23:10:35 -0500 |
| commit | 58e47f72906773748183a141f314a21f5b970b0b (patch) | |
| tree | da9291c5a54509318d580b486242091381ff7dcc /src/theory/strings/regexp_operation.cpp | |
| parent | ff3efb7f258c04a3371e28da3558451a4c81f000 (diff) | |
Fixed bug 589
Diffstat (limited to 'src/theory/strings/regexp_operation.cpp')
| -rw-r--r-- | src/theory/strings/regexp_operation.cpp | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index e769eb712..69b089c84 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -21,18 +21,20 @@ namespace CVC4 { namespace theory { namespace strings { -RegExpOpr::RegExpOpr() { +RegExpOpr::RegExpOpr() + : d_card( 256 ), + RMAXINT( LONG_MAX ) +{ d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); + d_emptySingleton = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString ); d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); d_one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) ); - d_emptySingleton = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString ); std::vector< Node > nvec; d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec ); d_sigma = NodeManager::currentNM()->mkNode( kind::REGEXP_SIGMA, nvec ); d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma ); - d_card = 256; } int RegExpOpr::gcd ( int a, int b ) { @@ -1284,6 +1286,7 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< unsigned, std::se 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"); unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt(); return cnt == y; } else if(n.getKind() == kind::REGEXP_CONCAT) { @@ -1322,6 +1325,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>() <= RMAXINT, "Exceeded LONG_MAX in RegExpOpr::containC2"); unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt(); r1 = d_emptySingleton; if(cnt == y) { |