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