diff options
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/arith_entail.cpp | 6 | ||||
-rw-r--r-- | src/theory/strings/extf_solver.cpp | 10 | ||||
-rw-r--r-- | src/theory/strings/extf_solver.h | 8 | ||||
-rw-r--r-- | src/theory/strings/regexp_entail.cpp | 4 | ||||
-rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 96 | ||||
-rw-r--r-- | src/theory/strings/sequences_rewriter.h | 65 | ||||
-rw-r--r-- | src/theory/strings/sequences_stats.cpp | 3 | ||||
-rw-r--r-- | src/theory/strings/sequences_stats.h | 3 | ||||
-rw-r--r-- | src/theory/strings/strings_entail.cpp | 10 | ||||
-rw-r--r-- | src/theory/strings/strings_entail.h | 27 | ||||
-rw-r--r-- | src/theory/strings/strings_rewriter.cpp | 61 | ||||
-rw-r--r-- | src/theory/strings/strings_rewriter.h | 20 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 9 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.h | 6 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 2 |
15 files changed, 206 insertions, 124 deletions
diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp index 5933f2586..71680264d 100644 --- a/src/theory/strings/arith_entail.cpp +++ b/src/theory/strings/arith_entail.cpp @@ -66,11 +66,9 @@ bool ArithEntail::check(Node a, bool strict) return a.getConst<Rational>().sgn() >= (strict ? 1 : 0); } - Node ar = - strict - ? NodeManager::currentNM()->mkNode( + Node ar = strict ? NodeManager::currentNM()->mkNode( kind::MINUS, a, NodeManager::currentNM()->mkConst(Rational(1))) - : a; + : a; ar = Rewriter::rewrite(ar); if (ar.getAttribute(StrCheckEntailArithComputedAttr())) diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index a1c04848a..0c46881e7 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -32,18 +32,20 @@ ExtfSolver::ExtfSolver(context::Context* c, SolverState& s, InferenceManager& im, SkolemCache& skc, + StringsRewriter& rewriter, BaseSolver& bs, CoreSolver& cs, ExtTheory* et, - SequencesStatistics& stats) + SequencesStatistics& statistics) : d_state(s), d_im(im), d_skCache(skc), + d_rewriter(rewriter), d_bsolver(bs), d_csolver(cs), d_extt(et), - d_statistics(stats), - d_preproc(&skc, u, stats), + d_statistics(statistics), + d_preproc(&skc, u, statistics), d_hasExtf(c, false), d_extfInferCache(c) { @@ -620,7 +622,7 @@ void ExtfSolver::checkExtfInference(Node n, if (inferEqr.getKind() == EQUAL) { // try to use the extended rewriter for equalities - inferEqrr = SequencesRewriter::rewriteEqualityExt(inferEqr); + inferEqrr = d_rewriter.rewriteEqualityExt(inferEqr); } if (inferEqrr != inferEqr) { diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index 9ca72fed2..e7e2512bd 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -17,8 +17,8 @@ #ifndef CVC4__THEORY__STRINGS__EXTF_SOLVER_H #define CVC4__THEORY__STRINGS__EXTF_SOLVER_H -#include <vector> #include <map> +#include <vector> #include "context/cdo.h" #include "expr/node.h" @@ -29,6 +29,7 @@ #include "theory/strings/sequences_stats.h" #include "theory/strings/skolem_cache.h" #include "theory/strings/solver_state.h" +#include "theory/strings/strings_rewriter.h" #include "theory/strings/theory_strings_preprocess.h" namespace CVC4 { @@ -87,10 +88,11 @@ class ExtfSolver SolverState& s, InferenceManager& im, SkolemCache& skc, + StringsRewriter& rewriter, BaseSolver& bs, CoreSolver& cs, ExtTheory* et, - SequencesStatistics& stats); + SequencesStatistics& statistics); ~ExtfSolver(); /** check extended functions evaluation @@ -180,6 +182,8 @@ class ExtfSolver InferenceManager& d_im; /** cache of all skolems */ SkolemCache& d_skCache; + /** The theory rewriter for this theory. */ + StringsRewriter& d_rewriter; /** reference to the base solver, used for certain queries */ BaseSolver& d_bsolver; /** reference to the core solver, used for certain queries */ diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index d03893483..a43ec4430 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -438,7 +438,9 @@ bool RegExpEntail::testConstStringInRegExp(CVC4::String& s, return true; } } - case REGEXP_EMPTY: { return false; + case REGEXP_EMPTY: + { + return false; } case REGEXP_SIGMA: { diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 9ccda55c2..152f71019 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -21,7 +21,6 @@ #include "theory/rewriter.h" #include "theory/strings/arith_entail.h" #include "theory/strings/regexp_entail.h" -#include "theory/strings/strings_entail.h" #include "theory/strings/strings_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" @@ -33,6 +32,11 @@ namespace CVC4 { namespace theory { namespace strings { +SequencesRewriter::SequencesRewriter(HistogramStat<Rewrite>* statistics) + : d_statistics(statistics), d_stringsEntail(*this) +{ +} + Node SequencesRewriter::rewriteEquality(Node node) { Assert(node.getKind() == kind::EQUAL); @@ -53,7 +57,7 @@ Node SequencesRewriter::rewriteEquality(Node node) // 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 = StringsEntail::checkContains(node[r], node[1 - r], false); + Node ctn = d_stringsEntail.checkContains(node[r], node[1 - r], false); if (!ctn.isNull()) { if (!ctn.getConst<bool>()) @@ -810,7 +814,7 @@ Node SequencesRewriter::rewriteConcatRegExp(TNode node) // e.g. this ensures we rewrite (a)* ++ (_)* ---> (_)* while (!cvec.empty() && RegExpEntail::isConstRegExp(cvec.back()) && RegExpEntail::testConstStringInRegExp( - emptyStr, 0, cvec.back())) + emptyStr, 0, cvec.back())) { cvec.pop_back(); } @@ -1337,8 +1341,8 @@ Node SequencesRewriter::rewriteMembership(TNode node) RewriteResponse SequencesRewriter::postRewrite(TNode node) { - Trace("strings-postrewrite") - << "Strings::postRewrite start " << node << std::endl; + Trace("sequences-postrewrite") + << "Strings::SequencesRewriter::postRewrite start " << node << std::endl; Node retNode = node; Kind nk = node.getKind(); if (nk == kind::STRING_CONCAT) @@ -1365,14 +1369,6 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node) { retNode = rewriteContains(node); } - else if (nk == kind::STRING_LT) - { - retNode = StringsRewriter::rewriteStringLt(node); - } - else if (nk == kind::STRING_LEQ) - { - retNode = StringsRewriter::rewriteStringLeq(node); - } else if (nk == kind::STRING_STRIDOF) { retNode = rewriteIndexof(node); @@ -1385,10 +1381,6 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node) { retNode = rewriteReplaceAll(node); } - else if (nk == STRING_TOLOWER || nk == STRING_TOUPPER) - { - retNode = StringsRewriter::rewriteStrConvert(node); - } else if (nk == STRING_REV) { retNode = rewriteStrReverse(node); @@ -1397,30 +1389,10 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node) { retNode = rewritePrefixSuffix(node); } - else if (nk == STRING_IS_DIGIT) - { - retNode = StringsRewriter::rewriteStringIsDigit(node); - } - else if (nk == kind::STRING_ITOS) - { - retNode = StringsRewriter::rewriteIntToStr(node); - } - else if (nk == kind::STRING_STOI) - { - retNode = StringsRewriter::rewriteStrToInt(node); - } else if (nk == kind::STRING_IN_REGEXP) { retNode = rewriteMembership(node); } - else if (nk == STRING_TO_CODE) - { - retNode = StringsRewriter::rewriteStringToCode(node); - } - else if (nk == STRING_FROM_CODE) - { - retNode = StringsRewriter::rewriteStringFromCode(node); - } else if (nk == REGEXP_CONCAT) { retNode = rewriteConcatRegExp(node); @@ -1458,12 +1430,13 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node) retNode = rewriteRepeatRegExp(node); } - Trace("strings-postrewrite") - << "Strings::postRewrite returning " << retNode << std::endl; + Trace("sequences-postrewrite") + << "Strings::SequencesRewriter::postRewrite returning " << retNode + << std::endl; if (node != retNode) { - Trace("strings-rewrite-debug") - << "Strings: post-rewrite " << node << " to " << retNode << std::endl; + Trace("strings-rewrite-debug") << "Strings::SequencesRewriter::postRewrite " + << node << " to " << retNode << std::endl; return RewriteResponse(REWRITE_AGAIN_FULL, retNode); } return RewriteResponse(REWRITE_DONE, retNode); @@ -1866,7 +1839,7 @@ Node SequencesRewriter::rewriteContains(Node node) } else if (node[0].getKind() == STRING_STRREPL) { - Node rplDomain = StringsEntail::checkContains(node[0][1], node[1]); + Node rplDomain = d_stringsEntail.checkContains(node[0][1], node[1]); if (!rplDomain.isNull() && !rplDomain.getConst<bool>()) { Node d1 = nm->mkNode(STRING_STRCTN, node[0][0], node[1]); @@ -1892,7 +1865,7 @@ Node SequencesRewriter::rewriteContains(Node node) // component-wise containment std::vector<Node> nc1rb; std::vector<Node> nc1re; - if (StringsEntail::componentContains(nc1, nc2, nc1rb, nc1re) != -1) + if (d_stringsEntail.componentContains(nc1, nc2, nc1rb, nc1re) != -1) { Node ret = NodeManager::currentNM()->mkConst(true); return returnRewrite(node, ret, Rewrite::CTN_COMPONENT); @@ -1920,10 +1893,10 @@ Node SequencesRewriter::rewriteContains(Node node) // replacement does not change y. (str.contains x w) checks that if the // replacement changes anything in y, the w makes it impossible for it to // occur in x. - Node ctnConst = StringsEntail::checkContains(node[0], n[0]); + Node ctnConst = d_stringsEntail.checkContains(node[0], n[0]); if (!ctnConst.isNull() && !ctnConst.getConst<bool>()) { - Node ctnConst2 = StringsEntail::checkContains(node[0], n[2]); + Node ctnConst2 = d_stringsEntail.checkContains(node[0], n[2]); if (!ctnConst2.isNull() && !ctnConst2.getConst<bool>()) { Node res = nm->mkConst(false); @@ -2091,7 +2064,7 @@ Node SequencesRewriter::rewriteContains(Node node) // if (str.contains z w) ---> false and (str.len w) = 1 if (StringsEntail::checkLengthOne(node[1])) { - Node ctn = StringsEntail::checkContains(node[1], node[0][2]); + Node ctn = d_stringsEntail.checkContains(node[1], node[0][2]); if (!ctn.isNull() && !ctn.getConst<bool>()) { Node empty = nm->mkConst(String("")); @@ -2235,7 +2208,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) fstr = Rewriter::rewrite(fstr); } - Node cmp_conr = StringsEntail::checkContains(fstr, node[1]); + Node cmp_conr = d_stringsEntail.checkContains(fstr, node[1]); Trace("strings-rewrite-debug") << "For " << node << ", check contains(" << fstr << ", " << node[1] << ")" << std::endl; Trace("strings-rewrite-debug") << "...got " << cmp_conr << std::endl; @@ -2250,7 +2223,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) // past the first position in node[0] that contains node[1], we can drop std::vector<Node> nb; std::vector<Node> ne; - int cc = StringsEntail::componentContains( + int cc = d_stringsEntail.componentContains( children0, children1, nb, ne, true, 1); if (cc != -1 && !ne.empty()) { @@ -2445,14 +2418,14 @@ Node SequencesRewriter::rewriteReplace(Node node) // check if contains definitely does (or does not) hold Node cmp_con = nm->mkNode(kind::STRING_STRCTN, node[0], node[1]); Node cmp_conr = Rewriter::rewrite(cmp_con); - if (!StringsEntail::checkContains(node[0], node[1]).isNull()) + if (!d_stringsEntail.checkContains(node[0], node[1]).isNull()) { if (cmp_conr.getConst<bool>()) { // component-wise containment std::vector<Node> cb; std::vector<Node> ce; - int cc = StringsEntail::componentContains( + int cc = d_stringsEntail.componentContains( children0, children1, cb, ce, true, 1); if (cc != -1) { @@ -2673,7 +2646,7 @@ Node SequencesRewriter::rewriteReplace(Node node) return returnRewrite(node, node[0], Rewrite::REPL_REPL2_INV_ID); } bool dualReplIteSuccess = false; - Node cmp_con2 = StringsEntail::checkContains(node[1][0], node[1][2]); + Node cmp_con2 = d_stringsEntail.checkContains(node[1][0], node[1][2]); if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>()) { // str.contains( x, z ) ---> false @@ -2688,10 +2661,10 @@ Node SequencesRewriter::rewriteReplace(Node node) // implies // str.replace( x, str.replace( x, y, z ), w ) ---> // ite( str.contains( x, y ), x, w ) - cmp_con2 = StringsEntail::checkContains(node[1][1], node[1][2]); + cmp_con2 = d_stringsEntail.checkContains(node[1][1], node[1][2]); if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>()) { - cmp_con2 = StringsEntail::checkContains(node[1][2], node[1][1]); + cmp_con2 = d_stringsEntail.checkContains(node[1][2], node[1][1]); if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>()) { dualReplIteSuccess = true; @@ -2721,7 +2694,7 @@ Node SequencesRewriter::rewriteReplace(Node node) // str.contains(y, z) ----> false and ( y == w or x == w ) implies // implies // str.replace(x, str.replace(y, x, z), w) ---> str.replace(x, y, w) - Node cmp_con2 = StringsEntail::checkContains(node[1][0], node[1][2]); + Node cmp_con2 = d_stringsEntail.checkContains(node[1][0], node[1][2]); invSuccess = !cmp_con2.isNull() && !cmp_con2.getConst<bool>(); } } @@ -2730,10 +2703,10 @@ Node SequencesRewriter::rewriteReplace(Node node) // str.contains(x, z) ----> false and str.contains(x, w) ----> false // implies // str.replace(x, str.replace(y, z, w), u) ---> str.replace(x, y, u) - Node cmp_con2 = StringsEntail::checkContains(node[0], node[1][1]); + Node cmp_con2 = d_stringsEntail.checkContains(node[0], node[1][1]); if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>()) { - cmp_con2 = StringsEntail::checkContains(node[0], node[1][2]); + cmp_con2 = d_stringsEntail.checkContains(node[0], node[1][2]); invSuccess = !cmp_con2.isNull() && !cmp_con2.getConst<bool>(); } } @@ -2749,7 +2722,7 @@ Node SequencesRewriter::rewriteReplace(Node node) { // str.contains( z, w ) ----> false implies // str.replace( x, w, str.replace( z, x, y ) ) ---> str.replace( x, w, z ) - Node cmp_con2 = StringsEntail::checkContains(node[1], node[2][0]); + Node cmp_con2 = d_stringsEntail.checkContains(node[1], node[2][0]); if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>()) { Node res = @@ -2769,7 +2742,7 @@ Node SequencesRewriter::rewriteReplace(Node node) { // str.contains( x, z ) ----> false implies // str.replace( x, y, str.replace( y, z, w ) ) ---> x - cmp_con = StringsEntail::checkContains(node[0], node[2][1]); + cmp_con = d_stringsEntail.checkContains(node[0], node[2][1]); success = !cmp_con.isNull() && !cmp_con.getConst<bool>(); } if (success) @@ -2795,7 +2768,7 @@ Node SequencesRewriter::rewriteReplace(Node node) checkLhs.end(), children0.begin(), children0.begin() + checkIndex); Node lhs = utils::mkConcat(checkLhs, stype); Node rhs = children0[checkIndex]; - Node ctn = StringsEntail::checkContains(lhs, rhs); + Node ctn = d_stringsEntail.checkContains(lhs, rhs); if (!ctn.isNull() && ctn.getConst<bool>()) { lastLhs = lhs; @@ -3102,6 +3075,11 @@ Node SequencesRewriter::returnRewrite(Node node, Node ret, Rewrite r) NodeManager* nm = NodeManager::currentNM(); + if (d_statistics != nullptr) + { + (*d_statistics) << r; + } + // 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 diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h index 7391a7bd0..56b74f536 100644 --- a/src/theory/strings/sequences_rewriter.h +++ b/src/theory/strings/sequences_rewriter.h @@ -22,6 +22,8 @@ #include "expr/node.h" #include "theory/strings/rewrites.h" +#include "theory/strings/sequences_stats.h" +#include "theory/strings/strings_entail.h" #include "theory/theory_rewriter.h" namespace CVC4 { @@ -30,82 +32,85 @@ namespace strings { class SequencesRewriter : public TheoryRewriter { + public: + SequencesRewriter(HistogramStat<Rewrite>* statistics); + protected: /** rewrite regular expression concatenation * * This is the entry point for post-rewriting applications of re.++. * Returns the rewritten form of node. */ - static Node rewriteConcatRegExp(TNode node); + Node rewriteConcatRegExp(TNode node); /** rewrite regular expression star * * This is the entry point for post-rewriting applications of re.*. * Returns the rewritten form of node. */ - static Node rewriteStarRegExp(TNode node); + Node rewriteStarRegExp(TNode node); /** rewrite regular expression intersection/union * * This is the entry point for post-rewriting applications of re.inter and * re.union. Returns the rewritten form of node. */ - static Node rewriteAndOrRegExp(TNode node); + Node rewriteAndOrRegExp(TNode node); /** rewrite regular expression loop * * This is the entry point for post-rewriting applications of re.loop. * Returns the rewritten form of node. */ - static Node rewriteLoopRegExp(TNode node); + Node rewriteLoopRegExp(TNode node); /** rewrite regular expression repeat * * This is the entry point for post-rewriting applications of re.repeat. * Returns the rewritten form of node. */ - static Node rewriteRepeatRegExp(TNode node); + Node rewriteRepeatRegExp(TNode node); /** rewrite regular expression option * * This is the entry point for post-rewriting applications of re.opt. * Returns the rewritten form of node. */ - static Node rewriteOptionRegExp(TNode node); + Node rewriteOptionRegExp(TNode node); /** rewrite regular expression plus * * This is the entry point for post-rewriting applications of re.+. * Returns the rewritten form of node. */ - static Node rewritePlusRegExp(TNode node); + Node rewritePlusRegExp(TNode node); /** rewrite regular expression difference * * This is the entry point for post-rewriting applications of re.diff. * Returns the rewritten form of node. */ - static Node rewriteDifferenceRegExp(TNode node); + Node rewriteDifferenceRegExp(TNode node); /** rewrite regular expression range * * This is the entry point for post-rewriting applications of re.range. * Returns the rewritten form of node. */ - static Node rewriteRangeRegExp(TNode node); + Node rewriteRangeRegExp(TNode node); /** rewrite regular expression membership * * This is the entry point for post-rewriting applications of str.in.re * Returns the rewritten form of node. */ - static Node rewriteMembership(TNode node); + Node rewriteMembership(TNode node); /** rewrite string equality extended * * This method returns a formula that is equivalent to the equality between * two strings s = t, given by node. It is called by rewriteEqualityExt. */ - static Node rewriteStrEqualityExt(Node node); + Node rewriteStrEqualityExt(Node node); /** rewrite arithmetic equality extended * * This method returns a formula that is equivalent to the equality between * two arithmetic string terms s = t, given by node. t is called by * rewriteEqualityExt. */ - static Node rewriteArithEqualityExt(Node node); + Node rewriteArithEqualityExt(Node node); /** * Called when node rewrites to ret. * @@ -117,7 +122,7 @@ class SequencesRewriter : public TheoryRewriter * additional rewrites on ret, after which we return the result of this call. * Otherwise, this method simply returns ret. */ - static Node returnRewrite(Node node, Node ret, Rewrite r); + Node returnRewrite(Node node, Node ret, Rewrite r); public: RewriteResponse postRewrite(TNode node) override; @@ -129,7 +134,7 @@ class SequencesRewriter : public TheoryRewriter * two strings s = t, given by node. The result of rewrite is one of * { s = t, t = s, true, false }. */ - static Node rewriteEquality(Node node); + Node rewriteEquality(Node node); /** rewrite equality extended * * This method returns a formula that is equivalent to the equality between @@ -140,31 +145,31 @@ class SequencesRewriter : public TheoryRewriter * Specifically, this function performs rewrites whose conclusion is not * necessarily one of { s = t, t = s, true, false }. */ - static Node rewriteEqualityExt(Node node); + Node rewriteEqualityExt(Node node); /** rewrite string length * This is the entry point for post-rewriting terms node of the form * str.len( t ) * Returns the rewritten form of node. */ - static Node rewriteLength(Node node); + Node rewriteLength(Node node); /** rewrite concat * This is the entry point for post-rewriting terms node of the form * str.++( t1, .., tn ) * Returns the rewritten form of node. */ - static Node rewriteConcat(Node node); + Node rewriteConcat(Node node); /** rewrite character at * This is the entry point for post-rewriting terms node of the form * str.charat( s, i1 ) * Returns the rewritten form of node. */ - static Node rewriteCharAt(Node node); + Node rewriteCharAt(Node node); /** rewrite substr * This is the entry point for post-rewriting terms node of the form * str.substr( s, i1, i2 ) * Returns the rewritten form of node. */ - static Node rewriteSubstr(Node node); + Node rewriteSubstr(Node node); /** rewrite contains * This is the entry point for post-rewriting terms node of the form * str.contains( t, s ) @@ -174,51 +179,51 @@ class SequencesRewriter : public TheoryRewriter * 7 of Reynolds et al "Scaling Up DPLL(T) String Solvers Using * Context-Dependent Rewriting", CAV 2017. */ - static Node rewriteContains(Node node); + Node rewriteContains(Node node); /** rewrite indexof * This is the entry point for post-rewriting terms n of the form * str.indexof( s, t, n ) * Returns the rewritten form of node. */ - static Node rewriteIndexof(Node node); + Node rewriteIndexof(Node node); /** rewrite replace * This is the entry point for post-rewriting terms n of the form * str.replace( s, t, r ) * Returns the rewritten form of node. */ - static Node rewriteReplace(Node node); + Node rewriteReplace(Node node); /** rewrite replace all * This is the entry point for post-rewriting terms n of the form * str.replaceall( s, t, r ) * Returns the rewritten form of node. */ - static Node rewriteReplaceAll(Node node); + Node rewriteReplaceAll(Node node); /** rewrite replace internal * * This method implements rewrite rules that apply to both str.replace and * str.replaceall. If it returns a non-null ret, then node rewrites to ret. */ - static Node rewriteReplaceInternal(Node node); + Node rewriteReplaceInternal(Node node); /** rewrite string reverse * * This is the entry point for post-rewriting terms n of the form * str.rev( s ) * Returns the rewritten form of node. */ - static Node rewriteStrReverse(Node node); + Node rewriteStrReverse(Node node); /** rewrite prefix/suffix * This is the entry point for post-rewriting terms n of the form * str.prefixof( s, t ) / str.suffixof( s, t ) * Returns the rewritten form of node. */ - static Node rewritePrefixSuffix(Node node); + Node rewritePrefixSuffix(Node node); /** rewrite str.to_code * This is the entry point for post-rewriting terms n of the form * str.to_code( t ) * Returns the rewritten form of node. */ - static Node rewriteStringToCode(Node node); + Node rewriteStringToCode(Node node); /** length preserving rewrite * @@ -235,6 +240,12 @@ class SequencesRewriter : public TheoryRewriter * string exists. */ static Node canonicalStrForSymbolicLength(Node n, TypeNode stype); + + /** Reference to the rewriter statistics. */ + HistogramStat<Rewrite>* d_statistics; + + /** Instance of the entailment checker for strings. */ + StringsEntail d_stringsEntail; }; /* class SequencesRewriter */ } // namespace strings diff --git a/src/theory/strings/sequences_stats.cpp b/src/theory/strings/sequences_stats.cpp index 5cd844290..afcfb1a60 100644 --- a/src/theory/strings/sequences_stats.cpp +++ b/src/theory/strings/sequences_stats.cpp @@ -27,6 +27,7 @@ SequencesStatistics::SequencesStatistics() d_reductions("theory::strings::reductions"), d_regexpUnfoldingsPos("theory::strings::regexpUnfoldingsPos"), d_regexpUnfoldingsNeg("theory::strings::regexpUnfoldingsNeg"), + d_rewrites("theory::strings::rewrites"), d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0), d_conflictsEagerPrefix("theory::strings::conflictsEagerPrefix", 0), d_conflictsInfer("theory::strings::conflictsInfer", 0), @@ -42,6 +43,7 @@ SequencesStatistics::SequencesStatistics() smtStatisticsRegistry()->registerStat(&d_reductions); smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsPos); smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsNeg); + smtStatisticsRegistry()->registerStat(&d_rewrites); smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine); smtStatisticsRegistry()->registerStat(&d_conflictsEagerPrefix); smtStatisticsRegistry()->registerStat(&d_conflictsInfer); @@ -59,6 +61,7 @@ SequencesStatistics::~SequencesStatistics() smtStatisticsRegistry()->unregisterStat(&d_reductions); smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsPos); smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsNeg); + smtStatisticsRegistry()->unregisterStat(&d_rewrites); smtStatisticsRegistry()->unregisterStat(&d_conflictsEqEngine); smtStatisticsRegistry()->unregisterStat(&d_conflictsEagerPrefix); smtStatisticsRegistry()->unregisterStat(&d_conflictsInfer); diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h index 65f50dbbc..63d9f55eb 100644 --- a/src/theory/strings/sequences_stats.h +++ b/src/theory/strings/sequences_stats.h @@ -19,6 +19,7 @@ #include "expr/kind.h" #include "theory/strings/infer_info.h" +#include "theory/strings/rewrites.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -77,6 +78,8 @@ class SequencesStatistics HistogramStat<Kind> d_regexpUnfoldingsPos; HistogramStat<Kind> d_regexpUnfoldingsNeg; //--------------- end of inferences + /** Counts the number of applications of each type of rewrite rule */ + HistogramStat<Rewrite> d_rewrites; //--------------- conflicts, partition of calls to OutputChannel::conflict /** Number of equality engine conflicts */ IntStat d_conflictsEqEngine; diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp index a1abfabe5..99219af82 100644 --- a/src/theory/strings/strings_entail.cpp +++ b/src/theory/strings/strings_entail.cpp @@ -27,6 +27,10 @@ namespace CVC4 { namespace theory { namespace strings { +StringsEntail::StringsEntail(SequencesRewriter& rewriter) : d_rewriter(rewriter) +{ +} + bool StringsEntail::canConstantContainConcat(Node c, Node n, int& firstc, @@ -468,10 +472,10 @@ bool StringsEntail::componentContainsBase( { // (str.contains (str.replace x y z) w) ---> true // if (str.contains x w) --> true and (str.contains z w) ---> true - Node xCtnW = StringsEntail::checkContains(n1[0], n2); + Node xCtnW = checkContains(n1[0], n2); if (!xCtnW.isNull() && xCtnW.getConst<bool>()) { - Node zCtnW = StringsEntail::checkContains(n1[2], n2); + Node zCtnW = checkContains(n1[2], n2); if (!zCtnW.isNull() && zCtnW.getConst<bool>()) { return true; @@ -680,7 +684,7 @@ Node StringsEntail::checkContains(Node a, Node b, bool fullRewriter) do { prev = ctn; - ctn = SequencesRewriter::rewriteContains(ctn); + ctn = d_rewriter.rewriteContains(ctn); } while (prev != ctn && ctn.getKind() == STRING_STRCTN); } diff --git a/src/theory/strings/strings_entail.h b/src/theory/strings/strings_entail.h index d4993faf4..379c09043 100644 --- a/src/theory/strings/strings_entail.h +++ b/src/theory/strings/strings_entail.h @@ -25,6 +25,8 @@ namespace CVC4 { namespace theory { namespace strings { +class SequencesRewriter; + /** * Entailment tests involving strings. * Some of these techniques are described in Reynolds et al, "High Level @@ -33,6 +35,8 @@ namespace strings { class StringsEntail { public: + StringsEntail(SequencesRewriter& rewriter); + /** can constant contain list * return true if constant c can contain the list l in order * firstc/lastc store which indices in l were used to determine the return @@ -153,12 +157,12 @@ class StringsEntail * n1 is updated to { "c", x, "def" }, * nb is updated to { y, "ab" } */ - static int componentContains(std::vector<Node>& n1, - std::vector<Node>& n2, - std::vector<Node>& nb, - std::vector<Node>& ne, - bool computeRemainder = false, - int remainderDir = 0); + int componentContains(std::vector<Node>& n1, + std::vector<Node>& n2, + std::vector<Node>& nb, + std::vector<Node>& ne, + bool computeRemainder = false, + int remainderDir = 0); /** strip constant endpoints * This function is used when rewriting str.contains( t1, t2 ), where * n1 is the vector form of t1 @@ -208,7 +212,7 @@ class StringsEntail * @return true node if it can be shown that `a` contains `b`, false node if * it can be shown that `a` does not contain `b`, null node otherwise */ - static Node checkContains(Node a, Node b, bool fullRewriter = true); + Node checkContains(Node a, Node b, bool fullRewriter = true); /** entail non-empty * @@ -346,7 +350,7 @@ class StringsEntail * Since we do not wish to introduce ITE terms in the rewriter, we instead * return false, indicating that we cannot compute the remainder. */ - static bool componentContainsBase( + bool componentContainsBase( Node n1, Node n2, Node& n1rb, Node& n1re, int dir, bool computeRemainder); /** * Simplifies a given node `a` s.t. the result is a concatenation of string @@ -362,6 +366,13 @@ class StringsEntail * @return A concatenation that can be interpreted as a multiset */ static Node getMultisetApproximation(Node a); + + private: + /** + * Reference to the sequences rewriter that owns this `StringsEntail` + * instance. + */ + SequencesRewriter& d_rewriter; }; } // namespace strings diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index 28ed14095..f27a19065 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -25,6 +25,67 @@ namespace CVC4 { namespace theory { namespace strings { +StringsRewriter::StringsRewriter(HistogramStat<Rewrite>* statistics) + : SequencesRewriter(statistics) +{ +} + +RewriteResponse StringsRewriter::postRewrite(TNode node) +{ + Trace("strings-postrewrite") + << "Strings::StringsRewriter::postRewrite start " << node << std::endl; + + Node retNode = node; + Kind nk = node.getKind(); + if (nk == kind::STRING_LT) + { + retNode = rewriteStringLt(node); + } + else if (nk == kind::STRING_LEQ) + { + retNode = rewriteStringLeq(node); + } + else if (nk == STRING_TOLOWER || nk == STRING_TOUPPER) + { + retNode = rewriteStrConvert(node); + } + else if (nk == STRING_IS_DIGIT) + { + retNode = rewriteStringIsDigit(node); + } + else if (nk == kind::STRING_ITOS) + { + retNode = rewriteIntToStr(node); + } + else if (nk == kind::STRING_STOI) + { + retNode = rewriteStrToInt(node); + } + else if (nk == STRING_TO_CODE) + { + retNode = rewriteStringToCode(node); + } + else if (nk == STRING_FROM_CODE) + { + retNode = rewriteStringFromCode(node); + } + else + { + return SequencesRewriter::postRewrite(node); + } + + Trace("strings-postrewrite") + << "Strings::StringsRewriter::postRewrite returning " << retNode + << std::endl; + if (node != retNode) + { + Trace("strings-rewrite-debug") << "Strings::StringsRewriter::postRewrite " + << node << " to " << retNode << std::endl; + return RewriteResponse(REWRITE_AGAIN_FULL, retNode); + } + return RewriteResponse(REWRITE_DONE, retNode); +} + Node StringsRewriter::rewriteStrToInt(Node node) { Assert(node.getKind() == STRING_STOI); diff --git a/src/theory/strings/strings_rewriter.h b/src/theory/strings/strings_rewriter.h index 0c5b0b2f8..ce4be476d 100644 --- a/src/theory/strings/strings_rewriter.h +++ b/src/theory/strings/strings_rewriter.h @@ -32,13 +32,17 @@ namespace strings { class StringsRewriter : public SequencesRewriter { public: + StringsRewriter(HistogramStat<Rewrite>* statistics); + + RewriteResponse postRewrite(TNode node) override; + /** rewrite string to integer * * This is the entry point for post-rewriting terms n of the form * str.to_int( s ) * Returns the rewritten form of n. */ - static Node rewriteStrToInt(Node n); + Node rewriteStrToInt(Node n); /** rewrite integer to string * @@ -46,7 +50,7 @@ class StringsRewriter : public SequencesRewriter * str.from_int( i ) * Returns the rewritten form of n. */ - static Node rewriteIntToStr(Node n); + Node rewriteIntToStr(Node n); /** rewrite string convert * @@ -54,7 +58,7 @@ class StringsRewriter : public SequencesRewriter * str.tolower( s ) and str.toupper( s ) * Returns the rewritten form of n. */ - static Node rewriteStrConvert(Node n); + Node rewriteStrConvert(Node n); /** rewrite string less than * @@ -62,7 +66,7 @@ class StringsRewriter : public SequencesRewriter * str.<( t, s ) * Returns the rewritten form of n. */ - static Node rewriteStringLt(Node n); + Node rewriteStringLt(Node n); /** rewrite string less than or equal * @@ -70,7 +74,7 @@ class StringsRewriter : public SequencesRewriter * str.<=( t, s ) * Returns the rewritten form of n. */ - static Node rewriteStringLeq(Node n); + Node rewriteStringLeq(Node n); /** rewrite str.from_code * @@ -78,7 +82,7 @@ class StringsRewriter : public SequencesRewriter * str.from_code( t ) * Returns the rewritten form of n. */ - static Node rewriteStringFromCode(Node n); + Node rewriteStringFromCode(Node n); /** rewrite str.to_code * @@ -86,7 +90,7 @@ class StringsRewriter : public SequencesRewriter * str.to_code( t ) * Returns the rewritten form of n. */ - static Node rewriteStringToCode(Node n); + Node rewriteStringToCode(Node n); /** rewrite is digit * @@ -94,7 +98,7 @@ class StringsRewriter : public SequencesRewriter * str.is_digit( t ) * Returns the rewritten form of n. */ - static Node rewriteStringIsDigit(Node n); + Node rewriteStringIsDigit(Node n); }; } // namespace strings diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index d5eb2dbbd..d74a0e9ca 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -26,7 +26,6 @@ #include "smt/smt_statistics_registry.h" #include "theory/ext_theory.h" #include "theory/rewriter.h" -#include "theory/strings/sequences_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/type_enumerator.h" #include "theory/strings/word.h" @@ -70,6 +69,7 @@ TheoryStrings::TheoryStrings(context::Context* c, const LogicInfo& logicInfo) : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo), d_notify(*this), + d_statistics(), d_equalityEngine(d_notify, c, "theory::strings::ee", true), d_state(c, d_equalityEngine, d_valuation), d_im(*this, c, u, d_state, d_sk_cache, out, d_statistics), @@ -77,6 +77,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_registered_terms_cache(u), d_functionsTerms(c), d_has_str_code(false), + d_rewriter(&d_statistics.d_rewrites), d_bsolver(c, u, d_state, d_im), d_csolver(c, u, d_state, d_im, d_sk_cache, d_bsolver), d_esolver(nullptr), @@ -91,6 +92,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_state, d_im, d_sk_cache, + d_rewriter, d_bsolver, d_csolver, extt, @@ -131,11 +133,6 @@ TheoryStrings::~TheoryStrings() { } -std::unique_ptr<TheoryRewriter> TheoryStrings::mkTheoryRewriter() -{ - return std::unique_ptr<TheoryRewriter>(new SequencesRewriter()); -} - bool TheoryStrings::areCareDisequal( TNode x, TNode y ) { Assert(d_equalityEngine.hasTerm(x)); Assert(d_equalityEngine.hasTerm(y)); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 0e95628bc..5ae0ac7a9 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -39,6 +39,7 @@ #include "theory/strings/skolem_cache.h" #include "theory/strings/solver_state.h" #include "theory/strings/strings_fmf.h" +#include "theory/strings/strings_rewriter.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -109,7 +110,7 @@ class TheoryStrings : public Theory { const LogicInfo& logicInfo); ~TheoryStrings(); - std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override; + TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } void setMasterEqualityEngine(eq::EqualityEngine* eq) override; @@ -352,6 +353,9 @@ private: // Symbolic Regular Expression private: + /** The theory rewriter for this theory. */ + StringsRewriter d_rewriter; + /** * The base solver, responsible for reasoning about congruent terms and * inferring constants for equivalence classes. diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 097cef235..5fc13f023 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -79,7 +79,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node sk2 = ArithEntail::check(t12, lt0) ? emp : d_sc->mkSkolemCached( - s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr"); + s, t12, SkolemCache::SK_SUFFIX_REM, "sssufr"); Node b11 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, skt, sk2)); //length of first skolem is second argument Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n); |