diff options
author | Liana Hadarean <lianahady@gmail.com> | 2013-09-30 13:56:51 -0400 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2013-09-30 13:56:51 -0400 |
commit | 7d2265eb2b5dc96ddff04211959e208b1cb8a7f0 (patch) | |
tree | 26fb270349580c90efe163ca7767bccce6607902 /src/theory/bv/bv_subtheory.h | |
parent | db6df44574927f9b75db664e1e490f757725d13a (diff) | |
parent | 0c2eafec69b694a507ac914bf285fe0574be085f (diff) |
merged golden
Diffstat (limited to 'src/theory/bv/bv_subtheory.h')
-rw-r--r-- | src/theory/bv/bv_subtheory.h | 29 |
1 files changed, 13 insertions, 16 deletions
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 8374a3f75..0b0551283 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -9,7 +9,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Algebraic solver. + ** \brief Algebraic solver. ** ** Algebraic solver. **/ @@ -46,7 +46,7 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) { out << "BV_CORE_SUBTHEORY"; break; case SUB_INEQUALITY: - out << "BV_INEQUALITY_SUBTHEORY"; + out << "BV_INEQUALITY_SUBTHEORY"; default: Unreachable(); break; @@ -55,13 +55,10 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) { } -const bool d_useEqualityEngine = true; -const bool d_useSatPropagation = true; +// forward declaration +class TheoryBV; -// forward declaration -class TheoryBV; - -typedef context::CDQueue<Node> AssertionQueue; +typedef context::CDQueue<Node> AssertionQueue; /** * Abstract base class for bit-vector subtheory solvers * @@ -78,7 +75,7 @@ protected: AssertionQueue d_assertionQueue; context::CDO<uint32_t> d_assertionIndex; public: - + SubtheorySolver(context::Context* c, TheoryBV* bv) : d_context(c), d_bv(bv), @@ -86,24 +83,24 @@ public: d_assertionIndex(c, 0) {} virtual ~SubtheorySolver() {} - virtual bool check(Theory::Effort e) = 0; + virtual bool check(Theory::Effort e) = 0; virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0; virtual void preRegister(TNode node) {} virtual void propagate(Theory::Effort e) {} - virtual void collectModelInfo(TheoryModel* m) = 0; - virtual Node getModelValue(TNode var) = 0; + virtual void collectModelInfo(TheoryModel* m, bool fullModel) = 0; + virtual Node getModelValue(TNode var) = 0; virtual bool isComplete() = 0; virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0; - virtual void addSharedTerm(TNode node) {} + 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; + return res; } virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); } -}; +}; } } |