Replace propagateAsDecision() with Theory::getNextDecisionRequest():

* arrays now uses the new approach by using a CDQueue<>
* uf strong solver has had the feature disabled, pending a merge from Andy
* theory kinds files now have a getNextDecisionRequest property (if you want to take part in such decision requests you have to list that property)
* the staticLearning property has been renamed ppStaticLearn to match the function name
* theory kinds files are now checked again for correctly-declared properties (this had been disabled)
* minor documentation and other fixups

1 files changed, 22 insertions, 19 deletions

diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 60ff05d35..c8ef23a78 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -47,10 +47,11 @@ mk_type_enumerator_cases=
 
 theory_has_check="false"
 theory_has_propagate="false"
-theory_has_staticLearning="false"
+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"
@@ -143,36 +144,37 @@ struct TheoryTraits<${theory_id}> {
 
     static const bool hasCheck = ${theory_has_check};
     static const bool hasPropagate = ${theory_has_propagate};
-    static const bool hasStaticLearning = ${theory_has_staticLearning};
+    static const bool hasPpStaticLearn = ${theory_has_ppStaticLearn};
     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
-  # TODO: fix, not corresponding to staticLearning anymore
-  # dir="$(dirname "$kf")/../../"
-  # if [ -e "$dir/$theory_header" ]; then
-  #   for function in check propagate staticLearning 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
-  #      else
-  #        grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' &&
-  #          echo "$kf: warning: $theory_class does not have property \"$function\" in its kinds file but appears to declare the function" >&2
-  #      fi
-  #    done
-  # else
-  #   echo "$me: warning: theory header \"$theory_header\" does not exist or is unreadable" >&2
-  # fi
+  dir="$(dirname "$kf")/../../"
+  if [ -e "$dir/$theory_header" ]; then
+    for function in check propagate ppStaticLearn notifyRestart presolve postsolve getNextDecisionRequest; 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
+       else
+         grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' &&
+           echo "$kf: warning: $theory_class does not have property \"$function\" in its kinds file but appears to declare the function" >&2
+       fi
+     done
+  else
+    echo "$me: warning: theory header \"$theory_header\" does not exist or is unreadable" >&2
+  fi
 
   theory_has_check="false"
   theory_has_propagate="false"
-  theory_has_staticLearning="false"
+  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"
@@ -264,9 +266,10 @@ function properties {
        polite) theory_polite="true";;
        check) theory_has_check="true";;
        propagate) theory_has_propagate="true";;
-       staticLearning) theory_has_staticLearning="true";;
+       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