diff options
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r-- | src/theory/bv/theory_bv.h | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index afa9f4b4f..3d151cfb1 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -31,6 +31,14 @@ #include "util/hash.h" #include "util/statistics_registry.h" +// Forward declarations, needed because the BV theory and the BV Proof classes +// are cyclically dependent +namespace CVC4 { +namespace proof { +class BitVectorProof; +} +} // namespace CVC4 + namespace CVC4 { namespace theory { namespace bv { @@ -104,7 +112,7 @@ public: bool applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); - void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp); + void setProofLog(proof::BitVectorProof* bvp); private: |