diff options
-rw-r--r-- | src/options/strings_options.toml | 63 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 5 | ||||
-rw-r--r-- | src/theory/strings/skolem_cache.cpp | 108 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 21 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 55 | ||||
-rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 2 |
6 files changed, 227 insertions, 27 deletions
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index fd00b8917..dd9599c5c 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -216,3 +216,66 @@ header = "options/strings_options.h" default = "true" read_only = true help = "do flat form inferences" + +[[option]] + name = "stringsCacheSkolems" + category = "expert" + long = "strings-cache-skolems" + type = "bool" + default = "true" + read_only = true + help = "Cache skolems in string reductions" + +[[option]] + name = "stringsNormalizeSkolems" + category = "expert" + long = "strings-normalize-skolems" + type = "bool" + default = "true" + read_only = true + help = "Normalize string skolems before looking them up in the cache" + +[[option]] + name = "stringsRewriterEntailChecks" + category = "expert" + long = "strings-rewriter-entail-checks" + type = "bool" + default = "true" + read_only = true + help = "Enable the entailment checks in the strings rewriter" + +[[option]] + name = "stringsRewriterApprox" + category = "expert" + long = "strings-rewriter-entail-approx" + type = "bool" + default = "true" + read_only = true + help = "Enable the entailment checks in the strings rewriter" + +[[option]] + name = "stringsRewriterEntailContainsChecks" + category = "expert" + long = "strings-rewriter-entail-contains-checks" + type = "bool" + default = "true" + read_only = true + help = "Enable the contains entailment checks in the strings rewriter" + +[[option]] + name = "stringsRewriterMultisetReasoning" + category = "expert" + long = "strings-rewriter-multiset-reasoning" + type = "bool" + default = "true" + read_only = true + help = "Enable multiset reasoning in the strings rewriter" + +[[option]] + name = "stringsRewriterStripConstantEndpoints" + category = "expert" + long = "strings-rewriter-strip-constant-endpoints" + type = "bool" + default = "true" + read_only = true + help = "Enable stripping of constant endpoints" diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index f873b94f2..e15fc85bb 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -273,8 +273,9 @@ void BoundedIntegers::process( Node q, Node n, bool pol, } } -bool BoundedIntegers::needsCheck( Theory::Effort e ) { - return e==Theory::EFFORT_LAST_CALL; +bool BoundedIntegers::needsCheck(Theory::Effort e) +{ + return e == Theory::EFFORT_LAST_CALL; } void BoundedIntegers::check(Theory::Effort e, QEffort quant_e) diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 8791b54b5..669b424a4 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -14,10 +14,13 @@ #include "theory/strings/skolem_cache.h" +#include "options/strings_options.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_rewriter.h" #include "util/rational.h" +using namespace CVC4::kind; + namespace CVC4 { namespace theory { namespace strings { @@ -42,6 +45,13 @@ Node SkolemCache::mkSkolemCached(Node a, SkolemId id, const char* c) Node SkolemCache::mkTypedSkolemCached( TypeNode tn, Node a, Node b, SkolemId id, const char* c) { + if (!options::stringsCacheSkolems()) + { + Node n = NodeManager::currentNM()->mkSkolem(c, tn, "string skolem"); + d_allSkolems.insert(n); + return n; + } + a = a.isNull() ? a : Rewriter::rewrite(a); b = b.isNull() ? b : Rewriter::rewrite(b); @@ -87,26 +97,108 @@ bool SkolemCache::isSkolem(Node n) const std::tuple<SkolemCache::SkolemId, Node, Node> SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) { + if (!options::stringsNormalizeSkolems()) + { + return std::make_tuple(id, a, b); + } + Trace("skolem-cache") << "normalizeStringSkolem start: (" << id << ", " << a << ", " << b << ")" << std::endl; - // SK_PURIFY(str.substr x 0 (str.indexof x y 0)) ---> SK_FIRST_CTN_PRE(x, y) + NodeManager* nm = NodeManager::currentNM(); + + if (id == SK_FIRST_CTN_POST) + { + // SK_FIRST_CTN_POST(x, y) ---> + // SK_SUFFIX_REM(x, (+ (str.len SK_FIRST_CTN_PRE(x, y)) (str.len y))) + id = SK_SUFFIX_REM; + Node pre = mkSkolemCached(a, b, SK_FIRST_CTN_PRE, "pre"); + b = Rewriter::rewrite(nm->mkNode( + PLUS, nm->mkNode(STRING_LENGTH, pre), nm->mkNode(STRING_LENGTH, b))); + } + + if (id == SK_ID_C_SPT) + { + // SK_ID_C_SPT(x, y) ---> SK_SUFFIX_REM(x, (str.len y)) + id = SK_SUFFIX_REM; + b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, b)); + } + else if (id == SK_ID_VC_SPT) + { + // SK_ID_VC_SPT(x, y) ---> SK_SUFFIX_REM(x, 1) + id = SK_SUFFIX_REM; + b = nm->mkConst(Rational(1)); + } + else if (id == SK_ID_VC_SPT_REV) + { + // SK_ID_VC_SPT_REV(x, y) ---> SK_PREFIX(x, (- (str.len x) 1)) + id = SK_PREFIX; + b = Rewriter::rewrite(nm->mkNode( + MINUS, nm->mkNode(STRING_LENGTH, a), nm->mkConst(Rational(1)))); + } + else if (id == SK_ID_DC_SPT) + { + // SK_ID_DC_SPT(x, y) ---> SK_PREFIX(x, 1) + id = SK_PREFIX; + b = nm->mkConst(Rational(1)); + } + else if (id == SK_ID_DC_SPT_REM) + { + // SK_ID_DC_SPT_REM(x, y) ---> SK_SUFFIX_REM(x, 1) + id = SK_SUFFIX_REM; + b = nm->mkConst(Rational(1)); + } + else if (id == SK_ID_DEQ_X) + { + // SK_ID_DEQ_X(x, y) ---> SK_PREFIX(y, (str.len x)) + id = SK_PREFIX; + Node aOld = a; + a = b; + b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, aOld)); + } + else if (id == SK_ID_DEQ_Y) + { + // SK_ID_DEQ_Y(x, y) ---> SK_PREFIX(x, (str.len y)) + id = SK_PREFIX; + b = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, b)); + } + + if (id == SK_SUFFIX_REM) { + //std::cout << "suffix" << a << " " << b << std::endl; + } + if (id == SK_PURIFY && a.getKind() == kind::STRING_SUBSTR) { Node s = a[0]; Node n = a[1]; Node m = a[2]; - if (m.getKind() == kind::STRING_STRIDOF && m[0] == s) + + if (n == d_zero) + { + // SK_PURIFY((str.substr x 0 m)) ---> SK_PREFIX(x, m) + id = SK_PREFIX; + a = s; + b = m; + } + else if (TheoryStringsRewriter::checkEntailArith( + nm->mkNode(PLUS, n, m), nm->mkNode(STRING_LENGTH, s))) { - if (n == d_zero && m[2] == d_zero) - { - id = SK_FIRST_CTN_PRE; - a = m[0]; - b = m[1]; - } + // SK_PURIFY((str.substr x n m)) ---> SK_SUFFIX_REM(x, n) + // if n + m >= (str.len x) + id = SK_SUFFIX_REM; + a = s; + b = n; } } + if (id == SK_PREFIX && b.getKind() == kind::STRING_STRIDOF && a == b[0] + && b[2] == d_zero) + { + // SK_PREFIX(x, (str.indexof x y 0)) ---> SK_FIRST_CTN_PRE(x, y) + id = SK_FIRST_CTN_PRE; + b = b[1]; + } + if (id == SK_FIRST_CTN_PRE) { // SK_FIRST_CTN_PRE((str.substr x 0 n), y) ---> SK_FIRST_CTN_PRE(x, y) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 6333bfee1..14216f8aa 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3274,7 +3274,6 @@ void TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal Node firstChar = stra.size() == 1 ? const_str : NodeManager::currentNM()->mkConst( isRev ? stra.suffix( 1 ) : stra.prefix( 1 ) ); Node sk = d_sk_cache.mkSkolemCached( other_str, - firstChar, isRev ? SkolemCache::SK_ID_VC_SPT_REV : SkolemCache::SK_ID_VC_SPT, "c_spt"); @@ -3662,11 +3661,10 @@ void TheoryStrings::processDeq( Node ni, Node nj ) { } }else{ Node sk = d_sk_cache.mkSkolemCached( - nconst_k, firstChar, SkolemCache::SK_ID_DC_SPT, "dc_spt"); + nconst_k, SkolemCache::SK_ID_DC_SPT, "dc_spt"); registerLength(sk, LENGTH_ONE); Node skr = d_sk_cache.mkSkolemCached(nconst_k, - firstChar, SkolemCache::SK_ID_DC_SPT_REM, "dc_spt_rem"); Node eq1 = nconst_k.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk, skr ) ); @@ -3985,6 +3983,23 @@ void TheoryStrings::registerTerm( Node n, int effort ) { Trace("strings-assert") << "(assert " << lem << ")" << std::endl; d_out->lemma(lem); } + else if (n.getKind() == STRING_STRIDOF) + { + Node lower = n[2]; + if (!TheoryStringsRewriter::checkEntailArith(lower)) { + lower = d_zero; + } + Node neg = Rewriter::rewrite(nm->mkNode(EQUAL, n, d_neg_one)); + Node geq = Rewriter::rewrite(nm->mkNode(GEQ, n, lower)); + Node lem = nm->mkNode(OR, neg, geq); + Trace("strings-lemma") << "Strings::Lemma STRIDOF : " << lem << std::endl; + Trace("strings-assert") << "(assert " << lem << ")" << std::endl; + //d_out->lemma(lem); + //d_out->requirePhase(neg, true); + + lem = Rewriter::rewrite(nm->mkNode(GT, nm->mkNode(STRING_LENGTH, n[0]), n)); + d_out->lemma(lem); + } } bool TheoryStrings::sendInternalInference(std::vector<Node>& exp, diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 2e50ade0c..ec9a46e3a 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -624,6 +624,13 @@ Node TheoryStringsRewriter::rewriteArithEqualityExt(Node node) } } + if (checkEntailArith(node[0], node[1], true) + || checkEntailArith(node[1], node[0], true)) + { + Node ret = nm->mkConst(false); + return returnRewrite(node, ret, "int-eq-false"); + } + return node; } @@ -1967,6 +1974,7 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { { Node ret = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, mkConcat(kind::STRING_CONCAT, nc1), node[1]); + Trace("strip-constant-endpoints") << node << " ---> " << ret << std::endl; return returnRewrite(node, ret, "ctn-strip-endpt"); } @@ -2093,18 +2101,6 @@ 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 ret = nm->mkNode(kind::EQUAL, node[0], node[1]); - return returnRewrite(node, ret, "ctn-substr"); - } - } else if (node[0].getKind() == kind::STRING_STRREPL) { if (node[1].isConst() && node[0][1].isConst() && node[0][2].isConst()) @@ -2395,6 +2391,7 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) { { Node ret = mkConcat(kind::STRING_CONCAT, children0); ret = nm->mkNode(STRING_STRIDOF, ret, node[1], node[2]); + Trace("strip-constant-endpoints") << node << " ---> " << ret << std::endl; // For example: // str.indexof( str.++( x, "A" ), "B", 0 ) ---> str.indexof( x, "B", 0 ) return returnRewrite(node, ret, "rpl-pull-endpt"); @@ -2617,6 +2614,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { node[2])); cc.insert(cc.end(), ce.begin(), ce.end()); Node ret = mkConcat(kind::STRING_CONCAT, cc); + Trace("strip-constant-endpoints") << node << " ---> " << ret << std::endl; return returnRewrite(node, ret, "rpl-pull-endpt"); } } @@ -3361,6 +3359,11 @@ int TheoryStringsRewriter::componentContains(std::vector<Node>& n1, bool computeRemainder, int remainderDir) { + if (!options::stringsRewriterEntailContainsChecks()) + { + return -1; + } + Assert(nb.empty()); Assert(ne.empty()); // if n2 is a singleton, we can do optimized version here @@ -3627,6 +3630,11 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1, std::vector<Node>& ne, int dir) { + if (!options::stringsRewriterStripConstantEndpoints()) + { + return false; + } + Assert(nb.empty()); Assert(ne.empty()); @@ -3870,6 +3878,11 @@ Node TheoryStringsRewriter::checkEntailContains(Node a, Node b, bool fullRewriter) { + if (!options::stringsRewriterEntailContainsChecks()) + { + return Node::null(); + } + NodeManager* nm = NodeManager::currentNM(); Node ctn = nm->mkNode(kind::STRING_STRCTN, a, b); @@ -3952,6 +3965,10 @@ bool TheoryStringsRewriter::checkEntailArith(Node a, bool strict) return a.getConst<Rational>().sgn() >= (strict ? 1 : 0); } + if (!options::stringsRewriterEntailChecks()) { + return false; + } + Node ar = strict ? NodeManager::currentNM()->mkNode( @@ -3965,7 +3982,7 @@ bool TheoryStringsRewriter::checkEntailArith(Node a, bool strict) } bool ret = checkEntailArithInternal(ar); - if (!ret) + if (!ret && options::stringsRewriterApprox()) { // try with approximations ret = checkEntailArithApprox(ar); @@ -4441,6 +4458,11 @@ void TheoryStringsRewriter::getArithApproximations(Node a, bool TheoryStringsRewriter::checkEntailMultisetSubset(Node a, Node b) { + if (!options::stringsRewriterMultisetReasoning()) + { + return false; + } + NodeManager* nm = NodeManager::currentNM(); std::vector<Node> avec; @@ -4527,6 +4549,11 @@ bool TheoryStringsRewriter::checkEntailMultisetSubset(Node a, Node b) Node TheoryStringsRewriter::checkEntailHomogeneousString(Node a) { + if (!options::stringsRewriterMultisetReasoning()) + { + return Node::null(); + } + NodeManager* nm = NodeManager::currentNM(); std::vector<Node> avec; @@ -4757,7 +4784,7 @@ Node TheoryStringsRewriter::getConstantArithBound(Node a, bool isLower) ret = NodeManager::currentNM()->mkConst(Rational(0)); } } - else if (a.getKind() == kind::PLUS || a.getKind() == kind::MULT) + else if (options::stringsRewriterEntailChecks() && (a.getKind() == kind::PLUS || a.getKind() == kind::MULT)) { std::vector<Node> children; bool success = true; diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index 00eb0b495..86f5cd5d6 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -700,6 +700,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 ab = d_nm->mkConst(::CVC4::String("AB")); Node b = d_nm->mkConst(::CVC4::String("B")); Node c = d_nm->mkConst(::CVC4::String("C")); @@ -713,6 +714,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite 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)); |