1 files changed, 10 insertions, 0 deletions
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 545ae1770..fb6f673d9 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -40,6 +40,7 @@ class DecisionEngine {
 
   vector <DecisionStrategy* > d_enabledStrategies;
   vector <ITEDecisionStrategy* > d_needIteSkolemMap;
+  RelevancyStrategy* d_relevancyStrategy;
 
   vector <Node> d_assertions;
 
@@ -107,6 +108,15 @@ public:
     return ret;
   }
 
+  /** 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 "