diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-04-30 14:11:16 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-04-30 14:11:16 -0500 |
commit | d36423fb74e3ec294b222b806cb24b5229e72ed1 (patch) | |
tree | c78260dd402be419cdc49e27f0cdb15ed14c7b08 | |
parent | 6538957335ecf83af38150054cf80555a57e72d0 (diff) |
Remove stoi solve rewrite (#2985)
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 27 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
-rw-r--r-- | test/regress/regress1/strings/issue2981.smt2 | 20 | ||||
-rw-r--r-- | test/regress/regress1/strings/stoi-solve.smt2 (renamed from test/regress/regress0/strings/stoi-solve.smt2) | 0 |
4 files changed, 25 insertions, 25 deletions
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/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/regress0/strings/stoi-solve.smt2 b/test/regress/regress1/strings/stoi-solve.smt2 index 4fbbdcfc1..4fbbdcfc1 100644 --- a/test/regress/regress0/strings/stoi-solve.smt2 +++ b/test/regress/regress1/strings/stoi-solve.smt2 |