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.

2 files changed, 23 insertions, 8 deletions

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 83f2146f4..996a51e90 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -226,11 +226,11 @@ void SmtSolver::processAssertions(Assertions& as)
   // process the assertions with the preprocessor
   bool noConflict = d_pp.process(as);
 
-  // Push the formula to decision engine
+  // Notify the input formulas to theory engine
   if (noConflict)
   {
-    Chat() << "notifying theory engine and decision engine..." << std::endl;
-    d_propEngine->notifyPreprocessedAssertions(ap);
+    Chat() << "notifying theory engine..." << std::endl;
+    d_propEngine->notifyPreprocessedAssertions(ap.ref());
   }
 
   // end: INVARIANT to maintain: no reordering of assertions or
@@ -240,10 +240,27 @@ void SmtSolver::processAssertions(Assertions& as)
   {
     Chat() << "converting to CNF..." << endl;
     TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime);
-    for (const Node& assertion : ap.ref())
+    const std::vector<Node>& assertions = ap.ref();
+    // It is important to distinguish the input assertions from the skolem
+    // 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++)
     {
-      Chat() << "+ " << assertion << std::endl;
-      d_propEngine->assertFormula(assertion);
+      // 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);
+      }
     }
   }
 
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 54dc488bf..803021fc3 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -34,8 +34,6 @@
 
 namespace CVC4 {
 
-typedef std::unordered_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
-
 class RemoveTermFormulas {
  public:
   RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm = nullptr);