#include "preprocessing/passes/apply_substs.h"
#include "context/cdo.h"
-#include "preprocessing/preprocessing_pass_registry.h"
#include "theory/rewriter.h"
#include "theory/substitutions.h"
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<ApplySubsts> X("apply-substs");
-
} // namespace passes
} // namespace preprocessing
} // namespace CVC4
#include "preprocessing/passes/apply_to_const.h"
-#include "preprocessing/preprocessing_pass_registry.h"
#include "theory/rewriter.h"
namespace CVC4 {
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<ApplyToConst> X("apply-to-const");
} // namespace passes
} // namespace preprocessing
#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"
smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered);
}
-static RegisterPass<BoolToBV> X("bool-to-bv");
} // namespace passes
} // namespace preprocessing
#include <vector>
#include "options/bv_options.h"
-#include "preprocessing/preprocessing_pass_registry.h"
#include "theory/bv/theory_bv.h"
#include "theory/rewriter.h"
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<BvAbstraction> X("bv-abstraction");
} // namespace passes
} // namespace preprocessing
#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;
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<BVAckermann> X("bv-ackermann");
/* -------------------------------------------------------------------------- */
#include "preprocessing/passes/bv_eager_atoms.h"
-#include "preprocessing/preprocessing_pass_registry.h"
#include "theory/theory_model.h"
namespace CVC4 {
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<BvEagerAtoms> X("bv-eager-atoms");
} // namespace passes
} // namespace preprocessing
#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"
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<BVGauss> X("bv-gauss");
} // namespace passes
} // namespace preprocessing
#include <unordered_map>
-#include "preprocessing/preprocessing_pass_registry.h"
#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
#include "theory/rewriter.h"
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<BvIntroPow2> X("bv-intro-pow2");
}/* CVC4::theory::bv namespace */
}/* CVC4::theory namespace */
#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"
smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLifted);
}
-static RegisterPass<BVToBool> X("bv-to-bool");
} // passes
} // Preprocessing
#include "preprocessing/passes/extended_rewriter_pass.h"
-#include "preprocessing/preprocessing_pass_registry.h"
#include "theory/quantifiers/extended_rewrite.h"
namespace CVC4 {
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<ExtRewPre> X("ext-rew-pre");
} // namespace passes
} // namespace preprocessing
#include <vector>
#include "expr/node.h"
-#include "preprocessing/preprocessing_pass_registry.h"
#include "theory/rewriter.h"
using namespace std;
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<GlobalNegate> X("global-negate");
} // namespace passes
} // namespace preprocessing
#include <vector>
#include "expr/node.h"
-#include "preprocessing/preprocessing_pass_registry.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<IntToBV> X("int-to-bv");
} // namespace passes
} // namespace preprocessing
#include "preprocessing/passes/ite_removal.h"
-#include "preprocessing/preprocessing_pass_registry.h"
#include "theory/rewriter.h"
namespace CVC4 {
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<IteRemoval> X("ite-removal");
} // namespace passes
} // namespace preprocessing
#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"
: PreprocessingPassResult::CONFLICT;
}
-static RegisterPass<ITESimp> X("ite-simp");
/* -------------------------------------------------------------------------- */
#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"
smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved);
}
-static RegisterPass<MipLibTrick> X("miplib-trick");
} // namespace passes
} // namespace preprocessing
#include "preprocessing/passes/nl_ext_purify.h"
-#include "preprocessing/preprocessing_pass_registry.h"
namespace CVC4 {
namespace preprocessing {
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<NlExtPurify> X("nl-ext-purify");
} // namespace passes
} // namespace preprocessing
#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"
return PreprocessingPassResult::NO_CONFLICT;
} // namespace passes
-static RegisterPass<NonClausalSimp> X("non-clausal-simp");
/* -------------------------------------------------------------------------- */
#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"
d_neg.clear();
}
-static RegisterPass<PseudoBooleanProcessor> X("pseudo-boolean-processor");
} // namespace passes
} // namespace preprocessing
#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"
}
}
-static RegisterPass<QuantifierMacros> X("quantifier-macros");
} // passes
} // preprocessing
#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"
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<QuantifiersPreprocess> X("quantifiers-preprocess");
} // namespace passes
} // namespace preprocessing
#include <string>
-#include "preprocessing/preprocessing_pass_registry.h"
#include "theory/arith/arith_msum.h"
#include "theory/rewriter.h"
#include "theory/theory_model.h"
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<RealToInt> X("real-to-int");
} // namespace passes
} // namespace preprocessing
#include "preprocessing/passes/rewrite.h"
-#include "preprocessing/preprocessing_pass_registry.h"
#include "theory/rewriter.h"
namespace CVC4 {
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<Rewrite> X("rewrite");
} // namespace passes
} // namespace preprocessing
#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"
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<SepSkolemEmp> X("sep-skolem-emp");
} // namespace passes
} // namespace preprocessing
#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"
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<SortInferencePass> X("sort-inference");
} // namespace passes
} // namespace preprocessing
#include <string>
#include "expr/node.h"
-#include "preprocessing/preprocessing_pass_registry.h"
namespace CVC4 {
namespace preprocessing {
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<StaticLearning> X("static-learning");
} // namespace passes
} // namespace preprocessing
#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"
return true;
}
-static RegisterPass<SygusInference> X("sygus-infer");
} // namespace passes
} // namespace preprocessing
#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;
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<SymBreakerPass> X("sym-break");
} // namespace passes
} // namespace preprocessing
#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"
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<SynthRewRulesPass> X("synth-rr");
} // namespace passes
} // namespace preprocessing
#include "preprocessing/passes/theory_preprocess.h"
-#include "preprocessing/preprocessing_pass_registry.h"
#include "theory/rewriter.h"
#include "theory/theory_engine.h"
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<TheoryPreprocess> X("theory-preprocess");
} // namespace passes
} // namespace preprocessing
#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"
return PreprocessingPassResult::NO_CONFLICT;
}
-static RegisterPass<UnconstrainedSimplifier> X("unconstrained-simplifier");
} // namespace passes
} // namespace preprocessing
** \brief The preprocessing pass registry
**
** This file defines the classes PreprocessingPassRegistry, which keeps track
- ** of the available preprocessing passes, and RegisterPass, which registers a
- ** preprocessing pass with the registry.
+ ** of the available preprocessing passes.
**/
#include "preprocessing/preprocessing_pass_registry.h"
#include <utility>
#include "base/cvc4_assert.h"
+#include "base/map_util.h"
#include "base/output.h"
+#include "preprocessing/passes/apply_substs.h"
+#include "preprocessing/passes/apply_to_const.h"
+#include "preprocessing/passes/bool_to_bv.h"
+#include "preprocessing/passes/bv_abstraction.h"
+#include "preprocessing/passes/bv_ackermann.h"
+#include "preprocessing/passes/bv_eager_atoms.h"
+#include "preprocessing/passes/bv_gauss.h"
+#include "preprocessing/passes/bv_intro_pow2.h"
+#include "preprocessing/passes/bv_to_bool.h"
+#include "preprocessing/passes/extended_rewriter_pass.h"
+#include "preprocessing/passes/global_negate.h"
+#include "preprocessing/passes/int_to_bv.h"
+#include "preprocessing/passes/ite_removal.h"
+#include "preprocessing/passes/ite_simp.h"
+#include "preprocessing/passes/miplib_trick.h"
+#include "preprocessing/passes/nl_ext_purify.h"
+#include "preprocessing/passes/non_clausal_simp.h"
+#include "preprocessing/passes/pseudo_boolean_processor.h"
+#include "preprocessing/passes/quantifier_macros.h"
+#include "preprocessing/passes/quantifiers_preprocess.h"
+#include "preprocessing/passes/real_to_int.h"
+#include "preprocessing/passes/rewrite.h"
+#include "preprocessing/passes/sep_skolem_emp.h"
+#include "preprocessing/passes/sort_infer.h"
+#include "preprocessing/passes/static_learning.h"
+#include "preprocessing/passes/sygus_inference.h"
+#include "preprocessing/passes/symmetry_breaker.h"
+#include "preprocessing/passes/symmetry_detect.h"
+#include "preprocessing/passes/synth_rew_rules.h"
+#include "preprocessing/passes/theory_preprocess.h"
+#include "preprocessing/passes/unconstrained_simplifier.h"
#include "preprocessing/preprocessing_pass.h"
namespace CVC4 {
namespace preprocessing {
+using namespace CVC4::preprocessing::passes;
+
PreprocessingPassRegistry& PreprocessingPassRegistry::getInstance()
{
static PreprocessingPassRegistry* ppReg = new PreprocessingPassRegistry();
const std::string& name,
std::function<PreprocessingPass*(PreprocessingPassContext*)> ctor)
{
+ AlwaysAssert(!ContainsKey(d_ppInfo, name));
d_ppInfo[name] = ctor;
}
return d_ppInfo.find(name) != d_ppInfo.end();
}
+namespace {
+
+/**
+ * This method is stored by the `PreprocessingPassRegistry` and used to create
+ * a new instance of the preprocessing pass T.
+ *
+ * @param ppCtx The preprocessing pass context passed to the constructor of
+ * the preprocessing pass
+ */
+template <class T>
+PreprocessingPass* callCtor(PreprocessingPassContext* ppCtx)
+{
+ return new T(ppCtx);
+}
+
+} // namespace
+
+PreprocessingPassRegistry::PreprocessingPassRegistry()
+{
+ registerPassInfo("apply-substs", callCtor<ApplySubsts>);
+ registerPassInfo("bv-gauss", callCtor<BVGauss>);
+ registerPassInfo("static-learning", callCtor<StaticLearning>);
+ registerPassInfo("ite-simp", callCtor<ITESimp>);
+ registerPassInfo("apply-to-const", callCtor<ApplyToConst>);
+ registerPassInfo("global-negate", callCtor<GlobalNegate>);
+ registerPassInfo("int-to-bv", callCtor<IntToBV>);
+ registerPassInfo("synth-rr", callCtor<SynthRewRulesPass>);
+ registerPassInfo("real-to-int", callCtor<RealToInt>);
+ registerPassInfo("sygus-infer", callCtor<SygusInference>);
+ registerPassInfo("bv-to-bool", callCtor<BVToBool>);
+ registerPassInfo("bv-intro-pow2", callCtor<BvIntroPow2>);
+ registerPassInfo("sort-inference", callCtor<SortInferencePass>);
+ registerPassInfo("sep-skolem-emp", callCtor<SepSkolemEmp>);
+ registerPassInfo("rewrite", callCtor<Rewrite>);
+ registerPassInfo("bv-abstraction", callCtor<BvAbstraction>);
+ registerPassInfo("bv-eager-atoms", callCtor<BvEagerAtoms>);
+ registerPassInfo("pseudo-boolean-processor",
+ callCtor<PseudoBooleanProcessor>);
+ registerPassInfo("unconstrained-simplifier",
+ callCtor<UnconstrainedSimplifier>);
+ registerPassInfo("quantifiers-preprocess", callCtor<QuantifiersPreprocess>);
+ registerPassInfo("ite-removal", callCtor<IteRemoval>);
+ registerPassInfo("miplib-trick", callCtor<MipLibTrick>);
+ registerPassInfo("non-clausal-simp", callCtor<NonClausalSimp>);
+ registerPassInfo("bv-ackermann", callCtor<BVAckermann>);
+ registerPassInfo("sym-break", callCtor<SymBreakerPass>);
+ registerPassInfo("ext-rew-pre", callCtor<ExtRewPre>);
+ registerPassInfo("theory-preprocess", callCtor<TheoryPreprocess>);
+ registerPassInfo("quantifier-macros", callCtor<QuantifierMacros>);
+ registerPassInfo("nl-ext-purify", callCtor<NlExtPurify>);
+ registerPassInfo("bool-to-bv", callCtor<BoolToBV>);
+}
+
} // namespace preprocessing
} // namespace CVC4
** \brief The preprocessing pass registry
**
** This file defines the classes PreprocessingPassRegistry, which keeps track
- ** of the available preprocessing passes, and RegisterPass, which registers a
- ** preprocessing pass with the registry.
+ ** of the available preprocessing passes.
**/
#include "cvc4_private.h"
bool hasPass(const std::string& name);
private:
+ /**
+ * Private constructor for the preprocessing pass registry. The
+ * registry is a singleton and no other instance should be created.
+ */
+ PreprocessingPassRegistry();
+
/**
* Map of available preprocessing passes, mapping from preprocessing pass
* name to a function that constructs a corresponding instance.
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
projects / cvc5.git / commitdiff