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 | |
parent | ff3efb7f258c04a3371e28da3558451a4c81f000 (diff) |
Fixed bug 589
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 10 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.h | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 4 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.h | 3 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 24 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 1 |
7 files changed, 36 insertions, 10 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) { diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index 2ae578cd6..ce3093528 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -22,6 +22,7 @@ #include <vector> #include <set> #include <algorithm> +#include <climits> #include "util/hash.h" #include "util/regexp.h" #include "theory/theory.h" @@ -46,6 +47,7 @@ private: Node d_emptyRegexp; Node d_zero; Node d_one; + CVC4::Rational RMAXINT; char d_char_start; char d_char_end; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index e0916974e..e8bf87a17 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -35,6 +35,7 @@ namespace strings { TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo), + RMAXINT(LONG_MAX), d_notify( *this ), d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings"), d_conflict(c, false), @@ -284,6 +285,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { 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"); unsigned lvalue = lts[i].getConst<Rational>().getNumerator().toUnsignedInt(); values_used[ lvalue ] = true; }else{ @@ -292,6 +294,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { 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"); unsigned lvalue = v.getConst<Rational>().getNumerator().toUnsignedInt(); values_used[ lvalue ] = true; }else{ @@ -346,6 +349,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { //use type enumerator + Assert(lts_values[i].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model"); StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt()); for( unsigned j=0; j<pure_eq.size(); j++ ){ Assert( !sel.isFinished() ); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 797c1bd29..95eba27bc 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -27,6 +27,8 @@ #include "context/cdchunk_list.h" #include "context/cdhashset.h" +#include <climits> + namespace CVC4 { namespace theory { namespace strings { @@ -125,6 +127,7 @@ private: Node d_false; Node d_zero; Node d_one; + CVC4::Rational RMAXINT; // Options bool d_opt_fmf; bool d_opt_regexp_gcd; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 6e7ca6d95..71db11fe1 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -126,7 +126,7 @@ int StringsPreprocess::checkFixLenVar( Node t ) { } } if(ret != 2) { - int len = t[ret].getConst<Rational>().getNumerator().toUnsignedInt(); + unsigned len = t[ret].getConst<Rational>().getNumerator().toUnsignedInt(); if(len < 2) { ret = 2; } diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index e37cabfb6..c952a7b3c 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -382,16 +382,23 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); } else if( node[1].isConst() && node[2].isConst() ) { if(node[1].getConst<Rational>().sgn()>=0 && node[2].getConst<Rational>().sgn()>=0) { - int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt(); - int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); + CVC4::Rational sum(node[1].getConst<Rational>() + node[2].getConst<Rational>()); if( node[0].isConst() ) { - if( node[0].getConst<String>().size() >= (unsigned) (i + j) ) { + CVC4::Rational size(node[0].getConst<String>().size()); + if( size >= sum ) { + //because size is smaller than MAX_INT + size_t i = node[1].getConst<Rational>().getNumerator().toUnsignedInt(); + size_t j = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) ); } else { retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); } } else if(node[0].getKind() == kind::STRING_CONCAT && node[0][0].isConst()) { - if( node[0][0].getConst<String>().size() >= (unsigned) (i + j) ) { + CVC4::Rational size2(node[0][0].getConst<String>().size()); + if( size2 >= sum ) { + //because size2 is smaller than MAX_INT + size_t i = node[1].getConst<Rational>().getNumerator().toUnsignedInt(); + size_t j = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); retNode = NodeManager::currentNM()->mkConst( node[0][0].getConst<String>().substr(i, j) ); } } @@ -451,10 +458,12 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) { CVC4::String s = node[0].getConst<String>(); CVC4::String t = node[1].getConst<String>(); - int i = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); + CVC4::Rational RMAXINT(LONG_MAX); + Assert(node[2].getConst<Rational>() <= RMAXINT, "Number exceeds LONG_MAX in string index_of"); + std::size_t i = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); std::size_t ret = s.find(t, i); if( ret != std::string::npos ) { - retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational((int) ret) ); + retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational((unsigned) ret) ); } else { retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); } @@ -634,6 +643,8 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { if(r.getKind() == kind::REGEXP_STAR) { retNode = r; } else { + CVC4::Rational RMAXINT(LONG_MAX); + Assert(node[1].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (1)"); unsigned l = node[1].getConst<Rational>().getNumerator().toUnsignedInt(); std::vector< Node > vec_nodes; for(unsigned i=0; i<l; i++) { @@ -642,6 +653,7 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) { if(node.getNumChildren() == 3) { Node n = vec_nodes.size()==0 ? NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst(CVC4::String(""))) : vec_nodes.size()==1 ? r : prerewriteConcatRegExp(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, vec_nodes)); + Assert(node[2].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string REGEXP_LOOP (2)"); unsigned u = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); if(u <= l) { retNode = n; diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index d33254e1b..9d04f107f 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -23,6 +23,7 @@ #include "theory/rewriter.h" #include "theory/type_enumerator.h" #include "expr/attribute.h" +#include <climits> namespace CVC4 { namespace theory { |