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