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