Refactor preprocessing pass registration (#2468)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 1 Oct 2018 17:06:38 +0000 (10:06 -0700)
committerGitHub <noreply@github.com>
Mon, 1 Oct 2018 17:06:38 +0000 (10:06 -0700)
commit48ea68aa581d492c48fe9e08b54e9ce26f3508b9
treeda50b320545331f2b3f7b8e3304c9d16b40c6c13
parent5a19b4d2d2fce73b0d29ff3d40d52c7ef1f4246b
Refactor preprocessing pass registration (#2468)

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

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

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

[0] https://llvm.org/docs/WritingAnLLVMPass.html
35 files changed:
src/preprocessing/passes/apply_substs.cpp
src/preprocessing/passes/apply_to_const.cpp
src/preprocessing/passes/bool_to_bv.cpp
src/preprocessing/passes/bv_abstraction.cpp
src/preprocessing/passes/bv_ackermann.cpp
src/preprocessing/passes/bv_eager_atoms.cpp
src/preprocessing/passes/bv_gauss.cpp
src/preprocessing/passes/bv_intro_pow2.cpp
src/preprocessing/passes/bv_to_bool.cpp
src/preprocessing/passes/extended_rewriter_pass.cpp
src/preprocessing/passes/global_negate.cpp
src/preprocessing/passes/int_to_bv.cpp
src/preprocessing/passes/ite_removal.cpp
src/preprocessing/passes/ite_simp.cpp
src/preprocessing/passes/miplib_trick.cpp
src/preprocessing/passes/nl_ext_purify.cpp
src/preprocessing/passes/non_clausal_simp.cpp
src/preprocessing/passes/pseudo_boolean_processor.cpp
src/preprocessing/passes/quantifier_macros.cpp
src/preprocessing/passes/quantifiers_preprocess.cpp
src/preprocessing/passes/real_to_int.cpp
src/preprocessing/passes/rewrite.cpp
src/preprocessing/passes/sep_skolem_emp.cpp
src/preprocessing/passes/sort_infer.cpp
src/preprocessing/passes/sort_infer.h
src/preprocessing/passes/static_learning.cpp
src/preprocessing/passes/sygus_inference.cpp
src/preprocessing/passes/symmetry_breaker.cpp
src/preprocessing/passes/symmetry_detect.cpp
src/preprocessing/passes/synth_rew_rules.cpp
src/preprocessing/passes/theory_preprocess.cpp
src/preprocessing/passes/unconstrained_simplifier.cpp
src/preprocessing/preprocessing_pass_registry.cpp
src/preprocessing/preprocessing_pass_registry.h
src/smt/smt_engine.cpp