Merge branch 'master' into rmCoverityrmCoverity

38 files changed, 1281 insertions, 936 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 3b8a12fa5..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 \
@@ -85,14 +89,14 @@ libcvc4_la_SOURCES = \
 	preprocessing/passes/ite_removal.h \
 	preprocessing/passes/ite_simp.cpp \
 	preprocessing/passes/ite_simp.h \
+	preprocessing/passes/nl_ext_purify.cpp \
+	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 \
+	preprocessing/passes/quantifier_macros.h \
 	preprocessing/passes/real_to_int.cpp \
 	preprocessing/passes/real_to_int.h \
 	preprocessing/passes/rewrite.cpp \
@@ -111,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 \
@@ -240,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 \
@@ -480,8 +484,6 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/lazy_trie.h \
 	theory/quantifiers/local_theory_ext.cpp \
 	theory/quantifiers/local_theory_ext.h \
-	theory/quantifiers/macros.cpp \
-	theory/quantifiers/macros.h \
 	theory/quantifiers/quant_conflict_find.cpp \
 	theory/quantifiers/quant_conflict_find.h \
 	theory/quantifiers/quant_epr.cpp \
diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp
new file mode 100644
index 000000000..afb092571
--- /dev/null
+++ b/src/preprocessing/passes/nl_ext_purify.cpp
@@ -0,0 +1,130 @@
+/*********************                                                        */
+/*! \file nl_ext_purify.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The NlExtPurify preprocessing pass
+ **
+ ** Purifies non-linear terms
+ **/
+
+#include "preprocessing/passes/nl_ext_purify.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+
+Node NlExtPurify::purifyNlTerms(TNode n,
+                                NodeMap& cache,
+                                NodeMap& bcache,
+                                std::vector<Node>& var_eq,
+                                bool beneathMult)
+{
+  if (beneathMult)
+  {
+    NodeMap::iterator find = bcache.find(n);
+    if (find != bcache.end())
+    {
+      return (*find).second;
+    }
+  }
+  else
+  {
+    NodeMap::iterator find = cache.find(n);
+    if (find != cache.end())
+    {
+      return (*find).second;
+    }
+  }
+  Node ret = n;
+  if (n.getNumChildren() > 0)
+  {
+    if (beneathMult
+        && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS))
+    {
+      // don't do it if it rewrites to a constant
+      Node nr = Rewriter::rewrite(n);
+      if (nr.isConst())
+      {
+        // return the rewritten constant
+        ret = nr;
+      }
+      else
+      {
+        // new variable
+        ret = NodeManager::currentNM()->mkSkolem(
+            "__purifyNl_var",
+            n.getType(),
+            "Variable introduced in purifyNl pass");
+        Node np = purifyNlTerms(n, cache, bcache, var_eq, false);
+        var_eq.push_back(np.eqNode(ret));
+        Trace("nl-ext-purify") << "Purify : " << ret << " -> " << np
+                               << std::endl;
+      }
+    }
+    else
+    {
+      bool beneathMultNew = beneathMult || n.getKind() == kind::MULT;
+      bool childChanged = false;
+      std::vector<Node> children;
+      for (unsigned i = 0, size = n.getNumChildren(); i < size; ++i)
+      {
+        Node nc = purifyNlTerms(n[i], cache, bcache, var_eq, beneathMultNew);
+        childChanged = childChanged || nc != n[i];
+        children.push_back(nc);
+      }
+      if (childChanged)
+      {
+        ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
+      }
+    }
+  }
+  if (beneathMult)
+  {
+    bcache[n] = ret;
+  }
+  else
+  {
+    cache[n] = ret;
+  }
+  return ret;
+}
+
+NlExtPurify::NlExtPurify(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "nl-ext-purify"){};
+
+PreprocessingPassResult NlExtPurify::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  unordered_map<Node, Node, NodeHashFunction> cache;
+  unordered_map<Node, Node, NodeHashFunction> bcache;
+  std::vector<Node> var_eq;
+  unsigned size = assertionsToPreprocess->size();
+  for (unsigned i = 0; i < size; ++i)
+  {
+    Node a = (*assertionsToPreprocess)[i];
+    assertionsToPreprocess->replace(i, purifyNlTerms(a, cache, bcache, var_eq));
+    Trace("nl-ext-purify") << "Purify : " << a << " -> "
+                           << (*assertionsToPreprocess)[i] << "\n";
+  }
+  if (!var_eq.empty())
+  {
+    unsigned lastIndex = size - 1;
+    var_eq.insert(var_eq.begin(), (*assertionsToPreprocess)[lastIndex]);
+    assertionsToPreprocess->replace(
+        lastIndex, NodeManager::currentNM()->mkNode(kind::AND, var_eq));
+  }
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/nl_ext_purify.h b/src/preprocessing/passes/nl_ext_purify.h
new file mode 100644
index 000000000..8d28b0742
--- /dev/null
+++ b/src/preprocessing/passes/nl_ext_purify.h
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file nl_ext_purify.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The NlExtPurify preprocessing pass
+ **
+ ** Purifies non-linear terms by replacing sums under multiplications by fresh
+ ** variables
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H
+#define __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H
+
+#include <unordered_map>
+#include <vector>
+
+#include "expr/node.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
+
+class NlExtPurify : public PreprocessingPass
+{
+ public:
+  NlExtPurify(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+  Node purifyNlTerms(TNode n,
+                     NodeMap& cache,
+                     NodeMap& bcache,
+                     std::vector<Node>& var_eq,
+                     bool beneathMult = false);
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H */
diff --git a/src/theory/quantifiers/macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index d88f8eec9..e3bc02309 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file macros.cpp
+/*! \file quantifier_macros.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Andrew Reynolds, Tim King, Kshitij Bansal
@@ -14,7 +14,7 @@
  ** This class implements quantifiers macro definitions.
  **/
 
-#include "theory/quantifiers/macros.h"
+#include "preprocessing/passes/quantifier_macros.h"
 
 #include <vector>
 
@@ -27,19 +27,48 @@
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 
-using namespace CVC4;
 using namespace std;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 using namespace CVC4::kind;
 
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
 
-QuantifierMacros::QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){
+QuantifierMacros::QuantifierMacros(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "quantifier-macros"),
+      d_ground_macros(false)
+{
+}
+
+PreprocessingPassResult QuantifierMacros::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  bool success;
+  do
+  {
+    success = simplify(assertionsToPreprocess->ref(), true);
+  } while (success);
+  finalizeDefinitions();
+  clearMaps();
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+void QuantifierMacros::clearMaps()
+{
+  d_macro_basis.clear();
+  d_macro_defs.clear();
+  d_macro_defs_new.clear();
+  d_macro_def_contains.clear();
+  d_simplify_cache.clear();
+  d_quant_macros.clear();
   d_ground_macros = false;
 }
-  
+
 bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
   unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1;
   for( unsigned r=0; r<rmax; r++ ){
@@ -72,14 +101,14 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite
           //for now, it is dependent upon all assertions involving macros, this is an over-approximation.
           //a more fine-grained unsat core computation would require caching dependencies for each subterm of the formula, 
           // which is expensive.
-          PROOF( 
-            ProofManager::currentPM()->addDependence(curr, assertions[i]); 
-            for( unsigned j=0; j<macro_assertions.size(); j++ ){
-              if( macro_assertions[j]!=assertions[i] ){
-                ProofManager::currentPM()->addDependence(curr,macro_assertions[j]);
-              }
-            }
-          );
+          PROOF(ProofManager::currentPM()->addDependence(curr, assertions[i]);
+                for (unsigned j = 0; j < macro_assertions.size(); j++) {
+                  if (macro_assertions[j] != assertions[i])
+                  {
+                    ProofManager::currentPM()->addDependence(
+                        curr, macro_assertions[j]);
+                  }
+                });
           assertions[i] = curr;
           retVal = true;
         }
@@ -154,7 +183,10 @@ bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
 }
 
 bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
-  Node icn = d_qe->getTermUtil()->substituteBoundVariablesToInstConstants(n, f);
+  Node icn = d_preprocContext->getTheoryEngine()
+                 ->getQuantifiersEngine()
+                 ->getTermUtil()
+                 ->substituteBoundVariablesToInstConstants(n, f);
   Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
   std::vector< Node > var;
   quantifiers::TermUtil::computeInstConstContainsForQuant(f, icn, var);
@@ -512,3 +544,7 @@ void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) {
     }
   }
 }
+
+}  // passes
+}  // preprocessing
+}  // CVC4
diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h
new file mode 100644
index 000000000..092a62942
--- /dev/null
+++ b/src/preprocessing/passes/quantifier_macros.h
@@ -0,0 +1,89 @@
+/*********************                                                        */
+/*! \file quantifier_macros.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Pre-process step for detecting quantifier macro definitions
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
+#define __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
+
+#include <map>
+#include <string>
+#include <vector>
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class QuantifierMacros : public PreprocessingPass
+{
+ public:
+  QuantifierMacros(PreprocessingPassContext* preprocContext);
+  ~QuantifierMacros() {}
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+  bool processAssertion(Node n);
+  bool isBoundVarApplyUf(Node n);
+  bool process(Node n, bool pol, std::vector<Node>& args, Node f);
+  bool containsBadOp(Node n,
+                     Node op,
+                     std::vector<Node>& opc,
+                     std::map<Node, bool>& visited);
+  bool isMacroLiteral(Node n, bool pol);
+  bool isGroundUfTerm(Node f, Node n);
+  void getMacroCandidates(Node n,
+                          std::vector<Node>& candidates,
+                          std::map<Node, bool>& visited);
+  Node solveInEquality(Node n, Node lit);
+  bool getFreeVariables(Node n,
+                        std::vector<Node>& v_quant,
+                        std::vector<Node>& vars,
+                        bool retOnly,
+                        std::map<Node, bool>& visited);
+  bool getSubstitution(std::vector<Node>& v_quant,
+                       std::map<Node, Node>& solved,
+                       std::vector<Node>& vars,
+                       std::vector<Node>& subs,
+                       bool reqComplete);
+  void addMacro(Node op, Node n, std::vector<Node>& opc);
+  void debugMacroDefinition(Node oo, Node n);
+  bool simplify(std::vector<Node>& assertions, bool doRewrite = false);
+  Node simplify(Node n);
+  void finalizeDefinitions();
+  void clearMaps();
+
+  // map from operators to macro basis terms
+  std::map<Node, std::vector<Node> > d_macro_basis;
+  // map from operators to macro definition
+  std::map<Node, Node> d_macro_defs;
+  std::map<Node, Node> d_macro_defs_new;
+  // operators to macro ops that contain them
+  std::map<Node, std::vector<Node> > d_macro_def_contains;
+  // simplify caches
+  std::map<Node, Node> d_simplify_cache;
+  std::map<Node, bool> d_quant_macros;
+  bool d_ground_macros;
+};
+
+}  // passes
+}  // preprocessing
+}  // CVC4
+
+#endif /*__CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */
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 c4492d3a1..02e9892e2 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -83,7 +83,10 @@
 #include "preprocessing/passes/int_to_bv.h"
 #include "preprocessing/passes/ite_removal.h"
 #include "preprocessing/passes/ite_simp.h"
+#include "preprocessing/passes/nl_ext_purify.h"
 #include "preprocessing/passes/pseudo_boolean_processor.h"
+#include "preprocessing/passes/quantifier_macros.h"
+#include "preprocessing/passes/quantifier_macros.h"
 #include "preprocessing/passes/quantifiers_preprocess.h"
 #include "preprocessing/passes/real_to_int.h"
 #include "preprocessing/passes/rewrite.h"
@@ -94,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"
@@ -117,7 +121,6 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/logic_info.h"
 #include "theory/quantifiers/fun_def_process.h"
-#include "theory/quantifiers/macros.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/single_inv_partition.h"
 #include "theory/quantifiers/sygus/ce_guided_instantiation.h"
@@ -202,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 */
@@ -236,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),
@@ -255,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);
@@ -276,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);
@@ -567,14 +565,6 @@ class SmtEnginePrivate : public NodeManagerListener {
   bool nonClausalSimplify();
 
   /**
-   * Performs static learning on the assertions.
-   */
-  void staticLearning();
-
-  Node realToInt(TNode n, NodeToNodeHashMap& cache, std::vector< Node >& var_eq);
-  Node purifyNlTerms(TNode n, NodeToNodeHashMap& cache, NodeToNodeHashMap& bcache, std::vector< Node >& var_eq, bool beneathMult = false);
-
-  /**
    * Helper function to fix up assertion list to restore invariants needed after
    * ite removal.
    */
@@ -586,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.
@@ -790,7 +777,7 @@ class SmtEnginePrivate : public NodeManagerListener {
   /** Process a user push.
   */
   void notifyPush() {
-  
+
   }
 
   /**
@@ -872,13 +859,13 @@ class SmtEnginePrivate : public NodeManagerListener {
   std::ostream* getReplayLog() const {
     return d_managedReplayLog.getReplayLog();
   }
-  
+
   //------------------------------- expression names
   // implements setExpressionName, as described in smt_engine.h
   void setExpressionName(Expr e, std::string name) {
     d_exprNames[Node::fromExpr(e)] = name;
   }
-  
+
   // implements getExpressionName, as described in smt_engine.h
   bool getExpressionName(Expr e, std::string& name) const {
     context::CDHashMap< Node, std::string, NodeHashFunction >::const_iterator it = d_exprNames.find(e);
@@ -2026,7 +2013,6 @@ void SmtEngine::setDefaults() {
     }
     if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV))
     {
-      options::cbqiAll.set( false );
       if( !options::quantConflictFind.wasSetByUser() ){
         options::quantConflictFind.set( false );
       }
@@ -2658,6 +2644,8 @@ void SmtEnginePrivate::finishInit()
       new IntToBV(d_preprocessingPassContext.get()));
   std::unique_ptr<ITESimp> iteSimp(
       new ITESimp(d_preprocessingPassContext.get()));
+  std::unique_ptr<NlExtPurify> nlExtPurify(
+      new NlExtPurify(d_preprocessingPassContext.get()));
   std::unique_ptr<QuantifiersPreprocess> quantifiersPreprocess(
       new QuantifiersPreprocess(d_preprocessingPassContext.get()));
   std::unique_ptr<PseudoBooleanProcessor> pbProc(
@@ -2681,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",
@@ -2692,6 +2682,8 @@ void SmtEnginePrivate::finishInit()
                                            std::move(bvAckermann));
   d_preprocessingPassRegistry.registerPass("bv-eager-atoms",
                                            std::move(bvEagerAtoms));
+  std::unique_ptr<QuantifierMacros> quantifierMacros(
+      new QuantifierMacros(d_preprocessingPassContext.get()));
   d_preprocessingPassRegistry.registerPass("bv-gauss", std::move(bvGauss));
   d_preprocessingPassRegistry.registerPass("bv-intro-pow2",
                                            std::move(bvIntroPow2));
@@ -2701,6 +2693,8 @@ void SmtEnginePrivate::finishInit()
                                            std::move(globalNegate));
   d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
   d_preprocessingPassRegistry.registerPass("ite-simp", std::move(iteSimp));
+  d_preprocessingPassRegistry.registerPass("nl-ext-purify",
+                                           std::move(nlExtPurify));
   d_preprocessingPassRegistry.registerPass("quantifiers-preprocess",
                                            std::move(quantifiersPreprocess));
   d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor",
@@ -2713,12 +2707,16 @@ void SmtEnginePrivate::finishInit()
                                            std::move(sepSkolemEmp));
   d_preprocessingPassRegistry.registerPass("sort-inference",
                                            std::move(sortInfer));
-  d_preprocessingPassRegistry.registerPass("static-learning", 
+  d_preprocessingPassRegistry.registerPass("static-learning",
                                            std::move(staticLearning));
   d_preprocessingPassRegistry.registerPass("sygus-infer",
                                            std::move(sygusInfer));
   d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc));
   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)
@@ -2904,68 +2902,6 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
   return result.top();
 }
 
-typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
-
-Node SmtEnginePrivate::purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache, std::vector< Node >& var_eq, bool beneathMult) {
-  if( beneathMult ){
-    NodeMap::iterator find = bcache.find(n);
-    if (find != bcache.end()) {
-      return (*find).second;
-    }
-  }else{
-    NodeMap::iterator find = cache.find(n);
-    if (find != cache.end()) {
-      return (*find).second;
-    }
-  }
-  Node ret = n;
-  if( n.getNumChildren()>0 ){
-    if (beneathMult
-        && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS))
-    {
-      // don't do it if it rewrites to a constant
-      Node nr = Rewriter::rewrite(n);
-      if (nr.isConst())
-      {
-        // return the rewritten constant
-        ret = nr;
-      }
-      else
-      {
-        // new variable
-        ret = NodeManager::currentNM()->mkSkolem(
-            "__purifyNl_var",
-            n.getType(),
-            "Variable introduced in purifyNl pass");
-        Node np = purifyNlTerms(n, cache, bcache, var_eq, false);
-        var_eq.push_back(np.eqNode(ret));
-        Trace("nl-ext-purify")
-            << "Purify : " << ret << " -> " << np << std::endl;
-      }
-    }
-    else
-    {
-      bool beneathMultNew = beneathMult || n.getKind()==kind::MULT;
-      bool childChanged = false;
-      std::vector< Node > children;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        Node nc = purifyNlTerms( n[i], cache, bcache, var_eq, beneathMultNew );
-        childChanged = childChanged || nc!=n[i];
-        children.push_back( nc );
-      }
-      if( childChanged ){
-        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
-      }
-    }
-  }
-  if( beneathMult ){
-    bcache[n] = ret;
-  }else{
-    cache[n] = ret;
-  }
-  return ret;
-}
-
 // do dumping (before/after any preprocessing pass)
 static void dumpAssertions(const char* key,
                            const AssertionPipeline& assertionList) {
@@ -3316,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) {
@@ -3806,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(): "
@@ -4038,20 +3963,7 @@ void SmtEnginePrivate::processAssertions() {
   }
 
   if( options::nlExtPurify() ){
-    unordered_map<Node, Node, NodeHashFunction> cache;
-    unordered_map<Node, Node, NodeHashFunction> bcache;
-    std::vector< Node > var_eq;
-    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-      Node a = d_assertions[i];
-      d_assertions.replace(i, purifyNlTerms(a, cache, bcache, var_eq));
-      Trace("nl-ext-purify")
-          << "Purify : " << a << " -> " << d_assertions[i] << std::endl;
-    }
-    if( !var_eq.empty() ){
-      unsigned lastIndex = d_assertions.size()-1;
-      var_eq.insert( var_eq.begin(), d_assertions[lastIndex] );
-      d_assertions.replace(lastIndex, NodeManager::currentNM()->mkNode( kind::AND, var_eq ) );
-    }
+    d_preprocessingPassRegistry.getPass("nl-ext-purify")->apply(&d_assertions);
   }
 
   if( options::ceGuidedInst() ){
@@ -4101,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())
@@ -4157,13 +4066,8 @@ void SmtEnginePrivate::processAssertions() {
     dumpAssertions("post-skolem-quant", d_assertions);
     if( options::macrosQuant() ){
       //quantifiers macro expansion
-      quantifiers::QuantifierMacros qm( d_smt.d_theoryEngine->getQuantifiersEngine() );
-      bool success;
-      do{
-        success = qm.simplify( d_assertions.ref(), true );
-      }while( success );
-      //finalize the definitions
-      qm.finalizeDefinitions();
+      d_preprocessingPassRegistry.getPass("quantifier-macros")
+          ->apply(&d_assertions);
     }
 
     //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
@@ -5528,7 +5432,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
     Assert( inst_qs.size()<=1 );
     Node ret_n;
     if( inst_qs.size()==1 ){
-      Node top_q = inst_qs[0]; 
+      Node top_q = inst_qs[0];
       //Node top_q = Rewriter::rewrite( nn_e ).negate();
       Assert( top_q.getKind()==kind::FORALL );
       Trace("smt-qe") << "Get qe for " << top_q << std::endl;
@@ -5951,7 +5855,7 @@ void SmtEngine::setReplayStream(ExprStream* replayStream) {
   AlwaysAssert(!d_fullyInited,
                "Cannot set replay stream once fully initialized");
   d_replayStream = replayStream;
-}  
+}
 
 bool SmtEngine::getExpressionName(Expr e, std::string& name) const {
   return d_private->getExpressionName(e, name);
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 65df3a642..283c70ada 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -41,24 +41,26 @@ namespace CVC4 {
 namespace theory {
 namespace datatypes {
 
-TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
-                                 Valuation valuation, const LogicInfo& logicInfo)
+TheoryDatatypes::TheoryDatatypes(Context* c,
+                                 UserContext* u,
+                                 OutputChannel& out,
+                                 Valuation valuation,
+                                 const LogicInfo& logicInfo)
     : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo),
-      //d_cycle_check(c),
-      d_hasSeenCycle(c, false),
       d_infer(c),
       d_infer_exp(c),
-      d_term_sk( u ),
-      d_notify( *this ),
+      d_term_sk(u),
+      d_notify(*this),
       d_equalityEngine(d_notify, c, "theory::datatypes", true),
-      d_labels( c ),
-      d_selector_apps( c ),
-      //d_consEqc( c ),
-      d_conflict( c, false ),
-      d_collectTermsCache( c ),
-      d_functionTerms( c ),
-      d_singleton_eq( u ),
-      d_lemmas_produced_c( u )
+      d_labels(c),
+      d_selector_apps(c),
+      d_conflict(c, false),
+      d_addedLemma(false),
+      d_addedFact(false),
+      d_collectTermsCache(c),
+      d_functionTerms(c),
+      d_singleton_eq(u),
+      d_lemmas_produced_c(u)
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
@@ -765,25 +767,6 @@ void TheoryDatatypes::conflict(TNode a, TNode b){
 void TheoryDatatypes::eqNotifyNewClass(TNode t){
   if( t.getKind()==APPLY_CONSTRUCTOR ){
     getOrMakeEqcInfo( t, true );
-    //look at all equivalence classes with constructor terms
-/*
-    for( BoolMap::const_iterator it = d_consEqc.begin(); it != d_consEqc.end(); ++it ){
-      if( (*it).second ){
-        TNode r = (*it).first;
-        if( r.getType()==t.getType() ){
-          EqcInfo * ei = getOrMakeEqcInfo( r, false );
-          if( ei && !ei->d_constructor.get().isNull() && ei->d_constructor.get().getOperator()!=t.getOperator() ){
-            Node deq = ei->d_constructor.get().eqNode( t ).negate();
-            d_pending.push_back( deq );
-            d_pending_exp[ deq ] = d_true;
-            Trace("datatypes-infer") << "DtInfer : diff constructor : " << deq << std::endl;
-            d_infer.push_back( deq );
-          }
-        }
-      }
-    }
-*/
-    //d_consEqc[t] = true;
   }
 }
 
@@ -865,14 +848,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
             if( d_conflict ){
               return;
             }
-            //d_consEqc[t1] = true;
           }
-          //AJR: do this?
-          //else if( cons2.isConst() ){
-          //  //prefer the constant
-          //  eqc1->d_constructor = cons2;
-          //}
-          //d_consEqc[t2] = false;
         }
       }else{
         Trace("datatypes-debug") << "  no eqc info for " << t1 << ", must create" << std::endl;
@@ -1998,9 +1974,6 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on,
       for( unsigned i=0; i<ncons.getNumChildren(); i++ ) {
         TNode cn = searchForCycle( ncons[i], on, visited, proc, explanation, false );
         if( cn==on ) {
-          //if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n, ncons[i] ) ){
-          //  Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << ncons[i] << "!!!!" << std::endl;
-          //}
           //add explanation for why the constructor is connected
           if( n != ncons ) {
             explainEquality( n, ncons, true, explanation );
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index e06bb7408..233ebd052 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -46,10 +46,6 @@ class TheoryDatatypes : public Theory {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
 
-  /** transitive closure to record equivalence/subterm relation.  */
-  // TransitiveClosureNode d_cycle_check;
-  /** has seen cycle */
-  context::CDO<bool> d_hasSeenCycle;
   /** inferences */
   NodeList d_infer;
   NodeList d_infer_exp;
@@ -179,12 +175,19 @@ private:
   /** selector apps for eqch equivalence class */
   NodeIntMap d_selector_apps;
   std::map< Node, std::vector< Node > > d_selector_apps_data;
-  /** constructor terms */
-  //BoolMap d_consEqc;
   /** Are we in conflict */
   context::CDO<bool> d_conflict;
-  /** Added lemma ? */
+  /** added lemma
+   *
+   * This flag is set to true during a full effort check if this theory
+   * called d_out->lemma(...).
+   */
   bool d_addedLemma;
+  /** added fact
+   *
+   * This flag is set to true during a full effort check if this theory
+   * added an internal fact to its equality engine.
+   */
   bool d_addedFact;
   /** The conflict node */
   Node d_conflictNode;
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index 83098e3ba..3cf605238 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -57,7 +57,7 @@ class CegInstantiatorBvInverterQuery : public BvInverterQuery
 };
 
 BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn)
-    : Instantiator(qe, tn)
+    : Instantiator(qe, tn), d_inst_id_counter(0)
 {
   // get the global inverter utility
   // this must be global since we need to:
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
index c281e81ca..ac76ee31f 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp
@@ -38,11 +38,14 @@ using namespace CVC4::theory::arith;
 
 #define ARITH_INSTANTIATOR_USE_MINUS_DELTA
 
-InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe )
-  : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), 
-d_elim_quants( qe->getSatContext() ),
-d_nested_qe_waitlist_size( qe->getUserContext() ),
-d_nested_qe_waitlist_proc( qe->getUserContext() )
+InstStrategyCbqi::InstStrategyCbqi(QuantifiersEngine* qe)
+    : QuantifiersModule(qe),
+      d_cbqi_set_quant_inactive(false),
+      d_incomplete_check(false),
+      d_added_cbqi_lemma(qe->getUserContext()),
+      d_elim_quants(qe->getSatContext()),
+      d_nested_qe_waitlist_size(qe->getUserContext()),
+      d_nested_qe_waitlist_proc(qe->getUserContext())
 //, d_added_inst( qe->getUserContext() )
 {
   d_qid_count = 0;
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
index 236904ef2..4334652da 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h
@@ -37,7 +37,18 @@ class InstStrategyCbqi : public QuantifiersModule {
   typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
 
  protected:
+  /** set quantified formula inactive
+   *
+   * This flag is set to true during a full effort check if at least one
+   * quantified formula is set "inactive", that is, its negation is
+   * unsatisfiable in the current context.
+   */
   bool d_cbqi_set_quant_inactive;
+  /** incomplete check
+   *
+   * This is set to true during a full effort check if this strategy could
+   * not find an instantiation for at least one asserted quantified formula.
+   */
   bool d_incomplete_check;
   /** whether we have added cbqi lemma */
   NodeSet d_added_cbqi_lemma;
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index e82ab617a..a1c132fda 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -80,16 +80,18 @@ void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >&
   }
 }
 
-
-
-ConjectureGenerator::ConjectureGenerator( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ),
-d_notify( *this ),
-d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false),
-d_ee_conjectures( c ){
-  d_fullEffortCount = 0;
-  d_conj_count = 0;
-  d_subs_confirmCount = 0;
-  d_subs_unkCount = 0;
+ConjectureGenerator::ConjectureGenerator(QuantifiersEngine* qe,
+                                         context::Context* c)
+    : QuantifiersModule(qe),
+      d_notify(*this),
+      d_uequalityEngine(d_notify, c, "ConjectureGenerator::ee", false),
+      d_ee_conjectures(c),
+      d_conj_count(0),
+      d_subs_confirmCount(0),
+      d_subs_unkCount(0),
+      d_fullEffortCount(0),
+      d_hasAddedLemma(false)
+{
   d_uequalityEngine.addFunctionKind( kind::APPLY_UF );
   d_uequalityEngine.addFunctionKind( kind::APPLY_CONSTRUCTOR );
 
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 6d626038d..a3a0b8795 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -70,10 +70,19 @@ class TermGenEnv;
 
 class TermGenerator
 {
-private:
+ private:
   unsigned calculateGeneralizationDepth( TermGenEnv * s, std::map< TypeNode, std::vector< int > >& fvs );
-public:
-  TermGenerator(){}
+
+ public:
+  TermGenerator()
+      : d_id(0),
+        d_status(0),
+        d_status_num(0),
+        d_match_status(0),
+        d_match_status_child_num(0),
+        d_match_mode(0)
+  {
+  }
   TypeNode d_typ;
   unsigned d_id;
   //1 : consider as unique variable
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 4208b11ae..6ea6e50b3 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -33,8 +33,9 @@ bool CandidateGenerator::isLegalCandidate( Node n ){
   return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(n) );
 }
 
-CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node pat ) :
-CandidateGenerator( qe ), d_term_iter( -1 ){
+CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat)
+    : CandidateGenerator(qe), d_term_iter(-1), d_term_iter_limit(0)
+{
   d_op = qe->getTermDatabase()->getMatchOperator( pat );
   Assert( !d_op.isNull() );
 }
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index a8079f775..1e3116f43 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -572,10 +572,6 @@ void FirstOrderModelIG::resetEvaluate(){
   d_eval_uf_use_default.clear();
   d_eval_uf_model.clear();
   d_eval_term_index_order.clear();
-  d_eval_formulas = 0;
-  d_eval_uf_terms = 0;
-  d_eval_lits = 0;
-  d_eval_lits_unknown = 0;
 }
 
 //if evaluate( n ) = eVal,
@@ -585,7 +581,6 @@ void FirstOrderModelIG::resetEvaluate(){
 // if eVal is not 0, then
 //   each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model
 int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
-  ++d_eval_formulas;
   Debug("fmf-eval-debug2") << "Evaluate " << n << std::endl;
   //Notice() << "Eval " << n << std::endl;
   if( n.getKind()==NOT ){
@@ -661,7 +656,6 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
   }else if( n.getKind()==FORALL ){
     return 0;
   }else{
-    ++d_eval_lits;
     //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl;
     int retVal = 0;
     depIndex = ri->getNumTerms()-1;
@@ -684,7 +678,6 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
     if( retVal!=0 ){
       Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depIndex = " << depIndex << std::endl;
     }else{
-      ++d_eval_lits_unknown;
       Trace("fmf-eval-amb") << "Neither true nor false : " << n << std::endl;
       Trace("fmf-eval-amb") << "   value : " << val << std::endl;
     }
@@ -731,7 +724,6 @@ Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri
         //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
         //if it is a defined UF, then consult the interpretation
         if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){
-          ++d_eval_uf_terms;
           int argDepIndex = 0;
           //make the term model specifically for n
           makeEvalUfModel( n );
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 059250f8d..7da5b2088 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -266,12 +266,6 @@ public:
   /** evaluate functions */
   int evaluate( Node n, int& depIndex, RepSetIterator* ri  );
   Node evaluateTerm( Node n, int& depIndex, RepSetIterator* ri  );
-public:
-  //statistics
-  int d_eval_formulas;
-  int d_eval_uf_terms;
-  int d_eval_lits;
-  int d_eval_lits_unknown;
 private:
   //default evaluate term function
   Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri  );
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index d1b7eebb8..c03fc7a32 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -457,24 +457,17 @@ bool QModelBuilderIG::hasConstantDefinition( Node n ){
   return false;
 }
 
-QModelBuilderIG::Statistics::Statistics():
-  d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
-  d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0),
-  d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0 ),
-  d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0 ),
-  d_eval_formulas("QModelBuilderIG::Eval_Formulas", 0 ),
-  d_eval_uf_terms("QModelBuilderIG::Eval_Uf_Terms", 0 ),
-  d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ),
-  d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 )
+QModelBuilderIG::Statistics::Statistics()
+    : d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
+      d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers",
+                                0),
+      d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0),
+      d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_num_quants_init);
   smtStatisticsRegistry()->registerStat(&d_num_partial_quants_init);
   smtStatisticsRegistry()->registerStat(&d_init_inst_gen_lemmas);
   smtStatisticsRegistry()->registerStat(&d_inst_gen_lemmas);
-  smtStatisticsRegistry()->registerStat(&d_eval_formulas);
-  smtStatisticsRegistry()->registerStat(&d_eval_uf_terms);
-  smtStatisticsRegistry()->registerStat(&d_eval_lits);
-  smtStatisticsRegistry()->registerStat(&d_eval_lits_unknown);
 }
 
 QModelBuilderIG::Statistics::~Statistics(){
@@ -482,10 +475,6 @@ QModelBuilderIG::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_num_partial_quants_init);
   smtStatisticsRegistry()->unregisterStat(&d_init_inst_gen_lemmas);
   smtStatisticsRegistry()->unregisterStat(&d_inst_gen_lemmas);
-  smtStatisticsRegistry()->unregisterStat(&d_eval_formulas);
-  smtStatisticsRegistry()->unregisterStat(&d_eval_uf_terms);
-  smtStatisticsRegistry()->unregisterStat(&d_eval_lits);
-  smtStatisticsRegistry()->unregisterStat(&d_eval_lits_unknown);
 }
 
 //do exhaustive instantiation
@@ -558,12 +547,6 @@ int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, in
         }
       }
       //print debugging information
-      if( fmig ){
-        d_statistics.d_eval_formulas += fmig->d_eval_formulas;
-        d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms;
-        d_statistics.d_eval_lits += fmig->d_eval_lits;
-        d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown;
-      }
       Trace("inst-fmf-ei") << "For " << f << ", finished: " << std::endl;
       Trace("inst-fmf-ei") << "   Inst Tried: " << d_triedLemmas << std::endl;
       Trace("inst-fmf-ei") << "   Inst Added: " << d_addedLemmas << std::endl;
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index 353883a20..b34f1e580 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -148,10 +148,6 @@ class QModelBuilderIG : public QModelBuilder
     IntStat d_num_partial_quants_init;
     IntStat d_init_inst_gen_lemmas;
     IntStat d_inst_gen_lemmas;
-    IntStat d_eval_formulas;
-    IntStat d_eval_uf_terms;
-    IntStat d_eval_lits;
-    IntStat d_eval_lits_unknown;
     Statistics();
     ~Statistics();
   };
diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h
deleted file mode 100644
index b36be7aec..000000000
--- a/src/theory/quantifiers/macros.h
+++ /dev/null
@@ -1,74 +0,0 @@
-/*********************                                                        */
-/*! \file macros.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Pre-process step for detecting quantifier macro definitions
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__QUANTIFIERS_MACROS_H
-#define __CVC4__QUANTIFIERS_MACROS_H
-
-#include <iostream>
-#include <string>
-#include <vector>
-#include <map>
-#include "expr/node.h"
-#include "expr/type_node.h"
-#include "theory/quantifiers_engine.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class QuantifierMacros{
-private:
-  QuantifiersEngine * d_qe;
-private:
-  bool d_ground_macros;
-  bool processAssertion( Node n );
-  bool isBoundVarApplyUf( Node n );
-  bool process( Node n, bool pol, std::vector< Node >& args, Node f );
-  bool containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited );
-  bool isMacroLiteral( Node n, bool pol );
-  bool isGroundUfTerm( Node f, Node n );
-  void getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited );
-  Node solveInEquality( Node n, Node lit );
-  bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited );
-  bool getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved,
-                        std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete );
-  //map from operators to macro basis terms
-  std::map< Node, std::vector< Node > > d_macro_basis;
-  //map from operators to macro definition
-  std::map< Node, Node > d_macro_defs;
-  std::map< Node, Node > d_macro_defs_new;
-  //operators to macro ops that contain them
-  std::map< Node, std::vector< Node > > d_macro_def_contains;
-  //simplify caches
-  std::map< Node, Node > d_simplify_cache;
-  std::map< Node, bool > d_quant_macros;
-private:
-  Node simplify( Node n );
-  void addMacro( Node op, Node n, std::vector< Node >& opc );
-  void debugMacroDefinition( Node oo, Node n );
-public:
-  QuantifierMacros( QuantifiersEngine * qe );
-  ~QuantifierMacros(){}
-
-  bool simplify( std::vector< Node >& assertions, bool doRewrite = false );
-  void finalizeDefinitions();
-};
-
-}
-}
-}
-
-#endif
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a5cd95d29..510953035 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -70,10 +70,36 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
                                      context::UserContext* u,
                                      TheoryEngine* te)
     : d_te(te),
+      d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)),
+      d_eq_inference(nullptr),
+      d_inst_prop(nullptr),
+      d_tr_trie(new inst::TriggerTrie),
+      d_model(nullptr),
+      d_quant_rel(nullptr),
+      d_rel_dom(nullptr),
+      d_bv_invert(nullptr),
+      d_builder(nullptr),
+      d_qepr(nullptr),
+      d_term_util(new quantifiers::TermUtil(this)),
+      d_term_db(new quantifiers::TermDb(c, u, this)),
+      d_sygus_tdb(nullptr),
       d_quant_attr(new quantifiers::QuantAttributes(this)),
       d_instantiate(new quantifiers::Instantiate(this, u)),
       d_skolemize(new quantifiers::Skolemize(this, u)),
       d_term_enum(new quantifiers::TermEnumeration),
+      d_alpha_equiv(nullptr),
+      d_inst_engine(nullptr),
+      d_model_engine(nullptr),
+      d_bint(nullptr),
+      d_qcf(nullptr),
+      d_rr_engine(nullptr),
+      d_sg_gen(nullptr),
+      d_ceg_inst(nullptr),
+      d_lte_part_inst(nullptr),
+      d_fs(nullptr),
+      d_i_cbqi(nullptr),
+      d_qsplit(nullptr),
+      d_anti_skolem(nullptr),
       d_conflict_c(c, false),
       // d_quants(u),
       d_quants_prereg(u),
@@ -89,41 +115,29 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
       d_presolve_cache_wq(u),
       d_presolve_cache_wic(u)
 {
-  //utilities
-  d_eq_query = new quantifiers::EqualityQueryQuantifiersEngine( c, this );
-  d_util.push_back( d_eq_query );
+  //---- utilities
+  d_util.push_back(d_eq_query.get());
+  // term util must come before the other utilities
+  d_util.push_back(d_term_util.get());
+  d_util.push_back(d_term_db.get());
 
-  // term util must come first
-  d_term_util = new quantifiers::TermUtil(this);
-  d_util.push_back(d_term_util);
-
-  d_term_db = new quantifiers::TermDb( c, u, this );
-  d_util.push_back( d_term_db );
-  
   if (options::ceGuidedInst()) {
-    d_sygus_tdb = new quantifiers::TermDbSygus(c, this);
-  }else{
-    d_sygus_tdb = NULL;
+    d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this));
   }
 
   if( options::instPropagate() ){
     // notice that this option is incompatible with options::qcfAllConflict()
-    d_inst_prop = new quantifiers::InstPropagator( this );
-    d_util.push_back( d_inst_prop );
+    d_inst_prop.reset(new quantifiers::InstPropagator(this));
+    d_util.push_back(d_inst_prop.get());
     d_instantiate->addNotify(d_inst_prop->getInstantiationNotify());
-  }else{
-    d_inst_prop = NULL;
   }
   
   if( options::inferArithTriggerEq() ){
-    d_eq_inference = new quantifiers::EqualityInference(c, false);
-  }else{
-    d_eq_inference = NULL;
+    d_eq_inference.reset(new quantifiers::EqualityInference(c, false));
   }
 
   d_util.push_back(d_instantiate.get());
 
-  d_tr_trie = new inst::TriggerTrie;
   d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
   d_conflict = false;
   d_hasAddedLemma = false;
@@ -135,37 +149,15 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
 
   if( options::relevantTriggers() ){
-    d_quant_rel = new quantifiers::QuantRelevance;
-    d_util.push_back(d_quant_rel);
-  }else{
-    d_quant_rel = NULL;
+    d_quant_rel.reset(new quantifiers::QuantRelevance);
+    d_util.push_back(d_quant_rel.get());
   }
 
   if( options::quantEpr() ){
     Assert( !options::incrementalSolving() );
-    d_qepr = new quantifiers::QuantEPR;
-  }else{
-    d_qepr = NULL;
+    d_qepr.reset(new quantifiers::QuantEPR);
   }
-
-
-  d_qcf = NULL;
-  d_sg_gen = NULL;
-  d_inst_engine = NULL;
-  d_i_cbqi = NULL;
-  d_qsplit = NULL;
-  d_anti_skolem = NULL;
-  d_model = NULL;
-  d_model_engine = NULL;
-  d_bint = NULL;
-  d_rr_engine = NULL;
-  d_ceg_inst = NULL;
-  d_lte_part_inst = NULL;
-  d_alpha_equiv = NULL;
-  d_fs = NULL;
-  d_rel_dom = NULL;
-  d_bv_invert = NULL;
-  d_builder = NULL;
+  //---- end utilities
 
   //allow theory combination to go first, once initially
   d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
@@ -178,70 +170,70 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   bool needsRelDom = false;
   //add quantifiers modules
   if( options::quantConflictFind() || options::quantRewriteRules() ){
-    d_qcf = new quantifiers::QuantConflictFind( this, c);
-    d_modules.push_back( d_qcf );
+    d_qcf.reset(new quantifiers::QuantConflictFind(this, c));
+    d_modules.push_back(d_qcf.get());
   }
   if( options::conjectureGen() ){
-    d_sg_gen = new quantifiers::ConjectureGenerator( this, c );
-    d_modules.push_back( d_sg_gen );
+    d_sg_gen.reset(new quantifiers::ConjectureGenerator(this, c));
+    d_modules.push_back(d_sg_gen.get());
   }
   if( !options::finiteModelFind() || options::fmfInstEngine() ){
-    d_inst_engine = new quantifiers::InstantiationEngine( this );
-    d_modules.push_back(  d_inst_engine );
+    d_inst_engine.reset(new quantifiers::InstantiationEngine(this));
+    d_modules.push_back(d_inst_engine.get());
   }
   if( options::cbqi() ){
-    d_i_cbqi = new quantifiers::InstStrategyCegqi( this );
-    d_modules.push_back( d_i_cbqi );
+    d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(this));
+    d_modules.push_back(d_i_cbqi.get());
     if( options::cbqiBv() ){
       // if doing instantiation for BV, need the inverter class
-      d_bv_invert = new quantifiers::BvInverter;
+      d_bv_invert.reset(new quantifiers::BvInverter);
     }
   }
   if( options::ceGuidedInst() ){
-    d_ceg_inst = new quantifiers::CegInstantiation( this, c );
-    d_modules.push_back( d_ceg_inst );
+    d_ceg_inst.reset(new quantifiers::CegInstantiation(this, c));
+    d_modules.push_back(d_ceg_inst.get());
     //needsBuilder = true;
   }  
   //finite model finding
   if( options::finiteModelFind() ){
     if( options::fmfBound() ){
-      d_bint = new quantifiers::BoundedIntegers( c, this );
-      d_modules.push_back( d_bint );
+      d_bint.reset(new quantifiers::BoundedIntegers(c, this));
+      d_modules.push_back(d_bint.get());
     }
-    d_model_engine = new quantifiers::ModelEngine( c, this );
-    d_modules.push_back( d_model_engine );
+    d_model_engine.reset(new quantifiers::ModelEngine(c, this));
+    d_modules.push_back(d_model_engine.get());
     //finite model finder has special ways of building the model
     needsBuilder = true;
   }
   if( options::quantRewriteRules() ){
-    d_rr_engine = new quantifiers::RewriteEngine( c, this );
-    d_modules.push_back(d_rr_engine);
+    d_rr_engine.reset(new quantifiers::RewriteEngine(c, this));
+    d_modules.push_back(d_rr_engine.get());
   }
   if( options::ltePartialInst() ){
-    d_lte_part_inst = new quantifiers::LtePartialInst( this, c );
-    d_modules.push_back( d_lte_part_inst );
+    d_lte_part_inst.reset(new quantifiers::LtePartialInst(this, c));
+    d_modules.push_back(d_lte_part_inst.get());
   }
   if( options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ){
-    d_qsplit = new quantifiers::QuantDSplit( this, c );
-    d_modules.push_back( d_qsplit );
+    d_qsplit.reset(new quantifiers::QuantDSplit(this, c));
+    d_modules.push_back(d_qsplit.get());
   }
   if( options::quantAntiSkolem() ){
-    d_anti_skolem = new quantifiers::QuantAntiSkolem( this );
-    d_modules.push_back( d_anti_skolem );
+    d_anti_skolem.reset(new quantifiers::QuantAntiSkolem(this));
+    d_modules.push_back(d_anti_skolem.get());
   }
   if( options::quantAlphaEquiv() ){
-    d_alpha_equiv = new quantifiers::AlphaEquivalence( this );
+    d_alpha_equiv.reset(new quantifiers::AlphaEquivalence(this));
   }
   //full saturation : instantiate from relevant domain, then arbitrary terms
   if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){
-    d_fs = new quantifiers::InstStrategyEnum(this);
-    d_modules.push_back( d_fs );
+    d_fs.reset(new quantifiers::InstStrategyEnum(this));
+    d_modules.push_back(d_fs.get());
     needsRelDom = true;
   }
   
   if( needsRelDom ){
-    d_rel_dom = new quantifiers::RelevantDomain( this );
-    d_util.push_back( d_rel_dom );
+    d_rel_dom.reset(new quantifiers::RelevantDomain(this));
+    d_util.push_back(d_rel_dom.get());
   }
   
   // if we require specialized ways of building the model
@@ -252,53 +244,27 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
         || options::fmfBound())
     {
       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
-      d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
-      d_builder = new quantifiers::fmcheck::FullModelChecker( c, this );
+      d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
+          this, c, "FirstOrderModelFmc"));
+      d_builder.reset(new quantifiers::fmcheck::FullModelChecker(c, this));
     }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
       Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl;
-      d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" );
-      d_builder = new quantifiers::AbsMbqiBuilder( c, this );
+      d_model.reset(
+          new quantifiers::FirstOrderModelAbs(this, c, "FirstOrderModelAbs"));
+      d_builder.reset(new quantifiers::AbsMbqiBuilder(c, this));
     }else{
       Trace("quant-engine-debug") << "...make default model builder." << std::endl;
-      d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
-      d_builder = new quantifiers::QModelBuilderDefault( c, this );
+      d_model.reset(
+          new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG"));
+      d_builder.reset(new quantifiers::QModelBuilderDefault(c, this));
     }
   }else{
-    d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
+    d_model.reset(
+        new quantifiers::FirstOrderModelIG(this, c, "FirstOrderModelIG"));
   }
 }
 
-QuantifiersEngine::~QuantifiersEngine()
-{
-  delete d_alpha_equiv;
-  delete d_builder;
-  delete d_qepr;
-  delete d_rr_engine;
-  delete d_bint;
-  delete d_model_engine;
-  delete d_inst_engine;
-  delete d_qcf;
-  delete d_quant_rel;
-  delete d_rel_dom;
-  delete d_bv_invert;
-  delete d_model;
-  delete d_tr_trie;
-  delete d_term_db;
-  delete d_sygus_tdb;
-  delete d_term_util;
-  delete d_eq_inference;
-  delete d_eq_query;
-  delete d_sg_gen;
-  delete d_ceg_inst;
-  delete d_lte_part_inst;
-  delete d_fs;
-  delete d_i_cbqi;
-  delete d_qsplit;
-  delete d_anti_skolem;
-  delete d_inst_prop;
-}
-
-EqualityQuery* QuantifiersEngine::getEqualityQuery() { return d_eq_query; }
+QuantifiersEngine::~QuantifiersEngine() {}
 
 context::Context* QuantifiersEngine::getSatContext()
 {
@@ -325,6 +291,96 @@ const LogicInfo& QuantifiersEngine::getLogicInfo() const
   return d_te->getLogicInfo();
 }
 
+EqualityQuery* QuantifiersEngine::getEqualityQuery() const
+{
+  return d_eq_query.get();
+}
+quantifiers::EqualityInference* QuantifiersEngine::getEqualityInference() const
+{
+  return d_eq_inference.get();
+}
+quantifiers::RelevantDomain* QuantifiersEngine::getRelevantDomain() const
+{
+  return d_rel_dom.get();
+}
+quantifiers::BvInverter* QuantifiersEngine::getBvInverter() const
+{
+  return d_bv_invert.get();
+}
+quantifiers::QuantRelevance* QuantifiersEngine::getQuantifierRelevance() const
+{
+  return d_quant_rel.get();
+}
+quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
+{
+  return d_builder.get();
+}
+quantifiers::QuantEPR* QuantifiersEngine::getQuantEPR() const
+{
+  return d_qepr.get();
+}
+quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
+{
+  return d_model.get();
+}
+quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
+{
+  return d_term_db.get();
+}
+quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const
+{
+  return d_sygus_tdb.get();
+}
+quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const
+{
+  return d_term_util.get();
+}
+quantifiers::QuantAttributes* QuantifiersEngine::getQuantAttributes() const
+{
+  return d_quant_attr.get();
+}
+quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const
+{
+  return d_instantiate.get();
+}
+quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const
+{
+  return d_skolemize.get();
+}
+quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const
+{
+  return d_term_enum.get();
+}
+inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
+{
+  return d_tr_trie.get();
+}
+
+quantifiers::BoundedIntegers* QuantifiersEngine::getBoundedIntegers() const
+{
+  return d_bint.get();
+}
+quantifiers::QuantConflictFind* QuantifiersEngine::getConflictFind() const
+{
+  return d_qcf.get();
+}
+quantifiers::RewriteEngine* QuantifiersEngine::getRewriteEngine() const
+{
+  return d_rr_engine.get();
+}
+quantifiers::CegInstantiation* QuantifiersEngine::getCegInstantiation() const
+{
+  return d_ceg_inst.get();
+}
+quantifiers::InstStrategyEnum* QuantifiersEngine::getInstStrategyEnum() const
+{
+  return d_fs.get();
+}
+quantifiers::InstStrategyCbqi* QuantifiersEngine::getInstStrategyCbqi() const
+{
+  return d_i_cbqi.get();
+}
+
 QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
   std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q );
   if( it==d_owner.end() ){
@@ -419,7 +475,8 @@ void QuantifiersEngine::check( Theory::Effort e ){
   // if we want to use the model's equality engine, build the model now
   if( d_useModelEe && !d_model->isBuilt() ){
     Trace("quant-engine-debug") << "Build the model." << std::endl;
-    if( !d_te->getModelBuilder()->buildModel( d_model ) ){
+    if (!d_te->getModelBuilder()->buildModel(d_model.get()))
+    {
       //we are done if model building was unsuccessful
       flushLemmas();
       if( d_hasAddedLemma ){
@@ -582,9 +639,10 @@ void QuantifiersEngine::check( Theory::Effort e ){
         {
           // theory engine's model builder is quantifier engine's builder if it
           // has one
-          Assert(!d_builder || d_builder == d_te->getModelBuilder());
+          Assert(!getModelBuilder()
+                 || getModelBuilder() == d_te->getModelBuilder());
           Trace("quant-engine-debug") << "Build model..." << std::endl;
-          if (!d_te->getModelBuilder()->buildModel(d_model))
+          if (!d_te->getModelBuilder()->buildModel(d_model.get()))
           {
             flushLemmas();
           }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 674954023..aabca1640 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -84,134 +84,17 @@ namespace inst {
 
 
 class QuantifiersEngine {
-  // TODO: remove these github issue #1163
-  friend class quantifiers::InstantiationEngine;
-  friend class quantifiers::InstStrategyCbqi;
-  friend class quantifiers::InstStrategyCegqi;
-  friend class quantifiers::ModelEngine;
-  friend class quantifiers::RewriteEngine;
-  friend class quantifiers::QuantConflictFind;
-  friend class inst::InstMatch;
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
   typedef context::CDList<Node> NodeList;
   typedef context::CDList<bool> BoolList;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
-private:
-  /** reference to theory engine object */
-  TheoryEngine* d_te;
-  /** vector of utilities for quantifiers */
-  std::vector< QuantifiersUtil* > d_util;
-  /** vector of modules for quantifiers */
-  std::vector< QuantifiersModule* > d_modules;
-  /** equality query class */
-  quantifiers::EqualityQueryQuantifiersEngine* d_eq_query;
-  /** equality inference class */
-  quantifiers::EqualityInference* d_eq_inference;
-  /** for computing relevance of quantifiers */
-  quantifiers::QuantRelevance* d_quant_rel;
-  /** relevant domain */
-  quantifiers::RelevantDomain* d_rel_dom;
-  /** inversion utility for BV instantiation */
-  quantifiers::BvInverter * d_bv_invert;
-  /** alpha equivalence */
-  quantifiers::AlphaEquivalence * d_alpha_equiv;
-  /** model builder */
-  quantifiers::QModelBuilder* d_builder;
-  /** utility for effectively propositional logic */
-  quantifiers::QuantEPR* d_qepr;
-  /** term database */
-  quantifiers::TermDb* d_term_db;
-  /** sygus term database */
-  quantifiers::TermDbSygus* d_sygus_tdb;
-  /** term utilities */
-  quantifiers::TermUtil* d_term_util;
-  /** quantifiers attributes */
-  std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
-  /** instantiate utility */
-  std::unique_ptr<quantifiers::Instantiate> d_instantiate;
-  /** skolemize utility */
-  std::unique_ptr<quantifiers::Skolemize> d_skolemize;
-  /** term enumeration utility */
-  std::unique_ptr<quantifiers::TermEnumeration> d_term_enum;
-  /** instantiation engine */
-  quantifiers::InstantiationEngine* d_inst_engine;
-  /** model engine */
-  quantifiers::ModelEngine* d_model_engine;
-  /** bounded integers utility */
-  quantifiers::BoundedIntegers * d_bint;
-  /** Conflict find mechanism for quantifiers */
-  quantifiers::QuantConflictFind* d_qcf;
-  /** rewrite rules utility */
-  quantifiers::RewriteEngine * d_rr_engine;
-  /** subgoal generator */
-  quantifiers::ConjectureGenerator * d_sg_gen;
-  /** ceg instantiation */
-  quantifiers::CegInstantiation * d_ceg_inst;
-  /** lte partial instantiation */
-  quantifiers::LtePartialInst * d_lte_part_inst;
-  /** full saturation */
-  quantifiers::InstStrategyEnum* d_fs;
-  /** counterexample-based quantifier instantiation */
-  quantifiers::InstStrategyCbqi * d_i_cbqi;
-  /** quantifiers splitting */
-  quantifiers::QuantDSplit * d_qsplit;
-  /** quantifiers anti-skolemization */
-  quantifiers::QuantAntiSkolem * d_anti_skolem;
-  /** quantifiers instantiation propagtor */
-  quantifiers::InstPropagator * d_inst_prop;
-
- private:  //this information is reset during check
-    /** current effort level */
-  QuantifiersModule::QEffort d_curr_effort_level;
-  /** are we in conflict */
-  bool d_conflict;
-  context::CDO<bool> d_conflict_c;
-  /** has added lemma this round */
-  bool d_hasAddedLemma;
-  /** whether to use model equality engine */
-  bool d_useModelEe;
- private:
-  /** list of all quantifiers seen */
-  std::map< Node, bool > d_quants;
-  /** quantifiers pre-registered */
-  NodeSet d_quants_prereg;
-  /** quantifiers reduced */
-  BoolMap d_quants_red;
-  std::map< Node, Node > d_quants_red_lem;
-  /** list of all lemmas produced */
-  //std::map< Node, bool > d_lemmas_produced;
-  BoolMap d_lemmas_produced_c;
-  /** lemmas waiting */
-  std::vector< Node > d_lemmas_waiting;
-  /** phase requirements waiting */
-  std::map< Node, bool > d_phase_req_waiting;
-  /** all triggers will be stored in this trie */
-  inst::TriggerTrie* d_tr_trie;
-  /** extended model object */
-  quantifiers::FirstOrderModel* d_model;
-  /** inst round counters TODO: make context-dependent? */
-  context::CDO< int > d_ierCounter_c;
-  int d_ierCounter;
-  int d_ierCounter_lc;
-  int d_ierCounterLastLc;
-  int d_inst_when_phase;
-  /** has presolve been called */
-  context::CDO< bool > d_presolve;
-  /** presolve cache */
-  NodeSet d_presolve_in;
-  NodeList d_presolve_cache;
-  BoolList d_presolve_cache_wq;
-  BoolList d_presolve_cache_wic;
 
 public:
   QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
   ~QuantifiersEngine();
+  //---------------------- external interface
   /** get theory engine */
-  TheoryEngine* getTheoryEngine() { return d_te; }
-  /** get equality query */
-  EqualityQuery* getEqualityQuery();
-  /** get the equality inference */
-  quantifiers::EqualityInference* getEqualityInference() { return d_eq_inference; }
+  TheoryEngine* getTheoryEngine() const { return d_te; }
   /** get default sat context for quantifiers engine */
   context::Context* getSatContext();
   /** get default sat context for quantifiers engine */
@@ -222,42 +105,56 @@ public:
   Valuation& getValuation();
   /** get the logic info for the quantifiers engine */
   const LogicInfo& getLogicInfo() const;
+  //---------------------- end external interface
+  //---------------------- utilities
+  /** get equality query */
+  EqualityQuery* getEqualityQuery() const;
+  /** get the equality inference */
+  quantifiers::EqualityInference* getEqualityInference() const;
   /** get relevant domain */
-  quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; }
+  quantifiers::RelevantDomain* getRelevantDomain() const;
   /** get the BV inverter utility */
-  quantifiers::BvInverter * getBvInverter() { return d_bv_invert; }
+  quantifiers::BvInverter* getBvInverter() const;
   /** get quantifier relevance */
-  quantifiers::QuantRelevance* getQuantifierRelevance() { return d_quant_rel; }
+  quantifiers::QuantRelevance* getQuantifierRelevance() const;
   /** get the model builder */
-  quantifiers::QModelBuilder* getModelBuilder() { return d_builder; }
+  quantifiers::QModelBuilder* getModelBuilder() const;
   /** get utility for EPR */
-  quantifiers::QuantEPR* getQuantEPR() { return d_qepr; }
- public:  // modules
-  /** get instantiation engine */
-  quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
-  /** get model engine */
-  quantifiers::ModelEngine* getModelEngine() { return d_model_engine; }
+  quantifiers::QuantEPR* getQuantEPR() const;
+  /** get model */
+  quantifiers::FirstOrderModel* getModel() const;
+  /** get term database */
+  quantifiers::TermDb* getTermDatabase() const;
+  /** get term database sygus */
+  quantifiers::TermDbSygus* getTermDatabaseSygus() const;
+  /** get term utilities */
+  quantifiers::TermUtil* getTermUtil() const;
+  /** get quantifiers attributes */
+  quantifiers::QuantAttributes* getQuantAttributes() const;
+  /** get instantiate utility */
+  quantifiers::Instantiate* getInstantiate() const;
+  /** get skolemize utility */
+  quantifiers::Skolemize* getSkolemize() const;
+  /** get term enumeration utility */
+  quantifiers::TermEnumeration* getTermEnumeration() const;
+  /** get trigger database */
+  inst::TriggerTrie* getTriggerDatabase() const;
+  //---------------------- end utilities
+  //---------------------- modules
   /** get bounded integers utility */
-  quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; }
+  quantifiers::BoundedIntegers* getBoundedIntegers() const;
   /** Conflict find mechanism for quantifiers */
-  quantifiers::QuantConflictFind* getConflictFind() { return d_qcf; }
+  quantifiers::QuantConflictFind* getConflictFind() const;
   /** rewrite rules utility */
-  quantifiers::RewriteEngine * getRewriteEngine() { return d_rr_engine; }
-  /** subgoal generator */
-  quantifiers::ConjectureGenerator * getConjectureGenerator() { return d_sg_gen; }
+  quantifiers::RewriteEngine* getRewriteEngine() const;
   /** ceg instantiation */
-  quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; }
-  /** local theory ext partial inst */
-  quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; }
+  quantifiers::CegInstantiation* getCegInstantiation() const;
   /** get full saturation */
-  quantifiers::InstStrategyEnum* getInstStrategyEnum() { return d_fs; }
+  quantifiers::InstStrategyEnum* getInstStrategyEnum() const;
   /** get inst strategy cbqi */
-  quantifiers::InstStrategyCbqi * getInstStrategyCbqi() { return d_i_cbqi; }
-  /** get quantifiers splitting */
-  quantifiers::QuantDSplit * getQuantDSplit() { return d_qsplit; }
-  /** get quantifiers anti-skolemization */
-  quantifiers::QuantAntiSkolem * getQuantAntiSkolem() { return d_anti_skolem; }
-private:
+  quantifiers::InstStrategyCbqi* getInstStrategyCbqi() const;
+  //---------------------- end modules
+ private:
   /** owner of quantified formulas */
   std::map< Node, QuantifiersModule * > d_owner;
   std::map< Node, int > d_owner_priority;
@@ -331,29 +228,6 @@ public:
   /** get user pat mode */
   quantifiers::UserPatMode getInstUserPatMode();
 public:
-  /** get model */
-  quantifiers::FirstOrderModel* getModel() { return d_model; }
-  /** get term database */
-  quantifiers::TermDb* getTermDatabase() { return d_term_db; }
-  /** get term database sygus */
-  quantifiers::TermDbSygus * getTermDatabaseSygus() { return d_sygus_tdb; }
-  /** get term utilities */
-  quantifiers::TermUtil* getTermUtil() { return d_term_util; }
-  /** get quantifiers attributes */
-  quantifiers::QuantAttributes* getQuantAttributes() {
-    return d_quant_attr.get();
-  }
-  /** get instantiate utility */
-  quantifiers::Instantiate* getInstantiate() { return d_instantiate.get(); }
-  /** get skolemize utility */
-  quantifiers::Skolemize* getSkolemize() { return d_skolemize.get(); }
-  /** get term enumeration utility */
-  quantifiers::TermEnumeration* getTermEnumeration()
-  {
-    return d_term_enum.get();
-  }
-  /** get trigger database */
-  inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
   /** add term to database */
   void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
   /** notification when master equality engine is updated */
@@ -439,6 +313,117 @@ public:
     ~Statistics();
   };/* class QuantifiersEngine::Statistics */
   Statistics d_statistics;
+  
+ private:
+  /** reference to theory engine object */
+  TheoryEngine* d_te;
+  /** vector of utilities for quantifiers */
+  std::vector<QuantifiersUtil*> d_util;
+  /** vector of modules for quantifiers */
+  std::vector<QuantifiersModule*> d_modules;
+  //------------- quantifiers utilities
+  /** equality query class */
+  std::unique_ptr<quantifiers::EqualityQueryQuantifiersEngine> d_eq_query;
+  /** equality inference class */
+  std::unique_ptr<quantifiers::EqualityInference> d_eq_inference;
+  /** quantifiers instantiation propagtor */
+  std::unique_ptr<quantifiers::InstPropagator> d_inst_prop;
+  /** all triggers will be stored in this trie */
+  std::unique_ptr<inst::TriggerTrie> d_tr_trie;
+  /** extended model object */
+  std::unique_ptr<quantifiers::FirstOrderModel> d_model;
+  /** for computing relevance of quantifiers */
+  std::unique_ptr<quantifiers::QuantRelevance> d_quant_rel;
+  /** relevant domain */
+  std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom;
+  /** inversion utility for BV instantiation */
+  std::unique_ptr<quantifiers::BvInverter> d_bv_invert;
+  /** model builder */
+  std::unique_ptr<quantifiers::QModelBuilder> d_builder;
+  /** utility for effectively propositional logic */
+  std::unique_ptr<quantifiers::QuantEPR> d_qepr;
+  /** term utilities */
+  std::unique_ptr<quantifiers::TermUtil> d_term_util;
+  /** term database */
+  std::unique_ptr<quantifiers::TermDb> d_term_db;
+  /** sygus term database */
+  std::unique_ptr<quantifiers::TermDbSygus> d_sygus_tdb;
+  /** quantifiers attributes */
+  std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
+  /** instantiate utility */
+  std::unique_ptr<quantifiers::Instantiate> d_instantiate;
+  /** skolemize utility */
+  std::unique_ptr<quantifiers::Skolemize> d_skolemize;
+  /** term enumeration utility */
+  std::unique_ptr<quantifiers::TermEnumeration> d_term_enum;
+  //------------- end quantifiers utilities
+  //------------- quantifiers modules
+  /** alpha equivalence */
+  std::unique_ptr<quantifiers::AlphaEquivalence> d_alpha_equiv;
+  /** instantiation engine */
+  std::unique_ptr<quantifiers::InstantiationEngine> d_inst_engine;
+  /** model engine */
+  std::unique_ptr<quantifiers::ModelEngine> d_model_engine;
+  /** bounded integers utility */
+  std::unique_ptr<quantifiers::BoundedIntegers> d_bint;
+  /** Conflict find mechanism for quantifiers */
+  std::unique_ptr<quantifiers::QuantConflictFind> d_qcf;
+  /** rewrite rules utility */
+  std::unique_ptr<quantifiers::RewriteEngine> d_rr_engine;
+  /** subgoal generator */
+  std::unique_ptr<quantifiers::ConjectureGenerator> d_sg_gen;
+  /** ceg instantiation */
+  std::unique_ptr<quantifiers::CegInstantiation> d_ceg_inst;
+  /** lte partial instantiation */
+  std::unique_ptr<quantifiers::LtePartialInst> d_lte_part_inst;
+  /** full saturation */
+  std::unique_ptr<quantifiers::InstStrategyEnum> d_fs;
+  /** counterexample-based quantifier instantiation */
+  std::unique_ptr<quantifiers::InstStrategyCbqi> d_i_cbqi;
+  /** quantifiers splitting */
+  std::unique_ptr<quantifiers::QuantDSplit> d_qsplit;
+  /** quantifiers anti-skolemization */
+  std::unique_ptr<quantifiers::QuantAntiSkolem> d_anti_skolem;
+  //------------- end quantifiers modules
+  //------------- temporary information during check
+  /** current effort level */
+  QuantifiersModule::QEffort d_curr_effort_level;
+  /** are we in conflict */
+  bool d_conflict;
+  context::CDO<bool> d_conflict_c;
+  /** has added lemma this round */
+  bool d_hasAddedLemma;
+  /** whether to use model equality engine */
+  bool d_useModelEe;
+  //------------- end temporary information during check
+ private:
+  /** list of all quantifiers seen */
+  std::map<Node, bool> d_quants;
+  /** quantifiers pre-registered */
+  NodeSet d_quants_prereg;
+  /** quantifiers reduced */
+  BoolMap d_quants_red;
+  std::map<Node, Node> d_quants_red_lem;
+  /** list of all lemmas produced */
+  // std::map< Node, bool > d_lemmas_produced;
+  BoolMap d_lemmas_produced_c;
+  /** lemmas waiting */
+  std::vector<Node> d_lemmas_waiting;
+  /** phase requirements waiting */
+  std::map<Node, bool> d_phase_req_waiting;
+  /** inst round counters TODO: make context-dependent? */
+  context::CDO<int> d_ierCounter_c;
+  int d_ierCounter;
+  int d_ierCounter_lc;
+  int d_ierCounterLastLc;
+  int d_inst_when_phase;
+  /** has presolve been called */
+  context::CDO<bool> d_presolve;
+  /** presolve cache */
+  NodeSet d_presolve_in;
+  NodeList d_presolve_cache;
+  BoolList d_presolve_cache_wq;
+  BoolList d_presolve_cache_wic;
 };/* class QuantifiersEngine */
 
 }/* CVC4::theory namespace */
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index ab9fa6d54..317080ba6 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -37,25 +37,28 @@ namespace sets {
 
 TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
                                      context::Context* c,
-                                     context::UserContext* u):
-  d_rels(NULL),
-  d_members(c),
-  d_deq(c),
-  d_deq_processed(u),
-  d_keep(c),
-  d_proxy(u),
-  d_proxy_to_term(u),
-  d_lemmas_produced(u),
-  d_card_processed(u),
-  d_var_elim(u),
-  d_external(external),
-  d_notify(*this),
-  d_equalityEngine(d_notify, c, "theory::sets::ee", true),
-  d_conflict(c)
+                                     context::UserContext* u)
+    : d_members(c),
+      d_deq(c),
+      d_deq_processed(u),
+      d_keep(c),
+      d_sentLemma(false),
+      d_addedFact(false),
+      d_full_check_incomplete(false),
+      d_proxy(u),
+      d_proxy_to_term(u),
+      d_lemmas_produced(u),
+      d_card_enabled(false),
+      d_card_processed(u),
+      d_var_elim(u),
+      d_external(external),
+      d_notify(*this),
+      d_equalityEngine(d_notify, c, "theory::sets::ee", true),
+      d_conflict(c),
+      d_rels(
+          new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external)),
+      d_rels_enabled(false)
 {
-
-  d_rels = new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external);
-
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
   d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
@@ -68,21 +71,14 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
   d_equalityEngine.addFunctionKind(kind::MEMBER);
   d_equalityEngine.addFunctionKind(kind::SUBSET);
 
-  // If cardinality is on.
   d_equalityEngine.addFunctionKind(kind::CARD);
-
-  d_card_enabled = false;
-  d_rels_enabled = false;
-
-}/* TheorySetsPrivate::TheorySetsPrivate() */
+}
 
 TheorySetsPrivate::~TheorySetsPrivate(){
-  delete d_rels;
   for (std::pair<const Node, EqcInfo*>& current_pair : d_eqc_info) {
     delete current_pair.second;
   }
-}/* TheorySetsPrivate::~TheorySetsPrivate() */
-
+}
 
 void TheorySetsPrivate::eqNotifyNewClass(TNode t) {
   if( t.getKind()==kind::SINGLETON || t.getKind()==kind::EMPTYSET ){
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 31aec85c3..d36e0ddb1 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -46,8 +46,6 @@ class TheorySetsPrivate {
   typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
   typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
-private:
-  TheorySetsRels * d_rels;
 public:
   void eqNotifyNewClass(TNode t);
   void eqNotifyPreMerge(TNode t1, TNode t2);
@@ -113,9 +111,25 @@ private:
   void addEqualityToExp( Node a, Node b, std::vector< Node >& exp );
   
   void debugPrintSet( Node s, const char * c );
-  
+
+  /** sent lemma
+   *
+   * This flag is set to true during a full effort check if this theory
+   * called d_out->lemma(...).
+   */
   bool d_sentLemma;
+  /** added fact
+   *
+   * This flag is set to true during a full effort check if this theory
+   * added an internal fact to its equality engine.
+   */
   bool d_addedFact;
+  /** full check incomplete
+   *
+   * This flag is set to true during a full effort check if this theory
+   * is incomplete for some reason (for instance, if we combine cardinality
+   * with a relation or extended function kind).
+   */
   bool d_full_check_incomplete;
   NodeMap d_proxy;  
   NodeMap d_proxy_to_term;  
@@ -139,11 +153,15 @@ private:
   std::map< Kind, std::map< Node, std::map< Node, Node > > > d_bop_index;
   std::map< Kind, std::vector< Node > > d_op_list;
   //cardinality
-private:
+ private:
+  /** is cardinality enabled?
+   *
+   * This flag is set to true during a full effort check if any constraint
+   * involving cardinality constraints is asserted to this theory.
+   */
   bool d_card_enabled;
   /** element types of sets for which cardinality is enabled */
   std::map<TypeNode, bool> d_t_card_enabled;
-  bool d_rels_enabled;
   std::map< Node, Node > d_eqc_to_card_term;
   NodeSet d_card_processed;
   std::map< Node, std::vector< Node > > d_card_parent;
@@ -300,7 +318,16 @@ private:
   bool isCareArg( Node n, unsigned a );
 public:
   bool isEntailed( Node n, bool pol );
-  
+
+ private:
+  /** subtheory solver for the theory of relations */
+  std::unique_ptr<TheorySetsRels> d_rels;
+  /** are relations enabled?
+   *
+   * This flag is set to true during a full effort check if any constraint
+   * involving relational constraints is asserted to this theory.
+   */
+  bool d_rels_enabled;
 };/* class TheorySetsPrivate */
 
 
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 477e99b9b..f53f82cc4 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -34,7 +34,6 @@ RegExpOpr::RegExpOpr()
                                                      std::vector<Node>{})),
       d_zero(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))),
       d_one(NodeManager::currentNM()->mkConst(::CVC4::Rational(1))),
-      RMAXINT(LONG_MAX),
       d_sigma(NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA,
                                                std::vector<Node>{})),
       d_sigma_star(NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, d_sigma))
@@ -1137,7 +1136,8 @@ bool RegExpOpr::isPairNodesInSet(std::set< PairNodes > &s, Node n1, Node n2) {
 
 bool RegExpOpr::containC2(unsigned cnt, Node n) {
   if(n.getKind() == kind::REGEXP_RV) {
-    Assert(n[0].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in RegExpOpr::containC2");
+    Assert(n[0].getConst<Rational>() <= Rational(String::maxSize()),
+           "Exceeded UINT32_MAX in RegExpOpr::containC2");
     unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt();
     return cnt == y;
   } else if(n.getKind() == kind::REGEXP_CONCAT) {
@@ -1178,7 +1178,8 @@ void RegExpOpr::convert2(unsigned cnt, Node n, Node &r1, Node &r2) {
     r1 = d_emptySingleton;
     r2 = d_emptySingleton;
   } else if(n.getKind() == kind::REGEXP_RV) {
-    Assert(n[0].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in RegExpOpr::convert2");
+    Assert(n[0].getConst<Rational>() <= Rational(String::maxSize()),
+           "Exceeded UINT32_MAX in RegExpOpr::convert2");
     unsigned y = n[0].getConst<Rational>().getNumerator().toUnsignedInt();
     r1 = d_emptySingleton;
     if(cnt == y) {
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index a646f0e6f..57e68abfb 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -48,7 +48,6 @@ class RegExpOpr {
   Node d_emptyRegexp;
   Node d_zero;
   Node d_one;
-  CVC4::Rational RMAXINT;
 
   Node d_sigma;
   Node d_sigma_star;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ce0100686..72e82edca 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -103,7 +103,6 @@ TheoryStrings::TheoryStrings(context::Context* c,
                              Valuation valuation,
                              const LogicInfo& logicInfo)
     : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
-      RMAXINT(LONG_MAX),
       d_notify(*this),
       d_equalityEngine(d_notify, c, "theory::strings", true),
       d_conflict(c, false),
@@ -536,7 +535,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
     Trace("strings-model") << " } (length is " << lts[i] << ")" << std::endl;
     if( lts[i].isConst() ) {
       lts_values.push_back( lts[i] );
-      Assert(lts[i].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model");
+      Assert(lts[i].getConst<Rational>() <= Rational(String::maxSize()),
+             "Exceeded UINT32_MAX in string model");
       unsigned lvalue = lts[i].getConst<Rational>().getNumerator().toUnsignedInt();
       values_used[ lvalue ] = true;
     }else{
@@ -545,7 +545,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
         Node v = d_valuation.getModelValue(lts[i]);
         Trace("strings-model") << "Model value for " << lts[i] << " is " << v << std::endl;
         lts_values.push_back( v );
-        Assert(v.getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model");
+        Assert(v.getConst<Rational>() <= Rational(String::maxSize()),
+               "Exceeded UINT32_MAX in string model");
         unsigned lvalue =  v.getConst<Rational>().getNumerator().toUnsignedInt();
         values_used[ lvalue ] = true;
       }else{
@@ -621,7 +622,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
       Trace("strings-model") << std::endl;
 
       //use type enumerator
-      Assert(lts_values[i].getConst<Rational>() <= RMAXINT, "Exceeded LONG_MAX in string model");
+      Assert(lts_values[i].getConst<Rational>() <= Rational(String::maxSize()),
+             "Exceeded UINT32_MAX in string model");
       StringEnumeratorLength sel(lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt());
       for (const Node& eqc : pure_eq)
       {
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index de505f262..2c0cb42aa 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -234,7 +234,6 @@ private:
   Node d_zero;
   Node d_one;
   Node d_neg_one;
-  CVC4::Rational RMAXINT;
   unsigned d_card_size;
   // Helper functions
   Node getRepresentative( Node t );
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 9a0fad7d8..1c68097ae 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -653,13 +653,13 @@ Node TheoryStringsRewriter::rewriteLoopRegExp(TNode node)
   }
   TNode n1 = node[1];
   NodeManager* nm = NodeManager::currentNM();
-  CVC4::Rational RMAXINT(LONG_MAX);
+  CVC4::Rational rMaxInt(String::maxSize());
   AlwaysAssert(n1.isConst(), "re.loop contains non-constant integer (1).");
   AlwaysAssert(n1.getConst<Rational>().sgn() >= 0,
                "Negative integer in string REGEXP_LOOP (1)");
-  Assert(n1.getConst<Rational>() <= RMAXINT,
-         "Exceeded LONG_MAX in string REGEXP_LOOP (1)");
-  unsigned l = n1.getConst<Rational>().getNumerator().toUnsignedInt();
+  Assert(n1.getConst<Rational>() <= rMaxInt,
+         "Exceeded UINT32_MAX in string REGEXP_LOOP (1)");
+  uint32_t l = n1.getConst<Rational>().getNumerator().toUnsignedInt();
   std::vector<Node> vec_nodes;
   for (unsigned i = 0; i < l; i++)
   {
@@ -675,9 +675,9 @@ Node TheoryStringsRewriter::rewriteLoopRegExp(TNode node)
     AlwaysAssert(n2.isConst(), "re.loop contains non-constant integer (2).");
     AlwaysAssert(n2.getConst<Rational>().sgn() >= 0,
                  "Negative integer in string REGEXP_LOOP (2)");
-    Assert(n2.getConst<Rational>() <= RMAXINT,
-           "Exceeded LONG_MAX in string REGEXP_LOOP (2)");
-    unsigned u = n2.getConst<Rational>().getNumerator().toUnsignedInt();
+    Assert(n2.getConst<Rational>() <= rMaxInt,
+           "Exceeded UINT32_MAX in string REGEXP_LOOP (2)");
+    uint32_t u = n2.getConst<Rational>().getNumerator().toUnsignedInt();
     if (u <= l)
     {
       retNode = n;
@@ -838,7 +838,7 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i
       }
     }
     case kind::REGEXP_LOOP: {
-      unsigned l = r[1].getConst<Rational>().getNumerator().toUnsignedInt();
+      uint32_t l = r[1].getConst<Rational>().getNumerator().toUnsignedInt();
       if(s.size() == index_start) {
         return l==0? true : testConstStringInRegExp(s, index_start, r[0]);
       } else if(l==0 && r[1]==r[2]) {
@@ -847,7 +847,7 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i
         Assert(r.getNumChildren() == 3, "String rewriter error: LOOP has 2 children");
         if(l==0) {
           //R{0,u}
-          unsigned u = r[2].getConst<Rational>().getNumerator().toUnsignedInt();
+          uint32_t u = r[2].getConst<Rational>().getNumerator().toUnsignedInt();
           for(unsigned len=s.size() - index_start; len>=1; len--) {
             CVC4::String t = s.substr(index_start, len);
             if(testConstStringInRegExp(t, 0, r[0])) {
@@ -1216,9 +1216,9 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
     if (node[1].isConst() && node[2].isConst())
     {
       CVC4::String s = node[0].getConst<String>();
-      CVC4::Rational RMAXINT(LONG_MAX);
-      unsigned start;
-      if (node[1].getConst<Rational>() > RMAXINT)
+      CVC4::Rational rMaxInt(String::maxSize());
+      uint32_t start;
+      if (node[1].getConst<Rational>() > rMaxInt)
       {
         // start beyond the maximum size of strings
         // thus, it must be beyond the end point of this string
@@ -1241,7 +1241,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
           return returnRewrite(node, ret, "ss-const-start-oob");
         }
       }
-      if (node[2].getConst<Rational>() > RMAXINT)
+      if (node[2].getConst<Rational>() > rMaxInt)
       {
         // take up to the end of the string
         Node ret = nm->mkConst(::CVC4::String(s.suffix(s.size() - start)));
@@ -1254,7 +1254,7 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node)
       }
       else
       {
-        unsigned len =
+        uint32_t len =
             node[2].getConst<Rational>().getNumerator().toUnsignedInt();
         if (start + len > s.size())
         {
@@ -1743,17 +1743,17 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
   getConcat(node[0], children0);
   if (children0[0].isConst() && node[1].isConst() && node[2].isConst())
   {
-    CVC4::Rational RMAXINT(CVC4::String::maxSize());
-    if (node[2].getConst<Rational>() > RMAXINT)
+    CVC4::Rational rMaxInt(CVC4::String::maxSize());
+    if (node[2].getConst<Rational>() > rMaxInt)
     {
       // We know that, due to limitations on the size of string constants
       // in our implementation, that accessing a position greater than
-      // RMAXINT is guaranteed to be out of bounds.
+      // rMaxInt is guaranteed to be out of bounds.
       Node negone = nm->mkConst(Rational(-1));
       return returnRewrite(node, negone, "idof-max");
     }
     Assert(node[2].getConst<Rational>().sgn() >= 0);
-    unsigned start =
+    uint32_t start =
         node[2].getConst<Rational>().getNumerator().toUnsignedInt();
     CVC4::String s = children0[0].getConst<String>();
     CVC4::String t = node[1].getConst<String>();
@@ -2641,10 +2641,10 @@ bool TheoryStringsRewriter::stripSymbolicLength(std::vector<Node>& n1,
               // we can remove part of the constant
               // lower bound minus the length of a concrete string is negative,
               // hence lowerBound cannot be larger than long max
-              Assert(lbr < Rational(LONG_MAX));
+              Assert(lbr < Rational(String::maxSize()));
               curr = Rewriter::rewrite(NodeManager::currentNM()->mkNode(
                   kind::MINUS, curr, lowerBound));
-              unsigned lbsize = lbr.getNumerator().toUnsignedInt();
+              uint32_t lbsize = lbr.getNumerator().toUnsignedInt();
               Assert(lbsize < s.size());
               if (dir == 1)
               {
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; }
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index 8d68d4e86..34175a775 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -442,10 +442,8 @@ bool String::isDigit(unsigned character)
   return c >= '0' && c <= '9';
 }
 
-size_t String::maxSize()
-{
-  return std::numeric_limits<size_t>::max();
-}
+size_t String::maxSize() { return std::numeric_limits<uint32_t>::max(); }
+
 Rational String::toNumber() const
 {
   // when smt2 standard for strings is set, this may change, based on the
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 6400411cb..f707da219 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -503,6 +503,7 @@ REG0_TESTS = \
 	regress0/nl/magnitude-wrong-1020-m.smt2 \
 	regress0/nl/mult-po.smt2 \
 	regress0/nl/nia-wrong-tl.smt2 \
+	regress0/nl/nlExtPurify-test.smt2 \
 	regress0/nl/nta/cos-sig-value.smt2 \
 	regress0/nl/nta/exp-n0.5-lb.smt2 \
 	regress0/nl/nta/exp-n0.5-ub.smt2 \
@@ -1301,6 +1302,7 @@ REG1_TESTS = \
 	regress1/quantifiers/model_6_1_bv.smt2 \
 	regress1/quantifiers/mutualrec2.cvc \
 	regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 \
+	regress1/quantifiers/nl-pow-trick.smt2 \
 	regress1/quantifiers/nra-interleave-inst.smt2 \
 	regress1/quantifiers/opisavailable-12.smt2 \
 	regress1/quantifiers/parametric-lists.smt2 \
diff --git a/test/regress/regress0/nl/nlExtPurify-test.smt2 b/test/regress/regress0/nl/nlExtPurify-test.smt2
new file mode 100644
index 000000000..1a2391c3b
--- /dev/null
+++ b/test/regress/regress0/nl/nlExtPurify-test.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --nl-ext-purify
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_NRA)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun skoX () Real)
+(declare-fun skoS3 () Real)
+(declare-fun skoSX () Real)
+
+(assert (and (not (<= skoX 0)) (and (not (<= (* (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX) (+ skoS3 skoSX)) 0)) (not (<= skoS3 0)))))
+
+
+(check-sat)
+(exit)
diff --git a/test/regress/regress1/quantifiers/nl-pow-trick.smt2 b/test/regress/regress1/quantifiers/nl-pow-trick.smt2
new file mode 100644
index 000000000..a369fd9f9
--- /dev/null
+++ b/test/regress/regress1/quantifiers/nl-pow-trick.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --cbqi-all
+; EXPECT: unsat
+(set-logic NIA)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(define-fun s ((x Int)) Int (+ x 1))
+(define-fun seq ((a Int) (b Int) (k Int) (x Int)) Bool ( = x (mod (+ 1 (* b (+ 1 k))) a)))
+(define-fun power ((a Int) (b Int) (c Int)) Bool 
+(exists ((x Int) (y Int)) (and (seq x y 0 1) (seq x y b c) (forall ((k Int) (z Int)) (=> (and (< k b) (seq x y k z)) (seq x y (+ 1 k) (* a z))))))
+)
+(assert (power 2 3 8))
+(check-sat)