Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly.

1 files changed, 331 insertions, 86 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index b9a415e46..f3061f575 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/theory_engine.h"
 
 using namespace std;
@@ -34,9 +35,13 @@ using namespace CVC4::theory::arith;
 #define ARITH_INSTANTIATOR_USE_MINUS_DELTA
 
 InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe )
-  : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() )
+  : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), 
+d_elim_quants( qe->getSatContext() ),
+d_nested_qe_waitlist_size( qe->getUserContext() ),
+d_nested_qe_waitlist_proc( qe->getUserContext() )
 //, d_added_inst( qe->getUserContext() )
 {
+  d_qid_count = 0;
 }
 
 InstStrategyCbqi::~InstStrategyCbqi() throw(){}
@@ -55,6 +60,103 @@ unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) {
   return QuantifiersEngine::QEFFORT_NONE;
 }
 
+bool InstStrategyCbqi::registerCbqiLemma( Node q ) {
+  if( !hasAddedCbqiLemma( q ) ){
+    d_added_cbqi_lemma.insert( q );
+    Trace("cbqi-debug") << "Do cbqi for " << q << std::endl;
+    //add cbqi lemma
+    //get the counterexample literal
+    Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
+    Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
+    if( !ceBody.isNull() ){
+      //add counterexample lemma
+      Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
+      //require any decision on cel to be phase=true
+      d_quantEngine->addRequirePhase( ceLit, true );
+      Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
+      //add counterexample lemma
+      lem = Rewriter::rewrite( lem );
+      Trace("cbqi-lemma") << "Counterexample lemma : " << lem << std::endl;
+      registerCounterexampleLemma( q, lem );
+      
+      //totality lemmas for EPR
+      QuantEPR * qepr = d_quantEngine->getQuantEPR();
+      if( qepr!=NULL ){   
+        for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+          TypeNode tn = q[0][i].getType();
+          if( tn.isSort() ){
+            if( qepr->isEPR( tn ) ){
+              //add totality lemma
+              std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn );
+              if( itc!=qepr->d_consts.end() ){
+                Assert( !itc->second.empty() );
+                Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i );
+                std::vector< Node > disj;
+                for( unsigned j=0; j<itc->second.size(); j++ ){
+                  disj.push_back( ic.eqNode( itc->second[j] ) );
+                }
+                Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj );
+                Trace("cbqi-lemma") << "EPR totality lemma : " << tlem << std::endl;
+                d_quantEngine->getOutputChannel().lemma( tlem );
+              }else{
+                Assert( false );
+              }                  
+            }else{
+              Assert( !options::cbqiAll() );
+            }
+          }
+        }
+      }      
+      
+      //compute dependencies between quantified formulas
+      if( options::cbqiLitDepend() || options::cbqiInnermost() ){
+        std::vector< Node > ics;
+        TermDb::computeVarContains( q, ics );
+        d_parent_quant[q].clear();
+        d_children_quant[q].clear();
+        std::vector< Node > dep;
+        for( unsigned i=0; i<ics.size(); i++ ){
+          Node qi = ics[i].getAttribute(InstConstantAttribute());
+          if( std::find( d_parent_quant[q].begin(), d_parent_quant[q].end(), qi )==d_parent_quant[q].end() ){
+            d_parent_quant[q].push_back( qi );
+            d_children_quant[qi].push_back( q );
+            Node qicel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( qi );
+            dep.push_back( qi );
+            dep.push_back( qicel );
+          }
+        }
+        if( !dep.empty() ){
+          Node dep_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, ceLit, NodeManager::currentNM()->mkNode( kind::AND, dep ) );
+          Trace("cbqi-lemma") << "Counterexample dependency lemma : " << dep_lemma << std::endl;
+          d_quantEngine->getOutputChannel().lemma( dep_lemma );
+        }
+      }
+      
+      //must register all sub-quantifiers of counterexample lemma, register their lemmas
+      std::vector< Node > quants;
+      TermDb::computeQuantContains( lem, quants );
+      for( unsigned i=0; i<quants.size(); i++ ){
+        if( doCbqi( quants[i] ) ){
+          registerCbqiLemma( quants[i] );
+        }
+        if( options::cbqiNestedQE() ){
+          //record these as counterexample quantifiers
+          QAttributes qa;
+          TermDb::computeQuantAttributes( quants[i], qa );
+          if( qa.d_qid_num!=-1 ){
+            d_id_to_ce_quant[ qa.d_qid_num ] = quants[i];
+            d_ce_quant_to_id[ quants[i] ] = qa.d_qid_num;
+            Trace("cbqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl;
+          }
+        }
+      }
+    }
+    return true;
+  }else{
+    return false;
+  }
+}
+
 void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
   d_cbqi_set_quant_inactive = false;
   d_incomplete_check = false;
@@ -64,77 +166,8 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
     //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
     if( doCbqi( q ) ){
-      if( !hasAddedCbqiLemma( q ) ){
-        d_added_cbqi_lemma.insert( q );
-        Trace("cbqi") << "Do cbqi for " << q << std::endl;
-        //add cbqi lemma
-        //get the counterexample literal
-        Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
-        Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
-        if( !ceBody.isNull() ){
-          //add counterexample lemma
-          Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
-          //require any decision on cel to be phase=true
-          d_quantEngine->addRequirePhase( ceLit, true );
-          Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
-          //add counterexample lemma
-          lem = Rewriter::rewrite( lem );
-          Trace("cbqi") << "Counterexample lemma : " << lem << std::endl;
-          registerCounterexampleLemma( q, lem );
-          
-          //totality lemmas for EPR
-          QuantEPR * qepr = d_quantEngine->getQuantEPR();
-          if( qepr!=NULL ){   
-            for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-              TypeNode tn = q[0][i].getType();
-              if( tn.isSort() ){
-                if( qepr->isEPR( tn ) ){
-                  //add totality lemma
-                  std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn );
-                  if( itc!=qepr->d_consts.end() ){
-                    Assert( !itc->second.empty() );
-                    Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i );
-                    std::vector< Node > disj;
-                    for( unsigned j=0; j<itc->second.size(); j++ ){
-                      disj.push_back( ic.eqNode( itc->second[j] ) );
-                    }
-                    Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj );
-                    Trace("cbqi") << "EPR totality lemma : " << tlem << std::endl;
-                    d_quantEngine->getOutputChannel().lemma( tlem );
-                  }else{
-                    Assert( false );
-                  }                  
-                }else{
-                  Assert( !options::cbqiAll() );
-                }
-              }
-            }
-          }      
-          
-          //compute dependencies between quantified formulas
-          if( options::cbqiLitDepend() || options::cbqiInnermost() ){
-            std::vector< Node > ics;
-            TermDb::computeVarContains( q, ics );
-            d_parent_quant[q].clear();
-            d_children_quant[q].clear();
-            std::vector< Node > dep;
-            for( unsigned i=0; i<ics.size(); i++ ){
-              Node qi = ics[i].getAttribute(InstConstantAttribute());
-              if( std::find( d_parent_quant[q].begin(), d_parent_quant[q].end(), qi )==d_parent_quant[q].end() ){
-                d_parent_quant[q].push_back( qi );
-                d_children_quant[qi].push_back( q );
-                Node qicel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( qi );
-                dep.push_back( qi );
-                dep.push_back( qicel );
-              }
-            }
-            if( !dep.empty() ){
-              Node dep_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, ceLit, NodeManager::currentNM()->mkNode( kind::AND, dep ) );
-              Trace("cbqi") << "Counterexample dependency lemma : " << dep_lemma << std::endl;
-              d_quantEngine->getOutputChannel().lemma( dep_lemma );
-            }
-          }
-        }
+      if( registerCbqiLemma( q ) ){
+        Debug("cbqi-debug") << "Registered cbqi lemma." << std::endl;
       //set inactive the quantified formulas whose CE literals are asserted false
       }else if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
         d_active_quant[q] = true;
@@ -147,9 +180,24 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
             if( d_quantEngine->getValuation().isDecision( cel ) ){
               Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
             }else{
+              Trace("cbqi") << "Inactive : " << q << std::endl;
               d_quantEngine->getModel()->setQuantifierActive( q, false );
               d_cbqi_set_quant_inactive = true;
               d_active_quant.erase( q );
+              d_elim_quants.insert( q );
+              Trace("cbqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl;
+              //process from waitlist
+              while( d_nested_qe_waitlist_proc[q]<d_nested_qe_waitlist_size[q] ){
+                int index = d_nested_qe_waitlist_proc[q];
+                Assert( index>=0 );
+                Assert( index<(int)d_nested_qe_waitlist[q].size() );
+                Node nq = d_nested_qe_waitlist[q][index];
+                Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts );
+                Node dqelem = nq.iffNode( nqeqn ); 
+                Trace("cbqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl;
+                d_quantEngine->getOutputChannel().lemma( dqelem );
+                d_nested_qe_waitlist_proc[q] = index + 1;
+              }
             }
           }
         }else{
@@ -204,9 +252,15 @@ void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) {
       //  if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
       for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
         Node q = it->first;
-        process( q, e, ee );
-        if( d_quantEngine->inConflict() ){
-          break;
+        Trace("cbqi") << "CBQI : Process " << q << " at effort " << ee << std::endl;
+        if( d_nested_qe.find( q )==d_nested_qe.end() ){
+          process( q, e, ee );
+          if( d_quantEngine->inConflict() ){
+            break;
+          }
+        }else{
+          Trace("cbqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl;
+          Assert( false );
         }
       }
       if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
@@ -231,11 +285,79 @@ bool InstStrategyCbqi::checkComplete() {
   }
 }
 
+Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ){
+  std::map< Node, Node >::iterator it = visited.find( n );
+  if( it==visited.end() ){
+    Node ret = n;
+    if( n.getKind()==FORALL ){
+      QAttributes qa;
+      TermDb::computeQuantAttributes( n, qa );
+      if( qa.d_qid_num==-1 ){
+        std::vector< Node > rc;
+        rc.push_back( n[0] );
+        rc.push_back( getIdMarkedQuantNode( n[1], visited ) );
+        Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() );
+        QuantIdNumAttribute ida;
+        avar.setAttribute(ida,d_qid_count);
+        d_qid_count++;
+        std::vector< Node > iplc;
+        iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) );
+        if( n.getNumChildren()==3 ){
+          for( unsigned i=0; i<n[2].getNumChildren(); i++ ){
+            iplc.push_back( n[2][i] );
+          }
+        }
+        rc.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, iplc ) );
+        ret = NodeManager::currentNM()->mkNode( FORALL, rc );
+      }
+    }else if( n.getNumChildren()>0 ){
+      std::vector< Node > children;
+      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+        children.push_back( n.getOperator() );
+      }
+      bool childChanged = false;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node nc = getIdMarkedQuantNode( n[i], visited );
+        childChanged = childChanged || nc!=n[i];
+        children.push_back( nc );
+      }
+      if( childChanged ){
+        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }
+    }
+    visited[n] = ret;
+    return ret;
+  }else{
+    return it->second;
+  }
+}
+
 void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
   if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
     if( !options::cbqiAll() && !options::cbqiSplx() ){
       //take full ownership of the quantified formula
       d_quantEngine->setOwner( q, this );
+      
+      //mark all nested quantifiers with id
+      if( options::cbqiNestedQE() ){
+        std::map< Node, Node > visited;
+        Node mq = getIdMarkedQuantNode( q[1], visited );
+        if( mq!=q[1] ){
+          //do not do cbqi
+          d_do_cbqi[q] = false;
+          //instead do reduction
+          std::vector< Node > qqc;
+          qqc.push_back( q[0] );
+          qqc.push_back( mq );
+          if( q.getNumChildren()==3 ){
+            qqc.push_back( q[2] );
+          }
+          Node qq = NodeManager::currentNM()->mkNode( FORALL, qqc );
+          Node mlem = NodeManager::currentNM()->mkNode( IMPLIES, q, qq );
+          Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl;
+          d_quantEngine->getOutputChannel().lemma( mlem );
+        }
+      }
     }
   }
 }
@@ -244,6 +366,97 @@ void InstStrategyCbqi::registerQuantifier( Node q ) {
 
 }
 
+Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts ) {
+  // there is a nested quantified formula (forall y. nq[y,x]) such that 
+  //    q is (forall y. nq[y,t]) for ground terms t,
+  //    ceq is (forall y. nq[y,e]) for CE variables e.
+  // we call this function when we know (exists e. ceq[e,k]) is equivalent to quantifier-free formula C[k].
+  // in this case, q is equivalent to the quantifier-free formula C[t].
+  if( d_nested_qe.find( ceq )==d_nested_qe.end() ){
+    d_nested_qe[ceq] = d_quantEngine->getInstantiatedConjunction( ceq );
+    Trace("cbqi-nqe") << "CE quantifier elimination : " << std::endl;
+    Trace("cbqi-nqe") << "  " << ceq << std::endl; 
+    Trace("cbqi-nqe") << "  " << d_nested_qe[ceq] << std::endl;
+    //should not contain quantifiers
+    Assert( !QuantifiersRewriter::containsQuantifiers( d_nested_qe[ceq] ) );
+  }
+  Assert( d_quantEngine->getTermDatabase()->d_inst_constants[q].size()==inst_terms.size() );
+  //replace inst constants with instantiation
+  Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermDatabase()->d_inst_constants[q].begin(),
+                                          d_quantEngine->getTermDatabase()->d_inst_constants[q].end(),
+                                          inst_terms.begin(), inst_terms.end() );
+  if( doVts ){
+    //do virtual term substitution
+    ret = Rewriter::rewrite( ret );
+    ret = d_quantEngine->getTermDatabase()->rewriteVtsSymbols( ret );
+  }
+  Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl;
+  Trace("cbqi-nqe") << "  " << n << std::endl; 
+  Trace("cbqi-nqe") << "  " << ret << std::endl;
+  return ret;
+}
+
+Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts ) {
+  std::map< Node, Node >::iterator it = visited.find( n );
+  if( visited.find( n )==visited.end() ){
+    Node ret = n;
+    if( n.getKind()==FORALL ){
+      QAttributes qa;
+      TermDb::computeQuantAttributes( n, qa );
+      if( qa.d_qid_num!=-1 ){
+        //if it has an id, check whether we have done quantifier elimination for this id
+        std::map< int, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num );
+        if( it!=d_id_to_ce_quant.end() ){
+          Node ceq = it->second;
+          bool doNestedQe = d_elim_quants.contains( ceq );
+          if( doNestedQe ){
+            ret = doNestedQENode( q, ceq, n, inst_terms, doVts );
+          }else{
+            Trace("cbqi-nqe") << "Add to nested qe waitlist : " << std::endl;
+            Node nr = Rewriter::rewrite( n );
+            Trace("cbqi-nqe") << "  " << ceq << std::endl;
+            Trace("cbqi-nqe") << "  " << nr << std::endl;
+            int wlsize = d_nested_qe_waitlist_size[ceq] + 1;
+            d_nested_qe_waitlist_size[ceq] = wlsize;
+            if( wlsize<(int)d_nested_qe_waitlist[ceq].size() ){
+              d_nested_qe_waitlist[ceq][wlsize] = nr;
+            }else{
+              d_nested_qe_waitlist[ceq].push_back( nr );
+            }
+            d_nested_qe_info[nr].d_q = q;
+            d_nested_qe_info[nr].d_inst_terms.clear();
+            d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() );
+            d_nested_qe_info[nr].d_doVts = doVts;
+          }
+        } 
+      } 
+    }else if( n.getNumChildren()>0 ){
+      std::vector< Node > children;
+      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+        children.push_back( n.getOperator() );
+      }
+      bool childChanged = false;
+      for( unsigned i=0; i<n.getNumChildren(); i++ ){
+        Node nc = doNestedQERec( q, n[i], visited, inst_terms, doVts );
+        childChanged = childChanged || nc!=n[i];
+        children.push_back( nc );
+      }
+      if( childChanged ){
+        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }
+    }
+    visited[n] = ret;
+    return ret;
+  }else{
+    return n;
+  }  
+}
+
+Node InstStrategyCbqi::doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts ) {
+  std::map< Node, Node > visited;
+  return doNestedQERec( q, lem, visited, inst_terms, doVts );
+}
+
 void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){
   Trace("cbqi-debug") << "Counterexample lemma  : " << lem << std::endl;
   d_quantEngine->addLemma( lem, false );
@@ -299,14 +512,17 @@ int InstStrategyCbqi::hasNonCbqiVariable( Node q ){
 bool InstStrategyCbqi::doCbqi( Node q ){
   std::map< Node, bool >::iterator it = d_do_cbqi.find( q );
   if( it==d_do_cbqi.end() ){
-    bool ret = false;
-    if( d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){
-      ret = true;
-    }else{
+    bool ret = true;
+    if( !d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){
       //if has an instantiation pattern, don't do it
       if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
-        ret = false;
-      }else{
+        for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
+          if( q[2][i].getKind()==INST_PATTERN ){
+            ret = false;
+          }
+        }
+      }
+      if( ret ){
         if( options::cbqiAll() ){
           ret = true;
         }else{
@@ -320,11 +536,13 @@ bool InstStrategyCbqi::doCbqi( Node q ){
           }else if( ncbqiv==0 ){
             std::map< Node, bool > visited;
             ret = !hasNonCbqiOperator( q[1], visited );
+          }else{
+            ret = false;
           }
         }
       }
     }
-    Trace("cbqi") << "doCbqi " << q << " returned " << ret << std::endl;
+    Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
     d_do_cbqi[q] = ret;
     return ret;
   }else{
@@ -332,10 +550,20 @@ bool InstStrategyCbqi::doCbqi( Node q ){
   }
 }
 
-Node InstStrategyCbqi::getNextDecisionRequest(){
-  // all counterexample literals that are not asserted
-  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-    Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ) {
+  if( proc.find( q )==proc.end() ){
+    proc[q] = true;
+    //first check children
+    std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( q );
+    if( itc!=d_children_quant.end() ){
+      for( unsigned j=0; j<itc->second.size(); j++ ){
+        Node d = getNextDecisionRequestProc( itc->second[j], proc );
+        if( !d.isNull() ){
+          return d;
+        }
+      }
+    }
+    //then check self
     if( hasAddedCbqiLemma( q ) ){
       Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
       bool value;
@@ -343,6 +571,18 @@ Node InstStrategyCbqi::getNextDecisionRequest(){
         Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl;
         return cel;
       }
+    }    
+  }
+  return Node::null(); 
+}
+
+Node InstStrategyCbqi::getNextDecisionRequest(){
+  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() ){
+      return d;
     }
   }
   return Node::null();
@@ -755,6 +995,9 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
       //d_added_inst.insert( d_curr_quant );
       return true;
     }else{
+      //this should never happen for monotonic selection strategies
+      Trace("cbqi-warn") << "Existing instantiation" << std::endl;
+      Assert( !options::cbqiNestedQE() || options::cbqiAll() );
       return false;
     }
   }
@@ -827,7 +1070,9 @@ void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) {
 void InstStrategyCegqi::presolve() {
   if( options::cbqiPreRegInst() ){
     for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){
+      Trace("cbqi-presolve") << "Presolve " << it->first << std::endl;
       it->second->presolve( it->first );
     }
   }
 }
+