src/theory/quantifiers_engine.cpp

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