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