diff options
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 3 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 30 | ||||
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue2060.smt2 | 20 |
4 files changed, 52 insertions, 2 deletions
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) |