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

diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index f5c3520d01545a386764dca6ee3f24dae0819004..59b628e3b1462b10ee2d830be39ee5eef99c0451 100644 (file)
--- 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 bbe4439ec03aebd43c41614a52c488e93e124f29..65bdf5c1f6ef89c7f26dd6cdbe45e11bdae506df 100644 (file)
--- 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 4c08d7e47f7f474b2f68e0ba878d825e25a3e48e..15b0ee67874e736452dca1089a62965044d3a4c5 100644 (file)
--- 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 27069de2fc0d83fef90af1ad46ed7499b061f696..addee305dd37dc8f69fd14d689012ccfb2a24b0d 100644 (file)
--- 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 26785f15b9b22b4c6517a96890b8c88e3237758b..01fa70b6148c195ffeb48bf8e948eead772d1296 100644 (file)
--- 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 fe43ebcd0510714bf4bc57eb3a39db93945a4649..6b80a4e65a0723d8dfa9ea01c945d87e0998eb4d 100644 (file)
--- 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 8b438dde4a98fecdbdf8402824c8831f4391ed0a..ffecc868291f76a72624dc7c4fbc7f1e7cee642a 100644 (file)
--- 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 860aab5ca0846df09f2971588dd9d40ab647ea30..82781b8485699fea35dd7ded7258e96861d48d66 100644 (file)
--- 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 bcfdeb24f1cd263f0fce878a13d18a92af82b800..c6d98705c454309d6066d0d95291a8893bcd86c1 100644 (file)
--- 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 572aaed7a4153d170005bc54e129f6a9bfd16082..8ca0a82ab1c37da69d60cb6d69599034559be200 100644 (file)
--- 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 8f48d417cce5abe39907ba8b9fd0af76bc3c2e61..be4f087171d7cf84542438d11e3accd2cb57625b 100644 (file)
--- 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 99770583559b3b1039f38c3a54bb248995091f70..f4aa1cfe90adc3792ea3964c471bdfcee7a27de0 100644 (file)
--- 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 86c40a793ddc8133aa62059770e5dd28cf85805c..bbc09b89c853e5a2e27cd93c2c6953698a149984 100644 (file)
--- 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 137925f77859894cc26347489537ab20c31272d6..fbc22597d1d06a54b09bc6875ea35fc70003848c 100644 (file)
--- 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 616ecd969000bece4b4c927fdfe5c71fe88470da..c45c6266e468cee1707b03452d782741616c2626 100644 (file)
--- 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 afb092571daa352d260a2d444c56e3faa251ac22..630f35c140f1e364838a62058edede5eb4455a8b 100644 (file)
--- 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 653aed8adb19fcfa609f6d7d03320f7d5ae690a4..d061434417ab523f782bf0265438e0253d5d1d5b 100644 (file)
--- 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 c2cd7e34fbcd176dabe90c0f4a7a495479718d62..3d448ddf17a93b9fef5f204511f0b43aa60deb31 100644 (file)
--- 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 e3bc023092670fb13cf59f12c49ed3eb3389708a..01416016a521c12ed3f8225d12be1fc4ac99603a 100644 (file)
--- 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 e6c1557c09fa5ebcf99dd51eecaf8c11944936e9..5217bc8072d7db94c2ad5ff88f60aba9c3181c8c 100644 (file)
--- 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 c92f4b96222750ab7ca02162c79040d11fbecdaa..d15a1991296d722ffc6f3466a72aa35c0f17c486 100644 (file)
--- 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 dff807d58f8e41c420d52d2cbfd06e297bf1ebd8..8d0f76c389ce13350df450ea9ad049f1c7b02e70 100644 (file)
--- 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 d79ec8b93b68721292b3ae69b4a0ee577c6fdf6a..55ce1c5d15ac8dce92a9b350bba02d61a5bf08c5 100644 (file)
--- 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 e2b0bfb59306875d25500a33ac8b76d5890d3b7b..f8faab9bcfb3ca0e1674721c48a7c666a5dbd01d 100644 (file)
--- 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 e56d7ab60123fc408fcb30090d4c3f6bbf9e57ee..7c913e9cf6d6a11bdbf585cf43cc0c84f4dfa58b 100644 (file)
--- 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 0a792b5d41e8d25d9736f798eca8403966301187..df116166d54a2ac6439c16af11dd0338faf0a2f7 100644 (file)
--- 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 eb883562360c17e31cd0d74f280f7dbfa750e032..09db93cbcce1b36ef035ecc4fc907d8b016a9799 100644 (file)
--- 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 1e4b9853dbd04100ae1601dd15b6908f26950b2c..92065b2a0af1ef92f26a4e980350e42c95ceba8b 100644 (file)
--- 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 24db144e41153eacd445edb5c61f148a2b35f72a..ec784a6ba71436e9473061c2572f19c070e7b199 100644 (file)
--- 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 e3e3a548ab80c69b9ee2eb2836aa5e13472a8743..47c24bb5eafae530b8f357b7ab4efb75d8bda90c 100644 (file)
--- 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 edb0fc80054dbac09a873f1527e6457f1dd9a745..a5d054c8b620e9351c6ae12c0be51066d96ee994 100644 (file)
--- 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 6bb46f3f2e429615a9109e1593fb5a11db67a440..52d37830563503818fbbaeb9d855131acb906f17 100644 (file)
--- 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 03aaec46aabbe0b509732a4ea87843560d223524..a50cd2541e0c9f8ba2e02bfcc6ae876015270593 100644 (file)
--- 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 30a2db5796d55bd12ee8d3b1b4527b46e2c88c79..44e9b4e6eb52c0bb3d79eed224448a6b6d0d620e 100644 (file)
--- 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 15f8280b52288c483e2d2b354c46949857dec100..b133f3a364aad2858b7132aa6ac518f630af46fb 100644 (file)
--- 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