equality status for bitvectors can now look into the sat solver to check for IN_MODEL status

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 {
-  
-// }; 
-
-
 }
 }
 }