Refactor preprocessing pass registration (#2468)

This commit refactors how preprocessing pass registration works,
inspired by LLVM's approach [0]. The basic idea is that every
preprocessing pass declares a static variable of type `RegisterPass` in
its source file that registers the pass with the
`PreprocessingPassRegistry` when starting the program. The registry is a
singleton that keeps track of all the available passes and allows other
code to create instances of the passes (note: previously the registry
itself was owning the passes but this is no longer the case). One of the
advantages of this solution is that we have a list of available passes
directly at the beginning of the program, which is useful for example
when parsing options.

As a side effect, this commit also fixes the SortInference pass, which
was expecting arguments other than the preprocessing pass context in its
constructor.

This commit is required for fixing dumping pre/post preprocessing
passes. It is also the ground work for allowing the user to specify a
preprocessing pipeline using command-line arguments.

[0] https://llvm.org/docs/WritingAnLLVMPass.html

35 files changed, 290 insertions, 259 deletions

diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index f5c3520d0..59b628e3b 100644
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -18,6 +18,7 @@
 #include "preprocessing/passes/apply_substs.h"
 
 #include "context/cdo.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/rewriter.h"
 #include "theory/substitutions.h"
 
@@ -68,6 +69,8 @@ PreprocessingPassResult ApplySubsts::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<ApplySubsts> X("apply-substs");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/apply_to_const.cpp b/src/preprocessing/passes/apply_to_const.cpp
index bbe4439ec..65bdf5c1f 100644
--- a/src/preprocessing/passes/apply_to_const.cpp
+++ b/src/preprocessing/passes/apply_to_const.cpp
@@ -16,6 +16,7 @@
 
 #include "preprocessing/passes/apply_to_const.h"
 
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
@@ -103,6 +104,8 @@ PreprocessingPassResult ApplyToConst::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<ApplyToConst> X("apply-to-const");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index 4c08d7e47..15b0ee678 100644
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -20,6 +20,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
@@ -209,6 +210,8 @@ BoolToBV::Statistics::~Statistics()
   smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered);
 }
 
+static RegisterPass<BoolToBV> X("bool-to-bv");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp
index 27069de2f..addee305d 100644
--- a/src/preprocessing/passes/bv_abstraction.cpp
+++ b/src/preprocessing/passes/bv_abstraction.cpp
@@ -26,6 +26,7 @@
 #include <vector>
 
 #include "options/bv_options.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/rewriter.h"
 
@@ -60,6 +61,8 @@ PreprocessingPassResult BvAbstraction::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<BvAbstraction> X("bv-abstraction");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/bv_ackermann.cpp b/src/preprocessing/passes/bv_ackermann.cpp
index 26785f15b..01fa70b61 100644
--- a/src/preprocessing/passes/bv_ackermann.cpp
+++ b/src/preprocessing/passes/bv_ackermann.cpp
@@ -24,6 +24,7 @@
 #include "preprocessing/passes/bv_ackermann.h"
 
 #include "options/bv_options.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/bv/theory_bv_utils.h"
 
 using namespace CVC4;
@@ -213,6 +214,8 @@ PreprocessingPassResult BVAckermann::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<BVAckermann> X("bv-ackermann");
+
 /* -------------------------------------------------------------------------- */
 
 }  // namespace passes
diff --git a/src/preprocessing/passes/bv_eager_atoms.cpp b/src/preprocessing/passes/bv_eager_atoms.cpp
index fe43ebcd0..6b80a4e65 100644
--- a/src/preprocessing/passes/bv_eager_atoms.cpp
+++ b/src/preprocessing/passes/bv_eager_atoms.cpp
@@ -18,6 +18,7 @@
 
 #include "preprocessing/passes/bv_eager_atoms.h"
 
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/theory_model.h"
 
 namespace CVC4 {
@@ -42,6 +43,8 @@ PreprocessingPassResult BvEagerAtoms::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<BvEagerAtoms> X("bv-eager-atoms");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp
index 8b438dde4..ffecc8682 100644
--- a/src/preprocessing/passes/bv_gauss.cpp
+++ b/src/preprocessing/passes/bv_gauss.cpp
@@ -18,9 +18,10 @@
 #include "preprocessing/passes/bv_gauss.h"
 
 #include "expr/node.h"
-#include "theory/rewriter.h"
-#include "theory/bv/theory_bv_utils.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/rewriter.h"
 #include "util/bitvector.h"
 
 #include <unordered_map>
@@ -818,6 +819,8 @@ PreprocessingPassResult BVGauss::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<BVGauss> X("bv-gauss");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp
index 860aab5ca..82781b848 100644
--- a/src/preprocessing/passes/bv_intro_pow2.cpp
+++ b/src/preprocessing/passes/bv_intro_pow2.cpp
@@ -20,6 +20,7 @@
 
 #include <unordered_map>
 
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/rewriter.h"
 
@@ -98,6 +99,8 @@ PreprocessingPassResult BvIntroPow2::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<BvIntroPow2> X("bv-intro-pow2");
+
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */
 
diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp
index bcfdeb24f..c6d98705c 100644
--- a/src/preprocessing/passes/bv_to_bool.cpp
+++ b/src/preprocessing/passes/bv_to_bool.cpp
@@ -21,11 +21,11 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/rewriter.h"
-#include "theory/theory.h"
-
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/node_visitor.h"
+#include "theory/rewriter.h"
+#include "theory/theory.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -304,6 +304,8 @@ BVToBool::Statistics::~Statistics()
   smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLifted);
 }
 
+static RegisterPass<BVToBool> X("bv-to-bool");
+
 }  // passes
 }  // Preprocessing
 }  // CVC4
diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp
index 572aaed7a..8ca0a82ab 100644
--- a/src/preprocessing/passes/extended_rewriter_pass.cpp
+++ b/src/preprocessing/passes/extended_rewriter_pass.cpp
@@ -16,6 +16,7 @@
 
 #include "preprocessing/passes/extended_rewriter_pass.h"
 
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/quantifiers/extended_rewrite.h"
 
 namespace CVC4 {
@@ -37,6 +38,8 @@ PreprocessingPassResult ExtRewPre::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<ExtRewPre> X("ext-rew-pre");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp
index 8f48d417c..be4f08717 100644
--- a/src/preprocessing/passes/global_negate.cpp
+++ b/src/preprocessing/passes/global_negate.cpp
@@ -13,8 +13,11 @@
  **/
 
 #include "preprocessing/passes/global_negate.h"
+
 #include <vector>
+
 #include "expr/node.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/rewriter.h"
 
 using namespace std;
@@ -117,6 +120,8 @@ PreprocessingPassResult GlobalNegate::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<GlobalNegate> X("global-negate");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index 997705835..f4aa1cfe9 100644
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 
@@ -334,6 +335,8 @@ PreprocessingPassResult IntToBV::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<IntToBV> X("int-to-bv");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 86c40a793..bbc09b89c 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -16,6 +16,8 @@
  **/
 
 #include "preprocessing/passes/ite_removal.h"
+
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
@@ -44,6 +46,8 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<IteRemoval> X("ite-removal");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 137925f77..fbc22597d 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -14,13 +14,14 @@
 
 #include "preprocessing/passes/ite_simp.h"
 
+#include <vector>
+
 #include "options/proof_options.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/nary_builder.h"
 #include "theory/arith/arith_ite_utils.h"
 
-#include <vector>
-
 using namespace CVC4;
 using namespace CVC4::theory;
 
@@ -256,6 +257,8 @@ PreprocessingPassResult ITESimp::applyInternal(
               : PreprocessingPassResult::CONFLICT;
 }
 
+static RegisterPass<ITESimp> X("ite-simp");
+
 /* -------------------------------------------------------------------------- */
 
 }  // namespace passes
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 616ecd969..c45c6266e 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -19,6 +19,7 @@
 
 #include "expr/node_self_iterator.h"
 #include "options/arith_options.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/booleans/circuit_propagator.h"
@@ -659,6 +660,8 @@ MipLibTrick::Statistics::~Statistics()
   smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved);
 }
 
+static RegisterPass<MipLibTrick> X("miplib-trick");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp
index afb092571..630f35c14 100644
--- a/src/preprocessing/passes/nl_ext_purify.cpp
+++ b/src/preprocessing/passes/nl_ext_purify.cpp
@@ -16,6 +16,8 @@
 
 #include "preprocessing/passes/nl_ext_purify.h"
 
+#include "preprocessing/preprocessing_pass_registry.h"
+
 namespace CVC4 {
 namespace preprocessing {
 namespace passes {
@@ -125,6 +127,8 @@ PreprocessingPassResult NlExtPurify::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<NlExtPurify> X("nl-ext-purify");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 653aed8ad..d06143441 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -16,13 +16,14 @@
 
 #include "preprocessing/passes/non_clausal_simp.h"
 
+#include <vector>
+
 #include "context/cdo.h"
 #include "options/proof_options.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/theory_model.h"
 
-#include <vector>
-
 using namespace CVC4;
 using namespace CVC4::theory;
 
@@ -452,6 +453,8 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }  // namespace passes
 
+static RegisterPass<NonClausalSimp> X("non-clausal-simp");
+
 /* -------------------------------------------------------------------------- */
 
 }  // namespace passes
diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp
index c2cd7e34f..3d448ddf1 100644
--- a/src/preprocessing/passes/pseudo_boolean_processor.cpp
+++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp
@@ -18,6 +18,7 @@
 #include "preprocessing/passes/pseudo_boolean_processor.h"
 
 #include "base/output.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
 #include "theory/rewriter.h"
@@ -413,6 +414,8 @@ void PseudoBooleanProcessor::clear()
   d_neg.clear();
 }
 
+static RegisterPass<PseudoBooleanProcessor> X("pseudo-boolean-processor");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index e3bc02309..01416016a 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -20,6 +20,7 @@
 
 #include "options/quantifiers_modes.h"
 #include "options/quantifiers_options.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "proof/proof_manager.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
@@ -545,6 +546,8 @@ void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) {
   }
 }
 
+static RegisterPass<QuantifierMacros> X("quantifier-macros");
+
 }  // passes
 }  // preprocessing
 }  // CVC4
diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp
index e6c1557c0..5217bc807 100644
--- a/src/preprocessing/passes/quantifiers_preprocess.cpp
+++ b/src/preprocessing/passes/quantifiers_preprocess.cpp
@@ -20,6 +20,7 @@
 #include "preprocessing/passes/quantifiers_preprocess.h"
 
 #include "base/output.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/rewriter.h"
 
@@ -52,6 +53,8 @@ PreprocessingPassResult QuantifiersPreprocess::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<QuantifiersPreprocess> X("quantifiers-preprocess");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index c92f4b962..d15a19912 100644
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -18,6 +18,7 @@
 
 #include <string>
 
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
@@ -197,6 +198,8 @@ PreprocessingPassResult RealToInt::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<RealToInt> X("real-to-int");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp
index dff807d58..8d0f76c38 100644
--- a/src/preprocessing/passes/rewrite.cpp
+++ b/src/preprocessing/passes/rewrite.cpp
@@ -16,6 +16,7 @@
 
 #include "preprocessing/passes/rewrite.h"
 
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
@@ -39,6 +40,8 @@ PreprocessingPassResult Rewrite::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<Rewrite> X("rewrite");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp
index d79ec8b93..55ce1c5d1 100644
--- a/src/preprocessing/passes/sep_skolem_emp.cpp
+++ b/src/preprocessing/passes/sep_skolem_emp.cpp
@@ -20,6 +20,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
@@ -119,6 +120,8 @@ PreprocessingPassResult SepSkolemEmp::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<SepSkolemEmp> X("sep-skolem-emp");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp
index e2b0bfb59..f8faab9bc 100644
--- a/src/preprocessing/passes/sort_infer.cpp
+++ b/src/preprocessing/passes/sort_infer.cpp
@@ -16,7 +16,9 @@
 
 #include "options/smt_options.h"
 #include "options/uf_options.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/rewriter.h"
+#include "theory/sort_inference.h"
 
 using namespace std;
 
@@ -24,24 +26,25 @@ namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
-SortInferencePass::SortInferencePass(PreprocessingPassContext* preprocContext,
-                                     SortInference* si)
-    : PreprocessingPass(preprocContext, "sort-inference"), d_si(si)
+SortInferencePass::SortInferencePass(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "sort-inference")
 {
 }
 
 PreprocessingPassResult SortInferencePass::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
+  SortInference* si = d_preprocContext->getTheoryEngine()->getSortInference();
+
   if (options::sortInference())
   {
-    d_si->initialize(assertionsToPreprocess->ref());
+    si->initialize(assertionsToPreprocess->ref());
     std::map<Node, Node> model_replace_f;
     std::map<Node, std::map<TypeNode, Node> > visited;
     for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; i++)
     {
       Node prev = (*assertionsToPreprocess)[i];
-      Node next = d_si->simplify(prev, model_replace_f, visited);
+      Node next = si->simplify(prev, model_replace_f, visited);
       if (next != prev)
       {
         next = theory::Rewriter::rewrite(next);
@@ -53,7 +56,7 @@ PreprocessingPassResult SortInferencePass::applyInternal(
       }
     }
     std::vector<Node> newAsserts;
-    d_si->getNewAssertions(newAsserts);
+    si->getNewAssertions(newAsserts);
     for (const Node& na : newAsserts)
     {
       Node nar = theory::Rewriter::rewrite(na);
@@ -75,11 +78,13 @@ PreprocessingPassResult SortInferencePass::applyInternal(
   // using this option
   if (options::ufssFairnessMonotone())
   {
-    d_si->computeMonotonicity(assertionsToPreprocess->ref());
+    si->computeMonotonicity(assertionsToPreprocess->ref());
   }
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<SortInferencePass> X("sort-inference");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/sort_infer.h b/src/preprocessing/passes/sort_infer.h
index e56d7ab60..7c913e9cf 100644
--- a/src/preprocessing/passes/sort_infer.h
+++ b/src/preprocessing/passes/sort_infer.h
@@ -18,11 +18,10 @@
 #include <map>
 #include <string>
 #include <vector>
-#include "expr/node.h"
 
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
-#include "theory/sort_inference.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -36,19 +35,11 @@ namespace passes {
 class SortInferencePass : public PreprocessingPass
 {
  public:
-  SortInferencePass(PreprocessingPassContext* preprocContext,
-                    SortInference* si);
+  SortInferencePass(PreprocessingPassContext* preprocContext);
 
  protected:
   PreprocessingPassResult applyInternal(
       AssertionPipeline* assertionsToPreprocess) override;
-
- private:
-  /**
-   * Pointer to the sort inference module. This should be the sort inference
-   * belonging to the theory engine of the current SMT engine.
-   */
-  SortInference* d_si;
 };
 
 }  // namespace passes
diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp
index 0a792b5d4..df116166d 100644
--- a/src/preprocessing/passes/static_learning.cpp
+++ b/src/preprocessing/passes/static_learning.cpp
@@ -18,6 +18,7 @@
 #include <string>
 
 #include "expr/node.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -50,6 +51,8 @@ PreprocessingPassResult StaticLearning::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<StaticLearning> X("static-learning");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index eb8835623..09db93cbc 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -14,6 +14,7 @@
 
 #include "preprocessing/passes/sygus_inference.h"
 
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
@@ -316,6 +317,8 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions,
   return true;
 }
 
+static RegisterPass<SygusInference> X("sygus-infer");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/symmetry_breaker.cpp b/src/preprocessing/passes/symmetry_breaker.cpp
index 1e4b9853d..92065b2a0 100644
--- a/src/preprocessing/passes/symmetry_breaker.cpp
+++ b/src/preprocessing/passes/symmetry_breaker.cpp
@@ -13,7 +13,9 @@
  **/
 
 #include "preprocessing/passes/symmetry_breaker.h"
+
 #include "preprocessing/passes/symmetry_detect.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -175,6 +177,8 @@ PreprocessingPassResult SymBreakerPass::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<SymBreakerPass> X("sym-break");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/symmetry_detect.cpp b/src/preprocessing/passes/symmetry_detect.cpp
index 24db144e4..ec784a6ba 100644
--- a/src/preprocessing/passes/symmetry_detect.cpp
+++ b/src/preprocessing/passes/symmetry_detect.cpp
@@ -13,6 +13,7 @@
  **/
 
 #include "preprocessing/passes/symmetry_detect.h"
+
 #include "expr/node_algorithm.h"
 #include "theory/quantifiers/alpha_equivalence.h"
 #include "theory/quantifiers/term_util.h"
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index e3e3a548a..47c24bb5e 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -17,6 +17,7 @@
 
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "printer/printer.h"
 #include "theory/quantifiers/candidate_rewrite_database.h"
 
@@ -154,6 +155,8 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<SynthRewRulesPass> X("synth-rr");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index edb0fc800..a5d054c8b 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -16,6 +16,7 @@
 
 #include "preprocessing/passes/theory_preprocess.h"
 
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 
@@ -44,6 +45,8 @@ PreprocessingPassResult TheoryPreprocess::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<TheoryPreprocess> X("theory-preprocess");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 6bb46f3f2..52d378305 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -18,6 +18,7 @@
 
 #include "preprocessing/passes/unconstrained_simplifier.h"
 
+#include "preprocessing/preprocessing_pass_registry.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/logic_info.h"
 #include "theory/rewriter.h"
@@ -842,6 +843,8 @@ PreprocessingPassResult UnconstrainedSimplifier::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+static RegisterPass<UnconstrainedSimplifier> X("unconstrained-simplifier");
+
 }  // namespace passes
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp
index 03aaec46a..a50cd2541 100644
--- a/src/preprocessing/preprocessing_pass_registry.cpp
+++ b/src/preprocessing/preprocessing_pass_registry.cpp
@@ -11,11 +11,14 @@
  **
  ** \brief The preprocessing pass registry
  **
- ** The preprocessing pass registry.
+ ** This file defines the classes PreprocessingPassRegistry, which keeps track
+ ** of the available preprocessing passes, and RegisterPass, which registers a
+ ** preprocessing pass with the registry.
  **/
 
 #include "preprocessing/preprocessing_pass_registry.h"
 
+#include <algorithm>
 #include <utility>
 
 #include "base/cvc4_assert.h"
@@ -25,29 +28,39 @@
 namespace CVC4 {
 namespace preprocessing {
 
-void PreprocessingPassRegistry::registerPass(
-    const std::string& ppName,
-    std::unique_ptr<PreprocessingPass> preprocessingPass) {
-  Debug("pp-registry") << "Registering pass " << ppName << std::endl;
-  Assert(preprocessingPass != nullptr);
-  Assert(!this->hasPass(ppName));
-  d_stringToPreprocessingPass[ppName] = std::move(preprocessingPass);
+PreprocessingPassRegistry& PreprocessingPassRegistry::getInstance()
+{
+  static PreprocessingPassRegistry* ppReg = new PreprocessingPassRegistry();
+  return *ppReg;
+}
+
+void PreprocessingPassRegistry::registerPassInfo(
+    const std::string& name,
+    std::function<PreprocessingPass*(PreprocessingPassContext*)> ctor)
+{
+  d_ppInfo[name] = ctor;
 }
 
-bool PreprocessingPassRegistry::hasPass(const std::string& ppName) {
-  return d_stringToPreprocessingPass.find(ppName) !=
-         d_stringToPreprocessingPass.end();
+PreprocessingPass* PreprocessingPassRegistry::createPass(
+    PreprocessingPassContext* ppCtx, const std::string& name)
+{
+  return d_ppInfo[name](ppCtx);
 }
 
-PreprocessingPass* PreprocessingPassRegistry::getPass(
-    const std::string& ppName) {
-  Assert(this->hasPass(ppName));
-  return d_stringToPreprocessingPass[ppName].get();
+std::vector<std::string> PreprocessingPassRegistry::getAvailablePasses()
+{
+  std::vector<std::string> passes;
+  for (const auto& info : d_ppInfo)
+  {
+    passes.push_back(info.first);
+  }
+  std::sort(passes.begin(), passes.end());
+  return passes;
 }
 
-void PreprocessingPassRegistry::unregisterPasses()
+bool PreprocessingPassRegistry::hasPass(const std::string& name)
 {
-  d_stringToPreprocessingPass.clear();
+  return d_ppInfo.find(name) != d_ppInfo.end();
 }
 
 }  // namespace preprocessing
diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h
index 30a2db579..44e9b4e6e 100644
--- a/src/preprocessing/preprocessing_pass_registry.h
+++ b/src/preprocessing/preprocessing_pass_registry.h
@@ -11,9 +11,9 @@
  **
  ** \brief The preprocessing pass registry
  **
- ** The preprocessing pass registry keeps track of all the instances of
- ** preprocessing passes. Upon creation, preprocessing passes are registered in
- ** the registry, which then takes ownership of them.
+ ** This file defines the classes PreprocessingPassRegistry, which keeps track
+ ** of the available preprocessing passes, and RegisterPass, which registers a
+ ** preprocessing pass with the registry.
  **/
 #include "cvc4_private.h"
 
@@ -29,32 +29,102 @@
 namespace CVC4 {
 namespace preprocessing {
 
+class PreprocessingPassContext;
+
+/**
+ * The PreprocessingPassRegistry keeps track of the available preprocessing
+ * passes and how to create instances of those passes. This class is intended
+ * to be used as a singleton and can be shared between threads (assuming that
+ * the memory allocator is thread-safe) as well as different solver instances.
+ */
 class PreprocessingPassRegistry {
  public:
   /**
-   *  Registers a pass with a unique name and takes ownership of it.
+   * Gets the single instance of this class.
    */
-  void registerPass(const std::string& ppName,
-                    std::unique_ptr<PreprocessingPass> preprocessingPass);
+  static PreprocessingPassRegistry& getInstance();
 
   /**
-   * Retrieves a pass with a given name from registry.
+   * Registers a pass. Do not call this directly, use the `RegisterPass` class
+   * instead.
+   *
+   * @param name The name of the preprocessing pass to register
+   * @param ctor A function that creates an instance of the pass given a
+   *             preprocessing pass context
    */
-  PreprocessingPass* getPass(const std::string& ppName);
+  void registerPassInfo(
+      const std::string& name,
+      std::function<PreprocessingPass*(PreprocessingPassContext*)> ctor);
 
   /**
-   Clears all passes from the registry.
+   * Creates an instance of a pass.
+   *
+   * @param ppCtx The preprocessing pass context to pass to the preprocessing
+   *              pass constructor
+   * @param name The name of the pass to create an instance of
    */
-  void unregisterPasses();
+  PreprocessingPass* createPass(PreprocessingPassContext* ppCtx,
+                                const std::string& name);
 
- private:
-  bool hasPass(const std::string& ppName);
+  /**
+   * Returns a sorted list of available preprocessing passes.
+   */
+  std::vector<std::string> getAvailablePasses();
 
-  /* Stores all the registered preprocessing passes. */
-  std::unordered_map<std::string, std::unique_ptr<PreprocessingPass>>
-      d_stringToPreprocessingPass;
+  /**
+   * Checks whether a pass with a given name is available.
+   *
+   * @param name The name of the pass to check for
+   */
+  bool hasPass(const std::string& name);
+
+ private:
+  /**
+   * Map of available preprocessing passes, mapping from preprocessing pass
+   * name to a function that constructs a corresponding instance.
+   */
+  std::unordered_map<
+      std::string,
+      std::function<PreprocessingPass*(PreprocessingPassContext*)> >
+      d_ppInfo;
 };  // class PreprocessingPassRegistry
 
+/**
+ * Class used to register a preprocessing pass. In the source file of a given
+ * pass, create a static instance of this class, e.g.:
+ *
+ * static RegisterPass<MyPass> X("my-pass");
+ *
+ * where `MyPass` is the class of your pass and "my-pass" is its name. This
+ * registers the pass with the `PreprocessingPassRegistry`.
+ */
+template <class T>
+class RegisterPass
+{
+ public:
+  /**
+   * Creates a new preprocessing pass registration.
+   *
+   * @param name The name that should be associated with the preprocessing pass
+   */
+  RegisterPass(const std::string& name)
+  {
+    PreprocessingPassRegistry::getInstance().registerPassInfo(name, callCtor);
+  }
+
+  /**
+   * This method is used by the `PreprocessingPassRegistry` to create a new
+   * instance of the preprocessing pass T.
+   *
+   * @param ppCtx The preprocessing pass context passed to the constructor of
+   *              the preprocessing pass
+   */
+  static PreprocessingPass* callCtor(PreprocessingPassContext* ppCtx)
+  {
+    return new T(ppCtx);
+  }
+};  // class RegisterPass
+
 }  // namespace preprocessing
 }  // namespace CVC4
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 15f8280b5..b133f3a36 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -70,37 +70,6 @@
 #include "options/strings_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
-#include "preprocessing/passes/apply_substs.h"
-#include "preprocessing/passes/apply_to_const.h"
-#include "preprocessing/passes/bool_to_bv.h"
-#include "preprocessing/passes/bv_abstraction.h"
-#include "preprocessing/passes/bv_ackermann.h"
-#include "preprocessing/passes/bv_eager_atoms.h"
-#include "preprocessing/passes/bv_gauss.h"
-#include "preprocessing/passes/bv_intro_pow2.h"
-#include "preprocessing/passes/bv_to_bool.h"
-#include "preprocessing/passes/extended_rewriter_pass.h"
-#include "preprocessing/passes/global_negate.h"
-#include "preprocessing/passes/int_to_bv.h"
-#include "preprocessing/passes/ite_removal.h"
-#include "preprocessing/passes/ite_simp.h"
-#include "preprocessing/passes/miplib_trick.h"
-#include "preprocessing/passes/nl_ext_purify.h"
-#include "preprocessing/passes/non_clausal_simp.h"
-#include "preprocessing/passes/pseudo_boolean_processor.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"
-#include "preprocessing/passes/sep_skolem_emp.h"
-#include "preprocessing/passes/sort_infer.h"
-#include "preprocessing/passes/static_learning.h"
-#include "preprocessing/passes/sygus_inference.h"
-#include "preprocessing/passes/symmetry_breaker.h"
-#include "preprocessing/passes/symmetry_detect.h"
-#include "preprocessing/passes/synth_rew_rules.h"
-#include "preprocessing/passes/theory_preprocess.h"
-#include "preprocessing/passes/unconstrained_simplifier.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "preprocessing/preprocessing_pass_registry.h"
@@ -145,7 +114,6 @@ using namespace std;
 using namespace CVC4;
 using namespace CVC4::smt;
 using namespace CVC4::preprocessing;
-using namespace CVC4::preprocessing::passes;
 using namespace CVC4::prop;
 using namespace CVC4::context;
 using namespace CVC4::theory;
@@ -531,7 +499,12 @@ class SmtEnginePrivate : public NodeManagerListener {
 
  private:
   std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext;
-  PreprocessingPassRegistry d_preprocessingPassRegistry;
+
+  /**
+   * Map of preprocessing pass instances, mapping from names to preprocessing
+   * pass instance
+   */
+  std::unordered_map<std::string, std::unique_ptr<PreprocessingPass>> d_passes;
 
   /**
    * Helper function to fix up assertion list to restore invariants needed after
@@ -639,10 +612,7 @@ class SmtEnginePrivate : public NodeManagerListener {
     d_smt.d_nodeManager->unsubscribeEvents(this);
   }
 
-  void unregisterPreprocessingPasses()
-  {
-    d_preprocessingPassRegistry.unregisterPasses();
-  }
+  void cleanupPreprocessingPasses() { d_passes.clear(); }
 
   ResourceManager* getResourceManager() { return d_resourceManager; }
   void spendResource(unsigned amount)
@@ -1055,7 +1025,7 @@ SmtEngine::~SmtEngine()
     d_fmfRecFunctionsDefined->deleteSelf();
 
     //destroy all passes before destroying things that they refer to
-    d_private->unregisterPreprocessingPasses();
+    d_private->cleanupPreprocessingPasses();
 
     delete d_theoryEngine;
     d_theoryEngine = NULL;
@@ -2558,121 +2528,19 @@ bool SmtEngine::isDefinedFunction( Expr func ){
 
 void SmtEnginePrivate::finishInit()
 {
+  PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
   d_preprocessingPassContext.reset(new PreprocessingPassContext(
       &d_smt, d_resourceManager, &d_iteRemover, &d_propagator));
-  // TODO: register passes here (this will likely change when we add support for
-  // actually assembling preprocessing pipelines).
-  std::unique_ptr<ApplySubsts> applySubsts(
-      new ApplySubsts(d_preprocessingPassContext.get()));
-  std::unique_ptr<ApplyToConst> applyToConst(
-      new ApplyToConst(d_preprocessingPassContext.get()));
-  std::unique_ptr<BoolToBV> boolToBv(
-      new BoolToBV(d_preprocessingPassContext.get()));
-  std::unique_ptr<BvAbstraction> bvAbstract(
-      new BvAbstraction(d_preprocessingPassContext.get()));
-  std::unique_ptr<BvEagerAtoms> bvEagerAtoms(
-      new BvEagerAtoms(d_preprocessingPassContext.get()));
-  std::unique_ptr<BVAckermann> bvAckermann(
-      new BVAckermann(d_preprocessingPassContext.get()));
-  std::unique_ptr<BVGauss> bvGauss(
-      new BVGauss(d_preprocessingPassContext.get()));
-  std::unique_ptr<BvIntroPow2> bvIntroPow2(
-      new BvIntroPow2(d_preprocessingPassContext.get()));
-  std::unique_ptr<BVToBool> bvToBool(
-      new BVToBool(d_preprocessingPassContext.get()));
-  std::unique_ptr<ExtRewPre> extRewPre(
-      new ExtRewPre(d_preprocessingPassContext.get()));
-  std::unique_ptr<GlobalNegate> globalNegate(
-      new GlobalNegate(d_preprocessingPassContext.get()));
-  std::unique_ptr<IntToBV> intToBV(
-      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<NonClausalSimp> nonClausalSimp(
-      new NonClausalSimp(d_preprocessingPassContext.get()));
-  std::unique_ptr<MipLibTrick> mipLibTrick(
-      new MipLibTrick(d_preprocessingPassContext.get()));
-  std::unique_ptr<QuantifiersPreprocess> quantifiersPreprocess(
-      new QuantifiersPreprocess(d_preprocessingPassContext.get()));
-  std::unique_ptr<PseudoBooleanProcessor> pbProc(
-      new PseudoBooleanProcessor(d_preprocessingPassContext.get()));
-  std::unique_ptr<IteRemoval> iteRemoval(
-      new IteRemoval(d_preprocessingPassContext.get()));
-  std::unique_ptr<RealToInt> realToInt(
-      new RealToInt(d_preprocessingPassContext.get()));
-  std::unique_ptr<Rewrite> rewrite(
-      new Rewrite(d_preprocessingPassContext.get()));
-  std::unique_ptr<SortInferencePass> sortInfer(
-      new SortInferencePass(d_preprocessingPassContext.get(),
-                            d_smt.d_theoryEngine->getSortInference()));
-  std::unique_ptr<StaticLearning> staticLearning(
-      new StaticLearning(d_preprocessingPassContext.get()));
-  std::unique_ptr<SygusInference> sygusInfer(
-      new SygusInference(d_preprocessingPassContext.get()));
-  std::unique_ptr<SymBreakerPass> sbProc(
-      new SymBreakerPass(d_preprocessingPassContext.get()));
-  std::unique_ptr<SynthRewRulesPass> srrProc(
-      new SynthRewRulesPass(d_preprocessingPassContext.get()));
-  std::unique_ptr<SepSkolemEmp> sepSkolemEmp(
-      new SepSkolemEmp(d_preprocessingPassContext.get()));
-  std::unique_ptr<TheoryPreprocess> theoryPreprocess(
-      new TheoryPreprocess(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",
-                                           std::move(applyToConst));
-  d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv));
-  d_preprocessingPassRegistry.registerPass("bv-abstraction",
-                                           std::move(bvAbstract));
-  d_preprocessingPassRegistry.registerPass("bv-ackermann",
-                                           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));
-  d_preprocessingPassRegistry.registerPass("bv-to-bool", std::move(bvToBool));
-  d_preprocessingPassRegistry.registerPass("ext-rew-pre", std::move(extRewPre));
-  d_preprocessingPassRegistry.registerPass("global-negate",
-                                           std::move(globalNegate));
-  d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
-  d_preprocessingPassRegistry.registerPass("ite-removal",
-                                           std::move(iteRemoval));
-  d_preprocessingPassRegistry.registerPass("ite-simp", std::move(iteSimp));
-  d_preprocessingPassRegistry.registerPass("nl-ext-purify",
-                                           std::move(nlExtPurify));
-  d_preprocessingPassRegistry.registerPass("non-clausal-simp",
-                                           std::move(nonClausalSimp));
-  d_preprocessingPassRegistry.registerPass("miplib-trick",
-                                           std::move(mipLibTrick));
-  d_preprocessingPassRegistry.registerPass("quantifiers-preprocess",
-                                           std::move(quantifiersPreprocess));
-  d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor",
-                                           std::move(pbProc));
-  d_preprocessingPassRegistry.registerPass("real-to-int", std::move(realToInt));
-  d_preprocessingPassRegistry.registerPass("rewrite", std::move(rewrite));
-  d_preprocessingPassRegistry.registerPass("sep-skolem-emp",
-                                           std::move(sepSkolemEmp));
-  d_preprocessingPassRegistry.registerPass("sort-inference",
-                                           std::move(sortInfer));
-  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("theory-preprocess",
-                                           std::move(theoryPreprocess));
-  d_preprocessingPassRegistry.registerPass("quantifier-macros",
-                                           std::move(quantifierMacros));
-  d_preprocessingPassRegistry.registerPass("unconstrained-simplifier",
-                                           std::move(unconstrainedSimplifier));
+
+  // TODO: this will likely change when we add support for actually assembling
+  // preprocessing pipelines. For now, we just create an instance of each
+  // available preprocessing pass.
+  std::vector<std::string> passNames = ppReg.getAvailablePasses();
+  for (const std::string& passName : passNames)
+  {
+    d_passes[passName].reset(
+        ppReg.createPass(d_preprocessingPassContext.get(), passName));
+  }
 }
 
 Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
@@ -2874,6 +2742,8 @@ static void dumpAssertions(const char* key,
 // returns false if simplification led to "false"
 bool SmtEnginePrivate::simplifyAssertions()
 {
+  PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
+
   spendResource(options::preprocessStep());
   Assert(d_smt.d_pendingPops == 0);
   try {
@@ -2887,8 +2757,7 @@ bool SmtEnginePrivate::simplifyAssertions()
       {
         // Perform non-clausal simplification
         PreprocessingPassResult res =
-            d_preprocessingPassRegistry.getPass("non-clausal-simp")
-                ->apply(&d_assertions);
+            d_passes["non-clausal-simp"]->apply(&d_assertions);
         if (res == PreprocessingPassResult::CONFLICT)
         {
           return false;
@@ -2908,8 +2777,7 @@ bool SmtEnginePrivate::simplifyAssertions()
           // re-simplification, which we don't expect to be useful anyway)
           d_assertions.getRealAssertionsEnd() == d_assertions.size())
       {
-        d_preprocessingPassRegistry.getPass("miplib-trick")
-            ->apply(&d_assertions);
+        d_passes["miplib-trick"]->apply(&d_assertions);
       } else {
         Trace("simplify") << "SmtEnginePrivate::simplify(): "
                           << "skipping miplib pseudobooleans pass (either incrementalSolving is on, or miplib pbs are turned off)..." << endl;
@@ -2924,16 +2792,14 @@ bool SmtEnginePrivate::simplifyAssertions()
     // Theory preprocessing
     if (d_smt.d_earlyTheoryPP)
     {
-      d_preprocessingPassRegistry.getPass("theory-preprocess")
-          ->apply(&d_assertions);
+      d_passes["theory-preprocess"]->apply(&d_assertions);
     }
 
     // ITE simplification
     if (options::doITESimp()
         && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat()))
     {
-      PreprocessingPassResult res =
-          d_preprocessingPassRegistry.getPass("ite-simp")->apply(&d_assertions);
+      PreprocessingPassResult res = d_passes["ite-simp"]->apply(&d_assertions);
       if (res == PreprocessingPassResult::CONFLICT)
       {
         Chat() << "...ITE simplification found unsat..." << endl;
@@ -2945,8 +2811,7 @@ bool SmtEnginePrivate::simplifyAssertions()
 
     // Unconstrained simplification
     if(options::unconstrainedSimp()) {
-      d_preprocessingPassRegistry.getPass("unconstrained-simplifier")
-          ->apply(&d_assertions);
+      d_passes["unconstrained-simplifier"]->apply(&d_assertions);
     }
 
     if (options::repeatSimp()
@@ -2954,8 +2819,7 @@ bool SmtEnginePrivate::simplifyAssertions()
         && !options::unsatCores() && !options::fewerPreprocessingHoles())
     {
       PreprocessingPassResult res =
-          d_preprocessingPassRegistry.getPass("non-clausal-simp")
-              ->apply(&d_assertions);
+          d_passes["non-clausal-simp"]->apply(&d_assertions);
       if (res == PreprocessingPassResult::CONFLICT)
       {
         return false;
@@ -3108,6 +2972,8 @@ void SmtEnginePrivate::processAssertions() {
   SubstitutionMap& top_level_substs =
       d_preprocessingPassContext->getTopLevelSubstitutions();
 
+  PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
+
   // Dump the assertions
   dumpAssertions("pre-everything", d_assertions);
 
@@ -3123,7 +2989,7 @@ void SmtEnginePrivate::processAssertions() {
 
   if (options::bvGaussElim())
   {
-    d_preprocessingPassRegistry.getPass("bv-gauss")->apply(&d_assertions);
+    d_passes["bv-gauss"]->apply(&d_assertions);
   }
 
   if (d_assertionsProcessed && options::incrementalSolving()) {
@@ -3171,12 +3037,12 @@ void SmtEnginePrivate::processAssertions() {
   if (options::globalNegate())
   {
     // global negation of the formula
-    d_preprocessingPassRegistry.getPass("global-negate")->apply(&d_assertions);
+    d_passes["global-negate"]->apply(&d_assertions);
     d_smt.d_globalNegation = !d_smt.d_globalNegation;
   }
 
   if( options::nlExtPurify() ){
-    d_preprocessingPassRegistry.getPass("nl-ext-purify")->apply(&d_assertions);
+    d_passes["nl-ext-purify"]->apply(&d_assertions);
   }
 
   if( options::ceGuidedInst() ){
@@ -3189,12 +3055,12 @@ void SmtEnginePrivate::processAssertions() {
   }
 
   if (options::solveRealAsInt()) {
-    d_preprocessingPassRegistry.getPass("real-to-int")->apply(&d_assertions);
+    d_passes["real-to-int"]->apply(&d_assertions);
   }
 
   if (options::solveIntAsBV() > 0)
   {
-    d_preprocessingPassRegistry.getPass("int-to-bv")->apply(&d_assertions);
+    d_passes["int-to-bv"]->apply(&d_assertions);
   }
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
@@ -3209,12 +3075,12 @@ void SmtEnginePrivate::processAssertions() {
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
       && !options::incrementalSolving())
   {
-    d_preprocessingPassRegistry.getPass("bv-ackermann")->apply(&d_assertions);
+    d_passes["bv-ackermann"]->apply(&d_assertions);
   }
 
   if (options::bvAbstraction() && !options::incrementalSolving())
   {
-    d_preprocessingPassRegistry.getPass("bv-abstraction")->apply(&d_assertions);
+    d_passes["bv-abstraction"]->apply(&d_assertions);
   }
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
@@ -3223,30 +3089,29 @@ void SmtEnginePrivate::processAssertions() {
 
   if (options::extRewPrep())
   {
-    d_preprocessingPassRegistry.getPass("ext-rew-pre")->apply(&d_assertions);
+    d_passes["ext-rew-pre"]->apply(&d_assertions);
   }
 
   // Unconstrained simplification
   if(options::unconstrainedSimp()) {
-    d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions);
-    d_preprocessingPassRegistry.getPass("unconstrained-simplifier")
-        ->apply(&d_assertions);
+    d_passes["rewrite"]->apply(&d_assertions);
+    d_passes["unconstrained-simplifier"]->apply(&d_assertions);
   }
 
   if(options::bvIntroducePow2())
   {
-    d_preprocessingPassRegistry.getPass("bv-intro-pow2")->apply(&d_assertions);
+    d_passes["bv-intro-pow2"]->apply(&d_assertions);
   }
 
   if (options::unsatCores())
   {
     // special rewriting pass for unsat cores, since many of the passes below
     // are skipped
-    d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions);
+    d_passes["rewrite"]->apply(&d_assertions);
   }
   else
   {
-    d_preprocessingPassRegistry.getPass("apply-substs")->apply(&d_assertions);
+    d_passes["apply-substs"]->apply(&d_assertions);
   }
 
   // Assertions ARE guaranteed to be rewritten by this point
@@ -3260,25 +3125,23 @@ void SmtEnginePrivate::processAssertions() {
   // Lift bit-vectors of size 1 to bool
   if (options::bitvectorToBool())
   {
-    d_preprocessingPassRegistry.getPass("bv-to-bool")->apply(&d_assertions);
+    d_passes["bv-to-bool"]->apply(&d_assertions);
   }
   // Convert non-top-level Booleans to bit-vectors of size 1
   if (options::boolToBitvector())
   {
-    d_preprocessingPassRegistry.getPass("bool-to-bv")->apply(&d_assertions);
+    d_passes["bool-to-bv"]->apply(&d_assertions);
   }
   if(options::sepPreSkolemEmp()) {
-    d_preprocessingPassRegistry.getPass("sep-skolem-emp")->apply(&d_assertions);
+    d_passes["sep-skolem-emp"]->apply(&d_assertions);
   }
 
   if( d_smt.d_logic.isQuantified() ){
     //remove rewrite rules, apply pre-skolemization to existential quantifiers
-    d_preprocessingPassRegistry.getPass("quantifiers-preprocess")
-        ->apply(&d_assertions);
+    d_passes["quantifiers-preprocess"]->apply(&d_assertions);
     if( options::macrosQuant() ){
       //quantifiers macro expansion
-      d_preprocessingPassRegistry.getPass("quantifier-macros")
-          ->apply(&d_assertions);
+      d_passes["quantifier-macros"]->apply(&d_assertions);
     }
 
     //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF
@@ -3312,23 +3175,22 @@ void SmtEnginePrivate::processAssertions() {
     }
     if (options::sygusInference())
     {
-      d_preprocessingPassRegistry.getPass("sygus-infer")->apply(&d_assertions);
+      d_passes["sygus-infer"]->apply(&d_assertions);
     }
   }
 
   if( options::sortInference() || options::ufssFairnessMonotone() ){
-    d_preprocessingPassRegistry.getPass("sort-inference")->apply(&d_assertions);
+    d_passes["sort-inference"]->apply(&d_assertions);
   }
 
   if( options::pbRewrites() ){
-    d_preprocessingPassRegistry.getPass("pseudo-boolean-processor")
-        ->apply(&d_assertions);
+    d_passes["pseudo-boolean-processor"]->apply(&d_assertions);
   }
 
   if (options::synthRrPrep())
   {
     // do candidate rewrite rule synthesis
-    d_preprocessingPassRegistry.getPass("synth-rr")->apply(&d_assertions);
+    d_passes["synth-rr"]->apply(&d_assertions);
   }
 
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-simplify" << endl;
@@ -3344,22 +3206,21 @@ void SmtEnginePrivate::processAssertions() {
   if (options::symmetryBreakerExp() && !options::incrementalSolving())
   {
     // apply symmetry breaking if not in incremental mode
-    d_preprocessingPassRegistry.getPass("sym-break")->apply(&d_assertions);
+    d_passes["sym-break"]->apply(&d_assertions);
   }
 
   if(options::doStaticLearning()) {
-    d_preprocessingPassRegistry.getPass("static-learning")
-        ->apply(&d_assertions);
+    d_passes["static-learning"]->apply(&d_assertions);
   }
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
   {
     d_smt.d_stats->d_numAssertionsPre += d_assertions.size();
-    d_preprocessingPassRegistry.getPass("ite-removal")->apply(&d_assertions);
+    d_passes["ite-removal"]->apply(&d_assertions);
     // This is needed because when solving incrementally, removeITEs may introduce
     // skolems that were solved for earlier and thus appear in the substitution
     // map.
-    d_preprocessingPassRegistry.getPass("apply-substs")->apply(&d_assertions);
+    d_passes["apply-substs"]->apply(&d_assertions);
     d_smt.d_stats->d_numAssertionsPost += d_assertions.size();
   }
 
@@ -3429,8 +3290,8 @@ void SmtEnginePrivate::processAssertions() {
       }
       // TODO(b/1256): For some reason this is needed for some benchmarks, such as
       // QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
-      d_preprocessingPassRegistry.getPass("ite-removal")->apply(&d_assertions);
-      d_preprocessingPassRegistry.getPass("apply-substs")->apply(&d_assertions);
+      d_passes["ite-removal"]->apply(&d_assertions);
+      d_passes["apply-substs"]->apply(&d_assertions);
       //      Assert(iteRewriteAssertionsEnd == d_assertions.size());
     }
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl;
@@ -3439,7 +3300,7 @@ void SmtEnginePrivate::processAssertions() {
 
   if (options::rewriteApplyToConst())
   {
-    d_preprocessingPassRegistry.getPass("apply-to-const")->apply(&d_assertions);
+    d_passes["apply-to-const"]->apply(&d_assertions);
   }
 
   // begin: INVARIANT to maintain: no reordering of assertions or
@@ -3453,12 +3314,11 @@ void SmtEnginePrivate::processAssertions() {
   Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
-  d_preprocessingPassRegistry.getPass("theory-preprocess")
-      ->apply(&d_assertions);
+  d_passes["theory-preprocess"]->apply(&d_assertions);
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
   {
-    d_preprocessingPassRegistry.getPass("bv-eager-atoms")->apply(&d_assertions);
+    d_passes["bv-eager-atoms"]->apply(&d_assertions);
   }
 
   //notify theory engine new preprocessed assertions