cherry-picked registry branch

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 46c925e43..d58a932ca 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"
@@ -129,7 +131,14 @@ class PreprocessingPass {
   //d_assertions.push_back(Rewriter::rewrite(n));
   }
 
-  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);
+    }
   }
 
   PreprocessingPass(ResourceManager* resourceManager, Node dtrue) : d_resourceManager(resourceManager), d_true(dtrue){
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 c72262406..84c1700ec 100644
--- a/src/preproc/preprocessing_passes_core.cpp
+++ b/src/preproc/preprocessing_passes_core.cpp
@@ -205,9 +205,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;
@@ -1030,7 +1030,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 7bd9fdf39..2cf5feffc 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 dc5740f8c..78b5535d8 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"
@@ -3516,8 +3517,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() ){