diff options
Diffstat (limited to 'src/theory/strings/theory_strings_preprocess.cpp')
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 137 |
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 5fc13f023..c4576326a 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -223,8 +223,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_TO_CODE, nm->mkConst(String("0"))); - Node c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_CODE, sx), c0); + + Node c; + if (options::useCode()) + { + Node c0 = nm->mkNode(STRING_TO_CODE, nm->mkConst(String("0"))); + c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_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))); @@ -233,7 +283,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); @@ -287,13 +337,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_TO_CODE, nm->mkConst(String("0"))); - Node codeSk = nm->mkNode( - MINUS, - nm->mkNode(STRING_TO_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_TO_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; @@ -317,11 +383,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_TO_CODE, sx), c0); + + Node c; + if (options::useCode()) + { + c = nm->mkNode(MINUS, nm->mkNode(STRING_TO_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); |