summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/inst_strategy_cbqi.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.cpp')
-rw-r--r--src/theory/quantifiers/inst_strategy_cbqi.cpp3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index ac6e1edbe..895a0c93c 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -592,12 +592,13 @@ Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool
return Node::null();
}
-Node InstStrategyCbqi::getNextDecisionRequest(){
+Node InstStrategyCbqi::getNextDecisionRequest( unsigned& priority ){
std::map< Node, bool > proc;
for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
Node d = getNextDecisionRequestProc( q, proc );
if( !d.isNull() ){
+ priority = 0;
return d;
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback