diff options
author | Andres Noetzli <noetzli@stanford.edu> | 2017-07-26 17:19:10 -0700 |
---|---|---|
committer | Andres Noetzli <noetzli@stanford.edu> | 2017-07-26 17:55:57 -0700 |
commit | 673ee2e5b8414d3155d83ca4c16269c1a02632ad (patch) | |
tree | faa442d6a7018e075f7f709b3aac2c18a8472a15 | |
parent | 7d0ddc953192d34f9924cd1a0565681636627e05 (diff) |
Initial work on PreprocessingPassRegistryrefactor_pp_registry
-rw-r--r-- | src/Makefile.am | 4 | ||||
-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 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 7 |
7 files changed, 92 insertions, 8 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 45e5c6627..de6d755dc 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -62,8 +62,10 @@ libcvc4_la_SOURCES = \ decision/justification_heuristic.cpp \ decision/justification_heuristic.h \ preproc/preprocessing_pass.h \ - preproc/preprocessing_passes_core.h \ + preproc/preprocessing_pass_registry.cpp \ + preproc/preprocessing_pass_registry.h \ preproc/preprocessing_passes_core.cpp \ + preproc/preprocessing_passes_core.h \ printer/dagification_visitor.cpp \ printer/dagification_visitor.h \ printer/printer.cpp \ 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); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 159201e71..215fb89ae 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -65,6 +65,7 @@ #include "options/strings_options.h" #include "options/theory_options.h" #include "options/uf_options.h" +#include "preproc/preprocessing_pass_registry.h" #include "preproc/preprocessing_passes_core.h" #include "printer/printer.h" #include "proof/proof.h" @@ -3518,8 +3519,12 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertions : " << d_assertions.size() << endl; if( options::nlExtPurify() ){ - preproc::NlExtPurifyPass pass(d_resourceManager); + preproc::NlExtPurifyPass pass; pass.apply(&d_assertions); + + // TODO: With the PreprocessingPassRegistry, it should be possible to do + // something like this: + // PreprocessingPassRegistry::getInstance()->getPass("nl-ext-purify")->apply(&d_assertions); } if( options::ceGuidedInst() ){ |