Option for toggling str.codeijcar2020

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);