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

2 files changed, 31 insertions, 8 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 8daa0149f..ad89a2aaa 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -17,7 +17,6 @@
 #define __CVC4__THEORY__THEORY_H
 
 #include "expr/node.h"
-#include "util/literal.h"
 #include "theory/output_channel.h"
 
 namespace CVC4 {
@@ -31,7 +30,7 @@ class Theory {
   /**
    * Return whether a node is shared or not.  Used by setup().
    */
-  bool isShared(Node);
+  bool isShared(const Node& n);
 
 public:
 
@@ -66,29 +65,33 @@ public:
   /**
    * Prepare for a Node.
    */
-  virtual void setup(Node) = 0;
+  virtual void setup(const Node& n) = 0;
 
   /**
-   * Assert a literal in the current context.
+   * Assert a fact in the current context.
    */
-  void assertLiteral(Literal);
+  void assertFact(const Node& n);
 
   /**
    * Check the current assignment's consistency.
    */
-  virtual void check(OutputChannel& out, Effort level = FULL_EFFORT) = 0;
+  virtual void check(OutputChannel& out,
+                     Effort level = FULL_EFFORT) = 0;
 
   /**
    * T-propagate new literal assignments in the current context.
    */
-  virtual void propagate(OutputChannel& out, Effort level = FULL_EFFORT) = 0;
+  virtual void propagate(OutputChannel& out,
+                         Effort level = FULL_EFFORT) = 0;
 
   /**
    * Return an explanation for the literal represented by parameter n
    * (which was previously propagated by this theory).  Report
    * explanations to an output channel.
    */
-  virtual void explain(OutputChannel& out, Node n, Effort level = FULL_EFFORT) = 0;
+  virtual void explain(OutputChannel& out,
+                       const Node& n,
+                       Effort level = FULL_EFFORT) = 0;
 
 };/* class Theory */
 
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 */