From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 30 Apr 2019 19:11:16 +0000 (-0500)
Subject: Remove stoi solve rewrite (#2985)
X-Git-Tag: cvc5-1.0.0~4158
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d36423fb74e3ec294b222b806cb24b5229e72ed1;p=cvc5.git

Remove stoi solve rewrite (#2985)
---

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 2e50ade0c..47f29e814 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -599,30 +599,9 @@ Node TheoryStringsRewriter::rewriteArithEqualityExt(Node node)
 {
   Assert(node.getKind() == EQUAL && node[0].getType().isInteger());
 
-  NodeManager* nm = NodeManager::currentNM();
-
   // cases where we can solve the equality
-  for (unsigned i = 0; i < 2; i++)
-  {
-    if (node[i].isConst())
-    {
-      Node on = node[1 - i];
-      Kind onk = on.getKind();
-      if (onk == STRING_STOI)
-      {
-        Rational r = node[i].getConst<Rational>();
-        int sgn = r.sgn();
-        Node onEq;
-        std::stringstream ss;
-        if (sgn >= 0)
-        {
-          ss << r.getNumerator();
-        }
-        Node new_ret = on[0].eqNode(nm->mkConst(String(ss.str())));
-        return returnRewrite(node, new_ret, "stoi-solve");
-      }
-    }
-  }
+
+  // notice we cannot rewrite str.to.int(x)=n to x="n" due to leading zeroes.
 
   return node;
 }
@@ -1490,7 +1469,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
       if(s.isNumber()) {
         retNode = nm->mkConst(s.toNumber());
       } else {
-        retNode = nm->mkConst(::CVC4::Rational(-1));
+        retNode = nm->mkConst(Rational(-1));
       }
     } else if(node[0].getKind() == kind::STRING_CONCAT) {
       for(unsigned i=0; i<node[0].getNumChildren(); ++i) {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c9514dd76..d8adbb59e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -846,7 +846,6 @@ set(regress_0_tests
   regress0/strings/rewrites-re-concat.smt2
   regress0/strings/rewrites-v2.smt2
   regress0/strings/std2.6.1.smt2
-  regress0/strings/stoi-solve.smt2
   regress0/strings/str003.smt2
   regress0/strings/str004.smt2
   regress0/strings/str005.smt2
@@ -1537,6 +1536,7 @@ set(regress_1_tests
   regress1/strings/issue1684-regex.smt2
   regress1/strings/issue2060.smt2
   regress1/strings/issue2429-code.smt2
+  regress1/strings/issue2981.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2
@@ -1569,6 +1569,7 @@ set(regress_1_tests
   regress1/strings/replaceall-replace.smt2
   regress1/strings/rew-020618.smt2
   regress1/strings/stoi-400million.smt2
+  regress1/strings/stoi-solve.smt2
   regress1/strings/str-code-sat.smt2
   regress1/strings/str-code-unsat-2.smt2
   regress1/strings/str-code-unsat-3.smt2
diff --git a/test/regress/regress0/strings/stoi-solve.smt2 b/test/regress/regress0/strings/stoi-solve.smt2
deleted file mode 100644
index 4fbbdcfc1..000000000
--- a/test/regress/regress0/strings/stoi-solve.smt2
+++ /dev/null
@@ -1,6 +0,0 @@
-(set-logic ALL)
-(set-info :status sat)
-(set-option :strings-exp true)
-(declare-fun x () String)
-(assert (= (str.to.int x) 12345)) 
-(check-sat)
diff --git a/test/regress/regress1/strings/issue2981.smt2 b/test/regress/regress1/strings/issue2981.smt2
new file mode 100644
index 000000000..78cdb2a8c
--- /dev/null
+++ b/test/regress/regress1/strings/issue2981.smt2
@@ -0,0 +1,20 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_SLIA)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-const x String)
+(declare-const y String)
+(declare-const m String)
+(declare-const n String)
+(assert (str.in.re x (re.+ (re.range "0" "9"))))
+(assert (= 0 (str.to.int x)))                   
+(assert (not (= x ""))) 
+(assert (not (= x "0")))
+(assert (not (= x "3")))
+(assert (not (= x "T")))
+(assert (not (= x "8")))
+(assert (not (= x ""))) 
+(assert (not (= x "5")))
+(assert (not (= x "<")))
+(assert (not (= x "N")))               
+(check-sat)
diff --git a/test/regress/regress1/strings/stoi-solve.smt2 b/test/regress/regress1/strings/stoi-solve.smt2
new file mode 100644
index 000000000..4fbbdcfc1
--- /dev/null
+++ b/test/regress/regress1/strings/stoi-solve.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-info :status sat)
+(set-option :strings-exp true)
+(declare-fun x () String)
+(assert (= (str.to.int x) 12345)) 
+(check-sat)