From 48ea68aa581d492c48fe9e08b54e9ce26f3508b9 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 1 Oct 2018 10:06:38 -0700 Subject: 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 --- src/preprocessing/passes/apply_substs.cpp | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/preprocessing/passes/apply_substs.cpp') 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 X("apply-substs"); + } // namespace passes } // namespace preprocessing } // namespace CVC4 -- cgit v1.2.3