diff options
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r-- | src/theory/bv/theory_bv.h | 6 |
1 files changed, 5 insertions, 1 deletions
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; |