diff options
Diffstat (limited to 'src')
32 files changed, 96 insertions, 101 deletions
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" @@ -80,6 +79,12 @@ class PreprocessingPassRegistry { 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 |