src/theory/quantifiers_engine.cpp

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