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