src/theory/quantifiers_engine.cpp

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