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 /src | |
parent | 6538957335ecf83af38150054cf80555a57e72d0 (diff) |
Remove stoi solve rewrite (#2985)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 27 |
1 files changed, 3 insertions, 24 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) { |