summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/prop/cryptominisat.cpp22
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp44
-rw-r--r--test/unit/theory/theory_strings_rewriter_white.h72
3 files changed, 118 insertions, 20 deletions
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index c04fb8b56..970ba13cf 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -119,13 +119,23 @@ ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){
std::vector<CMSat::Lit> internal_clause;
toInternalClause(clause, internal_clause);
bool nowOkay = d_solver->add_clause(internal_clause);
- ClauseId freshId = ClauseId(ProofManager::currentPM()->nextId());
- THEORY_PROOF(
- // If this clause results in a conflict, then `nowOkay` may be false, but
- // we still need to register this clause as used. Thus, we look at
- // `d_okay` instead
- if (d_bvp && d_okay) { d_bvp->registerUsedClause(freshId, clause); })
+ ClauseId freshId;
+ if (THEORY_PROOF_ON())
+ {
+ freshId = ClauseId(ProofManager::currentPM()->nextId());
+ // If this clause results in a conflict, then `nowOkay` may be false, but
+ // we still need to register this clause as used. Thus, we look at
+ // `d_okay` instead
+ if (d_bvp && d_okay)
+ {
+ d_bvp->registerUsedClause(freshId, clause);
+ }
+ }
+ else
+ {
+ freshId = ClauseIdError;
+ }
d_okay &= nowOkay;
return freshId;
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 9799b8736..7dc486795 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -2018,13 +2018,6 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
return returnRewrite(node, ret, "ctn-mset-nss");
}
- if (checkEntailArith(len_n2, len_n1, false))
- {
- // len( n2 ) >= len( n1 ) => contains( n1, n2 ) ---> n1 = n2
- Node ret = node[0].eqNode(node[1]);
- return returnRewrite(node, ret, "ctn-len-ineq-nstrict");
- }
-
// splitting
if (node[0].getKind() == kind::STRING_CONCAT)
{
@@ -2069,14 +2062,25 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
}
else if (node[0].getKind() == kind::STRING_SUBSTR)
{
- // (str.contains (str.substr x n (str.len y)) y) --->
- // (= (str.substr x n (str.len y)) y)
- //
- // TODO: Remove with under-/over-approximation
- if (node[0][2] == nm->mkNode(kind::STRING_LENGTH, node[1]))
+ Node zero = nm->mkConst(Rational(0));
+ if (node[0][1] == zero && node[0][2].getKind() == kind::STRING_STRIDOF
+ && node[0][0] == node[0][2][0] && node[0][2][1] == node[1]
+ && node[0][2][2] == zero && checkEntailNonEmpty(node[1]))
+ {
+ Node ret = nm->mkConst(false);
+ return returnRewrite(node, ret, "ctn-substr-idof");
+ }
+
+ Node substr = node[0];
+ while (substr.getKind() == kind::STRING_SUBSTR)
{
- Node ret = nm->mkNode(kind::EQUAL, node[0], node[1]);
- return returnRewrite(node, ret, "ctn-substr");
+ substr = substr[0];
+ Node ectn = checkEntailContains(substr, node[1]);
+ if (!ectn.isNull() && !ectn.getConst<bool>())
+ {
+ Node ret = nm->mkConst(false);
+ return returnRewrite(node, ret, "ctn-substr-nested");
+ }
}
}
else if (node[0].getKind() == kind::STRING_STRREPL)
@@ -2151,6 +2155,18 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) {
}
}
+ // NOTE: This rewrite should be attempted at the end because we could miss
+ // out on other rewrites. E.g. if contains(x, y) can be rewritten to false
+ // then this rewrite might instead rewrite it to an equality and we have
+ // cannot detect that the equality is false because this rewrite applies
+ // again when we check if one side of the equality contains the other.
+ if (checkEntailArith(len_n2, len_n1, false))
+ {
+ // len( n2 ) >= len( n1 ) => contains( n1, n2 ) ---> n1 = n2
+ Node ret = node[0].eqNode(node[1]);
+ return returnRewrite(node, ret, "ctn-len-ineq-nstrict");
+ }
+
Trace("strings-rewrite-nf") << "No rewrites for : " << node << std::endl;
return node;
}
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index 59d36d9e8..760e35471 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -448,6 +448,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
Node x = d_nm->mkVar("x", strType);
Node y = d_nm->mkVar("y", strType);
Node negOne = d_nm->mkConst(Rational(-1));
+ Node zero = d_nm->mkConst(Rational(0));
Node one = d_nm->mkConst(Rational(1));
Node two = d_nm->mkConst(Rational(2));
Node three = d_nm->mkConst(Rational(3));
@@ -486,6 +487,32 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
a,
i);
sameNormalForm(idof_substr, negOne);
+
+ Node substr_idof =
+ d_nm->mkNode(kind::STRING_SUBSTR,
+ x,
+ zero,
+ d_nm->mkNode(kind::STRING_STRIDOF, x, a, zero));
+
+ // (str.indexof (str.substr x 0 (str.indexof "A" 0)) 0) ---> -1
+ {
+ Node idof = d_nm->mkNode(kind::STRING_STRIDOF, substr_idof, a, zero);
+ sameNormalForm(idof, negOne);
+ }
+
+ // (str.indexof (str.++ (str.substr (str.substr x 0 (str.indexof "A" 0)) 0
+ // 1) "B") 0) ---> -1
+ {
+ Node idof = d_nm->mkNode(
+ kind::STRING_STRIDOF,
+ d_nm->mkNode(
+ kind::STRING_CONCAT,
+ d_nm->mkNode(kind::STRING_SUBSTR, substr_idof, zero, one),
+ b),
+ a,
+ zero);
+ sameNormalForm(idof, negOne);
+ }
}
void testRewriteReplace()
@@ -634,6 +661,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
Node empty = d_nm->mkConst(::CVC4::String(""));
Node a = d_nm->mkConst(::CVC4::String("A"));
+ Node aac = d_nm->mkConst(::CVC4::String("AAC"));
Node b = d_nm->mkConst(::CVC4::String("B"));
Node c = d_nm->mkConst(::CVC4::String("C"));
Node x = d_nm->mkVar("x", strType);
@@ -642,6 +670,8 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
Node yx = d_nm->mkNode(kind::STRING_CONCAT, y, x);
Node z = d_nm->mkVar("z", strType);
Node n = d_nm->mkVar("n", intType);
+ Node m = d_nm->mkVar("m", intType);
+ Node zero = d_nm->mkConst(Rational(0));
Node one = d_nm->mkConst(Rational(1));
Node two = d_nm->mkConst(Rational(2));
Node three = d_nm->mkConst(Rational(3));
@@ -874,6 +904,48 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
d_nm->mkNode(kind::STRING_CONCAT, b, x));
sameNormalForm(ctn, f);
}
+
+ {
+ // (str.contains (str.substr x 0 (str.indexof x "A" zero) "A")) ---> false
+ Node ctn = d_nm->mkNode(
+ kind::STRING_STRCTN,
+ d_nm->mkNode(kind::STRING_SUBSTR,
+ x,
+ zero,
+ d_nm->mkNode(kind::STRING_STRIDOF, x, a, zero)),
+ a);
+ sameNormalForm(ctn, f);
+ }
+
+ {
+ // (str.contains (str.substr (str.substr x 0 (str.indexof x "AAC" zero)) 0
+ // n) "B") ---> false
+ Node ctn = d_nm->mkNode(
+ kind::STRING_STRCTN,
+ d_nm->mkNode(kind::STRING_SUBSTR,
+ d_nm->mkNode(kind::STRING_SUBSTR, aac, zero, m),
+ zero,
+ n),
+ b);
+ sameNormalForm(ctn, f);
+ }
+
+ {
+ // (str.contains (str.substr (str.substr x 0 (str.indexof x "A" zero)) 0
+ // 1) "A") ---> false
+ Node ctn = d_nm->mkNode(
+ kind::STRING_STRCTN,
+ d_nm->mkNode(
+ kind::STRING_SUBSTR,
+ d_nm->mkNode(kind::STRING_SUBSTR,
+ x,
+ zero,
+ d_nm->mkNode(kind::STRING_STRIDOF, x, a, zero)),
+ zero,
+ one),
+ a);
+ sameNormalForm(ctn, f);
+ }
}
void testInferEqsFromContains()
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback