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, 3 insertions, 3 deletions

diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index bad80d4ef..d26b28eeb 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -19,6 +19,7 @@
 #ifndef __CVC4__DECISION__DECISION_STRATEGY_H
 #define __CVC4__DECISION__DECISION_STRATEGY_H
 
+#include "preprocessing/assertion_pipeline.h"
 #include "prop/sat_solver_types.h"
 #include "smt/term_formula_removal.h"
 
@@ -57,9 +58,8 @@ public:
 
   bool needIteSkolemMap() override { return true; }
 
-  virtual void addAssertions(const std::vector<Node> &assertions,
-                             unsigned assertionsEnd,
-                             IteSkolemMap iteSkolemMap) = 0;
+  virtual void addAssertions(
+      const preprocessing::AssertionPipeline& assertions) = 0;
 };/* class ITEDecisionStrategy */
 
 class RelevancyStrategy : public ITEDecisionStrategy {