Clean remaining references to getNextDecisionRequest and simplify (#2500)

8 files changed, 13 insertions, 48 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index a04c12903..3313a684f 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -40,7 +40,6 @@
 #       notifyRestart     the theory supports notifyRestart()
 #       presolve          the theory supports presolve()
 #       postsolve         the theory supports postsolve()
-#       getNextDecisionRequest the theory supports getNextDecisionRequest()
 #
 #     In the case of the "theory-supports-function" properties, you
 #     need to declare these for your theory or the functions will not
diff --git a/src/theory/decision_manager.cpp b/src/theory/decision_manager.cpp
index 3cc67fe6d..5c43e6159 100644
--- a/src/theory/decision_manager.cpp
+++ b/src/theory/decision_manager.cpp
@@ -38,7 +38,7 @@ void DecisionManager::registerStrategy(StrategyId id, DecisionStrategy* ds)
   d_reg_strategy[id].push_back(ds);
 }
 
-Node DecisionManager::getNextDecisionRequest(unsigned& priority)
+Node DecisionManager::getNextDecisionRequest()
 {
   Trace("dec-manager-debug")
       << "DecisionManager: Get next decision..." << std::endl;
@@ -51,10 +51,6 @@ Node DecisionManager::getNextDecisionRequest(unsigned& priority)
       Node lit = ds->getNextDecisionRequest();
       if (!lit.isNull())
       {
-        StrategyId sid = rs.first;
-        priority = sid < STRAT_LAST_M_SOUND
-                       ? 0
-                       : (sid < STRAT_LAST_FM_COMPLETE ? 1 : 2);
         Trace("dec-manager")
             << "DecisionManager:  -> literal " << lit << " decided by strategy "
             << ds->identify() << std::endl;
diff --git a/src/theory/decision_manager.h b/src/theory/decision_manager.h
index 7ac27a531..fbc0e2cd6 100644
--- a/src/theory/decision_manager.h
+++ b/src/theory/decision_manager.h
@@ -105,11 +105,8 @@ class DecisionManager
    * returns null, then no decisions are required by a decision strategy
    * registered to this class. In the latter case, the SAT solver will choose
    * a decision based on its given heuristic.
-   *
-   * The argument priority has the same role as in
-   * Theory::getNextDecisionRequest.
    */
-  Node getNextDecisionRequest(unsigned& priorty);
+  Node getNextDecisionRequest();
 
  private:
   /** Map containing all strategies registered to this manager */
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 15166fc1f..456a4b0ea 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -53,7 +53,6 @@ theory_has_ppStaticLearn="false"
 theory_has_notifyRestart="false"
 theory_has_presolve="false"
 theory_has_postsolve="false"
-theory_has_getNextDecisionRequest="false"
 
 theory_stable_infinite="false"
 theory_finite="false"
@@ -177,14 +176,13 @@ struct TheoryTraits<${theory_id}> {
     static const bool hasNotifyRestart = ${theory_has_notifyRestart};
     static const bool hasPresolve = ${theory_has_presolve};
     static const bool hasPostsolve = ${theory_has_postsolve};
-    static const bool hasGetNextDecisionRequest = ${theory_has_getNextDecisionRequest};
 };/* struct TheoryTraits<${theory_id}> */
 "
 
   # warnings about theory content and properties
   dir="$(dirname "$kf")/../../"
   if [ -e "$dir/$theory_header" ]; then
-    for function in check propagate ppStaticLearn notifyRestart presolve postsolve getNextDecisionRequest; do
+    for function in check propagate ppStaticLearn notifyRestart presolve postsolve; do
        if eval "\$theory_has_$function"; then
          grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' ||
            echo "$kf: warning: $theory_class has property \"$function\" in its kinds file but doesn't appear to declare the function" >&2
@@ -203,7 +201,6 @@ struct TheoryTraits<${theory_id}> {
   theory_has_notifyRestart="false"
   theory_has_presolve="false"
   theory_has_postsolve="false"
-  theory_has_getNextDecisionRequest="false"
 
   theory_stable_infinite="false"
   theory_finite="false"
@@ -286,7 +283,6 @@ function properties {
        ppStaticLearn) theory_has_ppStaticLearn="true";;
        presolve) theory_has_presolve="true";;
        postsolve) theory_has_postsolve="true";;
-       getNextDecisionRequest) theory_has_getNextDecisionRequest="true";;
        notifyRestart) theory_has_notifyRestart="true";;
        *) echo "$kf:$lineno: error: unknown theory property \"$property\"" >&2; exit 1;;
     esac
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index de4a013cd..7fb2d26c6 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -6,7 +6,7 @@
 
 theory THEORY_STRINGS ::CVC4::theory::strings::TheoryStrings "theory/strings/theory_strings.h"
 
-properties check parametric propagate getNextDecisionRequest presolve
+properties check parametric propagate presolve
 
 rewriter ::CVC4::theory::strings::TheoryStringsRewriter "theory/strings/theory_strings_rewriter.h"
 
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 534f091bf..8a0c87c9e 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -533,16 +533,6 @@ public:
   /** if theories want to do something with model after building, do it here */
   virtual void postProcessModel( TheoryModel* m ){ }
   /**
-   * Return a decision request, if the theory has one, or the NULL node
-   * otherwise.
-   * If returning non-null node, should set priority to
-   *                        0 if decision is necessary for model-soundness,
-   *                        1 if decision is necessary for completeness,
-   *                        >1 otherwise.
-   */
-  virtual Node getNextDecisionRequest( unsigned& priority ) { return Node(); }
-
-  /**
    * Statically learn from assertion "in," which has been asserted
    * true at the top level.  The theory should only add (via
    * ::operator<< or ::append()) to the "learned" builder---it should
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index b9c3ccc4e..54ac272cc 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -767,28 +767,9 @@ void TheoryEngine::propagate(Theory::Effort effort) {
   }
 }
 
-Node TheoryEngine::getNextDecisionRequest() {
-  unsigned min_priority = 0;
-  Node dec = d_decManager->getNextDecisionRequest(min_priority);
-
-  // Definition of the statement that is to be run by every theory
-#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
-#undef CVC4_FOR_EACH_THEORY_STATEMENT
-#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-  if (theory::TheoryTraits<THEORY>::hasGetNextDecisionRequest && d_logicInfo.isTheoryEnabled(THEORY)) { \
-    unsigned priority; \
-    Node n = theoryOf(THEORY)->getNextDecisionRequest( priority ); \
-    if(! n.isNull() && ( dec.isNull() || priority<min_priority ) ) { \
-      dec = n; \
-      min_priority = priority; \
-    } \
-  }
-
-  // Request decision from each theory using the statement above
-  CVC4_FOR_EACH_THEORY;
-
-  return dec;
+Node TheoryEngine::getNextDecisionRequest()
+{
+  return d_decManager->getNextDecisionRequest();
 }
 
 bool TheoryEngine::properConflict(TNode conflict) const {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index b5ac208d7..09f986686 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -702,6 +702,12 @@ public:
     }
   }
 
+  /**
+   * Returns the next decision request, or null if none exist. The next
+   * decision request is a literal that this theory engine prefers the SAT
+   * solver to make as its next decision. Decision requests are managed by
+   * the decision manager d_decManager.
+   */
   Node getNextDecisionRequest();
 
   bool properConflict(TNode conflict) const;