diff options
Diffstat (limited to 'src/preprocessing/preprocessing_pass_registry.h')
-rw-r--r-- | src/preprocessing/preprocessing_pass_registry.h | 100 |
1 files changed, 85 insertions, 15 deletions
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 |