Refactor unconstrained simplification pass (#2374)

8 files changed, 408 insertions, 286 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index e0a9fb807..3681280ec 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -65,6 +65,8 @@ libcvc4_la_SOURCES = \
 	preprocessing/passes/apply_substs.h \
 	preprocessing/passes/apply_to_const.cpp \
 	preprocessing/passes/apply_to_const.h \
+	preprocessing/passes/bool_to_bv.cpp \
+	preprocessing/passes/bool_to_bv.h \
 	preprocessing/passes/bv_abstraction.cpp \
 	preprocessing/passes/bv_abstraction.h \
 	preprocessing/passes/bv_ackermann.cpp \
@@ -75,6 +77,8 @@ libcvc4_la_SOURCES = \
 	preprocessing/passes/bv_gauss.h \
 	preprocessing/passes/bv_intro_pow2.cpp \
 	preprocessing/passes/bv_intro_pow2.h \
+	preprocessing/passes/bv_to_bool.cpp \
+	preprocessing/passes/bv_to_bool.h \
 	preprocessing/passes/extended_rewriter_pass.cpp \
 	preprocessing/passes/extended_rewriter_pass.h \
 	preprocessing/passes/global_negate.cpp \
@@ -89,10 +93,6 @@ libcvc4_la_SOURCES = \
 	preprocessing/passes/nl_ext_purify.h \
 	preprocessing/passes/pseudo_boolean_processor.cpp \
 	preprocessing/passes/pseudo_boolean_processor.h \
-	preprocessing/passes/bool_to_bv.cpp \
-	preprocessing/passes/bool_to_bv.h \
-	preprocessing/passes/bv_to_bool.cpp \
-	preprocessing/passes/bv_to_bool.h \
 	preprocessing/passes/quantifiers_preprocess.cpp \
 	preprocessing/passes/quantifiers_preprocess.h \
 	preprocessing/passes/quantifier_macros.cpp \
@@ -115,6 +115,8 @@ libcvc4_la_SOURCES = \
 	preprocessing/passes/symmetry_detect.h \
 	preprocessing/passes/synth_rew_rules.cpp \
 	preprocessing/passes/synth_rew_rules.h \
+	preprocessing/passes/unconstrained_simplifier.cpp \
+	preprocessing/passes/unconstrained_simplifier.h \
 	preprocessing/preprocessing_pass.cpp \
 	preprocessing/preprocessing_pass.h \
 	preprocessing/preprocessing_pass_context.cpp \
@@ -244,8 +246,6 @@ libcvc4_la_SOURCES = \
 	theory/type_enumerator.h \
 	theory/type_set.cpp \
 	theory/type_set.h \
-	theory/unconstrained_simplifier.cpp \
-	theory/unconstrained_simplifier.h \
 	theory/valuation.cpp \
 	theory/valuation.h \
 	theory/arith/approx_simplex.cpp \
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 41529760b..6bb46f3f2 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -11,44 +11,46 @@
  **
  ** \brief Simplifications based on unconstrained variables
  **
- ** This module implements a preprocessing phase which replaces certain "unconstrained" expressions
- ** by variables.  Based on Roberto Bruttomesso's PhD thesis.
+ ** This module implements a preprocessing phase which replaces certain
+ ** "unconstrained" expressions by variables.  Based on Roberto
+ ** Bruttomesso's PhD thesis.
  **/
 
+#include "preprocessing/passes/unconstrained_simplifier.h"
 
-#include "theory/unconstrained_simplifier.h"
-
-#include "theory/rewriter.h"
-#include "theory/logic_info.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/logic_info.h"
+#include "theory/rewriter.h"
 
-using namespace std;
-using namespace CVC4;
-using namespace theory;
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
 
+using namespace CVC4::theory;
 
-UnconstrainedSimplifier::UnconstrainedSimplifier(context::Context* context,
-                                                 const LogicInfo& logicInfo)
-  : d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0),
-    d_context(context), d_substitutions(context), d_logicInfo(logicInfo)
+UnconstrainedSimplifier::UnconstrainedSimplifier(
+    PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "unconstrained-simplifier"),
+      d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0),
+      d_context(preprocContext->getDecisionContext()),
+      d_substitutions(preprocContext->getDecisionContext()),
+      d_logicInfo(preprocContext->getLogicInfo())
 {
   smtStatisticsRegistry()->registerStat(&d_numUnconstrainedElim);
 }
 
-
 UnconstrainedSimplifier::~UnconstrainedSimplifier()
 {
   smtStatisticsRegistry()->unregisterStat(&d_numUnconstrainedElim);
 }
 
-
-struct unc_preprocess_stack_element {
+struct unc_preprocess_stack_element
+{
   TNode node;
   TNode parent;
   unc_preprocess_stack_element(TNode n) : node(n) {}
   unc_preprocess_stack_element(TNode n, TNode p) : node(n), parent(p) {}
-};/* struct unc_preprocess_stack_element */
-
+}; /* struct unc_preprocess_stack_element */
 
 void UnconstrainedSimplifier::visitAll(TNode assertion)
 {
@@ -64,10 +66,13 @@ void UnconstrainedSimplifier::visitAll(TNode assertion)
     toVisit.pop_back();
 
     TNodeCountMap::iterator find = d_visited.find(current);
-    if (find != d_visited.end()) {
-      if (find->second == 1) {
+    if (find != d_visited.end())
+    {
+      if (find->second == 1)
+      {
         d_visitedOnce.erase(current);
-        if (current.isVar()) {
+        if (current.isVar())
+        {
           d_unconstrained.erase(current);
         }
       }
@@ -78,14 +83,18 @@ void UnconstrainedSimplifier::visitAll(TNode assertion)
     d_visited[current] = 1;
     d_visitedOnce[current] = parent;
 
-    if (current.getNumChildren() == 0) {
-      if (current.getKind()==kind::VARIABLE || current.getKind()==kind::SKOLEM) {
+    if (current.getNumChildren() == 0)
+    {
+      if (current.getKind() == kind::VARIABLE
+          || current.getKind() == kind::SKOLEM)
+      {
         d_unconstrained.insert(current);
       }
     }
-    else {
-      for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
-        TNode childNode = *child_it;
+    else
+    {
+      for (TNode childNode : current)
+      {
         toVisit.push_back(unc_preprocess_stack_element(childNode, current));
       }
     }
@@ -94,18 +103,19 @@ void UnconstrainedSimplifier::visitAll(TNode assertion)
 
 Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var)
 {
-  Node n = NodeManager::currentNM()->mkSkolem("unconstrained", t, "a new var introduced because of unconstrained variable " + var.toString());
+  Node n = NodeManager::currentNM()->mkSkolem(
+      "unconstrained",
+      t,
+      "a new var introduced because of unconstrained variable "
+          + var.toString());
   return n;
 }
 
-
 void UnconstrainedSimplifier::processUnconstrained()
 {
-  TNodeSet::iterator it = d_unconstrained.begin(), iend = d_unconstrained.end();
-  vector<TNode> workList;
-  for ( ; it != iend; ++it) {
-    workList.push_back(*it);
-  }
+  NodeManager* nm = NodeManager::currentNM();
+
+  vector<TNode> workList(d_unconstrained.begin(), d_unconstrained.end());
   Node currentSub;
   TNode parent;
   bool swap;
@@ -116,65 +126,94 @@ void UnconstrainedSimplifier::processUnconstrained()
 
   TNode current = workList.back();
   workList.pop_back();
-  for (;;) {
+  for (;;)
+  {
     Assert(d_visitedOnce.find(current) != d_visitedOnce.end());
     parent = d_visitedOnce[current];
-    if (!parent.isNull()) {
+    if (!parent.isNull())
+    {
       swap = isSigned = strict = false;
       bool checkParent = false;
-      switch (parent.getKind()) {
-
-        // If-then-else operator - any two unconstrained children makes the parent unconstrained
-        case kind::ITE: {
-          Assert(parent[0] == current || parent[1] == current || parent[2] == current);
-          bool uCond = parent[0] == current || d_unconstrained.find(parent[0]) != d_unconstrained.end();
-          bool uThen = parent[1] == current || d_unconstrained.find(parent[1]) != d_unconstrained.end();
-          bool uElse = parent[2] == current || d_unconstrained.find(parent[2]) != d_unconstrained.end();
-          if ((uCond && uThen) || (uCond && uElse) || (uThen && uElse)) {
-            if (d_unconstrained.find(parent) == d_unconstrained.end() &&
-                !d_substitutions.hasSubstitution(parent)) {
+      switch (parent.getKind())
+      {
+        // If-then-else operator - any two unconstrained children makes the
+        // parent unconstrained
+        case kind::ITE:
+        {
+          Assert(parent[0] == current || parent[1] == current
+                 || parent[2] == current);
+          bool uCond =
+              parent[0] == current
+              || d_unconstrained.find(parent[0]) != d_unconstrained.end();
+          bool uThen =
+              parent[1] == current
+              || d_unconstrained.find(parent[1]) != d_unconstrained.end();
+          bool uElse =
+              parent[2] == current
+              || d_unconstrained.find(parent[2]) != d_unconstrained.end();
+          if ((uCond && uThen) || (uCond && uElse) || (uThen && uElse))
+          {
+            if (d_unconstrained.find(parent) == d_unconstrained.end()
+                && !d_substitutions.hasSubstitution(parent))
+            {
               ++d_numUnconstrainedElim;
-              if (uThen) {
-                if (parent[1] != current) {
-                  if (parent[1].isVar()) {
+              if (uThen)
+              {
+                if (parent[1] != current)
+                {
+                  if (parent[1].isVar())
+                  {
                     currentSub = parent[1];
                   }
-                  else {
+                  else
+                  {
                     Assert(d_substitutions.hasSubstitution(parent[1]));
                     currentSub = d_substitutions.apply(parent[1]);
                   }
                 }
-                else if (currentSub.isNull()) {
+                else if (currentSub.isNull())
+                {
                   currentSub = current;
                 }
               }
-              else if (parent[2] != current) {
-                if (parent[2].isVar()) {
+              else if (parent[2] != current)
+              {
+                if (parent[2].isVar())
+                {
                   currentSub = parent[2];
                 }
-                else {
+                else
+                {
                   Assert(d_substitutions.hasSubstitution(parent[2]));
                   currentSub = d_substitutions.apply(parent[2]);
                 }
               }
-              else if (currentSub.isNull()) {
+              else if (currentSub.isNull())
+              {
                 currentSub = current;
               }
               current = parent;
             }
-            else {
+            else
+            {
               currentSub = Node();
             }
           }
-          else if (uCond) {
+          else if (uCond)
+          {
             Cardinality card = parent.getType().getCardinality();
-            if (card.isFinite() && !card.isLargeFinite() && card.getFiniteCardinality() == 2) {
-              // Special case: condition is unconstrained, then and else are different, and total cardinality of the type is 2, then the result
-              // is unconstrained
+            if (card.isFinite() && !card.isLargeFinite()
+                && card.getFiniteCardinality() == 2)
+            {
+              // Special case: condition is unconstrained, then and else are
+              // different, and total cardinality of the type is 2, then the
+              // result is unconstrained
               Node test = Rewriter::rewrite(parent[1].eqNode(parent[2]));
-              if (test == NodeManager::currentNM()->mkConst<bool>(false)) {
+              if (test == nm->mkConst<bool>(false))
+              {
                 ++d_numUnconstrainedElim;
-                if (currentSub.isNull()) {
+                if (currentSub.isNull())
+                {
                   currentSub = current;
                 }
                 currentSub = newUnconstrainedVar(parent.getType(), currentSub);
@@ -185,24 +224,30 @@ void UnconstrainedSimplifier::processUnconstrained()
           break;
         }
 
-        // Comparisons that return a different type - assuming domains are larger than 1, any
-        // unconstrained child makes parent unconstrained as well
+        // Comparisons that return a different type - assuming domains are
+        // larger than 1, any unconstrained child makes parent unconstrained as
+        // well
         case kind::EQUAL:
-          if (parent[0].getType() != parent[1].getType()) {
+          if (parent[0].getType() != parent[1].getType())
+          {
             TNode other = (parent[0] == current) ? parent[1] : parent[0];
-            if (current.getType().isSubtypeOf(other.getType())) {
+            if (current.getType().isSubtypeOf(other.getType()))
+            {
               break;
             }
           }
-          if( parent[0].getType().isDatatype() ){
+          if (parent[0].getType().isDatatype())
+          {
             TypeNode tn = parent[0].getType();
             const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-            if( dt.isRecursiveSingleton( tn.toType() ) ){
-              //domain size may be 1
+            if (dt.isRecursiveSingleton(tn.toType()))
+            {
+              // domain size may be 1
               break;
             }
           }
-          if( parent[0].getType().isBoolean() ){
+          if (parent[0].getType().isBoolean())
+          {
             checkParent = true;
             break;
           }
@@ -212,18 +257,21 @@ void UnconstrainedSimplifier::processUnconstrained()
         case kind::GT:
         case kind::GEQ:
         {
-          if (d_unconstrained.find(parent) == d_unconstrained.end() &&
-              !d_substitutions.hasSubstitution(parent)) {
+          if (d_unconstrained.find(parent) == d_unconstrained.end()
+              && !d_substitutions.hasSubstitution(parent))
+          {
             ++d_numUnconstrainedElim;
-            Assert(parent[0] != parent[1] &&
-                   (parent[0] == current || parent[1] == current));
-            if (currentSub.isNull()) {
+            Assert(parent[0] != parent[1]
+                   && (parent[0] == current || parent[1] == current));
+            if (currentSub.isNull())
+            {
               currentSub = current;
             }
             currentSub = newUnconstrainedVar(parent.getType(), currentSub);
             current = parent;
           }
-          else {
+          else
+          {
             currentSub = Node();
           }
           break;
@@ -236,24 +284,28 @@ void UnconstrainedSimplifier::processUnconstrained()
         case kind::UMINUS:
           ++d_numUnconstrainedElim;
           Assert(parent[0] == current);
-          if (currentSub.isNull()) {
+          if (currentSub.isNull())
+          {
             currentSub = current;
           }
           current = parent;
           break;
 
-        // Unary operators that propagate unconstrainedness and return a different type
+        // Unary operators that propagate unconstrainedness and return a
+        // different type
         case kind::BITVECTOR_EXTRACT:
           ++d_numUnconstrainedElim;
           Assert(parent[0] == current);
-          if (currentSub.isNull()) {
+          if (currentSub.isNull())
+          {
             currentSub = current;
           }
           currentSub = newUnconstrainedVar(parent.getType(), currentSub);
           current = parent;
           break;
 
-        // Operators returning same type requiring all children to be unconstrained
+        // Operators returning same type requiring all children to be
+        // unconstrained
         case kind::AND:
         case kind::OR:
         case kind::IMPLIES:
@@ -263,13 +315,16 @@ void UnconstrainedSimplifier::processUnconstrained()
         case kind::BITVECTOR_NOR:
         {
           bool allUnconstrained = true;
-          for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) {
-            if (d_unconstrained.find(*child_it) == d_unconstrained.end()) {
+          for (TNode child : parent)
+          {
+            if (d_unconstrained.find(child) == d_unconstrained.end())
+            {
               allUnconstrained = false;
               break;
             }
           }
-          if (allUnconstrained) {
+          if (allUnconstrained)
+          {
             checkParent = true;
           }
         }
@@ -283,135 +338,177 @@ void UnconstrainedSimplifier::processUnconstrained()
         case kind::BITVECTOR_UREM_TOTAL:
         case kind::BITVECTOR_SDIV:
         case kind::BITVECTOR_SREM:
-        case kind::BITVECTOR_SMOD: {
+        case kind::BITVECTOR_SMOD:
+        {
           bool allUnconstrained = true;
           bool allDifferent = true;
-          for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) {
-            if (d_unconstrained.find(*child_it) == d_unconstrained.end()) {
+          for (TNode::iterator child_it = parent.begin();
+               child_it != parent.end();
+               ++child_it)
+          {
+            if (d_unconstrained.find(*child_it) == d_unconstrained.end())
+            {
               allUnconstrained = false;
               break;
             }
-            for(TNode::iterator child_it2 = child_it + 1; child_it2 != parent.end(); ++child_it2) {
-              if (*child_it == *child_it2) {
+            for (TNode::iterator child_it2 = child_it + 1;
+                 child_it2 != parent.end();
+                 ++child_it2)
+            {
+              if (*child_it == *child_it2)
+              {
                 allDifferent = false;
                 break;
               }
             }
           }
-          if (allUnconstrained && allDifferent) {
+          if (allUnconstrained && allDifferent)
+          {
             checkParent = true;
           }
           break;
         }
 
-        // Requires all children to be unconstrained and different, and returns a different type
+        // Requires all children to be unconstrained and different, and returns
+        // a different type
         case kind::BITVECTOR_CONCAT:
         {
           bool allUnconstrained = true;
           bool allDifferent = true;
-          for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) {
-            if (d_unconstrained.find(*child_it) == d_unconstrained.end()) {
+          for (TNode::iterator child_it = parent.begin();
+               child_it != parent.end();
+               ++child_it)
+          {
+            if (d_unconstrained.find(*child_it) == d_unconstrained.end())
+            {
               allUnconstrained = false;
               break;
             }
-            for(TNode::iterator child_it2 = child_it + 1; child_it2 != parent.end(); ++child_it2) {
-              if (*child_it == *child_it2) {
+            for (TNode::iterator child_it2 = child_it + 1;
+                 child_it2 != parent.end();
+                 ++child_it2)
+            {
+              if (*child_it == *child_it2)
+              {
                 allDifferent = false;
                 break;
               }
             }
           }
-          if (allUnconstrained && allDifferent) {
-            if (d_unconstrained.find(parent) == d_unconstrained.end() &&
-                !d_substitutions.hasSubstitution(parent)) {
+          if (allUnconstrained && allDifferent)
+          {
+            if (d_unconstrained.find(parent) == d_unconstrained.end()
+                && !d_substitutions.hasSubstitution(parent))
+            {
               ++d_numUnconstrainedElim;
-              if (currentSub.isNull()) {
+              if (currentSub.isNull())
+              {
                 currentSub = current;
               }
               currentSub = newUnconstrainedVar(parent.getType(), currentSub);
               current = parent;
             }
-            else {
+            else
+            {
               currentSub = Node();
             }
           }
         }
         break;
 
-        // N-ary operators returning same type requiring at least one child to be unconstrained
+        // N-ary operators returning same type requiring at least one child to
+        // be unconstrained
         case kind::PLUS:
         case kind::MINUS:
-          if (current.getType().isInteger() &&
-              !parent.getType().isInteger()) {
+          if (current.getType().isInteger() && !parent.getType().isInteger())
+          {
             break;
           }
         case kind::XOR:
         case kind::BITVECTOR_XOR:
         case kind::BITVECTOR_XNOR:
         case kind::BITVECTOR_PLUS:
-        case kind::BITVECTOR_SUB:
-          checkParent = true;
-          break;
+        case kind::BITVECTOR_SUB: checkParent = true; break;
 
-        // Multiplication/division: must be non-integer and other operand must be non-zero
-        case kind::MULT: {
+        // Multiplication/division: must be non-integer and other operand must
+        // be non-zero
+        case kind::MULT:
         case kind::DIVISION:
+        {
           Assert(parent.getNumChildren() == 2);
           TNode other;
-          if (parent[0] == current) {
+          if (parent[0] == current)
+          {
             other = parent[1];
           }
-          else {
+          else
+          {
             Assert(parent[1] == current);
             other = parent[0];
           }
-          if (d_unconstrained.find(other) != d_unconstrained.end()) {
-            if (d_unconstrained.find(parent) == d_unconstrained.end() &&
-                !d_substitutions.hasSubstitution(parent)) {
-              if (current.getType().isInteger() && other.getType().isInteger()) {
-                Assert(parent.getKind() == kind::DIVISION || parent.getType().isInteger());
-                if (parent.getKind() == kind::DIVISION) {
+          if (d_unconstrained.find(other) != d_unconstrained.end())
+          {
+            if (d_unconstrained.find(parent) == d_unconstrained.end()
+                && !d_substitutions.hasSubstitution(parent))
+            {
+              if (current.getType().isInteger() && other.getType().isInteger())
+              {
+                Assert(parent.getKind() == kind::DIVISION
+                       || parent.getType().isInteger());
+                if (parent.getKind() == kind::DIVISION)
+                {
                   break;
                 }
               }
               ++d_numUnconstrainedElim;
-              if (currentSub.isNull()) {
+              if (currentSub.isNull())
+              {
                 currentSub = current;
               }
               current = parent;
             }
-            else {
+            else
+            {
               currentSub = Node();
             }
           }
-          else {
-            // if only the denominator of a division is unconstrained, can't set it to 0 so the result is not unconstrained
-            if (parent.getKind() == kind::DIVISION && current == parent[1]) {
+          else
+          {
+            // if only the denominator of a division is unconstrained, can't
+            // set it to 0 so the result is not unconstrained
+            if (parent.getKind() == kind::DIVISION && current == parent[1])
+            {
               break;
             }
-            NodeManager* nm = NodeManager::currentNM();
-            // if we are an integer, the only way we are unconstrained is if we are a MULT by -1
-            if (current.getType().isInteger()) {
+            // if we are an integer, the only way we are unconstrained is if
+            // we are a MULT by -1
+            if (current.getType().isInteger())
+            {
               // div/mult by 1 should have been simplified
               Assert(other != nm->mkConst<Rational>(1));
-              if (other == nm->mkConst<Rational>(-1)) {
-                // div by -1 should have been simplified
+              // div by -1 should have been simplified
+              if (other != nm->mkConst<Rational>(-1))
+              {
+                break;
+              }
+              else
+              {
                 Assert(parent.getKind() == kind::MULT);
                 Assert(parent.getType().isInteger());
               }
-              else {
-                break;
-              }
             }
-            else {
-              // TODO: could build ITE here
+            else
+            {
+              // TODO(#2377): could build ITE here
               Node test = other.eqNode(nm->mkConst<Rational>(0));
-              if (Rewriter::rewrite(test) != nm->mkConst<bool>(false)) {
+              if (Rewriter::rewrite(test) != nm->mkConst<bool>(false))
+              {
                 break;
               }
             }
             ++d_numUnconstrainedElim;
-            if (currentSub.isNull()) {
+            if (currentSub.isNull())
+            {
               currentSub = current;
             }
             current = parent;
@@ -425,97 +522,120 @@ void UnconstrainedSimplifier::processUnconstrained()
         {
           bool found = false;
           bool done = false;
-          for(TNode::iterator child_it = parent.begin(); child_it != parent.end(); ++child_it) {
-            if ((*child_it) == current) {
-              if (found) {
+
+          for (TNode child : parent)
+          {
+            if (child == current)
+            {
+              if (found)
+              {
                 done = true;
                 break;
               }
               found = true;
               continue;
             }
-            else if (d_unconstrained.find(*child_it) != d_unconstrained.end()) {
-              continue;
-            }
-            else {
-              NodeManager* nm = NodeManager::currentNM();
-              Node extractOp = nm->mkConst<BitVectorExtract>(BitVectorExtract(0,0));
+            else if (d_unconstrained.find(child) == d_unconstrained.end())
+            {
+              Node extractOp =
+                  nm->mkConst<BitVectorExtract>(BitVectorExtract(0, 0));
               vector<Node> children;
-              children.push_back(*child_it);
+              children.push_back(child);
               Node test = nm->mkNode(extractOp, children);
-              BitVector one(1,unsigned(1));
+              BitVector one(1, unsigned(1));
               test = test.eqNode(nm->mkConst<BitVector>(one));
-              if (Rewriter::rewrite(test) != nm->mkConst<bool>(true)) {
+              if (Rewriter::rewrite(test) != nm->mkConst<bool>(true))
+              {
                 done = true;
                 break;
               }
             }
           }
-          if (done) {
+          if (done)
+          {
             break;
           }
           checkParent = true;
           break;
         }
 
-        // Uninterpreted function - if domain is infinite, no quantifiers are used, and any child is unconstrained, result is unconstrained
+        // Uninterpreted function - if domain is infinite, no quantifiers are
+        // used, and any child is unconstrained, result is unconstrained
         case kind::APPLY_UF:
-          if (d_logicInfo.isQuantified() || !current.getType().getCardinality().isInfinite()) {
+          if (d_logicInfo.isQuantified()
+              || !current.getType().getCardinality().isInfinite())
+          {
             break;
           }
-          if (d_unconstrained.find(parent) == d_unconstrained.end() &&
-              !d_substitutions.hasSubstitution(parent)) {
+          if (d_unconstrained.find(parent) == d_unconstrained.end()
+              && !d_substitutions.hasSubstitution(parent))
+          {
             ++d_numUnconstrainedElim;
-            if (currentSub.isNull()) {
+            if (currentSub.isNull())
+            {
               currentSub = current;
             }
-            if (parent.getType() != current.getType()) {
+            if (parent.getType() != current.getType())
+            {
               currentSub = newUnconstrainedVar(parent.getType(), currentSub);
             }
             current = parent;
           }
-          else {
+          else
+          {
             currentSub = Node();
           }
           break;
 
         // Array select - if array is unconstrained, so is result
         case kind::SELECT:
-          if (parent[0] == current) {
+          if (parent[0] == current)
+          {
             ++d_numUnconstrainedElim;
             Assert(current.getType().isArray());
-            if (currentSub.isNull()) {
+            if (currentSub.isNull())
+            {
               currentSub = current;
             }
-            currentSub = newUnconstrainedVar(current.getType().getArrayConstituentType(), currentSub);
+            currentSub = newUnconstrainedVar(
+                current.getType().getArrayConstituentType(), currentSub);
             current = parent;
           }
           break;
 
-        // Array store - if both store and value are unconstrained, so is resulting store
+        // Array store - if both store and value are unconstrained, so is
+        // resulting store
         case kind::STORE:
-          if (((parent[0] == current &&
-                d_unconstrained.find(parent[2]) != d_unconstrained.end()) ||
-               (parent[2] == current &&
-                d_unconstrained.find(parent[0]) != d_unconstrained.end()))) {
-            if (d_unconstrained.find(parent) == d_unconstrained.end() &&
-                !d_substitutions.hasSubstitution(parent)) {
+          if (((parent[0] == current
+                && d_unconstrained.find(parent[2]) != d_unconstrained.end())
+               || (parent[2] == current
+                   && d_unconstrained.find(parent[0])
+                          != d_unconstrained.end())))
+          {
+            if (d_unconstrained.find(parent) == d_unconstrained.end()
+                && !d_substitutions.hasSubstitution(parent))
+            {
               ++d_numUnconstrainedElim;
-              if (parent[0] != current) {
-                if (parent[0].isVar()) {
+              if (parent[0] != current)
+              {
+                if (parent[0].isVar())
+                {
                   currentSub = parent[0];
                 }
-                else {
+                else
+                {
                   Assert(d_substitutions.hasSubstitution(parent[0]));
                   currentSub = d_substitutions.apply(parent[0]);
                 }
               }
-              else if (currentSub.isNull()) {
+              else if (currentSub.isNull())
+              {
                 currentSub = current;
               }
               current = parent;
             }
-            else {
+            else
+            {
               currentSub = Node();
             }
           }
@@ -531,24 +651,19 @@ void UnconstrainedSimplifier::processUnconstrained()
         case kind::BITVECTOR_SLT:
         case kind::BITVECTOR_SGE:
         case kind::BITVECTOR_SGT:
-        case kind::BITVECTOR_SLE: {
+        case kind::BITVECTOR_SLE:
+        {
           // Tuples over (signed, swap, strict).
-          switch (parent.getKind()) {
-            case kind::BITVECTOR_UGE:
-              break;
-            case kind::BITVECTOR_ULT:
-              strict = true;
-              break;
-            case kind::BITVECTOR_ULE:
-              swap = true;
-              break;
+          switch (parent.getKind())
+          {
+            case kind::BITVECTOR_UGE: break;
+            case kind::BITVECTOR_ULT: strict = true; break;
+            case kind::BITVECTOR_ULE: swap = true; break;
             case kind::BITVECTOR_UGT:
               swap = true;
               strict = true;
               break;
-            case kind::BITVECTOR_SGE:
-              isSigned = true;
-              break;
+            case kind::BITVECTOR_SGE: isSigned = true; break;
             case kind::BITVECTOR_SLT:
               isSigned = true;
               strict = true;
@@ -562,54 +677,62 @@ void UnconstrainedSimplifier::processUnconstrained()
               swap = true;
               strict = true;
               break;
-            default:
-              Unreachable();
+            default: Unreachable();
           }
           TNode other;
           bool left = false;
-          if (parent[0] == current) {
+          if (parent[0] == current)
+          {
             other = parent[1];
             left = true;
-          } else {
+          }
+          else
+          {
             Assert(parent[1] == current);
             other = parent[0];
           }
-          if (d_unconstrained.find(other) != d_unconstrained.end()) {
-            if (d_unconstrained.find(parent) == d_unconstrained.end() &&
-                !d_substitutions.hasSubstitution(parent)) {
+          if (d_unconstrained.find(other) != d_unconstrained.end())
+          {
+            if (d_unconstrained.find(parent) == d_unconstrained.end()
+                && !d_substitutions.hasSubstitution(parent))
+            {
               ++d_numUnconstrainedElim;
-              if (currentSub.isNull()) {
+              if (currentSub.isNull())
+              {
                 currentSub = current;
               }
               currentSub = newUnconstrainedVar(parent.getType(), currentSub);
               current = parent;
-            } else {
+            }
+            else
+            {
               currentSub = Node();
             }
-          } else {
+          }
+          else
+          {
             unsigned size = current.getType().getBitVectorSize();
             BitVector bv =
                 isSigned ? BitVector(size, Integer(1).multiplyByPow2(size - 1))
                          : BitVector(size, unsigned(0));
-            if (swap == left) {
+            if (swap == left)
+            {
               bv = ~bv;
             }
-            if (currentSub.isNull()) {
+            if (currentSub.isNull())
+            {
               currentSub = current;
             }
             currentSub = newUnconstrainedVar(parent.getType(), currentSub);
             current = parent;
-            NodeManager* nm = NodeManager::currentNM();
             Node test =
                 Rewriter::rewrite(other.eqNode(nm->mkConst<BitVector>(bv)));
-            if (test == nm->mkConst<bool>(false)) {
+            if (test == nm->mkConst<bool>(false))
+            {
               break;
             }
-            if (strict) {
-              currentSub = currentSub.andNode(test.notNode());
-            } else {
-              currentSub = currentSub.orNode(test);
-            }
+            currentSub = strict ? currentSub.andNode(test.notNode())
+                                : currentSub.orNode(test);
             // Delay adding this substitution - see comment at end of function
             delayQueueLeft.push_back(current);
             delayQueueRight.push_back(currentSub);
@@ -619,40 +742,46 @@ void UnconstrainedSimplifier::processUnconstrained()
           break;
         }
 
-        // Do nothing 
+        // Do nothing
         case kind::BITVECTOR_SIGN_EXTEND:
         case kind::BITVECTOR_ZERO_EXTEND:
         case kind::BITVECTOR_REPEAT:
         case kind::BITVECTOR_ROTATE_LEFT:
         case kind::BITVECTOR_ROTATE_RIGHT:
 
-        default:
-          break;
+        default: break;
       }
-      if( checkParent ){
-        //run for various cases from above
-        if (d_unconstrained.find(parent) == d_unconstrained.end() &&
-            !d_substitutions.hasSubstitution(parent)) {
+      if (checkParent)
+      {
+        // run for various cases from above
+        if (d_unconstrained.find(parent) == d_unconstrained.end()
+            && !d_substitutions.hasSubstitution(parent))
+        {
           ++d_numUnconstrainedElim;
-          if (currentSub.isNull()) {
+          if (currentSub.isNull())
+          {
             currentSub = current;
           }
           current = parent;
         }
-        else {
+        else
+        {
           currentSub = Node();
         }
       }
-      if (current == parent && d_visited[parent] == 1) {
+      if (current == parent && d_visited[parent] == 1)
+      {
         d_unconstrained.insert(parent);
         continue;
       }
     }
-    if (!currentSub.isNull()) {
+    if (!currentSub.isNull())
+    {
       Assert(currentSub.isVar());
       d_substitutions.addSubstitution(current, currentSub, false);
     }
-    if (workList.empty()) {
+    if (workList.empty())
+    {
       break;
     }
     current = workList.back();
@@ -666,9 +795,11 @@ void UnconstrainedSimplifier::processUnconstrained()
   // substitution very quickly (never invalidating the substitution cache).
   // Bitvector comparisons are more complicated and may require
   // back-substitution and cache-invalidation.  So we do these last.
-  while (!delayQueueLeft.empty()) {
+  while (!delayQueueLeft.empty())
+  {
     left = delayQueueLeft.back();
-    if (!d_substitutions.hasSubstitution(left)) {
+    if (!d_substitutions.hasSubstitution(left))
+    {
       right = d_substitutions.apply(delayQueueRight.back());
       d_substitutions.addSubstitution(delayQueueLeft.back(), right);
     }
@@ -677,21 +808,27 @@ void UnconstrainedSimplifier::processUnconstrained()
   }
 }
 
-
-void UnconstrainedSimplifier::processAssertions(vector<Node>& assertions)
+PreprocessingPassResult UnconstrainedSimplifier::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
 {
+  d_preprocContext->spendResource(options::preprocessStep());
+
+  std::vector<Node>& assertions = assertionsToPreprocess->ref();
+
   d_context->push();
 
-  vector<Node>::iterator it = assertions.begin(), iend = assertions.end();
-  for (; it != iend; ++it) {
-    visitAll(*it);
+  for (const Node& assertion : assertions)
+  {
+    visitAll(assertion);
   }
 
-  if (!d_unconstrained.empty()) {
+  if (!d_unconstrained.empty())
+  {
     processUnconstrained();
     //    d_substitutions.print(Message.getStream());
-    for (it = assertions.begin(); it != iend; ++it) {
-      (*it) = Rewriter::rewrite(d_substitutions.apply(*it));
+    for (Node& assertion : assertions)
+    {
+      assertion = Rewriter::rewrite(d_substitutions.apply(assertion));
     }
   }
 
@@ -701,4 +838,10 @@ void UnconstrainedSimplifier::processAssertions(vector<Node>& assertions)
   d_visited.clear();
   d_visitedOnce.clear();
   d_unconstrained.clear();
+
+  return PreprocessingPassResult::NO_CONFLICT;
 }
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/theory/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h
index b13311e2a..658834ee3 100644
--- a/src/theory/unconstrained_simplifier.h
+++ b/src/preprocessing/passes/unconstrained_simplifier.h
@@ -11,37 +11,48 @@
  **
  ** \brief Simplifications based on unconstrained variables
  **
- ** This module implements a preprocessing phase which replaces certain "unconstrained" expressions
- ** by variables.  Based on Roberto Bruttomesso's PhD thesis.
+ ** This module implements a preprocessing phase which replaces certain
+ ** "unconstrained" expressions by variables.  Based on Roberto
+ ** Bruttomesso's PhD thesis.
  **/
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__UNCONSTRAINED_SIMPLIFIER_H
-#define __CVC4__UNCONSTRAINED_SIMPLIFIER_H
+#ifndef __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H
+#define __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H
 
 #include <unordered_map>
 #include <unordered_set>
-#include <utility>
 #include <vector>
 
+#include "context/context.h"
 #include "expr/node.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "theory/logic_info.h"
 #include "theory/substitutions.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+namespace preprocessing {
+namespace passes {
 
-/* Forward Declarations */
-class LogicInfo;
+class UnconstrainedSimplifier : public PreprocessingPass
+{
+ public:
+  UnconstrainedSimplifier(PreprocessingPassContext* preprocContext);
+  ~UnconstrainedSimplifier() override;
 
-class UnconstrainedSimplifier {
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
 
+ private:
   /** number of expressions eliminated due to unconstrained simplification */
   IntStat d_numUnconstrainedElim;
 
-  typedef std::unordered_map<TNode, unsigned, TNodeHashFunction> TNodeCountMap;
-  typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeMap;
-  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
+  using TNodeCountMap = std::unordered_map<TNode, unsigned, TNodeHashFunction>;
+  using TNodeMap = std::unordered_map<TNode, TNode, TNodeHashFunction>;
+  using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>;
 
   TNodeCountMap d_visited;
   TNodeMap d_visitedOnce;
@@ -55,13 +66,10 @@ class UnconstrainedSimplifier {
   void visitAll(TNode assertion);
   Node newUnconstrainedVar(TypeNode t, TNode var);
   void processUnconstrained();
-
-public:
-  UnconstrainedSimplifier(context::Context* context, const LogicInfo& logicInfo);
-  ~UnconstrainedSimplifier();
-  void processAssertions(std::vector<Node>& assertions);
 };
 
-}
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
 
 #endif
diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
index 97fa32d17..4143f2d4b 100644
--- a/src/preprocessing/preprocessing_pass.h
+++ b/src/preprocessing/preprocessing_pass.h
@@ -39,6 +39,7 @@
 #include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/term_formula_removal.h"
+#include "theory/logic_info.h"
 #include "theory/substitutions.h"
 
 namespace CVC4 {
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index a289752fa..96e554680 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -43,6 +43,7 @@ class PreprocessingPassContext
   DecisionEngine* getDecisionEngine() { return d_smt->d_decisionEngine; }
   prop::PropEngine* getPropEngine() { return d_smt->d_propEngine; }
   context::Context* getUserContext() { return d_smt->d_userContext; }
+  context::Context* getDecisionContext() { return d_smt->d_context; }
   RemoveTermFormulas* getIteRemover() { return d_iteRemover; }
 
   void spendResource(unsigned amount)
@@ -50,6 +51,8 @@ class PreprocessingPassContext
     d_resourceManager->spendResource(amount);
   }
 
+  const LogicInfo& getLogicInfo() { return d_smt->d_logic; }
+
   /* Widen the logic to include the given theory. */
   void widenLogic(theory::TheoryId id);
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0497c2814..02e9892e2 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -97,6 +97,7 @@
 #include "preprocessing/passes/symmetry_breaker.h"
 #include "preprocessing/passes/symmetry_detect.h"
 #include "preprocessing/passes/synth_rew_rules.h"
+#include "preprocessing/passes/unconstrained_simplifier.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "preprocessing/preprocessing_pass_registry.h"
@@ -204,8 +205,6 @@ struct SmtEngineStatistics {
   IntStat d_numMiplibAssertionsRemoved;
   /** number of constant propagations found during nonclausal simp */
   IntStat d_numConstantProps;
-  /** time spent in simplifying ITEs */
-  TimerStat d_unconstrainedSimpTime;
   /** time spent in theory preprocessing */
   TimerStat d_theoryPreprocessTime;
   /** time spent converting to CNF */
@@ -238,7 +237,6 @@ struct SmtEngineStatistics {
     d_miplibPassTime("smt::SmtEngine::miplibPassTime"),
     d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0),
     d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
-    d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
     d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
     d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
     d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
@@ -257,7 +255,6 @@ struct SmtEngineStatistics {
     smtStatisticsRegistry()->registerStat(&d_miplibPassTime);
     smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved);
     smtStatisticsRegistry()->registerStat(&d_numConstantProps);
-    smtStatisticsRegistry()->registerStat(&d_unconstrainedSimpTime);
     smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime);
     smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
     smtStatisticsRegistry()->registerStat(&d_numAssertionsPre);
@@ -278,7 +275,6 @@ struct SmtEngineStatistics {
     smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime);
     smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved);
     smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
-    smtStatisticsRegistry()->unregisterStat(&d_unconstrainedSimpTime);
     smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime);
     smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
     smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre);
@@ -580,9 +576,6 @@ class SmtEnginePrivate : public NodeManagerListener {
    */
   bool checkForBadSkolems(TNode n, TNode skolem, NodeToBoolHashMap& cache);
 
-  // Simplify based on unconstrained values
-  void unconstrainedSimp();
-
   /**
    * Trace nodes back to their assertions using CircuitPropagator's
    * BackEdgesMap.
@@ -2676,6 +2669,8 @@ void SmtEnginePrivate::finishInit()
       new SynthRewRulesPass(d_preprocessingPassContext.get()));
   std::unique_ptr<SepSkolemEmp> sepSkolemEmp(
       new SepSkolemEmp(d_preprocessingPassContext.get()));
+  std::unique_ptr<UnconstrainedSimplifier> unconstrainedSimplifier(
+      new UnconstrainedSimplifier(d_preprocessingPassContext.get()));
   d_preprocessingPassRegistry.registerPass("apply-substs",
                                            std::move(applySubsts));
   d_preprocessingPassRegistry.registerPass("apply-to-const",
@@ -2720,6 +2715,8 @@ void SmtEnginePrivate::finishInit()
   d_preprocessingPassRegistry.registerPass("synth-rr", std::move(srrProc));
   d_preprocessingPassRegistry.registerPass("quantifier-macros",
                                            std::move(quantifierMacros));
+  d_preprocessingPassRegistry.registerPass("unconstrained-simplifier",
+                                           std::move(unconstrainedSimplifier));
 }
 
 Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
@@ -3255,13 +3252,6 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   return true;
 }
 
-void SmtEnginePrivate::unconstrainedSimp() {
-  TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime);
-  spendResource(options::preprocessStep());
-  Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl;
-  d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref());
-}
-
 void SmtEnginePrivate::traceBackToAssertions(const std::vector<Node>& nodes, std::vector<TNode>& assertions) {
   const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges();
   for(vector<Node>::const_iterator i = nodes.begin(); i != nodes.end(); ++i) {
@@ -3745,14 +3735,10 @@ bool SmtEnginePrivate::simplifyAssertions()
 
     // Unconstrained simplification
     if(options::unconstrainedSimp()) {
-      Chat() << "...doing unconstrained simplification..." << endl;
-      unconstrainedSimp();
+      d_preprocessingPassRegistry.getPass("unconstrained-simplifier")
+          ->apply(&d_assertions);
     }
 
-    dumpAssertions("post-unconstrained", d_assertions);
-    Trace("smt") << "POST unconstrainedSimp" << endl;
-    Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
-
     if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
       Chat() << "...doing another round of nonclausal simplification..." << endl;
       Trace("simplify") << "SmtEnginePrivate::simplify(): "
@@ -4027,12 +4013,9 @@ void SmtEnginePrivate::processAssertions() {
 
   // Unconstrained simplification
   if(options::unconstrainedSimp()) {
-    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl;
-    dumpAssertions("pre-unconstrained-simp", d_assertions);
     d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions);
-    unconstrainedSimp();
-    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl;
-    dumpAssertions("post-unconstrained-simp", d_assertions);
+    d_preprocessingPassRegistry.getPass("unconstrained-simplifier")
+        ->apply(&d_assertions);
   }
 
   if(options::bvIntroducePow2())
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index c87a4be02..d75f7843d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -49,7 +49,6 @@
 #include "theory/theory_model.h"
 #include "theory/theory_traits.h"
 #include "theory/uf/equality_engine.h"
-#include "theory/unconstrained_simplifier.h"
 #include "util/resource_manager.h"
 
 using namespace std;
@@ -315,7 +314,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_factsAsserted(context, false),
   d_preRegistrationVisitor(this, context),
   d_sharedTermsVisitor(d_sharedTerms),
-  d_unconstrainedSimp(new UnconstrainedSimplifier(context, logicInfo)),
   d_theoryAlternatives(),
   d_attr_handle(),
   d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
@@ -360,9 +358,6 @@ TheoryEngine::~TheoryEngine() {
   delete d_masterEqualityEngine;
 
   smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
-
-  delete d_unconstrainedSimp;
-
   smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
 }
 
@@ -2146,11 +2141,6 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
     });
 }
 
-void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions)
-{
-  d_unconstrainedSimp->processAssertions(assertions);
-}
-
 void TheoryEngine::setUserAttribute(const std::string& attr,
                                     Node n,
                                     const std::vector<Node>& node_values,
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 71a0234ed..65402f0a6 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -99,7 +99,6 @@ namespace theory {
 
 class DecisionEngine;
 class RemoveTermFormulas;
-class UnconstrainedSimplifier;
 
 /**
  * This is essentially an abstraction for a collection of theories.  A
@@ -827,9 +826,6 @@ private:
   /** Dump the assertions to the dump */
   void dumpAssertions(const char* tag);
 
-  /** For preprocessing pass simplifying unconstrained expressions */
-  UnconstrainedSimplifier* d_unconstrainedSimp;
-
   /** For preprocessing pass lifting bit-vectors of size 1 to booleans */
 public:
   void staticInitializeBVOptions(const std::vector<Node>& assertions);
@@ -838,8 +834,6 @@ public:
   /** Returns false if an assertion simplified to false. */
   bool donePPSimpITE(std::vector<Node>& assertions);
 
-  void ppUnconstrainedSimp(std::vector<Node>& assertions);
-
   SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; }
 
   theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }