diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-03-26 19:27:31 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-26 21:27:31 -0500 |
commit | 6a656809c353776c9de9580b19a6de79ef5a76d4 (patch) | |
tree | 74a8c90517ec1711dcc4faa65c0620ffe298b9de /src | |
parent | ab70f7a01939515792221b33372ec994bd425fde (diff) |
Better normalization of string concatenation (#1719)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 78 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 17 |
2 files changed, 95 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 0777d696f..1c885434c 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -17,6 +17,7 @@ #include "theory/strings/theory_strings_rewriter.h" #include <stdint.h> +#include <algorithm> #include "options/strings_options.h" #include "smt/logic_exception.h" @@ -348,6 +349,32 @@ Node TheoryStringsRewriter::rewriteConcat(Node node) if( !preNode.isNull() && ( preNode.getKind()!=kind::CONST_STRING || !preNode.getConst<String>().isEmptyString() ) ){ node_vec.push_back( preNode ); } + + // Sort adjacent operands in str.++ that all result in the same string or the + // empty string. + // + // E.g.: (str.++ ... (str.replace "A" x "") "A" (str.substr "A" 0 z) ...) --> + // (str.++ ... [sort those 3 arguments] ... ) + size_t lastIdx = 0; + Node lastX; + for (size_t i = 0; i < node_vec.size(); i++) + { + Node s = getStringOrEmpty(node_vec[i]); + bool nextX = false; + if (s != lastX) + { + nextX = true; + } + + if (nextX) + { + std::sort(node_vec.begin() + lastIdx, node_vec.begin() + i); + lastX = s; + lastIdx = i; + } + } + std::sort(node_vec.begin() + lastIdx, node_vec.end()); + retNode = mkConcat( kind::STRING_CONCAT, node_vec ); Trace("strings-prerewrite") << "Strings::rewriteConcat end " << retNode << std::endl; @@ -3280,6 +3307,57 @@ Node TheoryStringsRewriter::mkSubstrChain(Node base, return base; } +Node TheoryStringsRewriter::getStringOrEmpty(Node n) +{ + NodeManager* nm = NodeManager::currentNM(); + Node res; + while (res.isNull()) + { + switch (n.getKind()) + { + case kind::STRING_STRREPL: + { + Node empty = nm->mkConst(::CVC4::String("")); + if (n[0] == empty) + { + // (str.replace "" x y) --> y + n = n[2]; + break; + } + + Node strlen = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n[0])); + if (strlen == nm->mkConst(Rational(1)) && n[2] == empty) + { + // (str.replace "A" x "") --> "A" + res = n[0]; + break; + } + + res = n; + break; + } + case kind::STRING_SUBSTR: + { + Node strlen = Rewriter::rewrite(nm->mkNode(kind::STRING_LENGTH, n[0])); + if (strlen == nm->mkConst(Rational(1))) + { + // (str.substr "A" x y) --> "A" + res = n[0]; + break; + } + res = n; + break; + } + default: + { + res = n; + break; + } + } + } + return res; +} + Node TheoryStringsRewriter::returnRewrite(Node node, Node ret, const char* c) { Trace("strings-rewrite") << "Rewrite " << node << " to " << ret << " by " << c diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 0e4cb594a..9671fa815 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -437,6 +437,23 @@ private: static Node mkSubstrChain(Node base, const std::vector<Node>& ss, const std::vector<Node>& ls); + + /** + * Overapproximates the possible values of node n. This overapproximation + * assumes that n can return a value x or the empty string and tries to find + * the simplest x such that this holds. In the general case, x is the same as + * the input n. This overapproximation can be used to sort terms with the + * same possible values in string concatenation for example. + * + * Example: + * + * getStringOrEmpty( (str.replace "" x y) ) --> y because (str.replace "" x y) + * either returns y or "" + * + * getStringOrEmpty( (str.substr "ABC" x y) ) --> (str.substr "ABC" x y) + * because the function could not compute a simpler + */ + static Node getStringOrEmpty(Node n); };/* class TheoryStringsRewriter */ }/* CVC4::theory::strings namespace */ |