diff options
| author | lianah <lianahady@gmail.com> | 2013-03-16 15:48:51 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-03-16 15:48:51 -0400 |
| commit | 25ac2c8f4b45e2b299895e97a30790fbf46cf79f (patch) | |
| tree | d7b52003d7157073be554bd9818230f1c3b439d3 /src/theory/bv/bv_subtheory.h | |
| parent | 3fcdb18fe92e5213aa708285c0d7d5e55633492b (diff) | |
started work on the inequality bv subtheory
Diffstat (limited to 'src/theory/bv/bv_subtheory.h')
| -rw-r--r-- | src/theory/bv/bv_subtheory.h | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index d95aaa873..9e7566ebb 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -32,9 +32,9 @@ class TheoryModel; namespace bv { enum SubTheory { - SUB_EQUALITY = 1, + SUB_CORE = 1, SUB_BITBLAST = 2, - SUB_CORE = 3 + SUB_INEQUALITY = 3 }; inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) { @@ -42,9 +42,11 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) { case SUB_BITBLAST: out << "BITBLASTER"; break; - case SUB_EQUALITY: - out << "EQUALITY"; + case SUB_CORE: + out << "BV_CORE_SUBTHEORY"; break; + case SUB_INEQUALITY: + out << "BV_INEQUALITY_SUBTHEORY"; default: Unreachable(); break; @@ -83,10 +85,10 @@ public: 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 propagate(Effort e) {} virtual void collectModelInfo(TheoryModel* m) = 0; bool done() { return d_assertionQueue.size() == d_assertionIndex; } TNode get() { |