src/theory/quantifiers_engine.cpp

   1 /*********************                                                        */
   2 /*! \file quantifiers_engine.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Tim King, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 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/cegqi/ceg_t_instantiator.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   bool needsCheck = !d_lemmas_waiting.empty();
 435   QuantifiersModule::QEffort needsModelE = QuantifiersModule::QEFFORT_NONE;
 436   std::vector< QuantifiersModule* > qm;
 437   if( d_model->checkNeeded() ){
 438     needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
 439     for (QuantifiersModule*& mdl : d_modules)
 440     {
 441       if (mdl->needsCheck(e))
 442       {
 443         qm.push_back(mdl);
 444         needsCheck = true;
 445         //can only request model at last call since theory combination can find inconsistencies
 446         if( e>=Theory::EFFORT_LAST_CALL ){
 447           QuantifiersModule::QEffort me = mdl->needsModel(e);
 448           needsModelE = me<needsModelE ? me : needsModelE;
 449         }
 450       }
 451     }
 452   }
 453
 454   d_conflict = false;
 455   d_hasAddedLemma = false;
 456   bool setIncomplete = false;
 457
 458   Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
 459   if( needsCheck ){
 460     //this will fail if a set of instances is marked as a conflict, but is not
 461     Assert( !d_conflict_c.get() );
 462     //flush previous lemmas (for instance, if was interupted), or other lemmas to process
 463     flushLemmas();
 464     if( d_hasAddedLemma ){
 465       return;
 466     }
 467
 468     double clSet = 0;
 469     if( Trace.isOn("quant-engine") ){
 470       clSet = double(clock())/double(CLOCKS_PER_SEC);
 471       Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e << " <<<<<" << std::endl;
 472     }
 473
 474     if( Trace.isOn("quant-engine-debug") ){
 475       Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
 476       Trace("quant-engine-debug") << "  depth : " << d_ierCounter_c << std::endl;
 477       Trace("quant-engine-debug") << "  modules to check : ";
 478       for( unsigned i=0; i<qm.size(); i++ ){
 479         Trace("quant-engine-debug") << qm[i]->identify() << " ";
 480       }
 481       Trace("quant-engine-debug") << std::endl;
 482       Trace("quant-engine-debug") << "  # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
 483       if( !d_lemmas_waiting.empty() ){
 484         Trace("quant-engine-debug") << "  lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
 485       }
 486       Trace("quant-engine-debug") << "  Theory engine finished : " << !d_te->needCheck() << std::endl;
 487       Trace("quant-engine-debug") << "  Needs model effort : " << needsModelE << std::endl;
 488     }
 489     if( Trace.isOn("quant-engine-ee-pre") ){
 490       Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
 491       debugPrintEqualityEngine( "quant-engine-ee-pre" );
 492     }
 493     if( Trace.isOn("quant-engine-assert") ){
 494       Trace("quant-engine-assert") << "Assertions : " << std::endl;
 495       getTheoryEngine()->printAssertions("quant-engine-assert");
 496     }
 497
 498     //reset utilities
 499     Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl;
 500     for (QuantifiersUtil*& util : d_util)
 501     {
 502       Trace("quant-engine-debug2") << "Reset " << util->identify().c_str()
 503                                    << "..." << std::endl;
 504       if (!util->reset(e))
 505       {
 506         flushLemmas();
 507         if( d_hasAddedLemma ){
 508           return;
 509         }else{
 510           //should only fail reset if added a lemma
 511           Assert( false );
 512         }
 513       }
 514     }
 515
 516     if( Trace.isOn("quant-engine-ee") ){
 517       Trace("quant-engine-ee") << "Equality engine : " << std::endl;
 518       debugPrintEqualityEngine( "quant-engine-ee" );
 519     }
 520
 521     //reset the model
 522     Trace("quant-engine-debug") << "Reset model..." << std::endl;
 523     d_model->reset_round();
 524
 525     //reset the modules
 526     Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
 527     for (QuantifiersModule*& mdl : d_modules)
 528     {
 529       Trace("quant-engine-debug2") << "Reset " << mdl->identify().c_str()
 530                                    << std::endl;
 531       mdl->reset_round(e);
 532     }
 533     Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
 534     //reset may have added lemmas
 535     flushLemmas();
 536     if( d_hasAddedLemma ){
 537       return;
 538     }
 539
 540     if( e==Theory::EFFORT_LAST_CALL ){
 541       //if effort is last call, try to minimize model first
 542       //uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
 543       //if( ufss && !ufss->minimize() ){ return; }
 544       ++(d_statistics.d_instantiation_rounds_lc);
 545     }else if( e==Theory::EFFORT_FULL ){
 546       ++(d_statistics.d_instantiation_rounds);
 547     }
 548     Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
 549     for (unsigned qef = QuantifiersModule::QEFFORT_CONFLICT;
 550          qef <= QuantifiersModule::QEFFORT_LAST_CALL;
 551          ++qef)
 552     {
 553       QuantifiersModule::QEffort quant_e =
 554           static_cast<QuantifiersModule::QEffort>(qef);
 555       d_curr_effort_level = quant_e;
 556       //build the model if any module requested it
 557       if (needsModelE == quant_e)
 558       {
 559         if (!d_model->isBuilt())
 560         {
 561           // theory engine's model builder is quantifier engine's builder if it
 562           // has one
 563           Assert(!d_builder || d_builder == d_te->getModelBuilder());
 564           Trace("quant-engine-debug") << "Build model..." << std::endl;
 565           if (!d_te->getModelBuilder()->buildModel(d_model))
 566           {
 567             flushLemmas();
 568           }
 569         }
 570         if (!d_model->isBuiltSuccess())
 571         {
 572           break;
 573         }
 574       }
 575       if( !d_hasAddedLemma ){
 576         //check each module
 577         for (QuantifiersModule*& mdl : qm)
 578         {
 579           Trace("quant-engine-debug") << "Check " << mdl->identify().c_str()
 580                                       << " at effort " << quant_e << "..."
 581                                       << std::endl;
 582           mdl->check(e, quant_e);
 583           if( d_conflict ){
 584             Trace("quant-engine-debug") << "...conflict!" << std::endl;
 585             break;
 586           }
 587         }
 588         //flush all current lemmas
 589         flushLemmas();
 590       }
 591       //if we have added one, stop
 592       if( d_hasAddedLemma ){
 593         break;
 594       }else{
 595         Assert( !d_conflict );
 596         if (quant_e == QuantifiersModule::QEFFORT_CONFLICT)
 597         {
 598           if( e==Theory::EFFORT_FULL ){
 599             //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase
 600             if( d_ierCounterLastLc!=d_ierCounter_lc || !options::instWhenStrictInterleave() || d_ierCounter%d_inst_when_phase!=0 ){
 601               d_ierCounter = d_ierCounter + 1;
 602               d_ierCounterLastLc = d_ierCounter_lc;
 603               d_ierCounter_c = d_ierCounter_c.get() + 1;
 604             }
 605           }else if( e==Theory::EFFORT_LAST_CALL ){
 606             d_ierCounter_lc = d_ierCounter_lc + 1;
 607           }
 608         }
 609         else if (quant_e == QuantifiersModule::QEFFORT_MODEL)
 610         {
 611           if( e==Theory::EFFORT_LAST_CALL ){
 612             //sources of incompleteness
 613             for (QuantifiersUtil*& util : d_util)
 614             {
 615               if (!util->checkComplete())
 616               {
 617                 Trace("quant-engine-debug") << "Set incomplete because utility "
 618                                             << util->identify().c_str()
 619                                             << " was incomplete." << std::endl;
 620                 setIncomplete = true;
 621               }
 622             }
 623             //if we have a chance not to set incomplete
 624             if( !setIncomplete ){
 625               //check if we should set the incomplete flag
 626               for (QuantifiersModule*& mdl : d_modules)
 627               {
 628                 if (!mdl->checkComplete())
 629                 {
 630                   Trace("quant-engine-debug")
 631                       << "Set incomplete because module "
 632                       << mdl->identify().c_str() << " was incomplete."
 633                       << std::endl;
 634                   setIncomplete = true;
 635                   break;
 636                 }
 637               }
 638               if( !setIncomplete ){
 639                 //look at individual quantified formulas, one module must claim completeness for each one
 640                 for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
 641                   bool hasCompleteM = false;
 642                   Node q = d_model->getAssertedQuantifier( i );
 643                   QuantifiersModule * qmd = getOwner( q );
 644                   if( qmd!=NULL ){
 645                     hasCompleteM = qmd->checkCompleteFor( q );
 646                   }else{
 647                     for( unsigned j=0; j<d_modules.size(); j++ ){
 648                       if( d_modules[j]->checkCompleteFor( q ) ){
 649                         qmd = d_modules[j];
 650                         hasCompleteM = true;
 651                         break;
 652                       }
 653                     }
 654                   }
 655                   if( !hasCompleteM ){
 656                     Trace("quant-engine-debug") << "Set incomplete because " << q << " was not fully processed." << std::endl;
 657                     setIncomplete = true;
 658                     break;
 659                   }else{
 660                     Assert( qmd!=NULL );
 661                     Trace("quant-engine-debug2") << "Complete for " << q << " due to " << qmd->identify().c_str() << std::endl;
 662                   }
 663                 }
 664               }
 665             }
 666             //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL
 667             if( !setIncomplete ){
 668               break;
 669             }
 670           }
 671         }
 672       }
 673     }
 674     d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
 675     Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
 676     if( d_hasAddedLemma ){
 677       d_instantiate->debugPrint();
 678     }
 679     if( Trace.isOn("quant-engine") ){
 680       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
 681       Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2-clSet);
 682       Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma;
 683       Trace("quant-engine") << std::endl;
 684     }
 685
 686     Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl;
 687   }else{
 688     Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl;
 689   }
 690
 691   //SAT case
 692   if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
 693     if( setIncomplete ){
 694       Trace("quant-engine") << "Set incomplete flag." << std::endl;
 695       getOutputChannel().setIncomplete();
 696     }
 697     //output debug stats
 698     d_instantiate->debugPrintModel();
 699   }
 700 }
 701
 702 void QuantifiersEngine::notifyCombineTheories() {
 703   //if allowing theory combination to happen at most once between instantiation rounds
 704   //d_ierCounter = 1;
 705   //d_ierCounterLastLc = -1;
 706 }
 707
 708 bool QuantifiersEngine::reduceQuantifier( Node q ) {
 709   //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants
 710   BoolMap::const_iterator it = d_quants_red.find( q );
 711   if( it==d_quants_red.end() ){
 712     Node lem;
 713     std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q );
 714     if( itr==d_quants_red_lem.end() ){
 715       if( d_alpha_equiv ){
 716         Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
 717         //add equivalence with another quantified formula
 718         lem = d_alpha_equiv->reduceQuantifier( q );
 719         if( !lem.isNull() ){
 720           Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
 721           ++(d_statistics.d_red_alpha_equiv);
 722         }
 723       }
 724       d_quants_red_lem[q] = lem;
 725     }else{
 726       lem = itr->second;
 727     }
 728     if( !lem.isNull() ){
 729       getOutputChannel().lemma( lem );
 730     }
 731     d_quants_red[q] = !lem.isNull();
 732     return !lem.isNull();
 733   }else{
 734     return (*it).second;
 735   }
 736 }
 737
 738 void QuantifiersEngine::registerQuantifierInternal(Node f)
 739 {
 740   std::map< Node, bool >::iterator it = d_quants.find( f );
 741   if( it==d_quants.end() ){
 742     Trace("quant") << "QuantifiersEngine : Register quantifier ";
 743     Trace("quant") << " : " << f << std::endl;
 744     unsigned prev_lemma_waiting = d_lemmas_waiting.size();
 745     ++(d_statistics.d_num_quant);
 746     Assert( f.getKind()==FORALL );
 747     // register with utilities
 748     for (unsigned i = 0; i < d_util.size(); i++)
 749     {
 750       d_util[i]->registerQuantifier(f);
 751     }
 752     // compute attributes
 753     d_quant_attr->computeAttributes(f);
 754
 755     for (QuantifiersModule*& mdl : d_modules)
 756     {
 757       Trace("quant-debug") << "check ownership with " << mdl->identify()
 758                            << "..." << std::endl;
 759       mdl->checkOwnership(f);
 760     }
 761     QuantifiersModule* qm = getOwner(f);
 762     Trace("quant") << " Owner : " << (qm == nullptr ? "[none]" : qm->identify())
 763                    << std::endl;
 764     // register with each module
 765     for (QuantifiersModule*& mdl : d_modules)
 766     {
 767       Trace("quant-debug") << "register with " << mdl->identify() << "..."
 768                            << std::endl;
 769       mdl->registerQuantifier(f);
 770       // since this is context-independent, we should not add any lemmas during
 771       // this call
 772       Assert(d_lemmas_waiting.size() == prev_lemma_waiting);
 773     }
 774     // TODO (#2020): remove this
 775     Node ceBody = d_term_util->getInstConstantBody(f);
 776     Trace("quant-debug") << "...finish." << std::endl;
 777     d_quants[f] = true;
 778     AlwaysAssert(d_lemmas_waiting.size() == prev_lemma_waiting);
 779   }
 780 }
 781
 782 void QuantifiersEngine::preRegisterQuantifier(Node q)
 783 {
 784   NodeSet::const_iterator it = d_quants_prereg.find(q);
 785   if (it != d_quants_prereg.end())
 786   {
 787     return;
 788   }
 789   Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q << std::endl;
 790   d_quants_prereg.insert(q);
 791   // ensure that it is registered
 792   registerQuantifierInternal(q);
 793   // register with each module
 794   for (QuantifiersModule*& mdl : d_modules)
 795   {
 796     Trace("quant-debug") << "pre-register with " << mdl->identify() << "..."
 797                          << std::endl;
 798     mdl->preRegisterQuantifier(q);
 799   }
 800   // flush the lemmas
 801   flushLemmas();
 802   Trace("quant-debug") << "...finish pre-register " << q << "..." << std::endl;
 803 }
 804
 805 void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
 806   for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){
 807     std::set< Node > added;
 808     getTermDatabase()->addTerm( *p, added );
 809   }
 810 }
 811
 812 void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
 813   if (reduceQuantifier(f))
 814   {
 815     // if we can reduce it, nothing left to do
 816     return;
 817   }
 818   if( !pol ){
 819     // do skolemization
 820     Node lem = d_skolemize->process(f);
 821     if (!lem.isNull())
 822     {
 823       if (Trace.isOn("quantifiers-sk-debug"))
 824       {
 825         Node slem = Rewriter::rewrite(lem);
 826         Trace("quantifiers-sk-debug")
 827             << "Skolemize lemma : " << slem << std::endl;
 828       }
 829       getOutputChannel().lemma(lem, false, true);
 830     }
 831     return;
 832   }
 833   // ensure the quantified formula is registered
 834   registerQuantifierInternal(f);
 835   // assert it to each module
 836   d_model->assertQuantifier(f);
 837   for (QuantifiersModule*& mdl : d_modules)
 838   {
 839     mdl->assertNode(f);
 840   }
 841   addTermToDatabase(d_term_util->getInstConstantBody(f), true);
 842 }
 843
 844 void QuantifiersEngine::propagate( Theory::Effort level ){
 845   CodeTimer codeTimer(d_statistics.d_time);
 846
 847 }
 848
 849 Node QuantifiersEngine::getNextDecisionRequest( unsigned& priority ){
 850   unsigned min_priority = 0;
 851   Node dec;
 852   for( unsigned i=0; i<d_modules.size(); i++ ){
 853     Node n = d_modules[i]->getNextDecisionRequest( priority );
 854     if( !n.isNull() && ( dec.isNull() || priority<min_priority ) ){
 855       dec = n;
 856       min_priority = priority;
 857     }
 858   }
 859   return dec;
 860 }
 861
 862 void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
 863   if( options::incrementalSolving() ){
 864     if( d_presolve_in.find( n )==d_presolve_in.end() ){
 865       d_presolve_in.insert( n );
 866       d_presolve_cache.push_back( n );
 867       d_presolve_cache_wq.push_back( withinQuant );
 868       d_presolve_cache_wic.push_back( withinInstClosure );
 869     }
 870   }
 871   //only wait if we are doing incremental solving
 872   if( !d_presolve || !options::incrementalSolving() ){
 873     std::set< Node > added;
 874     d_term_db->addTerm(n, added, withinQuant, withinInstClosure);
 875
 876     if (!withinQuant)
 877     {
 878       if (d_sygus_tdb)
 879       {
 880         d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n);
 881       }
 882
 883       // added contains also the Node that just have been asserted in this
 884       // branch
 885       if (d_quant_rel)
 886       {
 887         for (std::set<Node>::iterator i = added.begin(), end = added.end();
 888              i != end;
 889              i++)
 890         {
 891           d_quant_rel->setRelevance( i->getOperator(), 0 );
 892         }
 893       }
 894     }
 895   }
 896 }
 897
 898 void QuantifiersEngine::eqNotifyNewClass(TNode t) {
 899   addTermToDatabase( t );
 900   if( d_eq_inference ){
 901     d_eq_inference->eqNotifyNewClass( t );
 902   }
 903 }
 904
 905 void QuantifiersEngine::eqNotifyPreMerge(TNode t1, TNode t2) {
 906   if( d_eq_inference ){
 907     d_eq_inference->eqNotifyMerge( t1, t2 );
 908   }
 909 }
 910
 911 void QuantifiersEngine::eqNotifyPostMerge(TNode t1, TNode t2) {
 912
 913 }
 914
 915 void QuantifiersEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 916   //if( d_qcf ){
 917   //  d_qcf->assertDisequal( t1, t2 );
 918   //}
 919 }
 920
 921 bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
 922   if( doCache ){
 923     if( doRewrite ){
 924       lem = Rewriter::rewrite(lem);
 925     }
 926     Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl;
 927     BoolMap::const_iterator itp = d_lemmas_produced_c.find( lem );
 928     if( itp==d_lemmas_produced_c.end() || !(*itp).second ){
 929       //d_curr_out->lemma( lem, false, true );
 930       d_lemmas_produced_c[ lem ] = true;
 931       d_lemmas_waiting.push_back( lem );
 932       Trace("inst-add-debug") << "Added lemma" << std::endl;
 933       return true;
 934     }else{
 935       Trace("inst-add-debug") << "Duplicate." << std::endl;
 936       return false;
 937     }
 938   }else{
 939     //do not need to rewrite, will be rewritten after sending
 940     d_lemmas_waiting.push_back( lem );
 941     return true;
 942   }
 943 }
 944
 945 bool QuantifiersEngine::removeLemma( Node lem ) {
 946   std::vector< Node >::iterator it = std::find( d_lemmas_waiting.begin(), d_lemmas_waiting.end(), lem );
 947   if( it!=d_lemmas_waiting.end() ){
 948     d_lemmas_waiting.erase( it, it + 1 );
 949     d_lemmas_produced_c[ lem ] = false;
 950     return true;
 951   }else{
 952     return false;
 953   }
 954 }
 955
 956 void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
 957   d_phase_req_waiting[lit] = req;
 958 }
 959
 960 bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
 961   n = Rewriter::rewrite( n );
 962   Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() );
 963   if( addLemma( lem ) ){
 964     Debug("inst") << "*** Add split " << n<< std::endl;
 965     return true;
 966   }
 967   return false;
 968 }
 969
 970 bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool reqPhasePol ){
 971   //Assert( !areEqual( n1, n2 ) );
 972   //Assert( !areDisequal( n1, n2 ) );
 973   Node fm = NodeManager::currentNM()->mkNode( EQUAL, n1, n2 );
 974   return addSplit( fm );
 975 }
 976
 977 bool QuantifiersEngine::addEPRAxiom( TypeNode tn ) {
 978   if( d_qepr ){
 979     Assert( !options::incrementalSolving() );
 980     if( d_qepr->isEPR( tn ) && !d_qepr->hasEPRAxiom( tn ) ){
 981       Node lem = d_qepr->mkEPRAxiom( tn );
 982       Trace("quant-epr") << "EPR lemma for " << tn << " : " << lem << std::endl;
 983       getOutputChannel().lemma( lem );
 984     }
 985   }
 986   return false;
 987 }
 988
 989 void QuantifiersEngine::markRelevant( Node q ) {
 990   d_model->markRelevant( q );
 991 }
 992
 993 void QuantifiersEngine::setConflict() {
 994   d_conflict = true;
 995   d_conflict_c = true;
 996 }
 997
 998 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
 999   Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
1000   //determine if we should perform check, based on instWhenMode
1001   bool performCheck = false;
1002   if( options::instWhenMode()==quantifiers::INST_WHEN_FULL ){
1003     performCheck = ( e >= Theory::EFFORT_FULL );
1004   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){
1005     performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck();
1006   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){
1007     performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
1008   }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL ){
1009     performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
1010   }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){
1011     performCheck = ( e >= Theory::EFFORT_LAST_CALL );
1012   }else{
1013     performCheck = true;
1014   }
1015   if( e==Theory::EFFORT_LAST_CALL ){
1016     //with bounded integers, skip every other last call,
1017     // since matching loops may occur with infinite quantification
1018     if( d_ierCounter_lc%2==0 && options::fmfBound() ){
1019       performCheck = false;
1020     }
1021   }
1022   return performCheck;
1023 }
1024
1025 quantifiers::UserPatMode QuantifiersEngine::getInstUserPatMode() {
1026   if( options::userPatternsQuant()==quantifiers::USER_PAT_MODE_INTERLEAVE ){
1027     return d_ierCounter%2==0 ? quantifiers::USER_PAT_MODE_USE : quantifiers::USER_PAT_MODE_RESORT;
1028   }else{
1029     return options::userPatternsQuant();
1030   }
1031 }
1032
1033 void QuantifiersEngine::flushLemmas(){
1034   if( !d_lemmas_waiting.empty() ){
1035     //filter based on notify classes
1036     if (d_instantiate->hasNotify())
1037     {
1038       unsigned prev_lem_sz = d_lemmas_waiting.size();
1039       d_instantiate->notifyFlushLemmas();
1040       if( prev_lem_sz!=d_lemmas_waiting.size() ){
1041         Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting.size() << " / " << prev_lem_sz << std::endl;
1042       }
1043     }
1044     //take default output channel if none is provided
1045     d_hasAddedLemma = true;
1046     for( unsigned i=0; i<d_lemmas_waiting.size(); i++ ){
1047       Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting[i] << std::endl;
1048       getOutputChannel().lemma( d_lemmas_waiting[i], false, true );
1049     }
1050     d_lemmas_waiting.clear();
1051   }
1052   if( !d_phase_req_waiting.empty() ){
1053     for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){
1054       Trace("qe-lemma") << "Require phase : " << it->first << " -> " << it->second << std::endl;
1055       getOutputChannel().requirePhase( it->first, it->second );
1056     }
1057     d_phase_req_waiting.clear();
1058   }
1059 }
1060
1061 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) {
1062   return d_instantiate->getUnsatCoreLemmas(active_lemmas);
1063 }
1064
1065 bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp ) {
1066   return d_instantiate->getUnsatCoreLemmas(active_lemmas, weak_imp);
1067 }
1068
1069 void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
1070   d_instantiate->getInstantiationTermVectors(q, tvecs);
1071 }
1072
1073 void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
1074   d_instantiate->getInstantiationTermVectors(insts);
1075 }
1076
1077 void QuantifiersEngine::getExplanationForInstLemmas(
1078     const std::vector<Node>& lems,
1079     std::map<Node, Node>& quant,
1080     std::map<Node, std::vector<Node> >& tvec)
1081 {
1082   d_instantiate->getExplanationForInstLemmas(lems, quant, tvec);
1083 }
1084
1085 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
1086   bool printed = false;
1087   // print the skolemizations
1088   if (d_skolemize->printSkolemization(out))
1089   {
1090     printed = true;
1091   }
1092   // print the instantiations
1093   if (d_instantiate->printInstantiations(out))
1094   {
1095     printed = true;
1096   }
1097   if( !printed ){
1098     out << "No instantiations" << std::endl;
1099   }
1100 }
1101
1102 void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
1103   if( d_ceg_inst ){
1104     d_ceg_inst->printSynthSolution( out );
1105   }else{
1106     out << "Internal error : module for synth solution not found." << std::endl;
1107   }
1108 }
1109
1110 void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
1111   d_instantiate->getInstantiatedQuantifiedFormulas(qs);
1112 }
1113
1114 void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
1115   d_instantiate->getInstantiations(insts);
1116 }
1117
1118 void QuantifiersEngine::getInstantiations( Node q, std::vector< Node >& insts  ) {
1119   d_instantiate->getInstantiations(q, insts);
1120 }
1121
1122 Node QuantifiersEngine::getInstantiatedConjunction( Node q ) {
1123   return d_instantiate->getInstantiatedConjunction(q);
1124 }
1125
1126 QuantifiersEngine::Statistics::Statistics()
1127     : d_time("theory::QuantifiersEngine::time"),
1128       d_qcf_time("theory::QuantifiersEngine::time_qcf"),
1129       d_ematching_time("theory::QuantifiersEngine::time_ematching"),
1130       d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
1131       d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
1132       d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
1133       d_triggers("QuantifiersEngine::Triggers", 0),
1134       d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
1135       d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
1136       d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
1137       d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
1138       d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
1139       d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
1140       d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
1141       d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0),
1142       d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0),
1143       d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0),
1144       d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0),
1145       d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0),
1146       d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0)
1147 {
1148   smtStatisticsRegistry()->registerStat(&d_time);
1149   smtStatisticsRegistry()->registerStat(&d_qcf_time);
1150   smtStatisticsRegistry()->registerStat(&d_ematching_time);
1151   smtStatisticsRegistry()->registerStat(&d_num_quant);
1152   smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
1153   smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
1154   smtStatisticsRegistry()->registerStat(&d_triggers);
1155   smtStatisticsRegistry()->registerStat(&d_simple_triggers);
1156   smtStatisticsRegistry()->registerStat(&d_multi_triggers);
1157   smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations);
1158   smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
1159   smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns);
1160   smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen);
1161   smtStatisticsRegistry()->registerStat(&d_instantiations_guess);
1162   smtStatisticsRegistry()->registerStat(&d_instantiations_qcf);
1163   smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop);
1164   smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh);
1165   smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi);
1166   smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi);
1167   smtStatisticsRegistry()->registerStat(&d_instantiations_rr);
1168 }
1169
1170 QuantifiersEngine::Statistics::~Statistics(){
1171   smtStatisticsRegistry()->unregisterStat(&d_time);
1172   smtStatisticsRegistry()->unregisterStat(&d_qcf_time);
1173   smtStatisticsRegistry()->unregisterStat(&d_ematching_time);
1174   smtStatisticsRegistry()->unregisterStat(&d_num_quant);
1175   smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
1176   smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
1177   smtStatisticsRegistry()->unregisterStat(&d_triggers);
1178   smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
1179   smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
1180   smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations);
1181   smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
1182   smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns);
1183   smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen);
1184   smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess);
1185   smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf);
1186   smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop);
1187   smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh);
1188   smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi);
1189   smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi);
1190   smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr);
1191 }
1192
1193 eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
1194   return d_te->getMasterEqualityEngine();
1195 }
1196
1197 eq::EqualityEngine* QuantifiersEngine::getActiveEqualityEngine() {
1198   if( d_useModelEe ){
1199     return d_model->getEqualityEngine();
1200   }else{
1201     return d_te->getMasterEqualityEngine();
1202   }
1203 }
1204
1205 Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
1206   bool prevModelEe = d_useModelEe;
1207   d_useModelEe = false;
1208   Node ret = d_eq_query->getInternalRepresentative( a, q, index );
1209   d_useModelEe = prevModelEe;
1210   return ret;
1211 }
1212
1213 void QuantifiersEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
1214 {
1215   d_ceg_inst->getSynthSolutions(sol_map);
1216 }
1217
1218 void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
1219   eq::EqualityEngine* ee = getActiveEqualityEngine();
1220   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
1221   std::map< TypeNode, int > typ_num;
1222   while( !eqcs_i.isFinished() ){
1223     TNode r = (*eqcs_i);
1224     TypeNode tr = r.getType();
1225     if( typ_num.find( tr )==typ_num.end() ){
1226       typ_num[tr] = 0;
1227     }
1228     typ_num[tr]++;
1229     bool firstTime = true;
1230     Trace(c) << "  " << r;
1231     Trace(c) << " : { ";
1232     eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
1233     while( !eqc_i.isFinished() ){
1234       TNode n = (*eqc_i);
1235       if( r!=n ){
1236         if( firstTime ){
1237           Trace(c) << std::endl;
1238           firstTime = false;
1239         }
1240         Trace(c) << "    " << n << std::endl;
1241       }
1242       ++eqc_i;
1243     }
1244     if( !firstTime ){ Trace(c) << "  "; }
1245     Trace(c) << "}" << std::endl;
1246     ++eqcs_i;
1247   }
1248   Trace(c) << std::endl;
1249   for( std::map< TypeNode, int >::iterator it = typ_num.begin(); it != typ_num.end(); ++it ){
1250     Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl;
1251   }
1252 }
1253