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

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 6787f8ad8..f7cbe8b73 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -228,6 +228,8 @@ class TheoryArrays : public Theory {
   private:
   public:
 
+  Node getNextDecisionRequest();
+
   void presolve();
   void shutdown() { }
 
@@ -333,6 +335,9 @@ class TheoryArrays : public Theory {
   context::CDList<TNode> d_reads;
   std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache;
 
+  // The decision requests we have for the core
+  context::CDQueue<Node> d_decisionRequests;
+
   // List of nodes that need permanent references in this context
   context::CDList<Node> d_permRef;