Use skolem lemma in prop layer interfaces (#7320)

diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index 97e56c58cf9ca12868955705419e93b4d19878ae..c7ec46337f077b69a3168e5ac5c72585737ef479 100644 (file)
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -47,19 +47,17 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)
   {
     Node assertion = (*assertions)[i];
-    std::vector<TrustNode> newAsserts;
-    std::vector<Node> newSkolems;
-    TrustNode trn = pe->removeItes(assertion, newAsserts, newSkolems);
+    std::vector<SkolemLemma> newAsserts;
+    TrustNode trn = pe->removeItes(assertion, newAsserts);
     if (!trn.isNull())
     {
       // process
       assertions->replaceTrusted(i, trn);
     }
-    Assert(newSkolems.size() == newAsserts.size());
-    for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
+    for (const SkolemLemma& lem : newAsserts)
     {
-      imap[assertions->size()] = newSkolems[j];
-      assertions->pushBackTrusted(newAsserts[j]);
+      imap[assertions->size()] = lem.d_skolem;
+      assertions->pushBackTrusted(lem.d_lemma);
     }
   }
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)

diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index 641cab162def444db1915fafd12c00d37918798d..2f9d126378f7e7751f4c9c40afed6e176db4260c 100644 (file)
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -44,19 +44,17 @@ PreprocessingPassResult TheoryPreprocess::applyInternal(
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)
   {
     Node assertion = (*assertions)[i];
-    std::vector<TrustNode> newAsserts;
-    std::vector<Node> newSkolems;
-    TrustNode trn = propEngine->preprocess(assertion, newAsserts, newSkolems);
+    std::vector<SkolemLemma> newAsserts;
+    TrustNode trn = propEngine->preprocess(assertion, newAsserts);
     if (!trn.isNull())
     {
       // process
       assertions->replaceTrusted(i, trn);
     }
-    Assert(newSkolems.size() == newAsserts.size());
-    for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++)
+    for (const SkolemLemma& lem : newAsserts)
     {
-      imap[assertions->size()] = newSkolems[j];
-      assertions->pushBackTrusted(newAsserts[j]);
+      imap[assertions->size()] = lem.d_skolem;
+      assertions->pushBackTrusted(lem.d_lemma);
     }
   }
 

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 5bd719fe9e01df5c9dfbfee97726c6bd47c054e6..6f8bbe997b9d593fba8d6eb5ba8373215fac482c 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -161,17 +161,15 @@ PropEngine::~PropEngine() {
 }
 
 TrustNode PropEngine::preprocess(TNode node,
-                                 std::vector<TrustNode>& newLemmas,
-                                 std::vector<Node>& newSkolems)
+                                 std::vector<theory::SkolemLemma>& newLemmas)
 {
-  return d_theoryProxy->preprocess(node, newLemmas, newSkolems);
+  return d_theoryProxy->preprocess(node, newLemmas);
 }
 
 TrustNode PropEngine::removeItes(TNode node,
-                                 std::vector<TrustNode>& newLemmas,
-                                 std::vector<Node>& newSkolems)
+                                 std::vector<theory::SkolemLemma>& newLemmas)
 {
-  return d_theoryProxy->removeItes(node, newLemmas, newSkolems);
+  return d_theoryProxy->removeItes(node, newLemmas);
 }
 
 void PropEngine::assertInputFormulas(
@@ -210,12 +208,8 @@ void PropEngine::assertLemma(TrustNode tlemma, theory::LemmaProperty p)
   bool removable = isLemmaPropertyRemovable(p);
 
   // call preprocessor
-  std::vector<TrustNode> ppLemmas;
-  std::vector<Node> ppSkolems;
-  TrustNode tplemma =
-      d_theoryProxy->preprocessLemma(tlemma, ppLemmas, ppSkolems);
-
-  Assert(ppSkolems.size() == ppLemmas.size());
+  std::vector<theory::SkolemLemma> ppLemmas;
+  TrustNode tplemma = d_theoryProxy->preprocessLemma(tlemma, ppLemmas);
 
   // do final checks on the lemmas we are about to send
   if (isProofEnabled()
@@ -224,25 +218,25 @@ void PropEngine::assertLemma(TrustNode tlemma, theory::LemmaProperty p)
     Assert(tplemma.getGenerator() != nullptr);
     // ensure closed, make the proof node eagerly here to debug
     tplemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma");
-    for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
+    for (theory::SkolemLemma& lem : ppLemmas)
     {
-      Assert(ppLemmas[i].getGenerator() != nullptr);
-      ppLemmas[i].debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_new");
+      Assert(lem.d_lemma.getGenerator() != nullptr);
+      lem.d_lemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_new");
     }
   }
 
   if (Trace.isOn("te-lemma"))
   {
     Trace("te-lemma") << "Lemma, output: " << tplemma.getProven() << std::endl;
-    for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
+    for (const theory::SkolemLemma& lem : ppLemmas)
     {
-      Trace("te-lemma") << "Lemma, new lemma: " << ppLemmas[i].getProven()
-                        << " (skolem is " << ppSkolems[i] << ")" << std::endl;
+      Trace("te-lemma") << "Lemma, new lemma: " << lem.d_lemma.getProven()
+                        << " (skolem is " << lem.d_skolem << ")" << std::endl;
     }
   }
 
   // now, assert the lemmas
-  assertLemmasInternal(tplemma, ppLemmas, ppSkolems, removable);
+  assertLemmasInternal(tplemma, ppLemmas, removable);
 }
 
 void PropEngine::assertTrustedLemmaInternal(TrustNode trn, bool removable)
@@ -296,18 +290,18 @@ void PropEngine::assertInternal(
   }
 }
 
-void PropEngine::assertLemmasInternal(TrustNode trn,
-                                      const std::vector<TrustNode>& ppLemmas,
-                                      const std::vector<Node>& ppSkolems,
-                                      bool removable)
+void PropEngine::assertLemmasInternal(
+    TrustNode trn,
+    const std::vector<theory::SkolemLemma>& ppLemmas,
+    bool removable)
 {
   if (!trn.isNull())
   {
     assertTrustedLemmaInternal(trn, removable);
   }
-  for (const TrustNode& tnl : ppLemmas)
+  for (const theory::SkolemLemma& lem : ppLemmas)
   {
-    assertTrustedLemmaInternal(tnl, removable);
+    assertTrustedLemmaInternal(lem.d_lemma, removable);
   }
   // assert to decision engine
   if (!removable)
@@ -318,10 +312,9 @@ void PropEngine::assertLemmasInternal(TrustNode trn,
       // notify the theory proxy of the lemma
       d_theoryProxy->notifyAssertion(trn.getProven());
     }
-    Assert(ppSkolems.size() == ppLemmas.size());
-    for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
+    for (const theory::SkolemLemma& lem : ppLemmas)
     {
-      d_theoryProxy->notifyAssertion(ppLemmas[i].getProven(), ppSkolems[i]);
+      d_theoryProxy->notifyAssertion(lem.getProven(), lem.d_skolem);
     }
   }
 }
@@ -510,12 +503,11 @@ Node PropEngine::ensureLiteral(TNode n)
 Node PropEngine::getPreprocessedTerm(TNode n)
 {
   // must preprocess
-  std::vector<TrustNode> newLemmas;
-  std::vector<Node> newSkolems;
-  TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas, newSkolems);
+  std::vector<theory::SkolemLemma> newLemmas;
+  TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas);
   // send lemmas corresponding to the skolems introduced by preprocessing n
   TrustNode trnNull;
-  assertLemmasInternal(trnNull, newLemmas, newSkolems, false);
+  assertLemmasInternal(trnNull, newLemmas, false);
   return tpn.isNull() ? Node(n) : tpn.getNode();
 }
 

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 3556108d16575d78cf685f6e53fa07b9b6920da4..2f569ba7255f808eda478e38703532637b0dcc35 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -25,6 +25,7 @@
 #include "proof/trust_node.h"
 #include "prop/skolem_def_manager.h"
 #include "theory/output_channel.h"
+#include "theory/skolem_lemma.h"
 #include "util/result.h"
 
 namespace cvc5 {
@@ -85,14 +86,12 @@ class PropEngine
    * ppSkolems respectively.
    *
    * @param node The assertion to preprocess,
-   * @param ppLemmas The lemmas to add to the set of assertions,
-   * @param ppSkolems The skolems that newLemmas correspond to,
+   * @param ppLemmas The lemmas to add to the set of assertions, which tracks
+   * their corresponding skolems,
    * @return The (REWRITE) trust node corresponding to rewritten node via
    * preprocessing.
    */
-  TrustNode preprocess(TNode node,
-                       std::vector<TrustNode>& ppLemmas,
-                       std::vector<Node>& ppSkolems);
+  TrustNode preprocess(TNode node, std::vector<theory::SkolemLemma>& ppLemmas);
   /**
    * Remove term ITEs (and more generally, term formulas) from the given node.
    * Return the REWRITE trust node corresponding to rewriting node. New lemmas
@@ -101,14 +100,12 @@ class PropEngine
    * preprocessing and rewriting.
    *
    * @param node The assertion to preprocess,
-   * @param ppLemmas The lemmas to add to the set of assertions,
-   * @param ppSkolems The skolems that newLemmas correspond to,
+   * @param ppLemmas The lemmas to add to the set of assertions, which tracks
+   * their corresponding skolems.
    * @return The (REWRITE) trust node corresponding to rewritten node via
    * preprocessing.
    */
-  TrustNode removeItes(TNode node,
-                       std::vector<TrustNode>& ppLemmas,
-                       std::vector<Node>& ppSkolems);
+  TrustNode removeItes(TNode node, std::vector<theory::SkolemLemma>& ppLemmas);
 
   /**
    * Converts the given formulas to CNF and assert the CNF to the SAT solver.
@@ -334,13 +331,12 @@ class PropEngine
                       ProofGenerator* pg = nullptr);
   /**
    * Assert lemmas internal, where trn is a trust node corresponding to a
-   * formula to assert to the CNF stream, ppLemmas and ppSkolems are the
-   * skolem definitions and skolems obtained from preprocessing it, and
-   * removable is whether the lemma is removable.
+   * formula to assert to the CNF stream, ppLemmas are the skolem definitions
+   * obtained from preprocessing it, and removable is whether the lemma is
+   * removable.
    */
   void assertLemmasInternal(TrustNode trn,
-                            const std::vector<TrustNode>& ppLemmas,
-                            const std::vector<Node>& ppSkolems,
+                            const std::vector<theory::SkolemLemma>& ppLemmas,
                             bool removable);
 
   /**

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index a4690ff0a7d4ed85ed296b5a719261c4447c0120..254388a496f3e6e791dcaa10b16877268ac01cc9 100644 (file)
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -203,26 +203,23 @@ SatValue TheoryProxy::getDecisionPolarity(SatVariable var) {
 
 CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; }
 
-TrustNode TheoryProxy::preprocessLemma(TrustNode trn,
-                                       std::vector<TrustNode>& newLemmas,
-                                       std::vector<Node>& newSkolems)
+TrustNode TheoryProxy::preprocessLemma(
+    TrustNode trn, std::vector<theory::SkolemLemma>& newLemmas)
 {
-  return d_tpp.preprocessLemma(trn, newLemmas, newSkolems);
+  return d_tpp.preprocessLemma(trn, newLemmas);
 }
 
 TrustNode TheoryProxy::preprocess(TNode node,
-                                  std::vector<TrustNode>& newLemmas,
-                                  std::vector<Node>& newSkolems)
+                                  std::vector<theory::SkolemLemma>& newLemmas)
 {
-  return d_tpp.preprocess(node, newLemmas, newSkolems);
+  return d_tpp.preprocess(node, newLemmas);
 }
 
 TrustNode TheoryProxy::removeItes(TNode node,
-                                  std::vector<TrustNode>& newLemmas,
-                                  std::vector<Node>& newSkolems)
+                                  std::vector<theory::SkolemLemma>& newLemmas)
 {
   RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas();
-  return rtf.run(node, newLemmas, newSkolems, true);
+  return rtf.run(node, newLemmas, true);
 }
 
 void TheoryProxy::getSkolems(TNode node,

diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index a196bd4d40f5684dc13683c9191995ad94c1a413..67d3c06682419ce2dd9dd5b4c46e087834e390f5 100644 (file)
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -109,21 +109,16 @@ class TheoryProxy : public Registrar
    * rewrite.
    */
   TrustNode preprocessLemma(TrustNode trn,
-                            std::vector<TrustNode>& newLemmas,
-                            std::vector<Node>& newSkolems);
+                            std::vector<theory::SkolemLemma>& newLemmas);
   /**
    * Call the preprocessor on node, return trust node corresponding to the
    * rewrite.
    */
-  TrustNode preprocess(TNode node,
-                       std::vector<TrustNode>& newLemmas,
-                       std::vector<Node>& newSkolems);
+  TrustNode preprocess(TNode node, std::vector<theory::SkolemLemma>& newLemmas);
   /**
    * Remove ITEs from the node.
    */
-  TrustNode removeItes(TNode node,
-                       std::vector<TrustNode>& newLemmas,
-                       std::vector<Node>& newSkolems);
+  TrustNode removeItes(TNode node, std::vector<theory::SkolemLemma>& newLemmas);
   /**
    * Get the skolems within node and their corresponding definitions, store
    * them in sks and skAsserts respectively. Note that this method does not

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 6a2f6fbd467e07484aaf576fc2d48e5ff3a68268..470c035a99a989af49fce66d6aacb1c64afa55a9 100644 (file)
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -55,12 +55,10 @@ RemoveTermFormulas::RemoveTermFormulas(Env& env)
 RemoveTermFormulas::~RemoveTermFormulas() {}
 
 TrustNode RemoveTermFormulas::run(TNode assertion,
-                                  std::vector<TrustNode>& newAsserts,
-                                  std::vector<Node>& newSkolems,
+                                  std::vector<theory::SkolemLemma>& newAsserts,
                                   bool fixedPoint)
 {
-  Node itesRemoved = runInternal(assertion, newAsserts, newSkolems);
-  Assert(newAsserts.size() == newSkolems.size());
+  Node itesRemoved = runInternal(assertion, newAsserts);
   if (itesRemoved == assertion)
   {
     return TrustNode::null();
@@ -72,10 +70,10 @@ TrustNode RemoveTermFormulas::run(TNode assertion,
     size_t i = 0;
     while (i < newAsserts.size())
     {
-      TrustNode trn = newAsserts[i];
+      TrustNode trn = newAsserts[i].d_lemma;
       // do not run to fixed point on subcall, since we are processing all
       // lemmas in this loop
-      newAsserts[i] = runLemma(trn, newAsserts, newSkolems, false);
+      newAsserts[i].d_lemma = runLemma(trn, newAsserts, false);
       i++;
     }
   }
@@ -84,19 +82,12 @@ TrustNode RemoveTermFormulas::run(TNode assertion,
   return TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get());
 }
 
-TrustNode RemoveTermFormulas::run(TNode assertion)
+TrustNode RemoveTermFormulas::runLemma(
+    TrustNode lem,
+    std::vector<theory::SkolemLemma>& newAsserts,
+    bool fixedPoint)
 {
-  std::vector<TrustNode> newAsserts;
-  std::vector<Node> newSkolems;
-  return run(assertion, newAsserts, newSkolems, false);
-}
-
-TrustNode RemoveTermFormulas::runLemma(TrustNode lem,
-                                       std::vector<TrustNode>& newAsserts,
-                                       std::vector<Node>& newSkolems,
-                                       bool fixedPoint)
-{
-  TrustNode trn = run(lem.getProven(), newAsserts, newSkolems, fixedPoint);
+  TrustNode trn = run(lem.getProven(), newAsserts, fixedPoint);
   if (trn.isNull())
   {
     // no change
@@ -130,8 +121,7 @@ TrustNode RemoveTermFormulas::runLemma(TrustNode lem,
 }
 
 Node RemoveTermFormulas::runInternal(TNode assertion,
-                                     std::vector<TrustNode>& output,
-                                     std::vector<Node>& newSkolems)
+                                     std::vector<theory::SkolemLemma>& output)
 {
   NodeManager* nm = NodeManager::currentNM();
   TCtxStack ctx(&d_rtfc);
@@ -171,8 +161,7 @@ Node RemoveTermFormulas::runInternal(TNode assertion,
         // which we add to our vectors
         if (!newLem.isNull())
         {
-          output.push_back(newLem);
-          newSkolems.push_back(currt);
+          output.push_back(theory::SkolemLemma(newLem, currt));
         }
         Trace("rtf-debug") << "...replace by skolem" << std::endl;
         d_tfCache.insert(curr, currt);

diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index a47bcfbb058abcfacb215d7f9f7f9dadb4a1a9f0..80cbc3b030481eef2ca80f763b9a33567d918d26 100644 (file)
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -26,6 +26,7 @@
 #include "expr/term_context.h"
 #include "proof/trust_node.h"
 #include "smt/env_obj.h"
+#include "theory/skolem_lemma.h"
 #include "util/hash.h"
 
 namespace cvc5 {
@@ -81,7 +82,6 @@ class RemoveTermFormulas : protected EnvObj
    * @param assertion The assertion to remove term formulas from
    * @param newAsserts The new assertions corresponding to axioms for newly
    * introduced skolems.
-   * @param newSkolems The skolems corresponding to each of the newAsserts.
    * @param fixedPoint Whether to run term formula removal on the lemmas in
    * newAsserts. This adds new assertions to this vector until a fixed
    * point is reached. When this option is true, all lemmas in newAsserts
@@ -91,22 +91,14 @@ class RemoveTermFormulas : protected EnvObj
    * generator (if provided) that can prove the equivalence.
    */
   TrustNode run(TNode assertion,
-                std::vector<TrustNode>& newAsserts,
-                std::vector<Node>& newSkolems,
+                std::vector<theory::SkolemLemma>& newAsserts,
                 bool fixedPoint = false);
-  /**
-   * Same as above, but does not track lemmas, and does not run to fixed point.
-   * The relevant lemmas can be extracted by the caller later using getSkolems
-   * and getLemmaForSkolem.
-   */
-  TrustNode run(TNode assertion);
   /**
    * Same as above, but transforms a lemma, returning a LEMMA trust node that
    * proves the same formula as lem with term formulas removed.
    */
   TrustNode runLemma(TrustNode lem,
-                     std::vector<TrustNode>& newAsserts,
-                     std::vector<Node>& newSkolems,
+                     std::vector<theory::SkolemLemma>& newAsserts,
                      bool fixedPoint = false);
 
   /**
@@ -190,8 +182,7 @@ class RemoveTermFormulas : protected EnvObj
    * the version of assertion with all term formulas removed.
    */
   Node runInternal(TNode assertion,
-                   std::vector<TrustNode>& newAsserts,
-                   std::vector<Node>& newSkolems);
+                   std::vector<theory::SkolemLemma>& newAsserts);
   /**
    * This is called on curr of the form (t, val) where t is a term and val is
    * a term context identifier computed by RtfTermContext. If curr should be

diff --git a/src/theory/skolem_lemma.cpp b/src/theory/skolem_lemma.cpp
index ff1ffdcf9436c714a847b965309c549e555ea405..af4d09492b9805136e622b48cd732fc8d97243e0 100644 (file)
--- a/src/theory/skolem_lemma.cpp
+++ b/src/theory/skolem_lemma.cpp
@@ -31,6 +31,8 @@ SkolemLemma::SkolemLemma(Node k, ProofGenerator* pg) : d_lemma(), d_skolem(k)
   d_lemma = TrustNode::mkTrustLemma(lem, pg);
 }
 
+Node SkolemLemma::getProven() const { return d_lemma.getProven(); }
+
 Node SkolemLemma::getSkolemLemmaFor(Node k)
 {
   Node w = SkolemManager::getWitnessForm(k);

diff --git a/src/theory/skolem_lemma.h b/src/theory/skolem_lemma.h
index 277daf88c06e4bc2324662c9a657e1bb1fbd706c..4f17ed9d3a78a053dd4a75ca09b6edabb96a7b28 100644 (file)
--- a/src/theory/skolem_lemma.h
+++ b/src/theory/skolem_lemma.h
@@ -52,6 +52,8 @@ class SkolemLemma
   /** The skolem associated with that lemma */
   Node d_skolem;
 
+  /** Get proven from the lemma */
+  Node getProven() const;
   /**
    * Get the lemma for skolem k based on its witness form. If k has witness
    * form (witness ((x T)) (P x)), this is the formula (P k).

diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 4b100a12f77a140ab5030aaabcafbbb5d2c13b65..043b0b37c8b7c177ab01be9a22f8df9fd339e507 100644 (file)
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -80,17 +80,13 @@ TheoryPreprocessor::TheoryPreprocessor(Env& env, TheoryEngine& engine)
 TheoryPreprocessor::~TheoryPreprocessor() {}
 
 TrustNode TheoryPreprocessor::preprocess(TNode node,
-                                         std::vector<TrustNode>& newLemmas,
-                                         std::vector<Node>& newSkolems)
+                                         std::vector<SkolemLemma>& newLemmas)
 {
-  return preprocessInternal(node, newLemmas, newSkolems, true);
+  return preprocessInternal(node, newLemmas, true);
 }
 
 TrustNode TheoryPreprocessor::preprocessInternal(
-    TNode node,
-    std::vector<TrustNode>& newLemmas,
-    std::vector<Node>& newSkolems,
-    bool procLemmas)
+    TNode node, std::vector<SkolemLemma>& newLemmas, bool procLemmas)
 {
   // In this method, all rewriting steps of node are stored in d_tpg.
 
@@ -104,7 +100,7 @@ TrustNode TheoryPreprocessor::preprocessInternal(
   Node irNode = rewriteWithProof(node, d_tpgRew.get(), true);
 
   // run theory preprocessing
-  TrustNode tpp = theoryPreprocess(irNode, newLemmas, newSkolems);
+  TrustNode tpp = theoryPreprocess(irNode, newLemmas);
   Node ppNode = tpp.getNode();
 
   if (Trace.isOn("tpp-debug"))
@@ -131,8 +127,8 @@ TrustNode TheoryPreprocessor::preprocessInternal(
     size_t i = 0;
     while (i < newLemmas.size())
     {
-      TrustNode cur = newLemmas[i];
-      newLemmas[i] = preprocessLemmaInternal(cur, newLemmas, newSkolems, false);
+      TrustNode cur = newLemmas[i].d_lemma;
+      newLemmas[i].d_lemma = preprocessLemmaInternal(cur, newLemmas, false);
       Trace("tpp") << "Final lemma : " << newLemmas[i].getProven() << std::endl;
       i++;
     }
@@ -173,23 +169,18 @@ TrustNode TheoryPreprocessor::preprocessInternal(
   return tret;
 }
 
-TrustNode TheoryPreprocessor::preprocessLemma(TrustNode node,
-                                              std::vector<TrustNode>& newLemmas,
-                                              std::vector<Node>& newSkolems)
+TrustNode TheoryPreprocessor::preprocessLemma(
+    TrustNode node, std::vector<SkolemLemma>& newLemmas)
 {
-  return preprocessLemmaInternal(node, newLemmas, newSkolems, true);
+  return preprocessLemmaInternal(node, newLemmas, true);
 }
 
 TrustNode TheoryPreprocessor::preprocessLemmaInternal(
-    TrustNode node,
-    std::vector<TrustNode>& newLemmas,
-    std::vector<Node>& newSkolems,
-    bool procLemmas)
+    TrustNode node, std::vector<SkolemLemma>& newLemmas, bool procLemmas)
 {
   // what was originally proven
   Node lemma = node.getProven();
-  TrustNode tplemma =
-      preprocessInternal(lemma, newLemmas, newSkolems, procLemmas);
+  TrustNode tplemma = preprocessInternal(lemma, newLemmas, procLemmas);
   if (tplemma.isNull())
   {
     // no change needed
@@ -240,9 +231,7 @@ struct preprocess_stack_element
 };
 
 TrustNode TheoryPreprocessor::theoryPreprocess(
-    TNode assertion,
-    std::vector<TrustNode>& newLemmas,
-    std::vector<Node>& newSkolems)
+    TNode assertion, std::vector<SkolemLemma>& newLemmas)
 {
   Trace("theory::preprocess")
       << "TheoryPreprocessor::theoryPreprocess(" << assertion << ")" << endl;
@@ -284,13 +273,7 @@ TrustNode TheoryPreprocessor::theoryPreprocess(
     // If this is an atom, we preprocess its terms with the theory ppRewriter
     if (tid != THEORY_BOOL)
     {
-      std::vector<SkolemLemma> lems;
-      Node ppRewritten = ppTheoryRewrite(current, lems);
-      for (const SkolemLemma& lem : lems)
-      {
-        newLemmas.push_back(lem.d_lemma);
-        newSkolems.push_back(lem.d_skolem);
-      }
+      Node ppRewritten = ppTheoryRewrite(current, newLemmas);
       Assert(Rewriter::rewrite(ppRewritten) == ppRewritten);
       if (isProofEnabled() && ppRewritten != current)
       {
@@ -302,7 +285,7 @@ TrustNode TheoryPreprocessor::theoryPreprocess(
       // Term formula removal without fixed point. We do not need to do fixed
       // point since newLemmas are theory-preprocessed until fixed point in
       // preprocessInternal (at top-level, when procLemmas=true).
-      TrustNode ttfr = d_tfr.run(ppRewritten, newLemmas, newSkolems, false);
+      TrustNode ttfr = d_tfr.run(ppRewritten, newLemmas, false);
       Node rtfNode = ppRewritten;
       if (!ttfr.isNull())
       {

diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h
index d34bd5c457b02931e0b5dc275be9e0d732c09b5d..e4bd5955a21404a394a5d2ded69b5e6e183afd25 100644 (file)
--- a/src/theory/theory_preprocessor.h
+++ b/src/theory/theory_preprocessor.h
@@ -93,9 +93,7 @@ class TheoryPreprocessor : protected EnvObj
    * @return The (REWRITE) trust node corresponding to rewritten node via
    * preprocessing.
    */
-  TrustNode preprocess(TNode node,
-                       std::vector<TrustNode>& newLemmas,
-                       std::vector<Node>& newSkolems);
+  TrustNode preprocess(TNode node, std::vector<SkolemLemma>& newLemmas);
   /**
    * Same as above, but transforms the proof of node into a proof of the
    * preprocessed node and returns the LEMMA trust node.
@@ -107,8 +105,7 @@ class TheoryPreprocessor : protected EnvObj
    * form of the proven field of node.
    */
   TrustNode preprocessLemma(TrustNode node,
-                            std::vector<TrustNode>& newLemmas,
-                            std::vector<Node>& newSkolems);
+                            std::vector<SkolemLemma>& newLemmas);
 
   /** Get the term formula removal utility */
   RemoveTermFormulas& getRemoveTermFormulas();
@@ -118,17 +115,14 @@ class TheoryPreprocessor : protected EnvObj
    * Runs theory specific preprocessing (Theory::ppRewrite) on the non-Boolean
    * parts of the node.
    */
-  TrustNode theoryPreprocess(TNode node,
-                             std::vector<TrustNode>& newLemmas,
-                             std::vector<Node>& newSkolems);
+  TrustNode theoryPreprocess(TNode node, std::vector<SkolemLemma>& newLemmas);
   /**
    * Internal helper for preprocess, which also optionally preprocesses the
    * new lemmas generated until a fixed point is reached based on argument
    * procLemmas.
    */
   TrustNode preprocessInternal(TNode node,
-                               std::vector<TrustNode>& newLemmas,
-                               std::vector<Node>& newSkolems,
+                               std::vector<SkolemLemma>& newLemmas,
                                bool procLemmas);
   /**
    * Internal helper for preprocessLemma, which also optionally preprocesses the
@@ -136,8 +130,7 @@ class TheoryPreprocessor : protected EnvObj
    * procLemmas.
    */
   TrustNode preprocessLemmaInternal(TrustNode node,
-                                    std::vector<TrustNode>& newLemmas,
-                                    std::vector<Node>& newSkolems,
+                                    std::vector<SkolemLemma>& newLemmas,
                                     bool procLemmas);
   /** Reference to owning theory engine */
   TheoryEngine& d_engine;