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