summaryrefslogtreecommitdiff
path: root/src/theory/strings/theory_strings_preprocess.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/theory_strings_preprocess.cpp')
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp137
1 files changed, 127 insertions, 10 deletions
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 6272ad129..da8c457d2 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -217,8 +217,58 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
Node sx = nm->mkNode(STRING_SUBSTR, itost, x, d_one);
Node ux = nm->mkNode(APPLY_UF, u, x);
Node ux1 = nm->mkNode(APPLY_UF, u, xPlusOne);
- Node c0 = nm->mkNode(STRING_CODE, nm->mkConst(String("0")));
- Node c = nm->mkNode(MINUS, nm->mkNode(STRING_CODE, sx), c0);
+
+ Node c;
+ if (options::useCode())
+ {
+ Node c0 = nm->mkNode(STRING_CODE, nm->mkConst(String("0")));
+ c = nm->mkNode(MINUS, nm->mkNode(STRING_CODE, sx), c0);
+ }
+ else
+ {
+ c = nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("0"))),
+ nm->mkConst(Rational(0)),
+ nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("1"))),
+ nm->mkConst(Rational(1)),
+ nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("2"))),
+ nm->mkConst(Rational(2)),
+ nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("3"))),
+ nm->mkConst(Rational(3)),
+ nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("4"))),
+ nm->mkConst(Rational(4)),
+ nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("5"))),
+ nm->mkConst(Rational(5)),
+ nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("6"))),
+ nm->mkConst(Rational(6)),
+ nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("7"))),
+ nm->mkConst(Rational(7)),
+ nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("8"))),
+ nm->mkConst(Rational(8)),
+ nm->mkNode(kind::ITE,
+ sx.eqNode(nm->mkConst(
+ String("9"))),
+ nm->mkConst(Rational(9)),
+ nm->mkConst(Rational(
+ -1))))))))))));
+ }
Node ten = nm->mkConst(Rational(10));
Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux)));
@@ -227,7 +277,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
Node cb = nm->mkNode(
AND,
nm->mkNode(GEQ, c, nm->mkNode(ITE, leadingZeroPos, d_one, d_zero)),
- nm->mkNode(LT, c, ten));
+ options::useCode() ? nm->mkNode(LT, c, ten) : nm->mkConst(true));
Node ux1lem = nm->mkNode(GEQ, n, ux1);
@@ -280,13 +330,29 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
Node kc1 = nm->mkNode(GEQ, k, d_zero);
Node kc2 = nm->mkNode(LT, k, lens);
Node c0 = nm->mkNode(STRING_CODE, nm->mkConst(String("0")));
- Node codeSk = nm->mkNode(
- MINUS,
- nm->mkNode(STRING_CODE, nm->mkNode(STRING_SUBSTR, s, k, d_one)),
- c0);
+ Node sk = nm->mkNode(STRING_SUBSTR, s, k, d_one);
+ Node codeSk = nm->mkNode(MINUS, nm->mkNode(STRING_CODE, sk), c0);
Node ten = nm->mkConst(Rational(10));
Node kc3 = nm->mkNode(
OR, nm->mkNode(LT, codeSk, d_zero), nm->mkNode(GEQ, codeSk, ten));
+
+ if (!options::useCode())
+ {
+ NodeBuilder<> nb(OR);
+ nb << sk.eqNode(nm->mkConst(String("0")));
+ nb << sk.eqNode(nm->mkConst(String("1")));
+ nb << sk.eqNode(nm->mkConst(String("2")));
+ nb << sk.eqNode(nm->mkConst(String("3")));
+ nb << sk.eqNode(nm->mkConst(String("4")));
+ nb << sk.eqNode(nm->mkConst(String("5")));
+ nb << sk.eqNode(nm->mkConst(String("6")));
+ nb << sk.eqNode(nm->mkConst(String("7")));
+ nb << sk.eqNode(nm->mkConst(String("8")));
+ nb << sk.eqNode(nm->mkConst(String("9")));
+ kc3 = nb;
+ kc3 = kc3.negate();
+ }
+
conc1.push_back(nm->mkNode(OR, sEmpty, nm->mkNode(AND, kc1, kc2, kc3)));
std::vector<Node> conc2;
@@ -310,11 +376,62 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
Node sx = nm->mkNode(STRING_SUBSTR, s, x, d_one);
Node ux = nm->mkNode(APPLY_UF, u, x);
Node ux1 = nm->mkNode(APPLY_UF, u, nm->mkNode(PLUS, x, d_one));
- Node c = nm->mkNode(MINUS, nm->mkNode(STRING_CODE, sx), c0);
+
+ Node c;
+ if (options::useCode())
+ {
+ c = nm->mkNode(MINUS, nm->mkNode(STRING_CODE, sx), c0);
+ }
+ else
+ {
+ c = nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("0"))),
+ nm->mkConst(Rational(0)),
+ nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("1"))),
+ nm->mkConst(Rational(1)),
+ nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("2"))),
+ nm->mkConst(Rational(2)),
+ nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("3"))),
+ nm->mkConst(Rational(3)),
+ nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("4"))),
+ nm->mkConst(Rational(4)),
+ nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("5"))),
+ nm->mkConst(Rational(5)),
+ nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("6"))),
+ nm->mkConst(Rational(6)),
+ nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("7"))),
+ nm->mkConst(Rational(7)),
+ nm->mkNode(
+ kind::ITE,
+ sx.eqNode(nm->mkConst(String("8"))),
+ nm->mkConst(Rational(8)),
+ nm->mkNode(kind::ITE,
+ sx.eqNode(nm->mkConst(
+ String("9"))),
+ nm->mkConst(Rational(9)),
+ nm->mkConst(Rational(
+ -1))))))))))));
+ }
Node eq = ux1.eqNode(nm->mkNode(PLUS, c, nm->mkNode(MULT, ten, ux)));
- Node cb =
- nm->mkNode(AND, nm->mkNode(GEQ, c, d_zero), nm->mkNode(LT, c, ten));
+ Node cb = options::useCode() ? nm->mkNode(
+ AND, nm->mkNode(GEQ, c, d_zero), nm->mkNode(LT, c, ten))
+ : nm->mkNode(GEQ, c, d_zero);
Node ux1lem = nm->mkNode(GEQ, stoit, ux1);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback