Fix regexp cache issue in strings, add regression.

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index bf999806fed0cdc6c7497087d633971ac5577a81..2bce8beea91ffae8dae2c55a9150a424c9d83269 100644 (file)
--- 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 457afb15a4557fe3efdb955aabe507060240d373..0294c38845befc26a301f69c1ab986b0df76a3f8 100644 (file)
--- 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 );

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index a77c2bd6c6a2bc0bcf571d4b38e6364012150f6a..f4dc8ebf7ca511f78010821f87fd9da36c51e2a2 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -85,7 +85,8 @@ TESTS = \
   gm-inc-071516-2.smt2 \
   cmu-inc-nlpp-071516.smt2 \
   strings-index-empty.smt2 \
-  bug768.smt2
+  bug768.smt2 \
+  username_checker_min.smt2
 
 FAILING_TESTS =
 

diff --git a/test/regress/regress0/strings/username_checker_min.smt2 b/test/regress/regress0/strings/username_checker_min.smt2
new file mode 100644 (file)
index 0000000..2f1c358
--- /dev/null
+++ b/test/regress/regress0/strings/username_checker_min.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_S)
+(set-option :strings-exp true)
+(set-info :status unsat)
+
+(declare-const buff String)
+(declare-const pass_mem String)
+(assert (= (str.len buff) 4))
+(assert (= (str.len pass_mem) 1))
+
+(assert (str.in.re (str.++ buff pass_mem) (re.+ (str.to.re "A"))))
+
+(assert (str.contains buff "<"))
+
+(check-sat)