These rewrites introduce the possibility of non-termination in the rewriter, as demonstrated in the included regression.
Instead, these rewrites are now moved to the extended rewriter.
#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
+#include "theory/strings/arith_entail.h"
#include "theory/strings/sequences_rewriter.h"
+#include "theory/strings/word.h"
#include "theory/theory.h"
using namespace cvc5::kind;
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
+ d_zero = NodeManager::currentNM()->mkConst(Rational(0));
}
void ExtendedRewriter::setCache(Node n, Node ret) const
return false;
}
-Node ExtendedRewriter::extendedRewriteStrings(Node ret) const
+Node ExtendedRewriter::extendedRewriteStrings(Node node) const
{
- Node new_ret;
Trace("q-ext-rewrite-debug")
- << "Extended rewrite strings : " << ret << std::endl;
+ << "Extended rewrite strings : " << node << std::endl;
- if (ret.getKind() == EQUAL)
+ Kind k = node.getKind();
+ if (k == EQUAL)
{
strings::SequencesRewriter sr(&d_rew, nullptr);
- new_ret = sr.rewriteEqualityExt(ret);
+ return sr.rewriteEqualityExt(node);
}
+ else if (k == STRING_SUBSTR)
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ Node tot_len = d_rew.rewrite(nm->mkNode(STRING_LENGTH, node[0]));
+ strings::ArithEntail aent(&d_rew);
+ // (str.substr s x y) --> "" if x < len(s) |= 0 >= y
+ Node n1_lt_tot_len = d_rew.rewrite(nm->mkNode(LT, node[1], tot_len));
+ if (aent.checkWithAssumption(n1_lt_tot_len, d_zero, node[2], false))
+ {
+ Node ret = strings::Word::mkEmptyWord(node.getType());
+ debugExtendedRewrite(node, ret, "SS_START_ENTAILS_ZERO_LEN");
+ return ret;
+ }
- return new_ret;
+ // (str.substr s x y) --> "" if 0 < y |= x >= str.len(s)
+ Node non_zero_len = d_rew.rewrite(nm->mkNode(LT, d_zero, node[2]));
+ if (aent.checkWithAssumption(non_zero_len, node[1], tot_len, false))
+ {
+ Node ret = strings::Word::mkEmptyWord(node.getType());
+ debugExtendedRewrite(node, ret, "SS_NON_ZERO_LEN_ENTAILS_OOB");
+ return ret;
+ }
+ // (str.substr s x y) --> "" if x >= 0 |= 0 >= str.len(s)
+ Node geq_zero_start = d_rew.rewrite(nm->mkNode(GEQ, node[1], d_zero));
+ if (aent.checkWithAssumption(geq_zero_start, d_zero, tot_len, false))
+ {
+ Node ret = strings::Word::mkEmptyWord(node.getType());
+ debugExtendedRewrite(node, ret, "SS_GEQ_ZERO_START_ENTAILS_EMP_S");
+ return ret;
+ }
+ }
+
+ return Node::null();
}
void ExtendedRewriter::debugExtendedRewrite(Node n,
* may be applied as a preprocessing step.
*/
bool d_aggr;
- /** true/false nodes */
+ /** Common constant nodes */
Node d_true;
Node d_false;
+ Node d_zero;
};
} // namespace quantifiers
* checkWithAssumption(x + (str.len y) = 0, 0, x, false) = true
*
* Because: x = -(str.len y), so 0 >= x --> 0 >= -(str.len y) --> true
+ *
+ * Since this method rewrites on rewriting and may introduce new variables
+ * (slack variables for inequalities), it should *not* be called from the
+ * main rewriter of strings, or non-termination can occur.
*/
bool checkWithAssumption(Node assumption,
Node a,
* checkWithAssumptions([x + (str.len y) = 0], 0, x, false) = true
*
* Because: x = -(str.len y), so 0 >= x --> 0 >= -(str.len y) --> true
+ *
+ * Since this method rewrites on rewriting and may introduce new variables
+ * (slack variables for inequalities), it should *not* be called from the
+ * main rewriter of strings, or non-termination can occur.
*/
bool checkWithAssumptions(std::vector<Node> assumptions,
Node a,
}
}
+ // (str.substr s x x) ---> "" if (str.len s) <= 1
+ if (node[1] == node[2] && d_stringsEntail.checkLengthOne(node[0]))
+ {
+ Node ret = Word::mkEmptyWord(node.getType());
+ return returnRewrite(node, ret, Rewrite::SS_LEN_ONE_Z_Z);
+ }
+
// symbolic length analysis
for (unsigned r = 0; r < 2; r++)
{
d_arithEntail.rewrite(nm->mkNode(kind::MINUS, tot_len, end_pt));
}
}
-
- // (str.substr s x y) --> "" if x < len(s) |= 0 >= y
- Node n1_lt_tot_len =
- d_arithEntail.rewrite(nm->mkNode(kind::LT, node[1], tot_len));
- if (d_arithEntail.checkWithAssumption(
- n1_lt_tot_len, zero, node[2], false))
- {
- Node ret = Word::mkEmptyWord(node.getType());
- return returnRewrite(node, ret, Rewrite::SS_START_ENTAILS_ZERO_LEN);
- }
-
- // (str.substr s x y) --> "" if 0 < y |= x >= str.len(s)
- Node non_zero_len =
- d_arithEntail.rewrite(nm->mkNode(kind::LT, zero, node[2]));
- if (d_arithEntail.checkWithAssumption(
- non_zero_len, node[1], tot_len, false))
- {
- Node ret = Word::mkEmptyWord(node.getType());
- return returnRewrite(node, ret, Rewrite::SS_NON_ZERO_LEN_ENTAILS_OOB);
- }
-
- // (str.substr s x y) --> "" if x >= 0 |= 0 >= str.len(s)
- Node geq_zero_start =
- d_arithEntail.rewrite(nm->mkNode(kind::GEQ, node[1], zero));
- if (d_arithEntail.checkWithAssumption(
- geq_zero_start, zero, tot_len, false))
- {
- Node ret = Word::mkEmptyWord(node.getType());
- return returnRewrite(
- node, ret, Rewrite::SS_GEQ_ZERO_START_ENTAILS_EMP_S);
- }
-
- // (str.substr s x x) ---> "" if (str.len s) <= 1
- if (node[1] == node[2] && d_stringsEntail.checkLengthOne(node[0]))
- {
- Node ret = Word::mkEmptyWord(node.getType());
- return returnRewrite(node, ret, Rewrite::SS_LEN_ONE_Z_Z);
- }
}
if (!curr.isNull())
{
regress1/strings/nf-ff-contains-abs.smt2
regress1/strings/no-lazy-pp-quant.smt2
regress1/strings/non_termination_regular_expression4.smt2
+ regress1/strings/non-terminating-rewrite-aent.smt2
regress1/strings/norn-13.smt2
regress1/strings/norn-360.smt2
regress1/strings/norn-ab.smt2
--- /dev/null
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () String)
+(declare-fun b () String)
+(declare-fun c () String)
+(assert
+(let ((_let_1 (str.len a))) (let ((_let_2 (str.len b))) (let ((_let_3 (+ _let_1 (* (- 1) _let_2)))) (let ((_let_4 (ite (>= _let_3 1) (str.substr a 0 _let_3) (str.substr b 0 (+ (* (- 1) _let_1) _let_2))))) (let ((_let_5 (str.len _let_4))) (let ((_let_6 (str.len c))) (let ((_let_7 (+ _let_6 (* (- 1) _let_5)))) (let ((_let_8 (ite (>= _let_7 0) (str.substr c _let_5 _let_7) (str.substr _let_4 _let_6 (+ (* (- 1) _let_6) _let_5))))) (let ((_let_9 (str.len _let_8))) (let ((_let_10 (ite (>= _let_1 _let_9) (str.substr a _let_9 (- _let_1 _let_9)) (str.substr _let_8 _let_1 (- _let_9 _let_1))))) (and (= _let_8 (str.++ a _let_10)) (not (= "" _let_10)) (>= (str.len _let_10) 1))))))))))))
+)
+(check-sat)
a,
d_nodeManager->mkNode(kind::PLUS, x, d_nodeManager->mkConst(Rational(1))),
x);
- res = sr.rewriteSubstr(n);
- ASSERT_EQ(res, empty);
+ sameNormalForm(n, empty);
// (str.substr "A" (+ x (str.len s2)) x) -> ""
n = d_nodeManager->mkNode(
d_nodeManager->mkNode(
kind::PLUS, x, d_nodeManager->mkNode(kind::STRING_LENGTH, s)),
x);
- res = sr.rewriteSubstr(n);
- ASSERT_EQ(res, empty);
+ sameNormalForm(n, empty);
// (str.substr "A" x y) -> (str.substr "A" x y)
n = d_nodeManager->mkNode(kind::STRING_SUBSTR, a, x, y);
abcd,
d_nodeManager->mkNode(kind::PLUS, x, three),
x);
- res = sr.rewriteSubstr(n);
- ASSERT_EQ(res, empty);
+ sameNormalForm(n, empty);
// (str.substr "ABCD" (+ x 2) x) -> (str.substr "ABCD" (+ x 2) x)
n = d_nodeManager->mkNode(
kind::STRING_SUBSTR, abcd, d_nodeManager->mkNode(kind::PLUS, x, two), x);
res = sr.rewriteSubstr(n);
- ASSERT_EQ(res, n);
+ sameNormalForm(res, n);
// (str.substr (str.substr s x x) x x) -> ""
n = d_nodeManager->mkNode(kind::STRING_SUBSTR,
projects / cvc5.git / commitdiff