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, 59 insertions, 0 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