Refactor IteRemoval preprocessing pass (#1793)

This commit refactors the IteRemoval pass to follow the new format.
In addition to moving the code, this entails the following changes:

- The timer for the ITE removal is now called differently (the default
  timer of PreprocessingPass is used) and measures just the
  preprocessing pass without applySubstitutions(). It also measures the
  time used by both invocations of the ITE removal pass.
- Debug output will be slightly different because we now just rely on
  the default functionality of PreprocessingPass.
- d_iteRemover is now passed into the PreprocessingPassContext.
- AssertionPipeline now owns the d_iteSkolemMap, which makes it
  accessible by preprocessing passes. The idea behind this is that the
  preprocessing passes collect information in AssertionPipeline and
  d_iteSkolemMap fits that pattern.

5 files changed, 117 insertions, 4 deletions

diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
new file mode 100644
index 000000000..86c40a793
--- /dev/null
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -0,0 +1,49 @@
+/*********************                                                        */
+/*! \file ite_removal.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Tim King, Paul Meng
+ ** 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 Remove ITEs from the assertions
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "preprocessing/passes/ite_removal.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+
+IteRemoval::IteRemoval(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "ite-removal")
+{
+}
+
+PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
+{
+  d_preprocContext->spendResource(options::preprocessStep());
+
+  // Remove all of the ITE occurrences and normalize
+  d_preprocContext->getIteRemover()->run(
+      assertions->ref(), assertions->getIteSkolemMap(), true);
+  for (unsigned i = 0, size = assertions->size(); i < size; ++i)
+  {
+    assertions->replace(i, Rewriter::rewrite((*assertions)[i]));
+  }
+
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/ite_removal.h b/src/preprocessing/passes/ite_removal.h
new file mode 100644
index 000000000..27ec4f095
--- /dev/null
+++ b/src/preprocessing/passes/ite_removal.h
@@ -0,0 +1,46 @@
+/*********************                                                        */
+/*! \file ite_removal.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Tim King, Paul Meng
+ ** 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 Remove ITEs from the assertions
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
+#define __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
+
+#include <unordered_set>
+#include <vector>
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class IteRemoval : public PreprocessingPass
+{
+ public:
+  IteRemoval(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(AssertionPipeline* assertions) override;
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif  // __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
index 441d1c7cd..6f76b60e9 100644
--- a/src/preprocessing/preprocessing_pass.h
+++ b/src/preprocessing/preprocessing_pass.h
@@ -38,6 +38,7 @@
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/term_formula_removal.h"
 #include "theory/substitutions.h"
 
 namespace CVC4 {
@@ -86,6 +87,8 @@ class AssertionPipeline
    */
   void replace(size_t i, const std::vector<Node>& ns);
 
+  IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
+
   context::CDO<unsigned>& getSubstitutionsIndex()
   {
     return d_substitutionsIndex;
@@ -99,12 +102,17 @@ class AssertionPipeline
  private:
   std::vector<Node> d_nodes;
 
+  /**
+   * Map from skolem variables to index in d_assertions containing
+   * corresponding introduced Boolean ite
+   */
+  IteSkolemMap d_iteSkolemMap;
+  
   /* Index for where to store substitutions */
   context::CDO<unsigned> d_substitutionsIndex;
 
   /* The top level substitutions */
   theory::SubstitutionMap d_topLevelSubstitutions;
-
 }; /* class AssertionPipeline */
 
 /**
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 1f3d245d7..31987b00b 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -20,8 +20,10 @@ namespace CVC4 {
 namespace preprocessing {
 
 PreprocessingPassContext::PreprocessingPassContext(
-    SmtEngine* smt, ResourceManager* resourceManager)
-    : d_smt(smt), d_resourceManager(resourceManager)
+    SmtEngine* smt,
+    ResourceManager* resourceManager,
+    RemoveTermFormulas* iteRemover)
+    : d_smt(smt), d_resourceManager(resourceManager), d_iteRemover(iteRemover)
 {
 }
 
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index 9927cd8fb..b50421e6c 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -24,6 +24,7 @@
 #include "context/context.h"
 #include "decision/decision_engine.h"
 #include "smt/smt_engine.h"
+#include "smt/term_formula_removal.h"
 #include "theory/theory_engine.h"
 #include "util/resource_manager.h"
 
@@ -33,12 +34,16 @@ namespace preprocessing {
 class PreprocessingPassContext
 {
  public:
-  PreprocessingPassContext(SmtEngine* smt, ResourceManager* resourceManager);
+  PreprocessingPassContext(SmtEngine* smt,
+                           ResourceManager* resourceManager,
+                           RemoveTermFormulas* iteRemover);
   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; }
   context::Context* getUserContext() { return d_smt->d_userContext; }
+  RemoveTermFormulas* getIteRemover() { return d_iteRemover; }
+
   void spendResource(unsigned amount)
   {
     d_resourceManager->spendResource(amount);
@@ -51,6 +56,9 @@ class PreprocessingPassContext
   /* Pointer to the SmtEngine that this context was created in. */
   SmtEngine* d_smt;
   ResourceManager* d_resourceManager;
+
+  /** Instance of the ITE remover */
+  RemoveTermFormulas* d_iteRemover;
 };  // class PreprocessingPassContext
 
 }  // namespace preprocessing