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