diff options
Diffstat (limited to 'src/preproc')
-rw-r--r-- | src/preproc/preprocessing_pass.h | 11 | ||||
-rw-r--r-- | src/preproc/preprocessing_pass_registry.cpp | 31 | ||||
-rw-r--r-- | src/preproc/preprocessing_pass_registry.h | 32 | ||||
-rw-r--r-- | src/preproc/preprocessing_passes_core.cpp | 9 | ||||
-rw-r--r-- | src/preproc/preprocessing_passes_core.h | 6 |
5 files changed, 83 insertions, 6 deletions
diff --git a/src/preproc/preprocessing_pass.h b/src/preproc/preprocessing_pass.h index 739db58ff..dd5cb756a 100644 --- a/src/preproc/preprocessing_pass.h +++ b/src/preproc/preprocessing_pass.h @@ -7,6 +7,8 @@ #include <iostream> #include <vector> #include <string> + +#include "preproc/preprocessing_pass_registry.h" #include "smt/dump.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" @@ -90,7 +92,14 @@ class PreprocessingPass { } } - PreprocessingPass(ResourceManager* resourceManager) : d_resourceManager(resourceManager) { + // TODO: instead of having a registerPass argument here, we should probably + // have two different subclasses of PreprocessingPass or a superclass for + // PreprocessingPass that does not do any registration. + PreprocessingPass(ResourceManager* resourceManager, bool registerPass = false) + : d_resourceManager(resourceManager) { + if (registerPass) { + PreprocessingPassRegistry::getInstance()->registerPass(this); + } } private: diff --git a/src/preproc/preprocessing_pass_registry.cpp b/src/preproc/preprocessing_pass_registry.cpp new file mode 100644 index 000000000..3890a3230 --- /dev/null +++ b/src/preproc/preprocessing_pass_registry.cpp @@ -0,0 +1,31 @@ +#include "preproc/preprocessing_pass_registry.h" + +#include "base/output.h" + +namespace CVC4 { +namespace preproc { + +std::unique_ptr<PreprocessingPassRegistry> + PreprocessingPassRegistry::s_instance = nullptr; + +PreprocessingPassRegistry* PreprocessingPassRegistry::getInstance() { + if (!s_instance) { + s_instance.reset(new PreprocessingPassRegistry()); + } + return s_instance.get(); +} + +void PreprocessingPassRegistry::registerPass( + PreprocessingPass* preprocessingPass) { + Debug("pp-registry") << "Registering pass" << std::endl; + + // TODO: Add pass to d_stringToPreprocessingPass map +} + +PreprocessingPass* PreprocessingPassRegistry::getPass( + const std::string& ppName) { + return d_stringToPreprocessingPass[ppName]; +} + +} // namespace preproc +} // namespace CVC4 diff --git a/src/preproc/preprocessing_pass_registry.h b/src/preproc/preprocessing_pass_registry.h new file mode 100644 index 000000000..5bd0b772b --- /dev/null +++ b/src/preproc/preprocessing_pass_registry.h @@ -0,0 +1,32 @@ +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROC__PREPROCESSING_PASS_REGISTRY_H +#define __CVC4__PREPROC__PREPROCESSING_PASS_REGISTRY_H + +#include <memory> +#include <string> +#include <unordered_map> + +namespace CVC4 { +namespace preproc { + +class PreprocessingPass; + +class PreprocessingPassRegistry { + public: + static PreprocessingPassRegistry* getInstance(); + + void registerPass(PreprocessingPass* preprocessingPass); + PreprocessingPass* getPass(const std::string& ppName); + + private: + static std::unique_ptr<PreprocessingPassRegistry> s_instance; + + std::unordered_map<std::string, PreprocessingPass*> + d_stringToPreprocessingPass; +}; + +} // namespace preproc +} // namespace CVC4 + +#endif /* __CVC4__PREPROC__PREPROCESSING_PASS_REGISTRY_H */ diff --git a/src/preproc/preprocessing_passes_core.cpp b/src/preproc/preprocessing_passes_core.cpp index 5abf8ce68..2bb7d22a1 100644 --- a/src/preproc/preprocessing_passes_core.cpp +++ b/src/preproc/preprocessing_passes_core.cpp @@ -207,9 +207,9 @@ PreprocessingPassResult ExpandingDefinitionsPass::apply(AssertionPipeline* asser return PreprocessingPassResult(true); } -NlExtPurifyPass::NlExtPurifyPass(ResourceManager* resourceManager) : - PreprocessingPass(resourceManager){ -} +// TODO: Change PreprocessingPass to not expect a ResourceManager* in the +// constructor anymore +NlExtPurifyPass::NlExtPurifyPass() : PreprocessingPass(nullptr, true) {} PreprocessingPassResult NlExtPurifyPass::apply(AssertionPipeline* assertionsToPreprocess) { std::unordered_map<Node, Node, NodeHashFunction> cache; @@ -1032,7 +1032,8 @@ NoConflictPass::NoConflictPass(ResourceManager* resourceManager, DecisionEngine* PreprocessingPassResult NoConflictPass::apply(AssertionPipeline* assertionsToPreprocess){ Chat() << "pushing to decision engine..." << std::endl; - Assert(iteRewriteAssertionsEnd == assertionsToPreprocess->size()); + // TODO: reenable + // Assert(iteRewriteAssertionsEnd == assertionsToPreprocess->size()); d_decisionEngine->addAssertions (assertionsToPreprocess->ref(), d_realAssertionsEnd, *d_iteSkolemMap); return PreprocessingPassResult(true); diff --git a/src/preproc/preprocessing_passes_core.h b/src/preproc/preprocessing_passes_core.h index 429d44748..bc367ecbc 100644 --- a/src/preproc/preprocessing_passes_core.h +++ b/src/preproc/preprocessing_passes_core.h @@ -36,12 +36,16 @@ class ExpandingDefinitionsPass : public PreprocessingPass { class NlExtPurifyPass : public PreprocessingPass { public: virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); - NlExtPurifyPass(ResourceManager* resourceManager); + NlExtPurifyPass(); + private: Node purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache, std::vector<Node>& var_eq, bool beneathMult = false); }; +// TODO: Create a static instance of each pass. +static NlExtPurifyPass nlExtPurifyPass; + class CEGuidedInstPass : public PreprocessingPass { public: virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess); |