Simplify and fix decision engine's handling of skolem definitions (#5888)

This PR changes the front end of prop engine to distinguish input formulas from skolem definitions, which is required by the decision engine. This PR breaks the dependency of PropEngine on the AssertionsPipeline, as now the determining of whether an input formula is a skolem definition is handled externally, in SmtSolver.

With this PR, we should not be required to satisfy skolem definitions that are not relevant based on the techniques already implemented in the decision engine. Currently, we are not distinguishing input formulas from skolem definitions properly, meaning we assert more literals than we need to.

This also simplifies related interfaces within decision engine.

We should test this PR with --decision=justification on SMT-LIB.

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();
 }