updated preprocessing and rewriting input equalities into inequalities for LRA

5 files changed, 496 insertions, 522 deletions

diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index e5055c164..fd44ec13b 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -19,6 +19,7 @@
 #include "theory/booleans/circuit_propagator.h"
 #include "util/utility.h"
 
+#include <stack>
 #include <vector>
 #include <algorithm>
 
@@ -28,353 +29,363 @@ 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()) {
+void CircuitPropagator::assert(TNode assertion) 
+{
+  if (assertion.getKind() == kind::AND) {
+    for (unsigned i = 0; i < assertion.getNumChildren(); ++ i) {
+      assert(assertion[i]);  
+    }
+  } else {
+    // Analyze the assertion for back-edges and all that
+    computeBackEdges(assertion);
+    // Assign the given assertion to true
+    assignAndEnqueue(assertion, true);
+  }
+}
+
+void CircuitPropagator::computeBackEdges(TNode node) {
+
+  Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(" << node << ")" << endl;
+
+  // Vector of nodes to visit
+  vector<TNode> toVisit;
+
+  // Start with the top node
+  if (d_seen.find(node) == d_seen.end()) {
+    toVisit.push_back(node);
+    d_seen.insert(node);
+  }
+
+  // Initialize the back-edges for the root, so we don't have a special case
+  d_backEdges[node];
+
+  // Go through the visit list
+  for (unsigned i = 0; i < toVisit.size(); ++ i) {
+    // Node we need to visit
+    TNode current = toVisit[i];
+    Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(): processing " << current << endl;
+    Assert(d_seen.find(current) != d_seen.end());
+
+    // If this not an atom visit all the children and compute the back edges
+    if (Theory::theoryOf(current) == THEORY_BOOL) {
+      for (unsigned child = 0, child_end = current.getNumChildren(); child < child_end; ++ child) {
+        TNode childNode = current[child];
+        // Add the back edge
+        d_backEdges[childNode].push_back(current);
+        // Add to the queue if not seen yet
+        if (d_seen.find(childNode) == d_seen.end()) {
+          toVisit.push_back(childNode);
+          d_seen.insert(childNode);
+        }
+      }
+    }
+  }
+}
+
+void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) {
+
+  Debug("circuit-prop") << "CircuitPropagator::propagateBackward(" << parent << ", " << parentAssignment << ")" << endl;
+
+  // backward rules
+  switch(parent.getKind()) {
+  case kind::AND:
+    if (parentAssignment) {
+      // AND = TRUE: forall children c, assign(c = TRUE)
+      for(TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end; ++i) {
+        assignAndEnqueue(*i, true);
+      }
+    } else {
+      // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE)
+      TNode::iterator holdout = find_if_unique(parent.begin(), parent.end(), not1(IsAssignedTo(*this, true)));
+      if (holdout != parent.end()) {
+        assignAndEnqueue(*holdout, false);
+      }
+    }
+    break;
+  case kind::OR:
+    if (parentAssignment) {
+      // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE)
+      TNode::iterator holdout = find_if_unique(parent.begin(), parent.end(), not1(IsAssignedTo(*this, false)));
+      if (holdout != parent.end()) {
+        assignAndEnqueue(*holdout, true);
+      }
+    } else {
+      // OR = FALSE: forall children c, assign(c = FALSE)
+      for(TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end; ++i) {
+        assignAndEnqueue(*i, false);
+      }
+    }
+    break;
+  case kind::NOT:
+    // NOT = b: assign(c = !b)
+    assignAndEnqueue(parent[0], !parentAssignment);
+    break;
+  case kind::ITE:
+    if (isAssignedTo(parent[0], true)) {
+      // ITE c x y = v: if c is assigned and TRUE, assign(x = v)
+      assignAndEnqueue(parent[1], parentAssignment);
+    } else if (isAssignedTo(parent[0], false)) {
+      // ITE c x y = v: if c is assigned and FALSE, assign(y = v)
+      assignAndEnqueue(parent[2], parentAssignment);
+    } else if (isAssigned(parent[1]) && isAssigned(parent[2])) {
+      if (getAssignment(parent[1]) == parentAssignment && getAssignment(parent[2]) != parentAssignment) {
+        // ITE c x y = v: if c is unassigned, x and y are assigned, x==v and y!=v, assign(c = TRUE)
+        assignAndEnqueue(parent[0], true);
+      } else if (getAssignment(parent[1]) != parentAssignment && getAssignment(parent[2]) == parentAssignment) {
+        // ITE c x y = v: if c is unassigned, x and y are assigned, x!=v and y==v, assign(c = FALSE)
+        assignAndEnqueue(parent[0], false);
+      }
+    }
+    break;
+  case kind::IFF:
+    if (parentAssignment) {
+      // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment [resp x = y.assignment])
+      if (isAssigned(parent[0])) {
+        assignAndEnqueue(parent[1], getAssignment(parent[0]));
+      } else if (isAssigned(parent[1])) {
+        assignAndEnqueue(parent[0], getAssignment(parent[1]));
+      }
+    } else {
+      // IFF x y = FALSE: if x [resp y] is assigned, assign(y = !x.assignment [resp x = !y.assignment])
+      if (isAssigned(parent[0])) {
+        assignAndEnqueue(parent[1], !getAssignment(parent[0]));
+      } else if (isAssigned(parent[1])) {
+        assignAndEnqueue(parent[0], !getAssignment(parent[1]));
+      }
+    }
+    break;
+  case kind::IMPLIES:
+    if (parentAssignment) {
+      if (isAssignedTo(parent[0], true)) {
+        // IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE)
+        assignAndEnqueue(parent[1], true);
+      }
+      if (isAssignedTo(parent[1], false)) {
+        // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE)
+        assignAndEnqueue(parent[0], false);
+      }
+    } else {
+      // IMPLIES x y = FALSE: assign(x = TRUE) and assign(y = FALSE)
+      assignAndEnqueue(parent[0], true);
+      assignAndEnqueue(parent[1], false);
+    }
+    break;
+  case kind::XOR:
+    if (parentAssignment) {
+      if (isAssigned(parent[0])) {
+        // XOR x y = TRUE, and x assigned, assign(y = !assignment(x))
+        assignAndEnqueue(parent[1], !getAssignment(parent[0]));
+      } else if (isAssigned(parent[1])) {
+        // XOR x y = TRUE, and y assigned, assign(x = !assignment(y))
+        assignAndEnqueue(parent[0], !getAssignment(parent[1]));
+      }
+    } else {
+      if (isAssigned(parent[0])) {
+        // XOR x y = FALSE, and x assigned, assign(y = assignment(x))
+        assignAndEnqueue(parent[1], getAssignment(parent[0]));
+      } else if (isAssigned(parent[1])) {
+        // XOR x y = FALSE, and y assigned, assign(x = assignment(y))
+        assignAndEnqueue(parent[0], getAssignment(parent[1]));
+      }
+    }
+    break;
+  default:
+    Unhandled();
+  }
+}
+
+
+void CircuitPropagator::propagateForward(TNode child, bool childAssignment) {
+
+  // The assignment we have
+  Debug("circuit-prop") << "CircuitPropagator::propagateForward(" << child << ", " << childAssignment << ")" << endl;
+
+  // Get the back any nodes where this is child
+  const vector<TNode>& parents = d_backEdges.find(child)->second;
+
+  // Go through the parents and see if there is anything to propagate
+  vector<TNode>::const_iterator parent_it = parents.begin();
+  vector<TNode>::const_iterator parent_it_end = parents.end();
+  for(; parent_it != parent_it_end && !d_conflict; ++ parent_it) {
+    // The current parent of the child
+    TNode parent = *parent_it;
+    Assert(parent.hasSubterm(child));
+
+    // Forward rules
+    switch(parent.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);
+      if (childAssignment) {
+        TNode::iterator holdout;
+        holdout = find_if (parent.begin(), parent.end(), not1(IsAssignedTo(*this, true)));
+        if (holdout == parent.end()) { // all children are assigned TRUE
+          // AND ...(x=TRUE)...: if all children now assigned to TRUE, assign(AND = TRUE)
+          assignAndEnqueue(parent, true);
+        } else if (isAssignedTo(parent, false)) {// the AND is FALSE
+          // is the holdout unique ?
+          TNode::iterator other = find_if (holdout + 1, parent.end(), not1(IsAssignedTo(*this, true)));
+          if (other == parent.end()) { // the holdout is unique
+            // AND ...(x=TRUE)...: if all children BUT ONE now assigned to TRUE, and AND == FALSE, assign(last_holdout = FALSE)
+            assignAndEnqueue(*holdout, false);
+          }
         }
       } 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);
-        }
+        // AND ...(x=FALSE)...: assign(AND = FALSE)
+        assignAndEnqueue(parent, false);
       }
       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);
-        }
+      if (childAssignment) {
+        // OR ...(x=TRUE)...: assign(OR = TRUE)
+        assignAndEnqueue(parent, true);
       } 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);
+        TNode::iterator holdout;
+        holdout = find_if (parent.begin(), parent.end(), not1(IsAssignedTo(*this, false)));
+        if (holdout == parent.end()) { // all children are assigned FALSE
+          // OR ...(x=FALSE)...: if all children now assigned to FALSE, assign(OR = FALSE)
+          assignAndEnqueue(parent, false);
+        } else if (isAssignedTo(parent, true)) {// the OR is TRUE
+          // is the holdout unique ?
+          TNode::iterator other = find_if (holdout + 1, parent.end(), not1(IsAssignedTo(*this, false)));
+          if (other == parent.end()) { // the holdout is unique
+            // OR ...(x=FALSE)...: if all children BUT ONE now assigned to FALSE, and OR == TRUE, assign(last_holdout = TRUE)
+            assignAndEnqueue(*holdout, true);
+          }
         }
       }
       break;
+
     case kind::NOT:
-      // NOT = b: assign(c = !b)
-      Debug("circuit-prop") << "bNOT" << endl;
-      assign(in[0], !polarity, changed);
+      // NOT (x=b): assign(NOT = !b)
+      assignAndEnqueue(parent, !childAssignment);
       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);
+      if (child == parent[0]) {
+        if (childAssignment) {
+          if (isAssigned(parent[1])) {
+            // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment)
+            assignAndEnqueue(parent, getAssignment(parent[1]));
+          }
+        } else {
+          if (isAssigned(parent[2])) {
+            // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment)
+            assignAndEnqueue(parent, getAssignment(parent[2]));
+          }
+        }
+      }
+      if (child == parent[1]) {
+        if (isAssignedTo(parent[0], true)) {
+          // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v)
+          assignAndEnqueue(parent, childAssignment);
+        }
+      }
+      if (child == parent[2]) {
+        Assert(child == parent[2]);
+        if (isAssignedTo(parent[0], false)) {
+          // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v)
+          assignAndEnqueue(parent, childAssignment);
         }
       }
       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);
-        }
+      if (isAssigned(parent[0]) && isAssigned(parent[1])) {
+        // IFF x y: if x or y is assigned, assign(IFF = (x.assignment <=> y.assignment))
+        assignAndEnqueue(parent, getAssignment(parent[0]) == getAssignment(parent[1]));
       } 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);
+        if (isAssigned(parent)) {
+          if (child == parent[0]) {
+            if (getAssignment(parent)) {
+              // IFF (x = b) y: if IFF is assigned to TRUE, assign(y = b)
+              assignAndEnqueue(parent[1], childAssignment);
+            } else {
+              // IFF (x = b) y: if IFF is assigned to FALSE, assign(y = !b)
+              assignAndEnqueue(parent[1], !childAssignment);
+            }
+          } else {
+            Assert(child == parent[1]);
+            if (getAssignment(parent)) {
+              // IFF x y = b: if IFF is assigned to TRUE, assign(x = b)
+              assignAndEnqueue(parent[0], childAssignment);
+            } else {
+              // IFF x y = b y: if IFF is assigned to TRUE, assign(x = !b)
+              assignAndEnqueue(parent[0], !childAssignment);
+            }
+          }
         }
       }
       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 (isAssigned(parent[0]) && isAssigned(parent[1])) {
+        // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2))
+        assignAndEnqueue(parent, !getAssignment(parent[0]) || getAssignment(parent[1]));
+      } else {
+        if (child == parent[0] && childAssignment && isAssignedTo(parent, true)) {
+          // IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE)
+          assignAndEnqueue(parent[1], true);
         }
-        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);
+        if (child == parent[1] && !childAssignment && isAssignedTo(parent, true)) {
+          // IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE)
+          assignAndEnqueue(parent[0], false);
         }
-      } 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);
+        // 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(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);
+      if (isAssigned(parent)) {
+        if (child == parent[0]) {
+          // XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR)
+          assignAndEnqueue(parent[1], childAssignment != getAssignment(parent));
+        } else {
+          Assert(child == parent[1]);
+          // XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR))
+          assignAndEnqueue(parent[0], childAssignment != getAssignment(parent));
         }
       }
-      break;
-    case kind::CONST_BOOLEAN:
-      // nothing to do
+      if (isAssigned(parent[0]) && isAssigned(parent[1])) {
+        assignAndEnqueue(parent, getAssignment(parent[0]) != getAssignment(parent[1]));
+      }
       break;
     default:
-      Unhandled(k);
+      Unhandled();
     }
-    Debug("circuit-prop") << pop;
   }
 }
 
+bool CircuitPropagator::propagate() {
 
-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);
-      }
-    }
-  }
-}
+  Debug("circuit-prop") << "CircuitPropagator::propagate()" << std::endl;
 
+  for(unsigned i = 0; i < d_propagationQueue.size() && !d_conflict; ++ i) {
 
-bool CircuitPropagator::propagate(TNode in, bool polarity, vector<Node>& newFacts) {
-  try {
-    vector<TNode> changed;
+    // The current node we are propagating
+    TNode current = d_propagationQueue[i];
+    Debug("circuit-prop") << "CircuitPropagator::propagate(): processing " << current << std::endl;
+    bool assignment = getAssignment(current);
+    Debug("circuit-prop") << "CircuitPropagator::propagate(): assigned to " << (assignment ? "true" : "false") << std::endl;
 
-    Assert(kindToTheoryId(in.getKind()) == THEORY_BOOL);
+    // Is this an atom
+    bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.getMetaKind() == kind::metakind::VARIABLE;
 
-    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);
+    // If an atom, add to the list for simplification
+    if (atom) {
+      Debug("circuit-prop") << "CircuitPropagator::propagate(): adding to learned: " << (assignment ? (Node)current : current.notNode()) << std::endl;
+      d_learnedLiterals.push_back(assignment ? (Node)current : current.notNode());
+    }
 
-      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);
-        }
-      }
+    // Propagate this value to the children (if not an atom or a constant)
+    if (d_backwardPropagation && !atom && !current.isConst()) {
+      propagateBackward(current, assignment);
+    }
+    // Propagate this value to the parents
+    if (d_forwardPropagation) {
+      propagateForward(current, assignment);
     }
-  } catch(ConflictException& ce) {
-    return true;
   }
-  return false;
+
+  // No conflict
+  return d_conflict;
 }
 
 }/* CVC4::theory::booleans namespace */
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index f9efc20af..73a5be0f8 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -33,6 +33,7 @@ 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
@@ -40,104 +41,103 @@ namespace booleans {
  * 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 */
+public:
+
+  /**
+   * Value of a particular node
+   */
+  enum AssignmentStatus {
+    /** Node is currently unassigned */
+    UNASSIGNED = 0,
+    /** Node is assigned to true */
+    ASSIGNED_TO_TRUE,
+    /** Node is assigned to false */
+    ASSIGNED_TO_FALSE,
+  };
+
+  /** Invert a set value */
+  static inline AssignmentStatus neg(AssignmentStatus value) {
+    Assert(value != UNASSIGNED);
+    if (value == ASSIGNED_TO_TRUE) return ASSIGNED_TO_FALSE;
+    else return ASSIGNED_TO_TRUE;
+  }
+
+private:
+
+  /** Back edges from nodes to where they are used */
+  typedef std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction> BackEdgesMap;
+  BackEdgesMap d_backEdges;
 
-  enum {
-    ASSIGNMENT_MASK = 1,
-    IS_ASSIGNED_MASK = 2,
-    IS_PROPAGATED_FORWARD_MASK = 4,
-    IS_PROPAGATED_BACKWARD_MASK = 8
-  };/* enum */
+  /** The propagation queue */
+  std::vector<TNode> d_propagationQueue;
+
+  /** Are we in conflict */
+  bool d_conflict;
+
+  /** Map of substitutions */
+  std::vector<Node>& d_learnedLiterals;
+
+  /** Nodes that have been attached already (computed forward edges for) */
+  // All the nodes we've visited so far
+  std::hash_set<TNode, TNodeHashFunction> d_seen;
 
   /**
-   * 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
+   * Assignment status of each node.
    */
-  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;
+  typedef std::hash_map<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap;
+  AssignmentMap d_state;
+
+  /**
+   * Assign Node in circuit with the value and add it to the queue; note conflicts.
+   */
+  void assignAndEnqueue(TNode n, bool value) {
+
+    Debug("circuit-prop") << "CircuitPropagator::assign(" << n << ", " << (value ? "true" : "false") << ")" << std::endl;
+
+    if (n.getKind() == kind::CONST_BOOLEAN) {
+      // Assigning a constant to the opposite value is dumb
+      if (value != n.getConst<bool>()) {
+        d_conflict = true;
+        return;
       }
-      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;
+
+    // Get the current assignement
+    AssignmentStatus state = d_state[n];
+
+    if(state != UNASSIGNED) {
+      // If the node is already assigned we might have a conflict
+      if(value != (state == ASSIGNED_TO_TRUE)) {
+        d_conflict = true;
       }
-    } else {// if unassigned
-      Debug("circuit-prop") << "assigning(" << b << "): " << n << std::endl;
-      state |= IS_ASSIGNED_MASK | (b ? ASSIGNMENT_MASK : 0);
-      changed.push_back(n);
+    } else {
+      // If unassigned, mark it as assigned
+      d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE;
+      // Add for further propagation
+      d_propagationQueue.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);
+    AssignmentMap::const_iterator i = d_state.find(n);
+    return i != d_state.end() && ((*i).second != UNASSIGNED);
   }
-  /** 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);
+
+  /** True iff Node is assigned to the value. */
+  bool isAssignedTo(TNode n, bool value) const {
+    AssignmentMap::const_iterator i = d_state.find(n);
+    if (i == d_state.end()) return false;
+    if (value && ((*i).second == ASSIGNED_TO_TRUE)) return true;
+    if (!value && ((*i).second == ASSIGNED_TO_FALSE)) return true;
+    return false;
   }
+
   /** 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;
+  bool getAssignment(TNode n) const {
+    Assert(d_state.find(n) != d_state.end() && d_state.find(n)->second != UNASSIGNED);
+    return d_state.find(n)->second == ASSIGNED_TO_TRUE;
   }
 
   /** Predicate for use in STL functions. */
@@ -169,33 +169,52 @@ class CircuitPropagator {
   };/* class IsAssignedTo */
 
   /**
-   * Propagate new information (in = polarity) forward in circuit to
+   * Compute the map from nodes to the nodes that use it.
+   */
+  void computeBackEdges(TNode node);
+
+  /**
+   * Propagate new information forward in circuit to
    * the parents of "in".
    */
-  void propagateForward(TNode in, bool polarity, std::vector<TNode>& newFacts);
+  void propagateForward(TNode child, bool assignment);
+
   /**
-   * Propagate new information (in = polarity) backward in circuit to
+   * Propagate new information backward in circuit to
    * the children of "in".
    */
-  void propagateBackward(TNode in, bool polarity, std::vector<TNode>& newFacts);
+  void propagateBackward(TNode parent, bool assignment);
+
+  /** Whether to perform forward propagation */
+  bool d_forwardPropagation;
+  /** Whether to perform backward propagation */
+  bool d_backwardPropagation;
+  /** Whether to perform expensive propagations */
+  bool d_expensivePropagation;
 
 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) {
+  CircuitPropagator(std::vector<Node>& outLearnedLiterals, bool enableForward = true, bool enableBackward = true, bool enableExpensive = true) :
+    d_conflict(false),
+    d_learnedLiterals(outLearnedLiterals),
+    d_forwardPropagation(enableForward),
+    d_backwardPropagation(enableBackward),
+    d_expensivePropagation(enableExpensive)
+  {
   }
 
+  /** Assert for propagation */
+  void assert(TNode assertion);
+
   /**
-   * Propagate new information (in == polarity) through the circuit
-   * propagator.  New information discovered by the propagator are put
-   * in the (output-only) newFacts vector.
+   * Propagate through the asserted circuit propagator. New information discovered by the propagator
+   * are put in the subsitutions vector used in construction.
    *
    * @return true iff conflict found
    */
-  bool propagate(TNode in, bool polarity, std::vector<Node>& newFacts) CVC4_WARN_UNUSED_RESULT;
+  bool propagate() CVC4_WARN_UNUSED_RESULT;
 
 };/* class CircuitPropagator */
 
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 836022bc2..01185281a 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -97,134 +97,29 @@ Node TheoryBool::getValue(TNode n) {
   }
 }
 
-static void
-findAtoms(TNode in, vector<TNode>& atoms,
-          hash_map<TNode, vector<TNode>, TNodeHashFunction>& backEdges) {
-  Kind k CVC4_UNUSED = 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);
-        }
-      }
-    }
-  }
-}
+Theory::SolveStatus TheoryBool::solve(TNode in, SubstitutionMap& outSubstitutions) {
 
-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;
+  if (in.getKind() == kind::CONST_BOOLEAN && !in.getConst<bool>()) {
+    // If we get a false literal, we're in conflict
+    return SOLVE_STATUS_CONFLICT;
   }
 
-  // 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;
-      }
+  // Add the substitution from the variable to it's value
+  if (in.getKind() == kind::NOT) {
+    if (in[0].getKind() == kind::VARIABLE) {
+      outSubstitutions.addSubstitution(in[0], NodeManager::currentNM()->mkConst<bool>(false));
     } 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;
-      }
+      return SOLVE_STATUS_UNSOLVED;
     }
-  }
-
-  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);
-      }
+  } else {
+    if (in.getKind() == kind::VARIABLE) {
+      outSubstitutions.addSubstitution(in, NodeManager::currentNM()->mkConst<bool>(true));
+    } else {
+      return SOLVE_STATUS_UNSOLVED;
     }
-    n = b;
   }
-  Debug("simplify") << "final boolean simplification returned: " << n << endl;
-  return n;
+
+  return SOLVE_STATUS_SOLVED;
 }
 
 
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 40bbd3308..ce9938b10 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -36,7 +36,7 @@ public:
 
   Node getValue(TNode n);
 
-  Node simplify(TNode in, Substitutions& outSubstitutions);
+  SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions);
 
   std::string identify() const { return std::string("TheoryBool"); }
 };/* class TheoryBool */
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index c1be3b906..18aa71667 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -36,7 +36,31 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     if (n[0].getKind() == kind::NOT) return RewriteResponse(REWRITE_AGAIN, n[0][0]);
     break;
   }
-  case kind::IFF: {
+  case kind::OR: {
+    if (n.getNumChildren() == 2) {
+      if (n[0] == tt || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt);
+      if (n[0] == ff) return RewriteResponse(REWRITE_AGAIN, n[1]);
+      if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, n[0]);
+    }
+    break;
+  }
+  case kind::AND: {
+    if (n.getNumChildren() == 2) {
+      if (n[0] == ff || n[1] == ff) return RewriteResponse(REWRITE_DONE, ff);
+      if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]);
+      if (n[1] == tt) return RewriteResponse(REWRITE_AGAIN, n[0]);
+    }
+    break;
+  }
+  case kind::IMPLIES: {
+    if (n[0] == ff || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt);
+    if (n[0] == tt && n[0] == ff) return RewriteResponse(REWRITE_DONE, ff);
+    if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]);
+    if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+    break;
+  }
+  case kind::IFF:
+  case kind::EQUAL: {
     // rewrite simple cases of IFF
     if(n[0] == tt) {
       // IFF true x
@@ -62,10 +86,35 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     }
     break;
   }
+  case kind::XOR: {
+    // rewrite simple cases of XOR
+    if(n[0] == tt) {
+      // XOR true x
+      return RewriteResponse(REWRITE_AGAIN, n[1].notNode());
+    } else if(n[1] == tt) {
+      // XCR x true
+      return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+    } else if(n[0] == ff) {
+      // XOR false x
+      return RewriteResponse(REWRITE_AGAIN, n[1]);
+    } else if(n[1] == ff) {
+      // XOR x false
+      return RewriteResponse(REWRITE_AGAIN, n[0]);
+    } else if(n[0] == n[1]) {
+      // XOR x x
+      return RewriteResponse(REWRITE_DONE, ff);
+    } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) {
+      // XOR (NOT x) x
+      return RewriteResponse(REWRITE_DONE, tt);
+    } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
+      // XOR x (NOT x)
+      return RewriteResponse(REWRITE_DONE, tt);
+    }
+    break;
+  }
   case kind::ITE: {
     // non-Boolean-valued ITEs should have been removed in place of
     // a variable
-    Assert(n.getType().isBoolean());
     // rewrite simple cases of ITE
     if(n[0] == tt) {
       // ITE true x y