Move d_realAssertionsEnd from SmtEnginePrivate to AssertionPipeline. (#2350)

diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index 97b05802da113fb7138ad87e96a6e308a629977b..6a7078696e27d6b4079e242aa5c852c569306ad1 100644 (file)
--- a/src/preprocessing/preprocessing_pass.cpp
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -25,7 +25,9 @@ namespace CVC4 {
 namespace preprocessing {
 
 AssertionPipeline::AssertionPipeline(context::Context* context)
-    : d_substitutionsIndex(context, 0), d_topLevelSubstitutions(context)
+    : d_substitutionsIndex(context, 0),
+      d_topLevelSubstitutions(context),
+      d_realAssertionsEnd(0)
 {
 }
 

diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
index 6f76b60e9b7269a97c13ae431f8ca94e386b2c1b..97fa32d1759129cdc701c60d12a8b2c763cf0c78 100644 (file)
--- a/src/preprocessing/preprocessing_pass.h
+++ b/src/preprocessing/preprocessing_pass.h
@@ -56,7 +56,12 @@ class AssertionPipeline
   size_t size() const { return d_nodes.size(); }
 
   void resize(size_t n) { d_nodes.resize(n); }
-  void clear() { d_nodes.clear(); }
+
+  void clear()
+  {
+    d_nodes.clear();
+    d_realAssertionsEnd = 0;
+  }
 
   Node& operator[](size_t i) { return d_nodes[i]; }
   const Node& operator[](size_t i) const { return d_nodes[i]; }
@@ -99,6 +104,10 @@ class AssertionPipeline
     return d_topLevelSubstitutions;
   }
 
+  size_t getRealAssertionsEnd() { return d_realAssertionsEnd; }
+
+  void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); }
+
  private:
   std::vector<Node> d_nodes;
 
@@ -107,12 +116,15 @@ class AssertionPipeline
    * corresponding introduced Boolean ite
    */
   IteSkolemMap d_iteSkolemMap;
-  
+
   /* Index for where to store substitutions */
   context::CDO<unsigned> d_substitutionsIndex;
 
   /* The top level substitutions */
   theory::SubstitutionMap d_topLevelSubstitutions;
+
+  /** Size of d_nodes when preprocessing starts */
+  size_t d_realAssertionsEnd;
 }; /* class AssertionPipeline */
 
 /**

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index cabe825be87a1a2647c4055bbe96fcf7f1d79d3b..fbe6bcd63fea34a4a009b466c78bcecde48b4f92 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -502,9 +502,6 @@ class SmtEnginePrivate : public NodeManagerListener {
   /** Learned literals */
   vector<Node> d_nonClausalLearnedLiterals;
 
-  /** Size of assertions array when preprocessing starts */
-  unsigned d_realAssertionsEnd;
-
   /** A circuit propagator for non-clausal propositional deduction */
   booleans::CircuitPropagator d_propagator;
   bool d_propagatorNeedsFinish;
@@ -640,7 +637,6 @@ class SmtEnginePrivate : public NodeManagerListener {
         d_managedReplayLog(),
         d_listenerRegistrations(new ListenerRegistrationList()),
         d_nonClausalLearnedLiterals(),
-        d_realAssertionsEnd(0),
         d_propagator(d_nonClausalLearnedLiterals, true, true),
         d_propagatorNeedsFinish(false),
         d_assertions(d_smt.d_userContext),
@@ -815,7 +811,6 @@ class SmtEnginePrivate : public NodeManagerListener {
   void notifyPop() {
     d_assertions.clear();
     d_nonClausalLearnedLiterals.clear();
-    d_realAssertionsEnd = 0;
     getIteSkolemMap().clear();
   }
 
@@ -3260,8 +3255,8 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   }
 
   NodeBuilder<> learnedBuilder(kind::AND);
-  Assert(d_realAssertionsEnd <= d_assertions.size());
-  learnedBuilder << d_assertions[d_realAssertionsEnd - 1];
+  Assert(d_assertions.getRealAssertionsEnd() <= d_assertions.size());
+  learnedBuilder << d_assertions[d_assertions.getRealAssertionsEnd() - 1];
 
   for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) {
     Node learned = d_nonClausalLearnedLiterals[i];
@@ -3314,8 +3309,8 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   top_level_substs.addSubstitutions(newSubstitutions);
 
   if(learnedBuilder.getNumChildren() > 1) {
-    d_assertions.replace(d_realAssertionsEnd - 1,
-      Rewriter::rewrite(Node(learnedBuilder)));
+    d_assertions.replace(d_assertions.getRealAssertionsEnd() - 1,
+                         Rewriter::rewrite(Node(learnedBuilder)));
   }
 
   d_propagatorNeedsFinish = true;
@@ -3347,21 +3342,21 @@ bool SmtEnginePrivate::simpITE() {
 
 void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){
   size_t curr = d_assertions.size();
-  if(before >= curr ||
-     d_realAssertionsEnd <= 0 ||
-     d_realAssertionsEnd >= curr){
+  if (before >= curr || d_assertions.getRealAssertionsEnd() <= 0
+      || d_assertions.getRealAssertionsEnd() >= curr)
+  {
     return;
   }
 
   // assertions
-  // original: [0 ... d_realAssertionsEnd)
+  // original: [0 ... d_assertions.getRealAssertionsEnd())
   //  can be modified
-  // ites skolems [d_realAssertionsEnd, before)
+  // ites skolems [d_assertions.getRealAssertionsEnd(), before)
   //  cannot be moved
   // added [before, curr)
   //  can be modified
-  Assert(0 < d_realAssertionsEnd);
-  Assert(d_realAssertionsEnd <= before);
+  Assert(0 < d_assertions.getRealAssertionsEnd());
+  Assert(d_assertions.getRealAssertionsEnd() <= before);
   Assert(before < curr);
 
   std::vector<Node> intoConjunction;
@@ -3369,7 +3364,7 @@ void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){
     intoConjunction.push_back(d_assertions[i]);
   }
   d_assertions.resize(before);
-  size_t lastBeforeItes = d_realAssertionsEnd - 1;
+  size_t lastBeforeItes = d_assertions.getRealAssertionsEnd() - 1;
   intoConjunction.push_back(d_assertions[lastBeforeItes]);
   Node newLast = util::NaryBuilder::mkAssoc(kind::AND, intoConjunction);
   d_assertions.replace(lastBeforeItes, newLast);
@@ -3448,7 +3443,7 @@ size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::unordered_set
 }
 
 void SmtEnginePrivate::doMiplibTrick() {
-  Assert(d_realAssertionsEnd == d_assertions.size());
+  Assert(d_assertions.getRealAssertionsEnd() == d_assertions.size());
   Assert(!options::incrementalSolving());
 
   const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges();
@@ -3746,7 +3741,8 @@ void SmtEnginePrivate::doMiplibTrick() {
   }
   if(!removeAssertions.empty()) {
     Debug("miplib") << "SmtEnginePrivate::simplify(): scrubbing miplib encoding..." << endl;
-    for(size_t i = 0; i < d_realAssertionsEnd; ++i) {
+    for (size_t i = 0; i < d_assertions.getRealAssertionsEnd(); ++i)
+    {
       if(removeAssertions.find(d_assertions[i].getId()) != removeAssertions.end()) {
         Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertions[i] << endl;
         d_assertions[i] = d_true;
@@ -3767,7 +3763,7 @@ void SmtEnginePrivate::doMiplibTrick() {
   } else {
     Debug("miplib") << "SmtEnginePrivate::simplify(): miplib pass found nothing." << endl;
   }
-  d_realAssertionsEnd = d_assertions.size();
+  d_assertions.updateRealAssertionsEnd();
 }
 
 
@@ -3795,16 +3791,17 @@ bool SmtEnginePrivate::simplifyAssertions()
 
       // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
       // do the miplib trick.
-      if( // check that option is on
+      if (  // check that option is on
           options::arithMLTrick() &&
           // miplib rewrites aren't safe in incremental mode
-          ! options::incrementalSolving() &&
+          !options::incrementalSolving() &&
           // only useful in arith
           d_smt.d_logic.isTheoryEnabled(THEORY_ARITH) &&
           // we add new assertions and need this (in practice, this
           // restriction only disables miplib processing during
           // re-simplification, which we don't expect to be useful anyway)
-          d_realAssertionsEnd == d_assertions.size() ) {
+          d_assertions.getRealAssertionsEnd() == d_assertions.size())
+      {
         Chat() << "...fixing miplib encodings..." << endl;
         Trace("simplify") << "SmtEnginePrivate::simplify(): "
                           << "looking for miplib pseudobooleans..." << endl;
@@ -4057,7 +4054,7 @@ void SmtEnginePrivate::processAssertions() {
   d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true));
   // any assertions added beyond realAssertionsEnd must NOT affect the
   // equisatisfiability
-  d_realAssertionsEnd = d_assertions.size();
+  d_assertions.updateRealAssertionsEnd();
 
   // Assertions are NOT guaranteed to be rewritten by this point
 
@@ -4337,7 +4334,7 @@ void SmtEnginePrivate::processAssertions() {
       IteSkolemMap::iterator it = getIteSkolemMap().begin();
       IteSkolemMap::iterator iend = getIteSkolemMap().end();
       NodeBuilder<> builder(kind::AND);
-      builder << d_assertions[d_realAssertionsEnd - 1];
+      builder << d_assertions[d_assertions.getRealAssertionsEnd() - 1];
       vector<TNode> toErase;
       for (; it != iend; ++it) {
         if (skolemSet.find((*it).first) == skolemSet.end()) {
@@ -4366,7 +4363,8 @@ void SmtEnginePrivate::processAssertions() {
           getIteSkolemMap().erase(toErase.back());
           toErase.pop_back();
         }
-        d_assertions[d_realAssertionsEnd - 1] = Rewriter::rewrite(Node(builder));
+        d_assertions[d_assertions.getRealAssertionsEnd() - 1] =
+            Rewriter::rewrite(Node(builder));
       }
       // TODO(b/1256): For some reason this is needed for some benchmarks, such as
       // QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
@@ -4420,8 +4418,9 @@ void SmtEnginePrivate::processAssertions() {
   if(noConflict) {
     Chat() << "pushing to decision engine..." << endl;
     Assert(iteRewriteAssertionsEnd == d_assertions.size());
-    d_smt.d_decisionEngine->addAssertions(
-        d_assertions.ref(), d_realAssertionsEnd, getIteSkolemMap());
+    d_smt.d_decisionEngine->addAssertions(d_assertions.ref(),
+                                          d_assertions.getRealAssertionsEnd(),
+                                          getIteSkolemMap());
   }
 
   // end: INVARIANT to maintain: no reordering of assertions or