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, 1 insertions, 1 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index fb3e6fb36..0fa4fad12 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -381,7 +381,7 @@ void InstantiationEngine::propagate( Theory::Effort level ){
     bool value;
     if( !d_quantEngine->getValuation().hasSatValue( it->second, value ) ){
       //if not already set, propagate as decision
-      d_quantEngine->getOutputChannel().propagateAsDecision( it->second );
+      //d_quantEngine->getOutputChannel().propagateAsDecision( it->second );
       Debug("cbqi-prop-as-dec") << "CBQI: propagate as decision " << it->second << std::endl;
     }
   }