From aca0cef5cf1bcb882dce927a64917aa800dd8b27 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 30 Jul 2019 09:57:33 -0500 Subject: Minor improvement for rewriter for str.replace (#3124) --- src/theory/strings/theory_strings_rewriter.cpp | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) (limited to 'src/theory/strings') 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 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"); -- cgit v1.2.3