From 48ea68aa581d492c48fe9e08b54e9ce26f3508b9 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 1 Oct 2018 10:06:38 -0700 Subject: [PATCH] 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 + src/preprocessing/passes/apply_to_const.cpp | 3 + src/preprocessing/passes/bool_to_bv.cpp | 3 + src/preprocessing/passes/bv_abstraction.cpp | 3 + src/preprocessing/passes/bv_ackermann.cpp | 3 + src/preprocessing/passes/bv_eager_atoms.cpp | 3 + src/preprocessing/passes/bv_gauss.cpp | 7 +- src/preprocessing/passes/bv_intro_pow2.cpp | 3 + src/preprocessing/passes/bv_to_bool.cpp | 8 +- .../passes/extended_rewriter_pass.cpp | 3 + src/preprocessing/passes/global_negate.cpp | 5 + src/preprocessing/passes/int_to_bv.cpp | 3 + src/preprocessing/passes/ite_removal.cpp | 4 + src/preprocessing/passes/ite_simp.cpp | 7 +- src/preprocessing/passes/miplib_trick.cpp | 3 + src/preprocessing/passes/nl_ext_purify.cpp | 4 + src/preprocessing/passes/non_clausal_simp.cpp | 7 +- .../passes/pseudo_boolean_processor.cpp | 3 + .../passes/quantifier_macros.cpp | 3 + .../passes/quantifiers_preprocess.cpp | 3 + src/preprocessing/passes/real_to_int.cpp | 3 + src/preprocessing/passes/rewrite.cpp | 3 + src/preprocessing/passes/sep_skolem_emp.cpp | 3 + src/preprocessing/passes/sort_infer.cpp | 19 +- src/preprocessing/passes/sort_infer.h | 13 +- src/preprocessing/passes/static_learning.cpp | 3 + src/preprocessing/passes/sygus_inference.cpp | 3 + src/preprocessing/passes/symmetry_breaker.cpp | 4 + src/preprocessing/passes/symmetry_detect.cpp | 1 + src/preprocessing/passes/synth_rew_rules.cpp | 3 + .../passes/theory_preprocess.cpp | 3 + .../passes/unconstrained_simplifier.cpp | 3 + .../preprocessing_pass_registry.cpp | 47 ++-- .../preprocessing_pass_registry.h | 100 ++++++- src/smt/smt_engine.cpp | 260 ++++-------------- 35 files changed, 290 insertions(+), 259 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 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 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 #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 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 #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 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 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 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 @@ -818,6 +819,8 @@ PreprocessingPassResult BVGauss::applyInternal( return PreprocessingPassResult::NO_CONFLICT; } +static RegisterPass 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 +#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 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 #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 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 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 + #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 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 #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 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 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 + #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 - using namespace CVC4; using namespace CVC4::theory; @@ -256,6 +257,8 @@ PreprocessingPassResult ITESimp::applyInternal( : PreprocessingPassResult::CONFLICT; } +static RegisterPass 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 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 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 + #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 - using namespace CVC4; using namespace CVC4::theory; @@ -452,6 +453,8 @@ PreprocessingPassResult NonClausalSimp::applyInternal( return PreprocessingPassResult::NO_CONFLICT; } // namespace passes +static RegisterPass 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 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 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 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 +#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 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 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 #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 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 model_replace_f; std::map > 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 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 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 #include #include -#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 #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 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& assertions, return true; } +static RegisterPass 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 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 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 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 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 #include #include "base/cvc4_assert.h" @@ -25,29 +28,39 @@ namespace CVC4 { namespace preprocessing { -void PreprocessingPassRegistry::registerPass( - const std::string& ppName, - std::unique_ptr 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 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 PreprocessingPassRegistry::getAvailablePasses() +{ + std::vector 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); + 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 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 getAvailablePasses(); - /* Stores all the registered preprocessing passes. */ - std::unordered_map> - 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 > + 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 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 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 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 15f8280b5..b133f3a36 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -70,37 +70,6 @@ #include "options/strings_options.h" #include "options/theory_options.h" #include "options/uf_options.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" #include "preprocessing/preprocessing_pass_context.h" #include "preprocessing/preprocessing_pass_registry.h" @@ -145,7 +114,6 @@ using namespace std; using namespace CVC4; using namespace CVC4::smt; using namespace CVC4::preprocessing; -using namespace CVC4::preprocessing::passes; using namespace CVC4::prop; using namespace CVC4::context; using namespace CVC4::theory; @@ -531,7 +499,12 @@ class SmtEnginePrivate : public NodeManagerListener { private: std::unique_ptr d_preprocessingPassContext; - PreprocessingPassRegistry d_preprocessingPassRegistry; + + /** + * Map of preprocessing pass instances, mapping from names to preprocessing + * pass instance + */ + std::unordered_map> d_passes; /** * Helper function to fix up assertion list to restore invariants needed after @@ -639,10 +612,7 @@ class SmtEnginePrivate : public NodeManagerListener { d_smt.d_nodeManager->unsubscribeEvents(this); } - void unregisterPreprocessingPasses() - { - d_preprocessingPassRegistry.unregisterPasses(); - } + void cleanupPreprocessingPasses() { d_passes.clear(); } ResourceManager* getResourceManager() { return d_resourceManager; } void spendResource(unsigned amount) @@ -1055,7 +1025,7 @@ SmtEngine::~SmtEngine() d_fmfRecFunctionsDefined->deleteSelf(); //destroy all passes before destroying things that they refer to - d_private->unregisterPreprocessingPasses(); + d_private->cleanupPreprocessingPasses(); delete d_theoryEngine; d_theoryEngine = NULL; @@ -2558,121 +2528,19 @@ bool SmtEngine::isDefinedFunction( Expr func ){ void SmtEnginePrivate::finishInit() { + PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance(); d_preprocessingPassContext.reset(new PreprocessingPassContext( &d_smt, d_resourceManager, &d_iteRemover, &d_propagator)); - // TODO: register passes here (this will likely change when we add support for - // actually assembling preprocessing pipelines). - std::unique_ptr applySubsts( - new ApplySubsts(d_preprocessingPassContext.get())); - std::unique_ptr applyToConst( - new ApplyToConst(d_preprocessingPassContext.get())); - std::unique_ptr boolToBv( - new BoolToBV(d_preprocessingPassContext.get())); - std::unique_ptr bvAbstract( - new BvAbstraction(d_preprocessingPassContext.get())); - std::unique_ptr bvEagerAtoms( - new BvEagerAtoms(d_preprocessingPassContext.get())); - std::unique_ptr bvAckermann( - new BVAckermann(d_preprocessingPassContext.get())); - std::unique_ptr bvGauss( - new BVGauss(d_preprocessingPassContext.get())); - std::unique_ptr bvIntroPow2( - new BvIntroPow2(d_preprocessingPassContext.get())); - std::unique_ptr bvToBool( - new BVToBool(d_preprocessingPassContext.get())); - std::unique_ptr extRewPre( - new ExtRewPre(d_preprocessingPassContext.get())); - std::unique_ptr globalNegate( - new GlobalNegate(d_preprocessingPassContext.get())); - std::unique_ptr intToBV( - new IntToBV(d_preprocessingPassContext.get())); - std::unique_ptr iteSimp( - new ITESimp(d_preprocessingPassContext.get())); - std::unique_ptr nlExtPurify( - new NlExtPurify(d_preprocessingPassContext.get())); - std::unique_ptr nonClausalSimp( - new NonClausalSimp(d_preprocessingPassContext.get())); - std::unique_ptr mipLibTrick( - new MipLibTrick(d_preprocessingPassContext.get())); - std::unique_ptr quantifiersPreprocess( - new QuantifiersPreprocess(d_preprocessingPassContext.get())); - std::unique_ptr pbProc( - new PseudoBooleanProcessor(d_preprocessingPassContext.get())); - std::unique_ptr iteRemoval( - new IteRemoval(d_preprocessingPassContext.get())); - std::unique_ptr realToInt( - new RealToInt(d_preprocessingPassContext.get())); - std::unique_ptr rewrite( - new Rewrite(d_preprocessingPassContext.get())); - std::unique_ptr sortInfer( - new SortInferencePass(d_preprocessingPassContext.get(), - d_smt.d_theoryEngine->getSortInference())); - std::unique_ptr staticLearning( - new StaticLearning(d_preprocessingPassContext.get())); - std::unique_ptr sygusInfer( - new SygusInference(d_preprocessingPassContext.get())); - std::unique_ptr sbProc( - new SymBreakerPass(d_preprocessingPassContext.get())); - std::unique_ptr srrProc( - new SynthRewRulesPass(d_preprocessingPassContext.get())); - std::unique_ptr sepSkolemEmp( - new SepSkolemEmp(d_preprocessingPassContext.get())); - std::unique_ptr theoryPreprocess( - new TheoryPreprocess(d_preprocessingPassContext.get())); - std::unique_ptr unconstrainedSimplifier( - new UnconstrainedSimplifier(d_preprocessingPassContext.get())); - d_preprocessingPassRegistry.registerPass("apply-substs", - std::move(applySubsts)); - d_preprocessingPassRegistry.registerPass("apply-to-const", - std::move(applyToConst)); - d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv)); - d_preprocessingPassRegistry.registerPass("bv-abstraction", - std::move(bvAbstract)); - d_preprocessingPassRegistry.registerPass("bv-ackermann", - std::move(bvAckermann)); - d_preprocessingPassRegistry.registerPass("bv-eager-atoms", - std::move(bvEagerAtoms)); - std::unique_ptr quantifierMacros( - new QuantifierMacros(d_preprocessingPassContext.get())); - d_preprocessingPassRegistry.registerPass("bv-gauss", std::move(bvGauss)); - d_preprocessingPassRegistry.registerPass("bv-intro-pow2", - std::move(bvIntroPow2)); - d_preprocessingPassRegistry.registerPass("bv-to-bool", std::move(bvToBool)); - d_preprocessingPassRegistry.registerPass("ext-rew-pre", std::move(extRewPre)); - d_preprocessingPassRegistry.registerPass("global-negate", - std::move(globalNegate)); - d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV)); - d_preprocessingPassRegistry.registerPass("ite-removal", - std::move(iteRemoval)); - d_preprocessingPassRegistry.registerPass("ite-simp", std::move(iteSimp)); - d_preprocessingPassRegistry.registerPass("nl-ext-purify", - std::move(nlExtPurify)); - d_preprocessingPassRegistry.registerPass("non-clausal-simp", - std::move(nonClausalSimp)); - d_preprocessingPassRegistry.registerPass("miplib-trick", - std::move(mipLibTrick)); - d_preprocessingPassRegistry.registerPass("quantifiers-preprocess", - std::move(quantifiersPreprocess)); - d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor", - std::move(pbProc)); - d_preprocessingPassRegistry.registerPass("real-to-int", std::move(realToInt)); - d_preprocessingPassRegistry.registerPass("rewrite", std::move(rewrite)); - d_preprocessingPassRegistry.registerPass("sep-skolem-emp", - std::move(sepSkolemEmp)); - d_preprocessingPassRegistry.registerPass("sort-inference", - std::move(sortInfer)); - d_preprocessingPassRegistry.registerPass("static-learning", - std::move(staticLearning)); - d_preprocessingPassRegistry.registerPass("sygus-infer", - std::move(sygusInfer)); - d_preprocessingPassRegistry.registerPass("sym-break", std::move(sbProc)); - d_preprocessingPassRegistry.registerPass("synth-rr", std::move(srrProc)); - d_preprocessingPassRegistry.registerPass("theory-preprocess", - std::move(theoryPreprocess)); - d_preprocessingPassRegistry.registerPass("quantifier-macros", - std::move(quantifierMacros)); - d_preprocessingPassRegistry.registerPass("unconstrained-simplifier", - std::move(unconstrainedSimplifier)); + + // TODO: this will likely change when we add support for actually assembling + // preprocessing pipelines. For now, we just create an instance of each + // available preprocessing pass. + std::vector passNames = ppReg.getAvailablePasses(); + for (const std::string& passName : passNames) + { + d_passes[passName].reset( + ppReg.createPass(d_preprocessingPassContext.get(), passName)); + } } Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map& cache, bool expandOnly) @@ -2874,6 +2742,8 @@ static void dumpAssertions(const char* key, // returns false if simplification led to "false" bool SmtEnginePrivate::simplifyAssertions() { + PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance(); + spendResource(options::preprocessStep()); Assert(d_smt.d_pendingPops == 0); try { @@ -2887,8 +2757,7 @@ bool SmtEnginePrivate::simplifyAssertions() { // Perform non-clausal simplification PreprocessingPassResult res = - d_preprocessingPassRegistry.getPass("non-clausal-simp") - ->apply(&d_assertions); + d_passes["non-clausal-simp"]->apply(&d_assertions); if (res == PreprocessingPassResult::CONFLICT) { return false; @@ -2908,8 +2777,7 @@ bool SmtEnginePrivate::simplifyAssertions() // re-simplification, which we don't expect to be useful anyway) d_assertions.getRealAssertionsEnd() == d_assertions.size()) { - d_preprocessingPassRegistry.getPass("miplib-trick") - ->apply(&d_assertions); + d_passes["miplib-trick"]->apply(&d_assertions); } else { Trace("simplify") << "SmtEnginePrivate::simplify(): " << "skipping miplib pseudobooleans pass (either incrementalSolving is on, or miplib pbs are turned off)..." << endl; @@ -2924,16 +2792,14 @@ bool SmtEnginePrivate::simplifyAssertions() // Theory preprocessing if (d_smt.d_earlyTheoryPP) { - d_preprocessingPassRegistry.getPass("theory-preprocess") - ->apply(&d_assertions); + d_passes["theory-preprocess"]->apply(&d_assertions); } // ITE simplification if (options::doITESimp() && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat())) { - PreprocessingPassResult res = - d_preprocessingPassRegistry.getPass("ite-simp")->apply(&d_assertions); + PreprocessingPassResult res = d_passes["ite-simp"]->apply(&d_assertions); if (res == PreprocessingPassResult::CONFLICT) { Chat() << "...ITE simplification found unsat..." << endl; @@ -2945,8 +2811,7 @@ bool SmtEnginePrivate::simplifyAssertions() // Unconstrained simplification if(options::unconstrainedSimp()) { - d_preprocessingPassRegistry.getPass("unconstrained-simplifier") - ->apply(&d_assertions); + d_passes["unconstrained-simplifier"]->apply(&d_assertions); } if (options::repeatSimp() @@ -2954,8 +2819,7 @@ bool SmtEnginePrivate::simplifyAssertions() && !options::unsatCores() && !options::fewerPreprocessingHoles()) { PreprocessingPassResult res = - d_preprocessingPassRegistry.getPass("non-clausal-simp") - ->apply(&d_assertions); + d_passes["non-clausal-simp"]->apply(&d_assertions); if (res == PreprocessingPassResult::CONFLICT) { return false; @@ -3108,6 +2972,8 @@ void SmtEnginePrivate::processAssertions() { SubstitutionMap& top_level_substs = d_preprocessingPassContext->getTopLevelSubstitutions(); + PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance(); + // Dump the assertions dumpAssertions("pre-everything", d_assertions); @@ -3123,7 +2989,7 @@ void SmtEnginePrivate::processAssertions() { if (options::bvGaussElim()) { - d_preprocessingPassRegistry.getPass("bv-gauss")->apply(&d_assertions); + d_passes["bv-gauss"]->apply(&d_assertions); } if (d_assertionsProcessed && options::incrementalSolving()) { @@ -3171,12 +3037,12 @@ void SmtEnginePrivate::processAssertions() { if (options::globalNegate()) { // global negation of the formula - d_preprocessingPassRegistry.getPass("global-negate")->apply(&d_assertions); + d_passes["global-negate"]->apply(&d_assertions); d_smt.d_globalNegation = !d_smt.d_globalNegation; } if( options::nlExtPurify() ){ - d_preprocessingPassRegistry.getPass("nl-ext-purify")->apply(&d_assertions); + d_passes["nl-ext-purify"]->apply(&d_assertions); } if( options::ceGuidedInst() ){ @@ -3189,12 +3055,12 @@ void SmtEnginePrivate::processAssertions() { } if (options::solveRealAsInt()) { - d_preprocessingPassRegistry.getPass("real-to-int")->apply(&d_assertions); + d_passes["real-to-int"]->apply(&d_assertions); } if (options::solveIntAsBV() > 0) { - d_preprocessingPassRegistry.getPass("int-to-bv")->apply(&d_assertions); + d_passes["int-to-bv"]->apply(&d_assertions); } if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && @@ -3209,12 +3075,12 @@ void SmtEnginePrivate::processAssertions() { if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && !options::incrementalSolving()) { - d_preprocessingPassRegistry.getPass("bv-ackermann")->apply(&d_assertions); + d_passes["bv-ackermann"]->apply(&d_assertions); } if (options::bvAbstraction() && !options::incrementalSolving()) { - d_preprocessingPassRegistry.getPass("bv-abstraction")->apply(&d_assertions); + d_passes["bv-abstraction"]->apply(&d_assertions); } Debug("smt") << " d_assertions : " << d_assertions.size() << endl; @@ -3223,30 +3089,29 @@ void SmtEnginePrivate::processAssertions() { if (options::extRewPrep()) { - d_preprocessingPassRegistry.getPass("ext-rew-pre")->apply(&d_assertions); + d_passes["ext-rew-pre"]->apply(&d_assertions); } // Unconstrained simplification if(options::unconstrainedSimp()) { - d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions); - d_preprocessingPassRegistry.getPass("unconstrained-simplifier") - ->apply(&d_assertions); + d_passes["rewrite"]->apply(&d_assertions); + d_passes["unconstrained-simplifier"]->apply(&d_assertions); } if(options::bvIntroducePow2()) { - d_preprocessingPassRegistry.getPass("bv-intro-pow2")->apply(&d_assertions); + d_passes["bv-intro-pow2"]->apply(&d_assertions); } if (options::unsatCores()) { // special rewriting pass for unsat cores, since many of the passes below // are skipped - d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions); + d_passes["rewrite"]->apply(&d_assertions); } else { - d_preprocessingPassRegistry.getPass("apply-substs")->apply(&d_assertions); + d_passes["apply-substs"]->apply(&d_assertions); } // Assertions ARE guaranteed to be rewritten by this point @@ -3260,25 +3125,23 @@ void SmtEnginePrivate::processAssertions() { // Lift bit-vectors of size 1 to bool if (options::bitvectorToBool()) { - d_preprocessingPassRegistry.getPass("bv-to-bool")->apply(&d_assertions); + d_passes["bv-to-bool"]->apply(&d_assertions); } // Convert non-top-level Booleans to bit-vectors of size 1 if (options::boolToBitvector()) { - d_preprocessingPassRegistry.getPass("bool-to-bv")->apply(&d_assertions); + d_passes["bool-to-bv"]->apply(&d_assertions); } if(options::sepPreSkolemEmp()) { - d_preprocessingPassRegistry.getPass("sep-skolem-emp")->apply(&d_assertions); + d_passes["sep-skolem-emp"]->apply(&d_assertions); } if( d_smt.d_logic.isQuantified() ){ //remove rewrite rules, apply pre-skolemization to existential quantifiers - d_preprocessingPassRegistry.getPass("quantifiers-preprocess") - ->apply(&d_assertions); + d_passes["quantifiers-preprocess"]->apply(&d_assertions); if( options::macrosQuant() ){ //quantifiers macro expansion - d_preprocessingPassRegistry.getPass("quantifier-macros") - ->apply(&d_assertions); + d_passes["quantifier-macros"]->apply(&d_assertions); } //fmf-fun : assume admissible functions, applying preprocessing reduction to FMF @@ -3312,23 +3175,22 @@ void SmtEnginePrivate::processAssertions() { } if (options::sygusInference()) { - d_preprocessingPassRegistry.getPass("sygus-infer")->apply(&d_assertions); + d_passes["sygus-infer"]->apply(&d_assertions); } } if( options::sortInference() || options::ufssFairnessMonotone() ){ - d_preprocessingPassRegistry.getPass("sort-inference")->apply(&d_assertions); + d_passes["sort-inference"]->apply(&d_assertions); } if( options::pbRewrites() ){ - d_preprocessingPassRegistry.getPass("pseudo-boolean-processor") - ->apply(&d_assertions); + d_passes["pseudo-boolean-processor"]->apply(&d_assertions); } if (options::synthRrPrep()) { // do candidate rewrite rule synthesis - d_preprocessingPassRegistry.getPass("synth-rr")->apply(&d_assertions); + d_passes["synth-rr"]->apply(&d_assertions); } Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-simplify" << endl; @@ -3344,22 +3206,21 @@ void SmtEnginePrivate::processAssertions() { if (options::symmetryBreakerExp() && !options::incrementalSolving()) { // apply symmetry breaking if not in incremental mode - d_preprocessingPassRegistry.getPass("sym-break")->apply(&d_assertions); + d_passes["sym-break"]->apply(&d_assertions); } if(options::doStaticLearning()) { - d_preprocessingPassRegistry.getPass("static-learning") - ->apply(&d_assertions); + d_passes["static-learning"]->apply(&d_assertions); } Debug("smt") << " d_assertions : " << d_assertions.size() << endl; { d_smt.d_stats->d_numAssertionsPre += d_assertions.size(); - d_preprocessingPassRegistry.getPass("ite-removal")->apply(&d_assertions); + d_passes["ite-removal"]->apply(&d_assertions); // This is needed because when solving incrementally, removeITEs may introduce // skolems that were solved for earlier and thus appear in the substitution // map. - d_preprocessingPassRegistry.getPass("apply-substs")->apply(&d_assertions); + d_passes["apply-substs"]->apply(&d_assertions); d_smt.d_stats->d_numAssertionsPost += d_assertions.size(); } @@ -3429,8 +3290,8 @@ void SmtEnginePrivate::processAssertions() { } // TODO(b/1256): For some reason this is needed for some benchmarks, such as // QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2 - d_preprocessingPassRegistry.getPass("ite-removal")->apply(&d_assertions); - d_preprocessingPassRegistry.getPass("apply-substs")->apply(&d_assertions); + d_passes["ite-removal"]->apply(&d_assertions); + d_passes["apply-substs"]->apply(&d_assertions); // Assert(iteRewriteAssertionsEnd == d_assertions.size()); } Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl; @@ -3439,7 +3300,7 @@ void SmtEnginePrivate::processAssertions() { if (options::rewriteApplyToConst()) { - d_preprocessingPassRegistry.getPass("apply-to-const")->apply(&d_assertions); + d_passes["apply-to-const"]->apply(&d_assertions); } // begin: INVARIANT to maintain: no reordering of assertions or @@ -3453,12 +3314,11 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl; Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - d_preprocessingPassRegistry.getPass("theory-preprocess") - ->apply(&d_assertions); + d_passes["theory-preprocess"]->apply(&d_assertions); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - d_preprocessingPassRegistry.getPass("bv-eager-atoms")->apply(&d_assertions); + d_passes["bv-eager-atoms"]->apply(&d_assertions); } //notify theory engine new preprocessed assertions -- 2.30.2