diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 5 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 6 |
2 files changed, 5 insertions, 6 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 27718b63f..94fc1e34c 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -112,11 +112,6 @@ TheoryBV::TheoryBV(context::Context* c, TheoryBV::~TheoryBV() {} -std::unique_ptr<TheoryRewriter> TheoryBV::mkTheoryRewriter() -{ - return std::unique_ptr<TheoryRewriter>(new TheoryBVRewriter()); -} - void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { if (options::bitblastMode() == options::BitblastMode::EAGER) { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index ff1c9245a..bc54a09e7 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -26,6 +26,7 @@ #include "context/cdlist.h" #include "context/context.h" #include "theory/bv/bv_subtheory.h" +#include "theory/bv/theory_bv_rewriter.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory.h" #include "util/hash.h" @@ -72,7 +73,7 @@ public: ~TheoryBV(); - std::unique_ptr<TheoryRewriter> mkTheoryRewriter() override; + TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; } void setMasterEqualityEngine(eq::EqualityEngine* eq) override; @@ -259,6 +260,9 @@ public: void checkForLemma(TNode node); + /** The theory rewriter for this theory. */ + TheoryBVRewriter d_rewriter; + friend class LazyBitblaster; friend class TLazyBitblaster; friend class EagerBitblaster; |