src/theory/quantifiers_engine.cpp

   1 /*********************                                                        */
   2 /*! \file quantifiers_engine.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Andrew Reynolds
   6  ** Minor contributors (to current version): Francois Bobot
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Implementation of quantifiers engine class
  13  **/
  14
  15 #include "theory/quantifiers_engine.h"
  16 #include "theory/theory_engine.h"
  17 #include "theory/uf/theory_uf_strong_solver.h"
  18 #include "theory/uf/equality_engine.h"
  19 #include "theory/arrays/theory_arrays.h"
  20 #include "theory/datatypes/theory_datatypes.h"
  21 #include "theory/quantifiers/quantifiers_rewriter.h"
  22 #include "theory/quantifiers/options.h"
  23 #include "theory/quantifiers/model_engine.h"
  24 #include "theory/quantifiers/instantiation_engine.h"
  25 #include "theory/quantifiers/first_order_model.h"
  26 #include "theory/quantifiers/term_database.h"
  27 #include "theory/quantifiers/trigger.h"
  28 #include "theory/quantifiers/bounded_integers.h"
  29 #include "theory/quantifiers/rewrite_engine.h"
  30 #include "theory/quantifiers/quant_conflict_find.h"
  31 #include "theory/quantifiers/conjecture_generator.h"
  32 #include "theory/quantifiers/ce_guided_instantiation.h"
  33 #include "theory/quantifiers/local_theory_ext.h"
  34 #include "theory/quantifiers/relevant_domain.h"
  35 #include "theory/uf/options.h"
  36 #include "theory/uf/theory_uf.h"
  37 #include "theory/quantifiers/full_model_check.h"
  38 #include "theory/quantifiers/ambqi_builder.h"
  39
  40 using namespace std;
  41 using namespace CVC4;
  42 using namespace CVC4::kind;
  43 using namespace CVC4::context;
  44 using namespace CVC4::theory;
  45 using namespace CVC4::theory::inst;
  46
  47
  48 eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {
  49   return d_quantEngine->getMasterEqualityEngine();
  50 }
  51
  52 bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) {
  53   eq::EqualityEngine * ee = getEqualityEngine();
  54   return n1==n2 || ( ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areEqual( n1, n2 ) );
  55 }
  56
  57 bool QuantifiersModule::areDisequal( TNode n1, TNode n2 ) {
  58   eq::EqualityEngine * ee = getEqualityEngine();
  59   return n1!=n2 && ee->hasTerm( n1 ) && ee->hasTerm( n2 ) && ee->areDisequal( n1, n2, false );
  60 }
  61
  62 TNode QuantifiersModule::getRepresentative( TNode n ) {
  63   eq::EqualityEngine * ee = getEqualityEngine();
  64   if( ee->hasTerm( n ) ){
  65     return ee->getRepresentative( n );
  66   }else{
  67     return n;
  68   }
  69 }
  70
  71 quantifiers::TermDb * QuantifiersModule::getTermDatabase() {
  72   return d_quantEngine->getTermDatabase();
  73 }
  74
  75 QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
  76 d_te( te ),
  77 d_lemmas_produced_c(u){
  78   d_eq_query = new EqualityQueryQuantifiersEngine( this );
  79   d_term_db = new quantifiers::TermDb( c, u, this );
  80   d_tr_trie = new inst::TriggerTrie;
  81   //d_rr_tr_trie = new rrinst::TriggerTrie;
  82   //d_eem = new EfficientEMatcher( this );
  83   d_hasAddedLemma = false;
  84
  85   bool needsBuilder = false;
  86
  87   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
  88
  89   //the model object
  90   if( options::mbqiMode()==quantifiers::MBQI_FMC ||
  91       options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() ||
  92       options::mbqiMode()==quantifiers::MBQI_TRUST ){
  93     d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
  94   }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
  95     d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" );
  96   }else{
  97     d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
  98   }
  99   if( !options::finiteModelFind() ){
 100     d_rel_dom = new quantifiers::RelevantDomain( this, d_model );
 101   }else{
 102     d_rel_dom = NULL;
 103   }
 104   if( options::relevantTriggers() ){
 105     d_quant_rel = new QuantRelevance( false );
 106   }else{
 107     d_quant_rel = NULL;
 108   }
 109
 110   //add quantifiers modules
 111   if( options::quantConflictFind() || options::quantRewriteRules() ){
 112     d_qcf = new quantifiers::QuantConflictFind( this, c);
 113     d_modules.push_back( d_qcf );
 114   }else{
 115     d_qcf = NULL;
 116   }
 117   if( options::conjectureGen() ){
 118     d_sg_gen = new quantifiers::ConjectureGenerator( this, c );
 119     d_modules.push_back( d_sg_gen );
 120   }else{
 121     d_sg_gen = NULL;
 122   }
 123   if( !options::finiteModelFind() || options::fmfInstEngine() ){
 124     //the instantiation must set incomplete flag unless finite model finding is turned on
 125     d_inst_engine = new quantifiers::InstantiationEngine( this, !options::finiteModelFind() );
 126     d_modules.push_back(  d_inst_engine );
 127   }else{
 128     d_inst_engine = NULL;
 129   }
 130   if( options::finiteModelFind()  ){
 131     if( options::fmfBoundInt() ){
 132       d_bint = new quantifiers::BoundedIntegers( c, this );
 133       d_modules.push_back( d_bint );
 134     }else{
 135       d_bint = NULL;
 136     }
 137     d_model_engine = new quantifiers::ModelEngine( c, this );
 138     d_modules.push_back( d_model_engine );
 139     needsBuilder = true;
 140   }else{
 141     d_model_engine = NULL;
 142     d_bint = NULL;
 143   }
 144   if( options::quantRewriteRules() ){
 145     d_rr_engine = new quantifiers::RewriteEngine( c, this );
 146     d_modules.push_back(d_rr_engine);
 147   }else{
 148     d_rr_engine = NULL;
 149   }
 150   if( options::ceGuidedInst() ){
 151     d_ceg_inst = new quantifiers::CegInstantiation( this, c );
 152     d_modules.push_back( d_ceg_inst );
 153     needsBuilder = true;
 154   }else{
 155     d_ceg_inst = NULL;
 156   }
 157   if( options::ltePartialInst() ){
 158     d_lte_part_inst = new quantifiers::LtePartialInst( this, c );
 159     d_modules.push_back( d_lte_part_inst );
 160   }else{
 161     d_lte_part_inst = NULL;
 162   }
 163
 164   if( needsBuilder ){
 165     Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
 166     if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ||
 167         options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBoundInt() ){
 168       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
 169       d_builder = new quantifiers::fmcheck::FullModelChecker( c, this );
 170     }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
 171       Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl;
 172       d_builder = new quantifiers::AbsMbqiBuilder( c, this );
 173     }else{
 174       Trace("quant-engine-debug") << "...make default model builder." << std::endl;
 175       d_builder = new quantifiers::QModelBuilderDefault( c, this );
 176     }
 177   }else{
 178     d_builder = NULL;
 179   }
 180
 181   d_total_inst_count_debug = 0;
 182   d_ierCounter = 0;
 183   d_ierCounter_lc = 0;
 184 }
 185
 186 QuantifiersEngine::~QuantifiersEngine(){
 187   delete d_builder;
 188   delete d_rr_engine;
 189   delete d_bint;
 190   delete d_model_engine;
 191   delete d_inst_engine;
 192   delete d_qcf;
 193   delete d_quant_rel;
 194   delete d_rel_dom;
 195   delete d_model;
 196   delete d_tr_trie;
 197   delete d_term_db;
 198   delete d_eq_query;
 199   delete d_sg_gen;
 200   delete d_ceg_inst;
 201   delete d_lte_part_inst;
 202   for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) {
 203     delete (*i).second;
 204   }
 205 }
 206
 207 EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() {
 208   return d_eq_query;
 209 }
 210
 211 context::Context* QuantifiersEngine::getSatContext(){
 212   return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext();
 213 }
 214
 215 context::Context* QuantifiersEngine::getUserContext(){
 216   return d_te->theoryOf( THEORY_QUANTIFIERS )->getUserContext();
 217 }
 218
 219 OutputChannel& QuantifiersEngine::getOutputChannel(){
 220   return d_te->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel();
 221 }
 222 /** get default valuation for the quantifiers engine */
 223 Valuation& QuantifiersEngine::getValuation(){
 224   return d_te->theoryOf( THEORY_QUANTIFIERS )->getValuation();
 225 }
 226
 227 void QuantifiersEngine::finishInit(){
 228   for( int i=0; i<(int)d_modules.size(); i++ ){
 229     d_modules[i]->finishInit();
 230   }
 231 }
 232
 233 QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
 234   std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q );
 235   if( it==d_owner.end() ){
 236     return NULL;
 237   }else{
 238     return it->second;
 239   }
 240 }
 241
 242 void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m ) {
 243   QuantifiersModule * mo = getOwner( q );
 244   if( mo!=m ){
 245     if( mo!=NULL ){
 246       Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << "!" << std::endl;
 247     }
 248     d_owner[q] = m;
 249   }
 250 }
 251
 252 bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
 253   QuantifiersModule * mo = getOwner( q );
 254   return mo==m || mo==NULL;
 255 }
 256
 257 void QuantifiersEngine::check( Theory::Effort e ){
 258   CodeTimer codeTimer(d_time);
 259   if( !getMasterEqualityEngine()->consistent() ){
 260     Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
 261     return;
 262   }
 263   if( e==Theory::EFFORT_FULL ){
 264     d_ierCounter++;
 265   }else if( e==Theory::EFFORT_LAST_CALL ){
 266     d_ierCounter_lc++;
 267   }
 268   bool needsCheck = !d_lemmas_waiting.empty();
 269   bool needsModel = false;
 270   bool needsFullModel = false;
 271   std::vector< QuantifiersModule* > qm;
 272   if( d_model->checkNeeded() ){
 273     needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
 274     for( int i=0; i<(int)d_modules.size(); i++ ){
 275       if( d_modules[i]->needsCheck( e ) ){
 276         qm.push_back( d_modules[i] );
 277         needsCheck = true;
 278         if( d_modules[i]->needsModel( e ) ){
 279           needsModel = true;
 280           if( d_modules[i]->needsFullModel( e ) ){
 281             needsFullModel = true;
 282           }
 283         }
 284       }
 285     }
 286   }
 287   if( needsCheck ){
 288     Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
 289     if( Trace.isOn("quant-engine-debug") ){
 290       Trace("quant-engine-debug") << "  modules to check : ";
 291       for( unsigned i=0; i<qm.size(); i++ ){
 292         Trace("quant-engine-debug") << qm[i]->identify() << " ";
 293       }
 294       Trace("quant-engine-debug") << std::endl;
 295       Trace("quant-engine-debug") << "  # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
 296       if( d_model->getNumToReduceQuantifiers()>0 ){
 297         Trace("quant-engine-debug") << "  # quantified formulas to reduce = " << d_model->getNumToReduceQuantifiers() << std::endl;
 298       }
 299       if( !d_lemmas_waiting.empty() ){
 300         Trace("quant-engine-debug") << "  lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
 301       }
 302       Trace("quant-engine-debug") << "  Theory engine finished : " << !d_te->needCheck() << std::endl;
 303       Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
 304     }
 305     if( Trace.isOn("quant-engine-ee") ){
 306       Trace("quant-engine-ee") << "Equality engine : " << std::endl;
 307       debugPrintEqualityEngine( "quant-engine-ee" );
 308     }
 309
 310     //reset relevant information
 311     d_conflict = false;
 312     d_hasAddedLemma = false;
 313
 314     //flush previous lemmas (for instance, if was interupted), or other lemmas to process
 315     flushLemmas();
 316     if( d_hasAddedLemma ){
 317       return;
 318     }
 319
 320     Trace("quant-engine-debug2") << "Reset term db..." << std::endl;
 321     d_term_db->reset( e );
 322     d_eq_query->reset();
 323     if( d_rel_dom ){
 324       d_rel_dom->reset();
 325     }
 326     d_model->reset_round();
 327     for( unsigned i=0; i<d_modules.size(); i++ ){
 328       Trace("quant-engine-debug2") << "Reset " << d_modules[i]->identify().c_str() << std::endl;
 329       d_modules[i]->reset_round( e );
 330     }
 331     Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
 332
 333     if( e==Theory::EFFORT_LAST_CALL ){
 334       //if effort is last call, try to minimize model first FIXME: remove?
 335       uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
 336       if( ufss && !ufss->minimize() ){
 337         return;
 338       }
 339       ++(d_statistics.d_instantiation_rounds_lc);
 340     }else if( e==Theory::EFFORT_FULL ){
 341       ++(d_statistics.d_instantiation_rounds);
 342     }
 343
 344     Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
 345     for( unsigned quant_e = QEFFORT_CONFLICT; quant_e<=QEFFORT_MODEL; quant_e++ ){
 346       bool success = true;
 347       //build the model if any module requested it
 348       if( quant_e==QEFFORT_MODEL && needsModel ){
 349         Assert( d_builder!=NULL );
 350         Trace("quant-engine-debug") << "Build model, fullModel = " << ( needsFullModel || d_builder->optBuildAtFullModel() ) << "..." << std::endl;
 351         d_builder->d_addedLemmas = 0;
 352         d_builder->buildModel( d_model, needsFullModel || d_builder->optBuildAtFullModel() );
 353         //we are done if model building was unsuccessful
 354         if( d_builder->d_addedLemmas>0 ){
 355           success = false;
 356         }
 357       }
 358       if( success ){
 359         //check each module
 360         for( unsigned i=0; i<qm.size(); i++ ){
 361           Trace("quant-engine-debug") << "Check " << qm[i]->identify().c_str() << " at effort " << quant_e << "..." << std::endl;
 362           qm[i]->check( e, quant_e );
 363         }
 364       }
 365       //flush all current lemmas
 366       flushLemmas();
 367       //if we have added one, stop
 368       if( d_hasAddedLemma ){
 369         break;
 370       //otherwise, complete the model generation if necessary
 371       }else if( quant_e==QEFFORT_MODEL && needsModel && options::produceModels() && !needsFullModel && !d_builder->optBuildAtFullModel() ){
 372         Trace("quant-engine-debug") << "Build completed model..." << std::endl;
 373         d_builder->buildModel( d_model, true );
 374       }
 375     }
 376     Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
 377     if( d_hasAddedLemma ){
 378       //debug information
 379       if( Trace.isOn("inst-per-quant-round") ){
 380         for( std::map< Node, int >::iterator it = d_temp_inst_debug.begin(); it != d_temp_inst_debug.end(); ++it ){
 381           Trace("inst-per-quant-round") << " * " << it->second << " for " << it->first << std::endl;
 382           d_temp_inst_debug[it->first] = 0;
 383         }
 384       }
 385     }
 386     Trace("quant-engine") << "Finished quantifiers engine check." << std::endl;
 387   }
 388   //SAT case
 389   if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
 390     if( options::produceModels() && !d_model->isModelSet() ){
 391       //use default model builder when no module built the model
 392       Trace("quant-engine-debug") << "Build the model..." << std::endl;
 393       d_te->getModelBuilder()->buildModel( d_model, true );
 394       Trace("quant-engine-debug") << "Done building the model." << std::endl;
 395     }
 396     //check other sources of incompleteness
 397     bool setInc = false;
 398     if( d_lte_part_inst && d_lte_part_inst->wasInvoked() ){
 399       setInc = true;
 400     }
 401     if( setInc ){
 402       getOutputChannel().setIncomplete();
 403     }
 404     //output debug stats
 405     if( Trace.isOn("inst-per-quant") ){
 406       for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){
 407         Trace("inst-per-quant") << " * " << it->second << " for " << it->first << std::endl;
 408       }
 409     }
 410   }
 411 }
 412
 413 bool QuantifiersEngine::registerQuantifier( Node f ){
 414   std::map< Node, bool >::iterator it = d_quants.find( f );
 415   if( it==d_quants.end() ){
 416     Trace("quant") << "QuantifiersEngine : Register quantifier ";
 417     Trace("quant") << " : " << f << std::endl;
 418     ++(d_statistics.d_num_quant);
 419     Assert( f.getKind()==FORALL );
 420
 421     //check whether we should apply a reduction
 422     bool reduced = false;
 423     if( d_lte_part_inst && !f.getAttribute(LtePartialInstAttribute()) ){
 424       Trace("lte-partial-inst") << "LTE: Partially instantiate " << f << "?" << std::endl;
 425       if( d_lte_part_inst->addQuantifier( f ) ){
 426         reduced = true;
 427       }
 428     }
 429     if( reduced ){
 430       d_model->assertQuantifier( f, true );
 431       d_quants[f] = false;
 432       return false;
 433     }else{
 434       //make instantiation constants for f
 435       d_term_db->makeInstantiationConstantsFor( f );
 436       d_term_db->computeAttributes( f );
 437       QuantifiersModule * qm = getOwner( f );
 438       if( qm!=NULL ){
 439         Trace("quant") << "   Owner : " << qm->identify() << std::endl;
 440       }
 441       //register with quantifier relevance
 442       if( d_quant_rel ){
 443         d_quant_rel->registerQuantifier( f );
 444       }
 445       //register with each module
 446       for( int i=0; i<(int)d_modules.size(); i++ ){
 447         d_modules[i]->registerQuantifier( f );
 448       }
 449       Node ceBody = d_term_db->getInstConstantBody( f );
 450       //generate the phase requirements
 451       d_phase_reqs[f] = new QuantPhaseReq( ceBody, true );
 452       //also register it with the strong solver
 453       if( options::finiteModelFind() ){
 454         ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f );
 455       }
 456       d_quants[f] = true;
 457       return true;
 458     }
 459   }else{
 460     return it->second;
 461   }
 462 }
 463
 464 void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
 465   for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){
 466     std::set< Node > added;
 467     getTermDatabase()->addTerm( *p, added );
 468   }
 469 }
 470
 471 void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
 472   if( !pol ){
 473     //do skolemization
 474     if( d_skolemized.find( f )==d_skolemized.end() ){
 475       Node body = d_term_db->getSkolemizedBody( f );
 476       NodeBuilder<> nb(kind::OR);
 477       nb << f << body.notNode();
 478       Node lem = nb;
 479       if( Trace.isOn("quantifiers-sk") ){
 480         Node slem = Rewriter::rewrite( lem );
 481         Trace("quantifiers-sk") << "Skolemize lemma : " << slem << std::endl;
 482       }
 483       getOutputChannel().lemma( lem, false, true );
 484       d_skolemized[f] = true;
 485     }
 486   }
 487   //assert to modules TODO : handle !pol
 488   if( pol ){
 489     //register the quantifier
 490     bool nreduced = registerQuantifier( f );
 491     //assert it to each module
 492     if( nreduced ){
 493       d_model->assertQuantifier( f );
 494       for( int i=0; i<(int)d_modules.size(); i++ ){
 495         d_modules[i]->assertNode( f );
 496       }
 497     }
 498   }
 499 }
 500
 501 void QuantifiersEngine::propagate( Theory::Effort level ){
 502   CodeTimer codeTimer(d_time);
 503
 504   for( int i=0; i<(int)d_modules.size(); i++ ){
 505     d_modules[i]->propagate( level );
 506   }
 507 }
 508
 509 Node QuantifiersEngine::getNextDecisionRequest(){
 510   for( int i=0; i<(int)d_modules.size(); i++ ){
 511     Node n = d_modules[i]->getNextDecisionRequest();
 512     if( !n.isNull() ){
 513       return n;
 514     }
 515   }
 516   return Node::null();
 517 }
 518
 519 quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() {
 520   return getTermDatabase()->getTermDatabaseSygus();
 521 }
 522
 523 void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
 524   std::set< Node > added;
 525   getTermDatabase()->addTerm( n, added, withinQuant, withinInstClosure );
 526   //maybe have triggered instantiations if we are doing eager instantiation
 527   if( options::eagerInstQuant() ){
 528     flushLemmas();
 529   }
 530   //added contains also the Node that just have been asserted in this branch
 531   if( d_quant_rel ){
 532     for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
 533       if( !withinQuant ){
 534         d_quant_rel->setRelevance( i->getOperator(), 0 );
 535       }
 536     }
 537   }
 538 }
 539
 540 void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ){
 541   for( size_t i=0; i<f[0].getNumChildren(); i++ ){
 542     Node n = m.get( i );
 543     if( !n.isNull() ){
 544       vars.push_back( f[0][i] );
 545       terms.push_back( n );
 546     }
 547   }
 548 }
 549
 550 bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
 551   Assert( f.getKind()==FORALL );
 552   Assert( vars.size()==terms.size() );
 553   Node body = getInstantiation( f, vars, terms );
 554   Trace("inst-assert") << "(assert " << body << ")" << std::endl;
 555   //make the lemma
 556   NodeBuilder<> nb(kind::OR);
 557   nb << f.notNode() << body;
 558   Node lem = nb;
 559   //check for duplication
 560   if( addLemma( lem ) ){
 561     d_total_inst_debug[f]++;
 562     d_temp_inst_debug[f]++;
 563     d_total_inst_count_debug++;
 564     Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
 565     for( int i=0; i<(int)terms.size(); i++ ){
 566       Trace("inst") << "   " << terms[i];
 567       Trace("inst") << std::endl;
 568       Assert( terms[i].getType().isSubtypeOf( f[0][i].getType() ) );
 569     }
 570     if( options::cbqi() && !options::cbqi2() ){
 571       for( int i=0; i<(int)terms.size(); i++ ){
 572         if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){
 573           Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl;
 574           for( int i=0; i<(int)terms.size(); i++ ){
 575             Debug("inst") << "   " << terms[i] << std::endl;
 576           }
 577           Unreachable("Bad instantiation");
 578         }
 579       }
 580     }
 581     if( options::instMaxLevel()!=-1 ){
 582       uint64_t maxInstLevel = 0;
 583       for( int i=0; i<(int)terms.size(); i++ ){
 584         if( terms[i].hasAttribute(InstLevelAttribute()) ){
 585           if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){
 586             maxInstLevel = terms[i].getAttribute(InstLevelAttribute());
 587           }
 588         }
 589       }
 590       setInstantiationLevelAttr( body, f[1], maxInstLevel+1 );
 591     }
 592     ++(d_statistics.d_instantiations);
 593     return true;
 594   }else{
 595     ++(d_statistics.d_inst_duplicate);
 596     return false;
 597   }
 598 }
 599
 600 void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t level ){
 601   Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level << std::endl;
 602   //if not from the vector of terms we instantiatied
 603   if( qn.getKind()!=BOUND_VARIABLE && n!=qn ){
 604     //if this is a new term, without an instantiation level
 605     if( !n.hasAttribute(InstLevelAttribute()) ){
 606       InstLevelAttribute ila;
 607       n.setAttribute(ila,level);
 608       Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
 609     }
 610     Assert( n.getNumChildren()==qn.getNumChildren() );
 611     for( int i=0; i<(int)n.getNumChildren(); i++ ){
 612       setInstantiationLevelAttr( n[i], qn[i], level );
 613     }
 614   }
 615 }
 616
 617 void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){
 618   if( !n.hasAttribute(InstLevelAttribute()) ){
 619     InstLevelAttribute ila;
 620     n.setAttribute(ila,level);
 621     Trace("inst-level-debug") << "Set instantiation level " << n << " to " << level << std::endl;
 622   }
 623   for( int i=0; i<(int)n.getNumChildren(); i++ ){
 624     setInstantiationLevelAttr( n[i], level );
 625   }
 626 }
 627
 628 Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms ){
 629   if( n.getKind()==INST_CONSTANT ){
 630     Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
 631     return terms[n.getAttribute(InstVarNumAttribute())];
 632   }else{
 633     //if( !quantifiers::TermDb::hasInstConstAttr( n ) ){
 634       //Debug("check-inst") << "No inst const attr : " << n << std::endl;
 635       //return n;
 636     //}else{
 637       //Debug("check-inst") << "Recurse on : " << n << std::endl;
 638     std::vector< Node > cc;
 639     if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
 640       cc.push_back( n.getOperator() );
 641     }
 642     bool changed = false;
 643     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 644       Node c = getSubstitute( n[i], terms );
 645       cc.push_back( c );
 646       changed = changed || c!=n[i];
 647     }
 648     if( changed ){
 649       Node ret = NodeManager::currentNM()->mkNode( n.getKind(), cc );
 650       return ret;
 651     }else{
 652       return n;
 653     }
 654   }
 655 }
 656
 657
 658 Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){
 659   Node body;
 660   //process partial instantiation if necessary
 661   if( d_term_db->d_vars[f].size()!=vars.size() ){
 662     body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
 663     std::vector< Node > uninst_vars;
 664     //doing a partial instantiation, must add quantifier for all uninstantiated variables
 665     for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
 666       if( std::find( vars.begin(), vars.end(), f[0][i] )==vars.end() ){
 667         uninst_vars.push_back( f[0][i] );
 668       }
 669     }
 670     Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, uninst_vars );
 671     body = NodeManager::currentNM()->mkNode( FORALL, bvl, body );
 672     Trace("partial-inst") << "Partial instantiation : " << f << std::endl;
 673     Trace("partial-inst") << "                      : " << body << std::endl;
 674   }else{
 675     if( options::cbqi() ){
 676       body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
 677     }else{
 678       //do optimized version
 679       Node icb = d_term_db->getInstConstantBody( f );
 680       body = getSubstitute( icb, terms );
 681       if( Debug.isOn("check-inst") ){
 682         Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
 683         if( body!=body2 ){
 684           Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl;
 685         }
 686       }
 687     }
 688   }
 689   return body;
 690 }
 691
 692 Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){
 693   std::vector< Node > vars;
 694   std::vector< Node > terms;
 695   computeTermVector( f, m, vars, terms );
 696   return getInstantiation( f, vars, terms );
 697 }
 698
 699 Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& terms ) {
 700   return getInstantiation( f, d_term_db->d_inst_constants[f], terms );
 701 }
 702
 703 /*
 704 bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
 705   if( options::incrementalSolving() ){
 706     if( d_c_inst_match_trie.find( f )!=d_c_inst_match_trie.end() ){
 707       if( d_c_inst_match_trie[f]->existsInstMatch( this, f, m, getUserContext(), modEq, modInst ) ){
 708         return true;
 709       }
 710     }
 711   }else{
 712     if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
 713       if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, modInst ) ){
 714         return true;
 715       }
 716     }
 717   }
 718   //also check model builder (it may contain instantiations internally)
 719   if( d_builder && d_builder->existsInstantiation( f, m, modEq, modInst ) ){
 720     return true;
 721   }
 722   return false;
 723 }
 724 */
 725
 726 bool QuantifiersEngine::addLemma( Node lem, bool doCache ){
 727   if( doCache ){
 728     lem = Rewriter::rewrite(lem);
 729     Trace("inst-add-debug2") << "Adding lemma : " << lem << std::endl;
 730     if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
 731       //d_curr_out->lemma( lem, false, true );
 732       d_lemmas_produced_c[ lem ] = true;
 733       d_lemmas_waiting.push_back( lem );
 734       Trace("inst-add-debug2") << "Added lemma : " << lem << std::endl;
 735       return true;
 736     }else{
 737       Trace("inst-add-debug2") << "Duplicate." << std::endl;
 738       return false;
 739     }
 740   }else{
 741     d_lemmas_waiting.push_back( lem );
 742     return true;
 743   }
 744 }
 745
 746 void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
 747   d_phase_req_waiting[lit] = req;
 748 }
 749
 750 bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst ){
 751   std::vector< Node > terms;
 752   m.getTerms( this, f, terms );
 753   return addInstantiation( f, terms, mkRep, modEq, modInst );
 754 }
 755
 756 bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst ) {
 757   // For resource-limiting (also does a time check).
 758   getOutputChannel().safePoint();
 759
 760   Assert( terms.size()==f[0].getNumChildren() );
 761   Trace("inst-add-debug") << "Add instantiation: ";
 762   for( unsigned i=0; i<terms.size(); i++ ){
 763     if( i>0 ) Trace("inst-add-debug") << ", ";
 764     Trace("inst-add-debug") << f[0][i] << " -> " << terms[i];
 765     //make it representative, this is helpful for recognizing duplication
 766     if( mkRep ){
 767       //pick the best possible representative for instantiation, based on past use and simplicity of term
 768       terms[i] = d_eq_query->getInternalRepresentative( terms[i], f, i );
 769       Trace("inst-add-debug2") << " (" << terms[i] << ")";
 770     }
 771   }
 772   Trace("inst-add-debug") << std::endl;
 773
 774   //check based on instantiation level
 775   if( options::instMaxLevel()!=-1 || options::lteRestrictInstClosure() ){
 776     for( unsigned i=0; i<terms.size(); i++ ){
 777       if( !d_term_db->isTermEligibleForInstantiation( terms[i], f, true ) ){
 778         return false;
 779       }
 780     }
 781   }
 782   //check for entailment
 783   if( options::instNoEntail() ){
 784     std::map< TNode, TNode > subs;
 785     for( unsigned i=0; i<terms.size(); i++ ){
 786       subs[f[0][i]] = terms[i];
 787     }
 788     if( d_term_db->isEntailed( f[1], subs, false, true ) ){
 789       Trace("inst-add-debug") << " -> Currently entailed." << std::endl;
 790       return false;
 791     }
 792   }
 793
 794   //check for duplication
 795   bool alreadyExists = false;
 796   if( options::incrementalSolving() ){
 797     Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl;
 798     inst::CDInstMatchTrie* imt;
 799     std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( f );
 800     if( it!=d_c_inst_match_trie.end() ){
 801       imt = it->second;
 802     }else{
 803       imt = new CDInstMatchTrie( getUserContext() );
 804       d_c_inst_match_trie[f] = imt;
 805     }
 806     alreadyExists = !imt->addInstMatch( this, f, terms, getUserContext(), modEq, modInst );
 807   }else{
 808     Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
 809     alreadyExists = !d_inst_match_trie[f].addInstMatch( this, f, terms, modEq, modInst );
 810   }
 811   if( alreadyExists ){
 812     Trace("inst-add-debug") << " -> Already exists." << std::endl;
 813     ++(d_statistics.d_inst_duplicate_eq);
 814     return false;
 815   }
 816
 817
 818   //add the instantiation
 819   Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
 820   bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms );
 821   //report the result
 822   if( addedInst ){
 823     Trace("inst-add-debug") << " -> Success." << std::endl;
 824     return true;
 825   }else{
 826     Trace("inst-add-debug") << " -> Lemma already exists." << std::endl;
 827     return false;
 828   }
 829 }
 830
 831
 832 bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
 833   n = Rewriter::rewrite( n );
 834   Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() );
 835   if( addLemma( lem ) ){
 836     Debug("inst") << "*** Add split " << n<< std::endl;
 837     return true;
 838   }
 839   return false;
 840 }
 841
 842 bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool reqPhasePol ){
 843   //Assert( !areEqual( n1, n2 ) );
 844   //Assert( !areDisequal( n1, n2 ) );
 845   Kind knd = n1.getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
 846   Node fm = NodeManager::currentNM()->mkNode( knd, n1, n2 );
 847   return addSplit( fm );
 848 }
 849
 850 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
 851   //determine if we should perform check, based on instWhenMode
 852   bool performCheck = false;
 853   if( options::instWhenMode()==quantifiers::INST_WHEN_FULL ){
 854     performCheck = ( e >= Theory::EFFORT_FULL );
 855   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){
 856     performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck();
 857   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){
 858     performCheck = ( ( e==Theory::EFFORT_FULL  && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
 859   }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){
 860     performCheck = ( e >= Theory::EFFORT_LAST_CALL );
 861   }else{
 862     performCheck = true;
 863   }
 864   if( e==Theory::EFFORT_LAST_CALL ){
 865     //with bounded integers, skip every other last call,
 866     // since matching loops may occur with infinite quantification
 867     if( d_ierCounter_lc%2==0 && options::fmfBoundInt() ){
 868       performCheck = false;
 869     }
 870   }
 871   return performCheck;
 872 }
 873
 874 void QuantifiersEngine::flushLemmas(){
 875   if( !d_lemmas_waiting.empty() ){
 876     //take default output channel if none is provided
 877     d_hasAddedLemma = true;
 878     for( int i=0; i<(int)d_lemmas_waiting.size(); i++ ){
 879       getOutputChannel().lemma( d_lemmas_waiting[i], false, true );
 880     }
 881     d_lemmas_waiting.clear();
 882   }
 883   if( !d_phase_req_waiting.empty() ){
 884     for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){
 885       getOutputChannel().requirePhase( it->first, it->second );
 886     }
 887     d_phase_req_waiting.clear();
 888   }
 889 }
 890
 891 void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
 892   if( options::literalMatchMode()!=quantifiers::LITERAL_MATCH_NONE && d_phase_reqs.find( f )!=d_phase_reqs.end() ){
 893     // doing literal-based matching (consider polarity of literals)
 894     for( int i=0; i<(int)nodes.size(); i++ ){
 895       Node prev = nodes[i];
 896       if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){
 897         bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] );
 898         nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst<bool>(preq) );
 899       }
 900       //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){
 901       //  Node req = qe->getPhaseReqEquality( f, trNodes[i] );
 902       //  trNodes[i] = NodeManager::currentNM()->mkNode( EQUAL, trNodes[i], req );
 903       //}
 904     }
 905   }
 906 }
 907
 908 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
 909   for( std::map< Node, bool >::iterator it = d_skolemized.begin(); it != d_skolemized.end(); ++it ){
 910     out << "Skolem constants of " << it->first << " : " << std::endl;
 911     out << "  ( ";
 912     for( unsigned i=0; i<d_term_db->d_skolem_constants[it->first].size(); i++ ){
 913       if( i>0 ){ out << ", "; }
 914       out << d_term_db->d_skolem_constants[it->first][i];
 915     }
 916     out << " )" << std::endl;
 917     out << std::endl;
 918   }
 919   if( options::incrementalSolving() ){
 920     for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
 921       out << "Instantiations of " << it->first << " : " << std::endl;
 922       it->second->print( out, it->first );
 923     }
 924   }else{
 925     for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
 926       out << "Instantiations of " << it->first << " : " << std::endl;
 927       it->second.print( out, it->first );
 928       out << std::endl;
 929     }
 930   }
 931 }
 932
 933 void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
 934   if( d_ceg_inst ){
 935     d_ceg_inst->printSynthSolution( out );
 936   }else{
 937     out << "Internal error : module for synth solution not found." << std::endl;
 938   }
 939 }
 940
 941 QuantifiersEngine::Statistics::Statistics():
 942   d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
 943   d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
 944   d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
 945   d_instantiations("QuantifiersEngine::Instantiations_Total", 0),
 946   d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0),
 947   d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0),
 948   d_triggers("QuantifiersEngine::Triggers", 0),
 949   d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
 950   d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
 951   d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0)
 952 {
 953   StatisticsRegistry::registerStat(&d_num_quant);
 954   StatisticsRegistry::registerStat(&d_instantiation_rounds);
 955   StatisticsRegistry::registerStat(&d_instantiation_rounds_lc);
 956   StatisticsRegistry::registerStat(&d_instantiations);
 957   StatisticsRegistry::registerStat(&d_inst_duplicate);
 958   StatisticsRegistry::registerStat(&d_inst_duplicate_eq);
 959   StatisticsRegistry::registerStat(&d_triggers);
 960   StatisticsRegistry::registerStat(&d_simple_triggers);
 961   StatisticsRegistry::registerStat(&d_multi_triggers);
 962   StatisticsRegistry::registerStat(&d_multi_trigger_instantiations);
 963 }
 964
 965 QuantifiersEngine::Statistics::~Statistics(){
 966   StatisticsRegistry::unregisterStat(&d_num_quant);
 967   StatisticsRegistry::unregisterStat(&d_instantiation_rounds);
 968   StatisticsRegistry::unregisterStat(&d_instantiation_rounds_lc);
 969   StatisticsRegistry::unregisterStat(&d_instantiations);
 970   StatisticsRegistry::unregisterStat(&d_inst_duplicate);
 971   StatisticsRegistry::unregisterStat(&d_inst_duplicate_eq);
 972   StatisticsRegistry::unregisterStat(&d_triggers);
 973   StatisticsRegistry::unregisterStat(&d_simple_triggers);
 974   StatisticsRegistry::unregisterStat(&d_multi_triggers);
 975   StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations);
 976 }
 977
 978 eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
 979   return getTheoryEngine()->getMasterEqualityEngine();
 980 }
 981
 982 void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
 983   eq::EqualityEngine* ee = getMasterEqualityEngine();
 984   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
 985   std::map< TypeNode, int > typ_num;
 986   while( !eqcs_i.isFinished() ){
 987     TNode r = (*eqcs_i);
 988     TypeNode tr = r.getType();
 989     if( typ_num.find( tr )==typ_num.end() ){
 990       typ_num[tr] = 0;
 991     }
 992     typ_num[tr]++;
 993     bool firstTime = true;
 994     Trace(c) << "  " << r;
 995     Trace(c) << " : { ";
 996     eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
 997     while( !eqc_i.isFinished() ){
 998       TNode n = (*eqc_i);
 999       if( r!=n ){
1000         if( firstTime ){
1001           Trace(c) << std::endl;
1002           firstTime = false;
1003         }
1004         Trace(c) << "    " << n << std::endl;
1005       }
1006       ++eqc_i;
1007     }
1008     if( !firstTime ){ Trace(c) << "  "; }
1009     Trace(c) << "}" << std::endl;
1010     ++eqcs_i;
1011   }
1012   Trace(c) << std::endl;
1013   for( std::map< TypeNode, int >::iterator it = typ_num.begin(); it != typ_num.end(); ++it ){
1014     Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl;
1015   }
1016 }
1017
1018 void EqualityQueryQuantifiersEngine::reset(){
1019   d_int_rep.clear();
1020   d_reset_count++;
1021 }
1022
1023 bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
1024   return getEngine()->hasTerm( a );
1025 }
1026
1027 Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){
1028   eq::EqualityEngine* ee = getEngine();
1029   if( ee->hasTerm( a ) ){
1030     return ee->getRepresentative( a );
1031   }else{
1032     return a;
1033   }
1034 }
1035
1036 bool EqualityQueryQuantifiersEngine::areEqual( Node a, Node b ){
1037   if( a==b ){
1038     return true;
1039   }else{
1040     eq::EqualityEngine* ee = getEngine();
1041     if( d_liberal ){
1042       return true;//!areDisequal( a, b );
1043     }else{
1044       if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
1045         if( ee->areEqual( a, b ) ){
1046           return true;
1047         }
1048       }
1049       return false;
1050     }
1051   }
1052 }
1053
1054 bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
1055   eq::EqualityEngine* ee = getEngine();
1056   if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
1057     if( ee->areDisequal( a, b, false ) ){
1058       return true;
1059     }
1060   }
1061   return false;
1062 }
1063
1064 Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, int index ){
1065   Node r = getRepresentative( a );
1066   if( !options::internalReps() ){
1067     return r;
1068   }else{
1069     if( options::finiteModelFind() ){
1070       if( r.isConst() ){
1071         //map back from values assigned by model, if any
1072         if( d_qe->getModel() ){
1073           std::map< Node, Node >::iterator it = d_qe->getModel()->d_rep_set.d_values_to_terms.find( r );
1074           if( it!=d_qe->getModel()->d_rep_set.d_values_to_terms.end() ){
1075             r = it->second;
1076             r = getRepresentative( r );
1077           }else{
1078             if( r.getType().isSort() ){
1079               Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
1080             }
1081           }
1082         }
1083       }
1084     }
1085
1086     if( d_int_rep.find( r )==d_int_rep.end() ){
1087       //find best selection for representative
1088       Node r_best;
1089       //if( options::fmfRelevantDomain() && !f.isNull() ){
1090       //  Trace("internal-rep-debug") << "Consult relevant domain to mkRep " << r << std::endl;
1091       //  r_best = d_qe->getRelevantDomain()->getRelevantTerm( f, index, r );
1092       //  Trace("internal-rep-debug") << "Returned " << r_best << " " << r << std::endl;
1093       //}
1094       std::vector< Node > eqc;
1095       getEquivalenceClass( r, eqc );
1096       Trace("internal-rep-select") << "Choose representative for equivalence class : { ";
1097       for( unsigned i=0; i<eqc.size(); i++ ){
1098         if( i>0 ) Trace("internal-rep-select") << ", ";
1099         Trace("internal-rep-select") << eqc[i];
1100       }
1101       Trace("internal-rep-select")  << " } " << std::endl;
1102       int r_best_score = -1;
1103       for( size_t i=0; i<eqc.size(); i++ ){
1104         int score = getRepScore( eqc[i], f, index );
1105         if( score!=-2 ){
1106           if( r_best.isNull() || ( score>=0 && ( r_best_score<0 || score<r_best_score ) ) ){
1107             r_best = eqc[i];
1108             r_best_score = score;
1109           }
1110         }
1111       }
1112       if( r_best.isNull() ){
1113         if( !f.isNull() ){
1114           Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index );
1115           r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
1116         }else{
1117           r_best = a;
1118         }
1119       }
1120       //now, make sure that no other member of the class is an instance
1121       std::hash_map<TNode, Node, TNodeHashFunction> cache;
1122       r_best = getInstance( r_best, eqc, cache );
1123       //store that this representative was chosen at this point
1124       if( d_rep_score.find( r_best )==d_rep_score.end() ){
1125         d_rep_score[ r_best ] = d_reset_count;
1126       }
1127       Trace("internal-rep-select") << "...Choose " << r_best << std::endl;
1128       d_int_rep[r] = r_best;
1129       if( r_best!=a ){
1130         Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
1131         Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
1132       }
1133       return r_best;
1134     }else{
1135       return d_int_rep[r];
1136     }
1137   }
1138 }
1139
1140 void EqualityQueryQuantifiersEngine::flattenRepresentatives( std::map< TypeNode, std::vector< Node > >& reps ) {
1141   //make sure internal representatives currently exist
1142   for( std::map< TypeNode, std::vector< Node > >::iterator it = reps.begin(); it != reps.end(); ++it ){
1143     if( it->first.isSort() ){
1144       for( unsigned i=0; i<it->second.size(); i++ ){
1145         Node r = getInternalRepresentative( it->second[i], Node::null(), 0 );
1146       }
1147     }
1148   }
1149   Trace("internal-rep-flatten") << "---Flattening representatives : " << std::endl;
1150   for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
1151     Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl;
1152   }
1153   //store representatives for newly created terms
1154   std::map< Node, Node > temp_rep_map;
1155
1156   bool success;
1157   do {
1158     success = false;
1159     for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
1160       if( it->second.getKind()==APPLY_UF && it->second.getType().isSort() ){
1161         Node ni = it->second;
1162         std::vector< Node > cc;
1163         cc.push_back( it->second.getOperator() );
1164         bool changed = false;
1165         for( unsigned j=0; j<ni.getNumChildren(); j++ ){
1166           if( ni[j].getType().isSort() ){
1167             Node r = getRepresentative( ni[j] );
1168             if( d_int_rep.find( r )==d_int_rep.end() ){
1169               Assert( temp_rep_map.find( r )!=temp_rep_map.end() );
1170               r = temp_rep_map[r];
1171             }
1172             if( r==ni ){
1173               //found sub-term as instance
1174               Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to subterm " << ni[j] << std::endl;
1175               d_int_rep[it->first] = ni[j];
1176               changed = false;
1177               success = true;
1178               break;
1179             }else{
1180               Node ir = d_int_rep[r];
1181               cc.push_back( ir );
1182               if( ni[j]!=ir ){
1183                 changed = true;
1184               }
1185             }
1186           }else{
1187             changed = false;
1188             break;
1189           }
1190         }
1191         if( changed ){
1192           Node n = NodeManager::currentNM()->mkNode( APPLY_UF, cc );
1193           Trace("internal-rep-flatten-debug") << "...Changed " << it->second << " to " << n << std::endl;
1194           success = true;
1195           d_int_rep[it->first] = n;
1196           temp_rep_map[n] = it->first;
1197         }
1198       }
1199     }
1200   }while( success );
1201   Trace("internal-rep-flatten") << "---After flattening : " << std::endl;
1202   for( std::map< Node, Node >::iterator it = d_int_rep.begin(); it != d_int_rep.end(); ++it ){
1203     Trace("internal-rep-flatten") << it->first.getType() << " : irep( " << it->first << " ) = " << it->second << std::endl;
1204   }
1205 }
1206
1207 eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
1208   return d_qe->getMasterEqualityEngine();
1209 }
1210
1211 void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
1212   eq::EqualityEngine* ee = getEngine();
1213   if( ee->hasTerm( a ) ){
1214     Node rep = ee->getRepresentative( a );
1215     eq::EqClassIterator eqc_iter( rep, ee );
1216     while( !eqc_iter.isFinished() ){
1217       eqc.push_back( *eqc_iter );
1218       eqc_iter++;
1219     }
1220   }else{
1221     eqc.push_back( a );
1222   }
1223   //a should be in its equivalence class
1224   Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
1225 }
1226
1227 //helper functions
1228
1229 Node EqualityQueryQuantifiersEngine::getInstance( Node n, const std::vector< Node >& eqc, std::hash_map<TNode, Node, TNodeHashFunction>& cache ){
1230   if(cache.find(n) != cache.end()) {
1231     return cache[n];
1232   }
1233   for( size_t i=0; i<n.getNumChildren(); i++ ){
1234     Node nn = getInstance( n[i], eqc, cache );
1235     if( !nn.isNull() ){
1236       return cache[n] = nn;
1237     }
1238   }
1239   if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){
1240     return cache[n] = n;
1241   }else{
1242     return cache[n] = Node::null();
1243   }
1244 }
1245
1246 int getDepth( Node n ){
1247   if( n.getNumChildren()==0 ){
1248     return 0;
1249   }else{
1250     int maxDepth = -1;
1251     for( int i=0; i<(int)n.getNumChildren(); i++ ){
1252       int depth = getDepth( n[i] );
1253       if( depth>maxDepth ){
1254         maxDepth = depth;
1255       }
1256     }
1257     return maxDepth;
1258   }
1259 }
1260
1261 //smaller the score, the better
1262 int EqualityQueryQuantifiersEngine::getRepScore( Node n, Node f, int index ){
1263   if( options::cbqi() && quantifiers::TermDb::hasInstConstAttr(n) ){
1264     return -2;
1265   }else if( options::lteRestrictInstClosure() && ( !d_qe->getTermDatabase()->isInstClosure( n ) || !d_qe->getTermDatabase()->hasTermCurrent( n, false ) ) ){
1266     return -1;
1267   }else if( options::instMaxLevel()!=-1 ){
1268     //score prefer lowest instantiation level
1269     if( n.hasAttribute(InstLevelAttribute()) ){
1270       return n.getAttribute(InstLevelAttribute());
1271     }else{
1272       return options::instLevelInputOnly() ? -1 : 0;
1273     }
1274   }else{
1275     //score prefers earliest use of this term as a representative
1276     return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
1277   }
1278   //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n );    //term depth
1279 }
1280