From 6c6f44c32a6bb957c1e82ae75fbf62db2e286595 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Thu, 7 Nov 2013 11:04:31 -0600 Subject: [PATCH] Adds the header file into makefile, solving building error; adds cache for derivative; disables loop detection when finite model finding is enabled. --- src/theory/strings/Makefile.am | 1 + src/theory/strings/theory_strings.cpp | 75 ++++++++++++++++----------- src/theory/strings/theory_strings.h | 1 + 3 files changed, 46 insertions(+), 31 deletions(-) diff --git a/src/theory/strings/Makefile.am b/src/theory/strings/Makefile.am index f7a6fa0a2..d5e5d1a23 100644 --- a/src/theory/strings/Makefile.am +++ b/src/theory/strings/Makefile.am @@ -14,6 +14,7 @@ libstrings_la_SOURCES = \ type_enumerator.h \ theory_strings_preprocess.h \ theory_strings_preprocess.cpp \ + regexp_operation.h \ regexp_operation.cpp EXTRA_DIST = \ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index fc4b3ba9c..5bc0e5cbe 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -48,6 +48,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu //d_lit_to_decide_index( c, 0 ), //d_lit_to_decide( c ), d_reg_exp_mem( c ), + //d_reg_exp_deriv( c ), d_curr_cardinality( c, 0 ) { // The kinds we are treating as function application in congruence @@ -919,20 +920,22 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //check for loops //Trace("strings-loop") << "Check for loops i,j = " << (index_i+1) << "/" << normal_forms[i].size() << " " << (index_j+1) << "/" << normal_forms[j].size() << std::endl; int has_loop[2] = { -1, -1 }; - for( unsigned r=0; r<2; r++ ){ - int index = (r==0 ? index_i : index_j); - int other_index = (r==0 ? index_j : index_i ); - int n_index = (r==0 ? i : j); - int other_n_index = (r==0 ? j : i); - if( normal_forms[other_n_index][other_index].getKind() != kind::CONST_STRING ) { - for( unsigned lp = index+1; lpmkNode( kind::IMPLIES, ant, conc ); + if( ant == d_true ) { + lem = conc; + } Trace("strings-lemma") << "Strings " << c << " lemma : " << lem << std::endl; d_lemma_cache.push_back( lem ); } @@ -1974,29 +1980,36 @@ bool TheoryStrings::checkMemberships() { Trace("strings-regexp") << "We have regular expression assertion : " << assertion << std::endl; Node atom = assertion.getKind()==kind::NOT ? assertion[0] : assertion; bool polarity = assertion.getKind()!=kind::NOT; - if( polarity ){ - if( d_reg_exp_unroll.find(atom)==d_reg_exp_unroll.end() ){ - Assert( atom.getKind()==kind::STRING_IN_REGEXP ); - Node x = atom[0]; - Node r = atom[1]; - Assert( r.getKind()==kind::REGEXP_STAR ); - if( !areEqual( x, d_emptyString ) ){ - //if(splitRegExp( x, r, atom )) { - // addedLemma = true; - //} else - if( unrollStar( atom ) ) { - addedLemma = true; - } else { - Trace("strings-regexp") << "RegExp is incomplete due to " << assertion << ", depth = " << options::stringRegExpUnrollDepth() << std::endl; - is_unk = true; + if( polarity ) { + Assert( atom.getKind()==kind::STRING_IN_REGEXP ); + Node x = atom[0]; + Node r = atom[1]; + Assert( r.getKind()==kind::REGEXP_STAR ); + if( !areEqual( x, d_emptyString ) ) { + bool flag = true; + if( d_reg_exp_deriv.find(atom)==d_reg_exp_deriv.end() ) { + if(splitRegExp( x, r, atom )) { + addedLemma = true; flag = false; + d_reg_exp_deriv[ atom ] = true; } - }else{ - Trace("strings-regexp") << "...is satisfied." << std::endl; + } else { + flag = false; + Trace("strings-regexp-derivative") << "... is processed by deriv." << std::endl; } - }else{ - Trace("strings-regexp") << "...Already unrolled." << std::endl; + if( flag && d_reg_exp_unroll.find(atom)==d_reg_exp_unroll.end() ) { + if( unrollStar( atom ) ) { + addedLemma = true; + } else { + Trace("strings-regexp") << "RegExp is incomplete due to " << assertion << ", depth = " << options::stringRegExpUnrollDepth() << std::endl; + is_unk = true; + } + } else { + Trace("strings-regexp") << "...is already unrolled or splitted." << std::endl; + } + } else { + Trace("strings-regexp") << "...is satisfied." << std::endl; } - }else{ + } else { //TODO: negative membership //Node r = Rewriter::rewrite( atom[1] ); //r = d_regexp_opr.complement( r ); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index df31dcff7..7d4b740e4 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -154,6 +154,7 @@ class TheoryStrings : public Theory { NodeList d_reg_exp_mem; std::map< Node, bool > d_reg_exp_unroll; std::map< Node, int > d_reg_exp_unroll_depth; + std::map< Node, bool > d_reg_exp_deriv; //antecedant for why reg exp membership must be true std::map< Node, Node > d_reg_exp_ant; -- 2.30.2