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