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/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::fullSaturateInterleave() ){
 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       // flush lemmas
 745       flushLemmas();
 746       return true;
 747     }
 748   }else{
 749     return (*it).second;
 750   }
 751 }
 752
 753 void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
 754   for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){
 755     std::set< Node > added;
 756     getTermDatabase()->addTerm( *p, added );
 757   }
 758 }
 759
 760 void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
 761   if( !pol ){
 762     //if not reduced
 763     if( !reduceQuantifier( f ) ){
 764       //do skolemization
 765       if( d_skolemized.find( f )==d_skolemized.end() ){
 766         Node body = d_term_db->getSkolemizedBody( f );
 767         NodeBuilder<> nb(kind::OR);
 768         nb << f << body.notNode();
 769         Node lem = nb;
 770         if( Trace.isOn("quantifiers-sk-debug") ){
 771           Node slem = Rewriter::rewrite( lem );
 772           Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl;
 773         }
 774         getOutputChannel().lemma( lem, false, true );
 775         d_skolemized[f] = true;
 776       }
 777     }
 778   }else{
 779     //assert to modules TODO : also for !pol?
 780     //register the quantifier, assert it to each module
 781     if( registerQuantifier( f ) ){
 782       d_model->assertQuantifier( f );
 783       for( unsigned i=0; i<d_modules.size(); i++ ){
 784         d_modules[i]->assertNode( f );
 785       }
 786       addTermToDatabase( d_term_db->getInstConstantBody( f ), true );
 787     }
 788   }
 789 }
 790
 791 void QuantifiersEngine::propagate( Theory::Effort level ){
 792   CodeTimer codeTimer(d_statistics.d_time);
 793
 794   for( int i=0; i<(int)d_modules.size(); i++ ){
 795     d_modules[i]->propagate( level );
 796   }
 797 }
 798
 799 Node QuantifiersEngine::getNextDecisionRequest( unsigned& priority ){
 800   unsigned min_priority = 0;
 801   Node dec;
 802   for( unsigned i=0; i<d_modules.size(); i++ ){
 803     Node n = d_modules[i]->getNextDecisionRequest( priority );
 804     if( !n.isNull() && ( dec.isNull() || priority<min_priority ) ){
 805       dec = n;
 806       min_priority = priority;
 807     }
 808   }
 809   return dec;
 810 }
 811
 812 quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() {
 813   return getTermDatabase()->getTermDatabaseSygus();
 814 }
 815
 816 void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
 817   if( options::incrementalSolving() ){
 818     if( d_presolve_in.find( n )==d_presolve_in.end() ){
 819       d_presolve_in.insert( n );
 820       d_presolve_cache.push_back( n );
 821       d_presolve_cache_wq.push_back( withinQuant );
 822       d_presolve_cache_wic.push_back( withinInstClosure );
 823     }
 824   }
 825   //only wait if we are doing incremental solving
 826   if( !d_presolve || !options::incrementalSolving() ){
 827     std::set< Node > added;
 828     getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure );
 829
 830     //added contains also the Node that just have been asserted in this branch
 831     if( d_quant_rel ){
 832       for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
 833         if( !withinQuant ){
 834           d_quant_rel->setRelevance( i->getOperator(), 0 );
 835         }
 836       }
 837     }
 838   }
 839 }
 840
 841 void QuantifiersEngine::eqNotifyNewClass(TNode t) {
 842   addTermToDatabase( t );
 843   if( d_eq_query->getEqualityInference() ){
 844     d_eq_query->getEqualityInference()->eqNotifyNewClass( t );
 845   }
 846 }
 847
 848 void QuantifiersEngine::eqNotifyPreMerge(TNode t1, TNode t2) {
 849   if( d_eq_query->getEqualityInference() ){
 850     d_eq_query->getEqualityInference()->eqNotifyMerge( t1, t2 );
 851   }
 852 }
 853
 854 void QuantifiersEngine::eqNotifyPostMerge(TNode t1, TNode t2) {
 855
 856 }
 857
 858 void QuantifiersEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 859   //if( d_qcf ){
 860   //  d_qcf->assertDisequal( t1, t2 );
 861   //}
 862 }
 863
 864 void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ){
 865   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
 866     Node n = m.get( i );
 867     if( !n.isNull() ){
 868       vars.push_back( f[0][i] );
 869       terms.push_back( n );
 870     }
 871   }
 872 }
 873
 874
 875 bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool addedLem ) {
 876   if( !addedLem ){
 877     //record the instantiation for deletion later
 878     d_recorded_inst.push_back( std::pair< Node, std::vector< Node > >( q, terms ) );
 879   }
 880   if( options::incrementalSolving() ){
 881     Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << std::endl;
 882     inst::CDInstMatchTrie* imt;
 883     std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
 884     if( it!=d_c_inst_match_trie.end() ){
 885       imt = it->second;
 886     }else{
 887       imt = new CDInstMatchTrie( getUserContext() );
 888       d_c_inst_match_trie[q] = imt;
 889     }
 890     return imt->addInstMatch( this, q, terms, getUserContext(), modEq );
 891   }else{
 892     Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
 893     return d_inst_match_trie[q].addInstMatch( this, q, terms, modEq );
 894   }
 895 }
 896
 897 bool QuantifiersEngine::removeInstantiationInternal( Node q, std::vector< Node >& terms ) {
 898   if( options::incrementalSolving() ){
 899     std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
 900     if( it!=d_c_inst_match_trie.end() ){
 901       return it->second->removeInstMatch( this, q, terms );
 902     }else{
 903       return false;
 904     }
 905   }else{
 906     return d_inst_match_trie[q].removeInstMatch( this, q, terms );
 907   }
 908 }
 909
 910 void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t level ){
 911   Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level << std::endl;
 912   //if not from the vector of terms we instantiatied
 913   if( qn.getKind()!=BOUND_VARIABLE && n!=qn ){
 914     //if this is a new term, without an instantiation level
 915     if( !n.hasAttribute(InstLevelAttribute()) ){
 916       InstLevelAttribute ila;
 917       n.setAttribute(ila,level);
 918       Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
 919       Assert( n.getNumChildren()==qn.getNumChildren() );
 920       for( unsigned i=0; i<n.getNumChildren(); i++ ){
 921         setInstantiationLevelAttr( n[i], qn[i], level );
 922       }
 923     }
 924   }
 925 }
 926
 927 void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
 928   if( !n.hasAttribute(InstLevelAttribute()) ){
 929     InstLevelAttribute ila;
 930     n.setAttribute(ila,level);
 931     Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
 932     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 933       setInstantiationLevelAttr( n[i], level );
 934     }
 935   }
 936 }
 937
 938 Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms, std::map< Node, Node >& visited ){
 939   std::map< Node, Node >::iterator itv = visited.find( n );
 940   if( itv==visited.end() ){
 941     Node ret = n;
 942     if( n.getKind()==INST_CONSTANT ){
 943       Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
 944       ret = terms[n.getAttribute(InstVarNumAttribute())];
 945     }else{
 946       //if( !quantifiers::TermDb::hasInstConstAttr( n ) ){
 947         //Debug("check-inst") << "No inst const attr : " << n << std::endl;
 948         //return n;
 949       //}else{
 950         //Debug("check-inst") << "Recurse on : " << n << std::endl;
 951       std::vector< Node > cc;
 952       if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
 953         cc.push_back( n.getOperator() );
 954       }
 955       bool changed = false;
 956       for( unsigned i=0; i<n.getNumChildren(); i++ ){
 957         Node c = getSubstitute( n[i], terms, visited );
 958         cc.push_back( c );
 959         changed = changed || c!=n[i];
 960       }
 961       if( changed ){
 962         ret = NodeManager::currentNM()->mkNode( n.getKind(), cc );
 963       }
 964     }
 965     visited[n] = ret;
 966     return ret;
 967   }else{
 968     return itv->second;
 969   }
 970 }
 971
 972
 973 Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){
 974   Node body;
 975   Assert( vars.size()==terms.size() );
 976   //process partial instantiation if necessary
 977   if( q[0].getNumChildren()!=vars.size() ){
 978     body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
 979     std::vector< Node > uninst_vars;
 980     //doing a partial instantiation, must add quantifier for all uninstantiated variables
 981     for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
 982       if( std::find( vars.begin(), vars.end(), q[0][i] )==vars.end() ){
 983         uninst_vars.push_back( q[0][i] );
 984       }
 985     }
 986     Trace("partial-inst") << "Partially instantiating with " << vars.size() << " / " << q[0].getNumChildren() << " for " << q << std::endl;
 987     Assert( !uninst_vars.empty() );
 988     Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, uninst_vars );
 989     body = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
 990     Trace("partial-inst") << "Partial instantiation : " << q << std::endl;
 991     Trace("partial-inst") << "                      : " << body << std::endl;
 992   }else{
 993     if( options::cbqi() ){
 994       body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
 995     }else{
 996       //do optimized version
 997       Node icb = d_term_db->getInstConstantBody( q );
 998       std::map< Node, Node > visited;
 999       body = getSubstitute( icb, terms, visited );
1000       if( Debug.isOn("check-inst") ){
1001         Node body2 = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
1002         if( body!=body2 ){
1003           Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl;
1004         }
1005       }
1006     }
1007   }
1008   if( doVts ){
1009     //do virtual term substitution
1010     body = Rewriter::rewrite( body );
1011     Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl;
1012     Node body_r = d_term_db->rewriteVtsSymbols( body );
1013     Trace("quant-vts-debug") << "            ...result: " << body_r << std::endl;
1014     body = body_r;
1015   }
1016   return body;
1017 }
1018
1019 Node QuantifiersEngine::getInstantiation( Node q, InstMatch& m, bool doVts ){
1020   std::vector< Node > vars;
1021   std::vector< Node > terms;
1022   computeTermVector( q, m, vars, terms );
1023   return getInstantiation( q, vars, terms, doVts );
1024 }
1025
1026 Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& terms, bool doVts ) {
1027   Assert( d_term_db->d_vars.find( q )!=d_term_db->d_vars.end() );
1028   return getInstantiation( q, d_term_db->d_vars[q], terms, doVts );
1029 }
1030
1031 /*
1032 bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq ){
1033   if( options::incrementalSolving() ){
1034     if( d_c_inst_match_trie.find( f )!=d_c_inst_match_trie.end() ){
1035       if( d_c_inst_match_trie[f]->existsInstMatch( this, f, m, getUserContext(), modEq ) ){
1036         return true;
1037       }
1038     }
1039   }else{
1040     if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
1041       if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq ) ){
1042         return true;
1043       }
1044     }
1045   }
1046   return false;
1047 }
1048 */
1049
1050 bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
1051   if( doCache ){
1052     if( doRewrite ){
1053       lem = Rewriter::rewrite(lem);
1054     }
1055     Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl;
1056     BoolMap::const_iterator itp = d_lemmas_produced_c.find( lem );
1057     if( itp==d_lemmas_produced_c.end() || !(*itp).second ){
1058       //d_curr_out->lemma( lem, false, true );
1059       d_lemmas_produced_c[ lem ] = true;
1060       d_lemmas_waiting.push_back( lem );
1061       Trace("inst-add-debug") << "Added lemma" << std::endl;
1062       return true;
1063     }else{
1064       Trace("inst-add-debug") << "Duplicate." << std::endl;
1065       return false;
1066     }
1067   }else{
1068     //do not need to rewrite, will be rewritten after sending
1069     d_lemmas_waiting.push_back( lem );
1070     return true;
1071   }
1072 }
1073
1074 bool QuantifiersEngine::removeLemma( Node lem ) {
1075   std::vector< Node >::iterator it = std::find( d_lemmas_waiting.begin(), d_lemmas_waiting.end(), lem );
1076   if( it!=d_lemmas_waiting.end() ){
1077     d_lemmas_waiting.erase( it, it + 1 );
1078     d_lemmas_produced_c[ lem ] = false;
1079     return true;
1080   }else{
1081     return false;
1082   }
1083 }
1084
1085 void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
1086   d_phase_req_waiting[lit] = req;
1087 }
1088
1089 bool QuantifiersEngine::addInstantiation( Node q, InstMatch& m, bool mkRep, bool modEq, bool doVts ){
1090   std::vector< Node > terms;
1091   m.getTerms( q, terms );
1092   return addInstantiation( q, terms, mkRep, modEq, doVts );
1093 }
1094
1095 bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bool mkRep, bool modEq, bool doVts ) {
1096   // For resource-limiting (also does a time check).
1097   getOutputChannel().safePoint(options::quantifierStep());
1098   Assert( !d_conflict );
1099   Assert( terms.size()==q[0].getNumChildren() );
1100   Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl;
1101   std::vector< Node > rlv_cond;
1102   for( unsigned i=0; i<terms.size(); i++ ){
1103     Trace("inst-add-debug") << "  " << q[0][i];
1104     Trace("inst-add-debug2") << " -> " << terms[i];
1105     if( terms[i].isNull() ){
1106       terms[i] = d_term_db->getModelBasisTerm( q[0][i].getType() );
1107     }
1108     if( mkRep ){
1109       //pick the best possible representative for instantiation, based on past use and simplicity of term
1110       terms[i] = getInternalRepresentative( terms[i], q, i );
1111     }else{
1112       //ensure the type is correct
1113       terms[i] = quantifiers::TermDb::ensureType( terms[i], q[0][i].getType() );
1114     }
1115     Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
1116     if( terms[i].isNull() ){
1117       Trace("inst-add-debug") << " --> Failed to make term vector, due to term/type restrictions." << std::endl;
1118       return false;
1119     }else{
1120       //get relevancy conditions
1121       if( options::instRelevantCond() ){
1122         quantifiers::TermDb::getRelevancyCondition( terms[i], rlv_cond );
1123       }
1124     }
1125 #ifdef CVC4_ASSERTIONS
1126     bool bad_inst = false;
1127     if( quantifiers::TermDb::containsUninterpretedConstant( terms[i] ) ){
1128       Trace("inst") << "***& inst contains uninterpreted constant : " << terms[i] << std::endl;
1129       bad_inst = true;
1130     }else if( !terms[i].getType().isSubtypeOf( q[0][i].getType() ) ){
1131       Trace("inst") << "***& inst bad type : " << terms[i] << " " << terms[i].getType() << "/" << q[0][i].getType() << std::endl;
1132       bad_inst = true;
1133     }else if( options::cbqi() ){
1134       Node icf = quantifiers::TermDb::getInstConstAttr(terms[i]);
1135       if( !icf.isNull() ){
1136         if( icf==q ){
1137           Trace("inst") << "***& inst contains inst constant attr : " << terms[i] << std::endl;
1138           bad_inst = true;
1139         }else if( quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] ) ){
1140           Trace("inst") << "***& inst contains inst constants : " << terms[i] << std::endl;
1141           bad_inst = true;
1142         }
1143       }
1144     }
1145     //this assertion is critical to soundness
1146     if( bad_inst ){
1147       Trace("inst")<< "***& Bad Instantiate " << q << " with " << std::endl;
1148       for( unsigned j=0; j<terms.size(); j++ ){
1149         Trace("inst") << "   " << terms[j] << std::endl;
1150       }
1151       Assert( false );
1152     }
1153 #endif
1154   }
1155
1156   //check based on instantiation level
1157   if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
1158     for( unsigned i=0; i<terms.size(); i++ ){
1159       if( !d_term_db->isTermEligibleForInstantiation( terms[i], q, true ) ){
1160         return false;
1161       }
1162     }
1163   }
1164
1165   //check for positive entailment
1166   if( options::instNoEntail() ){
1167     //TODO: check consistency of equality engine (if not aborting on utility's reset)
1168     std::map< TNode, TNode > subs;
1169     for( unsigned i=0; i<terms.size(); i++ ){
1170       subs[q[0][i]] = terms[i];
1171     }
1172     if( d_term_db->isEntailed( q[1], subs, false, true ) ){
1173       Trace("inst-add-debug") << " --> Currently entailed." << std::endl;
1174       ++(d_statistics.d_inst_duplicate_ent);
1175       return false;
1176     }
1177     //Node eval = d_term_db->evaluateTerm( q[1], subs, false, true );
1178     //Trace("inst-add-debug2") << "Instantiation evaluates to : " << std::endl;
1179     //Trace("inst-add-debug2") << "   " << eval << std::endl;
1180   }
1181
1182   //check for term vector duplication
1183   bool alreadyExists = !recordInstantiationInternal( q, terms, modEq );
1184   if( alreadyExists ){
1185     Trace("inst-add-debug") << " --> Already exists." << std::endl;
1186     ++(d_statistics.d_inst_duplicate_eq);
1187     return false;
1188   }
1189
1190   //construct the instantiation
1191   Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
1192   Assert( d_term_db->d_vars[q].size()==terms.size() );
1193   Node body = getInstantiation( q, d_term_db->d_vars[q], terms, doVts );  //do virtual term substitution
1194   Node orig_body = body;
1195   if( options::cbqiNestedQE() && d_i_cbqi ){
1196     body = d_i_cbqi->doNestedQE( q, terms, body, doVts );
1197   }
1198   body = quantifiers::QuantifiersRewriter::preprocess( body, true );
1199   Trace("inst-debug") << "...preprocess to " << body << std::endl;
1200
1201   //construct the lemma
1202   Trace("inst-assert") << "(assert " << body << ")" << std::endl;
1203   body = Rewriter::rewrite(body);
1204
1205   if( d_useModelEe && options::instNoModelTrue() ){
1206     Node val_body = d_model->getValue( body );
1207     if( val_body==d_term_db->d_true ){
1208       Trace("inst-add-debug") << " --> True in model." << std::endl;
1209       ++(d_statistics.d_inst_duplicate_model_true);
1210       return false;
1211     }
1212   }
1213
1214   Node lem;
1215   if( rlv_cond.empty() ){
1216     lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body );
1217   }else{
1218     rlv_cond.push_back( q.negate() );
1219     rlv_cond.push_back( body );
1220     lem = NodeManager::currentNM()->mkNode( kind::OR, rlv_cond );
1221   }
1222   lem = Rewriter::rewrite(lem);
1223
1224   //check for lemma duplication
1225   if( addLemma( lem, true, false ) ){
1226     d_total_inst_debug[q]++;
1227     d_temp_inst_debug[q]++;
1228     d_total_inst_count_debug++;
1229     if( Trace.isOn("inst") ){
1230       Trace("inst") << "*** Instantiate " << q << " with " << std::endl;
1231       for( unsigned i=0; i<terms.size(); i++ ){
1232         if( Trace.isOn("inst") ){
1233           Trace("inst") << "   " << terms[i];
1234           if( Trace.isOn("inst-debug") ){
1235             Trace("inst-debug") << ", type=" << terms[i].getType() << ", var_type=" << q[0][i].getType();
1236           }
1237           Trace("inst") << std::endl;
1238         }
1239       }
1240     }
1241     if( options::instMaxLevel()!=-1 ){
1242       if( doVts ){
1243         //virtual term substitution/instantiation level features are incompatible
1244         Assert( false );
1245       }else{
1246         uint64_t maxInstLevel = 0;
1247         for( unsigned i=0; i<terms.size(); i++ ){
1248           if( terms[i].hasAttribute(InstLevelAttribute()) ){
1249             if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
1250               maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
1251             }
1252           }
1253         }
1254         setInstantiationLevelAttr( orig_body, q[1], maxInstLevel+1 );
1255       }
1256     }
1257     if( d_curr_effort_level>QEFFORT_CONFLICT && d_curr_effort_level<QEFFORT_NONE ){
1258       //notify listeners
1259       for( unsigned j=0; j<d_inst_notify.size(); j++ ){
1260         if( !d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body ) ){
1261           Trace("inst-add-debug") << "...we are in conflict." << std::endl;
1262           setConflict();
1263           Assert( !d_lemmas_waiting.empty() );
1264           break;
1265         }
1266       }
1267     }
1268     if( options::trackInstLemmas() ){
1269       bool recorded;
1270       if( options::incrementalSolving() ){
1271         recorded = d_c_inst_match_trie[q]->recordInstLemma( q, terms, lem );
1272       }else{
1273         recorded = d_inst_match_trie[q].recordInstLemma( q, terms, lem );
1274       }
1275       Trace("inst-add-debug") << "...was recorded : " << recorded << std::endl;
1276       Assert( recorded );
1277     }
1278     Trace("inst-add-debug") << " --> Success." << std::endl;
1279     ++(d_statistics.d_instantiations);
1280     return true;
1281   }else{
1282     Trace("inst-add-debug") << " --> Lemma already exists." << std::endl;
1283     ++(d_statistics.d_inst_duplicate);
1284     return false;
1285   }
1286 }
1287
1288 bool QuantifiersEngine::removeInstantiation( Node q, Node lem, std::vector< Node >& terms ) {
1289   //lem must occur in d_waiting_lemmas
1290   if( removeLemma( lem ) ){
1291     return removeInstantiationInternal( q, terms );
1292   }else{
1293     return false;
1294   }
1295 }
1296
1297 bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
1298   n = Rewriter::rewrite( n );
1299   Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() );
1300   if( addLemma( lem ) ){
1301     Debug("inst") << "*** Add split " << n<< std::endl;
1302     return true;
1303   }
1304   return false;
1305 }
1306
1307 bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool reqPhasePol ){
1308   //Assert( !areEqual( n1, n2 ) );
1309   //Assert( !areDisequal( n1, n2 ) );
1310   Node fm = NodeManager::currentNM()->mkNode( EQUAL, n1, n2 );
1311   return addSplit( fm );
1312 }
1313
1314 bool QuantifiersEngine::addEPRAxiom( TypeNode tn ) {
1315   if( d_qepr ){
1316     Assert( !options::incrementalSolving() );
1317     if( d_qepr->isEPR( tn ) && !d_qepr->hasEPRAxiom( tn ) ){
1318       Node lem = d_qepr->mkEPRAxiom( tn );
1319       Trace("quant-epr") << "EPR lemma for " << tn << " : " << lem << std::endl;
1320       getOutputChannel().lemma( lem );
1321     }
1322   }
1323   return false;
1324 }
1325
1326 void QuantifiersEngine::markRelevant( Node q ) {
1327   d_model->markRelevant( q );
1328 }
1329
1330 void QuantifiersEngine::setConflict() {
1331   d_conflict = true;
1332   d_conflict_c = true;
1333 }
1334
1335 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
1336   Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
1337   //determine if we should perform check, based on instWhenMode
1338   bool performCheck = false;
1339   if( options::instWhenMode()==quantifiers::INST_WHEN_FULL ){
1340     performCheck = ( e >= Theory::EFFORT_FULL );
1341   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){
1342     performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck();
1343   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){
1344     performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
1345   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL ){
1346     performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
1347   }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){
1348     performCheck = ( e >= Theory::EFFORT_LAST_CALL );
1349   }else{
1350     performCheck = true;
1351   }
1352   if( e==Theory::EFFORT_LAST_CALL ){
1353     //with bounded integers, skip every other last call,
1354     // since matching loops may occur with infinite quantification
1355     if( d_ierCounter_lc%2==0 && options::fmfBound() ){
1356       performCheck = false;
1357     }
1358   }
1359   return performCheck;
1360 }
1361
1362 quantifiers::UserPatMode QuantifiersEngine::getInstUserPatMode() {
1363   if( options::userPatternsQuant()==quantifiers::USER_PAT_MODE_INTERLEAVE ){
1364     return d_ierCounter%2==0 ? quantifiers::USER_PAT_MODE_USE : quantifiers::USER_PAT_MODE_RESORT;
1365   }else{
1366     return options::userPatternsQuant();
1367   }
1368 }
1369
1370 void QuantifiersEngine::flushLemmas(){
1371   if( !d_lemmas_waiting.empty() ){
1372     //filter based on notify classes
1373     if( !d_inst_notify.empty() ){
1374       unsigned prev_lem_sz = d_lemmas_waiting.size();
1375       for( unsigned j=0; j<d_inst_notify.size(); j++ ){
1376         d_inst_notify[j]->filterInstantiations();
1377       }
1378       if( prev_lem_sz!=d_lemmas_waiting.size() ){
1379         Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting.size() << " / " << prev_lem_sz << std::endl;
1380       }
1381     }
1382     //take default output channel if none is provided
1383     d_hasAddedLemma = true;
1384     for( unsigned i=0; i<d_lemmas_waiting.size(); i++ ){
1385       Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting[i] << std::endl;
1386       getOutputChannel().lemma( d_lemmas_waiting[i], false, true );
1387     }
1388     d_lemmas_waiting.clear();
1389   }
1390   if( !d_phase_req_waiting.empty() ){
1391     for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){
1392       Trace("qe-lemma") << "Require phase : " << it->first << " -> " << it->second << std::endl;
1393       getOutputChannel().requirePhase( it->first, it->second );
1394     }
1395     d_phase_req_waiting.clear();
1396   }
1397 }
1398
1399 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) {
1400   //only if unsat core available
1401   bool isUnsatCoreAvailable = false;
1402   if( options::proof() ){
1403     isUnsatCoreAvailable = ProofManager::currentPM()->unsatCoreAvailable();
1404   }
1405   if( isUnsatCoreAvailable ){
1406     Trace("inst-unsat-core") << "Get instantiations in unsat core..." << std::endl;
1407     ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS, active_lemmas);
1408     if( Trace.isOn("inst-unsat-core") ){
1409       Trace("inst-unsat-core") << "Quantifiers lemmas in unsat core: " << std::endl;
1410       for (unsigned i = 0; i < active_lemmas.size(); ++i) {
1411         Trace("inst-unsat-core") << "  " << active_lemmas[i] << std::endl;
1412       }
1413       Trace("inst-unsat-core") << std::endl;
1414     }
1415     return true;
1416   }else{
1417     return false;
1418   }
1419 }
1420
1421 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp ) {
1422   if( getUnsatCoreLemmas( active_lemmas ) ){
1423     for (unsigned i = 0; i < active_lemmas.size(); ++i) {
1424       Node n = ProofManager::currentPM()->getWeakestImplicantInUnsatCore(active_lemmas[i]);
1425       if( n!=active_lemmas[i] ){
1426         Trace("inst-unsat-core") << "  weaken : " << active_lemmas[i] << " -> " << n << std::endl;
1427       }
1428       weak_imp[active_lemmas[i]] = n;
1429     }
1430     return true;
1431   }else{
1432     return false;
1433   }
1434 }
1435
1436 void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
1437   std::vector< Node > lemmas;
1438   getInstantiations( q, lemmas );
1439   std::map< Node, Node > quant;
1440   std::map< Node, std::vector< Node > > tvec;
1441   getExplanationForInstLemmas( lemmas, quant, tvec );
1442   for( std::map< Node, std::vector< Node > >::iterator it = tvec.begin(); it != tvec.end(); ++it ){
1443     tvecs.push_back( it->second );
1444   }
1445 }
1446
1447 void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
1448   if( options::incrementalSolving() ){
1449     for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
1450       getInstantiationTermVectors( it->first, insts[it->first] );
1451     }
1452   }else{
1453     for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
1454       getInstantiationTermVectors( it->first, insts[it->first] );
1455     }
1456   }
1457 }
1458
1459 void QuantifiersEngine::getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) {
1460   if( options::trackInstLemmas() ){
1461     if( options::incrementalSolving() ){
1462       for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
1463         it->second->getExplanationForInstLemmas( it->first, lems, quant, tvec );
1464       }
1465     }else{
1466       for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
1467         it->second.getExplanationForInstLemmas( it->first, lems, quant, tvec );
1468       }
1469     }
1470 #ifdef CVC4_ASSERTIONS
1471     for( unsigned j=0; j<lems.size(); j++ ){
1472       Assert( quant.find( lems[j] )!=quant.end() );
1473       Assert( tvec.find( lems[j] )!=tvec.end() );
1474     }
1475 #endif
1476   }else{
1477     Assert( false );
1478   }
1479 }
1480
1481 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
1482   bool useUnsatCore = false;
1483   std::vector< Node > active_lemmas;
1484   if( options::trackInstLemmas() && getUnsatCoreLemmas( active_lemmas ) ){
1485     useUnsatCore = true;
1486   }
1487
1488   bool printed = false;
1489   for( BoolMap::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){
1490     Node q = (*it).first;
1491     printed = true;
1492     out << "(skolem " << q << std::endl;
1493     out << "  ( ";
1494     for( unsigned i=0; i<d_term_db->d_skolem_constants[q].size(); i++ ){
1495       if( i>0 ){ out << " "; }
1496       out << d_term_db->d_skolem_constants[q][i];
1497     }
1498     out << " )" << std::endl;
1499     out << ")" << std::endl;
1500   }
1501   if( options::incrementalSolving() ){
1502     for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
1503       bool firstTime = true;
1504       it->second->print( out, it->first, firstTime, useUnsatCore, active_lemmas );
1505       if( !firstTime ){
1506         out << ")" << std::endl;
1507       }
1508       printed = printed || !firstTime;
1509     }
1510   }else{
1511     for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
1512       bool firstTime = true;
1513       it->second.print( out, it->first, firstTime, useUnsatCore, active_lemmas );
1514       if( !firstTime ){
1515         out << ")" << std::endl;
1516       }
1517       printed = printed || !firstTime;
1518     }
1519   }
1520   if( !printed ){
1521     out << "No instantiations" << std::endl;
1522   }
1523 }
1524
1525 void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
1526   if( d_ceg_inst ){
1527     d_ceg_inst->printSynthSolution( out );
1528   }else{
1529     out << "Internal error : module for synth solution not found." << std::endl;
1530   }
1531 }
1532
1533 void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
1534   if( options::incrementalSolving() ){
1535     for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
1536       qs.push_back( it->first );
1537     }
1538   }else{
1539     for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
1540       qs.push_back( it->first );
1541     }
1542   }
1543 }
1544
1545 void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
1546   bool useUnsatCore = false;
1547   std::vector< Node > active_lemmas;
1548   if( options::trackInstLemmas() && getUnsatCoreLemmas( active_lemmas ) ){
1549     useUnsatCore = true;
1550   }
1551
1552   if( options::incrementalSolving() ){
1553     for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
1554       it->second->getInstantiations( insts[it->first], it->first, this, useUnsatCore, active_lemmas );
1555     }
1556   }else{
1557     for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
1558       it->second.getInstantiations( insts[it->first], it->first, this, useUnsatCore, active_lemmas );
1559     }
1560   }
1561 }
1562
1563 void QuantifiersEngine::getInstantiations( Node q, std::vector< Node >& insts  ) {
1564   if( options::incrementalSolving() ){
1565     std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
1566     if( it!=d_c_inst_match_trie.end() ){
1567       std::vector< Node > active_lemmas;
1568       it->second->getInstantiations( insts, it->first, this, false, active_lemmas );
1569     }
1570   }else{
1571     std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.find( q );
1572     if( it!=d_inst_match_trie.end() ){
1573       std::vector< Node > active_lemmas;
1574       it->second.getInstantiations( insts, it->first, this, false, active_lemmas );
1575     }
1576   }
1577 }
1578
1579 Node QuantifiersEngine::getInstantiatedConjunction( Node q ) {
1580   Assert( q.getKind()==FORALL );
1581   std::vector< Node > insts;
1582   getInstantiations( q, insts );
1583   if( insts.empty() ){
1584     return NodeManager::currentNM()->mkConst(true);
1585   }else{
1586     Node ret;
1587     if( insts.size()==1 ){
1588       ret = insts[0];
1589     }else{
1590       ret = NodeManager::currentNM()->mkNode( kind::AND, insts );
1591     }
1592     //have to remove q, TODO: avoid this in a better way
1593     TNode tq = q;
1594     TNode tt = d_term_db->d_true;
1595     ret = ret.substitute( tq, tt );
1596     return ret;
1597   }
1598 }
1599
1600 QuantifiersEngine::Statistics::Statistics()
1601     : d_time("theory::QuantifiersEngine::time"),
1602       d_qcf_time("theory::QuantifiersEngine::time_qcf"),
1603       d_ematching_time("theory::QuantifiersEngine::time_ematching"),
1604       d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
1605       d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
1606       d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
1607       d_instantiations("QuantifiersEngine::Instantiations_Total", 0),
1608       d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0),
1609       d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0),
1610       d_inst_duplicate_ent("QuantifiersEngine::Duplicate_Inst_Entailed", 0),
1611       d_inst_duplicate_model_true("QuantifiersEngine::Duplicate_Inst_Model_True", 0),
1612       d_triggers("QuantifiersEngine::Triggers", 0),
1613       d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
1614       d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
1615       d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
1616       d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
1617       d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
1618       d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
1619       d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
1620       d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0),
1621       d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0),
1622       d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0),
1623       d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0),
1624       d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0),
1625       d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0)
1626 {
1627   smtStatisticsRegistry()->registerStat(&d_time);
1628   smtStatisticsRegistry()->registerStat(&d_qcf_time);
1629   smtStatisticsRegistry()->registerStat(&d_ematching_time);
1630   smtStatisticsRegistry()->registerStat(&d_num_quant);
1631   smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
1632   smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
1633   smtStatisticsRegistry()->registerStat(&d_instantiations);
1634   smtStatisticsRegistry()->registerStat(&d_inst_duplicate);
1635   smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq);
1636   smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent);
1637   smtStatisticsRegistry()->registerStat(&d_inst_duplicate_model_true);
1638   smtStatisticsRegistry()->registerStat(&d_triggers);
1639   smtStatisticsRegistry()->registerStat(&d_simple_triggers);
1640   smtStatisticsRegistry()->registerStat(&d_multi_triggers);
1641   smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations);
1642   smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
1643   smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns);
1644   smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen);
1645   smtStatisticsRegistry()->registerStat(&d_instantiations_guess);
1646   smtStatisticsRegistry()->registerStat(&d_instantiations_qcf);
1647   smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop);
1648   smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh);
1649   smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi);
1650   smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi);
1651   smtStatisticsRegistry()->registerStat(&d_instantiations_rr);
1652 }
1653
1654 QuantifiersEngine::Statistics::~Statistics(){
1655   smtStatisticsRegistry()->unregisterStat(&d_time);
1656   smtStatisticsRegistry()->unregisterStat(&d_qcf_time);
1657   smtStatisticsRegistry()->unregisterStat(&d_ematching_time);
1658   smtStatisticsRegistry()->unregisterStat(&d_num_quant);
1659   smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
1660   smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
1661   smtStatisticsRegistry()->unregisterStat(&d_instantiations);
1662   smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate);
1663   smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq);
1664   smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent);
1665   smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_model_true);
1666   smtStatisticsRegistry()->unregisterStat(&d_triggers);
1667   smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
1668   smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
1669   smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations);
1670   smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
1671   smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns);
1672   smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen);
1673   smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess);
1674   smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf);
1675   smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop);
1676   smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh);
1677   smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi);
1678   smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi);
1679   smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr);
1680 }
1681
1682 eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
1683   return d_te->getMasterEqualityEngine();
1684 }
1685
1686 eq::EqualityEngine* QuantifiersEngine::getActiveEqualityEngine() {
1687   if( d_useModelEe ){
1688     return d_model->d_equalityEngine;
1689   }else{
1690     return d_te->getMasterEqualityEngine();
1691   }
1692 }
1693
1694 Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
1695   bool prevModelEe = d_useModelEe;
1696   d_useModelEe = false;
1697   Node ret = d_eq_query->getInternalRepresentative( a, q, index );
1698   d_useModelEe = prevModelEe;
1699   return ret;
1700 }
1701
1702 void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
1703   eq::EqualityEngine* ee = getActiveEqualityEngine();
1704   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
1705   std::map< TypeNode, int > typ_num;
1706   while( !eqcs_i.isFinished() ){
1707     TNode r = (*eqcs_i);
1708     TypeNode tr = r.getType();
1709     if( typ_num.find( tr )==typ_num.end() ){
1710       typ_num[tr] = 0;
1711     }
1712     typ_num[tr]++;
1713     bool firstTime = true;
1714     Trace(c) << "  " << r;
1715     Trace(c) << " : { ";
1716     eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
1717     while( !eqc_i.isFinished() ){
1718       TNode n = (*eqc_i);
1719       if( r!=n ){
1720         if( firstTime ){
1721           Trace(c) << std::endl;
1722           firstTime = false;
1723         }
1724         Trace(c) << "    " << n << std::endl;
1725       }
1726       ++eqc_i;
1727     }
1728     if( !firstTime ){ Trace(c) << "  "; }
1729     Trace(c) << "}" << std::endl;
1730     ++eqcs_i;
1731   }
1732   Trace(c) << std::endl;
1733   for( std::map< TypeNode, int >::iterator it = typ_num.begin(); it != typ_num.end(); ++it ){
1734     Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl;
1735   }
1736 }
1737
1738
1739 EqualityQueryQuantifiersEngine::EqualityQueryQuantifiersEngine( context::Context* c, QuantifiersEngine* qe ) : d_qe( qe ), d_eqi_counter( c ), d_reset_count( 0 ){
1740   if( options::inferArithTriggerEq() ){
1741     d_eq_inference = new quantifiers::EqualityInference( c, options::inferArithTriggerEqExp() );
1742   }else{
1743     d_eq_inference = NULL;
1744   }
1745 }
1746
1747 EqualityQueryQuantifiersEngine::~EqualityQueryQuantifiersEngine(){
1748   delete d_eq_inference;
1749 }
1750
1751 bool EqualityQueryQuantifiersEngine::reset( Theory::Effort e ){
1752   d_int_rep.clear();
1753   d_reset_count++;
1754   return processInferences( e );
1755 }
1756
1757 bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) {
1758   if( options::inferArithTriggerEq() ){
1759     eq::EqualityEngine* ee = getEngine();
1760     //updated implementation
1761     while( d_eqi_counter.get()<d_eq_inference->getNumPendingMerges() ){
1762       Node eq = d_eq_inference->getPendingMerge( d_eqi_counter.get() );
1763       Node eq_exp = d_eq_inference->getPendingMergeExplanation( d_eqi_counter.get() );
1764       Trace("quant-engine-ee-proc") << "processInferences : Infer : " << eq << std::endl;
1765       Trace("quant-engine-ee-proc") << "      explanation : " << eq_exp << std::endl;
1766       Assert( ee->hasTerm( eq[0] ) );
1767       Assert( ee->hasTerm( eq[1] ) );
1768       if( areDisequal( eq[0], eq[1] ) ){
1769         Trace("quant-engine-ee-proc") << "processInferences : Conflict : " << eq << std::endl;
1770         if( Trace.isOn("term-db-lemma") ){
1771           Trace("term-db-lemma") << "Disequal terms, equal by normalization : " << eq[0] << " " << eq[1] << "!!!!" << std::endl;
1772           if( !d_qe->getTheoryEngine()->needCheck() ){
1773             Trace("term-db-lemma") << "  all theories passed with no lemmas." << std::endl;
1774             //this should really never happen (implies arithmetic is incomplete when sharing is enabled)
1775             Assert( false );
1776           }
1777           Trace("term-db-lemma") << "  add split on : " << eq << std::endl;
1778         }
1779         d_qe->addSplit( eq );
1780         return false;
1781       }else{
1782         ee->assertEquality( eq, true, eq_exp );
1783         d_eqi_counter = d_eqi_counter.get() + 1;
1784       }
1785     }
1786     Assert( ee->consistent() );
1787   }
1788   return true;
1789 }
1790
1791 bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
1792   return getEngine()->hasTerm( a );
1793 }
1794
1795 Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){
1796   eq::EqualityEngine* ee = getEngine();
1797   if( ee->hasTerm( a ) ){
1798     return ee->getRepresentative( a );
1799   }else{
1800     return a;
1801   }
1802 }
1803
1804 bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
1805   if( a==b ){
1806     return true;
1807   }else{
1808     eq::EqualityEngine* ee = getEngine();
1809     if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
1810       return ee->areEqual( a, b );
1811     }else{
1812       return false;
1813     }
1814   }
1815 }
1816
1817 bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
1818   if( a==b ){
1819     return false;
1820   }else{
1821     eq::EqualityEngine* ee = getEngine();
1822     if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
1823       return ee->areDisequal( a, b, false );
1824     }else{
1825       return a.isConst() && b.isConst();
1826     }
1827   }
1828 }
1829
1830 Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
1831   Assert( f.isNull() || f.getKind()==FORALL );
1832   Node r = getRepresentative( a );
1833   if( options::finiteModelFind() ){
1834     if( r.isConst() && quantifiers::TermDb::containsUninterpretedConstant( r ) ){
1835       //map back from values assigned by model, if any
1836       if( d_qe->getModel() ){
1837         std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r );
1838         if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){
1839           r = it->second;
1840           r = getRepresentative( r );
1841         }else{
1842           if( r.getType().isSort() ){
1843             Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
1844             //should never happen : UF constants should never escape model
1845             Assert( false );
1846           }
1847         }
1848       }
1849     }
1850   }
1851   if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE ){
1852     return r;
1853   }else{
1854     TypeNode v_tn = f.isNull() ? a.getType() : f[0][index].getType();
1855     std::map< Node, Node >::iterator itir = d_int_rep[v_tn].find( r );
1856     if( itir==d_int_rep[v_tn].end() ){
1857       //find best selection for representative
1858       Node r_best;
1859       //if( options::fmfRelevantDomain() && !f.isNull() ){
1860       //  Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
1861       //  r_best = d_qe->getRelevantDomain()->getRelevantTerm( f, index, r );
1862       //  Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
1863       //}
1864       std::vector< Node > eqc;
1865       getEquivalenceClass( r, eqc );
1866       Trace("internal-rep-select") << "Choose representative for equivalence class : { ";
1867       for( unsigned i=0; i<eqc.size(); i++ ){
1868         if( i>0 ) Trace("internal-rep-select") << ", ";
1869         Trace("internal-rep-select") << eqc[i];
1870       }
1871       Trace("internal-rep-select")  << " }, type = " << v_tn << std::endl;
1872       int r_best_score = -1;
1873       for( size_t i=0; i<eqc.size(); i++ ){
1874         int score = getRepScore( eqc[i], f, index, v_tn );
1875         if( score!=-2 ){
1876           if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
1877             r_best = eqc[i];
1878             r_best_score = score;
1879           }
1880         }
1881       }
1882       if( r_best.isNull() ){
1883         Trace("internal-rep-warn") << "No valid choice for representative in eqc class." << std::endl;
1884         r_best = r;
1885       }
1886       //now, make sure that no other member of the class is an instance
1887       std::unordered_map<TNode, Node, TNodeHashFunction> cache;
1888       r_best = getInstance( r_best, eqc, cache );
1889       //store that this representative was chosen at this point
1890       if( d_rep_score.find( r_best )==d_rep_score.end() ){
1891         d_rep_score[ r_best ] = d_reset_count;
1892       }
1893       Trace("internal-rep-select") << "...Choose " << r_best << " with score " << r_best_score << std::endl;
1894       Assert( r_best.getType().isSubtypeOf( v_tn ) );
1895       d_int_rep[v_tn][r] = r_best;
1896       if( r_best!=a ){
1897         Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
1898         Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
1899       }
1900       return r_best;
1901     }else{
1902       return itir->second;
1903     }
1904   }
1905 }
1906
1907 void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ) {
1908   //make sure internal representatives currently exist
1909   for( std::map< TypeNode, std::vector< Node > >::iterator it = reps.begin(); it != reps.end(); ++it ){
1910     if( it->first.isSort() ){
1911       for( unsigned i=0; i<it->second.size(); i++ ){
1912         Node r = getInternalRepresentative( it->second[i], Node::null(), 0 );
1913       }
1914     }
1915   }
1916   Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl;
1917   for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
1918     for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
1919       Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
1920     }
1921   }
1922   //store representatives for newly created terms
1923   std::map< Node, Node > temp_rep_map;
1924
1925   bool success;
1926   do {
1927     success = false;
1928     for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
1929       for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
1930         if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){
1931           Node ni = it->second;
1932           std::vector< Node > cc;
1933           cc.push_back( it->second.getOperator() );
1934           bool changed = false;
1935           for( unsigned j=0; j<ni.getNumChildren(); j++ ){
1936             if( ni[j].getType().isSort() ){
1937               Node r = getRepresentative( ni[j] );
1938               if( itt->second.find( r )==itt->second.end() ){
1939                 Assert( temp_rep_map.find( r )!=temp_rep_map.end() );
1940                 r = temp_rep_map[r];
1941               }
1942               if( r==ni ){
1943                 //found sub-term as instance
1944                 Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl;
1945                 itt->second[it->first] = ni[j];
1946                 changed = false;
1947                 success = true;
1948                 break;
1949               }else{
1950                 Node ir = itt->second[r];
1951                 cc.push_back( ir );
1952                 if( ni[j]!=ir ){
1953                   changed = true;
1954                 }
1955               }
1956             }else{
1957               changed = false;
1958               break;
1959             }
1960           }
1961           if( changed ){
1962             Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc );
1963             Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl;
1964             success = true;
1965             itt->second[it->first] = n;
1966             temp_rep_map[n] = it->first;
1967           }
1968         }
1969       }
1970     }
1971   }while( success );
1972   Trace("internal-rep-flatten") << "---After flattening : " << std::endl;
1973   for( std::map< TypeNode, std::map< Node, Node > >::iterator itt = d_int_rep.begin(); itt != d_int_rep.end(); ++itt ){
1974     for( std::map< Node, Node >::iterator it = itt->second.begin(); it != itt->second.end(); ++it ){
1975       Trace("internal-rep-flatten") << itt->first << " : irep( " << it->first << " ) = " << it->second << std::endl;
1976     }
1977   }
1978 }
1979
1980 eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
1981   return d_qe->getActiveEqualityEngine();
1982 }
1983
1984 void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
1985   eq::EqualityEngine* ee = getEngine();
1986   if( ee->hasTerm( a ) ){
1987     Node rep = ee->getRepresentative( a );
1988     eq::EqClassIterator eqc_iter( rep, ee );
1989     while( !eqc_iter.isFinished() ){
1990       eqc.push_back( *eqc_iter );
1991       eqc_iter++;
1992     }
1993   }else{
1994     eqc.push_back( a );
1995   }
1996   //a should be in its equivalence class
1997   Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
1998 }
1999
2000 TNode EqualityQueryQuantifiersEngine::getCongruentTerm( Node f, std::vector< TNode >& args ) {
2001   return d_qe->getTermDatabase()->getCongruentTerm( f, args );
2002 }
2003
2004 //helper functions
2005
2006 Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::unordered_map<TNode, Node, TNodeHashFunction>& cache ){
2007   if(cache.find(n) != cache.end()) {
2008     return cache[n];
2009   }
2010   for( size_t i=0; i<n.getNumChildren(); i++ ){
2011     Node nn = getInstance( n[i], eqc, cache );
2012     if( !nn.isNull() ){
2013       return cache[n] = nn;
2014     }
2015   }
2016   if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){
2017     return cache[n] = n;
2018   }else{
2019     return cache[n] = Node::null();
2020   }
2021 }
2022
2023 //-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
2024 int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index, TypeNode v_tn ){
2025   if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){  //reject
2026     return -2;
2027   }else if( !n.getType().isSubtypeOf( v_tn ) ){  //reject if incorrect type
2028     return -2;
2029   }else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){
2030     return -1;
2031   }else if( options::instMaxLevel()!=-1 ){
2032     //score prefer lowest instantiation level
2033     if( n.hasAttribute(InstLevelAttribute()) ){
2034       return n.getAttribute(InstLevelAttribute());
2035     }else{
2036       return options::instLevelInputOnly() ? -1 : 0;
2037     }
2038   }else{
2039     if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_FIRST ){
2040       //score prefers earliest use of this term as a representative
2041       return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
2042     }else{
2043       Assert( options::quantRepMode()==quantifiers::QUANT_REP_MODE_DEPTH );
2044       return quantifiers::TermDb::getTermDepth( n );
2045     }
2046   }
2047 }