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-2017 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/anti_skolem.h"
  25 #include "theory/quantifiers/bounded_integers.h"
  26 #include "theory/quantifiers/ce_guided_instantiation.h"
  27 #include "theory/quantifiers/ceg_t_instantiator.h"
  28 #include "theory/quantifiers/conjecture_generator.h"
  29 #include "theory/quantifiers/equality_infer.h"
  30 #include "theory/quantifiers/equality_query.h"
  31 #include "theory/quantifiers/first_order_model.h"
  32 #include "theory/quantifiers/full_model_check.h"
  33 #include "theory/quantifiers/fun_def_engine.h"
  34 #include "theory/quantifiers/inst_propagator.h"
  35 #include "theory/quantifiers/inst_strategy_cbqi.h"
  36 #include "theory/quantifiers/inst_strategy_e_matching.h"
  37 #include "theory/quantifiers/inst_strategy_enumerative.h"
  38 #include "theory/quantifiers/instantiate.h"
  39 #include "theory/quantifiers/instantiation_engine.h"
  40 #include "theory/quantifiers/local_theory_ext.h"
  41 #include "theory/quantifiers/model_engine.h"
  42 #include "theory/quantifiers/quant_conflict_find.h"
  43 #include "theory/quantifiers/quant_epr.h"
  44 #include "theory/quantifiers/quant_equality_engine.h"
  45 #include "theory/quantifiers/quant_relevance.h"
  46 #include "theory/quantifiers/quant_split.h"
  47 #include "theory/quantifiers/quantifiers_attributes.h"
  48 #include "theory/quantifiers/quantifiers_rewriter.h"
  49 #include "theory/quantifiers/relevant_domain.h"
  50 #include "theory/quantifiers/rewrite_engine.h"
  51 #include "theory/quantifiers/skolemize.h"
  52 #include "theory/quantifiers/term_database.h"
  53 #include "theory/quantifiers/term_database_sygus.h"
  54 #include "theory/quantifiers/term_enumeration.h"
  55 #include "theory/quantifiers/term_util.h"
  56 #include "theory/quantifiers/trigger.h"
  57 #include "theory/sep/theory_sep.h"
  58 #include "theory/theory_engine.h"
  59 #include "theory/uf/equality_engine.h"
  60 #include "theory/uf/theory_uf.h"
  61 #include "theory/uf/theory_uf_strong_solver.h"
  62
  63 using namespace std;
  64 using namespace CVC4;
  65 using namespace CVC4::kind;
  66 using namespace CVC4::context;
  67 using namespace CVC4::theory;
  68 using namespace CVC4::theory::inst;
  69
  70 QuantifiersEngine::QuantifiersEngine(context::Context* c,
  71                                      context::UserContext* u,
  72                                      TheoryEngine* te)
  73     : d_te(te),
  74       d_quant_attr(new quantifiers::QuantAttributes(this)),
  75       d_instantiate(new quantifiers::Instantiate(this, u)),
  76       d_skolemize(new quantifiers::Skolemize(this, u)),
  77       d_term_enum(new quantifiers::TermEnumeration),
  78       d_conflict_c(c, false),
  79       // d_quants(u),
  80       d_quants_red(u),
  81       d_lemmas_produced_c(u),
  82       d_ierCounter_c(c),
  83       // d_ierCounter(c),
  84       // d_ierCounter_lc(c),
  85       // d_ierCounterLastLc(c),
  86       d_presolve(u, true),
  87       d_presolve_in(u),
  88       d_presolve_cache(u),
  89       d_presolve_cache_wq(u),
  90       d_presolve_cache_wic(u)
  91 {
  92   //utilities
  93   d_eq_query = new quantifiers::EqualityQueryQuantifiersEngine( c, this );
  94   d_util.push_back( d_eq_query );
  95
  96   // term util must come first
  97   d_term_util = new quantifiers::TermUtil(this);
  98   d_util.push_back(d_term_util);
  99
 100   d_term_db = new quantifiers::TermDb( c, u, this );
 101   d_util.push_back( d_term_db );
 102
 103   if (options::ceGuidedInst()) {
 104     d_sygus_tdb = new quantifiers::TermDbSygus(c, this);
 105   }else{
 106     d_sygus_tdb = NULL;
 107   }
 108
 109   if( options::instPropagate() ){
 110     // notice that this option is incompatible with options::qcfAllConflict()
 111     d_inst_prop = new quantifiers::InstPropagator( this );
 112     d_util.push_back( d_inst_prop );
 113     d_instantiate->addNotify(d_inst_prop->getInstantiationNotify());
 114   }else{
 115     d_inst_prop = NULL;
 116   }
 117
 118   if( options::inferArithTriggerEq() ){
 119     d_eq_inference = new quantifiers::EqualityInference( c, options::inferArithTriggerEqExp() );
 120   }else{
 121     d_eq_inference = NULL;
 122   }
 123
 124   d_util.push_back(d_instantiate.get());
 125
 126   d_tr_trie = new inst::TriggerTrie;
 127   d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
 128   d_conflict = false;
 129   d_hasAddedLemma = false;
 130   d_useModelEe = false;
 131   //don't add true lemma
 132   d_lemmas_produced_c[d_term_util->d_true] = true;
 133
 134   Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
 135   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
 136
 137   if( options::relevantTriggers() ){
 138     d_quant_rel = new quantifiers::QuantRelevance(false);
 139     d_util.push_back(d_quant_rel);
 140   }else{
 141     d_quant_rel = NULL;
 142   }
 143
 144   if( options::quantEpr() ){
 145     Assert( !options::incrementalSolving() );
 146     d_qepr = new quantifiers::QuantEPR;
 147   }else{
 148     d_qepr = NULL;
 149   }
 150
 151
 152   d_qcf = NULL;
 153   d_sg_gen = NULL;
 154   d_inst_engine = NULL;
 155   d_i_cbqi = NULL;
 156   d_qsplit = NULL;
 157   d_anti_skolem = NULL;
 158   d_model = NULL;
 159   d_model_engine = NULL;
 160   d_bint = NULL;
 161   d_rr_engine = NULL;
 162   d_ceg_inst = NULL;
 163   d_lte_part_inst = NULL;
 164   d_alpha_equiv = NULL;
 165   d_fun_def_engine = NULL;
 166   d_uee = NULL;
 167   d_fs = NULL;
 168   d_rel_dom = NULL;
 169   d_bv_invert = NULL;
 170   d_builder = NULL;
 171
 172   //allow theory combination to go first, once initially
 173   d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
 174   d_ierCounter_c = d_ierCounter;
 175   d_ierCounter_lc = 0;
 176   d_ierCounterLastLc = 0;
 177   d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
 178 }
 179
 180 QuantifiersEngine::~QuantifiersEngine(){
 181   delete d_alpha_equiv;
 182   delete d_builder;
 183   delete d_qepr;
 184   delete d_rr_engine;
 185   delete d_bint;
 186   delete d_model_engine;
 187   delete d_inst_engine;
 188   delete d_qcf;
 189   delete d_quant_rel;
 190   delete d_rel_dom;
 191   delete d_bv_invert;
 192   delete d_model;
 193   delete d_tr_trie;
 194   delete d_term_db;
 195   delete d_sygus_tdb;
 196   delete d_term_util;
 197   delete d_eq_inference;
 198   delete d_eq_query;
 199   delete d_sg_gen;
 200   delete d_ceg_inst;
 201   delete d_lte_part_inst;
 202   delete d_fun_def_engine;
 203   delete d_uee;
 204   delete d_fs;
 205   delete d_i_cbqi;
 206   delete d_qsplit;
 207   delete d_anti_skolem;
 208   delete d_inst_prop;
 209 }
 210
 211 EqualityQuery* QuantifiersEngine::getEqualityQuery() {
 212   return d_eq_query;
 213 }
 214
 215 context::Context* QuantifiersEngine::getSatContext(){
 216   return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext();
 217 }
 218
 219 context::UserContext* QuantifiersEngine::getUserContext(){
 220   return d_te->theoryOf( THEORY_QUANTIFIERS )->getUserContext();
 221 }
 222
 223 OutputChannel& QuantifiersEngine::getOutputChannel(){
 224   return d_te->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel();
 225 }
 226 /** get default valuation for the quantifiers engine */
 227 Valuation& QuantifiersEngine::getValuation(){
 228   return d_te->theoryOf( THEORY_QUANTIFIERS )->getValuation();
 229 }
 230
 231 void QuantifiersEngine::finishInit(){
 232   context::Context * c = getSatContext();
 233   Trace("quant-engine-debug") << "QuantifiersEngine : finishInit " << std::endl;
 234   bool needsBuilder = false;
 235   bool needsRelDom = false;
 236   //add quantifiers modules
 237   if( options::quantConflictFind() || options::quantRewriteRules() ){
 238     d_qcf = new quantifiers::QuantConflictFind( this, c);
 239     d_modules.push_back( d_qcf );
 240   }
 241   if( options::conjectureGen() ){
 242     d_sg_gen = new quantifiers::ConjectureGenerator( this, c );
 243     d_modules.push_back( d_sg_gen );
 244   }
 245   if( !options::finiteModelFind() || options::fmfInstEngine() ){
 246     d_inst_engine = new quantifiers::InstantiationEngine( this );
 247     d_modules.push_back(  d_inst_engine );
 248   }
 249   if( options::cbqi() ){
 250     d_i_cbqi = new quantifiers::InstStrategyCegqi( this );
 251     d_modules.push_back( d_i_cbqi );
 252     if( options::cbqiBv() ){
 253       // if doing instantiation for BV, need the inverter class
 254       d_bv_invert = new quantifiers::BvInverter;
 255     }
 256   }
 257   if( options::ceGuidedInst() ){
 258     d_ceg_inst = new quantifiers::CegInstantiation( this, c );
 259     d_modules.push_back( d_ceg_inst );
 260     //needsBuilder = true;
 261   }
 262   //finite model finding
 263   if( options::finiteModelFind() ){
 264     if( options::fmfBound() ){
 265       d_bint = new quantifiers::BoundedIntegers( c, this );
 266       d_modules.push_back( d_bint );
 267     }
 268     d_model_engine = new quantifiers::ModelEngine( c, this );
 269     d_modules.push_back( d_model_engine );
 270     //finite model finder has special ways of building the model
 271     needsBuilder = true;
 272   }
 273   if( options::quantRewriteRules() ){
 274     d_rr_engine = new quantifiers::RewriteEngine( c, this );
 275     d_modules.push_back(d_rr_engine);
 276   }
 277   if( options::ltePartialInst() ){
 278     d_lte_part_inst = new quantifiers::LtePartialInst( this, c );
 279     d_modules.push_back( d_lte_part_inst );
 280   }
 281   if( options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ){
 282     d_qsplit = new quantifiers::QuantDSplit( this, c );
 283     d_modules.push_back( d_qsplit );
 284   }
 285   if( options::quantAntiSkolem() ){
 286     d_anti_skolem = new quantifiers::QuantAntiSkolem( this );
 287     d_modules.push_back( d_anti_skolem );
 288   }
 289   if( options::quantAlphaEquiv() ){
 290     d_alpha_equiv = new quantifiers::AlphaEquivalence( this );
 291   }
 292   //if( options::funDefs() ){
 293   //  d_fun_def_engine = new quantifiers::FunDefEngine( this, c );
 294   //  d_modules.push_back( d_fun_def_engine );
 295   //}
 296   if( options::quantEqualityEngine() ){
 297     d_uee = new quantifiers::QuantEqualityEngine( this, c );
 298     d_modules.push_back( d_uee );
 299   }
 300   //full saturation : instantiate from relevant domain, then arbitrary terms
 301   if( options::fullSaturateQuant() || options::fullSaturateInterleave() ){
 302     d_fs = new quantifiers::InstStrategyEnum(this);
 303     d_modules.push_back( d_fs );
 304     needsRelDom = true;
 305   }
 306
 307   if( needsRelDom ){
 308     d_rel_dom = new quantifiers::RelevantDomain( this );
 309     d_util.push_back( d_rel_dom );
 310   }
 311
 312   // if we require specialized ways of building the model
 313   if( needsBuilder ){
 314     Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl;
 315     if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ||
 316         options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBound() ){
 317       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
 318       d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
 319       d_builder = new quantifiers::fmcheck::FullModelChecker( c, this );
 320     }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
 321       Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl;
 322       d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" );
 323       d_builder = new quantifiers::AbsMbqiBuilder( c, this );
 324     }else{
 325       Trace("quant-engine-debug") << "...make default model builder." << std::endl;
 326       d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
 327       d_builder = new quantifiers::QModelBuilderDefault( c, this );
 328     }
 329   }else{
 330     d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
 331   }
 332 }
 333
 334 QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
 335   std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q );
 336   if( it==d_owner.end() ){
 337     return NULL;
 338   }else{
 339     return it->second;
 340   }
 341 }
 342
 343 void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m, int priority ) {
 344   QuantifiersModule * mo = getOwner( q );
 345   if( mo!=m ){
 346     if( mo!=NULL ){
 347       if( priority<=d_owner_priority[q] ){
 348         Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << " with higher priority!" << std::endl;
 349         return;
 350       }
 351     }
 352     d_owner[q] = m;
 353     d_owner_priority[q] = priority;
 354   }
 355 }
 356
 357 bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
 358   QuantifiersModule * mo = getOwner( q );
 359   return mo==m || mo==NULL;
 360 }
 361
 362 bool QuantifiersEngine::isFiniteBound( Node q, Node v ) {
 363   if( getBoundedIntegers() && getBoundedIntegers()->isBoundVar( q, v ) ){
 364     return true;
 365   }else{
 366     TypeNode tn = v.getType();
 367     if( tn.isSort() && options::finiteModelFind() ){
 368       return true;
 369     }
 370     else if (d_term_enum->mayComplete(tn))
 371     {
 372       return true;
 373     }
 374   }
 375   return false;
 376 }
 377
 378 void QuantifiersEngine::presolve() {
 379   Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
 380   for( unsigned i=0; i<d_modules.size(); i++ ){
 381     d_modules[i]->presolve();
 382   }
 383   d_term_db->presolve();
 384   d_presolve = false;
 385   //add all terms to database
 386   if( options::incrementalSolving() ){
 387     Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache.size() << std::endl;
 388     for( unsigned i=0; i<d_presolve_cache.size(); i++ ){
 389       addTermToDatabase( d_presolve_cache[i], d_presolve_cache_wq[i], d_presolve_cache_wic[i] );
 390     }
 391     Trace("quant-engine-proc") << "Done add presolve cache " << std::endl;
 392   }
 393 }
 394
 395 void QuantifiersEngine::ppNotifyAssertions(
 396     const std::vector<Node>& assertions) {
 397   Trace("quant-engine-proc")
 398       << "ppNotifyAssertions in QE, #assertions = " << assertions.size()
 399       << " check epr = " << (d_qepr != NULL) << std::endl;
 400   if ((options::instLevelInputOnly() && options::instMaxLevel() != -1) ||
 401       d_qepr != NULL) {
 402     for (unsigned i = 0; i < assertions.size(); i++) {
 403       if (options::instLevelInputOnly() && options::instMaxLevel() != -1) {
 404         quantifiers::QuantAttributes::setInstantiationLevelAttr(assertions[i],
 405                                                                 0);
 406       }
 407       if (d_qepr != NULL) {
 408         d_qepr->registerAssertion(assertions[i]);
 409       }
 410     }
 411     if (d_qepr != NULL) {
 412       // must handle sources of other new constants e.g. separation logic
 413       // FIXME: cleanup
 414       sep::TheorySep* theory_sep =
 415           static_cast<sep::TheorySep*>(getTheoryEngine()->theoryOf(THEORY_SEP));
 416       theory_sep->initializeBounds();
 417       d_qepr->finishInit();
 418     }
 419   }
 420 }
 421
 422 void QuantifiersEngine::check( Theory::Effort e ){
 423   CodeTimer codeTimer(d_statistics.d_time);
 424   d_useModelEe = options::quantModelEe() && ( e>=Theory::EFFORT_LAST_CALL );
 425   // if we want to use the model's equality engine, build the model now
 426   if( d_useModelEe && !d_model->isBuilt() ){
 427     Trace("quant-engine-debug") << "Build the model." << std::endl;
 428     if( !d_te->getModelBuilder()->buildModel( d_model ) ){
 429       //we are done if model building was unsuccessful
 430       flushLemmas();
 431       if( d_hasAddedLemma ){
 432         Trace("quant-engine-debug") << "...failed." << std::endl;
 433         return;
 434       }
 435     }
 436   }
 437
 438   if( !getActiveEqualityEngine()->consistent() ){
 439     Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
 440     return;
 441   }
 442   bool needsCheck = !d_lemmas_waiting.empty();
 443   QuantifiersModule::QEffort needsModelE = QuantifiersModule::QEFFORT_NONE;
 444   std::vector< QuantifiersModule* > qm;
 445   if( d_model->checkNeeded() ){
 446     needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
 447     for (QuantifiersModule*& mdl : d_modules)
 448     {
 449       if (mdl->needsCheck(e))
 450       {
 451         qm.push_back(mdl);
 452         needsCheck = true;
 453         //can only request model at last call since theory combination can find inconsistencies
 454         if( e>=Theory::EFFORT_LAST_CALL ){
 455           QuantifiersModule::QEffort me = mdl->needsModel(e);
 456           needsModelE = me<needsModelE ? me : needsModelE;
 457         }
 458       }
 459     }
 460   }
 461
 462   d_conflict = false;
 463   d_hasAddedLemma = false;
 464   bool setIncomplete = false;
 465
 466   Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
 467   if( needsCheck ){
 468     //this will fail if a set of instances is marked as a conflict, but is not
 469     Assert( !d_conflict_c.get() );
 470     //flush previous lemmas (for instance, if was interupted), or other lemmas to process
 471     flushLemmas();
 472     if( d_hasAddedLemma ){
 473       return;
 474     }
 475
 476     double clSet = 0;
 477     if( Trace.isOn("quant-engine") ){
 478       clSet = double(clock())/double(CLOCKS_PER_SEC);
 479       Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e << " <<<<<" << std::endl;
 480     }
 481
 482     if( Trace.isOn("quant-engine-debug") ){
 483       Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
 484       Trace("quant-engine-debug") << "  depth : " << d_ierCounter_c << std::endl;
 485       Trace("quant-engine-debug") << "  modules to check : ";
 486       for( unsigned i=0; i<qm.size(); i++ ){
 487         Trace("quant-engine-debug") << qm[i]->identify() << " ";
 488       }
 489       Trace("quant-engine-debug") << std::endl;
 490       Trace("quant-engine-debug") << "  # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
 491       if( !d_lemmas_waiting.empty() ){
 492         Trace("quant-engine-debug") << "  lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
 493       }
 494       Trace("quant-engine-debug") << "  Theory engine finished : " << !d_te->needCheck() << std::endl;
 495       Trace("quant-engine-debug") << "  Needs model effort : " << needsModelE << std::endl;
 496     }
 497     if( Trace.isOn("quant-engine-ee-pre") ){
 498       Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
 499       debugPrintEqualityEngine( "quant-engine-ee-pre" );
 500     }
 501     if( Trace.isOn("quant-engine-assert") ){
 502       Trace("quant-engine-assert") << "Assertions : " << std::endl;
 503       getTheoryEngine()->printAssertions("quant-engine-assert");
 504     }
 505
 506     //reset utilities
 507     Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl;
 508     for (QuantifiersUtil*& util : d_util)
 509     {
 510       Trace("quant-engine-debug2") << "Reset " << util->identify().c_str()
 511                                    << "..." << std::endl;
 512       if (!util->reset(e))
 513       {
 514         flushLemmas();
 515         if( d_hasAddedLemma ){
 516           return;
 517         }else{
 518           //should only fail reset if added a lemma
 519           Assert( false );
 520         }
 521       }
 522     }
 523
 524     if( Trace.isOn("quant-engine-ee") ){
 525       Trace("quant-engine-ee") << "Equality engine : " << std::endl;
 526       debugPrintEqualityEngine( "quant-engine-ee" );
 527     }
 528
 529     //reset the model
 530     Trace("quant-engine-debug") << "Reset model..." << std::endl;
 531     d_model->reset_round();
 532
 533     //reset the modules
 534     Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
 535     for (QuantifiersModule*& mdl : d_modules)
 536     {
 537       Trace("quant-engine-debug2") << "Reset " << mdl->identify().c_str()
 538                                    << std::endl;
 539       mdl->reset_round(e);
 540     }
 541     Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
 542     //reset may have added lemmas
 543     flushLemmas();
 544     if( d_hasAddedLemma ){
 545       return;
 546     }
 547
 548     if( e==Theory::EFFORT_LAST_CALL ){
 549       //if effort is last call, try to minimize model first
 550       //uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
 551       //if( ufss && !ufss->minimize() ){ return; }
 552       ++(d_statistics.d_instantiation_rounds_lc);
 553     }else if( e==Theory::EFFORT_FULL ){
 554       ++(d_statistics.d_instantiation_rounds);
 555     }
 556     Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
 557     for (unsigned qef = QuantifiersModule::QEFFORT_CONFLICT;
 558          qef <= QuantifiersModule::QEFFORT_LAST_CALL;
 559          ++qef)
 560     {
 561       QuantifiersModule::QEffort quant_e =
 562           static_cast<QuantifiersModule::QEffort>(qef);
 563       d_curr_effort_level = quant_e;
 564       //build the model if any module requested it
 565       if( needsModelE==quant_e && !d_model->isBuilt() ){
 566         // theory engine's model builder is quantifier engine's builder if it has one
 567         Assert( !d_builder || d_builder==d_te->getModelBuilder() );
 568         Trace("quant-engine-debug") << "Build model..." << std::endl;
 569         if( !d_te->getModelBuilder()->buildModel( d_model ) ){
 570           //we are done if model building was unsuccessful
 571           Trace("quant-engine-debug") << "...added lemmas." << std::endl;
 572           flushLemmas();
 573         }
 574       }
 575       if( !d_hasAddedLemma ){
 576         //check each module
 577         for (QuantifiersModule*& mdl : qm)
 578         {
 579           Trace("quant-engine-debug") << "Check " << mdl->identify().c_str()
 580                                       << " at effort " << quant_e << "..."
 581                                       << std::endl;
 582           mdl->check(e, quant_e);
 583           if( d_conflict ){
 584             Trace("quant-engine-debug") << "...conflict!" << std::endl;
 585             break;
 586           }
 587         }
 588         //flush all current lemmas
 589         flushLemmas();
 590       }
 591       //if we have added one, stop
 592       if( d_hasAddedLemma ){
 593         break;
 594       }else{
 595         Assert( !d_conflict );
 596         if (quant_e == QuantifiersModule::QEFFORT_CONFLICT)
 597         {
 598           if( e==Theory::EFFORT_FULL ){
 599             //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase
 600             if( d_ierCounterLastLc!=d_ierCounter_lc || !options::instWhenStrictInterleave() || d_ierCounter%d_inst_when_phase!=0 ){
 601               d_ierCounter = d_ierCounter + 1;
 602               d_ierCounterLastLc = d_ierCounter_lc;
 603               d_ierCounter_c = d_ierCounter_c.get() + 1;
 604             }
 605           }else if( e==Theory::EFFORT_LAST_CALL ){
 606             d_ierCounter_lc = d_ierCounter_lc + 1;
 607           }
 608         }
 609         else if (quant_e == QuantifiersModule::QEFFORT_MODEL)
 610         {
 611           if( e==Theory::EFFORT_LAST_CALL ){
 612             //sources of incompleteness
 613             for (QuantifiersUtil*& util : d_util)
 614             {
 615               if (!util->checkComplete())
 616               {
 617                 Trace("quant-engine-debug") << "Set incomplete because utility "
 618                                             << util->identify().c_str()
 619                                             << " was incomplete." << std::endl;
 620                 setIncomplete = true;
 621               }
 622             }
 623             //if we have a chance not to set incomplete
 624             if( !setIncomplete ){
 625               //check if we should set the incomplete flag
 626               for (QuantifiersModule*& mdl : d_modules)
 627               {
 628                 if (!mdl->checkComplete())
 629                 {
 630                   Trace("quant-engine-debug")
 631                       << "Set incomplete because module "
 632                       << mdl->identify().c_str() << " was incomplete."
 633                       << std::endl;
 634                   setIncomplete = true;
 635                   break;
 636                 }
 637               }
 638               if( !setIncomplete ){
 639                 //look at individual quantified formulas, one module must claim completeness for each one
 640                 for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
 641                   bool hasCompleteM = false;
 642                   Node q = d_model->getAssertedQuantifier( i );
 643                   QuantifiersModule * qmd = getOwner( q );
 644                   if( qmd!=NULL ){
 645                     hasCompleteM = qmd->checkCompleteFor( q );
 646                   }else{
 647                     for( unsigned j=0; j<d_modules.size(); j++ ){
 648                       if( d_modules[j]->checkCompleteFor( q ) ){
 649                         qmd = d_modules[j];
 650                         hasCompleteM = true;
 651                         break;
 652                       }
 653                     }
 654                   }
 655                   if( !hasCompleteM ){
 656                     Trace("quant-engine-debug") << "Set incomplete because " << q << " was not fully processed." << std::endl;
 657                     setIncomplete = true;
 658                     break;
 659                   }else{
 660                     Assert( qmd!=NULL );
 661                     Trace("quant-engine-debug2") << "Complete for " << q << " due to " << qmd->identify().c_str() << std::endl;
 662                   }
 663                 }
 664               }
 665             }
 666             //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL
 667             if( !setIncomplete ){
 668               break;
 669             }
 670           }
 671         }
 672       }
 673     }
 674     d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
 675     Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
 676     if( d_hasAddedLemma ){
 677       d_instantiate->debugPrint();
 678     }
 679     if( Trace.isOn("quant-engine") ){
 680       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
 681       Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2-clSet);
 682       Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma;
 683       Trace("quant-engine") << std::endl;
 684     }
 685
 686     Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl;
 687   }else{
 688     Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl;
 689   }
 690
 691   //SAT case
 692   if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
 693     if( options::produceModels() ){
 694       if( d_model->isBuilt() ){
 695         Trace("quant-engine-debug") << "Already built model using model builder, finish..." << std::endl;
 696       }else{
 697         //use default model builder when no module built the model
 698         Trace("quant-engine-debug") << "Build the default model..." << std::endl;
 699         d_te->getModelBuilder()->buildModel( d_model );
 700         Trace("quant-engine-debug") << "Done building the model." << std::endl;
 701       }
 702     }
 703     if( setIncomplete ){
 704       Trace("quant-engine") << "Set incomplete flag." << std::endl;
 705       getOutputChannel().setIncomplete();
 706     }
 707     //output debug stats
 708     d_instantiate->debugPrintModel();
 709   }
 710 }
 711
 712 void QuantifiersEngine::notifyCombineTheories() {
 713   //if allowing theory combination to happen at most once between instantiation rounds
 714   //d_ierCounter = 1;
 715   //d_ierCounterLastLc = -1;
 716 }
 717
 718 bool QuantifiersEngine::reduceQuantifier( Node q ) {
 719   //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants
 720   BoolMap::const_iterator it = d_quants_red.find( q );
 721   if( it==d_quants_red.end() ){
 722     Node lem;
 723     std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q );
 724     if( itr==d_quants_red_lem.end() ){
 725       if( d_alpha_equiv ){
 726         Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
 727         //add equivalence with another quantified formula
 728         lem = d_alpha_equiv->reduceQuantifier( q );
 729         if( !lem.isNull() ){
 730           Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
 731           ++(d_statistics.d_red_alpha_equiv);
 732         }
 733       }
 734       d_quants_red_lem[q] = lem;
 735     }else{
 736       lem = itr->second;
 737     }
 738     if( !lem.isNull() ){
 739       getOutputChannel().lemma( lem );
 740     }
 741     d_quants_red[q] = !lem.isNull();
 742     return !lem.isNull();
 743   }else{
 744     return (*it).second;
 745   }
 746 }
 747
 748 bool QuantifiersEngine::registerQuantifier( Node f ){
 749   std::map< Node, bool >::iterator it = d_quants.find( f );
 750   if( it==d_quants.end() ){
 751     Trace("quant") << "QuantifiersEngine : Register quantifier ";
 752     Trace("quant") << " : " << f << std::endl;
 753     ++(d_statistics.d_num_quant);
 754     Assert( f.getKind()==FORALL );
 755
 756     //check whether we should apply a reduction
 757     if( reduceQuantifier( f ) ){
 758       Trace("quant") << "...reduced." << std::endl;
 759       d_quants[f] = false;
 760       return false;
 761     }else{
 762       // register with utilities
 763       for (unsigned i = 0; i < d_util.size(); i++)
 764       {
 765         d_util[i]->registerQuantifier(f);
 766       }
 767       // compute attributes
 768       d_quant_attr->computeAttributes(f);
 769
 770       for( unsigned i=0; i<d_modules.size(); i++ ){
 771         Trace("quant-debug") << "pre-register with " << d_modules[i]->identify() << "..." << std::endl;
 772         d_modules[i]->preRegisterQuantifier( f );
 773       }
 774       QuantifiersModule * qm = getOwner( f );
 775       if( qm!=NULL ){
 776         Trace("quant") << "   Owner : " << qm->identify() << std::endl;
 777       }
 778       //register with each module
 779       for( unsigned i=0; i<d_modules.size(); i++ ){
 780         Trace("quant-debug") << "register with " << d_modules[i]->identify() << "..." << std::endl;
 781         d_modules[i]->registerQuantifier( f );
 782       }
 783       //TODO: remove this
 784       Node ceBody = d_term_util->getInstConstantBody( f );
 785       Trace("quant-debug")  << "...finish." << std::endl;
 786       d_quants[f] = true;
 787       // flush lemmas
 788       flushLemmas();
 789       return true;
 790     }
 791   }else{
 792     return (*it).second;
 793   }
 794 }
 795
 796 void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
 797   for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){
 798     std::set< Node > added;
 799     getTermDatabase()->addTerm( *p, added );
 800   }
 801 }
 802
 803 void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
 804   if( !pol ){
 805     //if not reduced
 806     if( !reduceQuantifier( f ) ){
 807       //do skolemization
 808       Node lem = d_skolemize->process(f);
 809       if (!lem.isNull())
 810       {
 811         if( Trace.isOn("quantifiers-sk-debug") ){
 812           Node slem = Rewriter::rewrite( lem );
 813           Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl;
 814         }
 815         getOutputChannel().lemma( lem, false, true );
 816       }
 817     }
 818   }else{
 819     //assert to modules TODO : also for !pol?
 820     //register the quantifier, assert it to each module
 821     if( registerQuantifier( f ) ){
 822       d_model->assertQuantifier( f );
 823       for( unsigned i=0; i<d_modules.size(); i++ ){
 824         d_modules[i]->assertNode( f );
 825       }
 826       addTermToDatabase( d_term_util->getInstConstantBody( f ), true );
 827     }
 828   }
 829 }
 830
 831 void QuantifiersEngine::propagate( Theory::Effort level ){
 832   CodeTimer codeTimer(d_statistics.d_time);
 833
 834 }
 835
 836 Node QuantifiersEngine::getNextDecisionRequest( unsigned& priority ){
 837   unsigned min_priority = 0;
 838   Node dec;
 839   for( unsigned i=0; i<d_modules.size(); i++ ){
 840     Node n = d_modules[i]->getNextDecisionRequest( priority );
 841     if( !n.isNull() && ( dec.isNull() || priority<min_priority ) ){
 842       dec = n;
 843       min_priority = priority;
 844     }
 845   }
 846   return dec;
 847 }
 848
 849 void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
 850   if( options::incrementalSolving() ){
 851     if( d_presolve_in.find( n )==d_presolve_in.end() ){
 852       d_presolve_in.insert( n );
 853       d_presolve_cache.push_back( n );
 854       d_presolve_cache_wq.push_back( withinQuant );
 855       d_presolve_cache_wic.push_back( withinInstClosure );
 856     }
 857   }
 858   //only wait if we are doing incremental solving
 859   if( !d_presolve || !options::incrementalSolving() ){
 860     std::set< Node > added;
 861     d_term_db->addTerm(n, added, withinQuant, withinInstClosure);
 862
 863     if (!withinQuant)
 864     {
 865       if (d_sygus_tdb)
 866       {
 867         d_sygus_tdb->registerEvalTerm(n);
 868       }
 869
 870       // added contains also the Node that just have been asserted in this
 871       // branch
 872       if (d_quant_rel)
 873       {
 874         for (std::set<Node>::iterator i = added.begin(), end = added.end();
 875              i != end;
 876              i++)
 877         {
 878           d_quant_rel->setRelevance( i->getOperator(), 0 );
 879         }
 880       }
 881     }
 882   }
 883 }
 884
 885 void QuantifiersEngine::eqNotifyNewClass(TNode t) {
 886   addTermToDatabase( t );
 887   if( d_eq_inference ){
 888     d_eq_inference->eqNotifyNewClass( t );
 889   }
 890 }
 891
 892 void QuantifiersEngine::eqNotifyPreMerge(TNode t1, TNode t2) {
 893   if( d_eq_inference ){
 894     d_eq_inference->eqNotifyMerge( t1, t2 );
 895   }
 896 }
 897
 898 void QuantifiersEngine::eqNotifyPostMerge(TNode t1, TNode t2) {
 899
 900 }
 901
 902 void QuantifiersEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 903   //if( d_qcf ){
 904   //  d_qcf->assertDisequal( t1, t2 );
 905   //}
 906 }
 907
 908 bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
 909   if( doCache ){
 910     if( doRewrite ){
 911       lem = Rewriter::rewrite(lem);
 912     }
 913     Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl;
 914     BoolMap::const_iterator itp = d_lemmas_produced_c.find( lem );
 915     if( itp==d_lemmas_produced_c.end() || !(*itp).second ){
 916       //d_curr_out->lemma( lem, false, true );
 917       d_lemmas_produced_c[ lem ] = true;
 918       d_lemmas_waiting.push_back( lem );
 919       Trace("inst-add-debug") << "Added lemma" << std::endl;
 920       return true;
 921     }else{
 922       Trace("inst-add-debug") << "Duplicate." << std::endl;
 923       return false;
 924     }
 925   }else{
 926     //do not need to rewrite, will be rewritten after sending
 927     d_lemmas_waiting.push_back( lem );
 928     return true;
 929   }
 930 }
 931
 932 bool QuantifiersEngine::removeLemma( Node lem ) {
 933   std::vector< Node >::iterator it = std::find( d_lemmas_waiting.begin(), d_lemmas_waiting.end(), lem );
 934   if( it!=d_lemmas_waiting.end() ){
 935     d_lemmas_waiting.erase( it, it + 1 );
 936     d_lemmas_produced_c[ lem ] = false;
 937     return true;
 938   }else{
 939     return false;
 940   }
 941 }
 942
 943 void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
 944   d_phase_req_waiting[lit] = req;
 945 }
 946
 947 bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
 948   n = Rewriter::rewrite( n );
 949   Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() );
 950   if( addLemma( lem ) ){
 951     Debug("inst") << "*** Add split " << n<< std::endl;
 952     return true;
 953   }
 954   return false;
 955 }
 956
 957 bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool reqPhasePol ){
 958   //Assert( !areEqual( n1, n2 ) );
 959   //Assert( !areDisequal( n1, n2 ) );
 960   Node fm = NodeManager::currentNM()->mkNode( EQUAL, n1, n2 );
 961   return addSplit( fm );
 962 }
 963
 964 bool QuantifiersEngine::addEPRAxiom( TypeNode tn ) {
 965   if( d_qepr ){
 966     Assert( !options::incrementalSolving() );
 967     if( d_qepr->isEPR( tn ) && !d_qepr->hasEPRAxiom( tn ) ){
 968       Node lem = d_qepr->mkEPRAxiom( tn );
 969       Trace("quant-epr") << "EPR lemma for " << tn << " : " << lem << std::endl;
 970       getOutputChannel().lemma( lem );
 971     }
 972   }
 973   return false;
 974 }
 975
 976 void QuantifiersEngine::markRelevant( Node q ) {
 977   d_model->markRelevant( q );
 978 }
 979
 980 void QuantifiersEngine::setConflict() {
 981   d_conflict = true;
 982   d_conflict_c = true;
 983 }
 984
 985 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
 986   Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
 987   //determine if we should perform check, based on instWhenMode
 988   bool performCheck = false;
 989   if( options::instWhenMode()==quantifiers::INST_WHEN_FULL ){
 990     performCheck = ( e >= Theory::EFFORT_FULL );
 991   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){
 992     performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck();
 993   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){
 994     performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
 995   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL ){
 996     performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
 997   }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){
 998     performCheck = ( e >= Theory::EFFORT_LAST_CALL );
 999   }else{
1000     performCheck = true;
1001   }
1002   if( e==Theory::EFFORT_LAST_CALL ){
1003     //with bounded integers, skip every other last call,
1004     // since matching loops may occur with infinite quantification
1005     if( d_ierCounter_lc%2==0 && options::fmfBound() ){
1006       performCheck = false;
1007     }
1008   }
1009   return performCheck;
1010 }
1011
1012 quantifiers::UserPatMode QuantifiersEngine::getInstUserPatMode() {
1013   if( options::userPatternsQuant()==quantifiers::USER_PAT_MODE_INTERLEAVE ){
1014     return d_ierCounter%2==0 ? quantifiers::USER_PAT_MODE_USE : quantifiers::USER_PAT_MODE_RESORT;
1015   }else{
1016     return options::userPatternsQuant();
1017   }
1018 }
1019
1020 void QuantifiersEngine::flushLemmas(){
1021   if( !d_lemmas_waiting.empty() ){
1022     //filter based on notify classes
1023     if (d_instantiate->hasNotify())
1024     {
1025       unsigned prev_lem_sz = d_lemmas_waiting.size();
1026       d_instantiate->notifyFlushLemmas();
1027       if( prev_lem_sz!=d_lemmas_waiting.size() ){
1028         Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting.size() << " / " << prev_lem_sz << std::endl;
1029       }
1030     }
1031     //take default output channel if none is provided
1032     d_hasAddedLemma = true;
1033     for( unsigned i=0; i<d_lemmas_waiting.size(); i++ ){
1034       Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting[i] << std::endl;
1035       getOutputChannel().lemma( d_lemmas_waiting[i], false, true );
1036     }
1037     d_lemmas_waiting.clear();
1038   }
1039   if( !d_phase_req_waiting.empty() ){
1040     for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){
1041       Trace("qe-lemma") << "Require phase : " << it->first << " -> " << it->second << std::endl;
1042       getOutputChannel().requirePhase( it->first, it->second );
1043     }
1044     d_phase_req_waiting.clear();
1045   }
1046 }
1047
1048 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) {
1049   return d_instantiate->getUnsatCoreLemmas(active_lemmas);
1050 }
1051
1052 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp ) {
1053   return d_instantiate->getUnsatCoreLemmas(active_lemmas, weak_imp);
1054 }
1055
1056 void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
1057   d_instantiate->getInstantiationTermVectors(q, tvecs);
1058 }
1059
1060 void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
1061   d_instantiate->getInstantiationTermVectors(insts);
1062 }
1063
1064 void QuantifiersEngine::getExplanationForInstLemmas(
1065     const std::vector<Node>& lems,
1066     std::map<Node, Node>& quant,
1067     std::map<Node, std::vector<Node> >& tvec)
1068 {
1069   d_instantiate->getExplanationForInstLemmas(lems, quant, tvec);
1070 }
1071
1072 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
1073   bool printed = false;
1074   // print the skolemizations
1075   if (d_skolemize->printSkolemization(out))
1076   {
1077     printed = true;
1078   }
1079   // print the instantiations
1080   if (d_instantiate->printInstantiations(out))
1081   {
1082     printed = true;
1083   }
1084   if( !printed ){
1085     out << "No instantiations" << std::endl;
1086   }
1087 }
1088
1089 void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
1090   if( d_ceg_inst ){
1091     d_ceg_inst->printSynthSolution( out );
1092   }else{
1093     out << "Internal error : module for synth solution not found." << std::endl;
1094   }
1095 }
1096
1097 void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
1098   d_instantiate->getInstantiatedQuantifiedFormulas(qs);
1099 }
1100
1101 void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
1102   d_instantiate->getInstantiations(insts);
1103 }
1104
1105 void QuantifiersEngine::getInstantiations( Node q, std::vector< Node >& insts  ) {
1106   d_instantiate->getInstantiations(q, insts);
1107 }
1108
1109 Node QuantifiersEngine::getInstantiatedConjunction( Node q ) {
1110   return d_instantiate->getInstantiatedConjunction(q);
1111 }
1112
1113 QuantifiersEngine::Statistics::Statistics()
1114     : d_time("theory::QuantifiersEngine::time"),
1115       d_qcf_time("theory::QuantifiersEngine::time_qcf"),
1116       d_ematching_time("theory::QuantifiersEngine::time_ematching"),
1117       d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
1118       d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
1119       d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
1120       d_triggers("QuantifiersEngine::Triggers", 0),
1121       d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
1122       d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
1123       d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
1124       d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
1125       d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
1126       d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
1127       d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
1128       d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0),
1129       d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0),
1130       d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0),
1131       d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0),
1132       d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0),
1133       d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0)
1134 {
1135   smtStatisticsRegistry()->registerStat(&d_time);
1136   smtStatisticsRegistry()->registerStat(&d_qcf_time);
1137   smtStatisticsRegistry()->registerStat(&d_ematching_time);
1138   smtStatisticsRegistry()->registerStat(&d_num_quant);
1139   smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
1140   smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
1141   smtStatisticsRegistry()->registerStat(&d_triggers);
1142   smtStatisticsRegistry()->registerStat(&d_simple_triggers);
1143   smtStatisticsRegistry()->registerStat(&d_multi_triggers);
1144   smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations);
1145   smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
1146   smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns);
1147   smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen);
1148   smtStatisticsRegistry()->registerStat(&d_instantiations_guess);
1149   smtStatisticsRegistry()->registerStat(&d_instantiations_qcf);
1150   smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop);
1151   smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh);
1152   smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi);
1153   smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi);
1154   smtStatisticsRegistry()->registerStat(&d_instantiations_rr);
1155 }
1156
1157 QuantifiersEngine::Statistics::~Statistics(){
1158   smtStatisticsRegistry()->unregisterStat(&d_time);
1159   smtStatisticsRegistry()->unregisterStat(&d_qcf_time);
1160   smtStatisticsRegistry()->unregisterStat(&d_ematching_time);
1161   smtStatisticsRegistry()->unregisterStat(&d_num_quant);
1162   smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
1163   smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
1164   smtStatisticsRegistry()->unregisterStat(&d_triggers);
1165   smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
1166   smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
1167   smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations);
1168   smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
1169   smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns);
1170   smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen);
1171   smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess);
1172   smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf);
1173   smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop);
1174   smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh);
1175   smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi);
1176   smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi);
1177   smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr);
1178 }
1179
1180 eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
1181   return d_te->getMasterEqualityEngine();
1182 }
1183
1184 eq::EqualityEngine* QuantifiersEngine::getActiveEqualityEngine() {
1185   if( d_useModelEe ){
1186     return d_model->getEqualityEngine();
1187   }else{
1188     return d_te->getMasterEqualityEngine();
1189   }
1190 }
1191
1192 Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
1193   bool prevModelEe = d_useModelEe;
1194   d_useModelEe = false;
1195   Node ret = d_eq_query->getInternalRepresentative( a, q, index );
1196   d_useModelEe = prevModelEe;
1197   return ret;
1198 }
1199
1200 void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
1201   eq::EqualityEngine* ee = getActiveEqualityEngine();
1202   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
1203   std::map< TypeNode, int > typ_num;
1204   while( !eqcs_i.isFinished() ){
1205     TNode r = (*eqcs_i);
1206     TypeNode tr = r.getType();
1207     if( typ_num.find( tr )==typ_num.end() ){
1208       typ_num[tr] = 0;
1209     }
1210     typ_num[tr]++;
1211     bool firstTime = true;
1212     Trace(c) << "  " << r;
1213     Trace(c) << " : { ";
1214     eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
1215     while( !eqc_i.isFinished() ){
1216       TNode n = (*eqc_i);
1217       if( r!=n ){
1218         if( firstTime ){
1219           Trace(c) << std::endl;
1220           firstTime = false;
1221         }
1222         Trace(c) << "    " << n << std::endl;
1223       }
1224       ++eqc_i;
1225     }
1226     if( !firstTime ){ Trace(c) << "  "; }
1227     Trace(c) << "}" << std::endl;
1228     ++eqcs_i;
1229   }
1230   Trace(c) << std::endl;
1231   for( std::map< TypeNode, int >::iterator it = typ_num.begin(); it != typ_num.end(); ++it ){
1232     Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl;
1233   }
1234 }
1235