Merge from nonclausal-simplification-v2 branch:

* Preprocessing-time, non-clausal, Boolean simplification round to
  support "quasi-non-linear rewrites" as discussed at last few meetings.

* --simplification=none is the default for now, but we'll probably
  change that to --simplification=incremental.  --simplification=batch
  is also a possibility.  See --simplification=help for details.

* RecursionBreaker<T> now uses a hash set for the seen trail.
* Fixes to TLS stuff to support that.
* Fixes to theory and SmtEngine documentation.
* Fixes to stream indentation.
* Other miscellaneous stuff.

19 files changed, 1007 insertions, 42 deletions

diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index eecf95875..d720d5136 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -23,6 +23,7 @@ libtheory_la_SOURCES = \
 	rewriter.h \
 	rewriter_attributes.h \
 	rewriter.cpp \
+	substitutions.h \
 	valuation.h \
 	valuation.cpp
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e724312fa..7c72b5a28 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -83,6 +83,7 @@ TheoryArith::Statistics::Statistics():
   d_statSlackVariables("theory::arith::SlackVariables", 0),
   d_statDisequalitySplits("theory::arith::DisequalitySplits", 0),
   d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0),
+  d_simplifyTimer("theory::arith::simplifyTimer"),
   d_staticLearningTimer("theory::arith::staticLearningTimer"),
   d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0),
   d_presolveTime("theory::arith::presolveTime"),
@@ -96,6 +97,7 @@ TheoryArith::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_statSlackVariables);
   StatisticsRegistry::registerStat(&d_statDisequalitySplits);
   StatisticsRegistry::registerStat(&d_statDisequalityConflicts);
+  StatisticsRegistry::registerStat(&d_simplifyTimer);
   StatisticsRegistry::registerStat(&d_staticLearningTimer);
 
   StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables);
@@ -114,6 +116,7 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_statSlackVariables);
   StatisticsRegistry::unregisterStat(&d_statDisequalitySplits);
   StatisticsRegistry::unregisterStat(&d_statDisequalityConflicts);
+  StatisticsRegistry::unregisterStat(&d_simplifyTimer);
   StatisticsRegistry::unregisterStat(&d_staticLearningTimer);
 
   StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables);
@@ -127,6 +130,12 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_restartTimer);
 }
 
+Node TheoryArith::simplify(TNode in, std::vector< std::pair<Node, Node> >& outSubstitutions) {
+  TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer);
+  Trace("simplify:arith") << "arith-simplifying: " << in << endl;
+  return d_valuation.rewrite(in);
+}
+
 void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
   TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer);
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 9580a6c71..1c8955d35 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -149,6 +149,7 @@ public:
 
   void presolve();
   void notifyRestart();
+  Node simplify(TNode in, std::vector< std::pair<Node, Node> >& outSubstitutions);
   void staticLearning(TNode in, NodeBuilder<>& learned);
 
   std::string identify() const { return std::string("TheoryArith"); }
@@ -234,6 +235,7 @@ private:
     IntStat d_statUserVariables, d_statSlackVariables;
     IntStat d_statDisequalitySplits;
     IntStat d_statDisequalityConflicts;
+    TimerStat d_simplifyTimer;
     TimerStat d_staticLearningTimer;
 
     IntStat d_permanentlyRemovedVariables;
diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am
index 0263ae017..524a39b69 100644
--- a/src/theory/booleans/Makefile.am
+++ b/src/theory/booleans/Makefile.am
@@ -10,6 +10,8 @@ libbooleans_la_SOURCES = \
 	theory_bool.cpp \
 	theory_bool_type_rules.h \
 	theory_bool_rewriter.h \
-	theory_bool_rewriter.cpp	
+	theory_bool_rewriter.cpp \
+	circuit_propagator.h \
+	circuit_propagator.cpp
 
 EXTRA_DIST = kinds
diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
new file mode 100644
index 000000000..e5055c164
--- /dev/null
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -0,0 +1,382 @@
+/*********************                                                        */
+/*! \file circuit_propagator.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
+ **
+ ** \brief A non-clausal circuit propagator for Boolean simplification
+ **
+ ** A non-clausal circuit propagator for Boolean simplification.
+ **/
+
+#include "theory/booleans/circuit_propagator.h"
+#include "util/utility.h"
+
+#include <vector>
+#include <algorithm>
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+void CircuitPropagator::propagateBackward(TNode in, bool polarity, vector<TNode>& changed) {
+  if(!isPropagatedBackward(in)) {
+    Debug("circuit-prop") << push << "propagateBackward(" << polarity << "): " << in << endl;
+    setPropagatedBackward(in);
+    // backward rules
+    switch(Kind k = in.getKind()) {
+    case kind::AND:
+      if(polarity) {
+        // AND = TRUE: forall children c, assign(c = TRUE)
+        for(TNode::iterator i = in.begin(), i_end = in.end(); i != i_end; ++i) {
+          Debug("circuit-prop") << "bAND1" << endl;
+          assign(*i, true, changed);
+        }
+      } else {
+        // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE)
+        TNode::iterator holdout = find_if_unique(in.begin(), in.end(), not1(IsAssignedTo(*this, true)));
+        if(holdout != in.end()) {
+          Debug("circuit-prop") << "bAND2" << endl;
+          assign(*holdout, false, changed);
+        }
+      }
+      break;
+    case kind::OR:
+      if(polarity) {
+        // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE)
+        TNode::iterator holdout = find_if_unique(in.begin(), in.end(), not1(IsAssignedTo(*this, false)));
+        if(holdout != in.end()) {
+          Debug("circuit-prop") << "bOR1" << endl;
+          assign(*holdout, true, changed);
+        }
+      } else {
+        // OR = FALSE: forall children c, assign(c = FALSE)
+        for(TNode::iterator i = in.begin(), i_end = in.end(); i != i_end; ++i) {
+          Debug("circuit-prop") << "bOR2" << endl;
+          assign(*i, false, changed);
+        }
+      }
+      break;
+    case kind::NOT:
+      // NOT = b: assign(c = !b)
+      Debug("circuit-prop") << "bNOT" << endl;
+      assign(in[0], !polarity, changed);
+      break;
+    case kind::ITE:
+      if(isAssignedTo(in[0], true)) {
+        // ITE c x y = v: if c is assigned and TRUE, assign(x = v)
+        Debug("circuit-prop") << "bITE1" << endl;
+        assign(in[1], polarity, changed);
+      } else if(isAssignedTo(in[0], false)) {
+        // ITE c x y = v: if c is assigned and FALSE, assign(y = v)
+        Debug("circuit-prop") << "bITE2" << endl;
+        assign(in[2], polarity, changed);
+      } else if(isAssigned(in[1]) && isAssigned(in[2])) {
+        if(assignment(in[1]) == polarity && assignment(in[2]) != polarity) {
+          // ITE c x y = v: if c is unassigned, x and y are assigned, x==v and y!=v, assign(c = TRUE)
+          Debug("circuit-prop") << "bITE3" << endl;
+          assign(in[0], true, changed);
+        } else if(assignment(in[1]) == !polarity && assignment(in[2]) == polarity) {
+          // ITE c x y = v: if c is unassigned, x and y are assigned, x!=v and y==v, assign(c = FALSE)
+          Debug("circuit-prop") << "bITE4" << endl;
+          assign(in[0], true, changed);
+        }
+      }
+      break;
+    case kind::IFF:
+      if(polarity) {
+        // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment [resp x = y.assignment])
+        if(isAssigned(in[0])) {
+          assign(in[1], assignment(in[0]), changed);
+          Debug("circuit-prop") << "bIFF1" << endl;
+        } else if(isAssigned(in[1])) {
+          Debug("circuit-prop") << "bIFF2" << endl;
+          assign(in[0], assignment(in[1]), changed);
+        }
+      } else {
+        // IFF x y = FALSE: if x [resp y] is assigned, assign(y = !x.assignment [resp x = !y.assignment])
+        if(isAssigned(in[0])) {
+          Debug("circuit-prop") << "bIFF3" << endl;
+          assign(in[1], !assignment(in[0]), changed);
+        } else if(isAssigned(in[1])) {
+          Debug("circuit-prop") << "bIFF4" << endl;
+          assign(in[0], !assignment(in[1]), changed);
+        }
+      }
+      break;
+    case kind::IMPLIES:
+      if(polarity) {
+        if(isAssignedTo(in[0], true)) {
+          // IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE)
+          Debug("circuit-prop") << "bIMPLIES1" << endl;
+          assign(in[1], true, changed);
+        }
+        if(isAssignedTo(in[1], false)) {
+          // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE)
+          Debug("circuit-prop") << "bIMPLIES2" << endl;
+          assign(in[0], false, changed);
+        }
+      } else {
+        // IMPLIES x y = FALSE: assign(x = TRUE) and assign(y = FALSE)
+        Debug("circuit-prop") << "bIMPLIES3" << endl;
+        assign(in[0], true, changed);
+        assign(in[1], false, changed);
+      }
+      break;
+    case kind::XOR:
+      if(polarity) {
+        if(isAssigned(in[0])) {
+          // XOR x y = TRUE, and x assigned, assign(y = !assignment(x))
+          Debug("circuit-prop") << "bXOR1" << endl;
+          assign(in[1], !assignment(in[0]), changed);
+        } else if(isAssigned(in[1])) {
+          // XOR x y = TRUE, and y assigned, assign(x = !assignment(y))
+          Debug("circuit-prop") << "bXOR2" << endl;
+          assign(in[0], !assignment(in[1]), changed);
+        }
+      } else {
+        if(isAssigned(in[0])) {
+          // XOR x y = FALSE, and x assigned, assign(y = assignment(x))
+          Debug("circuit-prop") << "bXOR3" << endl;
+          assign(in[1], assignment(in[0]), changed);
+        } else if(isAssigned(in[1])) {
+          // XOR x y = FALSE, and y assigned, assign(x = assignment(y))
+          Debug("circuit-prop") << "bXOR4" << endl;
+          assign(in[0], assignment(in[1]), changed);
+        }
+      }
+      break;
+    case kind::CONST_BOOLEAN:
+      // nothing to do
+      break;
+    default:
+      Unhandled(k);
+    }
+    Debug("circuit-prop") << pop;
+  }
+}
+
+
+void CircuitPropagator::propagateForward(TNode child, bool polarity, vector<TNode>& changed) {
+  if(!isPropagatedForward(child)) {
+    IndentedScope(Debug("circuit-prop"));
+    Debug("circuit-prop") << "propagateForward (" << polarity << "): " << child << endl;
+    std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction>::const_iterator iter = d_backEdges.find(child);
+    if(d_backEdges.find(child) == d_backEdges.end()) {
+      Debug("circuit-prop") << "no backedges, must be ROOT?: " << child << endl;
+      return;
+    }
+    const vector<TNode>& uses = (*iter).second;
+    setPropagatedForward(child);
+    for(vector<TNode>::const_iterator useIter = uses.begin(), useIter_end = uses.end(); useIter != useIter_end; ++useIter) {
+      TNode in = *useIter; // this is the outer node
+      Debug("circuit-prop") << "considering use: " << in << endl;
+      IndentedScope(Debug("circuit-prop"));
+      // forward rules
+      switch(Kind k = in.getKind()) {
+      case kind::AND:
+        if(polarity) {
+          TNode::iterator holdout;
+          holdout = find_if(in.begin(), in.end(), not1(IsAssignedTo(*this, true)));
+          if(holdout == in.end()) { // all children are assigned TRUE
+            // AND ...(x=TRUE)...: if all children now assigned to TRUE, assign(AND = TRUE)
+            Debug("circuit-prop") << "fAND1" << endl;
+            assign(in, true, changed);
+          } else if(isAssignedTo(in, false)) {// the AND is FALSE
+            // is the holdout unique ?
+            TNode::iterator other = find_if(holdout, in.end(), not1(IsAssignedTo(*this, true)));
+            if(other == in.end()) { // the holdout is unique
+              // AND ...(x=TRUE)...: if all children BUT ONE now assigned to TRUE, and AND == FALSE, assign(last_holdout = FALSE)
+              Debug("circuit-prop") << "fAND2" << endl;
+              assign(*holdout, false, changed);
+            }
+          }
+        } else {
+          // AND ...(x=FALSE)...: assign(AND = FALSE)
+          Debug("circuit-prop") << "fAND3" << endl;
+          assign(in, false, changed);
+        }
+        break;
+      case kind::OR:
+        if(polarity) {
+          // OR ...(x=TRUE)...: assign(OR = TRUE)
+          Debug("circuit-prop") << "fOR1" << endl;
+          assign(in, true, changed);
+        } else {
+          TNode::iterator holdout;
+          holdout = find_if(in.begin(), in.end(), not1(IsAssignedTo(*this, false)));
+          if(holdout == in.end()) { // all children are assigned FALSE
+            // OR ...(x=FALSE)...: if all children now assigned to FALSE, assign(OR = FALSE)
+            Debug("circuit-prop") << "fOR2" << endl;
+            assign(in, false, changed);
+          } else if(isAssignedTo(in, true)) {// the OR is TRUE
+            // is the holdout unique ?
+            TNode::iterator other = find_if(holdout, in.end(), not1(IsAssignedTo(*this, false)));
+            if(other == in.end()) { // the holdout is unique
+              // OR ...(x=FALSE)...: if all children BUT ONE now assigned to FALSE, and OR == TRUE, assign(last_holdout = TRUE)
+              Debug("circuit-prop") << "fOR3" << endl;
+              assign(*holdout, true, changed);
+            }
+          }
+        }
+        break;
+
+      case kind::NOT:
+        // NOT (x=b): assign(NOT = !b)
+        Debug("circuit-prop") << "fNOT" << endl;
+        assign(in, !polarity, changed);
+        break;
+      case kind::ITE:
+        if(child == in[0]) {
+          if(polarity) {
+            if(isAssigned(in[1])) {
+              // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment)
+              Debug("circuit-prop") << "fITE1" << endl;
+              assign(in, assignment(in[1]), changed);
+            }
+          } else {
+            if(isAssigned(in[2])) {
+              // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment)
+              Debug("circuit-prop") << "fITE2" << endl;
+              assign(in, assignment(in[2]), changed);
+            }
+          }
+        } else if(child == in[1]) {
+          if(isAssignedTo(in[0], true)) {
+            // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v)
+            Debug("circuit-prop") << "fITE3" << endl;
+            assign(in, assignment(in[1]), changed);
+          }
+        } else {
+          Assert(child == in[2]);
+          if(isAssignedTo(in[0], false)) {
+            // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v)
+            Debug("circuit-prop") << "fITE4" << endl;
+            assign(in, assignment(in[2]), changed);
+          }
+        }
+        break;
+      case kind::IFF:
+        if(child == in[0]) {
+          if(isAssigned(in[1])) {
+            // IFF (x=b) y: if y is assigned, assign(IFF = (x.assignment <=> y.assignment))
+            Debug("circuit-prop") << "fIFF1" << endl;
+            assign(in, assignment(in[0]) == assignment(in[1]), changed);
+          } else if(isAssigned(in)) {
+            // IFF (x=b) y: if IFF is assigned, assign(y = (b <=> IFF.assignment))
+            Debug("circuit-prop") << "fIFF2" << endl;
+            assign(in[1], polarity == assignment(in), changed);
+          }
+        } else {
+          Assert(child == in[1]);
+          if(isAssigned(in[0])) {
+            // IFF x (y=b): if x is assigned, assign(IFF = (x.assignment <=> y.assignment))
+            Debug("circuit-prop") << "fIFF3" << endl;
+            assign(in, assignment(in[0]) == assignment(in[1]), changed);
+          } else if(isAssigned(in)) {
+            // IFF x (y=b): if IFF is assigned, assign(x = (b <=> IFF.assignment))
+            Debug("circuit-prop") << "fIFF4" << endl;
+            assign(in[0], polarity == assignment(in), changed);
+          }
+        }
+        break;
+      case kind::IMPLIES:
+        if(isAssigned(in[0]) && isAssigned(in[1])) {
+          // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2))
+          assign(in, !assignment(in[0]) || assignment(in[1]), changed);
+          Debug("circuit-prop") << "fIMPLIES1" << endl;
+        } else {
+          if(child == in[0] && assignment(in[0]) && isAssignedTo(in, true)) {
+            // IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE)
+            Debug("circuit-prop") << "fIMPLIES2" << endl;
+            assign(in[1], true, changed);
+          }
+          if(child == in[1] && !assignment(in[1]) && isAssignedTo(in, true)) {
+            // IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE)
+            Debug("circuit-prop") << "fIMPLIES3" << endl;
+            assign(in[0], false, changed);
+          }
+          // Note that IMPLIES == FALSE doesn't need any cases here
+          // because if that assignment has been done, we've already
+          // propagated all the children (in back-propagation).
+        }
+        break;
+      case kind::XOR:
+        if(isAssigned(in)) {
+          if(child == in[0]) {
+            // XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR)
+            Debug("circuit-prop") << "fXOR1" << endl;
+            assign(in[1], polarity ^ assignment(in), changed);
+          } else {
+            Assert(child == in[1]);
+            // XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR))
+            Debug("circuit-prop") << "fXOR2" << endl;
+            assign(in[0], polarity ^ assignment(in), changed);
+          }
+        }
+        if( (child == in[0] && isAssigned(in[1])) ||
+            (child == in[1] && isAssigned(in[0])) ) {
+          // XOR (x=v) y [with y assigned], assign(XOR = (v ^ assignment(y))
+          // XOR x (y=v) [with x assigned], assign(XOR = (assignment(x) ^ v)
+          Debug("circuit-prop") << "fXOR3" << endl;
+          assign(in, assignment(in[0]) ^ assignment(in[1]), changed);
+        }
+        break;
+      case kind::CONST_BOOLEAN:
+        InternalError("Forward-propagating a constant Boolean value makes no sense");
+      default:
+        Unhandled(k);
+      }
+    }
+  }
+}
+
+
+bool CircuitPropagator::propagate(TNode in, bool polarity, vector<Node>& newFacts) {
+  try {
+    vector<TNode> changed;
+
+    Assert(kindToTheoryId(in.getKind()) == THEORY_BOOL);
+
+    Debug("circuit-prop") << "B: " << (polarity ? "" : "~") << in << endl;
+    propagateBackward(in, polarity, changed);
+    Debug("circuit-prop") << "F: " << (polarity ? "" : "~") << in << endl;
+    propagateForward(in, polarity, changed);
+
+    while(!changed.empty()) {
+      vector<TNode> worklist;
+      worklist.swap(changed);
+
+      for(vector<TNode>::iterator i = worklist.begin(), i_end = worklist.end(); i != i_end; ++i) {
+        if(kindToTheoryId((*i).getKind()) != THEORY_BOOL) {
+          if(assignment(*i)) {
+            newFacts.push_back(*i);
+          } else {
+            newFacts.push_back((*i).notNode());
+          }
+        } else {
+          Debug("circuit-prop") << "B: " << (isAssignedTo(*i, true) ? "" : "~") << *i << endl;
+          propagateBackward(*i, assignment(*i), changed);
+          Debug("circuit-prop") << "F: " << (isAssignedTo(*i, true) ? "" : "~") << *i << endl;
+          propagateForward(*i, assignment(*i), changed);
+        }
+      }
+    }
+  } catch(ConflictException& ce) {
+    return true;
+  }
+  return false;
+}
+
+}/* CVC4::theory::booleans namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
new file mode 100644
index 000000000..f9efc20af
--- /dev/null
+++ b/src/theory/booleans/circuit_propagator.h
@@ -0,0 +1,206 @@
+/*********************                                                        */
+/*! \file circuit_propagator.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
+ **
+ ** \brief A non-clausal circuit propagator for Boolean simplification
+ **
+ ** A non-clausal circuit propagator for Boolean simplification.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
+#define __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
+
+#include <vector>
+#include <functional>
+
+#include "theory/theory.h"
+#include "context/context.h"
+#include "util/hash.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+/**
+ * The main purpose of the CircuitPropagator class is to maintain the
+ * state of the circuit for subsequent calls to propagate(), so that
+ * the same fact is not output twice, so that the same edge in the
+ * circuit isn't propagated twice, etc.
+ */
+class CircuitPropagator {
+  const std::vector<TNode>& d_atoms;
+  const std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction>& d_backEdges;
+
+  class ConflictException : Exception {
+  public:
+    ConflictException() : Exception("A conflict was found in the CircuitPropagator") {
+    }
+  };/* class ConflictException */
+
+  enum {
+    ASSIGNMENT_MASK = 1,
+    IS_ASSIGNED_MASK = 2,
+    IS_PROPAGATED_FORWARD_MASK = 4,
+    IS_PROPAGATED_BACKWARD_MASK = 8
+  };/* enum */
+
+  /**
+   * For each Node we care about, we have a 4-bit state:
+   *   Bit 0 (ASSIGNMENT_MASK) is set to indicate the current assignment
+   *   Bit 1 (IS_ASSIGNED_MASK) is set if a value is assigned
+   *   Bit 2 (IS_PROPAGATED_FORWARD) is set to indicate it's been propagated forward
+   *   Bit 2 (IS_PROPAGATED_BACKWARD) is set to indicate it's been propagated backward
+   */
+  std::hash_map<TNode, unsigned, TNodeHashFunction> d_state;
+
+  /** Assign Node in circuit with the value and add it to the changed vector; note conflicts. */
+  void assign(TNode n, bool b, std::vector<TNode>& changed) {
+    if(n.getMetaKind() == kind::metakind::CONSTANT) {
+      bool c = n.getConst<bool>();
+      if(c != b) {
+        Debug("circuit-prop") << "while assigning(" << b << "): " << n
+                              << ", constant conflict" << std::endl;
+        throw ConflictException();
+      } else {
+        Debug("circuit-prop") << "assigning(" << b << "): " << n
+                              << ", nothing to do" << std::endl;
+      }
+      return;
+    }
+    unsigned& state = d_state[n];
+    if((state & IS_ASSIGNED_MASK) != 0) {// if assigned already
+      if(((state & ASSIGNMENT_MASK) != 0) != b) {// conflict
+        Debug("circuit-prop") << "while assigning(" << b << "): " << n
+                              << ", got conflicting assignment(" << assignment(n) << "): "
+                              << n << std::endl;
+        throw ConflictException();
+      } else {
+        Debug("circuit-prop") << "already assigned(" << b << "): " << n << std::endl;
+      }
+    } else {// if unassigned
+      Debug("circuit-prop") << "assigning(" << b << "): " << n << std::endl;
+      state |= IS_ASSIGNED_MASK | (b ? ASSIGNMENT_MASK : 0);
+      changed.push_back(n);
+    }
+  }
+  /** True iff Node is assigned in circuit (either true or false). */
+  bool isAssigned(TNode n) {
+    return (d_state[n] & IS_ASSIGNED_MASK) != 0;
+  }
+  /** True iff Node is assigned in circuit (either true or false). */
+  bool isAssigned(TNode n) const {
+    std::hash_map<TNode, unsigned, TNodeHashFunction>::const_iterator i = d_state.find(n);
+    return i != d_state.end() && ((*i).second & IS_ASSIGNED_MASK) != 0;
+  }
+  /** True iff Node is assigned in circuit with the value given. */
+  bool isAssignedTo(TNode n, bool b) {
+    unsigned state = d_state[n];
+    return (state & IS_ASSIGNED_MASK) &&
+      (state & ASSIGNMENT_MASK) == (b ? ASSIGNMENT_MASK : 0);
+  }
+  /** True iff Node is assigned in circuit (either true or false). */
+  bool isAssignedTo(TNode n, bool b) const {
+    std::hash_map<TNode, unsigned, TNodeHashFunction>::const_iterator i = d_state.find(n);
+    return i != d_state.end() &&
+      ((*i).second & IS_ASSIGNED_MASK) &&
+      ((*i).second & ASSIGNMENT_MASK) == (b ? ASSIGNMENT_MASK : 0);
+  }
+  /** Get Node assignment in circuit.  Assert-fails if Node is unassigned. */
+  bool assignment(TNode n) {
+    unsigned state = d_state[n];
+    Assert((state & IS_ASSIGNED_MASK) != 0);
+    return (state & ASSIGNMENT_MASK) != 0;
+  }
+  /** Has this node already been propagated forward? */
+  bool isPropagatedForward(TNode n) {
+    return (d_state[n] & IS_PROPAGATED_FORWARD_MASK) != 0;
+  }
+  /** Has this node already been propagated backward? */
+  bool isPropagatedBackward(TNode n) {
+    return (d_state[n] & IS_PROPAGATED_BACKWARD_MASK) != 0;
+  }
+  /** Mark this node as already having been propagated forward. */
+  void setPropagatedForward(TNode n) {
+    d_state[n] |= IS_PROPAGATED_FORWARD_MASK;
+  }
+  /** Mark this node as already having been propagated backward. */
+  void setPropagatedBackward(TNode n) {
+    d_state[n] |= IS_PROPAGATED_BACKWARD_MASK;
+  }
+
+  /** Predicate for use in STL functions. */
+  class IsAssigned : public std::unary_function<TNode, bool> {
+    CircuitPropagator& d_circuit;
+  public:
+    IsAssigned(CircuitPropagator& circuit) :
+      d_circuit(circuit) {
+    }
+
+    bool operator()(TNode in) const {
+      return d_circuit.isAssigned(in);
+    }
+  };/* class IsAssigned */
+
+  /** Predicate for use in STL functions. */
+  class IsAssignedTo : public std::unary_function<TNode, bool> {
+    CircuitPropagator& d_circuit;
+    bool d_value;
+  public:
+    IsAssignedTo(CircuitPropagator& circuit, bool value) :
+      d_circuit(circuit),
+      d_value(value) {
+    }
+
+    bool operator()(TNode in) const {
+      return d_circuit.isAssignedTo(in, d_value);
+    }
+  };/* class IsAssignedTo */
+
+  /**
+   * Propagate new information (in = polarity) forward in circuit to
+   * the parents of "in".
+   */
+  void propagateForward(TNode in, bool polarity, std::vector<TNode>& newFacts);
+  /**
+   * Propagate new information (in = polarity) backward in circuit to
+   * the children of "in".
+   */
+  void propagateBackward(TNode in, bool polarity, std::vector<TNode>& newFacts);
+
+public:
+  /**
+   * Construct a new CircuitPropagator with the given atoms and backEdges.
+   */
+  CircuitPropagator(const std::vector<TNode>& atoms, const std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction>& backEdges)
+    : d_atoms(atoms),
+      d_backEdges(backEdges) {
+  }
+
+  /**
+   * Propagate new information (in == polarity) through the circuit
+   * propagator.  New information discovered by the propagator are put
+   * in the (output-only) newFacts vector.
+   *
+   * @return true iff conflict found
+   */
+  bool propagate(TNode in, bool polarity, std::vector<Node>& newFacts) CVC4_WARN_UNUSED_RESULT;
+
+};/* class CircuitPropagator */
+
+}/* CVC4::theory::booleans namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 878b18478..b06972a2e 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -5,7 +5,7 @@
  ** 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)
+ ** Copyright (c) 2009, 2010, 2011  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
@@ -18,7 +18,15 @@
 
 #include "theory/theory.h"
 #include "theory/booleans/theory_bool.h"
+#include "theory/booleans/circuit_propagator.h"
 #include "theory/valuation.h"
+#include "util/boolean_simplification.h"
+
+#include <vector>
+#include <stack>
+#include "util/hash.h"
+
+using namespace std;
 
 namespace CVC4 {
 namespace theory {
@@ -89,6 +97,137 @@ Node TheoryBool::getValue(TNode n) {
   }
 }
 
+static void
+findAtoms(TNode in, vector<TNode>& atoms,
+          hash_map<TNode, vector<TNode>, TNodeHashFunction>& backEdges) {
+  Kind k = in.getKind();
+  Assert(kindToTheoryId(k) == THEORY_BOOL);
+
+  stack< pair<TNode, TNode::iterator> > trail;
+  hash_set<TNode, TNodeHashFunction> seen;
+  trail.push(make_pair(in, in.begin()));
+
+  while(!trail.empty()) {
+    pair<TNode, TNode::iterator>& pr = trail.top();
+    Debug("simplify") << "looking at: " << pr.first << endl;
+    if(pr.second == pr.first.end()) {
+      trail.pop();
+    } else {
+      if(pr.second == pr.first.begin()) {
+        Debug("simplify") << "first visit: " << pr.first << endl;
+        // first time we've visited this node?
+        if(seen.find(pr.first) == seen.end()) {
+          Debug("simplify") << "+ haven't seen it yet." << endl;
+          seen.insert(pr.first);
+        } else {
+          Debug("simplify") << "+ saw it before." << endl;
+          trail.pop();
+          continue;
+        }
+      }
+      TNode n = *pr.second++;
+      if(seen.find(n) == seen.end()) {
+        Debug("simplify") << "back edge " << n << " to " << pr.first << endl;
+        backEdges[n].push_back(pr.first);
+        Kind nk = n.getKind();
+        if(kindToTheoryId(nk) == THEORY_BOOL) {
+          trail.push(make_pair(n, n.begin()));
+        } else {
+          Debug("simplify") << "atom: " << n << endl;
+          atoms.push_back(n);
+        }
+      }
+    }
+  }
+}
+
+Node TheoryBool::simplify(TNode in, Substitutions& outSubstitutions) {
+  const unsigned prev = outSubstitutions.size();
+
+  if(kindToTheoryId(in.getKind()) != THEORY_BOOL) {
+    Assert(in.getMetaKind() == kind::metakind::VARIABLE &&
+           in.getType().isBoolean());
+    return in;
+  }
+
+  // form back edges and atoms
+  vector<TNode> atoms;
+  hash_map<TNode, vector<TNode>, TNodeHashFunction> backEdges;
+  Debug("simplify") << "finding atoms..." << endl << push;
+  findAtoms(in, atoms, backEdges);
+  Debug("simplify") << pop << "done finding atoms..." << endl;
+
+  hash_map<TNode, Node, TNodeHashFunction> simplified;
+
+  vector<Node> newFacts;
+  CircuitPropagator circuit(atoms, backEdges);
+  Debug("simplify") << "propagate..." << endl;
+  if(circuit.propagate(in, true, newFacts)) {
+    Notice() << "Found a conflict in nonclausal Boolean reasoning" << endl;
+    return NodeManager::currentNM()->mkConst(false);
+  }
+  Debug("simplify") << "done w/ propagate..." << endl;
+
+  for(vector<Node>::iterator i = newFacts.begin(), i_end = newFacts.end(); i != i_end; ++i) {
+    TNode a = *i;
+    if(a.getKind() == kind::NOT) {
+      if(a[0].getMetaKind() == kind::metakind::VARIABLE ) {
+        Debug("simplify") << "found bool unit ~" << a[0] << "..." << endl;
+        outSubstitutions.push_back(make_pair(a[0], NodeManager::currentNM()->mkConst(false)));
+      } else if(kindToTheoryId(a[0].getKind()) != THEORY_BOOL) {
+        Debug("simplify") << "simplifying: " << a << endl;
+        simplified[a] = d_valuation.simplify(a, outSubstitutions);
+        Debug("simplify") << "done simplifying, got: " << simplified[a] << endl;
+      }
+    } else {
+      if(a.getMetaKind() == kind::metakind::VARIABLE) {
+        Debug("simplify") << "found bool unit " << a << "..." << endl;
+        outSubstitutions.push_back(make_pair(a, NodeManager::currentNM()->mkConst(true)));
+      } else if(kindToTheoryId(a.getKind()) != THEORY_BOOL) {
+        Debug("simplify") << "simplifying: " << a << endl;
+        simplified[a] = d_valuation.simplify(a, outSubstitutions);
+        Debug("simplify") << "done simplifying, got: " << simplified[a] << endl;
+      }
+    }
+  }
+
+  Debug("simplify") << "substituting in root..." << endl;
+  Node n = in.substitute(outSubstitutions.begin(), outSubstitutions.end());
+  Debug("simplify") << "got: " << n << endl;
+  if(Debug.isOn("simplify")) {
+    Debug("simplify") << "new substitutions:" << endl;
+    copy(outSubstitutions.begin() + prev, outSubstitutions.end(),
+         ostream_iterator< pair<TNode, TNode> >(Debug("simplify"), "\n"));
+    Debug("simplify") << "done." << endl;
+  }
+  if(outSubstitutions.size() > prev) {
+    NodeBuilder<> b(kind::AND);
+    b << n;
+    for(Substitutions::iterator i = outSubstitutions.begin() + prev,
+          i_end = outSubstitutions.end();
+        i != i_end;
+        ++i) {
+      if((*i).first.getType().isBoolean()) {
+        if((*i).second.getMetaKind() == kind::metakind::CONSTANT) {
+          if((*i).second.getConst<bool>()) {
+            b << (*i).first;
+          } else {
+            b << BooleanSimplification::negate((*i).first);
+          }
+        } else {
+          b << (*i).first.iffNode((*i).second);
+        }
+      } else {
+        b << (*i).first.eqNode((*i).second);
+      }
+    }
+    n = b;
+  }
+  Debug("simplify") << "final boolean simplification returned: " << n << endl;
+  return n;
+}
+
+
 }/* CVC4::theory::booleans namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index fd6d20e03..40bbd3308 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -5,13 +5,13 @@
  ** Major contributors: taking
  ** Minor contributors (to current version): barrett
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
  **
- ** \brief The theory of booleans.
+ ** \brief The theory of booleans
  **
  ** The theory of booleans.
  **/
@@ -36,8 +36,10 @@ public:
 
   Node getValue(TNode n);
 
+  Node simplify(TNode in, Substitutions& outSubstitutions);
+
   std::string identify() const { return std::string("TheoryBool"); }
-};
+};/* class TheoryBool */
 
 }/* CVC4::theory::booleans namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 1c779bd79..ddfd2ab59 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -26,6 +26,47 @@ namespace CVC4 {
 namespace theory {
 namespace builtin {
 
+Node TheoryBuiltin::simplify(TNode in, Substitutions& outSubstitutions) {
+  if(in.getKind() == kind::EQUAL) {
+    Node lhs = d_valuation.simplify(in[0], outSubstitutions);
+    Node rhs = d_valuation.simplify(in[1], outSubstitutions);
+    Node n = lhs.eqNode(rhs);
+    if( n[0].getMetaKind() == kind::metakind::VARIABLE &&
+        n[1].getMetaKind() == kind::metakind::CONSTANT ) {
+      Debug("simplify:builtin") << "found new substitution! "
+                                << n[0] << " => " << n[1] << endl;
+      outSubstitutions.push_back(make_pair(n[0], n[1]));
+      // with our substitutions we've subsumed the equality
+      return NodeManager::currentNM()->mkConst(true);
+    } else if( n[1].getMetaKind() == kind::metakind::VARIABLE &&
+               n[0].getMetaKind() == kind::metakind::CONSTANT ) {
+      Debug("simplify:builtin") << "found new substitution! "
+                                << n[1] << " => " << n[0] << endl;
+      outSubstitutions.push_back(make_pair(n[1], n[0]));
+      // with our substitutions we've subsumed the equality
+      return NodeManager::currentNM()->mkConst(true);
+    }
+  } else if(in.getKind() == kind::NOT && in[0].getKind() == kind::DISTINCT) {
+    TNode::iterator found = in[0].end();
+    for(TNode::iterator i = in[0].begin(), i_end = in[0].end(); i != i_end; ++i) {
+      if((*i).getMetaKind() == kind::metakind::CONSTANT) {
+        found = i;
+        break;
+      }
+    }
+    if(found != in[0].end()) {
+      for(TNode::iterator i = in[0].begin(), i_end = in[0].end(); i != i_end; ++i) {
+        if(i != found) {
+          outSubstitutions.push_back(make_pair(*i, *found));
+        }
+      }
+      // with our substitutions we've subsumed the (NOT (DISTINCT...))
+      return NodeManager::currentNM()->mkConst(true);
+    }
+  }
+  return in;
+}
+
 Node TheoryBuiltin::getValue(TNode n) {
   switch(n.getKind()) {
 
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 4e62401ff..a97773dce 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -31,6 +31,7 @@ class TheoryBuiltin : public Theory {
 public:
   TheoryBuiltin(context::Context* c, OutputChannel& out, Valuation valuation) :
     Theory(THEORY_BUILTIN, c, out, valuation) {}
+  Node simplify(TNode in, Substitutions& outSubstitutions);
   Node getValue(TNode n);
   std::string identify() const { return std::string("TheoryBuiltin"); }
 };/* class TheoryBuiltin */
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 2056c6306..45c108b72 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -131,7 +131,7 @@ struct TheoryTraits<${theory_id}> {
     static const bool hasPropagate = ${theory_has_propagate};
     static const bool hasStaticLearning = ${theory_has_staticLearning};
     static const bool hasRegisterTerm = ${theory_has_registerTerm};
-    static const bool hasNotifyRestart = ${theory_has_staticLearning};
+    static const bool hasNotifyRestart = ${theory_has_notifyRestart};
     static const bool hasPresolve = ${theory_has_presolve};
 };
 "
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index 403ccf755..884d0af72 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -1,9 +1,20 @@
-/*
- * rewriter.h
- *
- *  Created on: Dec 13, 2010
- *      Author: dejan
- */
+/*********************                                                        */
+/*! \file rewriter.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
+ **
+ ** \brief The Rewriter class
+ **
+ ** The Rewriter class.
+ **/
 
 #pragma once
 
@@ -13,11 +24,15 @@
 namespace CVC4 {
 namespace theory {
 
+/**
+ * Theory rewriters signal whether more rewriting is needed (or not)
+ * by using a member of this enumeration.  See RewriteResponse, below.
+ */
 enum RewriteStatus {
   REWRITE_DONE,
   REWRITE_AGAIN,
   REWRITE_AGAIN_FULL
-};
+};/* enum RewriteStatus */
 
 /**
  * Instances of this class serve as response codes from
@@ -29,9 +44,13 @@ enum RewriteStatus {
 struct RewriteResponse {
   const RewriteStatus status;
   const Node node;
-  RewriteResponse(RewriteStatus status, Node node) : status(status), node(node) {}
-};
+  RewriteResponse(RewriteStatus status, Node node) :
+    status(status), node(node) {}
+};/* struct RewriteResponse */
 
+/**
+ * The main rewriter class.  All functionality is static.
+ */
 class Rewriter {
 
   /** Returns the appropriate cache for a node */
@@ -41,21 +60,28 @@ class Rewriter {
   static Node getPostRewriteCache(theory::TheoryId theoryId, TNode node);
 
   /** Sets the appropriate cache for a node */
-  static void setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);
+  static void setPreRewriteCache(theory::TheoryId theoryId,
+                                 TNode node, TNode cache);
 
   /** Sets the appropriate cache for a node */
-  static void setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);
+  static void setPostRewriteCache(theory::TheoryId theoryId,
+                                  TNode node, TNode cache);
+
+  // disable construction of rewriters; all functionality is static
+  Rewriter() CVC4_UNUSED;
+  Rewriter(const Rewriter&) CVC4_UNUSED;
 
 public:
 
-  /** Calls the pre rewrite for the given theory */
+  /** Calls the pre-rewriter for the given theory */
   static RewriteResponse callPreRewrite(theory::TheoryId theoryId, TNode node);
 
-  /** Calls the post rewrite for the given theory */
+  /** Calls the post-rewriter for the given theory */
   static RewriteResponse callPostRewrite(theory::TheoryId theoryId, TNode node);
 
   /**
-   * Rewrites the node using theoryOf to determine which rewriter to use on the node.
+   * Rewrites the node using theoryOf() to determine which rewriter to
+   * use on the node.
    */
   static Node rewrite(Node node);
 
@@ -65,7 +91,7 @@ public:
   static Node rewriteTo(theory::TheoryId theoryId, Node node);
 
   /**
-   * Should be called before the rewriter get's used for the first time.
+   * Should be called before the rewriter gets used for the first time.
    */
   static void init();
 
@@ -73,7 +99,7 @@ public:
    * Should be called to clean up any state.
    */
   static void shutdown();
-};
+};/* class Rewriter */
 
-} // Namesapce theory
-} // Namespace CVC4
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/rewriter_attributes.h b/src/theory/rewriter_attributes.h
index d33d7314e..86c2585b1 100644
--- a/src/theory/rewriter_attributes.h
+++ b/src/theory/rewriter_attributes.h
@@ -1,9 +1,20 @@
-/*
- * rewriter_attributes.h
- *
- *  Created on: Dec 27, 2010
- *      Author: dejan
- */
+/*********************                                                        */
+/*! \file rewriter_attributes.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
+ **
+ ** \brief Rewriter attributes
+ **
+ ** Rewriter attributes.
+ **/
 
 #pragma once
 
@@ -79,8 +90,7 @@ struct RewriteAttibute {
       node.setAttribute(post_rewrite(), cache);
     }
   }
-};
-
-} // Namespace CVC4
-} // Namespace theory
+};/* struct RewriteAttribute */
 
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
new file mode 100644
index 000000000..32e1599ea
--- /dev/null
+++ b/src/theory/substitutions.h
@@ -0,0 +1,42 @@
+/*********************                                                        */
+/*! \file substitutions.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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.\endverbatim
+ **
+ ** \brief A substitution mapping for theory simplification
+ **
+ ** A substitution mapping for theory simplification.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SUBSTITUTIONS_H
+#define __CVC4__THEORY__SUBSTITUTIONS_H
+
+#include <utility>
+#include <vector>
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+
+/**
+ * The type for the Substitutions mapping output by
+ * Theory::simplify(), TheoryEngine::simplify(), and
+ * Valuation::simplify().  This is in its own header to avoid circular
+ * dependences between those three.
+ */
+typedef std::vector< std::pair<Node, Node> > Substitutions;
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SUBSTITUTIONS_H */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index ac40c55d1..bba4c623a 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -24,6 +24,7 @@
 #include "expr/node.h"
 #include "expr/attribute.h"
 #include "theory/valuation.h"
+#include "theory/substitutions.h"
 #include "theory/output_channel.h"
 #include "context/context.h"
 #include "context/cdlist.h"
@@ -159,6 +160,9 @@ protected:
 
 public:
 
+  /**
+   * Return the ID of the theory responsible for the given type.
+   */
   static inline TheoryId theoryOf(TypeNode typeNode) {
     if (typeNode.getKind() == kind::TYPE_CONSTANT) {
       return typeConstantToTheoryId(typeNode.getConst<TypeConstant>());
@@ -168,10 +172,11 @@ public:
   }
 
   /**
-   * Returns the theory responsible for the node.
+   * Returns the ID of the theory responsible for the given node.
    */
   static inline TheoryId theoryOf(TNode node) {
-    if (node.getMetaKind() == kind::metakind::VARIABLE || node.getMetaKind() == kind::metakind::CONSTANT) {
+    if (node.getMetaKind() == kind::metakind::VARIABLE ||
+        node.getMetaKind() == kind::metakind::CONSTANT) {
       // Constants, variables, 0-ary constructors
       return theoryOf(node.getType());
     } else {
@@ -374,13 +379,29 @@ public:
   }
 
   /**
-   * The theory should only add (via .operator<< or .append()) to the
-   * "learned" builder.  It is a conjunction to add to the formula at
+   * Statically learn from assertion "in," which has been asserted
+   * true at the top level.  The theory should only add (via
+   * ::operator<< or ::append()) to the "learned" builder---it should
+   * *never* clear it.  It is a conjunction to add to the formula at
    * the top-level and may contain other theories' contributions.
    */
   virtual void staticLearning(TNode in, NodeBuilder<>& learned) { }
 
   /**
+   * Simplify a node in a theory-specific way.  The node is a theory
+   * operation or its negation, or an equality between theory-typed
+   * terms or its negation.  Add to "outSubstitutions" any
+   * replacements you want to make for the entire subterm; if you add
+   * [x,y] to the vector, the enclosing Boolean formula (call it
+   * "phi") will be replaced with (AND phi[x->y] (x = y)).  Use
+   * Valuation::simplify() to simplify subterms (it maintains a cache
+   * and dispatches to the appropriate theory).
+   */
+  virtual Node simplify(TNode in, Substitutions& outSubstitutions) {
+    return in;
+  }
+
+  /**
    * A Theory is called with presolve exactly one time per user
    * check-sat.  presolve() is called after preregistration,
    * rewriting, and Boolean propagation, (other theories'
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index b4d6654b1..69220ad62 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -420,9 +420,40 @@ void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) {
     reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->staticLearning(in, learned); \
   }
 
-  // notify each theory using the statement above
+  // static learning for each theory using the statement above
   CVC4_FOR_EACH_THEORY
 }
 
+Node TheoryEngine::simplify(TNode in, theory::Substitutions& outSubstitutions) {
+  SimplifyCache::Scope cache(d_simplifyCache, in);
+  if(cache) {
+    outSubstitutions.insert(outSubstitutions.end(),
+                            cache.get().second.begin(),
+                            cache.get().second.end());
+    return cache.get().first;
+  }
+
+  size_t prevSize = outSubstitutions.size();
+
+  TNode atom = in.getKind() == kind::NOT ? in[0] : in;
+
+  theory::Theory* theory = theoryOf(atom);
+
+  Debug("simplify") << push << "simplifying " << in << " to " << theory->identify() << std::endl;
+  Node n = theory->simplify(in, outSubstitutions);
+  Debug("simplify") << "got from " << theory->identify() << " : " << n << std::endl << pop;
+
+  atom = n.getKind() == kind::NOT ? n[0] : n;
+
+  if(atom.getKind() == kind::EQUAL) {
+    theory::TheoryId typeTheory = theory::Theory::theoryOf(atom[0].getType());
+    Debug("simplify") << push << "simplifying " << n << " to " << typeTheory << std::endl;
+    n = d_theoryTable[typeTheory]->simplify(n, outSubstitutions);
+    Debug("simplify") << "got from " << d_theoryTable[typeTheory]->identify() << " : " << n << std::endl << pop;
+  }
+
+  cache(std::make_pair(n, theory::Substitutions(outSubstitutions.begin() + prevSize, outSubstitutions.end())));
+  return n;
+}
 
 }/* CVC4 namespace */
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 19374d6db..e571c2bbd 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -22,15 +22,20 @@
 #define __CVC4__THEORY_ENGINE_H
 
 #include <deque>
+#include <vector>
+#include <utility>
 
 #include "expr/node.h"
 #include "prop/prop_engine.h"
 #include "theory/shared_term_manager.h"
 #include "theory/theory.h"
 #include "theory/rewriter.h"
+#include "theory/substitutions.h"
 #include "theory/valuation.h"
 #include "util/options.h"
 #include "util/stats.h"
+#include "util/hash.h"
+#include "util/cache.h"
 
 namespace CVC4 {
 
@@ -69,6 +74,16 @@ class TheoryEngine {
   size_t d_activeTheories;
 
   /**
+   * The type of the simplification cache.
+   */
+  typedef Cache<Node, std::pair<Node, theory::Substitutions>, NodeHashFunction> SimplifyCache;
+
+  /**
+   * A cache for simplification.
+   */
+  SimplifyCache d_simplifyCache;
+
+  /**
    * An output channel for Theory that passes messages
    * back to a TheoryEngine.
    */
@@ -273,11 +288,17 @@ public:
   }
 
   /**
-   * Preprocess a node.  This involves theory-specific rewriting, then
-   * calling preRegister() on what's left over.
+   * Preprocess a node.  This involves ITE removal and theory-specific
+   * rewriting.
+   *
    * @param n the node to preprocess
    */
   Node preprocess(TNode n);
+
+  /**
+   * Preregister a Theory atom with the responsible theory (or
+   * theories).
+   */
   void preRegister(TNode preprocessed);
 
   /**
@@ -325,12 +346,18 @@ public:
   bool check(theory::Theory::Effort effort);
 
   /**
-   * Calls staticLearning() on all active theories, accumulating their
+   * Calls staticLearning() on all theories, accumulating their
    * combined contributions in the "learned" builder.
    */
   void staticLearning(TNode in, NodeBuilder<>& learned);
 
   /**
+   * Calls simplify() on all theories, accumulating their combined
+   * contributions in the "outSubstitutions" vector.
+   */
+  Node simplify(TNode in, theory::Substitutions& outSubstitutions);
+
+  /**
    * Calls presolve() on all active theories and returns true
    * if one of the theories discovers a conflict.
    */
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 536255c2d..604ae21e1 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -41,5 +41,13 @@ Node Valuation::getSatValue(TNode n) const{
   }
 }
 
+Node Valuation::simplify(TNode in, Substitutions& outSubstitutions) {
+  return d_engine->simplify(in, outSubstitutions);
+}
+
+Node Valuation::rewrite(TNode in) {
+  return d_engine->preprocess(in);
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 0c60ec5ea..d46b9aab1 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -24,6 +24,7 @@
 #define __CVC4__THEORY__VALUATION_H
 
 #include "expr/node.h"
+#include "theory/substitutions.h"
 
 namespace CVC4 {
 
@@ -50,6 +51,20 @@ public:
    */
   Node getSatValue(TNode n) const;
 
+  /**
+   * Simplify a node.  Intended to be used by a theory's simplify()
+   * function to simplify subterms (TheoryEngine will cache the
+   * results and make sure that the request is directed to the correct
+   * theory).
+   */
+  Node simplify(TNode in, Substitutions& outSubstitutions);
+
+  /**
+   * Rewrite a node.  Intended to be used by a theory to have the
+   * TheoryEngine fully rewrite a node.
+   */
+  Node rewrite(TNode in);
+
 };/* class Valuation */
 
 }/* CVC4::theory namespace */