diff options
author | Tim King <taking@cs.nyu.edu> | 2017-09-26 07:33:31 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2017-09-26 07:33:31 -0700 |
commit | 5854353603d5a3ce7e3a5914f1b6d29728d24ac2 (patch) | |
tree | 95d8f6905575ad801458a917fe01b08ceefea99f /src/theory | |
parent | ced4d68203bd78c9a59de569995751212d36067a (diff) |
Fixing CID 1362903: Initializing d_bvp to nullptr. (#1136)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/bv_subtheory.h | 61 |
1 files changed, 32 insertions, 29 deletions
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 4f074a202..deb366a99 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -60,32 +60,20 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) { // forward declaration class TheoryBV; -typedef context::CDQueue<Node> AssertionQueue; +using AssertionQueue = context::CDQueue<Node>; + /** * Abstract base class for bit-vector subtheory solvers * */ class SubtheorySolver { - -protected: - - /** The context we are using */ - context::Context* d_context; - - /** The bit-vector theory */ - TheoryBV* d_bv; - /** proof log */ - BitVectorProof * d_bvp; - AssertionQueue d_assertionQueue; - context::CDO<uint32_t> d_assertionIndex; -public: - - SubtheorySolver(context::Context* c, TheoryBV* bv) : - d_context(c), - d_bv(bv), - d_assertionQueue(c), - d_assertionIndex(c, 0) - {} + public: + SubtheorySolver(context::Context* c, TheoryBV* bv) + : d_context(c), + d_bv(bv), + d_bvp(nullptr), + d_assertionQueue(c), + d_assertionIndex(c, 0) {} virtual ~SubtheorySolver() {} virtual bool check(Theory::Effort e) = 0; virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0; @@ -98,19 +86,34 @@ public: virtual void addSharedTerm(TNode node) {} bool done() { return d_assertionQueue.size() == d_assertionIndex; } TNode get() { - Assert (!done()); + Assert(!done()); TNode res = d_assertionQueue[d_assertionIndex]; d_assertionIndex = d_assertionIndex + 1; return res; } virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); } - virtual void setProofLog( BitVectorProof * bvp ) {} - AssertionQueue::const_iterator assertionsBegin() { return d_assertionQueue.begin(); } - AssertionQueue::const_iterator assertionsEnd() { return d_assertionQueue.end(); } -}; + virtual void setProofLog(BitVectorProof* bvp) {} + AssertionQueue::const_iterator assertionsBegin() { + return d_assertionQueue.begin(); + } + AssertionQueue::const_iterator assertionsEnd() { + return d_assertionQueue.end(); + } -} -} -} + protected: + /** The context we are using */ + context::Context* d_context; + + /** The bit-vector theory */ + TheoryBV* d_bv; + /** proof log */ + BitVectorProof* d_bvp; + AssertionQueue d_assertionQueue; + context::CDO<uint32_t> d_assertionIndex; +}; /* class SubtheorySolver */ + +} // namespace bv +} // namespace theory +} // namespace CVC4 #endif /* __CVC4__THEORY__BV__BV_SUBTHEORY_H */ |