diff options
Diffstat (limited to 'src/theory/strings/strings_rewriter.cpp')
-rw-r--r-- | src/theory/strings/strings_rewriter.cpp | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index c7676d049..275c2e25e 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -41,7 +41,7 @@ Node StringsRewriter::rewriteStrToInt(Node node) { ret = nm->mkConst(Rational(-1)); } - return returnRewrite(node, ret, "stoi-eval"); + return returnRewrite(node, ret, Rewrite::STOI_EVAL); } else if (node[0].getKind() == STRING_CONCAT) { @@ -53,7 +53,7 @@ Node StringsRewriter::rewriteStrToInt(Node node) if (!t.isNumber()) { Node ret = nm->mkConst(Rational(-1)); - return returnRewrite(node, ret, "stoi-concat-nonnum"); + return returnRewrite(node, ret, Rewrite::STOI_CONCAT_NONNUM); } } } @@ -78,7 +78,7 @@ Node StringsRewriter::rewriteIntToStr(Node node) Assert(stmp[0] != '-'); ret = nm->mkConst(String(stmp)); } - return returnRewrite(node, ret, "itos-eval"); + return returnRewrite(node, ret, Rewrite::ITOS_EVAL); } return node; } @@ -114,7 +114,7 @@ Node StringsRewriter::rewriteStrConvert(Node node) nvec[i] = newChar; } Node retNode = nm->mkConst(String(nvec)); - return returnRewrite(node, retNode, "str-conv-const"); + return returnRewrite(node, retNode, Rewrite::STR_CONV_CONST); } else if (node[0].getKind() == STRING_CONCAT) { @@ -125,7 +125,7 @@ Node StringsRewriter::rewriteStrConvert(Node node) } // tolower( x1 ++ x2 ) --> tolower( x1 ) ++ tolower( x2 ) Node retNode = concatBuilder.constructNode(); - return returnRewrite(node, retNode, "str-conv-minscope-concat"); + return returnRewrite(node, retNode, Rewrite::STR_CONV_MINSCOPE_CONCAT); } else if (node[0].getKind() == STRING_TOLOWER || node[0].getKind() == STRING_TOUPPER) @@ -133,12 +133,12 @@ Node StringsRewriter::rewriteStrConvert(Node node) // tolower( tolower( x ) ) --> tolower( x ) // tolower( toupper( x ) ) --> tolower( x ) Node retNode = nm->mkNode(nk, node[0][0]); - return returnRewrite(node, retNode, "str-conv-idem"); + return returnRewrite(node, retNode, Rewrite::STR_CONV_IDEM); } else if (node[0].getKind() == STRING_ITOS) { // tolower( str.from.int( x ) ) --> str.from.int( x ) - return returnRewrite(node, node[0], "str-conv-itos"); + return returnRewrite(node, node[0], Rewrite::STR_CONV_ITOS); } return node; } @@ -150,14 +150,14 @@ Node StringsRewriter::rewriteStringLeq(Node n) if (n[0] == n[1]) { Node ret = nm->mkConst(true); - return returnRewrite(n, ret, "str-leq-id"); + return returnRewrite(n, ret, Rewrite::STR_LEQ_ID); } if (n[0].isConst() && n[1].isConst()) { String s = n[0].getConst<String>(); String t = n[1].getConst<String>(); Node ret = nm->mkConst(s.isLeq(t)); - return returnRewrite(n, ret, "str-leq-eval"); + return returnRewrite(n, ret, Rewrite::STR_LEQ_EVAL); } // empty strings for (unsigned i = 0; i < 2; i++) @@ -165,7 +165,7 @@ Node StringsRewriter::rewriteStringLeq(Node n) if (n[i].isConst() && n[i].getConst<String>().isEmptyString()) { Node ret = i == 0 ? nm->mkConst(true) : n[0].eqNode(n[1]); - return returnRewrite(n, ret, "str-leq-empty"); + return returnRewrite(n, ret, Rewrite::STR_LEQ_EMPTY); } } @@ -189,7 +189,7 @@ Node StringsRewriter::rewriteStringLeq(Node n) if (!s.isLeq(t)) { Node ret = nm->mkConst(false); - return returnRewrite(n, ret, "str-leq-cprefix"); + return returnRewrite(n, ret, Rewrite::STR_LEQ_CPREFIX); } } return n; @@ -213,7 +213,7 @@ Node StringsRewriter::rewriteStringFromCode(Node n) { ret = nm->mkConst(String("")); } - return returnRewrite(n, ret, "from-code-eval"); + return returnRewrite(n, ret, Rewrite::FROM_CODE_EVAL); } return n; } @@ -236,7 +236,7 @@ Node StringsRewriter::rewriteStringToCode(Node n) { ret = nm->mkConst(Rational(-1)); } - return returnRewrite(n, ret, "to-code-eval"); + return returnRewrite(n, ret, Rewrite::TO_CODE_EVAL); } return n; } |