From c4905e4aa2ec70929335497130f802254a0d4b4e Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 13 Jun 2018 13:36:22 -0500
Subject: [PATCH] Fix simple regexp consume (#2066)

---
 .../strings/theory_strings_rewriter.cpp       |  3 +-
 src/theory/strings/theory_strings_rewriter.h  | 30 ++++++++++++++++++-
 test/regress/Makefile.tests                   |  1 +
 test/regress/regress1/strings/issue2060.smt2  | 20 +++++++++++++
 4 files changed, 52 insertions(+), 2 deletions(-)
 create mode 100644 test/regress/regress1/strings/issue2060.smt2

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 78def9c0a..4ab81da7c 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -31,6 +31,7 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::strings;
 
 Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren, std::vector< Node >& children, int dir ){
+  NodeManager* nm = NodeManager::currentNM();
   unsigned tmin = dir<0 ? 0 : dir;
   unsigned tmax = dir<0 ? 1 : dir;
   //try to remove off front and back
@@ -61,7 +62,7 @@ Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren,
               if( index==0 ){
                 mchildren.push_back( s );
               }else{
-                children.push_back( s );
+                children.push_back(nm->mkNode(STRING_TO_REGEXP, s));
               }
             }
             do_next = true;
diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index 8befb5e0f..4c78a1945 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -28,7 +28,35 @@ namespace theory {
 namespace strings {
 
 class TheoryStringsRewriter {
-private:
+ private:
+  /** simple regular expression consume
+   *
+   * This method is called when we are rewriting a membership of the form
+   *   s1 ++ ... ++ sn in r1 ++ ... ++ rm
+   * We have that mchildren consists of the strings s1...sn, and children
+   * consists of the regular expressions r1...rm.
+   *
+   * This method tries to strip off parts of the concatenation terms. It updates
+   * the vectors such that the resulting vectors are such that the membership
+   * mchildren[n'...n''] in children[m'...m''] is equivalent to the input
+   * membership. The argument dir indicates the direction to consider, where
+   * 0 means strip off the front, 1 off the back, and < 0 off of both.
+   *
+   * If this method returns the false node, then we have inferred that the input
+   * membership is equivalent to false. Otherwise, it returns the null node.
+   *
+   * For example, given input
+   *   mchildren = { "ab", x }, children = { [["a"]], ([["cd"]])* } and dir = 0,
+   * this method updates:
+   *   mchildren = { "b", x }, children = { ("cd")* }
+   * and returns null.
+   *
+   * For example, given input
+   *   { x, "abb", x }, { [[x]], ["a"..."b"], allchar, [[y]], [[x]]} and dir=-1,
+   * this method updates:
+   *   { "b" }, { [[y]] }
+   * where [[.]] denotes str.to.re, and returns null.
+   */
   static Node simpleRegexpConsume( std::vector< Node >& mchildren, std::vector< Node >& children, int dir = -1 );
   static bool isConstRegExp( TNode t );
   static bool testConstStringInRegExp( CVC4::String &s, unsigned int index_start, TNode r );
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index fd4a7da39..41753720f 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1444,6 +1444,7 @@ REG1_TESTS = \
 	regress1/strings/idof-triv.smt2 \
 	regress1/strings/ilc-l-nt.smt2 \
 	regress1/strings/issue1105.smt2 \
+	regress1/strings/issue2060.smt2 \
 	regress1/strings/kaluza-fl.smt2 \
 	regress1/strings/loop002.smt2 \
 	regress1/strings/loop003.smt2 \
diff --git a/test/regress/regress1/strings/issue2060.smt2 b/test/regress/regress1/strings/issue2060.smt2
new file mode 100644
index 000000000..784fe1862
--- /dev/null
+++ b/test/regress/regress1/strings/issue2060.smt2
@@ -0,0 +1,20 @@
+(set-logic QF_S)
+(set-info :status sat)
+
+(declare-const action String)
+(declare-const example_key String)
+
+(assert (str.in.re action (re.++
+                           (str.to.re "foobar:ab")
+                           (re.* re.allchar)
+                   )))
+
+(declare-const action_1 String)
+(declare-const action_2 String)
+
+(assert (and
+         (= action (str.++ action_1 example_key action_2))
+         (= action_1 "foobar:a")
+         ))
+
+(check-sat)
-- 
2.30.2