src/theory/quantifiers_engine.cpp

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