From 383b0247470fe0553ba40dffcfc4b0fb5f30ed4b Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 5 Dec 2019 18:03:02 -0800 Subject: Option for toggling str.code --- src/options/strings_options.toml | 9 ++ src/theory/strings/sequences_rewriter.cpp | 3 +- src/theory/strings/theory_strings.cpp | 1 + src/theory/strings/theory_strings_preprocess.cpp | 137 +++++++++++++++++++++-- 4 files changed, 139 insertions(+), 11 deletions(-) diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 49c304bab..21dfcd047 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -223,3 +223,12 @@ header = "options/strings_options.h" [[option.mode.NONE]] name = "none" help = "Do not compute intersections for regular expressions." + +[[option]] + name = "useCode" + category = "expert" + long = "use-code" + type = "bool" + default = "true" + read_only = true + help = "use str.code to encode str.to.int/int.to.str/re.range" diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 152f71019..0abaa93c1 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -18,6 +18,7 @@ #include "expr/attribute.h" #include "expr/node_builder.h" +#include "options/strings_options.h" #include "theory/rewriter.h" #include "theory/strings/arith_entail.h" #include "theory/strings/regexp_entail.h" @@ -1234,7 +1235,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) Node retNode = x.eqNode(r[0]); return returnRewrite(node, retNode, Rewrite::RE_IN_CSTRING); } - else if (r.getKind() == REGEXP_RANGE) + else if (options::useCode() && r.getKind() == REGEXP_RANGE) { // x in re.range( char_i, char_j ) ---> i <= str.code(x) <= j Node xcode = nm->mkNode(STRING_TO_CODE, x); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 81e43c595..b01596e31 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1101,6 +1101,7 @@ void TheoryStrings::registerTerm(Node n, int effort) } else if (n.getKind() == STRING_TO_CODE) { + AlwaysAssert(options::useCode()) << n; d_has_str_code = true; // ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 ) Node code_len = utils::mkNLength(n[0]).eqNode(d_one); 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 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); -- cgit v1.2.3