Consolidate interface to prop engine (#6189)

This consolidates the interface for asserting input formulas to the PropEngine from SmtSolver.

As a consequence of this PR, this corrects one issue with the justification heuristic where skolem definitions were considered "assertions" by the justification heuristic (e.g. formulas that must be satisfied) instead of just being required for skolems in relevant literals. This was asymmetric from skolem definitions from lemmas, which were not being considered assertions. Now, skolem definitions are never assertions.

I tested this on QF_LIA SMT-LIB with decision=justification with 300 second timeout, essentially no difference in results (+6-5 all close to timeout). Also no difference on QF_S + QF_SLIA.

1 files changed, 27 insertions, 19 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index efe599106..65d20d9a0 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -171,27 +171,35 @@ theory::TrustNode PropEngine::removeItes(
   return d_theoryProxy->removeItes(node, newLemmas, newSkolems);
 }
 
-void PropEngine::notifyPreprocessedAssertions(
-    const std::vector<Node>& assertions)
-{
-  // notify the theory proxy of preprocessed assertions
-  d_theoryProxy->notifyPreprocessedAssertions(assertions);
-}
-
-void PropEngine::assertFormula(TNode node) {
-  Assert(!d_inCheckSat) << "Sat solver in solve()!";
-  Debug("prop") << "assertFormula(" << node << ")" << std::endl;
-  // NOTE: we do not notify the theory proxy here, since we've already
-  // notified the theory proxy during notifyPreprocessedAssertions
-  assertInternal(node, false, false, true);
-}
-
-void PropEngine::assertSkolemDefinition(TNode node, TNode skolem)
+void PropEngine::assertInputFormulas(
+    const std::vector<Node>& assertions,
+    std::unordered_map<size_t, Node>& skolemMap)
 {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
-  Debug("prop") << "assertFormula(" << node << ")" << std::endl;
-  d_theoryProxy->notifyAssertion(node, skolem);
-  assertInternal(node, false, false, true);
+  // notify the theory engine of preprocessed assertions
+  d_theoryEngine->notifyPreprocessedAssertions(assertions);
+  // Now, notify the theory proxy of the assertions and skolem definitions.
+  // Notice we do this before asserting the formulas to the CNF stream below,
+  // since (preregistration) lemmas may occur during calls to assertInternal.
+  // These lemmas we want to be notified about after the theory proxy has
+  // been notified about all input assertions.
+  std::unordered_map<size_t, Node>::iterator it;
+  for (size_t i = 0, asize = assertions.size(); i < asize; i++)
+  {
+    // is the assertion a skolem definition?
+    it = skolemMap.find(i);
+    Node skolem;
+    if (it != skolemMap.end())
+    {
+      skolem = it->second;
+    }
+    d_theoryProxy->notifyAssertion(assertions[i], skolem);
+  }
+  for (const Node& node : assertions)
+  {
+    Debug("prop") << "assertFormula(" << node << ")" << std::endl;
+    assertInternal(node, false, false, true);
+  }
 }
 
 void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)