diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-23 14:13:42 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-23 14:13:42 -0800 |
commit | 103e507ae0399532ec121c33a768ca8facb9e17d (patch) | |
tree | 84e8216ce38cf68f525780542ad8edc13ee76b17 | |
parent | 2454fb6c534ad9ed4a7140a09b3e334b98e1b81f (diff) |
Add trace statements
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 026280bde..9799b8736 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1939,6 +1939,7 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { { Node ret = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, mkConcat(kind::STRING_CONCAT, nc1), node[1]); + Trace("strip-constant-endpoints") << node << " ---> " << ret << std::endl; return returnRewrite(node, ret, "ctn-strip-endpt"); } @@ -2339,6 +2340,7 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) { { Node ret = mkConcat(kind::STRING_CONCAT, children0); ret = nm->mkNode(STRING_STRIDOF, ret, node[1], node[2]); + Trace("strip-constant-endpoints") << node << " ---> " << ret << std::endl; // For example: // str.indexof( str.++( x, "A" ), "B", 0 ) ---> str.indexof( x, "B", 0 ) return returnRewrite(node, ret, "rpl-pull-endpt"); @@ -2574,6 +2576,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { node[2])); cc.insert(cc.end(), ce.begin(), ce.end()); Node ret = mkConcat(kind::STRING_CONCAT, cc); + Trace("strip-constant-endpoints") << node << " ---> " << ret << std::endl; return returnRewrite(node, ret, "rpl-pull-endpt"); } } |