diff options
Diffstat (limited to 'src/preprocessing/passes')
30 files changed, 0 insertions, 61 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 |