Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.

1 files changed, 94 insertions, 440 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e2c42bccd..25fe29c67 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -26,14 +26,8 @@
 
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
-#include "theory/builtin/theory_builtin.h"
-#include "theory/booleans/theory_bool.h"
-#include "theory/uf/theory_uf.h"
-#include "theory/uf/morgan/theory_uf_morgan.h"
-#include "theory/uf/tim/theory_uf_tim.h"
-#include "theory/arith/theory_arith.h"
-#include "theory/arrays/theory_arrays.h"
-#include "theory/bv/theory_bv.h"
+#include "theory/rewriter.h"
+#include "theory/theory_traits.h"
 
 using namespace std;
 
@@ -41,6 +35,12 @@ using namespace CVC4;
 using namespace CVC4::theory;
 
 namespace CVC4 {
+
+/** 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;
+
 namespace theory {
 
 struct PreRegisteredTag {};
@@ -129,150 +129,101 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) {
 
 TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) :
   d_propEngine(NULL),
+  d_context(ctxt),
   d_theoryOut(this, ctxt),
   d_theoryRegistration(opts.theoryRegistration),
   d_hasShutDown(false),
   d_incomplete(ctxt, false),
   d_statistics() {
 
-  d_sharedTermManager = new SharedTermManager(this, ctxt);
+  Rewriter::init();
 
-  d_builtin = new theory::builtin::TheoryBuiltin(0, ctxt, d_theoryOut);
-  d_bool = new theory::booleans::TheoryBool(1, ctxt, d_theoryOut);
-  switch(opts.uf_implementation) {
-  case Options::TIM:
-    d_uf = new theory::uf::tim::TheoryUFTim(2, ctxt, d_theoryOut);
-    break;
-  case Options::MORGAN:
-    d_uf = new theory::uf::morgan::TheoryUFMorgan(2, ctxt, d_theoryOut);
-    break;
-  default:
-    Unhandled(opts.uf_implementation);
-  }
-  d_arith = new theory::arith::TheoryArith(3, ctxt, d_theoryOut);
-  d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut);
-  d_bv = new theory::bv::TheoryBV(5, ctxt, d_theoryOut);
-
-  d_sharedTermManager->registerTheory(static_cast<theory::builtin::TheoryBuiltin*>(d_builtin));
-  d_sharedTermManager->registerTheory(static_cast<theory::booleans::TheoryBool*>(d_bool));
-  d_sharedTermManager->registerTheory(static_cast<theory::uf::TheoryUF*>(d_uf));
-  d_sharedTermManager->registerTheory(static_cast<theory::arith::TheoryArith*>(d_arith));
-  d_sharedTermManager->registerTheory(static_cast<theory::arrays::TheoryArrays*>(d_arrays));
-  d_sharedTermManager->registerTheory(static_cast<theory::bv::TheoryBV*>(d_bv));
-
-  d_theoryOfTable.registerTheory(static_cast<theory::builtin::TheoryBuiltin*>(d_builtin));
-  d_theoryOfTable.registerTheory(static_cast<theory::booleans::TheoryBool*>(d_bool));
-  d_theoryOfTable.registerTheory(static_cast<theory::uf::TheoryUF*>(d_uf));
-  d_theoryOfTable.registerTheory(static_cast<theory::arith::TheoryArith*>(d_arith));
-  d_theoryOfTable.registerTheory(static_cast<theory::arrays::TheoryArrays*>(d_arrays));
-  d_theoryOfTable.registerTheory(static_cast<theory::bv::TheoryBV*>(d_bv));
+  d_sharedTermManager = new SharedTermManager(this, ctxt);
 }
 
 TheoryEngine::~TheoryEngine() {
   Assert(d_hasShutDown);
 
-  delete d_bv;
-  delete d_arrays;
-  delete d_arith;
-  delete d_uf;
-  delete d_bool;
-  delete d_builtin;
-
-  delete d_sharedTermManager;
-}
-
-Theory* TheoryEngine::theoryOf(TypeNode t) {
-  // FIXME: we don't yet have a Type-to-Theory map.  When we do,
-  // look up the type of the var and return that Theory (?)
-
-  // The following JUST hacks around this lack of a table
-  Kind k = t.getKind();
-  if(k == kind::TYPE_CONSTANT) {
-    switch(TypeConstant tc = t.getConst<TypeConstant>()) {
-    case BOOLEAN_TYPE:
-      return d_theoryOfTable[kind::CONST_BOOLEAN];
-    case INTEGER_TYPE:
-      return d_theoryOfTable[kind::CONST_INTEGER];
-    case REAL_TYPE:
-      return d_theoryOfTable[kind::CONST_RATIONAL];
-    case KIND_TYPE:
-    default:
-      Unhandled(tc);
+  for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++ theoryId) {
+    if (d_theoryTable[theoryId]) {
+      delete d_theoryTable[theoryId];
     }
   }
 
-  return d_theoryOfTable[k];
+  delete d_sharedTermManager;
 }
 
+struct preprocess_stack_element {
+  TNode node;
+  bool children_added;
+  preprocess_stack_element(TNode node)
+  : node(node), children_added(false) {}
+};
 
-Theory* TheoryEngine::theoryOf(TNode n) {
-  Kind k = n.getKind();
+Node TheoryEngine::preprocess(TNode node) {
 
-  Assert(k >= 0 && k < kind::LAST_KIND);
+  // Remove ITEs and rewrite the node
+  Node preprocessed = Rewriter::rewrite(removeITEs(node));
 
-  if(n.getMetaKind() == kind::metakind::VARIABLE) {
-    return theoryOf(n.getType());
-  } else if(k == kind::EQUAL) {
-    // equality is special: use LHS
-    return theoryOf(n[0]);
-  } else {
-    // use our Kind-to-Theory mapping
-    return d_theoryOfTable[k];
+  // If we are pre-registered already we are done
+  if (preprocessed.getAttribute(PreRegistered())) {
+    return preprocessed;
   }
-}
-
-Node TheoryEngine::preprocess(TNode t) {
-  Node top = rewrite(t);
-  Debug("rewrite") << "rewrote: " << t << endl << "to     : " << top << endl;
-
-  list<TNode> toReg;
-  toReg.push_back(top);
-
-  /* Essentially this is doing a breadth-first numbering of
-   * non-registered subterms with children.  Any non-registered
-   * leaves are immediately registered. */
-  for(list<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(theory::PreRegistered())) {// c not yet registered
-        if(c.getNumChildren() == 0) {
-          c.setAttribute(theory::PreRegistered(), true);
-          theoryOf(c)->preRegisterTerm(c);
+  // Do a topological sort of the subexpressions and preregister them
+  vector<preprocess_stack_element> toVisit;
+  toVisit.push_back((TNode) preprocessed);
+  while (!toVisit.empty()) {
+    preprocess_stack_element& stackHead = toVisit.back();
+    // The current node we are processing
+    TNode current = stackHead.node;
+    // If we already added all the children its time to register or just pop from the stack
+    if (stackHead.children_added || current.getAttribute(PreRegistered())) {
+      if (!current.getAttribute(PreRegistered())) {
+        // Mark it as registered
+        current.setAttribute(PreRegistered(), true);
+        // Register this node
+        if (current.getKind() == kind::EQUAL) {
+          TheoryId theoryLHS = Theory::theoryOf(current[0]);
+          Debug("register") << "preregistering " << current << " with " << theoryLHS << std::endl;
+          d_theoryTable[theoryLHS]->preRegisterTerm(current);
+//          TheoryId theoryRHS = Theory::theoryOf(current[1]);
+//          if (theoryLHS != theoryRHS) {
+//            d_theoryTable[theoryRHS]->preRegisterTerm(current);
+//            Debug("register") << "preregistering " << current << " with " << theoryRHS << std::endl;
+//          }
+//          TheoryId typeTheory = Theory::theoryOf(current[0].getType());
+//          if (typeTheory != theoryLHS && typeTheory != theoryRHS) {
+//            d_theoryTable[typeTheory]->preRegisterTerm(current);
+//            Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl;
+//          }
         } else {
-          toReg.push_back(c);
+          TheoryId theory = Theory::theoryOf(current);
+          Debug("register") << "preregistering " << current << " with " << theory << std::endl;
+          d_theoryTable[theory]->preRegisterTerm(current);
+          TheoryId typeTheory = Theory::theoryOf(current.getType());
+          if (theory != typeTheory) {
+            Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl;
+            d_theoryTable[typeTheory]->preRegisterTerm(current);
+          }
+        }
+      }
+      // Done with this node, remove from the stack
+      toVisit.pop_back();
+    } else {
+      // Mark that we have added the children
+      stackHead.children_added = true;
+      // We need to add the children
+      for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
+        TNode childNode = *child_it;
+        if (!childNode.getAttribute(PreRegistered())) {
+          toVisit.push_back(childNode);
         }
       }
     }
   }
 
-  /* 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(list<TNode>::reverse_iterator i = toReg.rbegin();
-      i != toReg.rend();
-      ++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(theory::PreRegistered())) {
-      n.setAttribute(theory::PreRegistered(), true);
-      theoryOf(n)->preRegisterTerm(n);
-    }
-  }
-
-  return top;
+  return preprocessed;
 }
 
 /* Our goal is to tease out any ITE's sitting under a theory operator. */
@@ -289,9 +240,9 @@ Node TheoryEngine::removeITEs(TNode node) {
 
   if(node.getKind() == kind::ITE){
     Assert( node.getNumChildren() == 3 );
-    TypeNode nodeType = node[1].getType();
+    TypeNode nodeType = node.getType();
     if(!nodeType.isBoolean()){
-      Node skolem = nodeManager->mkVar(node.getType());
+      Node skolem = nodeManager->mkVar(nodeType);
       Node newAssertion =
         nodeManager->mkNode(kind::ITE,
                             node[0],
@@ -299,7 +250,7 @@ Node TheoryEngine::removeITEs(TNode node) {
                             nodeManager->mkNode(kind::EQUAL, skolem, node[2]));
       nodeManager->setAttribute(node, theory::IteRewriteAttr(), skolem);
 
-      Debug("ite") << "removeITEs([" << node.getId() << "," << node << "])"
+      Debug("ite") << "removeITEs([" << node.getId() << "," << node << "," << nodeType << "])"
                    << "->"
                    << "["<<newAssertion.getId() << "," << newAssertion << "]"
                    << endl;
@@ -330,277 +281,6 @@ Node TheoryEngine::removeITEs(TNode node) {
   }
 }
 
-namespace theory {
-namespace rewrite {
-
-/**
- * TheoryEngine::rewrite() keeps a stack of things that are being pre-
- * and post-rewritten.  Each element of the stack is a
- * RewriteStackElement.
- */
-struct RewriteStackElement {
-  /**
-   * The node at this rewrite level.  For example (AND (OR x y) z)
-   * will have, as it's rewriting x, the stack:
-   *    x
-   *    (OR x y)
-   *    (AND (OR x y) z)
-   */
-  Node d_node;
-
-  /**
-   * The theory associated to d_node.  Cached here to avoid having to
-   * look it up again.
-   */
-  Theory* d_theory;
-
-  /**
-   * Whether or not this was a top-level rewrite.  Note that at theory
-   * boundaries, topLevel is forced to true, so it's not the case that
-   * this is true only at the lowest stack level.
-   */
-  bool d_topLevel;
-
-  /**
-   * A saved index to the "next child" to pre- and post-rewrite.  In
-   * the case when (AND (OR x y) z) is being rewritten, the AND, OR,
-   * and x are pre-rewritten, then (assuming they don't change), x is
-   * post-rewritten, then y is pre- and post-rewritten, then the OR is
-   * post-rewritten, then z is pre-rewritten, then the AND is
-   * post-rewritten.  At each stack level, we need to remember the
-   * child index we're currently processing.
-   */
-  int d_nextChild;
-
-  /**
-   * A (re)builder for this node.  As this node's children are
-   * post-rewritten, in order, they append to this builder.  When this
-   * node is post-rewritten, it is reformed from d_builder since the
-   * children may have changed.  Note Nodes aren't rebuilt if they
-   * have metakinds CONSTANT (which is illegal) or VARIABLE (which
-   * would create a fresh variable, not what we want)---which is fine,
-   * since those types don't have children anyway.
-   */
-  NodeBuilder<> d_builder;
-
-  /**
-   * Construct a fresh stack element.
-   */
-  RewriteStackElement(Node n, Theory* thy, bool topLevel) :
-    d_node(n),
-    d_theory(thy),
-    d_topLevel(topLevel),
-    d_nextChild(0) {
-  }
-};
-
-}/* CVC4::theory::rewrite namespace */
-}/* CVC4::theory namespace */
-
-Node TheoryEngine::rewrite(TNode in, bool topLevel) {
-  using theory::rewrite::RewriteStackElement;
-
-  Node noItes = removeITEs(in);
-  Node out;
-
-  Debug("theory-rewrite") << "removeITEs of: " << in << endl
-                          << "           is: " << noItes << endl;
-
-  // descend top-down into the theory rewriters
-  vector<RewriteStackElement> stack;
-  stack.push_back(RewriteStackElement(noItes, theoryOf(noItes), topLevel));
-  Debug("theory-rewrite") << "TheoryEngine::rewrite() starting at" << endl
-                          << "  " << noItes << " " << theoryOf(noItes)
-                          << " " << (topLevel ? "TOP-LEVEL " : "")
-                          << "0" << endl;
-  // This whole thing is essentially recursive, but we avoid actually
-  // doing any recursion.
-  do {// do until the stack is empty..
-    RewriteStackElement& rse = stack.back();
-    bool done;
-
-    Debug("theory-rewrite") << "rewriter looking at level " << stack.size()
-                            << endl
-                            << "  " << rse.d_node << " " << rse.d_theory
-                            << "[" << *rse.d_theory << "]"
-                            << " " << (rse.d_topLevel ? "TOP-LEVEL " : "")
-                            << rse.d_nextChild << endl;
-
-    if(rse.d_nextChild == 0) {
-      Node original = rse.d_node;
-      bool wasTopLevel = rse.d_topLevel;
-      Node cached = getPreRewriteCache(original, wasTopLevel);
-      if(cached.isNull()) {
-        do {
-          Debug("theory-rewrite") << "doing pre-rewrite in " << *rse.d_theory
-                                  << " topLevel==" << rse.d_topLevel << endl;
-          RewriteResponse response =
-            rse.d_theory->preRewrite(rse.d_node, rse.d_topLevel);
-          rse.d_node = response.getNode();
-          Assert(!rse.d_node.isNull(), "node illegally rewritten to null");
-          Theory* thy2 = theoryOf(rse.d_node);
-          Assert(thy2 != NULL, "node illegally rewritten to null theory");
-          Debug("theory-rewrite") << "got back " << rse.d_node << " "
-                                  << thy2 << "[" << *thy2 << "]"
-                                  << (response.needsMoreRewriting() ?
-                                      (response.needsFullRewriting() ?
-                                       " FULL-REWRITING" : " MORE-REWRITING")
-                                      : " DONE")
-                                  << endl;
-          if(rse.d_theory != thy2) {
-            Debug("theory-rewrite") << "pre-rewritten from " << *rse.d_theory
-                                    << " into " << *thy2
-                                    << ", marking top-level and !done" << endl;
-            rse.d_theory = thy2;
-            done = false;
-            // FIXME how to handle the "top-levelness" of a node that's
-            // rewritten from theory T1 into T2, then back to T1 ?
-            rse.d_topLevel = true;
-          } else {
-            done = response.isDone();
-          }
-        } while(!done);
-        setPreRewriteCache(original, wasTopLevel, rse.d_node);
-      } else {// is in pre-rewrite cache
-        Debug("theory-rewrite") << "in pre-cache: " << cached << endl;
-        rse.d_node = cached;
-        Theory* thy2 = theoryOf(cached);
-        if(rse.d_theory != thy2) {
-          Debug("theory-rewrite") << "[cache-]pre-rewritten from "
-                                  << *rse.d_theory << " into " << *thy2
-                                  << ", marking top-level" << endl;
-          rse.d_theory = thy2;
-          rse.d_topLevel = true;
-        }
-      }
-    }
-
-    // children
-    Node original = rse.d_node;
-    bool wasTopLevel = rse.d_topLevel;
-    Node cached = getPostRewriteCache(original, wasTopLevel);
-
-    if(cached.isNull()) {
-      unsigned nch = rse.d_nextChild++;
-
-      if(nch == 0 &&
-         rse.d_node.getMetaKind() == kind::metakind::PARAMETERIZED) {
-        // this is an apply, so we have to push the operator
-        TNode op = rse.d_node.getOperator();
-        Debug("theory-rewrite") << "pushing operator " << op
-                                << " of " << rse.d_node << endl;
-        rse.d_builder << op;
-      }
-
-      if(nch < rse.d_node.getNumChildren()) {
-        Debug("theory-rewrite") << "pushing child " << nch
-                                << " of " << rse.d_node << endl;
-        Node c = rse.d_node[nch];
-        Theory* t = theoryOf(c);
-        stack.push_back(RewriteStackElement(c, t, t != rse.d_theory));
-        continue;// break out of this node, do its child
-      }
-
-      // incorporate the children's rewrites
-      if(rse.d_node.getMetaKind() != kind::metakind::VARIABLE &&
-         rse.d_node.getMetaKind() != kind::metakind::CONSTANT) {
-        Debug("theory-rewrite") << "builder here is " << &rse.d_builder
-                                << " and it gets " << rse.d_node.getKind()
-                                << endl;
-        rse.d_builder << rse.d_node.getKind();
-        rse.d_node = Node(rse.d_builder);
-      }
-
-      // post-rewriting
-      do {
-        Debug("theory-rewrite") << "doing post-rewrite of "
-                                << rse.d_node << endl
-                                << " in " << *rse.d_theory
-                                << " topLevel==" << rse.d_topLevel << endl;
-        RewriteResponse response =
-          rse.d_theory->postRewrite(rse.d_node, rse.d_topLevel);
-        rse.d_node = response.getNode();
-        Assert(!rse.d_node.isNull(), "node illegally rewritten to null");
-        Theory* thy2 = theoryOf(rse.d_node);
-        Assert(thy2 != NULL, "node illegally rewritten to null theory");
-        Debug("theory-rewrite") << "got back " << rse.d_node << " "
-                                << thy2 << "[" << *thy2 << "]"
-                                << (response.needsMoreRewriting() ?
-                                    (response.needsFullRewriting() ?
-                                     " FULL-REWRITING" : " MORE-REWRITING")
-                                    : " DONE")
-                                << endl;
-        if(rse.d_theory != thy2) {
-          Debug("theory-rewrite") << "post-rewritten from " << *rse.d_theory
-                                  << " into " << *thy2
-                                  << ", marking top-level and !done" << endl;
-          rse.d_theory = thy2;
-          done = false;
-          // FIXME how to handle the "top-levelness" of a node that's
-          // rewritten from theory T1 into T2, then back to T1 ?
-          rse.d_topLevel = true;
-        } else {
-          done = response.isDone();
-        }
-        if(response.needsFullRewriting()) {
-          Debug("theory-rewrite") << "full-rewrite requested for node "
-                                  << rse.d_node.getId() << ", invoking..."
-                                  << endl;
-          Node n = rewrite(rse.d_node, rse.d_topLevel);
-          Debug("theory-rewrite") << "full-rewrite finished for node "
-                                  << rse.d_node.getId() << ", got node "
-                                  << n << " output." << endl;
-          rse.d_node = n;
-          done = true;
-        }
-      } while(!done);
-
-      /* If extra-checking is on, do _another_ rewrite before putting
-       * in the cache to make sure they are the same.  This is
-       * especially necessary if a theory post-rewrites something into
-       * a term of another theory. */
-      if(Debug.isOn("extra-checking") &&
-         !Debug.isOn("$extra-checking:inside-rewrite")) {
-        ScopedDebug d("$extra-checking:inside-rewrite");
-        Node rewrittenAgain = rewrite(rse.d_node, rse.d_topLevel);
-        Assert(rewrittenAgain == rse.d_node,
-               "\nExtra-checking assumption failed, "
-               "node is not completely rewritten.\n\n"
-               "Original : %s\n"
-               "Rewritten: %s\n"
-               "Again    : %s\n",
-               original.toString().c_str(),
-               rse.d_node.toString().c_str(),
-               rewrittenAgain.toString().c_str());
-      }
-      setPostRewriteCache(original, wasTopLevel, rse.d_node);
-
-      out = rse.d_node;
-    } else {
-      Debug("theory-rewrite") << "in post-cache: " << cached << endl;
-      out = cached;
-      Theory* thy2 = theoryOf(cached);
-      if(rse.d_theory != thy2) {
-        Debug("theory-rewrite") << "[cache-]post-rewritten from "
-                                << *rse.d_theory << " into " << *thy2 << endl;
-        rse.d_theory = thy2;
-      }
-    }
-
-    stack.pop_back();
-    if(!stack.empty()) {
-      Debug("theory-rewrite") << "asserting " << out << " to previous builder "
-                              << &stack.back().d_builder << endl;
-      stack.back().d_builder << out;
-    }
-  } while(!stack.empty());
-
-  Debug("theory-rewrite") << "DONE with theory rewriter." << endl;
-  Debug("theory-rewrite") << "result is:" << endl << out << endl;
-
-  return out;
-}/* TheoryEngine::rewrite(TNode in) */
-
 
 Node TheoryEngine::getValue(TNode node) {
   kind::MetaKind metakind = node.getMetaKind();
@@ -617,36 +297,16 @@ Node TheoryEngine::getValue(TNode node) {
   return theoryOf(node)->getValue(node, this);
 }/* TheoryEngine::getValue(TNode node) */
 
-
 bool TheoryEngine::presolve() {
   d_theoryOut.d_conflictNode = Node::null();
   d_theoryOut.d_propagatedLiterals.clear();
   try {
-    /*
-    d_builtin->presolve();
-    if(!d_theoryOut.d_conflictNode.get().isNull()) {
-      return true;
-    }
-    d_bool->presolve();
-    if(!d_theoryOut.d_conflictNode.get().isNull()) {
-      return true;
-    }
-    */
-    d_uf->presolve();
-    if(!d_theoryOut.d_conflictNode.get().isNull()) {
-      return true;
-    }
-    d_arith->presolve();
-    /*
-    if(!d_theoryOut.d_conflictNode.get().isNull()) {
-      return true;
-    }
-    d_arrays->presolve();
-    if(!d_theoryOut.d_conflictNode.get().isNull()) {
-      return true;
-    }
-    d_bv->presolve();
-    */
+    for(unsigned i = 0; i < THEORY_LAST; ++ i) {
+        d_theoryTable[i]->presolve();
+        if(!d_theoryOut.d_conflictNode.get().isNull()) {
+          return true;
+	}
+     }
   } catch(const theory::Interrupted&) {
     Debug("theory") << "TheoryEngine::presolve() => interrupted" << endl;
   }
@@ -656,26 +316,20 @@ bool TheoryEngine::presolve() {
 
 
 void TheoryEngine::notifyRestart() {
-  /*
-  d_builtin->notifyRestart();
-  d_bool->notifyRestart();
-  */
-  d_uf->notifyRestart();
-  /*
-  d_arith->notifyRestart();
-  d_arrays->notifyRestart();
-  d_bv->notifyRestart();
-  */
+  for(unsigned i = 0; i < THEORY_LAST; ++ i) {
+    if (d_theoryTable[i]) {
+      d_theoryTable[i]->notifyRestart();
+    }
+  }
 }
 
 
 void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) {
-  d_builtin->staticLearning(in, learned);
-  d_bool->staticLearning(in, learned);
-  d_uf->staticLearning(in, learned);
-  d_arith->staticLearning(in, learned);
-  d_arrays->staticLearning(in, learned);
-  d_bv->staticLearning(in, learned);
+  for(unsigned i = 0; i < THEORY_LAST; ++ i) {
+    if (d_theoryTable[i]) {
+      d_theoryTable[i]->staticLearning(in, learned);
+    }
+  }
 }