summaryrefslogtreecommitdiff
path: root/src/theory/strings
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings')
-rw-r--r--src/theory/strings/arith_entail.cpp6
-rw-r--r--src/theory/strings/extf_solver.cpp10
-rw-r--r--src/theory/strings/extf_solver.h8
-rw-r--r--src/theory/strings/regexp_entail.cpp4
-rw-r--r--src/theory/strings/sequences_rewriter.cpp96
-rw-r--r--src/theory/strings/sequences_rewriter.h65
-rw-r--r--src/theory/strings/sequences_stats.cpp3
-rw-r--r--src/theory/strings/sequences_stats.h3
-rw-r--r--src/theory/strings/strings_entail.cpp10
-rw-r--r--src/theory/strings/strings_entail.h27
-rw-r--r--src/theory/strings/strings_rewriter.cpp61
-rw-r--r--src/theory/strings/strings_rewriter.h20
-rw-r--r--src/theory/strings/theory_strings.cpp9
-rw-r--r--src/theory/strings/theory_strings.h6
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp2
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback