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