Adds the header file into makefile, solving building error; adds cache for derivative...

diff --git a/src/theory/strings/Makefile.am b/src/theory/strings/Makefile.am
index f7a6fa0a2d93a22ddd0486236c291f24f57c884e..d5e5d1a233ff20a8ca46d04a8033d88d0827edf0 100644 (file)
--- 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 fc4b3ba9c161648d9c7b0ca54a5c6bcd2bd8a9d9..5bc0e5cbeb2ff1b8dfec8fa79864aa7fecb15abd 100644 (file)
--- 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; lp<normal_forms[n_index].size(); lp++ ){
-                                                                                                       if( normal_forms[n_index][lp]==normal_forms[other_n_index][other_index] ){
-                                                                                                               has_loop[r] = lp;
-                                                                                                               break;
+                                                                               //if( !options::stringFMF() ) {
+                                                                                       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; lp<normal_forms[n_index].size(); lp++ ){
+                                                                                                               if( normal_forms[n_index][lp]==normal_forms[other_n_index][other_index] ){
+                                                                                                                       has_loop[r] = lp;
+                                                                                                                       break;
+                                                                                                               }
                                                                                                        }
                                                                                                }
                                                                                        }
-                                                                               }
+                                                                               //}
                                                                                if( has_loop[0]!=-1 || has_loop[1]!=-1 ){
                                                                                        int loop_n_index = has_loop[0]!=-1 ? i : j;
                                                                                        int other_n_index = has_loop[0]!=-1 ? j : i;
@@ -1373,6 +1376,9 @@ void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) {
                d_conflict = true;
        }else{
                Node lem = NodeManager::currentNM()->mkNode( 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 df31dcff7b91240aaa46681fd0534ba2232d3627..7d4b740e4742143024490b628410632cc932cc89 100644 (file)
--- 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;