22 files changed, 590 insertions, 104 deletions

diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index f6f4ae07e..951dbeb78 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -6,14 +6,34 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden
 noinst_LTLIBRARIES = libtheory.la
 
 libtheory_la_SOURCES = \
+	@srcdir@/theoryof_table.h \
 	theory_engine.h \
 	theory_engine.cpp \
 	theory.h \
 	theory.cpp
 
 libtheory_la_LIBADD = \
-	@builddir@/bool/libbool.la
-	@builddir@/uf/libuf.la
-	@builddir@/uf/libarith.la
+	@builddir@/booleans/libbooleans.la \
+	@builddir@/uf/libuf.la \
+	@builddir@/arith/libarith.la
 
-SUBDIRS = bool uf arith
+EXTRA_DIST = \
+	@srcdir@/theoryof_table.h \
+	theoryof_table_prologue.h \
+	theoryof_table_middle.h \
+	theoryof_table_epilogue.h
+
+@srcdir@/theoryof_table.h: @srcdir@/mktheoryof theoryof_table_prologue.h theoryof_table_middle.h theoryof_table_epilogue.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+	chmod +x @srcdir@/mktheoryof
+	(@srcdir@/mktheoryof \
+		@srcdir@/theoryof_table_prologue.h \
+		@srcdir@/theoryof_table_middle.h \
+		@srcdir@/theoryof_table_epilogue.h \
+		`grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
+	> @srcdir@/theoryof_table.h) || (rm -f @srcdir@/theoryof_table.h && exit 1)
+
+BUILT_SOURCES = @srcdir@/theoryof_table.h
+dist-hook: @srcdir@/theoryof_table.h
+MAINTAINERCLEANFILES = @srcdir@/theoryof_table.h
+
+SUBDIRS = booleans uf arith
diff --git a/src/theory/arith/Makefile b/src/theory/arith/Makefile
new file mode 100644
index 000000000..5016522e8
--- /dev/null
+++ b/src/theory/arith/Makefile
@@ -0,0 +1,4 @@
+topdir = ../../..
+srcdir = src/theory/arith
+
+include $(topdir)/Makefile.subdir
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 461659765..226d5af12 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -5,6 +5,8 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden
 
 noinst_LTLIBRARIES = libarith.la
 
-libarith_la_SOURCES =
+libarith_la_SOURCES = \
+	theory_def.h \
+	theory_arith.h
 
 EXTRA_DIST = kinds
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
new file mode 100644
index 000000000..5b596afd4
--- /dev/null
+++ b/src/theory/arith/theory_arith.h
@@ -0,0 +1,23 @@
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+class TheoryArith : public TheoryImpl<TheoryArith> {
+public:
+  TheoryArith(context::Context* c, OutputChannel& out) :
+    TheoryImpl<TheoryArith>(c, out) {
+  }
+
+  void preRegisterTerm(TNode n) { Unimplemented(); }
+  void registerTerm(TNode n) { Unimplemented(); }
+  void check(Effort e) { Unimplemented(); }
+  void propagate(Effort e) { Unimplemented(); }
+  void explain(TNode n, Effort e) { Unimplemented(); }
+};
+
+}
+}
+}
+
diff --git a/src/theory/arith/theory_def.h b/src/theory/arith/theory_def.h
new file mode 100644
index 000000000..9b01a458e
--- /dev/null
+++ b/src/theory/arith/theory_def.h
@@ -0,0 +1,9 @@
+#include "theory/arith/theory_arith.h"
+
+namespace CVC4 {
+  namespace theory {
+    namespace arith {
+      typedef TheoryArith TheoryARITH;
+    }
+  }
+}
diff --git a/src/theory/booleans/Makefile b/src/theory/booleans/Makefile
new file mode 100644
index 000000000..a74a72d83
--- /dev/null
+++ b/src/theory/booleans/Makefile
@@ -0,0 +1,4 @@
+topdir = ../../..
+srcdir = src/theory/bool
+
+include $(topdir)/Makefile.subdir
diff --git a/src/theory/bool/Makefile.am b/src/theory/booleans/Makefile.am
index 9c8b8365e..cbdf13add 100644
--- a/src/theory/bool/Makefile.am
+++ b/src/theory/booleans/Makefile.am
@@ -3,8 +3,10 @@ AM_CPPFLAGS = \
 	-I@srcdir@/../../include -I@srcdir@/../..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
 
-noinst_LTLIBRARIES = libbool.la
+noinst_LTLIBRARIES = libbooleans.la
 
-libbool_la_SOURCES =
+libbooleans_la_SOURCES = \
+	theory_def.h \
+	theory_bool.h
 
 EXTRA_DIST = kinds
diff --git a/src/theory/bool/kinds b/src/theory/booleans/kinds
index 7f1267383..7f1267383 100644
--- a/src/theory/bool/kinds
+++ b/src/theory/booleans/kinds
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
new file mode 100644
index 000000000..26e5a69fb
--- /dev/null
+++ b/src/theory/booleans/theory_bool.h
@@ -0,0 +1,24 @@
+#include "theory/theory.h"
+#include "context/context.h"
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+class TheoryBool : public TheoryImpl<TheoryBool> {
+public:
+  TheoryBool(context::Context* c, OutputChannel& out) :
+    TheoryImpl<TheoryBool>(c, out) {
+  }
+
+  void preRegisterTerm(TNode n) { Unimplemented(); }
+  void registerTerm(TNode n) { Unimplemented(); }
+  void check(Effort e) { Unimplemented(); }
+  void propagate(Effort e) { Unimplemented(); }
+  void explain(TNode n, Effort e) { Unimplemented(); }
+};
+
+}
+}
+}
+
diff --git a/src/theory/booleans/theory_def.h b/src/theory/booleans/theory_def.h
new file mode 100644
index 000000000..37aacb353
--- /dev/null
+++ b/src/theory/booleans/theory_def.h
@@ -0,0 +1,9 @@
+#include "theory/booleans/theory_bool.h"
+
+namespace CVC4 {
+  namespace theory {
+    namespace booleans {
+      typedef TheoryBool TheoryBOOLEANS;
+    }
+  }
+}
diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof
new file mode 100755
index 000000000..38c2153d6
--- /dev/null
+++ b/src/theory/mktheoryof
@@ -0,0 +1,57 @@
+#!/bin/bash
+#
+# mktheoryof
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+# Copyright (c) 2010  The CVC4 Project
+#
+# The purpose of this script is to create theoryof_table.h from a
+# prologue, epilogue, and a list of theory kinds.
+#
+# Invocation:
+#
+#   mktheoryof prologue-file epilogue-file theory-kind-files...
+#
+# Output is to standard out.
+#
+
+cat <<EOF
+/*********************                                           -*- C++ -*-  */
+/** theoryof_table.h
+ **
+ ** Copyright 2010  The AcSys Group, New York University, and as below.
+ **
+ ** This header file automatically generated by:
+ **
+ **     $0 $@
+ **
+ ** for the CVC4 project.
+ **/
+
+EOF
+
+prologue=$1; shift
+middle=$1; shift
+epilogue=$1; shift
+
+registers=
+cat "$prologue"
+while [ $# -gt 0 ]; do
+  b=$(basename $(dirname "$1"))
+  B=$(echo "$b" | tr 'a-z' 'A-Z')
+  echo "#include \"theory/$b/theory_def.h\""
+  registers="$registers
+  /* from $b */
+  void registerTheory(::CVC4::theory::$b::Theory$B* th) {
+"
+  for r in `cat "$1"`; do
+    registers="$registers    d_table[::CVC4::kind::$r] = th;
+"
+  done
+  registers="$registers  }
+"
+  shift
+done
+echo
+cat "$middle"
+echo "$registers"
+cat "$epilogue"
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index c530434f5..ad558e115 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -25,9 +25,21 @@ namespace theory {
  * Generic "theory output channel" interface.
  */
 class OutputChannel {
+  /** Disallow copying: private constructor */
+  OutputChannel(const OutputChannel&);
+
+  /** Disallow assignment: private operator=() */
+  OutputChannel& operator=(const OutputChannel&);
+
 public:
 
   /**
+   * Construct an OutputChannel.
+   */
+  OutputChannel() {
+  }
+
+  /**
    * Destructs an OutputChannel.  This implementation does nothing,
    * but we need a virtual destructor for safety in case subclasses
    * have a destructor.
@@ -39,24 +51,28 @@ public:
    * With safePoint(), the theory signals that it is at a safe point
    * and can be interrupted.
    */
-  virtual void safePoint() throw(Interrupted&) {
+  virtual void safePoint() throw(Interrupted) {
   }
 
   /**
    * Indicate a theory conflict has arisen.
    *
-   * @param n - a conflict at the current decision level
+   * @param n - a conflict at the current decision level.  This should
+   * be an OR-kinded node of literals that are false in the current
+   * assignment.
+   *
    * @param safe - whether it is safe to be interrupted
    */
-  virtual void conflict(Node n, bool safe = false) throw(Interrupted&) = 0;
+  virtual void conflict(TNode n, bool safe = false) throw(Interrupted) = 0;
 
   /**
    * Propagate a theory literal.
    *
-   * @param n - a theory consequence at the current decision level
+   * @param n - a theory consequence at the current decision level.
+   *
    * @param safe - whether it is safe to be interrupted
    */
-  virtual void propagate(Node n, bool safe = false) throw(Interrupted&) = 0;
+  virtual void propagate(TNode n, bool safe = false) throw(Interrupted) = 0;
 
   /**
    * Tell the core that a valid theory lemma at decision level 0 has
@@ -65,31 +81,7 @@ public:
    * @param n - a theory lemma valid at decision level 0
    * @param safe - whether it is safe to be interrupted
    */
-  virtual void lemma(Node n, bool safe = false) throw(Interrupted&) = 0;
-
-};/* class OutputChannel */
-
-/**
- * Generic "theory output channel" interface for explanations.
- */
-class ExplainOutputChannel {
-public:
-
-  /**
-   * Destructs an ExplainOutputChannel.  This implementation does
-   * nothing, but we need a virtual destructor for safety in case
-   * subclasses have a destructor.
-   */
-  virtual ~ExplainOutputChannel() {
-  }
-
-  /**
-   * With safePoint(), the theory signals that it is at a safe point
-   * and can be interrupted.  The default implementation never
-   * interrupts.
-   */
-  virtual void safePoint() throw(Interrupted&) {
-  }
+  virtual void lemma(TNode n, bool safe = false) throw(Interrupted) = 0;
 
   /**
    * Provide an explanation in response to an explanation request.
@@ -97,8 +89,9 @@ public:
    * @param n - an explanation
    * @param safe - whether it is safe to be interrupted
    */
-  virtual void explanation(Node n, bool safe = false) throw(Interrupted&) = 0;
-};/* class ExplainOutputChannel */
+  virtual void explanation(TNode n, bool safe = false) throw(Interrupted) = 0;
+
+};/* class OutputChannel */
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index cf52de75e..17a35f2ed 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -14,24 +14,14 @@
  **/
 
 #include "theory/theory.h"
+#include "util/Assert.h"
 
-namespace CVC4 {
-namespace theory {
-
-bool Theory::done() {
-  return d_nextAssertion >= d_assertions.size(); 
-}
+#include <vector>
 
+using namespace std;
 
-Node Theory::get() {
-  Node n = d_assertions[d_nextAssertion];
-  d_nextAssertion = d_nextAssertion + 1;
-  return n;
-}
-
-void Theory::assertFact(const Node& n){
-  d_assertions.push_back(n);
-}
+namespace CVC4 {
+namespace theory {
 
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 76b9697dc..e079d67bd 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -17,25 +17,91 @@
 #define __CVC4__THEORY__THEORY_H
 
 #include "expr/node.h"
+#include "expr/attribute.h"
 #include "theory/output_channel.h"
 #include "context/context.h"
 
+#include <queue>
+#include <vector>
+
+#include <typeinfo>
+
 namespace CVC4 {
 namespace theory {
 
+template <class T>
+class TheoryImpl;
+
 /**
  * Base class for T-solvers.  Abstract DPLL(T).
+ *
+ * This is essentially an interface class.  The TheoryEngine has
+ * pointers to Theory.  But each individual theory implementation T
+ * should inherit from TheoryImpl<T>, which specializes a few things
+ * for that theory.
  */
 class Theory {
+private:
+
+  template <class T>
+  friend class TheoryImpl;
+
+  /**
+   * Construct a Theory.
+   */
+  Theory(context::Context* ctxt, OutputChannel& out) throw() :
+    d_context(ctxt),
+    d_out(&out) {
+  }
+
+  /**
+   * Disallow default construction.
+   */
+  Theory();
+
+protected:
+
+  /**
+   * The output channel for the Theory.
+   */
+  context::Context* d_context;
+
+  /**
+   * The output channel for the Theory.
+   */
+  OutputChannel* d_out;
+
+  /**
+   * The assertFact() queue.
+   */
+  // FIXME CD: on backjump we clear the facts IFF the queue gets
+  // emptied on every DL.  In general I guess we need a CDQueue<>?
+  // Perhaps one that asserts it's empty at each push?
+  std::queue<Node> d_facts;
 
   /**
    * Return whether a node is shared or not.  Used by setup().
    */
-  bool isShared(const Node& n);
+  bool isShared(TNode n) throw();
+
+  /**
+   * Returns true if the assertFact queue is empty
+   */
+  bool done() throw() {
+    return d_facts.empty();
+  }
 
 public:
 
   /**
+   * Destructs a Theory.  This implementation does nothing, but we
+   * need a virtual destructor for safety in case subclasses have a
+   * destructor.
+   */
+  virtual ~Theory() {
+  }
+
+  /**
    * Subclasses of Theory may add additional efforts.  DO NOT CHECK
    * equality with one of these values (e.g. if STANDARD xxx) but
    * rather use range checks (or use the helper functions below).
@@ -58,20 +124,34 @@ public:
   static bool fullEffort(Effort e)           { return e >= FULL_EFFORT; }
 
   /**
-   * Construct a Theory.
+   * Set the output channel associated to this theory.
    */
-  Theory(context::Context* c) : d_assertions(c),  d_nextAssertion(c, 0){}
+  void setOutputChannel(OutputChannel& out) {
+    d_out = &out;
+  }
 
   /**
-   * Destructs a Theory.  This implementation does nothing, but we
-   * need a virtual destructor for safety in case subclasses have a
-   * destructor.
+   * Get the output channel associated to this theory.
    */
-  virtual ~Theory() {
+  OutputChannel& getOutputChannel() {
+    return *d_out;
+  }
+
+  /**
+   * Get the output channel associated to this theory [const].
+   */
+  const OutputChannel& getOutputChannel() const {
+    return *d_out;
   }
 
   /**
-   * Prepare for a Node.
+   * Pre-register a term.  Done one time for a Node, ever.
+   *
+   */
+  virtual void preRegisterTerm(TNode) = 0;
+
+  /**
+   * Register a term.
    *
    * When get() is called to get the next thing off the theory queue,
    * setup() is called on its subterms (in TheoryEngine).  Then setup()
@@ -81,55 +161,189 @@ public:
    * setup() MUST NOT MODIFY context-dependent objects that it hasn't
    * itself just created.
    */
-
-  /*virtual void setup(const Node& n) = 0;*/
-
-  virtual void registerTerm(TNode n) = 0;
+  virtual void registerTerm(TNode) = 0;
 
   /**
    * Assert a fact in the current context.
    */
-  void assertFact(const Node& n);
+  void assertFact(TNode n) {
+    d_facts.push(n);
+  }
 
   /**
    * Check the current assignment's consistency.
    */
-  virtual void check(OutputChannel& out,
-                     Effort level = FULL_EFFORT) = 0;
+  virtual void check(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(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,
-                       const Node& n,
-                       Effort level = FULL_EFFORT) = 0;
-private:
-  context::CDList<Node> d_assertions;
-  context::CDO<unsigned> d_nextAssertion;
+  virtual void explain(TNode n, Effort level = FULL_EFFORT) = 0;
+
+  //
+  // CODE INVARIANT CHECKING (used only with CVC4_ASSERTIONS)
+  //
 
-protected:
   /**
-   * Returns the next atom in the assertFact() queue.
-   * Guarentees that registerTerm is called on the theory specific subterms.
-   * @return the next atom in the assertFact() queue.
+   * Different states at which invariants are checked.
    */
-  Node get();
+  enum ReadyState {
+    ABOUT_TO_PUSH,
+    ABOUT_TO_POP
+  };/* enum ReadyState */
 
   /**
-   * Returns true if the assertFactQueue is empty
+   * Public invariant checker.  Assert that this theory is in a valid
+   * state for the (external) system state.  This implementation
+   * checks base invariants and then calls theoryReady().  This
+   * function may abort in the case of a failed assert, or return
+   * false (the caller should assert that the return value is true).
+   *
+   * @param s the state about which to check invariants
    */
-  bool done();
+  bool ready(ReadyState s) {
+    if(s == ABOUT_TO_PUSH) {
+      Assert(d_facts.empty(), "Theory base code invariant broken: "
+             "fact queue is nonempty on context push");
+    }
+
+    return theoryReady(s);
+  }
+
+protected:
+
+  /**
+   * Check any invariants at the ReadyState given.  Only called by
+   * Theory class, and then only with CVC4_ASSERTIONS enabled.  This
+   * function may abort in the case of a failed assert, or return
+   * false (the caller should assert that the return value is true).
+   *
+   * @param s the state about which to check invariants
+   */
+  virtual bool theoryReady(ReadyState s) {
+    return true;
+  }
 
 };/* class Theory */
 
+
+/**
+ * Base class for T-solver implementations.  Each individual
+ * implementation T of the Theory interface should inherit from
+ * TheoryImpl<T>.  This class specializes some things for a particular
+ * theory implementation.
+ *
+ * The problem with this is that Theory implementations cannot be
+ * further subclassed without designing all non-children in the type
+ * DAG to play the same trick as here (be template-polymorphic in their
+ * most-derived child), linearizing the inheritance hierarchy (viewing
+ * each instantiation separately).
+ */
+template <class T>
+class TheoryImpl : public Theory {
+
+protected:
+
+  /**
+   * Construct a Theory.
+   */
+  TheoryImpl(context::Context* ctxt, OutputChannel& out) :
+    Theory(ctxt, out) {
+    /* FIXME: assert here that a TheoryImpl<T> doesn't already exist
+     * for this NodeManager??  If it does, we're hosed because they'll
+     * share per-theory node attributes. */
+  }
+
+  /** Tag for the "registerTerm()-has-been-called" flag on Nodes */
+  struct Registered {};
+  /** The "registerTerm()-has-been-called" flag on Nodes */
+  typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr;
+
+  /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */
+  struct PreRegistered {};
+  /** The "preRegisterTerm()-has-been-called" flag on Nodes */
+  typedef CVC4::expr::Attribute<PreRegistered, bool> PreRegisteredAttr;
+
+  /**
+   * Returns the next atom in the assertFact() queue.  Guarantees that
+   * registerTerm() has been called on the theory specific subterms.
+   *
+   * @return the next atom in the assertFact() queue.
+   */
+  Node get();
+};/* class TheoryImpl<T> */
+
+template <class T>
+Node TheoryImpl<T>::get() {
+  Warning.printf("testing %s == %s\n", typeid(*this).name(), typeid(T).name());
+  /*Assert(typeid(*this) == typeid(T),
+         "Improper Theory inheritance chain detected.");*/
+
+  Assert( !d_facts.empty(),
+          "Theory::get() called with assertion queue empty!" );
+
+  Node fact = d_facts.front();
+  d_facts.pop();
+
+  if(! fact.getAttribute(RegisteredAttr())) {
+    std::vector<TNode> toReg;
+    toReg.push_back(fact);
+
+    /* Essentially this is doing a breadth-first numbering of
+     * non-registered subterms with children.  Any non-registered
+     * leaves are immediately registered. */
+    for(std::vector<TNode>::iterator workp = toReg.begin();
+        workp != toReg.end();
+        ++workp) {
+
+      TNode n = *workp;
+
+      for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
+        TNode c = *i;
+
+        if(! c.getAttribute(RegisteredAttr())) {
+          if(c.getNumChildren() == 0) {
+            c.setAttribute(RegisteredAttr(), true);
+            registerTerm(c);
+          } else {
+            toReg.push_back(c);
+          }
+        }
+      }
+    }
+
+    /* Now register the list of terms in reverse order.  Between this
+     * and the above registration of leaves, this should ensure that
+     * all subterms in the entire tree were registered in
+     * reverse-topological order. */
+    for(std::vector<TNode>::reverse_iterator i = toReg.rend();
+        i != toReg.rbegin();
+        ++i) {
+
+      TNode n = *i;
+
+      /* Note that a shared TNode in the DAG rooted at "fact" could
+       * appear twice on the list, so we have to avoid hitting it
+       * twice. */
+      // FIXME when ExprSets are online, use one of those to avoid
+      // duplicates in the above?
+      if(! n.getAttribute(RegisteredAttr())) {
+        n.setAttribute(RegisteredAttr(), true);
+        registerTerm(n);
+      }
+    }
+  }
+
+  return fact;
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 348d7e6df..7d630f667 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -18,6 +18,8 @@
 
 #include "expr/node.h"
 #include "theory/theory.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/theoryof_table.h"
 
 namespace CVC4 {
 
@@ -34,20 +36,67 @@ class SmtEngine;
  */
 class TheoryEngine {
 
+  /** Associated SMT engine */
   SmtEngine* d_smt;
 
+  /** A table of Kinds to pointers to Theory */
+  theory::TheoryOfTable theoryOfTable;
+
+  /**
+   * An output channel for Theory that passes messages
+   * back to a TheoryEngine.
+   */
+  class EngineOutputChannel : public theory::OutputChannel {
+    TheoryEngine* d_engine;
+  public:
+    void setEngine(TheoryEngine& engine) throw() {
+      d_engine = &engine;
+    }
+
+    void conflict(TNode, bool) throw(theory::Interrupted) {
+    }
+
+    void propagate(TNode, bool) throw(theory::Interrupted) {
+    }
+
+    void lemma(TNode, bool) throw(theory::Interrupted) {
+    }
+
+    void explanation(TNode, bool) throw(theory::Interrupted) {
+    }
+  };
+
+  EngineOutputChannel d_theoryOut;
+  theory::booleans::TheoryBool d_bool;
+  theory::uf::TheoryUF d_uf;
+  theory::arith::TheoryArith d_arith;
+
 public:
 
   /**
    * Construct a theory engine.
    */
-  TheoryEngine(SmtEngine* smt) : d_smt(smt) {
+  TheoryEngine(SmtEngine* smt, context::Context* ctxt) :
+    d_smt(smt),
+    d_theoryOut(),
+    d_bool(ctxt, d_theoryOut),
+    d_uf(ctxt, d_theoryOut),
+    d_arith(ctxt, d_theoryOut) {
+    d_theoryOut.setEngine(*this);
+    theoryOfTable.registerTheory(&d_bool);
+    theoryOfTable.registerTheory(&d_uf);
+    theoryOfTable.registerTheory(&d_arith);
   }
 
   /**
    * Get the theory associated to a given Node.
+   *
+   * @returns the theory, or NULL if the TNode is
+   * of built-in type.
    */
-  CVC4::theory::Theory* theoryOf(const Node& n);
+  theory::Theory* theoryOf(TNode n) {
+    return theoryOfTable[n];
+  }
 
 };/* class TheoryEngine */
 
diff --git a/src/theory/theoryof_table_epilogue.h b/src/theory/theoryof_table_epilogue.h
new file mode 100644
index 000000000..7483248ec
--- /dev/null
+++ b/src/theory/theoryof_table_epilogue.h
@@ -0,0 +1,21 @@
+/*********************                                                        */
+/** theoryof_table_epilogue.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** The theoryOf table.
+ **/
+
+};/* class TheoryOfTable */
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__THEORYOF_TABLE_H */
diff --git a/src/theory/theoryof_table_middle.h b/src/theory/theoryof_table_middle.h
new file mode 100644
index 000000000..17a945d01
--- /dev/null
+++ b/src/theory/theoryof_table_middle.h
@@ -0,0 +1,35 @@
+/*********************                                                        */
+/** theoryof_table_middle.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** The theoryOf table.
+ **/
+
+namespace CVC4 {
+namespace theory {
+
+class Theory;
+
+class TheoryOfTable {
+
+  Theory** d_table;
+
+public:
+
+  TheoryOfTable() :
+    d_table(new Theory*[::CVC4::kind::LAST_KIND]) {
+  }
+
+  Theory* operator[](TNode n) {
+    Assert(n.getKind() >= 0 && n.getKind() < ::CVC4::kind::LAST_KIND,
+           "illegal to inquire theoryOf(UNDEFINED_KIND or out-of-range)");
+    return d_table[n.getKind()];
+  }
diff --git a/src/theory/theoryof_table_prologue.h b/src/theory/theoryof_table_prologue.h
new file mode 100644
index 000000000..5f8c28723
--- /dev/null
+++ b/src/theory/theoryof_table_prologue.h
@@ -0,0 +1,21 @@
+/*********************                                                        */
+/** theoryof_table_prologue.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** The theoryOf table.
+ **/
+
+#ifndef __CVC4__THEORY__THEORYOF_TABLE_H
+#define __CVC4__THEORY__THEORYOF_TABLE_H
+
+#include "expr/kind.h"
+#include "util/Assert.h"
+
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index 537b8b124..156733c5b 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden
 noinst_LTLIBRARIES = libuf.la
 
 libuf_la_SOURCES = \
+	theory_def.h \
 	ecdata.h \
 	ecdata.cpp \
 	theory_uf.h \
diff --git a/src/theory/uf/theory_def.h b/src/theory/uf/theory_def.h
new file mode 100644
index 000000000..8e3f5e9f1
--- /dev/null
+++ b/src/theory/uf/theory_def.h
@@ -0,0 +1,7 @@
+namespace CVC4 {
+  namespace theory {
+    namespace uf {
+      class TheoryUF;
+    }
+  }
+}
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 1efe13b9b..47bda5bc4 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -19,9 +19,10 @@
 #include "expr/kind.h"
 
 using namespace CVC4;
-using namespace context;
-using namespace theory;
-using namespace uf;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
 
 
 
@@ -30,8 +31,8 @@ Node getOperator(Node x) { return Node::null(); }
 
 
 
-TheoryUF::TheoryUF(Context* c) :
-  Theory(c),
+TheoryUF::TheoryUF(Context* c, OutputChannel& out) :
+  TheoryImpl<TheoryUF>(c, out),
   d_pending(c),
   d_currentPendingIdx(c,0),
   d_disequality(c),
@@ -40,13 +41,16 @@ TheoryUF::TheoryUF(Context* c) :
 
 TheoryUF::~TheoryUF(){}
 
+void TheoryUF::preRegisterTerm(TNode n){
+}
+
 void TheoryUF::registerTerm(TNode n){
 
   d_registered.push_back(n);
 
   ECData* ecN;
 
-  if(n.hasAttribute(ECAttr(),&ecN)){
+  if(n.hasAttribute(ECAttr(), ecN)){
     /* registerTerm(n) is only called when a node has not been seen in the
      * current context.  ECAttr() is not a context-dependent attribute.
      * When n.hasAttribute(ECAttr(),...) is true on a registerTerm(n) call,
@@ -222,9 +226,9 @@ void TheoryUF::merge(){
   }
 }
 
-void TheoryUF::check(OutputChannel& out, Effort level){
+void TheoryUF::check(Effort level){
   while(!done()){
-    Node assertion = get();
+    Node assertion;// = get();
 
     switch(assertion.getKind()){
     case EQUAL:
@@ -252,7 +256,7 @@ void TheoryUF::check(OutputChannel& out, Effort level){
       TNode left  = (*diseqIter)[0];
       TNode right = (*diseqIter)[1];
       if(sameCongruenceClass(left, right)){
-        out.conflict(*diseqIter, true);
+        d_out->conflict(*diseqIter, true);
       }
     }
   }
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index b68a96e65..4bb18bd43 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -21,7 +21,6 @@
 #include "expr/attribute.h"
 
 #include "theory/theory.h"
-#include "theory/output_channel.h"
 
 #include "context/context.h"
 #include "theory/uf/ecdata.h"
@@ -30,9 +29,8 @@ namespace CVC4 {
 namespace theory {
 namespace uf {
 
+class TheoryUF : public TheoryImpl<TheoryUF> {
 
-
-class TheoryUF : public Theory {
 private:
 
 
@@ -72,7 +70,7 @@ private:
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-  TheoryUF(context::Context* c);
+  TheoryUF(context::Context* c, OutputChannel& out);
 
   /** Destructor for the TheoryUF object. */
   ~TheoryUF();
@@ -82,14 +80,13 @@ public:
   //has pending changes to the contracts
 
   void registerTerm(TNode n);
+  void preRegisterTerm(TNode n);
 
-  void check(OutputChannel& out, Effort level= FULL_EFFORT);
+  void check(Effort level);
 
-  void propagate(OutputChannel& out, Effort level= FULL_EFFORT){}
+  void propagate(Effort level) {}
 
-  void explain(OutputChannel& out,
-               const Node& n,
-               Effort level = FULL_EFFORT){}
+  void explain(TNode n, Effort level) {}
 
 private:
   /**