diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-23 17:23:27 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-23 17:23:27 -0800 |
commit | a383a08f87bd87faa1deae338ae2e671d267eb1d (patch) | |
tree | d7fba9b836d30fb423f41bdbfeda7f1b68ccf965 | |
parent | 103e507ae0399532ec121c33a768ca8facb9e17d (diff) | |
parent | b3bbecbd8b25a488cab989b95d37dd717a78ce23 (diff) |
Merge branch 'strongerContainsRew' into cav2019strings
-rw-r--r-- | src/prop/cryptominisat.cpp | 22 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 44 | ||||
-rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 72 |
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() |