1 files changed, 25 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 1479f910e..18aaab01f 100755
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -18,6 +18,7 @@
 #define __CVC4__THEORY__QUANT_UTIL_H
 
 #include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
 
 #include <ext/hash_set>
 #include <iostream>
@@ -71,6 +72,30 @@ public:
   std::map< Node, Node > d_phase_reqs_equality_term;
 };
 
+
+class EqualityQuery {
+public:
+  EqualityQuery(){}
+  virtual ~EqualityQuery(){};
+  /** contains term */
+  virtual bool hasTerm( Node a ) = 0;
+  /** get the representative of the equivalence class of a */
+  virtual Node getRepresentative( Node a ) = 0;
+  /** returns true if a and b are equal in the current context */
+  virtual bool areEqual( Node a, Node b ) = 0;
+  /** returns true is a and b are disequal in the current context */
+  virtual bool areDisequal( Node a, Node b ) = 0;
+  /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
+      If cbqi is active, this will return a term in the equivalence class of "a" that does
+      not contain instantiation constants, if such a term exists.
+   */
+  virtual Node getInternalRepresentative( Node a ) = 0;
+  /** get the equality engine associated with this query */
+  virtual eq::EqualityEngine* getEngine() = 0;
+  /** get the equivalence class of a */
+  virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) = 0;
+};/* class EqualityQuery */
+
 }
 }