diff options
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 18 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/strings/replace-const.smt2 | 12 |
3 files changed, 25 insertions, 6 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index d720fedc8..aac2477ea 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -2456,14 +2456,20 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { } else { - CVC4::String s1 = s.substr(0, (int)p); - CVC4::String s3 = s.substr((int)p + (int)t.size()); - Node ns1 = NodeManager::currentNM()->mkConst(::CVC4::String(s1)); - Node ns3 = NodeManager::currentNM()->mkConst(::CVC4::String(s3)); + String s1 = s.substr(0, (int)p); + String s3 = s.substr((int)p + (int)t.size()); std::vector<Node> children; - children.push_back(ns1); + if (s1.size() > 0) + { + Node ns1 = nm->mkConst(String(s1)); + children.push_back(ns1); + } children.push_back(node[2]); - children.push_back(ns3); + if (s3.size() > 0) + { + Node ns3 = nm->mkConst(String(s3)); + children.push_back(ns3); + } children.insert(children.end(), children0.begin() + 1, children0.end()); Node ret = utils::mkConcat(STRING_CONCAT, children); return returnRewrite(node, ret, "rpl-const-find"); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 90641fe2f..0ac2d4142 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -853,6 +853,7 @@ set(regress_0_tests regress0/strings/norn-simp-rew.smt2 regress0/strings/re.all.smt2 regress0/strings/repl-rewrites2.smt2 + regress0/strings/replace-const.smt2 regress0/strings/replaceall-eval.smt2 regress0/strings/rewrites-re-concat.smt2 regress0/strings/rewrites-v2.smt2 diff --git a/test/regress/regress0/strings/replace-const.smt2 b/test/regress/regress0/strings/replace-const.smt2 new file mode 100644 index 000000000..a7f225e33 --- /dev/null +++ b/test/regress/regress0/strings/replace-const.smt2 @@ -0,0 +1,12 @@ +(set-info :smt-lib-version 2.5) +(set-logic ALL) +(set-info :status sat) +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () String) + +(assert (= x (str.replace "AA" "AA" "def"))) +(assert (= y (str.replace "BAA" "B" "def"))) +(assert (= z (str.replace "AAB" "B" "def"))) + +(check-sat) |