diff options
author | lianah <lianahady@gmail.com> | 2013-03-13 13:44:33 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-03-13 13:44:33 -0400 |
commit | 3fcdb18fe92e5213aa708285c0d7d5e55633492b (patch) | |
tree | bbbd57efd9a8063a976a55afa7c384fb67db9b17 /src/theory/bv/bv_subtheory.h | |
parent | 267ad0ceb6808bd4c05d7c4bb04a7886efc19eab (diff) | |
parent | 9817df56827b4ee0ee67a33361f8619c5d1df6ed (diff) |
post failed attempts at getting the incremental solver to work
Diffstat (limited to 'src/theory/bv/bv_subtheory.h')
-rw-r--r-- | src/theory/bv/bv_subtheory.h | 24 |
1 files changed, 18 insertions, 6 deletions
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index a256b6001..d95aaa873 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -72,19 +72,31 @@ protected: /** The bit-vector theory */ TheoryBV* d_bv; - + context::CDQueue<TNode> d_assertionQueue; + context::CDO<uint32_t> d_assertionIndex; public: SubtheorySolver(context::Context* c, TheoryBV* bv) : d_context(c), - d_bv(bv) + d_bv(bv), + 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; + virtual void preRegister(TNode node) {} + virtual void collectModelInfo(TheoryModel* m) = 0; + bool done() { return d_assertionQueue.size() == d_assertionIndex; } + TNode get() { + Assert (!done()); + TNode res = d_assertionQueue[d_assertionIndex]; + d_assertionIndex = d_assertionIndex + 1; + return res; + } + void assertFact(TNode fact) { d_assertionQueue.push_back(fact); } - virtual bool addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) = 0; - virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0; - virtual void preRegister(TNode node) {} - virtual void collectModelInfo(TheoryModel* m) = 0; }; } |