diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-05 18:03:02 -0800 |
---|---|---|
committer | Andres Noetzli <noetzli@stanford.edu> | 2020-01-09 17:20:09 -0800 |
commit | 7abcfca172c02d701849c3c3fda2686a2b9224a4 (patch) | |
tree | 5efe1abb18db2601f4d6f7924501830766f6ecbe | |
parent | 2ac7e8c916bfb33eb73cd90b20a92bef7036ac6b (diff) |
Option for toggling str.codeijcar2020
-rw-r--r-- | src/options/strings_options.toml | 9 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 1 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 137 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 2 |
4 files changed, 138 insertions, 11 deletions
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 3916c68f3..98c26c79a 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -252,3 +252,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/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 1bc104096..4c4e1a2fe 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -4097,6 +4097,7 @@ void TheoryStrings::registerTerm( Node n, int effort ) { } else if (n.getKind() == STRING_CODE) { + AlwaysAssert(options::useCode()) << n; d_has_str_code = true; // ite( str.len(s)==1, 0 <= str.code(s) < num_codes, 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 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); diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index f17944027..02bd08cc1 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1473,7 +1473,7 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { }else if(r.getKind() == kind::STRING_TO_REGEXP) { retNode = x.eqNode(r[0]); } - 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_CODE, x); |