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.

5 files changed, 32 insertions, 54 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 8e419e768..01f78f2d6 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -98,31 +98,21 @@ SatValue DecisionEngine::getPolarity(SatVariable var)
   }
 }
 
-void DecisionEngine::addAssertions(const vector<Node> &assertions)
-{
-  Assert(false);  // doing this so that we revisit what to do
-                  // here. Currently not being used.
-
-  // d_result = SAT_VALUE_UNKNOWN;
-  // d_assertions.reserve(assertions.size());
-  // for(unsigned i = 0; i < assertions.size(); ++i)
-  //   d_assertions.push_back(assertions[i]);
-}
-
-void DecisionEngine::addAssertions(const vector<Node> &assertions,
-                                   unsigned assertionsEnd,
-                                   IteSkolemMap iteSkolemMap)
+void DecisionEngine::addAssertions(
+    const preprocessing::AssertionPipeline& assertions)
 {
   // new assertions, reset whatever result we knew
   d_result = SAT_VALUE_UNKNOWN;
 
-  // d_assertions.reserve(assertions.size());
-  for(unsigned i = 0; i < assertions.size(); ++i)
-    d_assertions.push_back(assertions[i]);
+  for (const Node& assertion : assertions)
+  {
+    d_assertions.push_back(assertion);
+  }
 
   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
-    d_needIteSkolemMap[i]->
-      addAssertions(assertions, assertionsEnd, iteSkolemMap);
+  {
+    d_needIteSkolemMap[i]->addAssertions(assertions);
+  }
 }
 
 }/* CVC4 namespace */
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 838e53b5a..c5325bc9a 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -24,11 +24,12 @@
 #include "base/output.h"
 #include "decision/decision_strategy.h"
 #include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "prop/sat_solver_types.h"
-#include "smt/term_formula_removal.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/term_formula_removal.h"
 
 using namespace std;
 using namespace CVC4::prop;
@@ -173,21 +174,10 @@ public:
   /*   return d_needIteSkolemMap.size() > 0; */
   /* } */
 
-  /* add a set of assertions */
-  void addAssertions(const vector<Node> &assertions);
-
   /**
-   * add a set of assertions, while providing a mapping between skolem
-   * variables and corresponding assertions. It is assumed that all
-   * assertions after assertionEnd were generated by ite
-   * removal. Hence, iteSkolemMap maps into only these.
+   * Add a list of assertions from an AssertionPipeline.
    */
-  void addAssertions(const vector<Node> &assertions,
-                     unsigned assertionsEnd,
-                     IteSkolemMap iteSkolemMap);
-
-  /* add a single assertion */
-  void addAssertion(Node n);
+  void addAssertions(const preprocessing::AssertionPipeline& assertions);
 
   // Interface for Strategies to use stuff stored in Decision Engine
   // (which was possibly requested by them on initialization)
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 {
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 7d19d3363..b4fbe1cbd 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -163,12 +163,10 @@ inline void computeXorIffDesiredValues
   }
 }
 
-
-
-void JustificationHeuristic::addAssertions
-(const std::vector<Node> &assertions,
- unsigned assertionsEnd,
- IteSkolemMap iteSkolemMap) {
+void JustificationHeuristic::addAssertions(
+    const preprocessing::AssertionPipeline &assertions)
+{
+  size_t assertionsEnd = assertions.getRealAssertionsEnd();
 
   Trace("decision")
     << "JustificationHeuristic::addAssertions()"
@@ -177,19 +175,19 @@ void JustificationHeuristic::addAssertions
     << std::endl;
 
   // Save the 'real' assertions locally
-  for(unsigned i = 0; i < assertionsEnd; ++i)
+  for (size_t i = 0; i < assertionsEnd; i++)
+  {
     d_assertions.push_back(assertions[i]);
+  }
 
   // Save mapping between ite skolems and ite assertions
-  for(IteSkolemMap::iterator i = iteSkolemMap.begin();
-      i != iteSkolemMap.end(); ++i) {
-
-    Trace("decision::jh::ite")
-      << " jh-ite: " << (i->first) << " maps to "
-      << assertions[(i->second)] << std::endl;
-    Assert(i->second >= assertionsEnd && i->second < assertions.size());
+  for (const std::pair<const Node, unsigned> &i : assertions.getIteSkolemMap())
+  {
+    Trace("decision::jh::ite") << " jh-ite: " << (i.first) << " maps to "
+                               << assertions[(i.second)] << std::endl;
+    Assert(i.second >= assertionsEnd && i.second < assertions.size());
 
-    d_iteAssertions[i->first] = assertions[i->second];
+    d_iteAssertions[i.first] = assertions[i.second];
   }
 
   // Automatic weight computation
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index a70bee02c..0cd45ada7 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -32,6 +32,7 @@
 #include "decision/decision_engine.h"
 #include "decision/decision_strategy.h"
 #include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "prop/sat_solver_types.h"
 
 namespace CVC4 {
@@ -119,9 +120,8 @@ public:
 
   prop::SatLiteral getNext(bool &stopSearch) override;
 
-  void addAssertions(const std::vector<Node> &assertions,
-                     unsigned assertionsEnd,
-                     IteSkolemMap iteSkolemMap) override;
+  void addAssertions(
+      const preprocessing::AssertionPipeline &assertions) override;
 
  private:
   /* getNext with an option to specify threshold */