diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index a81c96318..f9eeb2010 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -26,6 +26,7 @@ #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" @@ -129,6 +130,11 @@ 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)); |