(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.

diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
index 6ca430ac407680c05dd366d64cfb3c265b7b52f1..5c50903c5bae39b61cd4d8cf549ed753af0545e2 100644 (file)
--- a/src/preprocessing/assertion_pipeline.h
+++ b/src/preprocessing/assertion_pipeline.h
@@ -49,9 +49,6 @@ class AssertionPipeline
    */
   void clear();
 
-  /** TODO (projects #75): remove this */
-  Node& operator[](size_t i) { return d_nodes[i]; }
-  /** Get the assertion at index i */
   const Node& operator[](size_t i) const { return d_nodes[i]; }
 
   /**
@@ -72,9 +69,6 @@ class AssertionPipeline
   /** Same as above, with TrustNode */
   void pushBackTrusted(theory::TrustNode trn);
 
-  /** TODO (projects #75): remove this */
-  std::vector<Node>& ref() { return d_nodes; }
-
   /**
    * Get the constant reference to the underlying assertions. It is only
    * possible to modify these via the replace methods below.
@@ -134,7 +128,7 @@ class AssertionPipeline
    * @param n The substitution node
    * @param pg The proof generator that can provide a proof of n.
    */
-  void addSubstitutionNode(Node n, ProofGenerator* pgen = nullptr);
+  void addSubstitutionNode(Node n, ProofGenerator* pg = nullptr);
 
   /**
    * Conjoin n to the assertion vector at position i. This replaces

diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index a7b33ae2627958c7d2d6c0b8332ac902fb9a0b27..af6cae7966b10a539afd771880af4bff567b53ef 100644 (file)
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -276,9 +276,13 @@ void usortsToBitVectors(const LogicInfo& d_logic,
     for (size_t i = 0, size = assertions->size(); i < size; ++i)
     {
       Node old = (*assertions)[i];
-      assertions->replace(i, usVarsToBVVars.apply((*assertions)[i]));
-      Trace("uninterpretedSorts-to-bv")
-          << "  " << old << " => " << (*assertions)[i] << "\n";
+      Node newA = usVarsToBVVars.apply((*assertions)[i]);
+      if (newA != old)
+      {
+        assertions->replace(i, newA);
+        Trace("uninterpretedSorts-to-bv")
+            << "  " << old << " => " << (*assertions)[i] << "\n";
+      }
     }
   }
 }

diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp
index 05fee230e84719dd3b7df3c78e9047c01501bbf3..eaba90561af4eb9a5f5859644c4bedcc47ea65de 100644 (file)
--- a/src/preprocessing/passes/bv_gauss.cpp
+++ b/src/preprocessing/passes/bv_gauss.cpp
@@ -737,8 +737,8 @@ PreprocessingPassResult BVGauss::applyInternal(
   }
 
   std::unordered_map<Node, Node, NodeHashFunction> subst;
-  std::vector<Node>& atpp = assertionsToPreprocess->ref();
 
+  NodeManager* nm = NodeManager::currentNM();
   for (const auto& eq : equations)
   {
     if (eq.second.size() <= 1) { continue; }
@@ -756,11 +756,12 @@ PreprocessingPassResult BVGauss::applyInternal(
                            << std::endl;
     if (ret != BVGauss::Result::INVALID)
     {
-      NodeManager *nm = NodeManager::currentNM();
       if (ret == BVGauss::Result::NONE)
       {
-        atpp.clear();
-        atpp.push_back(nm->mkConst<bool>(false));
+        assertionsToPreprocess->clear();
+        Node n = nm->mkConst<bool>(false);
+        assertionsToPreprocess->push_back(n);
+        return PreprocessingPassResult::CONFLICT;
       }
       else
       {
@@ -773,7 +774,8 @@ PreprocessingPassResult BVGauss::applyInternal(
         {
           Node a = nm->mkNode(kind::EQUAL, p.first, p.second);
           Trace("bv-gauss-elim") << "added assertion: " << a << std::endl;
-          atpp.push_back(a);
+          // add new assertion
+          assertionsToPreprocess->push_back(a);
         }
       }
     }
@@ -782,9 +784,13 @@ PreprocessingPassResult BVGauss::applyInternal(
   if (!subst.empty())
   {
     /* delete (= substitute with true) obsolete assertions */
-    for (auto& a : atpp)
+    const std::vector<Node>& aref = assertionsToPreprocess->ref();
+    for (size_t i = 0, asize = aref.size(); i < asize; ++i)
     {
-      a = a.substitute(subst.begin(), subst.end());
+      Node a = aref[i];
+      Node as = a.substitute(subst.begin(), subst.end());
+      // replace the assertion
+      assertionsToPreprocess->replace(i, as);
     }
   }
   return PreprocessingPassResult::NO_CONFLICT;

diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp
index 5d29add3cc9e7436c66c45cb82030fe964e95e71..00ca1efd3a22da79492c447eb7acb20d336c9d88 100644 (file)
--- a/src/preprocessing/passes/global_negate.cpp
+++ b/src/preprocessing/passes/global_negate.cpp
@@ -27,7 +27,8 @@ namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
-Node GlobalNegate::simplify(std::vector<Node>& assertions, NodeManager* nm)
+Node GlobalNegate::simplify(const std::vector<Node>& assertions,
+                            NodeManager* nm)
 {
   Assert(!assertions.empty());
   Trace("cegqi-gn") << "Global negate : " << std::endl;

diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h
index 853e5a4dd59ec6ec4e0b20921fb191f4f7000bf9..208b8d990e2438b5e0135e5b09f48606dcb35815 100644 (file)
--- a/src/preprocessing/passes/global_negate.h
+++ b/src/preprocessing/passes/global_negate.h
@@ -42,7 +42,7 @@ class GlobalNegate : public PreprocessingPass
       AssertionPipeline* assertionsToPreprocess) override;
 
  private:
-  Node simplify(std::vector<Node>& assertions, NodeManager* nm);
+  Node simplify(const std::vector<Node>& assertions, NodeManager* nm);
 };
 
 }  // namespace passes

diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp
index 2b8b6f3bd6913e4443d5de426cc5c608b0eaed3a..34645b44129306765814d4bfe3cd30aec39e1cb9 100644 (file)
--- a/src/preprocessing/passes/ho_elim.cpp
+++ b/src/preprocessing/passes/ho_elim.cpp
@@ -353,12 +353,10 @@ PreprocessingPassResult HoElim::applyInternal(
   // add lambda lifting axioms as a conjunction to the first assertion
   if (!axioms.empty())
   {
-    Node orig = (*assertionsToPreprocess)[0];
-    axioms.push_back(orig);
-    Node conj = nm->mkNode(AND, axioms);
+    Node conj = nm->mkAnd(axioms);
     conj = theory::Rewriter::rewrite(conj);
     Assert(!expr::hasFreeVar(conj));
-    assertionsToPreprocess->replace(0, conj);
+    assertionsToPreprocess->conjoin(0, conj);
   }
   axioms.clear();
 
@@ -450,12 +448,10 @@ PreprocessingPassResult HoElim::applyInternal(
   // add new axioms as a conjunction to the first assertion
   if (!axioms.empty())
   {
-    Node orig = (*assertionsToPreprocess)[0];
-    axioms.push_back(orig);
-    Node conj = nm->mkNode(AND, axioms);
+    Node conj = nm->mkAnd(axioms);
     conj = theory::Rewriter::rewrite(conj);
     Assert(!expr::hasFreeVar(conj));
-    assertionsToPreprocess->replace(0, conj);
+    assertionsToPreprocess->conjoin(0, conj);
   }
 
   return PreprocessingPassResult::NO_CONFLICT;

diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 11ad273641446bafde78a6f4930c14b556a03f22..a75b6f5ad8de9f909f4084b2e5f0e248fcdd74ec 100644 (file)
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -43,12 +43,12 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
     TrustNode trn = d_preprocContext->getIteRemover()->run(
         (*assertions)[i], newAsserts, newSkolems, true);
     // process
-    assertions->replace(i, trn.getNode());
+    assertions->replaceTrusted(i, trn);
     Assert(newSkolems.size() == newAsserts.size());
     for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
     {
       imap[newSkolems[j]] = assertions->size();
-      assertions->ref().push_back(newAsserts[j].getNode());
+      assertions->pushBackTrusted(newAsserts[j]);
     }
   }
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)

diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 49a6fe603d2bf9208d8dd10578cbd312466296f5..8c99493ba2c4614dc6d9cd6f163f7f5136e1d077 100644 (file)
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -127,7 +127,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
   {
     if (options::compressItes())
     {
-      result = d_iteUtilities.compress(assertionsToPreprocess->ref());
+      result = d_iteUtilities.compress(assertionsToPreprocess);
     }
 
     if (result)
@@ -175,7 +175,8 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
           {
             Node more = aiteu.reduceConstantIteByGCD(res);
             Debug("arith::ite::red") << "  gcd->" << more << endl;
-            (*assertionsToPreprocess)[i] = Rewriter::rewrite(more);
+            Node morer = Rewriter::rewrite(more);
+            assertionsToPreprocess->replace(i, morer);
           }
         }
       }
@@ -214,7 +215,8 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
                                      << "   ->" << res << endl;
             Node more = aiteu.reduceConstantIteByGCD(res);
             Debug("arith::ite::red") << "  gcd->" << more << endl;
-            (*assertionsToPreprocess)[i] = Rewriter::rewrite(more);
+            Node morer = Rewriter::rewrite(more);
+            assertionsToPreprocess->replace(i, morer);
           }
         }
       }

diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp
index e4d79d6148fb3c17a6aea11013f25e0ccf033cb4..88bdf2e5c0e4544b92b777491abf6b9999a2356a 100644 (file)
--- a/src/preprocessing/passes/nl_ext_purify.cpp
+++ b/src/preprocessing/passes/nl_ext_purify.cpp
@@ -117,16 +117,19 @@ PreprocessingPassResult NlExtPurify::applyInternal(
   for (unsigned i = 0; i < size; ++i)
   {
     Node a = (*assertionsToPreprocess)[i];
-    assertionsToPreprocess->replace(i, purifyNlTerms(a, cache, bcache, var_eq));
-    Trace("nl-ext-purify") << "Purify : " << a << " -> "
-                           << (*assertionsToPreprocess)[i] << "\n";
+    Node ap = purifyNlTerms(a, cache, bcache, var_eq);
+    if (a != ap)
+    {
+      assertionsToPreprocess->replace(i, ap);
+      Trace("nl-ext-purify")
+          << "Purify : " << a << " -> " << (*assertionsToPreprocess)[i] << "\n";
+    }
   }
   if (!var_eq.empty())
   {
     unsigned lastIndex = size - 1;
-    var_eq.insert(var_eq.begin(), (*assertionsToPreprocess)[lastIndex]);
-    assertionsToPreprocess->replace(
-        lastIndex, NodeManager::currentNM()->mkNode(kind::AND, var_eq));
+    Node veq = NodeManager::currentNM()->mkAnd(var_eq);
+    assertionsToPreprocess->conjoin(lastIndex, veq);
   }
   return PreprocessingPassResult::NO_CONFLICT;
 }

diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 2ca9f783f835d7fe80e956b20554d5b119dfcad2..fcb6dd171cbfa4a127ecb6b78b2a5a7288eb9e4b 100644 (file)
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -375,11 +375,9 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
     }
   }
 
-  NodeBuilder<> learnedBuilder(kind::AND);
   Assert(assertionsToPreprocess->getRealAssertionsEnd()
          <= assertionsToPreprocess->size());
-  learnedBuilder << (*assertionsToPreprocess)
-          [assertionsToPreprocess->getRealAssertionsEnd() - 1];
+  std::vector<Node> learnedLitsToConjoin;
 
   for (size_t i = 0; i < learned_literals.size(); ++i)
   {
@@ -406,7 +404,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
       continue;
     }
     s.insert(learned);
-    learnedBuilder << learned;
+    learnedLitsToConjoin.push_back(learned);
     Trace("non-clausal-simplify")
         << "non-clausal learned : " << learned << std::endl;
   }
@@ -428,7 +426,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
       continue;
     }
     s.insert(cProp);
-    learnedBuilder << cProp;
+    learnedLitsToConjoin.push_back(cProp);
     Trace("non-clausal-simplify")
         << "non-clausal constant propagation : " << cProp << std::endl;
   }
@@ -439,11 +437,11 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   // substituting
   top_level_substs.addSubstitutions(newSubstitutions);
 
-  if (learnedBuilder.getNumChildren() > 1)
+  if (!learnedLitsToConjoin.empty())
   {
-    assertionsToPreprocess->replace(
-        assertionsToPreprocess->getRealAssertionsEnd() - 1,
-        Rewriter::rewrite(Node(learnedBuilder)));
+    size_t replIndex = assertionsToPreprocess->getRealAssertionsEnd() - 1;
+    Node newConj = NodeManager::currentNM()->mkAnd(learnedLitsToConjoin);
+    assertionsToPreprocess->conjoin(replIndex, newConj);
   }
 
   propagator->setNeedsFinish(true);

diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 7713dbc1b599a590441f14573aa0f5c82c8c6e42..8fea4cbac119864fded8c1fda9d99b3e3ebeffd6 100644 (file)
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -49,7 +49,7 @@ PreprocessingPassResult QuantifierMacros::applyInternal(
   bool success;
   do
   {
-    success = simplify(assertionsToPreprocess->ref(), true);
+    success = simplify(assertionsToPreprocess, true);
   } while (success);
   finalizeDefinitions();
   clearMaps();
@@ -67,7 +67,9 @@ void QuantifierMacros::clearMaps()
   d_ground_macros = false;
 }
 
-bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
+bool QuantifierMacros::simplify(AssertionPipeline* ap, bool doRewrite)
+{
+  const std::vector<Node>& assertions = ap->ref();
   unsigned rmax =
       options::macrosQuantMode() == options::MacrosQuantMode::ALL ? 2 : 1;
   for( unsigned r=0; r<rmax; r++ ){
@@ -116,7 +118,7 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite
               }
             }
           }
-          assertions[i] = curr;
+          ap->replace(i, curr);
           retVal = true;
         }
       }

diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h
index 59a4bee2d103b8df04de13089c5ab02fb6331e3f..c5e557a9e0e37792abe40e80cd0c56ae8fe0759d 100644 (file)
--- a/src/preprocessing/passes/quantifier_macros.h
+++ b/src/preprocessing/passes/quantifier_macros.h
@@ -64,7 +64,17 @@ class QuantifierMacros : public PreprocessingPass
                        bool reqComplete);
   void addMacro(Node op, Node n, std::vector<Node>& opc);
   void debugMacroDefinition(Node oo, Node n);
-  bool simplify(std::vector<Node>& assertions, bool doRewrite = false);
+  /**
+   * This applies macro elimination to the given pipeline, which discovers
+   * whether there are any quantified formulas corresponding to macros.
+   *
+   * @param ap The pipeline to apply macros to.
+   * @param doRewrite Whether we also wish to rewrite the assertions based on
+   * the discovered macro definitions.
+   * @return Whether new definitions were inferred and we rewrote the assertions
+   * based on them.
+   */
+  bool simplify(AssertionPipeline* ap, bool doRewrite = false);
   Node simplify(Node n);
   void finalizeDefinitions();
   void clearMaps();

diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 0b27d0c17e123e25c101d6be8ce4c4c97b564691..cdacd740aabac4bc867bfb74ac8fa24a79c34b2b 100644 (file)
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -80,7 +80,7 @@ PreprocessingPassResult SygusInference::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-bool SygusInference::solveSygus(std::vector<Node>& assertions,
+bool SygusInference::solveSygus(const std::vector<Node>& assertions,
                                 std::vector<Node>& funs,
                                 std::vector<Node>& sols)
 {

diff --git a/src/preprocessing/passes/sygus_inference.h b/src/preprocessing/passes/sygus_inference.h
index 02965c8edb6f3b8a68d8f3095ed7cd89a900ce7f..31d94efd2a678df902eba1d9b772e745091156eb 100644 (file)
--- a/src/preprocessing/passes/sygus_inference.h
+++ b/src/preprocessing/passes/sygus_inference.h
@@ -59,7 +59,7 @@ class SygusInference : public PreprocessingPass
    * If this function returns true, then we add all uninterpreted symbols s in
    * assertions to funs and their corresponding solution to sols.
    */
-  bool solveSygus(std::vector<Node>& assertions,
+  bool solveSygus(const std::vector<Node>& assertions,
                   std::vector<Node>& funs,
                   std::vector<Node>& sols);
 };

diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index 2ca11eb81902838ddb259ec825ab7a90b0970170..8465a63a0fd05267b30ae87769ea866e02eb2f88 100644 (file)
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -40,7 +40,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
 {
   Trace("srs-input") << "Synthesize rewrite rules from assertions..."
                      << std::endl;
-  std::vector<Node>& assertions = assertionsToPreprocess->ref();
+  const std::vector<Node>& assertions = assertionsToPreprocess->ref();
   if (assertions.empty())
   {
     return PreprocessingPassResult::NO_CONFLICT;

diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 64080987b2a4b27655ad96a00f256b453fedc2ad..9b4d02032b301270f739da2a461ccef6bc5c76d1 100644 (file)
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -842,7 +842,7 @@ PreprocessingPassResult UnconstrainedSimplifier::applyInternal(
 {
   d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
 
-  std::vector<Node>& assertions = assertionsToPreprocess->ref();
+  const std::vector<Node>& assertions = assertionsToPreprocess->ref();
 
   d_context->push();
 
@@ -855,9 +855,12 @@ PreprocessingPassResult UnconstrainedSimplifier::applyInternal(
   {
     processUnconstrained();
     //    d_substitutions.print(Message.getStream());
-    for (Node& assertion : assertions)
+    for (size_t i = 0, asize = assertions.size(); i < asize; ++i)
     {
-      assertion = Rewriter::rewrite(d_substitutions.apply(assertion));
+      Node a = assertions[i];
+      Node as = Rewriter::rewrite(d_substitutions.apply(a));
+      // replace the assertion
+      assertionsToPreprocess->replace(i, as);
     }
   }
 

diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp
index c72da162143dd3ca4cdc53b67c450f30083e1072..c9bf283ac490c9a36ab90ed5f6eea2fa12a010ab 100644 (file)
--- a/src/preprocessing/util/ite_utilities.cpp
+++ b/src/preprocessing/util/ite_utilities.cpp
@@ -130,13 +130,13 @@ bool ITEUtilities::simpIteDidALotOfWorkHeuristic() const
 }
 
 /* returns false if an assertion is discovered to be equal to false. */
-bool ITEUtilities::compress(std::vector<Node>& assertions)
+bool ITEUtilities::compress(AssertionPipeline* assertionsToPreprocess)
 {
   if (d_compressor == NULL)
   {
     d_compressor = new ITECompressor(d_containsVisitor.get());
   }
-  return d_compressor->compress(assertions);
+  return d_compressor->compress(assertionsToPreprocess);
 }
 
 Node ITEUtilities::simplifyWithCare(TNode e)
@@ -527,17 +527,18 @@ Node ITECompressor::compressBoolean(Node toCompress)
   }
 }
 
-bool ITECompressor::compress(std::vector<Node>& assertions)
+bool ITECompressor::compress(AssertionPipeline* assertionsToPreprocess)
 {
   reset();
 
-  d_assertions = &assertions;
-  d_incoming.computeReachability(assertions);
+  d_assertions = assertionsToPreprocess;
+  d_incoming.computeReachability(assertionsToPreprocess->ref());
 
   ++(d_statistics.d_compressCalls);
   Chat() << "Computed reachability" << endl;
 
   bool nofalses = true;
+  const std::vector<Node>& assertions = assertionsToPreprocess->ref();
   size_t original_size = assertions.size();
   Chat() << "compressing " << original_size << endl;
   for (size_t i = 0; i < original_size && nofalses; ++i)
@@ -545,7 +546,8 @@ bool ITECompressor::compress(std::vector<Node>& assertions)
     Node assertion = assertions[i];
     Node compressed = compressBoolean(assertion);
     Node rewritten = theory::Rewriter::rewrite(compressed);
-    assertions[i] = rewritten;
+    // replace
+    assertionsToPreprocess->replace(i, rewritten);
     Assert(!d_contains->containsTermITE(rewritten));
 
     nofalses = (rewritten != d_false);

diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h
index fbddf71690fbf60afdd60da2b41b1e3f902174de..c82bf7958d46cf81135ead6d81cc983b5be13598 100644 (file)
--- 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;

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 504814e07bda06fe985c4934ad707bfec47bacfe..971288b67513c70a8b2ba4c8a3e3f22d1e8df68b 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -339,8 +339,7 @@ bool ProcessAssertions::apply(Assertions& as)
       // assertion
       IteSkolemMap::iterator it = iskMap.begin();
       IteSkolemMap::iterator iend = iskMap.end();
-      NodeBuilder<> builder(AND);
-      builder << assertions[assertions.getRealAssertionsEnd() - 1];
+      std::vector<Node> newConj;
       vector<TNode> toErase;
       for (; it != iend; ++it)
       {
@@ -367,19 +366,20 @@ bool ProcessAssertions::apply(Assertions& as)
           }
         }
         // Move this iteExpr into the main assertions
-        builder << assertions[(*it).second];
-        assertions[(*it).second] = d_true;
+        newConj.push_back(assertions[(*it).second]);
+        assertions.replace((*it).second, d_true);
         toErase.push_back((*it).first);
       }
-      if (builder.getNumChildren() > 1)
+      if (!newConj.empty())
       {
         while (!toErase.empty())
         {
           iskMap.erase(toErase.back());
           toErase.pop_back();
         }
-        assertions[assertions.getRealAssertionsEnd() - 1] =
-            Rewriter::rewrite(Node(builder));
+        size_t index = assertions.getRealAssertionsEnd() - 1;
+        Node newAssertion = NodeManager::currentNM()->mkAnd(newConj);
+        assertions.conjoin(index, newAssertion);
       }
       // TODO(b/1256): For some reason this is needed for some benchmarks, such
       // as