src/theory/quantifiers_engine.cpp

   1 /*********************                                                        */
   2 /*! \file quantifiers_engine.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Tim King, Morgan Deters
   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 quantifiers engine class
  13  **/
  14
  15 #include "theory/quantifiers_engine.h"
  16
  17 #include "options/quantifiers_options.h"
  18 #include "options/uf_options.h"
  19 #include "smt/smt_statistics_registry.h"
  20 #include "theory/arrays/theory_arrays.h"
  21 #include "theory/datatypes/theory_datatypes.h"
  22 #include "theory/sep/theory_sep.h"
  23 #include "theory/quantifiers/alpha_equivalence.h"
  24 #include "theory/quantifiers/ambqi_builder.h"
  25 #include "theory/quantifiers/bounded_integers.h"
  26 #include "theory/quantifiers/ce_guided_instantiation.h"
  27 #include "theory/quantifiers/conjecture_generator.h"
  28 #include "theory/quantifiers/first_order_model.h"
  29 #include "theory/quantifiers/full_model_check.h"
  30 #include "theory/quantifiers/fun_def_engine.h"
  31 #include "theory/quantifiers/inst_strategy_cbqi.h"
  32 #include "theory/quantifiers/inst_strategy_e_matching.h"
  33 #include "theory/quantifiers/instantiation_engine.h"
  34 #include "theory/quantifiers/local_theory_ext.h"
  35 #include "theory/quantifiers/model_engine.h"
  36 #include "theory/quantifiers/quant_conflict_find.h"
  37 #include "theory/quantifiers/quant_equality_engine.h"
  38 #include "theory/quantifiers/quantifiers_rewriter.h"
  39 #include "theory/quantifiers/relevant_domain.h"
  40 #include "theory/quantifiers/rewrite_engine.h"
  41 #include "theory/quantifiers/term_database.h"
  42 #include "theory/quantifiers/trigger.h"
  43 #include "theory/quantifiers/quant_split.h"
  44 #include "theory/quantifiers/anti_skolem.h"
  45 #include "theory/quantifiers/equality_infer.h"
  46 #include "theory/quantifiers/inst_propagator.h"
  47 #include "theory/theory_engine.h"
  48 #include "theory/uf/equality_engine.h"
  49 #include "theory/uf/theory_uf.h"
  50 #include "theory/uf/theory_uf_strong_solver.h"
  51
  52 using namespace std;
  53 using namespace CVC4;
  54 using namespace CVC4::kind;
  55 using namespace CVC4::context;
  56 using namespace CVC4::theory;
  57 using namespace CVC4::theory::inst;
  58
  59 QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
  60     d_te( te ),
  61     d_conflict_c(c, false),
  62     //d_quants(u),
  63     d_quants_red(u),
  64     d_lemmas_produced_c(u),
  65     d_skolemized(u),
  66     d_ierCounter_c(c),
  67     //d_ierCounter(c),
  68     //d_ierCounter_lc(c),
  69     //d_ierCounterLastLc(c),
  70     d_presolve(u, true),
  71     d_presolve_in(u),
  72     d_presolve_cache(u),
  73     d_presolve_cache_wq(u),
  74     d_presolve_cache_wic(u){
  75   //utilities
  76   d_eq_query = new EqualityQueryQuantifiersEngine( c, this );
  77   d_util.push_back( d_eq_query );
  78
  79   d_term_db = new quantifiers::TermDb( c, u, this );
  80   d_util.push_back( d_term_db );
  81
  82   if( options::instPropagate() ){
  83     d_inst_prop = new quantifiers::InstPropagator( this );
  84     d_util.push_back( d_inst_prop );
  85     d_inst_notify.push_back( d_inst_prop->getInstantiationNotify() );
  86   }else{
  87     d_inst_prop = NULL;
  88   }
  89
  90   d_tr_trie = new inst::TriggerTrie;
  91   d_curr_effort_level = QEFFORT_NONE;
  92   d_conflict = false;
  93   d_hasAddedLemma = false;
  94   //don't add true lemma
  95   d_lemmas_produced_c[d_term_db->d_true] = true;
  96
  97   Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
  98   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
  99
 100   //the model object
 101   if( options::mbqiMode()==quantifiers::MBQI_FMC ||
 102       options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBound() ||
 103       options::mbqiMode()==quantifiers::MBQI_TRUST ){
 104     d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
 105   }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
 106     d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" );
 107   }else{
 108     d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
 109   }
 110   if( options::relevantTriggers() ){
 111     d_quant_rel = new QuantRelevance( false );
 112   }else{
 113     d_quant_rel = NULL;
 114   }
 115
 116   if( options::quantEpr() ){
 117     Assert( !options::incrementalSolving() );
 118     d_qepr = new QuantEPR;
 119   }else{
 120     d_qepr = NULL;
 121   }
 122
 123
 124   d_qcf = NULL;
 125   d_sg_gen = NULL;
 126   d_inst_engine = NULL;
 127   d_i_cbqi = NULL;
 128   d_qsplit = NULL;
 129   d_anti_skolem = NULL;
 130   d_model_engine = NULL;
 131   d_bint = NULL;
 132   d_rr_engine = NULL;
 133   d_ceg_inst = NULL;
 134   d_lte_part_inst = NULL;
 135   d_alpha_equiv = NULL;
 136   d_fun_def_engine = NULL;
 137   d_uee = NULL;
 138   d_fs = NULL;
 139   d_rel_dom = NULL;
 140   d_builder = NULL;
 141
 142   d_total_inst_count_debug = 0;
 143   //allow theory combination to go first, once initially
 144   d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
 145   d_ierCounter_c = d_ierCounter;
 146   d_ierCounter_lc = 0;
 147   d_ierCounterLastLc = 0;
 148   d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
 149 }
 150
 151 QuantifiersEngine::~QuantifiersEngine(){
 152   for(std::map< Node, inst::CDInstMatchTrie* >::iterator
 153       i = d_c_inst_match_trie.begin(), iend = d_c_inst_match_trie.end();
 154       i != iend; ++i)
 155   {
 156     delete (*i).second;
 157   }
 158   d_c_inst_match_trie.clear();
 159
 160   delete d_alpha_equiv;
 161   delete d_builder;
 162   delete d_qepr;
 163   delete d_rr_engine;
 164   delete d_bint;
 165   delete d_model_engine;
 166   delete d_inst_engine;
 167   delete d_qcf;
 168   delete d_quant_rel;
 169   delete d_rel_dom;
 170   delete d_model;
 171   delete d_tr_trie;
 172   delete d_term_db;
 173   delete d_eq_query;
 174   delete d_sg_gen;
 175   delete d_ceg_inst;
 176   delete d_lte_part_inst;
 177   delete d_fun_def_engine;
 178   delete d_uee;
 179   delete d_fs;
 180   delete d_i_cbqi;
 181   delete d_qsplit;
 182   delete d_anti_skolem;
 183   delete d_inst_prop;
 184 }
 185
 186 EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
 187   return d_eq_query;
 188 }
 189
 190 context::Context* QuantifiersEngine::getSatContext(){
 191   return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext();
 192 }
 193
 194 context::UserContext* QuantifiersEngine::getUserContext(){
 195   return d_te->theoryOf( THEORY_QUANTIFIERS )->getUserContext();
 196 }
 197
 198 OutputChannel& QuantifiersEngine::getOutputChannel(){
 199   return d_te->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel();
 200 }
 201 /** get default valuation for the quantifiers engine */
 202 Valuation& QuantifiersEngine::getValuation(){
 203   return d_te->theoryOf( THEORY_QUANTIFIERS )->getValuation();
 204 }
 205
 206 void QuantifiersEngine::finishInit(){
 207   context::Context * c = getSatContext();
 208   Trace("quant-engine-debug") << "QuantifiersEngine : finishInit " << std::endl;
 209   bool needsBuilder = false;
 210   bool needsRelDom = false;
 211   //add quantifiers modules
 212   if( options::quantConflictFind() || options::quantRewriteRules() ){
 213     d_qcf = new quantifiers::QuantConflictFind( this, c);
 214     d_modules.push_back( d_qcf );
 215   }
 216   if( options::conjectureGen() ){
 217     d_sg_gen = new quantifiers::ConjectureGenerator( this, c );
 218     d_modules.push_back( d_sg_gen );
 219   }
 220   if( !options::finiteModelFind() || options::fmfInstEngine() ){
 221     d_inst_engine = new quantifiers::InstantiationEngine( this );
 222     d_modules.push_back(  d_inst_engine );
 223   }
 224   if( options::cbqi() ){
 225     d_i_cbqi = new quantifiers::InstStrategyCegqi( this );
 226     d_modules.push_back( d_i_cbqi );
 227     if( options::cbqiModel() ){
 228       needsBuilder = true;
 229     }
 230   }
 231   if( options::ceGuidedInst() ){
 232     d_ceg_inst = new quantifiers::CegInstantiation( this, c );
 233     d_modules.push_back( d_ceg_inst );
 234     needsBuilder = true;
 235   }
 236   //finite model finding
 237   if( options::finiteModelFind() ){
 238     if( options::fmfBound() ){
 239       d_bint = new quantifiers::BoundedIntegers( c, this );
 240       d_modules.push_back( d_bint );
 241     }
 242     d_model_engine = new quantifiers::ModelEngine( c, this );
 243     d_modules.push_back( d_model_engine );
 244     needsBuilder = true;
 245   }
 246   if( options::quantRewriteRules() ){
 247     d_rr_engine = new quantifiers::RewriteEngine( c, this );
 248     d_modules.push_back(d_rr_engine);
 249   }
 250   if( options::ltePartialInst() ){
 251     d_lte_part_inst = new quantifiers::LtePartialInst( this, c );
 252     d_modules.push_back( d_lte_part_inst );
 253   }
 254   if( ( options::finiteModelFind() && options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ) ||
 255       options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
 256     d_qsplit = new quantifiers::QuantDSplit( this, c );
 257     d_modules.push_back( d_qsplit );
 258   }
 259   if( options::quantAntiSkolem() ){
 260     d_anti_skolem = new quantifiers::QuantAntiSkolem( this );
 261     d_modules.push_back( d_anti_skolem );
 262   }
 263   if( options::quantAlphaEquiv() ){
 264     d_alpha_equiv = new quantifiers::AlphaEquivalence( this );
 265   }
 266   //if( options::funDefs() ){
 267   //  d_fun_def_engine = new quantifiers::FunDefEngine( this, c );
 268   //  d_modules.push_back( d_fun_def_engine );
 269   //}
 270   if( options::quantEqualityEngine() ){
 271     d_uee = new quantifiers::QuantEqualityEngine( this, c );
 272     d_modules.push_back( d_uee );
 273   }
 274   //full saturation : instantiate from relevant domain, then arbitrary terms
 275   if( options::fullSaturateQuant() || options::fullSaturateInst() ){
 276     d_fs = new quantifiers::FullSaturation( this );
 277     d_modules.push_back( d_fs );
 278     needsRelDom = true;
 279   }
 280
 281   if( needsRelDom ){
 282     d_rel_dom = new quantifiers::RelevantDomain( this, d_model );
 283     d_util.push_back( d_rel_dom );
 284   }
 285
 286   if( needsBuilder ){
 287     Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl;
 288     if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ||
 289         options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBound() ){
 290       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
 291       d_builder = new quantifiers::fmcheck::FullModelChecker( c, this );
 292     }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
 293       Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl;
 294       d_builder = new quantifiers::AbsMbqiBuilder( c, this );
 295     }else{
 296       Trace("quant-engine-debug") << "...make default model builder." << std::endl;
 297       d_builder = new quantifiers::QModelBuilderDefault( c, this );
 298     }
 299   }
 300
 301 }
 302
 303 QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
 304   std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q );
 305   if( it==d_owner.end() ){
 306     return NULL;
 307   }else{
 308     return it->second;
 309   }
 310 }
 311
 312 void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m, int priority ) {
 313   QuantifiersModule * mo = getOwner( q );
 314   if( mo!=m ){
 315     if( mo!=NULL ){
 316       if( priority<=d_owner_priority[q] ){
 317         Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << " with higher priority!" << std::endl;
 318         return;
 319       }
 320     }
 321     d_owner[q] = m;
 322     d_owner_priority[q] = priority;
 323   }
 324 }
 325
 326 bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
 327   QuantifiersModule * mo = getOwner( q );
 328   return mo==m || mo==NULL;
 329 }
 330
 331 void QuantifiersEngine::presolve() {
 332   Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
 333   for( unsigned i=0; i<d_modules.size(); i++ ){
 334     d_modules[i]->presolve();
 335   }
 336   d_term_db->presolve();
 337   d_presolve = false;
 338   //add all terms to database
 339   if( options::incrementalSolving() ){
 340     Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache.size() << std::endl;
 341     for( unsigned i=0; i<d_presolve_cache.size(); i++ ){
 342       addTermToDatabase( d_presolve_cache[i], d_presolve_cache_wq[i], d_presolve_cache_wic[i] );
 343     }
 344     Trace("quant-engine-proc") << "Done add presolve cache " << std::endl;
 345   }
 346 }
 347
 348 void QuantifiersEngine::ppNotifyAssertions( std::vector< Node >& assertions ) {
 349   Trace("quant-engine-proc") << "ppNotifyAssertions in QE, #assertions = " << assertions.size() << " check epr = " << (d_qepr!=NULL) << std::endl;
 350   if( ( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ) || d_qepr!=NULL ){
 351     for( unsigned i=0; i<assertions.size(); i++ ) {
 352       if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){
 353         setInstantiationLevelAttr( assertions[i], 0 );
 354       }
 355       if( d_qepr!=NULL ){
 356         d_qepr->registerAssertion( assertions[i] );
 357       }
 358     }
 359     if( d_qepr!=NULL ){
 360       //must handle sources of other new constants e.g. separation logic
 361       //FIXME: cleanup
 362       ((sep::TheorySep*)getTheoryEngine()->theoryOf( THEORY_SEP ))->initializeBounds();
 363       d_qepr->finishInit();
 364     }
 365   }
 366 }
 367
 368 void QuantifiersEngine::check( Theory::Effort e ){
 369   CodeTimer codeTimer(d_statistics.d_time);
 370   if( !getMasterEqualityEngine()->consistent() ){
 371     Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
 372     return;
 373   }
 374   bool needsCheck = !d_lemmas_waiting.empty();
 375   unsigned needsModelE = QEFFORT_NONE;
 376   std::vector< QuantifiersModule* > qm;
 377   if( d_model->checkNeeded() ){
 378     needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
 379     for( unsigned i=0; i<d_modules.size(); i++ ){
 380       if( d_modules[i]->needsCheck( e ) ){
 381         qm.push_back( d_modules[i] );
 382         needsCheck = true;
 383         //can only request model at last call since theory combination can find inconsistencies
 384         if( e>=Theory::EFFORT_LAST_CALL ){
 385           unsigned me = d_modules[i]->needsModel( e );
 386           needsModelE = me<needsModelE ? me : needsModelE;
 387         }
 388       }
 389     }
 390   }
 391
 392   d_conflict = false;
 393   d_hasAddedLemma = false;
 394   bool setIncomplete = false;
 395   bool usedModelBuilder = false;
 396
 397   Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
 398   if( needsCheck ){
 399     //this will fail if a set of instances is marked as a conflict, but is not
 400     Assert( !d_conflict_c.get() );
 401     //flush previous lemmas (for instance, if was interupted), or other lemmas to process
 402     flushLemmas();
 403     if( d_hasAddedLemma ){
 404       return;
 405     }
 406     if( !d_recorded_inst.empty() ){
 407       Trace("quant-engine-debug") << "Removing " << d_recorded_inst.size() << " instantiations..." << std::endl;
 408       //remove explicitly recorded instantiations
 409       for( unsigned i=0; i<d_recorded_inst.size(); i++ ){
 410         removeInstantiationInternal( d_recorded_inst[i].first, d_recorded_inst[i].second );
 411       }
 412       d_recorded_inst.clear();
 413     }
 414
 415     double clSet = 0;
 416     if( Trace.isOn("quant-engine") ){
 417       clSet = double(clock())/double(CLOCKS_PER_SEC);
 418       Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e << " <<<<<" << std::endl;
 419     }
 420
 421     if( Trace.isOn("quant-engine-debug") ){
 422       Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
 423       Trace("quant-engine-debug") << "  depth : " << d_ierCounter_c << std::endl;
 424       Trace("quant-engine-debug") << "  modules to check : ";
 425       for( unsigned i=0; i<qm.size(); i++ ){
 426         Trace("quant-engine-debug") << qm[i]->identify() << " ";
 427       }
 428       Trace("quant-engine-debug") << std::endl;
 429       Trace("quant-engine-debug") << "  # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
 430       if( !d_lemmas_waiting.empty() ){
 431         Trace("quant-engine-debug") << "  lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
 432       }
 433       Trace("quant-engine-debug") << "  Theory engine finished : " << !d_te->needCheck() << std::endl;
 434       Trace("quant-engine-debug") << "  Needs model effort : " << needsModelE << std::endl;
 435     }
 436     if( Trace.isOn("quant-engine-ee-pre") ){
 437       Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
 438       debugPrintEqualityEngine( "quant-engine-ee-pre" );
 439     }
 440     if( Trace.isOn("quant-engine-assert") ){
 441       Trace("quant-engine-assert") << "Assertions : " << std::endl;
 442       getTheoryEngine()->printAssertions("quant-engine-assert");
 443     }
 444
 445     //reset utilities
 446     Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl;
 447     for( unsigned i=0; i<d_util.size(); i++ ){
 448       Trace("quant-engine-debug2") << "Reset " << d_util[i]->identify().c_str() << "..." << std::endl;
 449       if( !d_util[i]->reset( e ) ){
 450         flushLemmas();
 451         if( d_hasAddedLemma ){
 452           return;
 453         }else{
 454           //should only fail reset if added a lemma
 455           Assert( false );
 456         }
 457       }
 458     }
 459
 460     if( Trace.isOn("quant-engine-ee") ){
 461       Trace("quant-engine-ee") << "Equality engine : " << std::endl;
 462       debugPrintEqualityEngine( "quant-engine-ee" );
 463     }
 464
 465     //reset the model
 466     Trace("quant-engine-debug") << "Reset model..." << std::endl;
 467     d_model->reset_round();
 468
 469     //reset the modules
 470     Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
 471     for( unsigned i=0; i<d_modules.size(); i++ ){
 472       Trace("quant-engine-debug2") << "Reset " << d_modules[i]->identify().c_str() << std::endl;
 473       d_modules[i]->reset_round( e );
 474     }
 475     Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
 476     //reset may have added lemmas
 477     flushLemmas();
 478     if( d_hasAddedLemma ){
 479       return;
 480     }
 481
 482     if( e==Theory::EFFORT_LAST_CALL ){
 483       //if effort is last call, try to minimize model first
 484       //uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
 485       //if( ufss && !ufss->minimize() ){ return; }
 486       ++(d_statistics.d_instantiation_rounds_lc);
 487     }else if( e==Theory::EFFORT_FULL ){
 488       ++(d_statistics.d_instantiation_rounds);
 489     }
 490     Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
 491     for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_LAST_CALL; quant_e++ ){
 492       d_curr_effort_level = quant_e;
 493       bool success = true;
 494       //build the model if any module requested it
 495       if( needsModelE==quant_e ){
 496         Assert( d_builder!=NULL );
 497         Trace("quant-engine-debug") << "Build model..." << std::endl;
 498         usedModelBuilder = true;
 499         d_builder->d_addedLemmas = 0;
 500         d_builder->buildModel( d_model, false );
 501         //we are done if model building was unsuccessful
 502         if( d_builder->d_addedLemmas>0 ){
 503           success = false;
 504         }
 505       }
 506       if( success ){
 507         //check each module
 508         for( unsigned i=0; i<qm.size(); i++ ){
 509           Trace("quant-engine-debug") << "Check " << qm[i]->identify().c_str() << " at effort " << quant_e << "..." << std::endl;
 510           qm[i]->check( e, quant_e );
 511           if( d_conflict ){
 512             Trace("quant-engine-debug") << "...conflict!" << std::endl;
 513             break;
 514           }
 515         }
 516       }
 517       //flush all current lemmas
 518       flushLemmas();
 519       //if we have added one, stop
 520       if( d_hasAddedLemma ){
 521         break;
 522       }else{
 523         Assert( !d_conflict );
 524         if( quant_e==QEFFORT_CONFLICT ){
 525           if( e==Theory::EFFORT_FULL ){
 526             //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase
 527             if( d_ierCounterLastLc!=d_ierCounter_lc || !options::instWhenStrictInterleave() || d_ierCounter%d_inst_when_phase!=0 ){
 528               d_ierCounter = d_ierCounter + 1;
 529               d_ierCounterLastLc = d_ierCounter_lc;
 530               d_ierCounter_c = d_ierCounter_c.get() + 1;
 531             }
 532           }else if( e==Theory::EFFORT_LAST_CALL ){
 533             d_ierCounter_lc = d_ierCounter_lc + 1;
 534           }
 535         }else if( quant_e==QEFFORT_MODEL ){
 536           if( e==Theory::EFFORT_LAST_CALL ){
 537             //sources of incompleteness
 538             if( !d_recorded_inst.empty() ){
 539               Trace("quant-engine-debug") << "Set incomplete due to recorded instantiations." << std::endl;
 540               setIncomplete = true;
 541             }
 542             //if we have a chance not to set incomplete
 543             if( !setIncomplete ){
 544               setIncomplete = false;
 545               //check if we should set the incomplete flag
 546               for( unsigned i=0; i<d_modules.size(); i++ ){
 547                 if( !d_modules[i]->checkComplete() ){
 548                   Trace("quant-engine-debug") << "Set incomplete because " << d_modules[i]->identify().c_str() << " was incomplete." << std::endl;
 549                   setIncomplete = true;
 550                   break;
 551                 }
 552               }
 553               if( !setIncomplete ){
 554                 //look at individual quantified formulas, one module must claim completeness for each one
 555                 for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
 556                   bool hasCompleteM = false;
 557                   Node q = d_model->getAssertedQuantifier( i );
 558                   QuantifiersModule * qmd = getOwner( q );
 559                   if( qmd!=NULL ){
 560                     hasCompleteM = qmd->checkCompleteFor( q );
 561                   }else{
 562                     for( unsigned j=0; j<d_modules.size(); j++ ){
 563                       if( d_modules[j]->checkCompleteFor( q ) ){
 564                         qmd = d_modules[j];
 565                         hasCompleteM = true;
 566                         break;
 567                       }
 568                     }
 569                   }
 570                   if( !hasCompleteM ){
 571                     Trace("quant-engine-debug") << "Set incomplete because " << q << " was not fully processed." << std::endl;
 572                     setIncomplete = true;
 573                     break;
 574                   }else{
 575                     Assert( qmd!=NULL );
 576                     Trace("quant-engine-debug2") << "Complete for " << q << " due to " << qmd->identify().c_str() << std::endl;
 577                   }
 578                 }
 579               }
 580             }
 581             //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL
 582             if( !setIncomplete ){
 583               break;
 584             }
 585           }
 586         }
 587       }
 588     }
 589     d_curr_effort_level = QEFFORT_NONE;
 590     Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
 591     if( d_hasAddedLemma ){
 592       //debug information
 593       if( Trace.isOn("inst-per-quant-round") ){
 594         for( std::map< Node, int >::iterator it = d_temp_inst_debug.begin(); it != d_temp_inst_debug.end(); ++it ){
 595           Trace("inst-per-quant-round") << " * " << it->second << " for " << it->first << std::endl;
 596           d_temp_inst_debug[it->first] = 0;
 597         }
 598       }
 599     }
 600     if( Trace.isOn("quant-engine") ){
 601       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
 602       Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2-clSet);
 603       Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma;
 604       Trace("quant-engine") << std::endl;
 605     }
 606
 607     Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl;
 608   }else{
 609     Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl;
 610   }
 611
 612   //SAT case
 613   if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
 614     if( options::produceModels() ){
 615       if( usedModelBuilder ){
 616         Trace("quant-engine-debug") << "Build completed model..." << std::endl;
 617         d_builder->buildModel( d_model, true );
 618       }else if( !d_model->isModelSet() ){
 619         //use default model builder when no module built the model
 620         Trace("quant-engine-debug") << "Build the model..." << std::endl;
 621         d_te->getModelBuilder()->buildModel( d_model, true );
 622         Trace("quant-engine-debug") << "Done building the model." << std::endl;
 623       }
 624     }
 625     if( setIncomplete ){
 626       Trace("quant-engine") << "Set incomplete flag." << std::endl;
 627       getOutputChannel().setIncomplete();
 628     }
 629     //output debug stats
 630     if( Trace.isOn("inst-per-quant") ){
 631       for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){
 632         Trace("inst-per-quant") << " * " << it->second << " for " << it->first << std::endl;
 633       }
 634     }
 635   }
 636 }
 637
 638 void QuantifiersEngine::notifyCombineTheories() {
 639   //if allowing theory combination to happen at most once between instantiation rounds
 640   //d_ierCounter = 1;
 641   //d_ierCounterLastLc = -1;
 642 }
 643
 644 bool QuantifiersEngine::reduceQuantifier( Node q ) {
 645   //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants
 646   BoolMap::const_iterator it = d_quants_red.find( q );
 647   if( it==d_quants_red.end() ){
 648     Node lem;
 649     std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q );
 650     if( itr==d_quants_red_lem.end() ){
 651       if( d_alpha_equiv ){
 652         Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
 653         //add equivalence with another quantified formula
 654         lem = d_alpha_equiv->reduceQuantifier( q );
 655         if( !lem.isNull() ){
 656           Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
 657           ++(d_statistics.d_red_alpha_equiv);
 658         }
 659       }
 660       d_quants_red_lem[q] = lem;
 661     }else{
 662       lem = itr->second;
 663     }
 664     if( !lem.isNull() ){
 665       getOutputChannel().lemma( lem );
 666     }
 667     d_quants_red[q] = !lem.isNull();
 668     return !lem.isNull();
 669   }else{
 670     return (*it).second;
 671   }
 672 }
 673
 674 bool QuantifiersEngine::registerQuantifier( Node f ){
 675   std::map< Node, bool >::iterator it = d_quants.find( f );
 676   if( it==d_quants.end() ){
 677     Trace("quant") << "QuantifiersEngine : Register quantifier ";
 678     Trace("quant") << " : " << f << std::endl;
 679     ++(d_statistics.d_num_quant);
 680     Assert( f.getKind()==FORALL );
 681
 682     //check whether we should apply a reduction
 683     if( reduceQuantifier( f ) ){
 684       Trace("quant") << "...reduced." << std::endl;
 685       d_quants[f] = false;
 686       return false;
 687     }else{
 688       //make instantiation constants for f
 689       d_term_db->makeInstantiationConstantsFor( f );
 690       d_term_db->computeAttributes( f );
 691       for( unsigned i=0; i<d_modules.size(); i++ ){
 692         Trace("quant-debug") << "pre-register with " << d_modules[i]->identify() << "..." << std::endl;
 693         d_modules[i]->preRegisterQuantifier( f );
 694       }
 695       QuantifiersModule * qm = getOwner( f );
 696       if( qm!=NULL ){
 697         Trace("quant") << "   Owner : " << qm->identify() << std::endl;
 698       }
 699       //register with quantifier relevance
 700       if( d_quant_rel ){
 701         d_quant_rel->registerQuantifier( f );
 702       }
 703       //register with each module
 704       for( unsigned i=0; i<d_modules.size(); i++ ){
 705         Trace("quant-debug") << "register with " << d_modules[i]->identify() << "..." << std::endl;
 706         d_modules[i]->registerQuantifier( f );
 707       }
 708       //TODO: remove this
 709       Node ceBody = d_term_db->getInstConstantBody( f );
 710       //also register it with the strong solver
 711       //if( options::finiteModelFind() ){
 712       //  ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
 713       //}
 714       d_quants[f] = true;
 715       return true;
 716     }
 717   }else{
 718     return (*it).second;
 719   }
 720 }
 721
 722 void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
 723   for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){
 724     std::set< Node > added;
 725     getTermDatabase()->addTerm( *p, added );
 726   }
 727 }
 728
 729 void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
 730   if( !pol ){
 731     //if not reduced
 732     if( !reduceQuantifier( f ) ){
 733       //do skolemization
 734       if( d_skolemized.find( f )==d_skolemized.end() ){
 735         Node body = d_term_db->getSkolemizedBody( f );
 736         NodeBuilder<> nb(kind::OR);
 737         nb << f << body.notNode();
 738         Node lem = nb;
 739         if( Trace.isOn("quantifiers-sk-debug") ){
 740           Node slem = Rewriter::rewrite( lem );
 741           Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl;
 742         }
 743         getOutputChannel().lemma( lem, false, true );
 744         d_skolemized[f] = true;
 745       }
 746     }
 747   }else{
 748     //assert to modules TODO : also for !pol?
 749     //register the quantifier, assert it to each module
 750     if( registerQuantifier( f ) ){
 751       d_model->assertQuantifier( f );
 752       for( unsigned i=0; i<d_modules.size(); i++ ){
 753         d_modules[i]->assertNode( f );
 754       }
 755       addTermToDatabase( d_term_db->getInstConstantBody( f ), true );
 756     }
 757   }
 758 }
 759
 760 void QuantifiersEngine::propagate( Theory::Effort level ){
 761   CodeTimer codeTimer(d_statistics.d_time);
 762
 763   for( int i=0; i<(int)d_modules.size(); i++ ){
 764     d_modules[i]->propagate( level );
 765   }
 766 }
 767
 768 Node QuantifiersEngine::getNextDecisionRequest( unsigned& priority ){
 769   unsigned min_priority = 0;
 770   Node dec;
 771   for( unsigned i=0; i<d_modules.size(); i++ ){
 772     Node n = d_modules[i]->getNextDecisionRequest( priority );
 773     if( !n.isNull() && ( dec.isNull() || priority<min_priority ) ){
 774       dec = n;
 775       min_priority = priority;
 776     }
 777   }
 778   return dec;
 779 }
 780
 781 quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() {
 782   return getTermDatabase()->getTermDatabaseSygus();
 783 }
 784
 785 void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
 786   if( options::incrementalSolving() ){
 787     if( d_presolve_in.find( n )==d_presolve_in.end() ){
 788       d_presolve_in.insert( n );
 789       d_presolve_cache.push_back( n );
 790       d_presolve_cache_wq.push_back( withinQuant );
 791       d_presolve_cache_wic.push_back( withinInstClosure );
 792     }
 793   }
 794   //only wait if we are doing incremental solving
 795   if( !d_presolve || !options::incrementalSolving() ){
 796     std::set< Node > added;
 797     getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure );
 798
 799     //added contains also the Node that just have been asserted in this branch
 800     if( d_quant_rel ){
 801       for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
 802         if( !withinQuant ){
 803           d_quant_rel->setRelevance( i->getOperator(), 0 );
 804         }
 805       }
 806     }
 807   }
 808 }
 809
 810 void QuantifiersEngine::eqNotifyNewClass(TNode t) {
 811   addTermToDatabase( t );
 812   if( d_eq_query->getEqualityInference() ){
 813     d_eq_query->getEqualityInference()->eqNotifyNewClass( t );
 814   }
 815 }
 816
 817 void QuantifiersEngine::eqNotifyPreMerge(TNode t1, TNode t2) {
 818   if( d_eq_query->getEqualityInference() ){
 819     d_eq_query->getEqualityInference()->eqNotifyMerge( t1, t2 );
 820   }
 821 }
 822
 823 void QuantifiersEngine::eqNotifyPostMerge(TNode t1, TNode t2) {
 824
 825 }
 826
 827 void QuantifiersEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 828   //if( d_qcf ){
 829   //  d_qcf->assertDisequal( t1, t2 );
 830   //}
 831 }
 832
 833 void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ){
 834   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
 835     Node n = m.get( i );
 836     if( !n.isNull() ){
 837       vars.push_back( f[0][i] );
 838       terms.push_back( n );
 839     }
 840   }
 841 }
 842
 843
 844 bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool addedLem ) {
 845   if( !addedLem ){
 846     //record the instantiation for deletion later
 847     d_recorded_inst.push_back( std::pair< Node, std::vector< Node > >( q, terms ) );
 848   }
 849   if( options::incrementalSolving() ){
 850     Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << std::endl;
 851     inst::CDInstMatchTrie* imt;
 852     std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
 853     if( it!=d_c_inst_match_trie.end() ){
 854       imt = it->second;
 855     }else{
 856       imt = new CDInstMatchTrie( getUserContext() );
 857       d_c_inst_match_trie[q] = imt;
 858     }
 859     return imt->addInstMatch( this, q, terms, getUserContext(), modEq );
 860   }else{
 861     Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
 862     return d_inst_match_trie[q].addInstMatch( this, q, terms, modEq );
 863   }
 864 }
 865
 866 bool QuantifiersEngine::removeInstantiationInternal( Node q, std::vector< Node >& terms ) {
 867   if( options::incrementalSolving() ){
 868     std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
 869     if( it!=d_c_inst_match_trie.end() ){
 870       return it->second->removeInstMatch( this, q, terms );
 871     }else{
 872       return false;
 873     }
 874   }else{
 875     return d_inst_match_trie[q].removeInstMatch( this, q, terms );
 876   }
 877 }
 878
 879 void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t level ){
 880   Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level << std::endl;
 881   //if not from the vector of terms we instantiatied
 882   if( qn.getKind()!=BOUND_VARIABLE && n!=qn ){
 883     //if this is a new term, without an instantiation level
 884     if( !n.hasAttribute(InstLevelAttribute()) ){
 885       InstLevelAttribute ila;
 886       n.setAttribute(ila,level);
 887       Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
 888       Assert( n.getNumChildren()==qn.getNumChildren() );
 889       for( unsigned i=0; i<n.getNumChildren(); i++ ){
 890         setInstantiationLevelAttr( n[i], qn[i], level );
 891       }
 892     }
 893   }
 894 }
 895
 896 void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
 897   if( !n.hasAttribute(InstLevelAttribute()) ){
 898     InstLevelAttribute ila;
 899     n.setAttribute(ila,level);
 900     Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
 901     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 902       setInstantiationLevelAttr( n[i], level );
 903     }
 904   }
 905 }
 906
 907 Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms ){
 908   if( n.getKind()==INST_CONSTANT ){
 909     Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
 910     return terms[n.getAttribute(InstVarNumAttribute())];
 911   }else{
 912     //if( !quantifiers::TermDb::hasInstConstAttr( n ) ){
 913       //Debug("check-inst") << "No inst const attr : " << n << std::endl;
 914       //return n;
 915     //}else{
 916       //Debug("check-inst") << "Recurse on : " << n << std::endl;
 917     std::vector< Node > cc;
 918     if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
 919       cc.push_back( n.getOperator() );
 920     }
 921     bool changed = false;
 922     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 923       Node c = getSubstitute( n[i], terms );
 924       cc.push_back( c );
 925       changed = changed || c!=n[i];
 926     }
 927     if( changed ){
 928       Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cc );
 929       return ret;
 930     }else{
 931       return n;
 932     }
 933   }
 934 }
 935
 936
 937 Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){
 938   Node body;
 939   Assert( vars.size()==terms.size() );
 940   //process partial instantiation if necessary
 941   if( q[0].getNumChildren()!=vars.size() ){
 942     body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
 943     std::vector< Node > uninst_vars;
 944     //doing a partial instantiation, must add quantifier for all uninstantiated variables
 945     for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
 946       if( std::find( vars.begin(), vars.end(), q[0][i] )==vars.end() ){
 947         uninst_vars.push_back( q[0][i] );
 948       }
 949     }
 950     Trace("partial-inst") << "Partially instantiating with " << vars.size() << " / " << q[0].getNumChildren() << " for " << q << std::endl;
 951     Assert( !uninst_vars.empty() );
 952     Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, uninst_vars );
 953     body = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
 954     Trace("partial-inst") << "Partial instantiation : " << q << std::endl;
 955     Trace("partial-inst") << "                      : " << body << std::endl;
 956   }else{
 957     if( options::cbqi() ){
 958       body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
 959     }else{
 960       //do optimized version
 961       Node icb = d_term_db->getInstConstantBody( q );
 962       body = getSubstitute( icb, terms );
 963       if( Debug.isOn("check-inst") ){
 964         Node body2 = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
 965         if( body!=body2 ){
 966           Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl;
 967         }
 968       }
 969     }
 970   }
 971   if( doVts ){
 972     //do virtual term substitution
 973     body = Rewriter::rewrite( body );
 974     Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl;
 975     Node body_r = d_term_db->rewriteVtsSymbols( body );
 976     Trace("quant-vts-debug") << "            ...result: " << body_r << std::endl;
 977     body = body_r;
 978   }
 979   return body;
 980 }
 981
 982 Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m, bool doVts ){
 983   std::vector< Node > vars;
 984   std::vector< Node > terms;
 985   computeTermVector( q, m, vars, terms );
 986   return getInstantiation( q, vars, terms, doVts );
 987 }
 988
 989 Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms, bool doVts ) {
 990   Assert( d_term_db->d_vars.find( q )!=d_term_db->d_vars.end() );
 991   return getInstantiation( q, d_term_db->d_vars[q], terms, doVts );
 992 }
 993
 994 /*
 995 bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq ){
 996   if( options::incrementalSolving() ){
 997     if( d_c_inst_match_trie.find( f )!=d_c_inst_match_trie.end() ){
 998       if( d_c_inst_match_trie[f]->existsInstMatch( this, f, m, getUserContext(), modEq ) ){
 999         return true;
1000       }
1001     }
1002   }else{
1003     if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
1004       if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq ) ){
1005         return true;
1006       }
1007     }
1008   }
1009   return false;
1010 }
1011 */
1012
1013 bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
1014   if( doCache ){
1015     if( doRewrite ){
1016       lem = Rewriter::rewrite(lem);
1017     }
1018     Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl;
1019     BoolMap::const_iterator itp = d_lemmas_produced_c.find( lem );
1020     if( itp==d_lemmas_produced_c.end() || !(*itp).second ){
1021       //d_curr_out->lemma( lem, false, true );
1022       d_lemmas_produced_c[ lem ] = true;
1023       d_lemmas_waiting.push_back( lem );
1024       Trace("inst-add-debug") << "Added lemma" << std::endl;
1025       return true;
1026     }else{
1027       Trace("inst-add-debug") << "Duplicate." << std::endl;
1028       return false;
1029     }
1030   }else{
1031     //do not need to rewrite, will be rewritten after sending
1032     d_lemmas_waiting.push_back( lem );
1033     return true;
1034   }
1035 }
1036
1037 bool QuantifiersEngine::removeLemma( Node lem ) {
1038   std::vector< Node >::iterator it = std::find( d_lemmas_waiting.begin(), d_lemmas_waiting.end(), lem );
1039   if( it!=d_lemmas_waiting.end() ){
1040     d_lemmas_waiting.erase( it, it + 1 );
1041     d_lemmas_produced_c[ lem ] = false;
1042     return true;
1043   }else{
1044     return false;
1045   }
1046 }
1047
1048 void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
1049   d_phase_req_waiting[lit] = req;
1050 }
1051
1052 bool QuantifiersEngine::addInstantiation( Node q, InstMatch& m, bool mkRep, bool modEq, bool doVts ){
1053   std::vector< Node > terms;
1054   m.getTerms( q, terms );
1055   return addInstantiation( q, terms, mkRep, modEq, doVts );
1056 }
1057
1058 bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bool mkRep, bool modEq, bool doVts ) {
1059   // For resource-limiting (also does a time check).
1060   getOutputChannel().safePoint(options::quantifierStep());
1061   Assert( !d_conflict );
1062   Assert( terms.size()==q[0].getNumChildren() );
1063   Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl;
1064   std::vector< Node > rlv_cond;
1065   for( unsigned i=0; i<terms.size(); i++ ){
1066     Trace("inst-add-debug") << "  " << q[0][i];
1067     Trace("inst-add-debug2") << " -> " << terms[i];
1068     if( terms[i].isNull() ){
1069       terms[i] = d_term_db->getModelBasisTerm( q[0][i].getType() );
1070     }
1071     if( mkRep ){
1072       //pick the best possible representative for instantiation, based on past use and simplicity of term
1073       terms[i] = d_eq_query->getInternalRepresentative( terms[i], q, i );
1074     }else{
1075       //ensure the type is correct
1076       terms[i] = quantifiers::TermDb::ensureType( terms[i], q[0][i].getType() );
1077     }
1078     Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
1079     if( terms[i].isNull() ){
1080       Trace("inst-add-debug") << " --> Failed to make term vector, due to term/type restrictions." << std::endl;
1081       return false;
1082     }else{
1083       //get relevancy conditions
1084       if( options::instRelevantCond() ){
1085         quantifiers::TermDb::getRelevancyCondition( terms[i], rlv_cond );
1086       }
1087     }
1088 #ifdef CVC4_ASSERTIONS
1089     bool bad_inst = false;
1090     if( quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) ){
1091       Trace("inst") << "***& inst contains uninterpreted constant : " << terms[i] << std::endl;
1092       bad_inst = true;
1093     }else if( !terms[i].getType().isSubtypeOf( q[0][i].getType() ) ){
1094       Trace("inst") << "***& inst bad type : " << terms[i] << " " << terms[i].getType() << "/" << q[0][i].getType() << std::endl;
1095       bad_inst = true;
1096     }else if( options::cbqi() ){
1097       Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]);
1098       if( !icf.isNull() ){
1099         if( icf==q ){
1100           Trace("inst") << "***& inst contains inst constant attr : " << terms[i] << std::endl;
1101           bad_inst = true;
1102         }else if( quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] ) ){
1103           Trace("inst") << "***& inst contains inst constants : " << terms[i] << std::endl;
1104           bad_inst = true;
1105         }
1106       }
1107     }
1108     //this assertion is critical to soundness
1109     if( bad_inst ){
1110       Trace("inst")<< "***& Bad Instantiate " << q << " with " << std::endl;
1111       for( unsigned j=0; j<terms.size(); j++ ){
1112         Trace("inst") << "   " << terms[j] << std::endl;
1113       }
1114       Assert( false );
1115     }
1116 #endif
1117   }
1118
1119   //check based on instantiation level
1120   if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
1121     for( unsigned i=0; i<terms.size(); i++ ){
1122       if( !d_term_db->isTermEligibleForInstantiation( terms[i], q, true ) ){
1123         return false;
1124       }
1125     }
1126   }
1127
1128   //check for positive entailment
1129   if( options::instNoEntail() ){
1130     //TODO: check consistency of equality engine (if not aborting on utility's reset)
1131     std::map< TNode, TNode > subs;
1132     for( unsigned i=0; i<terms.size(); i++ ){
1133       subs[q[0][i]] = terms[i];
1134     }
1135     if( d_term_db->isEntailed( q[1], subs, false, true ) ){
1136       Trace("inst-add-debug") << " --> Currently entailed." << std::endl;
1137       ++(d_statistics.d_inst_duplicate_ent);
1138       return false;
1139     }
1140     //Node eval = d_term_db->evaluateTerm( q[1], subs, false, true );
1141     //Trace("inst-add-debug2") << "Instantiation evaluates to : " << std::endl;
1142     //Trace("inst-add-debug2") << "   " << eval << std::endl;
1143   }
1144
1145   //check for term vector duplication
1146   bool alreadyExists = !recordInstantiationInternal( q, terms, modEq );
1147   if( alreadyExists ){
1148     Trace("inst-add-debug") << " --> Already exists." << std::endl;
1149     ++(d_statistics.d_inst_duplicate_eq);
1150     return false;
1151   }
1152
1153   //construct the instantiation
1154   Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
1155   Assert( d_term_db->d_vars[q].size()==terms.size() );
1156   Node body = getInstantiation( q, d_term_db->d_vars[q], terms, doVts );  //do virtual term substitution
1157   Node orig_body = body;
1158   if( options::cbqiNestedQE() && d_i_cbqi ){
1159     body = d_i_cbqi->doNestedQE( q, terms, body, doVts );
1160   }
1161   body = quantifiers::QuantifiersRewriter::preprocess( body, true );
1162   Trace("inst-debug") << "...preprocess to " << body << std::endl;
1163
1164   //construct the lemma
1165   Trace("inst-assert") << "(assert " << body << ")" << std::endl;
1166   body = Rewriter::rewrite(body);
1167   Node lem;
1168   if( rlv_cond.empty() ){
1169     lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body );
1170   }else{
1171     rlv_cond.push_back( q.negate() );
1172     rlv_cond.push_back( body );
1173     lem = NodeManager::currentNM()->mkNode( kind::OR, rlv_cond );
1174   }
1175   lem = Rewriter::rewrite(lem);
1176
1177   //check for lemma duplication
1178   if( addLemma( lem, true, false ) ){
1179     d_total_inst_debug[q]++;
1180     d_temp_inst_debug[q]++;
1181     d_total_inst_count_debug++;
1182     if( Trace.isOn("inst") ){
1183       Trace("inst") << "*** Instantiate " << q << " with " << std::endl;
1184       for( unsigned i=0; i<terms.size(); i++ ){
1185         if( Trace.isOn("inst") ){
1186           Trace("inst") << "   " << terms[i];
1187           if( Trace.isOn("inst-debug") ){
1188             Trace("inst-debug") << ", type=" << terms[i].getType() << ", var_type=" << q[0][i].getType();
1189           }
1190           Trace("inst") << std::endl;
1191         }
1192       }
1193     }
1194     if( options::instMaxLevel()!=-1 ){
1195       if( doVts ){
1196         //virtual term substitution/instantiation level features are incompatible
1197         Assert( false );
1198       }else{
1199         uint64_t maxInstLevel = 0;
1200         for( unsigned i=0; i<terms.size(); i++ ){
1201           if( terms[i].hasAttribute(InstLevelAttribute()) ){
1202             if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
1203               maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
1204             }
1205           }
1206         }
1207         setInstantiationLevelAttr( orig_body, q[1], maxInstLevel+1 );
1208       }
1209     }
1210     if( d_curr_effort_level>QEFFORT_CONFLICT && d_curr_effort_level<QEFFORT_NONE ){
1211       //notify listeners
1212       for( unsigned j=0; j<d_inst_notify.size(); j++ ){
1213         if( !d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body ) ){
1214           Trace("inst-add-debug") << "...we are in conflict." << std::endl;
1215           d_conflict = true;
1216           d_conflict_c = true;
1217           Assert( !d_lemmas_waiting.empty() );
1218           break;
1219         }
1220       }
1221     }
1222     if( options::trackInstLemmas() ){
1223       bool recorded;
1224       if( options::incrementalSolving() ){
1225         recorded = d_c_inst_match_trie[q]->recordInstLemma( q, terms, lem );
1226       }else{
1227         recorded = d_inst_match_trie[q].recordInstLemma( q, terms, lem );
1228       }
1229       Trace("inst-add-debug") << "...was recorded : " << recorded << std::endl;
1230       Assert( recorded );
1231     }
1232     Trace("inst-add-debug") << " --> Success." << std::endl;
1233     ++(d_statistics.d_instantiations);
1234     return true;
1235   }else{
1236     Trace("inst-add-debug") << " --> Lemma already exists." << std::endl;
1237     ++(d_statistics.d_inst_duplicate);
1238     return false;
1239   }
1240 }
1241
1242 bool QuantifiersEngine::removeInstantiation( Node q, Node lem, std::vector< Node >& terms ) {
1243   //lem must occur in d_waiting_lemmas
1244   if( removeLemma( lem ) ){
1245     return removeInstantiationInternal( q, terms );
1246   }else{
1247     return false;
1248   }
1249 }
1250
1251 bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
1252   n = Rewriter::rewrite( n );
1253   Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() );
1254   if( addLemma( lem ) ){
1255     Debug("inst") << "*** Add split " << n<< std::endl;
1256     return true;
1257   }
1258   return false;
1259 }
1260
1261 bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool reqPhasePol ){
1262   //Assert( !areEqual( n1, n2 ) );
1263   //Assert( !areDisequal( n1, n2 ) );
1264   Kind knd = n1.getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
1265   Node fm = NodeManager::currentNM()->mkNode( knd, n1, n2 );
1266   return addSplit( fm );
1267 }
1268
1269 bool QuantifiersEngine::addEPRAxiom( TypeNode tn ) {
1270   if( d_qepr ){
1271     Assert( !options::incrementalSolving() );
1272     if( d_qepr->isEPR( tn ) && !d_qepr->hasEPRAxiom( tn ) ){
1273       Node lem = d_qepr->mkEPRAxiom( tn );
1274       Trace("quant-epr") << "EPR lemma for " << tn << " : " << lem << std::endl;
1275       getOutputChannel().lemma( lem );
1276     }
1277   }
1278   return false;
1279 }
1280
1281 void QuantifiersEngine::markRelevant( Node q ) {
1282   d_model->markRelevant( q );
1283 }
1284
1285 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
1286   Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
1287   //determine if we should perform check, based on instWhenMode
1288   bool performCheck = false;
1289   if( options::instWhenMode()==quantifiers::INST_WHEN_FULL ){
1290     performCheck = ( e >= Theory::EFFORT_FULL );
1291   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){
1292     performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck();
1293   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){
1294     performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
1295   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL ){
1296     performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
1297   }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){
1298     performCheck = ( e >= Theory::EFFORT_LAST_CALL );
1299   }else{
1300     performCheck = true;
1301   }
1302   if( e==Theory::EFFORT_LAST_CALL ){
1303     //with bounded integers, skip every other last call,
1304     // since matching loops may occur with infinite quantification
1305     if( d_ierCounter_lc%2==0 && options::fmfBound() ){
1306       performCheck = false;
1307     }
1308   }
1309   return performCheck;
1310 }
1311
1312 quantifiers::UserPatMode QuantifiersEngine::getInstUserPatMode() {
1313   if( options::userPatternsQuant()==quantifiers::USER_PAT_MODE_INTERLEAVE ){
1314     return d_ierCounter%2==0 ? quantifiers::USER_PAT_MODE_USE : quantifiers::USER_PAT_MODE_RESORT;
1315   }else{
1316     return options::userPatternsQuant();
1317   }
1318 }
1319
1320 void QuantifiersEngine::flushLemmas(){
1321   if( !d_lemmas_waiting.empty() ){
1322     //filter based on notify classes
1323     if( !d_inst_notify.empty() ){
1324       unsigned prev_lem_sz = d_lemmas_waiting.size();
1325       for( unsigned j=0; j<d_inst_notify.size(); j++ ){
1326         d_inst_notify[j]->filterInstantiations();
1327       }
1328       if( prev_lem_sz!=d_lemmas_waiting.size() ){
1329         Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting.size() << " / " << prev_lem_sz << std::endl;
1330       }
1331     }
1332     //take default output channel if none is provided
1333     d_hasAddedLemma = true;
1334     for( unsigned i=0; i<d_lemmas_waiting.size(); i++ ){
1335       Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting[i] << std::endl;
1336       getOutputChannel().lemma( d_lemmas_waiting[i], false, true );
1337     }
1338     d_lemmas_waiting.clear();
1339   }
1340   if( !d_phase_req_waiting.empty() ){
1341     for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){
1342       Trace("qe-lemma") << "Require phase : " << it->first << " -> " << it->second << std::endl;
1343       getOutputChannel().requirePhase( it->first, it->second );
1344     }
1345     d_phase_req_waiting.clear();
1346   }
1347 }
1348
1349 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) {
1350   //only if unsat core available
1351   bool isUnsatCoreAvailable = false;
1352   if( options::proof() ){
1353     isUnsatCoreAvailable = ProofManager::currentPM()->unsatCoreAvailable();
1354   }
1355   if( isUnsatCoreAvailable ){
1356     Trace("inst-unsat-core") << "Get instantiations in unsat core..." << std::endl;
1357     ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS, active_lemmas);
1358     if( Trace.isOn("inst-unsat-core") ){
1359       Trace("inst-unsat-core") << "Quantifiers lemmas in unsat core: " << std::endl;
1360       for (unsigned i = 0; i < active_lemmas.size(); ++i) {
1361         Trace("inst-unsat-core") << "  " << active_lemmas[i] << std::endl;
1362       }
1363       Trace("inst-unsat-core") << std::endl;
1364     }
1365     return true;
1366   }else{
1367     return false;
1368   }
1369 }
1370
1371 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp ) {
1372   if( getUnsatCoreLemmas( active_lemmas ) ){
1373     for (unsigned i = 0; i < active_lemmas.size(); ++i) {
1374       Node n = ProofManager::currentPM()->getWeakestImplicantInUnsatCore(active_lemmas[i]);
1375       if( n!=active_lemmas[i] ){
1376         Trace("inst-unsat-core") << "  weaken : " << active_lemmas[i] << " -> " << n << std::endl;
1377       }
1378       weak_imp[active_lemmas[i]] = n;
1379     }
1380     return true;
1381   }else{
1382     return false;
1383   }
1384 }
1385
1386 void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
1387   std::vector< Node > lemmas;
1388   getInstantiations( q, lemmas );
1389   std::map< Node, Node > quant;
1390   std::map< Node, std::vector< Node > > tvec;
1391   getExplanationForInstLemmas( lemmas, quant, tvec );
1392   for( std::map< Node, std::vector< Node > >::iterator it = tvec.begin(); it != tvec.end(); ++it ){
1393     tvecs.push_back( it->second );
1394   }
1395 }
1396
1397 void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
1398   if( options::incrementalSolving() ){
1399     for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
1400       getInstantiationTermVectors( it->first, insts[it->first] );
1401     }
1402   }else{
1403     for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
1404       getInstantiationTermVectors( it->first, insts[it->first] );
1405     }
1406   }
1407 }
1408
1409 void QuantifiersEngine::getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) {
1410   if( options::trackInstLemmas() ){
1411     if( options::incrementalSolving() ){
1412       for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
1413         it->second->getExplanationForInstLemmas( it->first, lems, quant, tvec );
1414       }
1415     }else{
1416       for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
1417         it->second.getExplanationForInstLemmas( it->first, lems, quant, tvec );
1418       }
1419     }
1420 #ifdef CVC4_ASSERTIONS
1421     for( unsigned j=0; j<lems.size(); j++ ){
1422       Assert( quant.find( lems[j] )!=quant.end() );
1423       Assert( tvec.find( lems[j] )!=tvec.end() );
1424     }
1425 #endif
1426   }else{
1427     Assert( false );
1428   }
1429 }
1430
1431 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
1432   bool useUnsatCore = false;
1433   std::vector< Node > active_lemmas;
1434   if( options::trackInstLemmas() && getUnsatCoreLemmas( active_lemmas ) ){
1435     useUnsatCore = true;
1436   }
1437
1438   bool printed = false;
1439   for( BoolMap::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){
1440     Node q = (*it).first;
1441     printed = true;
1442     out << "(skolem " << q << std::endl;
1443     out << "  ( ";
1444     for( unsigned i=0; i<d_term_db->d_skolem_constants[q].size(); i++ ){
1445       if( i>0 ){ out << " "; }
1446       out << d_term_db->d_skolem_constants[q][i];
1447     }
1448     out << " )" << std::endl;
1449     out << ")" << std::endl;
1450   }
1451   if( options::incrementalSolving() ){
1452     for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
1453       bool firstTime = true;
1454       it->second->print( out, it->first, firstTime, useUnsatCore, active_lemmas );
1455       if( !firstTime ){
1456         out << ")" << std::endl;
1457       }
1458       printed = printed || !firstTime;
1459     }
1460   }else{
1461     for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
1462       bool firstTime = true;
1463       it->second.print( out, it->first, firstTime, useUnsatCore, active_lemmas );
1464       if( !firstTime ){
1465         out << ")" << std::endl;
1466       }
1467       printed = printed || !firstTime;
1468     }
1469   }
1470   if( !printed ){
1471     out << "No instantiations" << std::endl;
1472   }
1473 }
1474
1475 void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
1476   if( d_ceg_inst ){
1477     d_ceg_inst->printSynthSolution( out );
1478   }else{
1479     out << "Internal error : module for synth solution not found." << std::endl;
1480   }
1481 }
1482
1483 void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
1484   if( options::incrementalSolving() ){
1485     for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
1486       qs.push_back( it->first );
1487     }
1488   }else{
1489     for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
1490       qs.push_back( it->first );
1491     }
1492   }
1493 }
1494
1495 void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
1496   bool useUnsatCore = false;
1497   std::vector< Node > active_lemmas;
1498   if( options::trackInstLemmas() && getUnsatCoreLemmas( active_lemmas ) ){
1499     useUnsatCore = true;
1500   }
1501
1502   if( options::incrementalSolving() ){
1503     for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
1504       it->second->getInstantiations( insts[it->first], it->first, this, useUnsatCore, active_lemmas );
1505     }
1506   }else{
1507     for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
1508       it->second.getInstantiations( insts[it->first], it->first, this, useUnsatCore, active_lemmas );
1509     }
1510   }
1511 }
1512
1513 void QuantifiersEngine::getInstantiations( Node q, std::vector< Node >& insts  ) {
1514   if( options::incrementalSolving() ){
1515     std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
1516     if( it!=d_c_inst_match_trie.end() ){
1517       std::vector< Node > active_lemmas;
1518       it->second->getInstantiations( insts, it->first, this, false, active_lemmas );
1519     }
1520   }else{
1521     std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.find( q );
1522     if( it!=d_inst_match_trie.end() ){
1523       std::vector< Node > active_lemmas;
1524       it->second.getInstantiations( insts, it->first, this, false, active_lemmas );
1525     }
1526   }
1527 }
1528
1529 Node QuantifiersEngine::getInstantiatedConjunction( Node q ) {
1530   Assert( q.getKind()==FORALL );
1531   std::vector< Node > insts;
1532   getInstantiations( q, insts );
1533   if( insts.empty() ){
1534     return NodeManager::currentNM()->mkConst(true);
1535   }else{
1536     Node ret;
1537     if( insts.size()==1 ){
1538       ret = insts[0];
1539     }else{
1540       ret = NodeManager::currentNM()->mkNode( kind::AND, insts );
1541     }
1542     //have to remove q, TODO: avoid this in a better way
1543     TNode tq = q;
1544     TNode tt = d_term_db->d_true;
1545     ret = ret.substitute( tq, tt );
1546     return ret;
1547   }
1548 }
1549
1550 QuantifiersEngine::Statistics::Statistics()
1551     : d_time("theory::QuantifiersEngine::time"),
1552       d_qcf_time("theory::QuantifiersEngine::time_qcf"),
1553       d_ematching_time("theory::QuantifiersEngine::time_ematching"),
1554       d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
1555       d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
1556       d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
1557       d_instantiations("QuantifiersEngine::Instantiations_Total", 0),
1558       d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0),
1559       d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0),
1560       d_inst_duplicate_ent("QuantifiersEngine::Duplicate_Inst_Entailed", 0),
1561       d_triggers("QuantifiersEngine::Triggers", 0),
1562       d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
1563       d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
1564       d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
1565       d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
1566       d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
1567       d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
1568       d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
1569       d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0),
1570       d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0),
1571       d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0),
1572       d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0),
1573       d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0),
1574       d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0)
1575 {
1576   smtStatisticsRegistry()->registerStat(&d_time);
1577   smtStatisticsRegistry()->registerStat(&d_qcf_time);
1578   smtStatisticsRegistry()->registerStat(&d_ematching_time);
1579   smtStatisticsRegistry()->registerStat(&d_num_quant);
1580   smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
1581   smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
1582   smtStatisticsRegistry()->registerStat(&d_instantiations);
1583   smtStatisticsRegistry()->registerStat(&d_inst_duplicate);
1584   smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq);
1585   smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent);
1586   smtStatisticsRegistry()->registerStat(&d_triggers);
1587   smtStatisticsRegistry()->registerStat(&d_simple_triggers);
1588   smtStatisticsRegistry()->registerStat(&d_multi_triggers);
1589   smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations);
1590   smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
1591   smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns);
1592   smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen);
1593   smtStatisticsRegistry()->registerStat(&d_instantiations_guess);
1594   smtStatisticsRegistry()->registerStat(&d_instantiations_qcf);
1595   smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop);
1596   smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh);
1597   smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi);
1598   smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi);
1599   smtStatisticsRegistry()->registerStat(&d_instantiations_rr);
1600 }
1601
1602 QuantifiersEngine::Statistics::~Statistics(){
1603   smtStatisticsRegistry()->unregisterStat(&d_time);
1604   smtStatisticsRegistry()->unregisterStat(&d_qcf_time);
1605   smtStatisticsRegistry()->unregisterStat(&d_ematching_time);
1606   smtStatisticsRegistry()->unregisterStat(&d_num_quant);
1607   smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
1608   smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
1609   smtStatisticsRegistry()->unregisterStat(&d_instantiations);
1610   smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate);
1611   smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq);
1612   smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent);
1613   smtStatisticsRegistry()->unregisterStat(&d_triggers);
1614   smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
1615   smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
1616   smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations);
1617   smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
1618   smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns);
1619   smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen);
1620   smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess);
1621   smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf);
1622   smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop);
1623   smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh);
1624   smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi);
1625   smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi);
1626   smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr);
1627 }
1628
1629 eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
1630   return getTheoryEngine()->getMasterEqualityEngine();
1631 }
1632
1633 void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
1634   eq::EqualityEngine* ee = getMasterEqualityEngine();
1635   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
1636   std::map< TypeNode, int > typ_num;
1637   while( !eqcs_i.isFinished() ){
1638     TNode r = (*eqcs_i);
1639     TypeNode tr = r.getType();
1640     if( typ_num.find( tr )==typ_num.end() ){
1641       typ_num[tr] = 0;
1642     }
1643     typ_num[tr]++;
1644     bool firstTime = true;
1645     Trace(c) << "  " << r;
1646     Trace(c) << " : { ";
1647     eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
1648     while( !eqc_i.isFinished() ){
1649       TNode n = (*eqc_i);
1650       if( r!=n ){
1651         if( firstTime ){
1652           Trace(c) << std::endl;
1653           firstTime = false;
1654         }
1655         Trace(c) << "    " << n << std::endl;
1656       }
1657       ++eqc_i;
1658     }
1659     if( !firstTime ){ Trace(c) << "  "; }
1660     Trace(c) << "}" << std::endl;
1661     ++eqcs_i;
1662   }
1663   Trace(c) << std::endl;
1664   for( std::map< TypeNode, int >::iterator it = typ_num.begin(); it != typ_num.end(); ++it ){
1665     Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl;
1666   }
1667 }
1668
1669
1670 EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ) : d_qe( qe ), d_eqi_counter( c ), d_reset_count( 0 ){
1671   if( options::inferArithTriggerEq() ){
1672     d_eq_inference = new quantifiers::EqualityInference( c, options::inferArithTriggerEqExp() );
1673   }else{
1674     d_eq_inference = NULL;
1675   }
1676 }
1677
1678 EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){
1679   delete d_eq_inference;
1680 }
1681
1682 bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){
1683   d_int_rep.clear();
1684   d_reset_count++;
1685   return processInferences( e );
1686 }
1687
1688 bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) {
1689   if( options::inferArithTriggerEq() ){
1690     eq::EqualityEngine* ee = getEngine();
1691     //updated implementation
1692     while( d_eqi_counter.get()<d_eq_inference->getNumPendingMerges() ){
1693       Node eq = d_eq_inference->getPendingMerge( d_eqi_counter.get() );
1694       Node eq_exp = d_eq_inference->getPendingMergeExplanation( d_eqi_counter.get() );
1695       Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq << std::endl;
1696       Trace("quant-engine-ee-proc") << "      explanation : " << eq_exp << std::endl;
1697       Assert( ee->hasTerm( eq[0] ) );
1698       Assert( ee->hasTerm( eq[1] ) );
1699       if( areDisequal( eq[0], eq[1] ) ){
1700         Trace("quant-engine-ee-proc") << "processInferences : Conflict : " << eq << std::endl;
1701         if( Trace.isOn("term-db-lemma") ){
1702           Trace("term-db-lemma") << "Disequal terms, equal by normalization : " << eq[0] << " " << eq[1] << "!!!!" << std::endl;
1703           if( !d_qe->getTheoryEngine()->needCheck() ){
1704             Trace("term-db-lemma") << "  all theories passed with no lemmas." << std::endl;
1705             //this should really never happen (implies arithmetic is incomplete when sharing is enabled)
1706             Assert( false );
1707           }
1708           Trace("term-db-lemma") << "  add split on : " << eq << std::endl;
1709         }
1710         d_qe->addSplit( eq );
1711         return false;
1712       }else{
1713         ee->assertEquality( eq, true, eq_exp );
1714         d_eqi_counter = d_eqi_counter.get() + 1;
1715       }
1716     }
1717     Assert( ee->consistent() );
1718   }
1719   return true;
1720 }
1721
1722 bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
1723   return getEngine()->hasTerm( a );
1724 }
1725
1726 Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){
1727   eq::EqualityEngine* ee = getEngine();
1728   if( ee->hasTerm( a ) ){
1729     return ee->getRepresentative( a );
1730   }else{
1731     return a;
1732   }
1733 }
1734
1735 bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
1736   if( a==b ){
1737     return true;
1738   }else{
1739     eq::EqualityEngine* ee = getEngine();
1740     if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
1741       return ee->areEqual( a, b );
1742     }else{
1743       return false;
1744     }
1745   }
1746 }
1747
1748 bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
1749   if( a==b ){
1750     return false;
1751   }else{
1752     eq::EqualityEngine* ee = getEngine();
1753     if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
1754       return ee->areDisequal( a, b, false );
1755     }else{
1756       return a.isConst() && b.isConst();
1757     }
1758   }
1759 }
1760
1761 Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
1762   Assert( f.isNull() || f.getKind()==FORALL );
1763   Node r = getRepresentative( a );
1764   if( options::finiteModelFind() ){
1765     if( r.isConst() && quantifiers::TermDb::containsUninterpretedConstant( r ) ){
1766       //map back from values assigned by model, if any
1767       if( d_qe->getModel() ){
1768         std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r );
1769         if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){
1770           r = it->second;
1771           r = getRepresentative( r );
1772         }else{
1773           if( r.getType().isSort() ){
1774             Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
1775             //should never happen : UF constants should never escape model
1776             Assert( false );
1777           }
1778         }
1779       }
1780     }
1781   }
1782   if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE ){
1783     return r;
1784   }else{
1785     TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType();
1786     std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r );
1787     if( itir==d_int_rep[v_tn].end() ){
1788       //find best selection for representative
1789       Node r_best;
1790       //if( options::fmfRelevantDomain() && !f.isNull() ){
1791       //  Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
1792       //  r_best = d_qe->getRelevantDomain()->getRelevantTerm( f, index, r );
1793       //  Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
1794       //}
1795       std::vector< Node > eqc;
1796       getEquivalenceClass( r, eqc );
1797       Trace("internal-rep-select") << "Choose representative for equivalence class : { ";
1798       for( unsigned i=0; i<eqc.size(); i++ ){
1799         if( i>0 ) Trace("internal-rep-select") << ", ";
1800         Trace("internal-rep-select") << eqc[i];
1801       }
1802       Trace("internal-rep-select")  << " }, type = " << v_tn << std::endl;
1803       int r_best_score = -1;
1804       for( size_t i=0; i<eqc.size(); i++ ){
1805         int score = getRepScore( eqc[i], f, index, v_tn );
1806         if( score!=-2 ){
1807           if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
1808             r_best = eqc[i];
1809             r_best_score = score;
1810           }
1811         }
1812       }
1813       if( r_best.isNull() ){
1814         Trace("internal-rep-warn") << "No valid choice for representative in eqc class." << std::endl;
1815         r_best = r;
1816       }
1817       //now, make sure that no other member of the class is an instance
1818       std::hash_map<TNode, Node, TNodeHashFunction> cache;
1819       r_best = getInstance( r_best, eqc, cache );
1820       //store that this representative was chosen at this point
1821       if( d_rep_score.find( r_best )==d_rep_score.end() ){
1822         d_rep_score[ r_best ] = d_reset_count;
1823       }
1824       Trace("internal-rep-select") << "...Choose " << r_best << " with score " << r_best_score << std::endl;
1825       Assert( r_best.getType().isSubtypeOf( v_tn ) );
1826       d_int_rep[v_tn][r] = r_best;
1827       if( r_best!=a ){
1828         Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
1829         Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
1830       }
1831       return r_best;
1832     }else{
1833       return itir->second;
1834     }
1835   }
1836 }
1837
1838 void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ) {
1839   //make sure internal representatives currently exist
1840   for( std::map< TypeNode, std::vector< Node > >::iterator it = reps.begin(); it != reps.end(); ++it ){
1841     if( it->first.isSort() ){
1842       for( unsigned i=0; i<it->second.size(); i++ ){
1843         Node r = getInternalRepresentative( it->second[i], Node::null(), 0 );
1844       }
1845     }
1846   }
1847   Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl;
1848   for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
1849     for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
1850       Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
1851     }
1852   }
1853   //store representatives for newly created terms
1854   std::map< Node, Node > temp_rep_map;
1855
1856   bool success;
1857   do {
1858     success = false;
1859     for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
1860       for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
1861         if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){
1862           Node ni = it->second;
1863           std::vector< Node > cc;
1864           cc.push_back( it->second.getOperator() );
1865           bool changed = false;
1866           for( unsigned j=0; j<ni.getNumChildren(); j++ ){
1867             if( ni[j].getType().isSort() ){
1868               Node r = getRepresentative( ni[j] );
1869               if( itt->second.find( r )==itt->second.end() ){
1870                 Assert( temp_rep_map.find( r )!=temp_rep_map.end() );
1871                 r = temp_rep_map[r];
1872               }
1873               if( r==ni ){
1874                 //found sub-term as instance
1875                 Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl;
1876                 itt->second[it->first] = ni[j];
1877                 changed = false;
1878                 success = true;
1879                 break;
1880               }else{
1881                 Node ir = itt->second[r];
1882                 cc.push_back( ir );
1883                 if( ni[j]!=ir ){
1884                   changed = true;
1885                 }
1886               }
1887             }else{
1888               changed = false;
1889               break;
1890             }
1891           }
1892           if( changed ){
1893             Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc );
1894             Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl;
1895             success = true;
1896             itt->second[it->first] = n;
1897             temp_rep_map[n] = it->first;
1898           }
1899         }
1900       }
1901     }
1902   }while( success );
1903   Trace("internal-rep-flatten") << "---After flattening : " << std::endl;
1904   for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
1905     for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
1906       Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
1907     }
1908   }
1909 }
1910
1911 eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
1912   return d_qe->getMasterEqualityEngine();
1913 }
1914
1915 void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
1916   eq::EqualityEngine* ee = getEngine();
1917   if( ee->hasTerm( a ) ){
1918     Node rep = ee->getRepresentative( a );
1919     eq::EqClassIterator eqc_iter( rep, ee );
1920     while( !eqc_iter.isFinished() ){
1921       eqc.push_back( *eqc_iter );
1922       eqc_iter++;
1923     }
1924   }else{
1925     eqc.push_back( a );
1926   }
1927   //a should be in its equivalence class
1928   Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
1929 }
1930
1931 TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNode >& args ) {
1932   return d_qe->getTermDatabase()->getCongruentTerm( f, args );
1933 }
1934
1935 //helper functions
1936
1937 Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ){
1938   if(cache.find(n) != cache.end()) {
1939     return cache[n];
1940   }
1941   for( size_t i=0; i<n.getNumChildren(); i++ ){
1942     Node nn = getInstance( n[i], eqc, cache );
1943     if( !nn.isNull() ){
1944       return cache[n] = nn;
1945     }
1946   }
1947   if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){
1948     return cache[n] = n;
1949   }else{
1950     return cache[n] = Node::null();
1951   }
1952 }
1953
1954 //-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
1955 int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, TypeNode v_tn ){
1956   if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){  //reject
1957     return -2;
1958   }else if( !n.getType().isSubtypeOf( v_tn ) ){  //reject if incorrect type
1959     return -2;
1960   }else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){
1961     return -1;
1962   }else if( options::instMaxLevel()!=-1 ){
1963     //score prefer lowest instantiation level
1964     if( n.hasAttribute(InstLevelAttribute()) ){
1965       return n.getAttribute(InstLevelAttribute());
1966     }else{
1967       return options::instLevelInputOnly() ? -1 : 0;
1968     }
1969   }else{
1970     if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_FIRST ){
1971       //score prefers earliest use of this term as a representative
1972       return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
1973     }else{
1974       Assert( options::quantRepMode()==quantifiers::QUANT_REP_MODE_DEPTH );
1975       return quantifiers::TermDb::getTermDepth( n );
1976     }
1977   }
1978 }