diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-05-16 15:21:18 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-05-16 15:21:18 +0000 |
commit | 1a890e13218be6e87dbf0124b03a73420631d816 (patch) | |
tree | 00d11474eda0adf95c285ee93f468833518cf3ad /src/theory/bv/theory_bv.h | |
parent | 03930f2a6fdfb85ecc81594ec65f41d7c1284577 (diff) |
refactored TheoryBV bitblaster and equality engine into subtheories (similar to TheoryEngine
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r-- | src/theory/bv/theory_bv.h | 97 |
1 files changed, 17 insertions, 80 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 9ab5f8e1c..214fa3b36 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -27,40 +27,24 @@ #include "context/cdhashset.h" #include "theory/bv/theory_bv_utils.h" #include "util/stats.h" -#include "theory/uf/equality_engine.h" #include "context/cdqueue.h" - -namespace BVMinisat { -class SimpSolver; -} - +#include "theory/bv/bv_subtheory.h" namespace CVC4 { namespace theory { namespace bv { -/// forward declarations -class Bitblaster; - class TheoryBV : public Theory { - -private: - /** The context we are using */ context::Context* d_context; - /** The asserted stuff */ - context::CDList<TNode> d_assertions; - - /** Bitblaster */ - Bitblaster* d_bitblaster; - - context::CDQueue<TNode> d_bitblastQueue; - /** Context dependent set of atoms we already propagated */ context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet; context::CDHashSet<TNode, TNodeHashFunction> d_sharedTermsSet; + + BitblastSolver d_bitblastSolver; + EqualitySolver d_equalitySolver; public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); @@ -70,6 +54,8 @@ public: void check(Effort e); + void propagate(Effort e); + Node explain(TNode n); Node getValue(TNode n); @@ -91,58 +77,6 @@ private: Statistics d_statistics; - // Added by Clark - // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module - class NotifyClass : public eq::EqualityEngineNotify { - - TheoryBV& d_bv; - - public: - - NotifyClass(TheoryBV& uf): d_bv(uf) {} - - bool eqNotifyTriggerEquality(TNode equality, bool value) { - Debug("bitvector") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; - if (value) { - return d_bv.storePropagation(equality, SUB_EQUALITY); - } else { - return d_bv.storePropagation(equality.notNode(), SUB_EQUALITY); - } - } - - bool eqNotifyTriggerPredicate(TNode predicate, bool value) { - Debug("bitvector") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl; - if (value) { - return d_bv.storePropagation(predicate, SUB_EQUALITY); - } else { - return d_bv.storePropagation(predicate.notNode(), SUB_EQUALITY); - } - } - - bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) { - Debug("bitvector") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl; - if (value) { - return d_bv.storePropagation(t1.eqNode(t2), SUB_EQUALITY); - } else { - return d_bv.storePropagation(t1.eqNode(t2).notNode(), SUB_EQUALITY); - } - } - - bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { - Debug("bitvector") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl; - if (Theory::theoryOf(t1) == THEORY_BOOL) { - return d_bv.storePropagation(t1.iffNode(t2), SUB_EQUALITY); - } - return d_bv.storePropagation(t1.eqNode(t2), SUB_EQUALITY); - } - }; - - /** The notify class for d_equalityEngine */ - NotifyClass d_notify; - - /** Equaltity engine */ - eq::EqualityEngine d_equalityEngine; - // Are we in conflict? context::CDO<bool> d_conflict; @@ -155,11 +89,9 @@ private: /** Index of the next literal to propagate */ context::CDO<unsigned> d_literalsToPropagateIndex; - context::CDQueue<Node> d_toBitBlast; - enum SubTheory { SUB_EQUALITY = 1, - SUB_BITBLASTER = 2 + SUB_BITBLAST = 2 }; /** @@ -187,17 +119,22 @@ private: EqualityStatus getEqualityStatus(TNode a, TNode b); - friend class Bitblaster; - inline std::string indent() { std::string indentStr(getSatContext()->getLevel(), ' '); return indentStr; } - -public: - void propagate(Effort e); + void setConflict(Node conflict) { + d_conflict = true; + d_conflictNode = conflict; + } + + bool inConflict() { return d_conflict == true; } + + friend class Bitblaster; + friend class BitblastSolver; + friend class EqualitySolver; };/* class TheoryBV */ |