Record assumption info in AssertionPipeline (#2678)

2 files changed, 55 insertions, 7 deletions

diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 0bce3b8cd..7d4351baa 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -22,7 +22,36 @@
 namespace CVC4 {
 namespace preprocessing {
 
-AssertionPipeline::AssertionPipeline() : d_realAssertionsEnd(0) {}
+AssertionPipeline::AssertionPipeline()
+    : d_realAssertionsEnd(0), d_assumptionsStart(0), d_numAssumptions(0)
+{
+}
+
+void AssertionPipeline::clear()
+{
+  d_nodes.clear();
+  d_realAssertionsEnd = 0;
+  d_assumptionsStart = 0;
+  d_numAssumptions = 0;
+}
+
+void AssertionPipeline::push_back(Node n, bool isAssumption)
+{
+  d_nodes.push_back(n);
+  if (isAssumption)
+  {
+    if (d_numAssumptions == 0)
+    {
+      d_assumptionsStart = d_nodes.size() - 1;
+    }
+    // Currently, we assume that assumptions are all added one after another
+    // and that we store them in the same vector as the assertions. Once we
+    // split the assertions up into multiple vectors (see issue #2473), we will
+    // not have this limitation anymore.
+    Assert(d_assumptionsStart + d_numAssumptions == d_nodes.size() - 1);
+    d_numAssumptions++;
+  }
+}
 
 void AssertionPipeline::replace(size_t i, Node n)
 {
diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
index af7a8dce3..77c5c4582 100644
--- a/src/preprocessing/assertion_pipeline.h
+++ b/src/preprocessing/assertion_pipeline.h
@@ -40,15 +40,22 @@ class AssertionPipeline
 
   void resize(size_t n) { d_nodes.resize(n); }
 
-  void clear()
-  {
-    d_nodes.clear();
-    d_realAssertionsEnd = 0;
-  }
+  /**
+   * Clear the list of assertions and assumptions.
+   */
+  void clear();
 
   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); }
+
+  /**
+   * Adds an assertion/assumption to be preprocessed.
+   *
+   * @param n The assertion/assumption
+   * @param isAssumption If true, records that \p n is an assumption. Note that
+   * all assumptions have to be added contiguously.
+   */
+  void push_back(Node n, bool isAssumption = false);
 
   std::vector<Node>& ref() { return d_nodes; }
   const std::vector<Node>& ref() const { return d_nodes; }
@@ -80,9 +87,16 @@ class AssertionPipeline
 
   size_t getRealAssertionsEnd() const { return d_realAssertionsEnd; }
 
+  /** @return The index of the first assumption */
+  size_t getAssumptionsStart() const { return d_assumptionsStart; }
+
+  /** @return The number of assumptions */
+  size_t getNumAssumptions() const { return d_numAssumptions; }
+
   void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); }
 
  private:
+  /** The list of current assertions */
   std::vector<Node> d_nodes;
 
   /**
@@ -93,6 +107,11 @@ class AssertionPipeline
 
   /** Size of d_nodes when preprocessing starts */
   size_t d_realAssertionsEnd;
+
+  /** Index of the first assumption */
+  size_t d_assumptionsStart;
+  /** The number of assumptions */
+  size_t d_numAssumptions;
 }; /* class AssertionPipeline */
 
 }  // namespace preprocessing