From 0dd2aa21f35b221ea96d277e9ea7cbc816ffe83c Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 30 Jan 2017 11:20:29 -0600
Subject: [PATCH] Fix regexp cache issue in strings, add regression.

---
 src/theory/strings/theory_strings.cpp              | 10 ++++++----
 src/theory/strings/theory_strings.h                |  4 +---
 test/regress/regress0/strings/Makefile.am          |  3 ++-
 .../regress0/strings/username_checker_min.smt2     | 14 ++++++++++++++
 4 files changed, 23 insertions(+), 8 deletions(-)
 create mode 100644 test/regress/regress0/strings/username_checker_min.smt2

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 );
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index a77c2bd6c..f4dc8ebf7 100644
--- 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
index 000000000..2f1c35844
--- /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)
-- 
2.30.2