Node ret = NodeManager::currentNM()->mkConst(false);
return returnRewrite(node, ret, Rewrite::EQ_CONST_FALSE);
}
+ // standard ordering
+ if (node[0] > node[1])
+ {
+ Node ret = NodeManager::currentNM()->mkNode(kind::EQUAL, node[1], node[0]);
+ return returnRewrite(node, ret, Rewrite::EQ_SYM);
+ }
+ return node;
+}
+Node SequencesRewriter::rewriteEqualityExt(Node node)
+{
+ Assert(node.getKind() == EQUAL);
+ TypeNode tn = node[0].getType();
+ if (tn.isInteger())
+ {
+ return rewriteArithEqualityExt(node);
+ }
+ if (tn.isStringLike())
+ {
+ return rewriteStrEqualityExt(node);
+ }
+ return node;
+}
+
+Node SequencesRewriter::rewriteStrEqualityExt(Node node)
+{
+ Assert(node.getKind() == EQUAL && node[0].getType().isStringLike());
+ TypeNode stype = node[0].getType();
+
+ NodeManager* nm = NodeManager::currentNM();
// ( ~contains( s, t ) V ~contains( t, s ) ) => ( s == t ---> false )
for (unsigned r = 0; r < 2; r++)
{
// must call rewrite contains directly to avoid infinite loop
- // we do a fix point since we may rewrite contains terms to simpler
- // contains terms.
- Node ctn = d_stringsEntail.checkContains(node[r], node[1 - r], false);
- if (!ctn.isNull())
+ Node ctn = nm->mkNode(STRING_CONTAINS, node[r], node[1 - r]);
+ ctn = rewriteContains(ctn);
+ Assert(!ctn.isNull());
+ if (ctn.isConst())
{
if (!ctn.getConst<bool>())
{
}
}
- // standard ordering
- if (node[0] > node[1])
- {
- Node ret = NodeManager::currentNM()->mkNode(kind::EQUAL, node[1], node[0]);
- return returnRewrite(node, ret, Rewrite::EQ_SYM);
- }
- return node;
-}
-
-Node SequencesRewriter::rewriteEqualityExt(Node node)
-{
- Assert(node.getKind() == EQUAL);
- if (node[0].getType().isInteger())
- {
- return rewriteArithEqualityExt(node);
- }
- if (node[0].getType().isStringLike())
- {
- return rewriteStrEqualityExt(node);
- }
- return node;
-}
-
-Node SequencesRewriter::rewriteStrEqualityExt(Node node)
-{
- Assert(node.getKind() == EQUAL && node[0].getType().isStringLike());
- TypeNode stype = node[0].getType();
-
- NodeManager* nm = NodeManager::currentNM();
- std::vector<Node> c[2];
Node new_ret;
- for (unsigned i = 0; i < 2; i++)
- {
- utils::getConcat(node[i], c[i]);
- }
// ------- equality unification
bool changed = false;
for (unsigned i = 0; i < 2; i++)
// original node was an equality but we may be able to do additional
// rewriting here, e.g.,
// x++y = "" --> x = "" and y = ""
- return returnRewrite(node, new_ret, Rewrite::STR_EQ_UNIFY, true);
+ new_ret = returnRewrite(node, new_ret, Rewrite::STR_EQ_UNIFY);
+ return rewriteStrEqualityExt(new_ret);
}
}
// original node was an equality but we may be able to do additional
// rewriting here.
new_ret = lhs.eqNode(ss);
- return returnRewrite(node, new_ret, Rewrite::STR_EQ_HOMOG_CONST, true);
+ new_ret = returnRewrite(node, new_ret, Rewrite::STR_EQ_HOMOG_CONST);
+ return rewriteStrEqualityExt(new_ret);
}
}
}
}
}
}
-
return node;
}
<< std::endl;
if (node != retNode)
{
+ // also post process the rewrite, which may apply extended rewriting to
+ // equalities, if we rewrite to an equality from a non-equality
+ retNode = postProcessRewrite(node, retNode);
Trace("strings-rewrite-debug") << "Strings::SequencesRewriter::postRewrite "
<< node << " to " << retNode << std::endl;
return RewriteResponse(REWRITE_AGAIN_FULL, retNode);
return node;
}
-Node SequencesRewriter::returnRewrite(Node node,
- Node ret,
- Rewrite r,
- bool rewriteEqAgain)
+Node SequencesRewriter::returnRewrite(Node node, Node ret, Rewrite r)
{
Trace("strings-rewrite") << "Rewrite " << node << " to " << ret << " by " << r
<< "." << std::endl;
-
- NodeManager* nm = NodeManager::currentNM();
-
if (d_statistics != nullptr)
{
(*d_statistics) << r;
}
+ return ret;
+}
+Node SequencesRewriter::postProcessRewrite(Node node, Node ret)
+{
+ NodeManager* nm = NodeManager::currentNM();
// standard post-processing
// We rewrite (string) equalities immediately here. This allows us to forego
// the standard invariant on equality rewrites (that s=t must rewrite to one
{
ret = nm->mkNode(NOT, rewriteEqualityExt(ret[0]));
}
- else if (retk == EQUAL && (rewriteEqAgain || node.getKind() != EQUAL))
+ else if (retk == EQUAL && node.getKind() != EQUAL)
{
Trace("strings-rewrite")
<< "Apply extended equality rewrite on " << ret << std::endl;
*
* The rewrite r indicates the justification for the rewrite, which is printed
* by this function for debugging.
- *
- * If node is not an equality (or rewriteEq is true) and ret is an equality,
- * this method applies an additional rewrite step (rewriteEqualityExt) that
- * performs additional rewrites on ret, after which we return the result of
- * this call. Otherwise, this method simply returns ret.
*/
- Node returnRewrite(Node node,
- Node ret,
- Rewrite r,
- bool rewriteEqAgain = false);
+ Node returnRewrite(Node node, Node ret, Rewrite r);
public:
RewriteResponse postRewrite(TNode node) override;
*/
static Node canonicalStrForSymbolicLength(Node n, TypeNode stype);
+ /**
+ * post-process rewrite
+ *
+ * If node is not an equality and ret is an equality,
+ * this method applies an additional rewrite step (rewriteEqualityExt) that
+ * performs additional rewrites on ret, after which we return the result of
+ * this call. Otherwise, this method simply returns ret.
+ */
+ Node postProcessRewrite(Node node, Node ret);
/** Reference to the rewriter statistics. */
HistogramStat<Rewrite>* d_statistics;
regress0/strings/norn-31.smt2
regress0/strings/norn-simp-rew.smt2
regress0/strings/parser-syms.cvc
- regress0/strings/quad-028-2-2-unsat.smt2
regress0/strings/re_diff.smt2
regress0/strings/re-in-rewrite.smt2
regress0/strings/re-syntax.smt2
regress1/strings/issue6057-replace-re-all-jiwonparc.smt2
regress1/strings/issue6072-inc-no-const-reg.smt2
regress1/strings/issue6075-repl-len-one-rr.smt2
+ regress1/strings/issue6101.smt2
+ regress1/strings/issue6101-2.smt2
regress1/strings/issue6132-non-unique-skolem.smt2
regress1/strings/issue6142-repl-inv-rew.smt2
regress1/strings/issue6191-replace-all.smt2
regress1/strings/issue6653-rre.smt2
regress1/strings/issue6653-rre-small.smt2
regress1/strings/issue6777-seq-nth-eval-cm.smt2
+ regress1/strings/issue6913.smt2
regress1/strings/kaluza-fl.smt2
regress1/strings/loop002.smt2
regress1/strings/loop003.smt2
regress0/auflia/fuzz01.smtv1.smt2
###
regress0/bv/test00.smtv1.smt2
+ # timeout after changes to equality rewriting policy in strings
+ regress0/strings/quad-028-2-2-unsat.smt2
# FIXME #1649
regress0/datatypes/datatype-dump.cvc
# no longer support overloaded symbols across multiple parametric datatypes
projects / cvc5.git / commitdiff