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, 12 insertions, 28 deletions

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 15dbf0d79..914636fe9 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -37,12 +37,6 @@ using namespace CVC4::decision;
 namespace CVC4 {
 
 class DecisionEngine {
-  std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy;
-  vector <ITEDecisionStrategy* > d_needIteSkolemMap;
-  RelevancyStrategy* d_relevancyStrategy;
-
-  typedef context::CDList<Node> AssertionsList;
-  AssertionsList d_assertions;
 
   // PropEngine* d_propEngine;
   CnfStream* d_cnfStream;
@@ -105,15 +99,6 @@ class DecisionEngine {
   /** Gets the next decision based on strategies that are enabled */
   SatLiteral getNext(bool& stopSearch);
 
-  /** Is a sat variable relevant */
-  bool isRelevant(SatVariable var);
-
-  /**
-   * Try to get tell SAT solver what polarity to try for a
-   * decision. Return SAT_VALUE_UNKNOWN if it can't help
-   */
-  SatValue getPolarity(SatVariable var);
-
   /** Is the DecisionEngine in a state where it has solved everything? */
   bool isDone() {
     Trace("decision") << "DecisionEngine::isDone() returning "
@@ -142,23 +127,18 @@ class DecisionEngine {
   // External World helping us help the Strategies
 
   /**
-   * Add a list of assertions, as well as lemmas coming from preprocessing
-   * (ppLemmas) and pairwise the skolems they constrain (ppSkolems).
+   * Notify this class that assertion is an (input) assertion, not corresponding
+   * to a skolem definition.
    */
-  void addAssertions(const std::vector<Node>& assertions,
-                     const std::vector<Node>& ppLemmas,
-                     const std::vector<Node>& ppSkolems);
-
-  // Interface for Strategies to use stuff stored in Decision Engine
-  // (which was possibly requested by them on initialization)
-
+  void addAssertion(TNode assertion);
   /**
-   * Get the assertions. Strategies are notified when these are available.
+   * Notify this class  that lem is the skolem definition for skolem, which is
+   * a part of the current assertions.
    */
-  AssertionsList& getAssertions() {
-    return d_assertions;
-  }
+  void addSkolemDefinition(TNode lem, TNode skolem);
 
+  // Interface for Strategies to use stuff stored in Decision Engine
+  // (which was possibly requested by them on initialization)
 
   // Interface for Strategies to get information about External World
 
@@ -177,6 +157,10 @@ class DecisionEngine {
   Node getNode(SatLiteral l) {
     return d_cnfStream->getNode(l);
   }
+
+ private:
+  /** The ITE decision strategy we have allocated */
+  std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy;
 };/* DecisionEngine class */
 
 }/* CVC4 namespace */