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

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.