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 */