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, 8 insertions, 22 deletions

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index afbff18c1..1d0b386e3 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -164,16 +164,8 @@ inline void computeXorIffDesiredValues
   }
 }
 
-void JustificationHeuristic::addAssertions(const std::vector<Node>& assertions,
-                                           const std::vector<Node>& ppLemmas,
-                                           const std::vector<Node>& ppSkolems)
+void JustificationHeuristic::addAssertion(TNode assertion)
 {
-  Assert(ppSkolems.size() == ppLemmas.size());
-  Trace("decision")
-    << "JustificationHeuristic::addAssertions()"
-    << " size = " << assertions.size()
-    << std::endl;
-
   // Save all assertions locally, including the assertions generated by term
   // removal. We have to make sure that we assign a value to all the Boolean
   // term variables. To illustrate why this is, consider the case where we have
@@ -191,20 +183,14 @@ void JustificationHeuristic::addAssertions(const std::vector<Node>& assertions,
   // assertion to be satisifed. However, we also have to make sure that we pick
   // a value for `b` that is not in conflict with the other assignments (we can
   // only choose `b` to be `true` otherwise the model is incorrect).
-  for (const Node& assertion : assertions)
-  {
-    d_assertions.push_back(assertion);
-  }
-
-  // Save mapping between ite skolems and ite assertions
-  for (size_t i = 0, nlemmas = ppLemmas.size(); i < nlemmas; i++)
-  {
-    Trace("decision::jh::ite") << " jh-ite: " << ppSkolems[i] << " maps to "
-                               << ppLemmas[i] << std::endl;
-    d_skolemAssertions[ppSkolems[i]] = ppLemmas[i];
-  }
+  d_assertions.push_back(assertion);
+}
 
-  // Automatic weight computation
+void JustificationHeuristic::addSkolemDefinition(TNode lem, TNode skolem)
+{
+  Trace("decision::jh::ite")
+      << " jh-ite: " << skolem << " maps to " << lem << std::endl;
+  d_skolemAssertions[skolem] = lem;
 }
 
 SatLiteral JustificationHeuristic::findSplitter(TNode node,