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