Refactor how assertions are added to decision engine (#2396)

Before refactoring the preprocessing passes, we were using three
arguments to add assertions to the decision engine. Now all that
information lives in the AssertionPipeline. This commit moves the
AssertionPipeline to its own file and changes the `addAssertions()`
methods related to the decision engine to take an AssertionPipeline as
an arguement instead of three separate ones. Additionally, the
TheoryEngine now uses an AssertionPipeline for lemmas.

9 files changed, 189 insertions, 138 deletions

diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
new file mode 100644
index 000000000..0bce3b8cd
--- /dev/null
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -0,0 +1,59 @@
+/*********************                                                        */
+/*! \file assertion_pipeline.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 AssertionPipeline stores a list of assertions modified by
+ ** preprocessing passes
+ **/
+
+#include "preprocessing/assertion_pipeline.h"
+
+#include "expr/node_manager.h"
+#include "proof/proof.h"
+#include "proof/proof_manager.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+AssertionPipeline::AssertionPipeline() : d_realAssertionsEnd(0) {}
+
+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);
+  }
+}
+
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
new file mode 100644
index 000000000..af7a8dce3
--- /dev/null
+++ b/src/preprocessing/assertion_pipeline.h
@@ -0,0 +1,101 @@
+/*********************                                                        */
+/*! \file assertion_pipeline.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 AssertionPipeline stores a list of assertions modified by
+ ** preprocessing passes
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
+#define __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H
+
+#include <vector>
+
+#include "expr/node.h"
+#include "smt/term_formula_removal.h"
+
+namespace CVC4 {
+namespace preprocessing {
+
+/**
+ * Assertion Pipeline stores a list of assertions modified by preprocessing
+ * passes. It is assumed that all assertions after d_realAssertionsEnd were
+ * generated by ITE removal. Hence, d_iteSkolemMap maps into only these.
+ */
+class AssertionPipeline
+{
+ public:
+  AssertionPipeline();
+
+  size_t size() const { return d_nodes.size(); }
+
+  void resize(size_t n) { d_nodes.resize(n); }
+
+  void clear()
+  {
+    d_nodes.clear();
+    d_realAssertionsEnd = 0;
+  }
+
+  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);
+
+  IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
+  const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; }
+
+  size_t getRealAssertionsEnd() const { return d_realAssertionsEnd; }
+
+  void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); }
+
+ private:
+  std::vector<Node> d_nodes;
+
+  /**
+   * Map from skolem variables to index in d_assertions containing
+   * corresponding introduced Boolean ite
+   */
+  IteSkolemMap d_iteSkolemMap;
+
+  /** Size of d_nodes when preprocessing starts */
+  size_t d_realAssertionsEnd;
+}; /* class AssertionPipeline */
+
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__ASSERTION_PIPELINE_H */
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index 6fb4b7793..f5c3520d0 100644
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -44,8 +44,9 @@ PreprocessingPassResult ApplySubsts::applyInternal(
     // When solving incrementally, all substitutions are piled into the
     // assertion at d_substitutionsIndex: we don't want to apply substitutions
     // to this assertion or information will be lost.
-    context::CDO<unsigned>& substs_index =
-        assertionsToPreprocess->getSubstitutionsIndex();
+    unsigned substs_index = d_preprocContext->getSubstitutionsIndex();
+    theory::SubstitutionMap& substMap =
+        d_preprocContext->getTopLevelSubstitutions();
     unsigned size = assertionsToPreprocess->size();
     unsigned substitutionAssertion = substs_index > 0 ? substs_index : size;
     for (unsigned i = 0; i < size; ++i)
@@ -57,11 +58,9 @@ PreprocessingPassResult ApplySubsts::applyInternal(
       Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i]
                         << std::endl;
       d_preprocContext->spendResource(options::preprocessStep());
-      assertionsToPreprocess->replace(
-          i,
-          theory::Rewriter::rewrite(
-              assertionsToPreprocess->getTopLevelSubstitutions().apply(
-                  (*assertionsToPreprocess)[i])));
+      assertionsToPreprocess->replace(i,
+                                      theory::Rewriter::rewrite(substMap.apply(
+                                          (*assertionsToPreprocess)[i])));
       Trace("apply-substs") << "  got " << (*assertionsToPreprocess)[i]
                         << std::endl;
     }
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 81588d039..616ecd969 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -188,7 +188,7 @@ PreprocessingPassResult MipLibTrick::applyInternal(
       propagator->getBackEdges();
   unordered_set<unsigned long> removeAssertions;
   SubstitutionMap& top_level_substs =
-      assertionsToPreprocess->getTopLevelSubstitutions();
+      d_preprocContext->getTopLevelSubstitutions();
 
   NodeManager* nm = NodeManager::currentNM();
   Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1));
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index e2ce1c301..653aed8ad 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -76,8 +76,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
 
   // Assert all the assertions to the propagator
   Trace("non-clausal-simplify") << "asserting to propagator" << std::endl;
-  context::CDO<unsigned>& substs_index =
-      assertionsToPreprocess->getSubstitutionsIndex();
+  unsigned substs_index = d_preprocContext->getSubstitutionsIndex();
   for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
   {
     Assert(Rewriter::rewrite((*assertionsToPreprocess)[i])
@@ -114,7 +113,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
       << " learned literals." << std::endl;
   // No conflict, go through the literals and solve them
   SubstitutionMap& top_level_substs =
-      assertionsToPreprocess->getTopLevelSubstitutions();
+      d_preprocContext->getTopLevelSubstitutions();
   SubstitutionMap constantPropagations(d_preprocContext->getUserContext());
   SubstitutionMap newSubstitutions(d_preprocContext->getUserContext());
   SubstitutionMap::iterator pos;
diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index 6a7078696..6a1d89d33 100644
--- a/src/preprocessing/preprocessing_pass.cpp
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -16,51 +16,12 @@
 
 #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 {
 
-AssertionPipeline::AssertionPipeline(context::Context* context)
-    : d_substitutionsIndex(context, 0),
-      d_topLevelSubstitutions(context),
-      d_realAssertionsEnd(0)
-{
-}
-
-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);
diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
index 4143f2d4b..448cacb87 100644
--- a/src/preprocessing/preprocessing_pass.h
+++ b/src/preprocessing/preprocessing_pass.h
@@ -32,103 +32,16 @@
 #define __CVC4__PREPROCESSING__PREPROCESSING_PASS_H
 
 #include <string>
-#include <vector>
 
-#include "context/cdo.h"
-#include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_engine_scope.h"
-#include "smt/term_formula_removal.h"
 #include "theory/logic_info.h"
-#include "theory/substitutions.h"
 
 namespace CVC4 {
 namespace preprocessing {
 
 /**
- * Assertion Pipeline stores a list of assertions modified by preprocessing
- * passes.
- */
-class AssertionPipeline
-{
- public:
-  AssertionPipeline(context::Context* context);
-
-  size_t size() const { return d_nodes.size(); }
-
-  void resize(size_t n) { d_nodes.resize(n); }
-
-  void clear()
-  {
-    d_nodes.clear();
-    d_realAssertionsEnd = 0;
-  }
-
-  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);
-
-  IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
-
-  context::CDO<unsigned>& getSubstitutionsIndex()
-  {
-    return d_substitutionsIndex;
-  }
-
-  theory::SubstitutionMap& getTopLevelSubstitutions()
-  {
-    return d_topLevelSubstitutions;
-  }
-
-  size_t getRealAssertionsEnd() { return d_realAssertionsEnd; }
-
-  void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); }
-
- 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;
-
-  /** Size of d_nodes when preprocessing starts */
-  size_t d_realAssertionsEnd;
-}; /* class AssertionPipeline */
-
-/**
  * Preprocessing passes return a result which indicates whether a conflict has
  * been detected during preprocessing.
  */
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 15f5d3eb0..3f72a4559 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -29,6 +29,8 @@ PreprocessingPassContext::PreprocessingPassContext(
     : d_smt(smt),
       d_resourceManager(resourceManager),
       d_iteRemover(iteRemover),
+      d_substitutionsIndex(smt->d_userContext, 0),
+      d_topLevelSubstitutions(smt->d_userContext),
       d_circuitPropagator(circuitPropagator),
       d_symsInAssertions(smt->d_userContext)
 {
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index ae989d700..3eb0f10b5 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -21,6 +21,7 @@
 #ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
 #define __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
 
+#include "context/cdo.h"
 #include "context/context.h"
 #include "decision/decision_engine.h"
 #include "preprocessing/util/ite_utilities.h"
@@ -70,6 +71,16 @@ class PreprocessingPassContext
   /* Widen the logic to include the given theory. */
   void widenLogic(theory::TheoryId id);
 
+  unsigned getSubstitutionsIndex() const { return d_substitutionsIndex.get(); }
+
+  void setSubstitutionsIndex(unsigned i) { d_substitutionsIndex = i; }
+
+  /** Gets a reference to the top-level substitution map */
+  theory::SubstitutionMap& getTopLevelSubstitutions()
+  {
+    return d_topLevelSubstitutions;
+  }
+
   /* Enable Integers. */
   void enableIntegers();
 
@@ -90,6 +101,12 @@ class PreprocessingPassContext
   /** Instance of the ITE remover */
   RemoveTermFormulas* d_iteRemover;
 
+  /* Index for where to store substitutions */
+  context::CDO<unsigned> d_substitutionsIndex;
+
+  /* The top level substitutions */
+  theory::SubstitutionMap d_topLevelSubstitutions;
+
   /** Instance of the circuit propagator */
   theory::booleans::CircuitPropagator* d_circuitPropagator;