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

3 files changed, 19 insertions, 4 deletions

diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index ef237e351..986654cd3 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -9,7 +9,7 @@ typechecker "theory/arrays/theory_arrays_type_rules.h"
 instantiator ::CVC4::theory::arrays::InstantiatorTheoryArrays "theory/arrays/theory_arrays_instantiator.h"
 
 properties polite stable-infinite parametric
-properties check propagate presolve
+properties check propagate presolve getNextDecisionRequest
 
 rewriter ::CVC4::theory::arrays::TheoryArraysRewriter "theory/arrays/theory_arrays_rewriter.h"
 
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();
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;