diff options
Diffstat (limited to 'src/theory/strings/strings_entail.cpp')
-rw-r--r-- | src/theory/strings/strings_entail.cpp | 10 |
1 files changed, 7 insertions, 3 deletions
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); } |