src/theory/quantifiers/inst_strategy_cbqi.cpp

   1 /*********************                                                        */
   2 /*! \file inst_strategy_cbqi.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Implementation of counterexample-guided quantifier instantiation strategies
  13  **/
  14 #include "theory/quantifiers/inst_strategy_cbqi.h"
  15
  16 #include "options/quantifiers_options.h"
  17 #include "smt/ite_removal.h"
  18 #include "theory/arith/partial_model.h"
  19 #include "theory/arith/theory_arith.h"
  20 #include "theory/arith/theory_arith_private.h"
  21 #include "theory/quantifiers/first_order_model.h"
  22 #include "theory/quantifiers/term_database.h"
  23 #include "theory/quantifiers/trigger.h"
  24 #include "theory/quantifiers/quantifiers_rewriter.h"
  25 #include "theory/theory_engine.h"
  26
  27 using namespace std;
  28 using namespace CVC4;
  29 using namespace CVC4::kind;
  30 using namespace CVC4::context;
  31 using namespace CVC4::theory;
  32 using namespace CVC4::theory::quantifiers;
  33 using namespace CVC4::theory::arith;
  34
  35 #define ARITH_INSTANTIATOR_USE_MINUS_DELTA
  36
  37 InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe )
  38   : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ),
  39 d_elim_quants( qe->getSatContext() ),
  40 d_nested_qe_waitlist_size( qe->getUserContext() ),
  41 d_nested_qe_waitlist_proc( qe->getUserContext() )
  42 //, d_added_inst( qe->getUserContext() )
  43 {
  44   d_qid_count = 0;
  45 }
  46
  47 InstStrategyCbqi::~InstStrategyCbqi() throw(){}
  48
  49 bool InstStrategyCbqi::needsCheck( Theory::Effort e ) {
  50   return e>=Theory::EFFORT_LAST_CALL;
  51 }
  52
  53 unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) {
  54   for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
  55     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
  56     if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
  57       return QuantifiersEngine::QEFFORT_STANDARD;
  58     }
  59   }
  60   return QuantifiersEngine::QEFFORT_NONE;
  61 }
  62
  63 bool InstStrategyCbqi::registerCbqiLemma( Node q ) {
  64   if( !hasAddedCbqiLemma( q ) ){
  65     d_added_cbqi_lemma.insert( q );
  66     Trace("cbqi-debug") << "Do cbqi for " << q << std::endl;
  67     //add cbqi lemma
  68     //get the counterexample literal
  69     Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
  70     Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( q );
  71     if( !ceBody.isNull() ){
  72       //add counterexample lemma
  73       Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
  74       //require any decision on cel to be phase=true
  75       d_quantEngine->addRequirePhase( ceLit, true );
  76       Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
  77       //add counterexample lemma
  78       lem = Rewriter::rewrite( lem );
  79       Trace("cbqi-lemma") << "Counterexample lemma : " << lem << std::endl;
  80       registerCounterexampleLemma( q, lem );
  81
  82       //totality lemmas for EPR
  83       QuantEPR * qepr = d_quantEngine->getQuantEPR();
  84       if( qepr!=NULL ){
  85         for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
  86           TypeNode tn = q[0][i].getType();
  87           if( tn.isSort() ){
  88             if( qepr->isEPR( tn ) ){
  89               //add totality lemma
  90               std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn );
  91               if( itc!=qepr->d_consts.end() ){
  92                 Assert( !itc->second.empty() );
  93                 Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i );
  94                 std::vector< Node > disj;
  95                 for( unsigned j=0; j<itc->second.size(); j++ ){
  96                   disj.push_back( ic.eqNode( itc->second[j] ) );
  97                 }
  98                 Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj );
  99                 Trace("cbqi-lemma") << "EPR totality lemma : " << tlem << std::endl;
 100                 d_quantEngine->getOutputChannel().lemma( tlem );
 101               }else{
 102                 Assert( false );
 103               }
 104             }else{
 105               Assert( !options::cbqiAll() );
 106             }
 107           }
 108         }
 109       }
 110
 111       //compute dependencies between quantified formulas
 112       if( options::cbqiLitDepend() || options::cbqiInnermost() ){
 113         std::vector< Node > ics;
 114         TermDb::computeVarContains( q, ics );
 115         d_parent_quant[q].clear();
 116         d_children_quant[q].clear();
 117         std::vector< Node > dep;
 118         for( unsigned i=0; i<ics.size(); i++ ){
 119           Node qi = ics[i].getAttribute(InstConstantAttribute());
 120           if( std::find( d_parent_quant[q].begin(), d_parent_quant[q].end(), qi )==d_parent_quant[q].end() ){
 121             d_parent_quant[q].push_back( qi );
 122             d_children_quant[qi].push_back( q );
 123             Node qicel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( qi );
 124             dep.push_back( qi );
 125             dep.push_back( qicel );
 126           }
 127         }
 128         if( !dep.empty() ){
 129           Node dep_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, ceLit, NodeManager::currentNM()->mkNode( kind::AND, dep ) );
 130           Trace("cbqi-lemma") << "Counterexample dependency lemma : " << dep_lemma << std::endl;
 131           d_quantEngine->getOutputChannel().lemma( dep_lemma );
 132         }
 133       }
 134
 135       //must register all sub-quantifiers of counterexample lemma, register their lemmas
 136       std::vector< Node > quants;
 137       TermDb::computeQuantContains( lem, quants );
 138       for( unsigned i=0; i<quants.size(); i++ ){
 139         if( doCbqi( quants[i] ) ){
 140           registerCbqiLemma( quants[i] );
 141         }
 142         if( options::cbqiNestedQE() ){
 143           //record these as counterexample quantifiers
 144           QAttributes qa;
 145           TermDb::computeQuantAttributes( quants[i], qa );
 146           if( !qa.d_qid_num.isNull() ){
 147             d_id_to_ce_quant[ qa.d_qid_num ] = quants[i];
 148             d_ce_quant_to_id[ quants[i] ] = qa.d_qid_num;
 149             Trace("cbqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl;
 150           }
 151         }
 152       }
 153     }
 154     return true;
 155   }else{
 156     return false;
 157   }
 158 }
 159
 160 void InstStrategyCbqi::reset_round( Theory::Effort effort ) {
 161   d_cbqi_set_quant_inactive = false;
 162   d_incomplete_check = false;
 163   d_active_quant.clear();
 164   //check if any cbqi lemma has not been added yet
 165   for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
 166     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
 167     //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
 168     if( doCbqi( q ) ){
 169       if( registerCbqiLemma( q ) ){
 170         Debug("cbqi-debug") << "Registered cbqi lemma." << std::endl;
 171       //set inactive the quantified formulas whose CE literals are asserted false
 172       }else if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
 173         d_active_quant[q] = true;
 174         Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl;
 175         Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
 176         bool value;
 177         if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
 178           Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl;
 179           if( !value ){
 180             if( d_quantEngine->getValuation().isDecision( cel ) ){
 181               Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
 182             }else{
 183               Trace("cbqi") << "Inactive : " << q << std::endl;
 184               d_quantEngine->getModel()->setQuantifierActive( q, false );
 185               d_cbqi_set_quant_inactive = true;
 186               d_active_quant.erase( q );
 187               d_elim_quants.insert( q );
 188               Trace("cbqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl;
 189               //process from waitlist
 190               while( d_nested_qe_waitlist_proc[q]<d_nested_qe_waitlist_size[q] ){
 191                 int index = d_nested_qe_waitlist_proc[q];
 192                 Assert( index>=0 );
 193                 Assert( index<(int)d_nested_qe_waitlist[q].size() );
 194                 Node nq = d_nested_qe_waitlist[q][index];
 195                 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 );
 196                 Node dqelem = nq.iffNode( nqeqn );
 197                 Trace("cbqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl;
 198                 d_quantEngine->getOutputChannel().lemma( dqelem );
 199                 d_nested_qe_waitlist_proc[q] = index + 1;
 200               }
 201             }
 202           }
 203         }else{
 204           Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl;
 205         }
 206       }
 207     }
 208   }
 209
 210   //refinement: only consider innermost active quantified formulas
 211   if( options::cbqiInnermost() ){
 212     if( !d_children_quant.empty() && !d_active_quant.empty() ){
 213       Trace("cbqi-debug") << "Find non-innermost quantifiers..." << std::endl;
 214       std::vector< Node > ninner;
 215       for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
 216         std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first );
 217         if( itc!=d_children_quant.end() ){
 218           for( unsigned j=0; j<itc->second.size(); j++ ){
 219             if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){
 220               Trace("cbqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl;
 221               ninner.push_back( it->first );
 222               break;
 223             }
 224           }
 225         }
 226       }
 227       Trace("cbqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl;
 228       for( unsigned i=0; i<ninner.size(); i++ ){
 229         Assert( d_active_quant.find( ninner[i] )!=d_active_quant.end() );
 230         d_active_quant.erase( ninner[i] );
 231       }
 232       Assert( !d_active_quant.empty() );
 233       Trace("cbqi-debug") << "...done removing." << std::endl;
 234     }
 235   }
 236
 237   processResetInstantiationRound( effort );
 238 }
 239
 240 void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) {
 241   if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
 242     Assert( !d_quantEngine->inConflict() );
 243     double clSet = 0;
 244     if( Trace.isOn("cbqi-engine") ){
 245       clSet = double(clock())/double(CLOCKS_PER_SEC);
 246       Trace("cbqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl;
 247     }
 248     unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
 249     for( int ee=0; ee<=1; ee++ ){
 250       //for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
 251       //  Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
 252       //  if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
 253       for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
 254         Node q = it->first;
 255         Trace("cbqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl;
 256         if( d_nested_qe.find( q )==d_nested_qe.end() ){
 257           process( q, e, ee );
 258           if( d_quantEngine->inConflict() ){
 259             break;
 260           }
 261         }else{
 262           Trace("cbqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl;
 263           Assert( false );
 264         }
 265       }
 266       if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
 267         break;
 268       }
 269     }
 270     if( Trace.isOn("cbqi-engine") ){
 271       if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
 272         Trace("cbqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
 273       }
 274       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
 275       Trace("cbqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl;
 276     }
 277   }
 278 }
 279
 280 bool InstStrategyCbqi::checkComplete() {
 281   if( ( !options::cbqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){
 282     return false;
 283   }else{
 284     return true;
 285   }
 286 }
 287
 288 bool InstStrategyCbqi::checkCompleteFor( Node q ) {
 289   std::map< Node, int >::iterator it = d_do_cbqi.find( q );
 290   if( it!=d_do_cbqi.end() ){
 291     return it->second>0;
 292   }else{
 293     return false;
 294   }
 295 }
 296
 297 Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited ){
 298   std::map< Node, Node >::iterator it = visited.find( n );
 299   if( it==visited.end() ){
 300     Node ret = n;
 301     if( n.getKind()==FORALL ){
 302       QAttributes qa;
 303       TermDb::computeQuantAttributes( n, qa );
 304       if( qa.d_qid_num.isNull() ){
 305         std::vector< Node > rc;
 306         rc.push_back( n[0] );
 307         rc.push_back( getIdMarkedQuantNode( n[1], visited ) );
 308         Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() );
 309         QuantIdNumAttribute ida;
 310         avar.setAttribute(ida,d_qid_count);
 311         d_qid_count++;
 312         std::vector< Node > iplc;
 313         iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) );
 314         if( n.getNumChildren()==3 ){
 315           for( unsigned i=0; i<n[2].getNumChildren(); i++ ){
 316             iplc.push_back( n[2][i] );
 317           }
 318         }
 319         rc.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, iplc ) );
 320         ret = NodeManager::currentNM()->mkNode( FORALL, rc );
 321       }
 322     }else if( n.getNumChildren()>0 ){
 323       std::vector< Node > children;
 324       if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
 325         children.push_back( n.getOperator() );
 326       }
 327       bool childChanged = false;
 328       for( unsigned i=0; i<n.getNumChildren(); i++ ){
 329         Node nc = getIdMarkedQuantNode( n[i], visited );
 330         childChanged = childChanged || nc!=n[i];
 331         children.push_back( nc );
 332       }
 333       if( childChanged ){
 334         ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
 335       }
 336     }
 337     visited[n] = ret;
 338     return ret;
 339   }else{
 340     return it->second;
 341   }
 342 }
 343
 344 void InstStrategyCbqi::preRegisterQuantifier( Node q ) {
 345   if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
 346     if( d_do_cbqi[q]==2 ){
 347       //take full ownership of the quantified formula
 348       d_quantEngine->setOwner( q, this );
 349
 350       //mark all nested quantifiers with id
 351       if( options::cbqiNestedQE() ){
 352         std::map< Node, Node > visited;
 353         Node mq = getIdMarkedQuantNode( q[1], visited );
 354         if( mq!=q[1] ){
 355           //do not do cbqi
 356           d_do_cbqi[q] = false;
 357           //instead do reduction
 358           std::vector< Node > qqc;
 359           qqc.push_back( q[0] );
 360           qqc.push_back( mq );
 361           if( q.getNumChildren()==3 ){
 362             qqc.push_back( q[2] );
 363           }
 364           Node qq = NodeManager::currentNM()->mkNode( FORALL, qqc );
 365           Node mlem = NodeManager::currentNM()->mkNode( IMPLIES, q, qq );
 366           Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl;
 367           d_quantEngine->getOutputChannel().lemma( mlem );
 368         }
 369       }
 370     }
 371   }
 372 }
 373
 374 void InstStrategyCbqi::registerQuantifier( Node q ) {
 375
 376 }
 377
 378 Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts ) {
 379   // there is a nested quantified formula (forall y. nq[y,x]) such that
 380   //    q is (forall y. nq[y,t]) for ground terms t,
 381   //    ceq is (forall y. nq[y,e]) for CE variables e.
 382   // we call this function when we know (forall y. nq[y,e]) is equivalent to quantifier-free formula C[e].
 383   // in this case, q is equivalent to the quantifier-free formula C[t].
 384   if( d_nested_qe.find( ceq )==d_nested_qe.end() ){
 385     d_nested_qe[ceq] = d_quantEngine->getInstantiatedConjunction( ceq );
 386     Trace("cbqi-nqe") << "CE quantifier elimination : " << std::endl;
 387     Trace("cbqi-nqe") << "  " << ceq << std::endl;
 388     Trace("cbqi-nqe") << "  " << d_nested_qe[ceq] << std::endl;
 389     //should not contain quantifiers
 390     Assert( !QuantifiersRewriter::containsQuantifiers( d_nested_qe[ceq] ) );
 391   }
 392   Assert( d_quantEngine->getTermDatabase()->d_inst_constants[q].size()==inst_terms.size() );
 393   //replace inst constants with instantiation
 394   Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermDatabase()->d_inst_constants[q].begin(),
 395                                           d_quantEngine->getTermDatabase()->d_inst_constants[q].end(),
 396                                           inst_terms.begin(), inst_terms.end() );
 397   if( doVts ){
 398     //do virtual term substitution
 399     ret = Rewriter::rewrite( ret );
 400     ret = d_quantEngine->getTermDatabase()->rewriteVtsSymbols( ret );
 401   }
 402   Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl;
 403   Trace("cbqi-nqe") << "  " << n << std::endl;
 404   Trace("cbqi-nqe") << "  " << ret << std::endl;
 405   return ret;
 406 }
 407
 408 Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts ) {
 409   if( visited.find( n )==visited.end() ){
 410     Node ret = n;
 411     if( n.getKind()==FORALL ){
 412       QAttributes qa;
 413       TermDb::computeQuantAttributes( n, qa );
 414       if( !qa.d_qid_num.isNull() ){
 415         //if it has an id, check whether we have done quantifier elimination for this id
 416         std::map< Node, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num );
 417         if( it!=d_id_to_ce_quant.end() ){
 418           Node ceq = it->second;
 419           bool doNestedQe = d_elim_quants.contains( ceq );
 420           if( doNestedQe ){
 421             ret = doNestedQENode( q, ceq, n, inst_terms, doVts );
 422           }else{
 423             Trace("cbqi-nqe") << "Add to nested qe waitlist : " << std::endl;
 424             Node nr = Rewriter::rewrite( n );
 425             Trace("cbqi-nqe") << "  " << ceq << std::endl;
 426             Trace("cbqi-nqe") << "  " << nr << std::endl;
 427             int wlsize = d_nested_qe_waitlist_size[ceq] + 1;
 428             d_nested_qe_waitlist_size[ceq] = wlsize;
 429             if( wlsize<(int)d_nested_qe_waitlist[ceq].size() ){
 430               d_nested_qe_waitlist[ceq][wlsize] = nr;
 431             }else{
 432               d_nested_qe_waitlist[ceq].push_back( nr );
 433             }
 434             d_nested_qe_info[nr].d_q = q;
 435             d_nested_qe_info[nr].d_inst_terms.clear();
 436             d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() );
 437             d_nested_qe_info[nr].d_doVts = doVts;
 438             //TODO: ensure this holds by restricting prenex when cbqiNestedQe is true.
 439             Assert( !options::cbqiInnermost() );
 440           }
 441         }
 442       }
 443     }else if( n.getNumChildren()>0 ){
 444       std::vector< Node > children;
 445       if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
 446         children.push_back( n.getOperator() );
 447       }
 448       bool childChanged = false;
 449       for( unsigned i=0; i<n.getNumChildren(); i++ ){
 450         Node nc = doNestedQERec( q, n[i], visited, inst_terms, doVts );
 451         childChanged = childChanged || nc!=n[i];
 452         children.push_back( nc );
 453       }
 454       if( childChanged ){
 455         ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
 456       }
 457     }
 458     visited[n] = ret;
 459     return ret;
 460   }else{
 461     return n;
 462   }
 463 }
 464
 465 Node InstStrategyCbqi::doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts ) {
 466   std::map< Node, Node > visited;
 467   return doNestedQERec( q, lem, visited, inst_terms, doVts );
 468 }
 469
 470 void InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){
 471   Trace("cbqi-debug") << "Counterexample lemma  : " << lem << std::endl;
 472   d_quantEngine->addLemma( lem, false );
 473 }
 474
 475 bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ){
 476   if( visited.find( n )==visited.end() ){
 477     visited[n] = true;
 478     if( n.getKind()!=BOUND_VARIABLE && TermDb::hasBoundVarAttr( n ) ){
 479       if( !inst::Trigger::isCbqiKind( n.getKind() ) ){
 480         Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n  << std::endl;
 481         return true;
 482       }else if( n.getKind()==MULT && ( n.getNumChildren()!=2 || !n[0].isConst() ) ){
 483         Trace("cbqi-debug2") << "Non-linear arithmetic : " << n << std::endl;
 484         return true;
 485       }else if( n.getKind()==FORALL ){
 486         return hasNonCbqiOperator( n[1], visited );
 487       }else{
 488         for( unsigned i=0; i<n.getNumChildren(); i++ ){
 489           if( hasNonCbqiOperator( n[i], visited ) ){
 490             return true;
 491           }
 492         }
 493       }
 494     }
 495   }
 496   return false;
 497 }
 498 int InstStrategyCbqi::hasNonCbqiVariable( Node q ){
 499   int hmin = 1;
 500   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
 501     TypeNode tn = q[0][i].getType();
 502     int handled = -1;
 503     if( tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector() ){
 504       handled = 0;
 505     }else if( tn.isDatatype() ){
 506       handled = 0;
 507     }else if( tn.isSort() ){
 508       QuantEPR * qepr = d_quantEngine->getQuantEPR();
 509       if( qepr!=NULL ){
 510         handled = qepr->isEPR( tn ) ? 1 : -1;
 511       }
 512     }
 513     if( handled==-1 ){
 514       return -1;
 515     }else if( handled<hmin ){
 516       hmin = handled;
 517     }
 518   }
 519   return hmin;
 520 }
 521
 522 bool InstStrategyCbqi::doCbqi( Node q ){
 523   std::map< Node, int >::iterator it = d_do_cbqi.find( q );
 524   if( it==d_do_cbqi.end() ){
 525     int ret = 2;
 526     if( !d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){
 527       //if has an instantiation pattern, don't do it
 528       if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
 529         for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
 530           if( q[2][i].getKind()==INST_PATTERN ){
 531             ret = 0;
 532           }
 533         }
 534       }
 535       if( ret!=0 ){
 536         //if quantifier has a non-handled variable, then do not use cbqi
 537         //if quantifier has an APPLY_UF term, then do not use cbqi unless EPR
 538         int ncbqiv = hasNonCbqiVariable( q );
 539         if( ncbqiv==0 || ncbqiv==1 ){
 540           std::map< Node, bool > visited;
 541           if( hasNonCbqiOperator( q[1], visited ) ){
 542             if( ncbqiv==1 ){
 543               //all variables are fully handled, this implies this will be handlable regardless of body (e.g. for EPR)
 544               //  so, try but not exclusively
 545               ret = 1;
 546             }else{
 547               //cannot be handled
 548               ret = 0;
 549             }
 550           }
 551         }else{
 552           // unhandled variable type
 553           ret = 0;
 554         }
 555         if( ret==0 && options::cbqiAll() ){
 556           //try but not exclusively
 557           ret = 1;
 558         }
 559       }
 560     }
 561     Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
 562     d_do_cbqi[q] = ret;
 563     return ret!=0;
 564   }else{
 565     return it->second!=0;
 566   }
 567 }
 568
 569 Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ) {
 570   if( proc.find( q )==proc.end() ){
 571     proc[q] = true;
 572     //first check children
 573     std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( q );
 574     if( itc!=d_children_quant.end() ){
 575       for( unsigned j=0; j<itc->second.size(); j++ ){
 576         Node d = getNextDecisionRequestProc( itc->second[j], proc );
 577         if( !d.isNull() ){
 578           return d;
 579         }
 580       }
 581     }
 582     //then check self
 583     if( hasAddedCbqiLemma( q ) ){
 584       Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
 585       bool value;
 586       if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){
 587         Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl;
 588         return cel;
 589       }
 590     }
 591   }
 592   return Node::null();
 593 }
 594
 595 Node InstStrategyCbqi::getNextDecisionRequest( unsigned& priority ){
 596   std::map< Node, bool > proc;
 597   for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
 598     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
 599     Node d = getNextDecisionRequestProc( q, proc );
 600     if( !d.isNull() ){
 601       priority = 0;
 602       return d;
 603     }
 604   }
 605   return Node::null();
 606 }
 607
 608
 609
 610 //new implementation
 611
 612 bool CegqiOutputInstStrategy::doAddInstantiation( std::vector< Node >& subs ) {
 613   return d_out->doAddInstantiation( subs );
 614 }
 615
 616 bool CegqiOutputInstStrategy::isEligibleForInstantiation( Node n ) {
 617   return d_out->isEligibleForInstantiation( n );
 618 }
 619
 620 bool CegqiOutputInstStrategy::addLemma( Node lem ) {
 621   return d_out->addLemma( lem );
 622 }
 623
 624
 625 InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe )
 626   : InstStrategyCbqi( qe ) {
 627   d_out = new CegqiOutputInstStrategy( this );
 628   d_small_const = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) );
 629   d_check_vts_lemma_lc = false;
 630 }
 631
 632 InstStrategyCegqi::~InstStrategyCegqi() throw () {
 633   delete d_out;
 634
 635   for(std::map< Node, CegInstantiator * >::iterator i = d_cinst.begin(),
 636           iend = d_cinst.end(); i != iend; ++i) {
 637     CegInstantiator * instantiator = (*i).second;
 638     delete instantiator;
 639   }
 640   d_cinst.clear();
 641 }
 642
 643 void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) {
 644   d_check_vts_lemma_lc = false;
 645 }
 646
 647 void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
 648   if( e==0 ){
 649     CegInstantiator * cinst = getInstantiator( q );
 650     Trace("inst-alg") << "-> Run cegqi for " << q << std::endl;
 651     d_curr_quant = q;
 652     if( !cinst->check() ){
 653       d_incomplete_check = true;
 654       d_check_vts_lemma_lc = true;
 655     }
 656     d_curr_quant = Node::null();
 657   }else if( e==1 ){
 658     //minimize the free delta heuristically on demand
 659     if( d_check_vts_lemma_lc ){
 660       Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl;
 661       d_check_vts_lemma_lc = false;
 662       d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const );
 663       d_small_const = Rewriter::rewrite( d_small_const );
 664       //heuristic for now, until we know how to do nested quantification
 665       Node delta = d_quantEngine->getTermDatabase()->getVtsDelta( true, false );
 666       if( !delta.isNull() ){
 667         Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl;
 668         Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const );
 669         d_quantEngine->getOutputChannel().lemma( delta_lem_ub );
 670       }
 671       std::vector< Node > inf;
 672       d_quantEngine->getTermDatabase()->getVtsTerms( inf, true, false, false );
 673       for( unsigned i=0; i<inf.size(); i++ ){
 674         Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
 675         Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) );
 676         d_quantEngine->getOutputChannel().lemma( inf_lem_lb );
 677       }
 678     }
 679   }
 680 }
 681
 682 bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
 683   Assert( !d_curr_quant.isNull() );
 684   //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
 685   if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( d_curr_quant ) ){
 686     d_cbqi_set_quant_inactive = true;
 687     d_incomplete_check = true;
 688     d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false );
 689     return true;
 690   }else{
 691     //check if we need virtual term substitution (if used delta or infinity)
 692     bool used_vts = d_quantEngine->getTermDatabase()->containsVtsTerm( subs, false );
 693     if( d_quantEngine->addInstantiation( d_curr_quant, subs, false, false, used_vts ) ){
 694       ++(d_quantEngine->d_statistics.d_instantiations_cbqi);
 695       //d_added_inst.insert( d_curr_quant );
 696       return true;
 697     }else{
 698       //this should never happen for monotonic selection strategies
 699       Trace("cbqi-warn") << "WARNING: Existing instantiation" << std::endl;
 700       Assert( !options::cbqiNestedQE() || options::cbqiAll() );
 701       return false;
 702     }
 703   }
 704 }
 705
 706 bool InstStrategyCegqi::addLemma( Node lem ) {
 707   return d_quantEngine->addLemma( lem );
 708 }
 709
 710 bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) {
 711   if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){
 712     if( n.getKind()==SKOLEM && d_quantEngine->getTermDatabase()->containsVtsTerm( n ) ){
 713       return true;
 714     }else{
 715       TypeNode tn = n.getType();
 716       if( tn.isSort() ){
 717         QuantEPR * qepr = d_quantEngine->getQuantEPR();
 718         if( qepr!=NULL ){
 719           //legal if in the finite set of constants of type tn
 720           if( qepr->isEPRConstant( tn, n ) ){
 721             return true;
 722           }
 723         }
 724       }
 725       //only legal if current quantified formula contains n
 726       return TermDb::containsTerm( d_curr_quant, n );
 727     }
 728   }else{
 729     return true;
 730   }
 731 }
 732
 733 CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
 734   std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( q );
 735   if( it==d_cinst.end() ){
 736     CegInstantiator * cinst = new CegInstantiator( d_quantEngine, d_out, true, true );
 737     d_cinst[q] = cinst;
 738     return cinst;
 739   }else{
 740    return it->second;
 741   }
 742 }
 743
 744 void InstStrategyCegqi::registerQuantifier( Node q ) {
 745   if( options::cbqiPreRegInst() ){
 746     if( doCbqi( q ) ){
 747       //just get the instantiator
 748       getInstantiator( q );
 749     }
 750   }
 751 }
 752
 753 void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) {
 754   //must register with the instantiator
 755   //must explicitly remove ITEs so that we record dependencies
 756   std::vector< Node > ce_vars;
 757   for( unsigned i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( q ); i++ ){
 758     ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) );
 759   }
 760   std::vector< Node > lems;
 761   lems.push_back( lem );
 762   CegInstantiator * cinst = getInstantiator( q );
 763   cinst->registerCounterexampleLemma( lems, ce_vars );
 764   for( unsigned i=0; i<lems.size(); i++ ){
 765     Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i] << std::endl;
 766     d_quantEngine->addLemma( lems[i], false );
 767   }
 768 }
 769
 770 void InstStrategyCegqi::presolve() {
 771   if( options::cbqiPreRegInst() ){
 772     for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){
 773       Trace("cbqi-presolve") << "Presolve " << it->first << std::endl;
 774       it->second->presolve( it->first );
 775     }
 776   }
 777 }
 778