summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/strings_options.toml9
-rw-r--r--src/theory/strings/sequences_rewriter.cpp3
-rw-r--r--src/theory/strings/theory_strings.cpp1
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp137
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<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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback