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