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