Add new infrastructure for preprocessing passes (#1053)

This commit adds new infrastructure for preprocessing passes. It is preparation only, it does not change how the current preprocessing passes work (this will be done in future commits).

6 files changed, 404 insertions, 0 deletions

diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
new file mode 100644
index 000000000..bf2e59229
--- /dev/null
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -0,0 +1,94 @@
+/*********************                                                        */
+/*! \file preprocessing_pass.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **  Justin Xu
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The preprocessing pass super class
+ **
+ ** Preprocessing pass super class.
+ **/
+
+#include "preprocessing/preprocessing_pass.h"
+
+#include "expr/node_manager.h"
+#include "proof/proof.h"
+#include "smt/dump.h"
+#include "smt/smt_statistics_registry.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+void AssertionPipeline::replace(size_t i, Node n) {
+  PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]););
+  d_nodes[i] = n;
+}
+
+void AssertionPipeline::replace(size_t i,
+                                Node n,
+                                const std::vector<Node>& addnDeps)
+{
+  PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]);
+        for (const auto& addnDep
+             : addnDeps) {
+          ProofManager::currentPM()->addDependence(n, addnDep);
+        });
+  d_nodes[i] = n;
+}
+
+void AssertionPipeline::replace(size_t i, const std::vector<Node>& ns)
+{
+  PROOF(
+      for (const auto& n
+           : ns) { ProofManager::currentPM()->addDependence(n, d_nodes[i]); });
+  d_nodes[i] = NodeManager::currentNM()->mkConst<bool>(true);
+
+  for (const auto& n : ns)
+  {
+    d_nodes.push_back(n);
+  }
+}
+
+PreprocessingPassResult PreprocessingPass::apply(
+    AssertionPipeline* assertionsToPreprocess) {
+  TimerStat::CodeTimer codeTimer(d_timer);
+  Trace("preprocessing") << "PRE " << d_name << std::endl;
+  Chat() << d_name << "..." << std::endl;
+  dumpAssertions(("pre-" + d_name).c_str(), *assertionsToPreprocess);
+  PreprocessingPassResult result = applyInternal(assertionsToPreprocess);
+  dumpAssertions(("post-" + d_name).c_str(), *assertionsToPreprocess);
+  Trace("preprocessing") << "POST " << d_name << std::endl;
+  return result;
+}
+
+void PreprocessingPass::dumpAssertions(const char* key,
+                                       const AssertionPipeline& assertionList) {
+  if (Dump.isOn("assertions") && Dump.isOn(std::string("assertions::") + key)) {
+    // Push the simplified assertions to the dump output stream
+    for (const auto& n : assertionList) {
+      Dump("assertions") << AssertCommand(Expr(n.toExpr()));
+    }
+  }
+}
+
+PreprocessingPass::PreprocessingPass(PreprocessingPassContext* preprocContext,
+                                     const std::string& name)
+    : d_name(name), d_timer("preprocessing::" + name) {
+  d_preprocContext = preprocContext;
+  smtStatisticsRegistry()->registerStat(&d_timer);
+}
+
+PreprocessingPass::~PreprocessingPass() {
+  Assert(smt::smtEngineInScope());
+  if (smtStatisticsRegistry() != nullptr) {
+    smtStatisticsRegistry()->unregisterStat(&d_timer);
+  }
+}
+
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
new file mode 100644
index 000000000..f7b30aa74
--- /dev/null
+++ b/src/preprocessing/preprocessing_pass.h
@@ -0,0 +1,126 @@
+/*********************                                                        */
+/*! \file preprocessing_pass.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **  Justin Xu
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The preprocessing pass super class
+ **
+ ** Implementation of the preprocessing pass super class. Preprocessing passes
+ ** that inherit from this class, need to pass their name to the constructor to
+ ** register the pass appropriately. The core of a preprocessing pass lives
+ ** in applyInternal(), which operates on a list of assertions and is called
+ ** from apply() in the super class. The apply() method automatically takes
+ ** care of the following:
+ **
+ ** - Dumping assertions before and after the pass
+ ** - Initializing the timer
+ ** - Tracing and chatting
+ **
+ ** Optionally, preprocessing passes can overwrite the initInteral() method to
+ ** do work that only needs to be done once.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_H
+#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_H
+
+#include <string>
+#include <vector>
+
+#include "expr/node.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "smt/smt_engine_scope.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+/* Assertion Pipeline stores a list of assertions modified by preprocessing
+ * passes. */
+class AssertionPipeline {
+  std::vector<Node> d_nodes;
+
+ public:
+  size_t size() const { return d_nodes.size(); }
+
+  void resize(size_t n) { d_nodes.resize(n); }
+  void clear() { d_nodes.clear(); }
+
+  Node& operator[](size_t i) { return d_nodes[i]; }
+  const Node& operator[](size_t i) const { return d_nodes[i]; }
+  void push_back(Node n) { d_nodes.push_back(n); }
+
+  std::vector<Node>& ref() { return d_nodes; }
+  const std::vector<Node>& ref() const { return d_nodes; }
+
+  std::vector<Node>::const_iterator begin() const { return d_nodes.cbegin(); }
+  std::vector<Node>::const_iterator end() const { return d_nodes.cend(); }
+
+  /*
+   * Replaces assertion i with node n and records the dependency between the
+   * original assertion and its replacement.
+   */
+  void replace(size_t i, Node n);
+
+  /*
+   * Replaces assertion i with node n and records that this replacement depends
+   * on assertion i and the nodes listed in addnDeps. The dependency
+   * information is used for unsat cores and proofs.
+   */
+  void replace(size_t i, Node n, const std::vector<Node>& addnDeps);
+
+  /*
+   * Replaces an assertion with a vector of assertions and records the
+   * dependencies.
+   */
+  void replace(size_t i, const std::vector<Node>& ns);
+}; /* class AssertionPipeline */
+
+/**
+ * Preprocessing passes return a result which indicates whether a conflict has
+ * been detected during preprocessing.
+ */
+enum PreprocessingPassResult { CONFLICT, NO_CONFLICT };
+
+class PreprocessingPass {
+ public:
+  /* Preprocesses a list of assertions assertionsToPreprocess */
+  PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess);
+
+  PreprocessingPass(PreprocessingPassContext* preprocContext,
+                    const std::string& name);
+  virtual ~PreprocessingPass();
+
+ protected:
+  /*
+   * Method for dumping assertions within a pass. Also called before and after
+   * applying the pass.
+   */
+  void dumpAssertions(const char* key, const AssertionPipeline& assertionList);
+
+  /*
+   * Abstract method that each pass implements to do the actual preprocessing.
+   */
+  virtual PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) = 0;
+
+  /* Context for Preprocessing Passes that initializes necessary variables */
+  PreprocessingPassContext* d_preprocContext;
+
+ private:
+  /* Name of pass */
+  std::string d_name;
+  /* Timer for registering the preprocessing time of this pass */
+  TimerStat d_timer;
+};
+
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_H */
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
new file mode 100644
index 000000000..a738f9484
--- /dev/null
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -0,0 +1,26 @@
+/*********************                                                        */
+/*! \file preprocessing_pass_context.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **  Justin Xu
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The preprocessing pass context for passes
+ **
+ ** The preprocessing pass context for passes.
+ **/
+
+#include "preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+PreprocessingPassContext::PreprocessingPassContext(SmtEngine* smt)
+    : d_smt(smt) {}
+
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
new file mode 100644
index 000000000..2e7a4eaf2
--- /dev/null
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -0,0 +1,49 @@
+/*********************                                                        */
+/*! \file preprocessing_pass_context.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **  Justin Xu
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The preprocessing pass context for passes
+ **
+ ** Implementation of the preprocessing pass context for passes. This context
+ ** allows preprocessing passes to retrieve information besides the assertions
+ ** from the solver and interact with it without getting full access.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
+#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
+
+#include "decision/decision_engine.h"
+#include "smt/smt_engine.h"
+#include "theory/arith/pseudoboolean_proc.h"
+#include "theory/booleans/circuit_propagator.h"
+#include "theory/theory_engine.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+class PreprocessingPassContext {
+ public:
+  PreprocessingPassContext(SmtEngine* smt);
+  SmtEngine* getSmt() { return d_smt; }
+  TheoryEngine* getTheoryEngine() { return d_smt->d_theoryEngine; }
+  DecisionEngine* getDecisionEngine() { return d_smt->d_decisionEngine; }
+  prop::PropEngine* getPropEngine() { return d_smt->d_propEngine; }
+
+ private:
+  /* Pointer to the SmtEngine that this context was created in. */
+  SmtEngine* d_smt;
+};  // class PreprocessingPassContext
+
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H */
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp
new file mode 100644
index 000000000..4f0693a25
--- /dev/null
+++ b/src/preprocessing/preprocessing_pass_registry.cpp
@@ -0,0 +1,49 @@
+/*********************                                                        */
+/*! \file preprocessing_pass_registry.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **  Justin Xu
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The preprocessing pass registry
+ **
+ ** The preprocessing pass registry.
+ **/
+
+#include "preprocessing/preprocessing_pass_registry.h"
+
+#include <utility>
+
+#include "base/cvc4_assert.h"
+#include "base/output.h"
+#include "preprocessing/preprocessing_pass.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+void PreprocessingPassRegistry::registerPass(
+    const std::string& ppName,
+    std::unique_ptr<PreprocessingPass> preprocessingPass) {
+  Debug("pp-registry") << "Registering pass " << ppName << std::endl;
+  Assert(preprocessingPass != nullptr);
+  Assert(!this->hasPass(ppName));
+  d_stringToPreprocessingPass[ppName] = std::move(preprocessingPass);
+}
+
+bool PreprocessingPassRegistry::hasPass(const std::string& ppName) {
+  return d_stringToPreprocessingPass.find(ppName) !=
+         d_stringToPreprocessingPass.end();
+}
+
+PreprocessingPass* PreprocessingPassRegistry::getPass(
+    const std::string& ppName) {
+  Assert(this->hasPass(ppName));
+  return d_stringToPreprocessingPass[ppName].get();
+}
+
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h
new file mode 100644
index 000000000..75c66a035
--- /dev/null
+++ b/src/preprocessing/preprocessing_pass_registry.h
@@ -0,0 +1,60 @@
+/*********************                                                        */
+/*! \file preprocessing_pass_registry.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **  Justin Xu
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \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.
+ **/
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
+#define __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
+
+#include <memory>
+#include <string>
+#include <unordered_map>
+
+#include "decision/decision_engine.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "theory/arith/pseudoboolean_proc.h"
+#include "theory/booleans/circuit_propagator.h"
+#include "theory/theory_engine.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+class PreprocessingPassRegistry {
+ public:
+  /**
+   *  Registers a pass with a unique name and takes ownership of it.
+   */
+  void registerPass(const std::string& ppName,
+                    std::unique_ptr<PreprocessingPass> preprocessingPass);
+
+  /**
+   * Retrieves a pass with a given name from registry.
+   */
+  PreprocessingPass* getPass(const std::string& ppName);
+
+ private:
+  bool hasPass(const std::string& ppName);
+
+  /* Stores all the registered preprocessing passes. */
+  std::unordered_map<std::string, std::unique_ptr<PreprocessingPass>>
+      d_stringToPreprocessingPass;
+};  // class PreprocessingPassRegistry
+
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H */