diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-01-30 11:20:29 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-01-30 11:20:29 -0600 |
commit | 0dd2aa21f35b221ea96d277e9ea7cbc816ffe83c (patch) | |
tree | 3aa2c1df2c732643c3ca95620fcf38e8e5608af8 /src/theory/strings | |
parent | a8a7949ec3e1a7f2a2d241d0fc58e08cbf4b7aec (diff) |
Fix regexp cache issue in strings, add regression.
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 10 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.h | 4 |
2 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index bf999806f..2bce8beea 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -4356,6 +4356,7 @@ void TheoryStrings::checkMemberships() { for( unsigned i=0; i<d_regexp_memberships.size(); i++ ) { //check regular expression membership Node assertion = d_regexp_memberships[i]; + Trace("regexp-debug") << "Check : " << assertion << " " << (d_regexp_ucached.find(assertion) == d_regexp_ucached.end()) << " " << (d_regexp_ccached.find(assertion) == d_regexp_ccached.end()) << std::endl; if( d_regexp_ucached.find(assertion) == d_regexp_ucached.end() && d_regexp_ccached.find(assertion) == d_regexp_ccached.end() ) { Trace("strings-regexp") << "We have regular expression assertion : " << assertion << std::endl; @@ -4396,7 +4397,7 @@ void TheoryStrings::checkMemberships() { } if( polarity ) { - flag = checkPDerivative(x, r, atom, addedLemma, processed, cprocessed, rnfexp); + flag = checkPDerivative(x, r, atom, addedLemma, rnfexp); if(options::stringOpt2() && flag) { if(d_regexp_opr.checkConstRegExp(r) && x.getKind()==kind::STRING_CONCAT) { std::vector< std::pair< Node, Node > > vec_can; @@ -4591,17 +4592,18 @@ void TheoryStrings::checkMemberships() { if( addedLemma ) { if( !d_conflict ){ for( unsigned i=0; i<processed.size(); i++ ) { + Trace("strings-regexp") << "...add " << processed[i] << " to u-cache." << std::endl; d_regexp_ucached.insert(processed[i]); } for( unsigned i=0; i<cprocessed.size(); i++ ) { + Trace("strings-regexp") << "...add " << cprocessed[i] << " to c-cache." << std::endl; d_regexp_ccached.insert(cprocessed[i]); } } } } -bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma, - std::vector< Node > &processed, std::vector< Node > &cprocessed, std::vector< Node > &nf_exp) { +bool TheoryStrings::checkPDerivative( Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &nf_exp ) { Node antnf = mkExplain(nf_exp); @@ -4654,7 +4656,7 @@ bool TheoryStrings::checkPDerivative(Node x, Node r, Node atom, bool &addedLemma sREant = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, sREant, antnf)); if(deriveRegExp( x, r, sREant )) { addedLemma = true; - processed.push_back( atom ); + d_regexp_ccached.insert(atom); return false; } } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 457afb15a..0294c3884 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -359,9 +359,7 @@ private: std::map< Node, std::vector< Node > > &XinR_with_exps); void checkMemberships(); bool checkMemberships2(); - bool checkPDerivative( Node x, Node r, Node atom, bool &addedLemma, - std::vector< Node > &processed, std::vector< Node > &cprocessed, - std::vector< Node > &nf_exp); + bool checkPDerivative( Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &nf_exp); //check contains void checkPosContains( std::vector< Node >& posContains ); void checkNegContains( std::vector< Node >& negContains ); |