(proof-new) Preprocessing passes use proper interfaces to assertions pipeline (#5164)

This PR eliminates all uses of assertions pipeline that are not proper, which two-fold:
(1) The assertion list should never be modified in a custom way (without going through replace / push_back),
(2) Places where an assertion is "conjoined" to an existing spot in the vector should use conjoin instead of replace.
This is required for proper proof generation.

This fixes CVC4/cvc4-projects#75.

1 files changed, 4 insertions, 3 deletions

diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h
index fbddf7169..c82bf7958 100644
--- a/src/preprocessing/util/ite_utilities.h
+++ b/src/preprocessing/util/ite_utilities.h
@@ -27,6 +27,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "util/hash.h"
 #include "util/statistics_registry.h"
 
@@ -74,7 +75,7 @@ class ITEUtilities
   bool simpIteDidALotOfWorkHeuristic() const;
 
   /* returns false if an assertion is discovered to be equal to false. */
-  bool compress(std::vector<Node>& assertions);
+  bool compress(AssertionPipeline* assertionsToPreprocess);
 
   Node simplifyWithCare(TNode e);
 
@@ -167,7 +168,7 @@ class ITECompressor
   ~ITECompressor();
 
   /* returns false if an assertion is discovered to be equal to false. */
-  bool compress(std::vector<Node>& assertions);
+  bool compress(AssertionPipeline* assertionsToPreprocess);
 
   /* garbage Collects the compressor. */
   void garbageCollect();
@@ -176,7 +177,7 @@ class ITECompressor
   Node d_true;  /* Copy of true. */
   Node d_false; /* Copy of false. */
   ContainsTermITEVisitor* d_contains;
-  std::vector<Node>* d_assertions;
+  AssertionPipeline* d_assertions;
   IncomingArcCounter d_incoming;
 
   typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;