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

34 files changed, 230 insertions, 59 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