diff options
Diffstat (limited to 'src/theory/bv/bv_subtheory.h')
-rw-r--r-- | src/theory/bv/bv_subtheory.h | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 725b61f95..f4b88b719 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -25,10 +25,6 @@ namespace CVC4 { -namespace proof { -class BitVectorProof; -} - namespace theory { class TheoryModel; @@ -72,7 +68,6 @@ class SubtheorySolver { SubtheorySolver(context::Context* c, TheoryBV* bv) : d_context(c), d_bv(bv), - d_bvp(nullptr), d_assertionQueue(c), d_assertionIndex(c, 0) {} virtual ~SubtheorySolver() {} @@ -93,7 +88,7 @@ class SubtheorySolver { return res; } virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); } - virtual void setProofLog(proof::BitVectorProof* bvp) {} + AssertionQueue::const_iterator assertionsBegin() { return d_assertionQueue.begin(); } @@ -107,8 +102,6 @@ class SubtheorySolver { /** The bit-vector theory */ TheoryBV* d_bv; - /** proof log */ - proof::ResolutionBitVectorProof* d_bvp; AssertionQueue d_assertionQueue; context::CDO<uint32_t> d_assertionIndex; }; /* class SubtheorySolver */ |