minor interface changes to TheoryEngine/Theory after meeting and conversation with Tim

1 files changed, 20 insertions, 0 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 3fb11b510..348d7e6df 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -16,8 +16,13 @@
 #ifndef __CVC4__THEORY_ENGINE_H
 #define __CVC4__THEORY_ENGINE_H
 
+#include "expr/node.h"
+#include "theory/theory.h"
+
 namespace CVC4 {
 
+class SmtEngine;
+
 // In terms of abstraction, this is below (and provides services to)
 // PropEngine.
 
@@ -28,7 +33,22 @@ namespace CVC4 {
  * CVC4.
  */
 class TheoryEngine {
+
+  SmtEngine* d_smt;
+
 public:
+
+  /**
+   * Construct a theory engine.
+   */
+  TheoryEngine(SmtEngine* smt) : d_smt(smt) {
+  }
+
+  /**
+   * Get the theory associated to a given Node.
+   */
+  CVC4::theory::Theory* theoryOf(const Node& n);
+
 };/* class TheoryEngine */
 
 }/* CVC4 namespace */