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.

1 files changed, 1 insertions, 88 deletions

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.
  */