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, 13 insertions, 3 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 47f3e31db..4f2497d2b 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -76,6 +76,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   d_sharedOther(c),
   d_sharedTerms(c, false),
   d_reads(c),
+  d_decisionRequests(c),
   d_permRef(c)
 {
   StatisticsRegistry::registerStat(&d_numRow);
@@ -1082,7 +1083,6 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
   Trace("arrays-crl")<<"Arrays::checkLemmas done.\n";
 }
 
-
 void TheoryArrays::queueRowLemma(RowLemmaType lem)
 {
   if (d_conflict || d_RowAlreadyAdded.count(lem) != 0) {
@@ -1148,8 +1148,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
 
   // Prefer equality between indexes so as not to introduce new read terms
   if (d_eagerIndexSplitting && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) {
-    Node split = d_valuation.ensureLiteral(i.eqNode(j));
-    d_out->propagateAsDecision(split);
+    d_decisionRequests.push(i.eqNode(j));
   }
 
   // TODO: maybe add triggers here
@@ -1215,6 +1214,17 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
 }
 
 
+Node TheoryArrays::getNextDecisionRequest() {
+  if(! d_decisionRequests.empty()) {
+    Node n = d_valuation.ensureLiteral(d_decisionRequests.front());
+    d_decisionRequests.pop();
+    return n;
+  } else {
+    return Node::null();
+  }
+}
+
+
 void TheoryArrays::dischargeLemmas()
 {
   size_t sz = d_RowQueue.size();