diff options
Diffstat (limited to 'src/preprocessing')
34 files changed, 230 insertions, 59 deletions
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<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 bbe4439ec..65bdf5c1f 100644 --- 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 4c08d7e47..15b0ee678 100644 --- 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 27069de2f..addee305d 100644 --- 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 26785f15b..01fa70b61 100644 --- 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 fe43ebcd0..6b80a4e65 100644 --- 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 8b438dde4..ffecc8682 100644 --- 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 860aab5ca..82781b848 100644 --- 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 bcfdeb24f..c6d98705c 100644 --- 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 572aaed7a..8ca0a82ab 100644 --- 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 8f48d417c..be4f08717 100644 --- 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 997705835..f4aa1cfe9 100644 --- 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 86c40a793..bbc09b89c 100644 --- 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 137925f77..fbc22597d 100644 --- 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 616ecd969..c45c6266e 100644 --- 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 afb092571..630f35c14 100644 --- 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 653aed8ad..d06143441 100644 --- 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 c2cd7e34f..3d448ddf1 100644 --- 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 e3bc02309..01416016a 100644 --- 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 e6c1557c0..5217bc807 100644 --- 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 c92f4b962..d15a19912 100644 --- 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 dff807d58..8d0f76c38 100644 --- 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 d79ec8b93..55ce1c5d1 100644 --- 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 e2b0bfb59..f8faab9bc 100644 --- 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 e56d7ab60..7c913e9cf 100644 --- 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 0a792b5d4..df116166d 100644 --- 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 eb8835623..09db93cbc 100644 --- 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 1e4b9853d..92065b2a0 100644 --- 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 24db144e4..ec784a6ba 100644 --- 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 e3e3a548a..47c24bb5e 100644 --- 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 edb0fc800..a5d054c8b 100644 --- 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 6bb46f3f2..52d378305 100644 --- 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 03aaec46a..a50cd2541 100644 --- 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 30a2db579..44e9b4e6e 100644 --- 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 |