1 files changed, 63 insertions, 56 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index da19480f9..e99e11eb2 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -171,40 +171,25 @@ theory::TrustNode PropEngine::removeItes(
 }
 
 void PropEngine::notifyPreprocessedAssertions(
-    const preprocessing::AssertionPipeline& ap)
+    const std::vector<Node>& assertions)
 {
   // notify the theory engine of preprocessed assertions
-  d_theoryEngine->notifyPreprocessedAssertions(ap.ref());
-
-  // Add assertions to decision engine, which manually extracts what assertions
-  // corresponded to term formula removal. Note that alternatively we could
-  // delay all theory preprocessing and term formula removal to this point, in
-  // which case this method could simply take a vector of Node and not rely on
-  // assertion pipeline or its ITE skolem map.
-  std::vector<Node> ppLemmas;
-  std::vector<Node> ppSkolems;
-  for (const std::pair<const Node, unsigned>& i : ap.getIteSkolemMap())
-  {
-    Assert(i.second >= ap.getRealAssertionsEnd() && i.second < ap.size());
-    ppSkolems.push_back(i.first);
-    ppLemmas.push_back(ap[i.second]);
-  }
-  d_decisionEngine->addAssertions(ap.ref(), ppLemmas, ppSkolems);
+  d_theoryEngine->notifyPreprocessedAssertions(assertions);
 }
 
 void PropEngine::assertFormula(TNode node) {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
   Debug("prop") << "assertFormula(" << node << ")" << endl;
-  if (isProofEnabled())
-  {
-    d_pfCnfStream->convertAndAssert(node, false, false, nullptr);
-    // register in proof manager
-    d_ppm->registerAssertion(node);
-  }
-  else
-  {
-    d_cnfStream->convertAndAssert(node, false, false, true);
-  }
+  d_decisionEngine->addAssertion(node);
+  assertInternal(node, false, false, true);
+}
+
+void PropEngine::assertSkolemDefinition(TNode node, TNode skolem)
+{
+  Assert(!d_inCheckSat) << "Sat solver in solve()!";
+  Debug("prop") << "assertFormula(" << node << ")" << endl;
+  d_decisionEngine->addSkolemDefinition(node, skolem);
+  assertInternal(node, false, false, true);
 }
 
 void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
@@ -243,42 +228,66 @@ void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
   }
 
   // now, assert the lemmas
-  assertLemmaInternal(tplemma, removable);
-  for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
-  {
-    assertLemmaInternal(ppLemmas[i], removable);
-  }
-
-  // assert to decision engine
-  if (!removable)
-  {
-    // also add to the decision engine, where notice we don't need proofs
-    std::vector<Node> assertions;
-    assertions.push_back(tplemma.getProven());
-    std::vector<Node> ppLemmasF;
-    for (const theory::TrustNode& tnl : ppLemmas)
-    {
-      ppLemmasF.push_back(tnl.getProven());
-    }
-    d_decisionEngine->addAssertions(assertions, ppLemmasF, ppSkolems);
-  }
+  assertLemmasInternal(tplemma, ppLemmas, ppSkolems, removable);
 }
 
-void PropEngine::assertLemmaInternal(theory::TrustNode trn, bool removable)
+void PropEngine::assertTrustedLemmaInternal(theory::TrustNode trn,
+                                            bool removable)
 {
   Node node = trn.getNode();
-  bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
+  bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
+  Assert(!isProofEnabled() || trn.getGenerator() != nullptr);
+  assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator());
+}
+
+void PropEngine::assertInternal(
+    TNode node, bool negated, bool removable, bool input, ProofGenerator* pg)
+{
   // Assert as (possibly) removable
   if (isProofEnabled())
   {
-    Assert(trn.getGenerator());
-    d_pfCnfStream->convertAndAssert(
-        node, negated, removable, trn.getGenerator());
+    d_pfCnfStream->convertAndAssert(node, negated, removable, pg);
+    // if input, register the assertion
+    if (input)
+    {
+      d_ppm->registerAssertion(node);
+    }
   }
   else
   {
-    d_cnfStream->convertAndAssert(node, removable, negated);
+    d_cnfStream->convertAndAssert(node, removable, negated, input);
+  }
+}
+void PropEngine::assertLemmasInternal(
+    theory::TrustNode trn,
+    const std::vector<theory::TrustNode>& ppLemmas,
+    const std::vector<Node>& ppSkolems,
+    bool removable)
+{
+  if (!trn.isNull())
+  {
+    assertTrustedLemmaInternal(trn, removable);
+  }
+  for (const theory::TrustNode& tnl : ppLemmas)
+  {
+    assertTrustedLemmaInternal(tnl, removable);
+  }
+  // assert to decision engine
+  if (!removable)
+  {
+    // also add to the decision engine, where notice we don't need proofs
+    if (!trn.isNull())
+    {
+      // notify the theory proxy of the lemma
+      d_decisionEngine->addAssertion(trn.getProven());
+    }
+    Assert(ppSkolems.size() == ppLemmas.size());
+    for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
+    {
+      Node lem = ppLemmas[i].getProven();
+      d_decisionEngine->addSkolemDefinition(lem, ppSkolems[i]);
+    }
   }
 }
 
@@ -441,10 +450,8 @@ Node PropEngine::getPreprocessedTerm(TNode n)
   std::vector<Node> newSkolems;
   theory::TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas, newSkolems);
   // send lemmas corresponding to the skolems introduced by preprocessing n
-  for (const theory::TrustNode& tnl : newLemmas)
-  {
-    assertLemma(tnl, theory::LemmaProperty::NONE);
-  }
+  theory::TrustNode trnNull;
+  assertLemmasInternal(trnNull, newLemmas, newSkolems, false);
   return tpn.isNull() ? Node(n) : tpn.getNode();
 }