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, 6 insertions, 0 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 397f7cff7..46244aec6 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -560,6 +560,12 @@ public:
   }
 
   /**
+   * Return a decision request, if the theory has one, or the NULL node
+   * otherwise.
+   */
+  virtual Node getNextDecisionRequest() { 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