From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 2 Oct 2018 21:55:21 +0000 (-0700)
Subject: Make registration of preprocessing passes explicit (#2564)
X-Git-Tag: cvc5-1.0.0~4473
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=937d37ef78d3ef445335928d498422083df74d77;p=cvc5.git

Make registration of preprocessing passes explicit (#2564)

As it turns out, self-registering types are problematic with static
linkage [0]. Instead of fixing the issue with linker flags, which seems
possible but also brittle (e.g. the flags may be different for different
linkers), this commit adds an explicit registration of each
preprocessing pass.

[0] https://www.bfilipek.com/2018/02/static-vars-static-lib.html
---

diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index 59b628e3b..f5c3520d0 100644
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -18,7 +18,6 @@
 #include "preprocessing/passes/apply_substs.h"
 
 #include "context/cdo.h"
-#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/rewriter.h"
 #include "theory/substitutions.h"
 
@@ -69,8 +68,6 @@ 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 65bdf5c1f..653a915d5 100644
--- a/src/preprocessing/passes/apply_to_const.cpp
+++ b/src/preprocessing/passes/apply_to_const.cpp
@@ -16,7 +16,6 @@
 
 #include "preprocessing/passes/apply_to_const.h"
 
-#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
@@ -104,7 +103,6 @@ PreprocessingPassResult ApplyToConst::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<ApplyToConst> X("apply-to-const");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index 15b0ee678..c8a59bdc4 100644
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -20,7 +20,6 @@
 #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"
@@ -210,7 +209,6 @@ BoolToBV::Statistics::~Statistics()
   smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered);
 }
 
-static RegisterPass<BoolToBV> X("bool-to-bv");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp
index addee305d..27648b45d 100644
--- a/src/preprocessing/passes/bv_abstraction.cpp
+++ b/src/preprocessing/passes/bv_abstraction.cpp
@@ -26,7 +26,6 @@
 #include <vector>
 
 #include "options/bv_options.h"
-#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/rewriter.h"
 
@@ -61,7 +60,6 @@ PreprocessingPassResult BvAbstraction::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<BvAbstraction> X("bv-abstraction");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/bv_ackermann.cpp b/src/preprocessing/passes/bv_ackermann.cpp
index 01fa70b61..2ec49b985 100644
--- a/src/preprocessing/passes/bv_ackermann.cpp
+++ b/src/preprocessing/passes/bv_ackermann.cpp
@@ -24,7 +24,6 @@
 #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;
@@ -214,7 +213,6 @@ PreprocessingPassResult BVAckermann::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<BVAckermann> X("bv-ackermann");
 
 /* -------------------------------------------------------------------------- */
 
diff --git a/src/preprocessing/passes/bv_eager_atoms.cpp b/src/preprocessing/passes/bv_eager_atoms.cpp
index 6b80a4e65..8ee46829a 100644
--- a/src/preprocessing/passes/bv_eager_atoms.cpp
+++ b/src/preprocessing/passes/bv_eager_atoms.cpp
@@ -18,7 +18,6 @@
 
 #include "preprocessing/passes/bv_eager_atoms.h"
 
-#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/theory_model.h"
 
 namespace CVC4 {
@@ -43,7 +42,6 @@ PreprocessingPassResult BvEagerAtoms::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<BvEagerAtoms> X("bv-eager-atoms");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp
index ffecc8682..58e5f93bf 100644
--- a/src/preprocessing/passes/bv_gauss.cpp
+++ b/src/preprocessing/passes/bv_gauss.cpp
@@ -18,7 +18,6 @@
 #include "preprocessing/passes/bv_gauss.h"
 
 #include "expr/node.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"
@@ -819,7 +818,6 @@ PreprocessingPassResult BVGauss::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<BVGauss> X("bv-gauss");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp
index 82781b848..fb9ceac71 100644
--- a/src/preprocessing/passes/bv_intro_pow2.cpp
+++ b/src/preprocessing/passes/bv_intro_pow2.cpp
@@ -20,7 +20,6 @@
 
 #include <unordered_map>
 
-#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/rewriter.h"
 
@@ -99,7 +98,6 @@ 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 c6d98705c..811fe9251 100644
--- a/src/preprocessing/passes/bv_to_bool.cpp
+++ b/src/preprocessing/passes/bv_to_bool.cpp
@@ -21,7 +21,6 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "preprocessing/preprocessing_pass_registry.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/node_visitor.h"
 #include "theory/rewriter.h"
@@ -304,7 +303,6 @@ BVToBool::Statistics::~Statistics()
   smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLifted);
 }
 
-static RegisterPass<BVToBool> X("bv-to-bool");
 
 }  // passes
 }  // Preprocessing
diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp
index 8ca0a82ab..261a5f2ae 100644
--- a/src/preprocessing/passes/extended_rewriter_pass.cpp
+++ b/src/preprocessing/passes/extended_rewriter_pass.cpp
@@ -16,7 +16,6 @@
 
 #include "preprocessing/passes/extended_rewriter_pass.h"
 
-#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/quantifiers/extended_rewrite.h"
 
 namespace CVC4 {
@@ -38,7 +37,6 @@ PreprocessingPassResult ExtRewPre::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<ExtRewPre> X("ext-rew-pre");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp
index be4f08717..428360e8d 100644
--- a/src/preprocessing/passes/global_negate.cpp
+++ b/src/preprocessing/passes/global_negate.cpp
@@ -17,7 +17,6 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/rewriter.h"
 
 using namespace std;
@@ -120,7 +119,6 @@ PreprocessingPassResult GlobalNegate::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<GlobalNegate> X("global-negate");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index f4aa1cfe9..cc95bd1f2 100644
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -23,7 +23,6 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 
@@ -335,7 +334,6 @@ PreprocessingPassResult IntToBV::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<IntToBV> X("int-to-bv");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index bbc09b89c..b70d2460d 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -17,7 +17,6 @@
 
 #include "preprocessing/passes/ite_removal.h"
 
-#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
@@ -46,7 +45,6 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<IteRemoval> X("ite-removal");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index fbc22597d..02f14f508 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -17,7 +17,6 @@
 #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"
@@ -257,7 +256,6 @@ PreprocessingPassResult ITESimp::applyInternal(
               : PreprocessingPassResult::CONFLICT;
 }
 
-static RegisterPass<ITESimp> X("ite-simp");
 
 /* -------------------------------------------------------------------------- */
 
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index c45c6266e..9a2dcca1f 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -19,7 +19,6 @@
 
 #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"
@@ -660,7 +659,6 @@ MipLibTrick::Statistics::~Statistics()
   smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved);
 }
 
-static RegisterPass<MipLibTrick> X("miplib-trick");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp
index 630f35c14..744bd8ad8 100644
--- a/src/preprocessing/passes/nl_ext_purify.cpp
+++ b/src/preprocessing/passes/nl_ext_purify.cpp
@@ -16,7 +16,6 @@
 
 #include "preprocessing/passes/nl_ext_purify.h"
 
-#include "preprocessing/preprocessing_pass_registry.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -127,7 +126,6 @@ PreprocessingPassResult NlExtPurify::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<NlExtPurify> X("nl-ext-purify");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index d06143441..d8e1b3d66 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -20,7 +20,6 @@
 
 #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"
 
@@ -453,7 +452,6 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }  // namespace passes
 
-static RegisterPass<NonClausalSimp> X("non-clausal-simp");
 
 /* -------------------------------------------------------------------------- */
 
diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp
index 3d448ddf1..624b98ec1 100644
--- a/src/preprocessing/passes/pseudo_boolean_processor.cpp
+++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp
@@ -18,7 +18,6 @@
 #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"
@@ -414,7 +413,6 @@ void PseudoBooleanProcessor::clear()
   d_neg.clear();
 }
 
-static RegisterPass<PseudoBooleanProcessor> X("pseudo-boolean-processor");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 01416016a..6bd94a3f0 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -20,7 +20,6 @@
 
 #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"
@@ -546,7 +545,6 @@ void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) {
   }
 }
 
-static RegisterPass<QuantifierMacros> X("quantifier-macros");
 
 }  // passes
 }  // preprocessing
diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp
index 5217bc807..cfc4a8103 100644
--- a/src/preprocessing/passes/quantifiers_preprocess.cpp
+++ b/src/preprocessing/passes/quantifiers_preprocess.cpp
@@ -20,7 +20,6 @@
 #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"
 
@@ -53,7 +52,6 @@ PreprocessingPassResult QuantifiersPreprocess::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<QuantifiersPreprocess> X("quantifiers-preprocess");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index d15a19912..4b1fc06eb 100644
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -18,7 +18,6 @@
 
 #include <string>
 
-#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
@@ -198,7 +197,6 @@ PreprocessingPassResult RealToInt::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<RealToInt> X("real-to-int");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp
index 8d0f76c38..4a5eccd4b 100644
--- a/src/preprocessing/passes/rewrite.cpp
+++ b/src/preprocessing/passes/rewrite.cpp
@@ -16,7 +16,6 @@
 
 #include "preprocessing/passes/rewrite.h"
 
-#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {
@@ -40,7 +39,6 @@ PreprocessingPassResult Rewrite::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<Rewrite> X("rewrite");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp
index 55ce1c5d1..95a7995ce 100644
--- a/src/preprocessing/passes/sep_skolem_emp.cpp
+++ b/src/preprocessing/passes/sep_skolem_emp.cpp
@@ -20,7 +20,6 @@
 #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"
@@ -120,7 +119,6 @@ PreprocessingPassResult SepSkolemEmp::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<SepSkolemEmp> X("sep-skolem-emp");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp
index f8faab9bc..807048696 100644
--- a/src/preprocessing/passes/sort_infer.cpp
+++ b/src/preprocessing/passes/sort_infer.cpp
@@ -16,7 +16,6 @@
 
 #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"
 
@@ -83,7 +82,6 @@ PreprocessingPassResult SortInferencePass::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<SortInferencePass> X("sort-inference");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp
index df116166d..26327fd5b 100644
--- a/src/preprocessing/passes/static_learning.cpp
+++ b/src/preprocessing/passes/static_learning.cpp
@@ -18,7 +18,6 @@
 #include <string>
 
 #include "expr/node.h"
-#include "preprocessing/preprocessing_pass_registry.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -51,7 +50,6 @@ PreprocessingPassResult StaticLearning::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<StaticLearning> X("static-learning");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 09db93cbc..b0c374ff9 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -14,7 +14,6 @@
 
 #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"
@@ -317,7 +316,6 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions,
   return true;
 }
 
-static RegisterPass<SygusInference> X("sygus-infer");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/symmetry_breaker.cpp b/src/preprocessing/passes/symmetry_breaker.cpp
index 92065b2a0..44fdd2c79 100644
--- a/src/preprocessing/passes/symmetry_breaker.cpp
+++ b/src/preprocessing/passes/symmetry_breaker.cpp
@@ -15,7 +15,6 @@
 #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;
@@ -177,7 +176,6 @@ PreprocessingPassResult SymBreakerPass::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<SymBreakerPass> X("sym-break");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index 47c24bb5e..2ff525285 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -17,7 +17,6 @@
 
 #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"
 
@@ -155,7 +154,6 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<SynthRewRulesPass> X("synth-rr");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index a5d054c8b..3a5213f43 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -16,7 +16,6 @@
 
 #include "preprocessing/passes/theory_preprocess.h"
 
-#include "preprocessing/preprocessing_pass_registry.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 
@@ -45,7 +44,6 @@ PreprocessingPassResult TheoryPreprocess::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<TheoryPreprocess> X("theory-preprocess");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 52d378305..f58f1a44b 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -18,7 +18,6 @@
 
 #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"
@@ -843,7 +842,6 @@ PreprocessingPassResult UnconstrainedSimplifier::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-static RegisterPass<UnconstrainedSimplifier> X("unconstrained-simplifier");
 
 }  // namespace passes
 }  // namespace preprocessing
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp
index a50cd2541..f2e7c8603 100644
--- a/src/preprocessing/preprocessing_pass_registry.cpp
+++ b/src/preprocessing/preprocessing_pass_registry.cpp
@@ -12,8 +12,7 @@
  ** \brief 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.
+ ** of the available preprocessing passes.
  **/
 
 #include "preprocessing/preprocessing_pass_registry.h"
@@ -22,12 +21,46 @@
 #include <utility>
 
 #include "base/cvc4_assert.h"
+#include "base/map_util.h"
 #include "base/output.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"
 
 namespace CVC4 {
 namespace preprocessing {
 
+using namespace CVC4::preprocessing::passes;
+
 PreprocessingPassRegistry& PreprocessingPassRegistry::getInstance()
 {
   static PreprocessingPassRegistry* ppReg = new PreprocessingPassRegistry();
@@ -38,6 +71,7 @@ void PreprocessingPassRegistry::registerPassInfo(
     const std::string& name,
     std::function<PreprocessingPass*(PreprocessingPassContext*)> ctor)
 {
+  AlwaysAssert(!ContainsKey(d_ppInfo, name));
   d_ppInfo[name] = ctor;
 }
 
@@ -63,5 +97,58 @@ bool PreprocessingPassRegistry::hasPass(const std::string& name)
   return d_ppInfo.find(name) != d_ppInfo.end();
 }
 
+namespace {
+
+/**
+ * This method is stored by the `PreprocessingPassRegistry` and used to create
+ * a new instance of the preprocessing pass T.
+ *
+ * @param ppCtx The preprocessing pass context passed to the constructor of
+ *              the preprocessing pass
+ */
+template <class T>
+PreprocessingPass* callCtor(PreprocessingPassContext* ppCtx)
+{
+  return new T(ppCtx);
+}
+
+}  // namespace
+
+PreprocessingPassRegistry::PreprocessingPassRegistry()
+{
+  registerPassInfo("apply-substs", callCtor<ApplySubsts>);
+  registerPassInfo("bv-gauss", callCtor<BVGauss>);
+  registerPassInfo("static-learning", callCtor<StaticLearning>);
+  registerPassInfo("ite-simp", callCtor<ITESimp>);
+  registerPassInfo("apply-to-const", callCtor<ApplyToConst>);
+  registerPassInfo("global-negate", callCtor<GlobalNegate>);
+  registerPassInfo("int-to-bv", callCtor<IntToBV>);
+  registerPassInfo("synth-rr", callCtor<SynthRewRulesPass>);
+  registerPassInfo("real-to-int", callCtor<RealToInt>);
+  registerPassInfo("sygus-infer", callCtor<SygusInference>);
+  registerPassInfo("bv-to-bool", callCtor<BVToBool>);
+  registerPassInfo("bv-intro-pow2", callCtor<BvIntroPow2>);
+  registerPassInfo("sort-inference", callCtor<SortInferencePass>);
+  registerPassInfo("sep-skolem-emp", callCtor<SepSkolemEmp>);
+  registerPassInfo("rewrite", callCtor<Rewrite>);
+  registerPassInfo("bv-abstraction", callCtor<BvAbstraction>);
+  registerPassInfo("bv-eager-atoms", callCtor<BvEagerAtoms>);
+  registerPassInfo("pseudo-boolean-processor",
+                   callCtor<PseudoBooleanProcessor>);
+  registerPassInfo("unconstrained-simplifier",
+                   callCtor<UnconstrainedSimplifier>);
+  registerPassInfo("quantifiers-preprocess", callCtor<QuantifiersPreprocess>);
+  registerPassInfo("ite-removal", callCtor<IteRemoval>);
+  registerPassInfo("miplib-trick", callCtor<MipLibTrick>);
+  registerPassInfo("non-clausal-simp", callCtor<NonClausalSimp>);
+  registerPassInfo("bv-ackermann", callCtor<BVAckermann>);
+  registerPassInfo("sym-break", callCtor<SymBreakerPass>);
+  registerPassInfo("ext-rew-pre", callCtor<ExtRewPre>);
+  registerPassInfo("theory-preprocess", callCtor<TheoryPreprocess>);
+  registerPassInfo("quantifier-macros", callCtor<QuantifierMacros>);
+  registerPassInfo("nl-ext-purify", callCtor<NlExtPurify>);
+  registerPassInfo("bool-to-bv", callCtor<BoolToBV>);
+}
+
 }  // namespace preprocessing
 }  // namespace CVC4
diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h
index 44e9b4e6e..e6c98c1f9 100644
--- a/src/preprocessing/preprocessing_pass_registry.h
+++ b/src/preprocessing/preprocessing_pass_registry.h
@@ -12,8 +12,7 @@
  ** \brief 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.
+ ** of the available preprocessing passes.
  **/
 #include "cvc4_private.h"
 
@@ -79,6 +78,12 @@ class PreprocessingPassRegistry {
   bool hasPass(const std::string& name);
 
  private:
+  /**
+   * Private constructor for the preprocessing pass registry. The
+   * registry is a singleton and no other instance should be created.
+   */
+  PreprocessingPassRegistry();
+
   /**
    * Map of available preprocessing passes, mapping from preprocessing pass
    * name to a function that constructs a corresponding instance.
@@ -89,42 +94,6 @@ class PreprocessingPassRegistry {
       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