src/theory/quantifiers_engine.cpp

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