Initial draft of CEGQI.

1 files changed, 10 insertions, 1 deletions

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index d40277112..b5a02df60 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -37,6 +37,10 @@ namespace theory {
 
 class QuantifiersEngine;
 
+namespace quantifiers {
+  class TermDb;
+}
+
 class QuantifiersModule {
 protected:
   QuantifiersEngine* d_quantEngine;
@@ -61,10 +65,15 @@ public:
   virtual Node explain(TNode n) { return TNode::null(); }
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   virtual std::string identify() const = 0;
+public:
+  eq::EqualityEngine * getEqualityEngine();
+  bool areDisequal( TNode n1, TNode n2 );
+  bool areEqual( TNode n1, TNode n2 );
+  TNode getRepresentative( TNode n );
+  quantifiers::TermDb * getTermDatabase();
 };/* class QuantifiersModule */
 
 namespace quantifiers {
-  class TermDb;
   class FirstOrderModel;
   //modules
   class InstantiationEngine;