diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-02 17:27:30 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-02 17:27:30 -0800 |
| commit | 92122506d8f98e8901e49a2813580cfe6b637944 (patch) | |
| tree | d242a0c6ff0c260abfed9163766cd51d3b44f13a | |
| parent | 9cd2bcd32a50792d284ad31d8da86034fb55c241 (diff) | |
minor
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 11 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 4 |
2 files changed, 12 insertions, 3 deletions
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 0232b281b..9ff73b255 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -186,7 +186,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { std::vector<Node> conc; std::vector< TypeNode > argTypes; argTypes.push_back(nm->integerType()); - Node u = nm->mkSkolem("U", nm->mkFunctionType(argTypes, nm->integerType())); + Node u = d_sc->mkTypedSkolemCached( + nm->mkFunctionType(argTypes, nm->integerType()), + itost, + SkolemCache::SK_STOI_U, + "U"); Node us = nm->mkSkolem("Us", nm->mkFunctionType(argTypes, nm->stringType())); Node ud = @@ -200,12 +204,17 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { lem = d_zero.eqNode(nm->mkNode(APPLY_UF, u, d_zero)); conc.push_back(lem); + + lem = nm->mkNode(LEQ, leni, nm->mkNode(PLUS, n, d_one)); + conc.push_back(lem); + /* lem = d_empty_str.eqNode(nm->mkNode(APPLY_UF, us, leni)); conc.push_back(lem); lem = itost.eqNode(nm->mkNode(APPLY_UF, us, d_zero)); conc.push_back(lem); + */ Node x = nm->mkBoundVar(nm->integerType()); Node xPlusOne = nm->mkNode(PLUS, x, d_one); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index e7255c63f..bd570b446 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1677,6 +1677,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } } } + /* else if (checkEntailLengthOne(node[0])) { Node negOne = nm->mkConst(Rational(-1)); @@ -1685,14 +1686,13 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { Node c0 = nm->mkNode(STRING_CODE, nm->mkConst(String("0"))); Node c = nm->mkNode(MINUS, nm->mkNode(STRING_CODE, node[0]), c0); - /* retNode = nm->mkNode( ITE, nm->mkNode(AND, nm->mkNode(LEQ, zero, c), nm->mkNode(LT, c, ten)), c, negOne); - */ } + */ } else if (nk == kind::STRING_IN_REGEXP) { |