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/decision_strategy.h b/src/decision/decision_strategy.h
index ebddc659d..5e8adb0b8 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -46,10 +46,6 @@ public:
   virtual ~DecisionStrategy() { }
 
   virtual prop::SatLiteral getNext(bool&) = 0;
-
-  virtual bool needIteSkolemMap() { return false; }
-
-  virtual void notifyAssertionsAvailable() { return; }
 };/* class DecisionStrategy */
 
 class ITEDecisionStrategy : public DecisionStrategy {
@@ -57,28 +53,18 @@ public:
   ITEDecisionStrategy(DecisionEngine* de, context::Context *c) :
     DecisionStrategy(de, c) {
   }
-
-  bool needIteSkolemMap() override { return true; }
-
   /**
-   * Add a list of assertions, as well as lemmas coming from preprocessing
-   * (ppLemmas) and pairwise the skolems they constrain (ppSkolems).
+   * Add that assertion is an (input) assertion, not corresponding to a
+   * skolem definition.
+   */
+  virtual void addAssertion(TNode assertion) = 0;
+  /**
+   * Add that lem is the skolem definition for skolem, which is a part of
+   * the current assertions.
    */
-  virtual void addAssertions(const std::vector<Node>& assertions,
-                             const std::vector<Node>& ppLemmas,
-                             const std::vector<Node>& ppSkolems) = 0;
+  virtual void addSkolemDefinition(TNode lem, TNode skolem) = 0;
 };/* class ITEDecisionStrategy */
 
-class RelevancyStrategy : public ITEDecisionStrategy {
-public:
-  RelevancyStrategy(DecisionEngine* de, context::Context *c) :
-    ITEDecisionStrategy(de, c) {
-  }
-
-  virtual bool isRelevant(TNode n) = 0;
-  virtual prop::SatValue getPolarity(TNode n) = 0;
-};/* class RelevancyStrategy */
-
 }/* CVC4::decision namespace */
 }/* CVC4 namespace */