diff options
author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-07-27 20:16:41 -0500 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-07-27 20:16:41 -0500 |
commit | 9f10a95e26e9e790a19a6f9e68a658ec2ab6d304 (patch) | |
tree | a94bc67c55196d574a98d8a35b3fdd65519afd6d | |
parent | bfb9c562ac509a0c7b00e53c17aab5cda83129ac (diff) |
Hotfix for substr function.
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 5bf44dce8..b5e741edd 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -866,15 +866,15 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } else if(node.getKind() == kind::STRING_LENGTH) { if(node[0].isConst()) { retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) ); - } /*else if(node[0].getKind() == kind::STRING_SUBSTR_TOTAL) { + } else if(node[0].getKind() == kind::STRING_SUBSTR_TOTAL) { retNode = node[0][2]; - }*/ else if(node[0].getKind() == kind::STRING_CONCAT) { + } else if(node[0].getKind() == kind::STRING_CONCAT) { Node tmpNode = rewriteConcatString(node[0]); if(tmpNode.isConst()) { retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst<String>().size() ) ); - } /*else if(tmpNode.getKind() == kind::STRING_SUBSTR_TOTAL) { - retNode = tmpNode[2]; - }*/ else { + } else if(tmpNode.getKind() == kind::STRING_SUBSTR_TOTAL) { + retNode = tmpNode[2]; + } else { // it has to be string concat std::vector<Node> node_vec; for(unsigned int i=0; i<tmpNode.getNumChildren(); ++i) { |