diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-16 16:18:52 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-16 16:18:52 +0000 |
commit | 9154e647013e4575f60807d5b73582bccfd052e2 (patch) | |
tree | d32c32473a9eea80798c2e4ae60b9420a05e5c57 /src/theory/bv/bv_subtheory.h | |
parent | 6d4822f197ccd235175669f199e922aa12eda4b1 (diff) |
equality status for bitvectors can now look into the sat solver to check for IN_MODEL status
Diffstat (limited to 'src/theory/bv/bv_subtheory.h')
-rw-r--r-- | src/theory/bv/bv_subtheory.h | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index cc62013fd..db7bad30c 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -68,9 +68,7 @@ public: /** * BitblastSolver - * */ - class BitblastSolver : public SubtheorySolver { /** Bitblaster */ @@ -86,14 +84,13 @@ public: void preRegister(TNode node); bool addAssertions(const std::vector<TNode>& assertions, Theory::Effort e); void explain(TNode literal, std::vector<TNode>& assumptions); + EqualityStatus getEqualityStatus(TNode a, TNode b); }; /** * EqualitySolver - * */ - class EqualitySolver : public SubtheorySolver { // NotifyClass: handles call-back from congruence closure module @@ -107,7 +104,7 @@ class EqualitySolver : public SubtheorySolver { bool eqNotifyTriggerPredicate(TNode predicate, bool value); bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value); bool eqNotifyConstantTermMerge(TNode t1, TNode t2); - }; +}; /** The notify class for d_equalityEngine */ @@ -140,11 +137,6 @@ public: }; -// class CoreSolver : public SubtheorySolver { - -// }; - - } } } |