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, 2 insertions, 25 deletions

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index fbb21034a..3a1c6b12c 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -232,14 +232,7 @@ void SmtSolver::processAssertions(Assertions& as)
   }
 
   // process the assertions with the preprocessor
-  bool noConflict = d_pp.process(as);
-
-  // Notify the input formulas to theory engine
-  if (noConflict)
-  {
-    Chat() << "notifying theory engine..." << std::endl;
-    d_propEngine->notifyPreprocessedAssertions(ap.ref());
-  }
+  d_pp.process(as);
 
   // end: INVARIANT to maintain: no reordering of assertions or
   // introducing new ones
@@ -253,23 +246,7 @@ void SmtSolver::processAssertions(Assertions& as)
     // definitions, as the decision justification heuristic treates the latter
     // specially.
     preprocessing::IteSkolemMap& ism = ap.getIteSkolemMap();
-    preprocessing::IteSkolemMap::iterator it;
-    for (size_t i = 0, asize = assertions.size(); i < asize; i++)
-    {
-      // is the assertion a skolem definition?
-      it = ism.find(i);
-      if (it == ism.end())
-      {
-        Chat() << "+ input " << assertions[i] << std::endl;
-        d_propEngine->assertFormula(assertions[i]);
-      }
-      else
-      {
-        Chat() << "+ skolem definition " << assertions[i] << " (from "
-               << it->second << ")" << std::endl;
-        d_propEngine->assertSkolemDefinition(assertions[i], it->second);
-      }
-    }
+    d_propEngine->assertInputFormulas(assertions, ism);
   }
 
   // clear the current assertions