src/theory/quantifiers_engine.cpp

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