From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 31 Oct 2018 14:23:09 +0000 (-0700)
Subject: Record assumption info in AssertionPipeline (#2678)
X-Git-Tag: cvc5-1.0.0~4385
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6a89ff6d106a012442f0ab3b212dc3d26a758da3;p=cvc5.git

Record assumption info in AssertionPipeline (#2678)
---

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
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 9a0d969d8..cb7766c2d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -756,8 +756,14 @@ class SmtEnginePrivate : public NodeManagerListener {
    * immediately, or it might be simplified and kept, or it might not
    * even be simplified.
    * the 2nd and 3rd arguments added for bookkeeping for proofs
+   *
+   * @param isAssumption If true, the formula is considered to be an assumption
+   * (this is used to distinguish assertions and assumptions)
    */
-  void addFormula(TNode n, bool inUnsatCore, bool inInput = true);
+  void addFormula(TNode n,
+                  bool inUnsatCore,
+                  bool inInput = true,
+                  bool isAssumption = false);
 
   /** Expand definitions in n. */
   Node expandDefinitions(TNode n,
@@ -3071,7 +3077,8 @@ void SmtEnginePrivate::processAssertions() {
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() begin" << endl;
   Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
 
-  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
+  Debug("smt") << "#Assertions : " << d_assertions.size() << endl;
+  Debug("smt") << "#Assumptions: " << d_assertions.getNumAssumptions() << endl;
 
   if (d_assertions.size() == 0) {
     // nothing to do
@@ -3450,14 +3457,20 @@ void SmtEnginePrivate::processAssertions() {
   getIteSkolemMap().clear();
 }
 
-void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput)
+void SmtEnginePrivate::addFormula(TNode n,
+                                  bool inUnsatCore,
+                                  bool inInput,
+                                  bool isAssumption)
 {
   if (n == d_true) {
     // nothing to do
     return;
   }
 
-  Trace("smt") << "SmtEnginePrivate::addFormula(" << n << "), inUnsatCore = " << inUnsatCore << ", inInput = " << inInput << endl;
+  Trace("smt") << "SmtEnginePrivate::addFormula(" << n
+               << "), inUnsatCore = " << inUnsatCore
+               << ", inInput = " << inInput
+               << ", isAssumption = " << isAssumption << endl;
 
   // Give it to proof manager
   PROOF(
@@ -3480,7 +3493,7 @@ void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput)
   );
 
   // Add the normalized formula to the queue
-  d_assertions.push_back(n);
+  d_assertions.push_back(n, isAssumption);
   //d_assertions.push_back(Rewriter::rewrite(n));
 }
 
@@ -3602,7 +3615,7 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
       {
         d_assertionList->push_back(e);
       }
-      d_private->addFormula(e.getNode(), inUnsatCore);
+      d_private->addFormula(e.getNode(), inUnsatCore, true, true);
     }
 
     r = isQuery ? check().asValidityResult() : check().asSatisfiabilityResult();