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