src/theory/quantifiers_engine.cpp

   1 /*********************                                                        */
   2 /*! \file quantifiers_engine.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Mathias Preiner
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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_engine_scope.h"
  20 #include "smt/smt_statistics_registry.h"
  21 #include "theory/quantifiers/fmf/full_model_check.h"
  22 #include "theory/quantifiers/quantifiers_modules.h"
  23 #include "theory/quantifiers/quantifiers_rewriter.h"
  24 #include "theory/theory_engine.h"
  25 #include "theory/uf/equality_engine.h"
  26
  27 using namespace std;
  28 using namespace CVC4::kind;
  29
  30 namespace CVC4 {
  31 namespace theory {
  32
  33 QuantifiersEngine::QuantifiersEngine(TheoryEngine* te,
  34                                      DecisionManager& dm,
  35                                      ProofNodeManager* pnm)
  36     : d_te(te),
  37       d_context(te->getSatContext()),
  38       d_userContext(te->getUserContext()),
  39       d_decManager(dm),
  40       d_masterEqualityEngine(nullptr),
  41       d_eq_query(
  42           new quantifiers::EqualityQueryQuantifiersEngine(d_context, this)),
  43       d_tr_trie(new inst::TriggerTrie),
  44       d_model(nullptr),
  45       d_builder(nullptr),
  46       d_qepr(nullptr),
  47       d_term_util(new quantifiers::TermUtil(this)),
  48       d_term_canon(new expr::TermCanonize),
  49       d_term_db(new quantifiers::TermDb(d_context, d_userContext, this)),
  50       d_sygus_tdb(nullptr),
  51       d_quant_attr(new quantifiers::QuantAttributes(this)),
  52       d_instantiate(new quantifiers::Instantiate(this, d_userContext, pnm)),
  53       d_skolemize(new quantifiers::Skolemize(this, d_userContext, pnm)),
  54       d_term_enum(new quantifiers::TermEnumeration),
  55       d_conflict_c(d_context, false),
  56       d_quants_prereg(d_userContext),
  57       d_quants_red(d_userContext),
  58       d_lemmas_produced_c(d_userContext),
  59       d_ierCounter_c(d_context),
  60       d_presolve(d_userContext, true),
  61       d_presolve_in(d_userContext),
  62       d_presolve_cache(d_userContext),
  63       d_presolve_cache_wq(d_userContext),
  64       d_presolve_cache_wic(d_userContext)
  65 {
  66   //---- utilities
  67   d_util.push_back(d_eq_query.get());
  68   // term util must come before the other utilities
  69   d_util.push_back(d_term_util.get());
  70   d_util.push_back(d_term_db.get());
  71
  72   if (options::sygus() || options::sygusInst())
  73   {
  74     // must be constructed here since it is required for datatypes finistInit
  75     d_sygus_tdb.reset(new quantifiers::TermDbSygus(d_context, this));
  76   }
  77
  78   d_util.push_back(d_instantiate.get());
  79
  80   d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
  81   d_conflict = false;
  82   d_hasAddedLemma = false;
  83   //don't add true lemma
  84   d_lemmas_produced_c[d_term_util->d_true] = true;
  85
  86   Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
  87   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
  88
  89   if( options::quantEpr() ){
  90     Assert(!options::incrementalSolving());
  91     d_qepr.reset(new quantifiers::QuantEPR);
  92   }
  93   //---- end utilities
  94
  95   //allow theory combination to go first, once initially
  96   d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
  97   d_ierCounter_c = d_ierCounter;
  98   d_ierCounter_lc = 0;
  99   d_ierCounterLastLc = 0;
 100   d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
 101
 102   // Finite model finding requires specialized ways of building the model.
 103   // We require constructing the model and model builder here, since it is
 104   // required for initializing the CombinationEngine.
 105   if (options::finiteModelFind() || options::fmfBound())
 106   {
 107     Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl;
 108     if (options::mbqiMode() == options::MbqiMode::FMC
 109         || options::mbqiMode() == options::MbqiMode::TRUST
 110         || options::fmfBound())
 111     {
 112       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
 113       d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
 114           this, d_context, "FirstOrderModelFmc"));
 115       d_builder.reset(
 116           new quantifiers::fmcheck::FullModelChecker(d_context, this));
 117     }else{
 118       Trace("quant-engine-debug") << "...make default model builder." << std::endl;
 119       d_model.reset(
 120           new quantifiers::FirstOrderModel(this, d_context, "FirstOrderModel"));
 121       d_builder.reset(new quantifiers::QModelBuilder(d_context, this));
 122     }
 123   }else{
 124     d_model.reset(
 125         new quantifiers::FirstOrderModel(this, d_context, "FirstOrderModel"));
 126   }
 127 }
 128
 129 QuantifiersEngine::~QuantifiersEngine() {}
 130
 131 void QuantifiersEngine::finishInit()
 132 {
 133   // Initialize the modules and the utilities here. We delay their
 134   // initialization to here, since this is after TheoryQuantifiers finishInit,
 135   // which has initialized the state and inference manager of this engine.
 136   d_qmodules.reset(new quantifiers::QuantifiersModules);
 137   d_qmodules->initialize(this, d_context, d_modules);
 138   if (d_qmodules->d_rel_dom.get())
 139   {
 140     d_util.push_back(d_qmodules->d_rel_dom.get());
 141   }
 142 }
 143
 144 void QuantifiersEngine::setMasterEqualityEngine(eq::EqualityEngine* mee)
 145 {
 146   d_masterEqualityEngine = mee;
 147 }
 148
 149 TheoryEngine* QuantifiersEngine::getTheoryEngine() const { return d_te; }
 150
 151 DecisionManager* QuantifiersEngine::getDecisionManager()
 152 {
 153   return &d_decManager;
 154 }
 155
 156 context::Context* QuantifiersEngine::getSatContext() { return d_context; }
 157
 158 context::UserContext* QuantifiersEngine::getUserContext()
 159 {
 160   return d_userContext;
 161 }
 162
 163 OutputChannel& QuantifiersEngine::getOutputChannel()
 164 {
 165   return d_te->theoryOf(THEORY_QUANTIFIERS)->getOutputChannel();
 166 }
 167 /** get default valuation for the quantifiers engine */
 168 Valuation& QuantifiersEngine::getValuation()
 169 {
 170   return d_te->theoryOf(THEORY_QUANTIFIERS)->getValuation();
 171 }
 172
 173 const LogicInfo& QuantifiersEngine::getLogicInfo() const
 174 {
 175   return d_te->getLogicInfo();
 176 }
 177
 178 EqualityQuery* QuantifiersEngine::getEqualityQuery() const
 179 {
 180   return d_eq_query.get();
 181 }
 182 quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
 183 {
 184   return d_builder.get();
 185 }
 186 quantifiers::QuantEPR* QuantifiersEngine::getQuantEPR() const
 187 {
 188   return d_qepr.get();
 189 }
 190 quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
 191 {
 192   return d_model.get();
 193 }
 194 quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
 195 {
 196   return d_term_db.get();
 197 }
 198 quantifiers::TermDbSygus* QuantifiersEngine::getTermDatabaseSygus() const
 199 {
 200   return d_sygus_tdb.get();
 201 }
 202 quantifiers::TermUtil* QuantifiersEngine::getTermUtil() const
 203 {
 204   return d_term_util.get();
 205 }
 206 expr::TermCanonize* QuantifiersEngine::getTermCanonize() const
 207 {
 208   return d_term_canon.get();
 209 }
 210 quantifiers::QuantAttributes* QuantifiersEngine::getQuantAttributes() const
 211 {
 212   return d_quant_attr.get();
 213 }
 214 quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const
 215 {
 216   return d_instantiate.get();
 217 }
 218 quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const
 219 {
 220   return d_skolemize.get();
 221 }
 222 quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const
 223 {
 224   return d_term_enum.get();
 225 }
 226 inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
 227 {
 228   return d_tr_trie.get();
 229 }
 230
 231 QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
 232   std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q );
 233   if( it==d_owner.end() ){
 234     return NULL;
 235   }else{
 236     return it->second;
 237   }
 238 }
 239
 240 void QuantifiersEngine::setOwner( Node q, QuantifiersModule * m, int priority ) {
 241   QuantifiersModule * mo = getOwner( q );
 242   if( mo!=m ){
 243     if( mo!=NULL ){
 244       if( priority<=d_owner_priority[q] ){
 245         Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << " with higher priority!" << std::endl;
 246         return;
 247       }
 248     }
 249     d_owner[q] = m;
 250     d_owner_priority[q] = priority;
 251   }
 252 }
 253
 254 void QuantifiersEngine::setOwner(Node q, quantifiers::QAttributes& qa)
 255 {
 256   if (qa.d_sygus || (options::sygusRecFun() && !qa.d_fundef_f.isNull()))
 257   {
 258     if (d_qmodules->d_synth_e.get() == nullptr)
 259     {
 260       Trace("quant-warn") << "WARNING : synth engine is null, and we have : "
 261                           << q << std::endl;
 262     }
 263     // set synth engine as owner since this is either a conjecture or a function
 264     // definition to be used by sygus
 265     setOwner(q, d_qmodules->d_synth_e.get(), 2);
 266   }
 267 }
 268
 269 bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
 270   QuantifiersModule * mo = getOwner( q );
 271   return mo==m || mo==NULL;
 272 }
 273
 274 bool QuantifiersEngine::isFiniteBound(Node q, Node v) const
 275 {
 276   quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get();
 277   if (bi && bi->isBound(q, v))
 278   {
 279     return true;
 280   }
 281   TypeNode tn = v.getType();
 282   if (tn.isSort() && options::finiteModelFind())
 283   {
 284     return true;
 285   }
 286   else if (d_term_enum->mayComplete(tn))
 287   {
 288     return true;
 289   }
 290   return false;
 291 }
 292
 293 BoundVarType QuantifiersEngine::getBoundVarType(Node q, Node v) const
 294 {
 295   quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get();
 296   if (bi)
 297   {
 298     return bi->getBoundVarType(q, v);
 299   }
 300   return isFiniteBound(q, v) ? BOUND_FINITE : BOUND_NONE;
 301 }
 302
 303 void QuantifiersEngine::getBoundVarIndices(Node q,
 304                                            std::vector<unsigned>& indices) const
 305 {
 306   Assert(indices.empty());
 307   // we take the bounded variables first
 308   quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get();
 309   if (bi)
 310   {
 311     bi->getBoundVarIndices(q, indices);
 312   }
 313   // then get the remaining ones
 314   for (unsigned i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
 315   {
 316     if (std::find(indices.begin(), indices.end(), i) == indices.end())
 317     {
 318       indices.push_back(i);
 319     }
 320   }
 321 }
 322
 323 bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi,
 324                                          bool initial,
 325                                          Node q,
 326                                          Node v,
 327                                          std::vector<Node>& elements) const
 328 {
 329   quantifiers::BoundedIntegers* bi = d_qmodules->d_bint.get();
 330   if (bi)
 331   {
 332     return bi->getBoundElements(rsi, initial, q, v, elements);
 333   }
 334   return false;
 335 }
 336
 337 void QuantifiersEngine::presolve() {
 338   Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
 339   d_lemmas_waiting.clear();
 340   d_phase_req_waiting.clear();
 341   for( unsigned i=0; i<d_modules.size(); i++ ){
 342     d_modules[i]->presolve();
 343   }
 344   d_term_db->presolve();
 345   d_presolve = false;
 346   //add all terms to database
 347   if( options::incrementalSolving() ){
 348     Trace("quant-engine-proc") << "Add presolve cache " << d_presolve_cache.size() << std::endl;
 349     for( unsigned i=0; i<d_presolve_cache.size(); i++ ){
 350       addTermToDatabase( d_presolve_cache[i], d_presolve_cache_wq[i], d_presolve_cache_wic[i] );
 351     }
 352     Trace("quant-engine-proc") << "Done add presolve cache " << std::endl;
 353   }
 354 }
 355
 356 void QuantifiersEngine::ppNotifyAssertions(
 357     const std::vector<Node>& assertions) {
 358   Trace("quant-engine-proc")
 359       << "ppNotifyAssertions in QE, #assertions = " << assertions.size()
 360       << " check epr = " << (d_qepr != NULL) << std::endl;
 361   if (options::instLevelInputOnly() && options::instMaxLevel() != -1)
 362   {
 363     for (const Node& a : assertions)
 364     {
 365       quantifiers::QuantAttributes::setInstantiationLevelAttr(a, 0);
 366     }
 367   }
 368   if (options::sygus())
 369   {
 370     quantifiers::SynthEngine* sye = d_qmodules->d_synth_e.get();
 371     for (const Node& a : assertions)
 372     {
 373       sye->preregisterAssertion(a);
 374     }
 375   }
 376   /* The SyGuS instantiation module needs a global view of all available
 377    * assertions to collect global terms that get added to each grammar.
 378    */
 379   if (options::sygusInst())
 380   {
 381     quantifiers::SygusInst* si = d_qmodules->d_sygus_inst.get();
 382     si->ppNotifyAssertions(assertions);
 383   }
 384 }
 385
 386 void QuantifiersEngine::check( Theory::Effort e ){
 387   CodeTimer codeTimer(d_statistics.d_time);
 388
 389   if (!getMasterEqualityEngine()->consistent())
 390   {
 391     Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
 392     return;
 393   }
 394   if (d_conflict_c.get())
 395   {
 396     if (e < Theory::EFFORT_LAST_CALL)
 397     {
 398       // this can happen in rare cases when quantifiers is the first to realize
 399       // there is a quantifier-free conflict, for example, when it discovers
 400       // disequal and congruent terms in the master equality engine during
 401       // term indexing. In such cases, quantifiers reports a "conflicting lemma"
 402       // that is, one that is entailed to be false by the current assignment.
 403       // If this lemma is not a SAT conflict, we may get another call to full
 404       // effort check and the quantifier-free solvers still haven't realized
 405       // there is a conflict. In this case, we return, trusting that theory
 406       // combination will do the right thing (split on equalities until there is
 407       // a conflict at the quantifier-free level).
 408       Trace("quant-engine-debug")
 409           << "Conflicting lemma already reported by quantifiers, return."
 410           << std::endl;
 411       return;
 412     }
 413     // we reported what we thought was a conflicting lemma, but now we have
 414     // gotten a check at LAST_CALL effort, indicating that the lemma we reported
 415     // was not conflicting. This should never happen, but in production mode, we
 416     // proceed with the check.
 417     Assert(false);
 418   }
 419   bool needsCheck = !d_lemmas_waiting.empty();
 420   QuantifiersModule::QEffort needsModelE = QuantifiersModule::QEFFORT_NONE;
 421   std::vector< QuantifiersModule* > qm;
 422   if( d_model->checkNeeded() ){
 423     needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL;  //always need to check at or above last call
 424     for (QuantifiersModule*& mdl : d_modules)
 425     {
 426       if (mdl->needsCheck(e))
 427       {
 428         qm.push_back(mdl);
 429         needsCheck = true;
 430         //can only request model at last call since theory combination can find inconsistencies
 431         if( e>=Theory::EFFORT_LAST_CALL ){
 432           QuantifiersModule::QEffort me = mdl->needsModel(e);
 433           needsModelE = me<needsModelE ? me : needsModelE;
 434         }
 435       }
 436     }
 437   }
 438
 439   d_conflict = false;
 440   d_hasAddedLemma = false;
 441   bool setIncomplete = false;
 442
 443   Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl;
 444   if( needsCheck ){
 445     //flush previous lemmas (for instance, if was interrupted), or other lemmas to process
 446     flushLemmas();
 447     if( d_hasAddedLemma ){
 448       return;
 449     }
 450
 451     double clSet = 0;
 452     if( Trace.isOn("quant-engine") ){
 453       clSet = double(clock())/double(CLOCKS_PER_SEC);
 454       Trace("quant-engine") << ">>>>> Quantifiers Engine Round, effort = " << e << " <<<<<" << std::endl;
 455     }
 456
 457     if( Trace.isOn("quant-engine-debug") ){
 458       Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
 459       Trace("quant-engine-debug") << "  depth : " << d_ierCounter_c << std::endl;
 460       Trace("quant-engine-debug") << "  modules to check : ";
 461       for( unsigned i=0; i<qm.size(); i++ ){
 462         Trace("quant-engine-debug") << qm[i]->identify() << " ";
 463       }
 464       Trace("quant-engine-debug") << std::endl;
 465       Trace("quant-engine-debug") << "  # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
 466       if( !d_lemmas_waiting.empty() ){
 467         Trace("quant-engine-debug") << "  lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
 468       }
 469       Trace("quant-engine-debug")
 470           << "  Theory engine finished : " << !theoryEngineNeedsCheck()
 471           << std::endl;
 472       Trace("quant-engine-debug") << "  Needs model effort : " << needsModelE << std::endl;
 473       Trace("quant-engine-debug")
 474           << "  In conflict : " << d_conflict << std::endl;
 475     }
 476     if( Trace.isOn("quant-engine-ee-pre") ){
 477       Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
 478       debugPrintEqualityEngine( "quant-engine-ee-pre" );
 479     }
 480     if( Trace.isOn("quant-engine-assert") ){
 481       Trace("quant-engine-assert") << "Assertions : " << std::endl;
 482       getTheoryEngine()->printAssertions("quant-engine-assert");
 483     }
 484
 485     //reset utilities
 486     Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl;
 487     for (QuantifiersUtil*& util : d_util)
 488     {
 489       Trace("quant-engine-debug2") << "Reset " << util->identify().c_str()
 490                                    << "..." << std::endl;
 491       if (!util->reset(e))
 492       {
 493         flushLemmas();
 494         if( d_hasAddedLemma ){
 495           return;
 496         }else{
 497           //should only fail reset if added a lemma
 498           Assert(false);
 499         }
 500       }
 501     }
 502
 503     if( Trace.isOn("quant-engine-ee") ){
 504       Trace("quant-engine-ee") << "Equality engine : " << std::endl;
 505       debugPrintEqualityEngine( "quant-engine-ee" );
 506     }
 507
 508     //reset the model
 509     Trace("quant-engine-debug") << "Reset model..." << std::endl;
 510     d_model->reset_round();
 511
 512     //reset the modules
 513     Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
 514     for (QuantifiersModule*& mdl : d_modules)
 515     {
 516       Trace("quant-engine-debug2") << "Reset " << mdl->identify().c_str()
 517                                    << std::endl;
 518       mdl->reset_round(e);
 519     }
 520     Trace("quant-engine-debug") << "Done resetting all modules." << std::endl;
 521     //reset may have added lemmas
 522     flushLemmas();
 523     if( d_hasAddedLemma ){
 524       return;
 525     }
 526
 527     if( e==Theory::EFFORT_LAST_CALL ){
 528       ++(d_statistics.d_instantiation_rounds_lc);
 529     }else if( e==Theory::EFFORT_FULL ){
 530       ++(d_statistics.d_instantiation_rounds);
 531     }
 532     Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
 533     for (unsigned qef = QuantifiersModule::QEFFORT_CONFLICT;
 534          qef <= QuantifiersModule::QEFFORT_LAST_CALL;
 535          ++qef)
 536     {
 537       QuantifiersModule::QEffort quant_e =
 538           static_cast<QuantifiersModule::QEffort>(qef);
 539       d_curr_effort_level = quant_e;
 540       // Force the theory engine to build the model if any module requested it.
 541       if (needsModelE == quant_e)
 542       {
 543         Trace("quant-engine-debug") << "Build model..." << std::endl;
 544         if (!d_te->buildModel())
 545         {
 546           // If we failed to build the model, flush all pending lemmas and
 547           // finish.
 548           flushLemmas();
 549           break;
 550         }
 551       }
 552       if( !d_hasAddedLemma ){
 553         //check each module
 554         for (QuantifiersModule*& mdl : qm)
 555         {
 556           Trace("quant-engine-debug") << "Check " << mdl->identify().c_str()
 557                                       << " at effort " << quant_e << "..."
 558                                       << std::endl;
 559           mdl->check(e, quant_e);
 560           if( d_conflict ){
 561             Trace("quant-engine-debug") << "...conflict!" << std::endl;
 562             break;
 563           }
 564         }
 565         //flush all current lemmas
 566         flushLemmas();
 567       }
 568       //if we have added one, stop
 569       if( d_hasAddedLemma ){
 570         break;
 571       }else{
 572         Assert(!d_conflict);
 573         if (quant_e == QuantifiersModule::QEFFORT_CONFLICT)
 574         {
 575           if( e==Theory::EFFORT_FULL ){
 576             //increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase
 577             if( d_ierCounterLastLc!=d_ierCounter_lc || !options::instWhenStrictInterleave() || d_ierCounter%d_inst_when_phase!=0 ){
 578               d_ierCounter = d_ierCounter + 1;
 579               d_ierCounterLastLc = d_ierCounter_lc;
 580               d_ierCounter_c = d_ierCounter_c.get() + 1;
 581             }
 582           }else if( e==Theory::EFFORT_LAST_CALL ){
 583             d_ierCounter_lc = d_ierCounter_lc + 1;
 584           }
 585         }
 586         else if (quant_e == QuantifiersModule::QEFFORT_MODEL)
 587         {
 588           if( e==Theory::EFFORT_LAST_CALL ){
 589             //sources of incompleteness
 590             for (QuantifiersUtil*& util : d_util)
 591             {
 592               if (!util->checkComplete())
 593               {
 594                 Trace("quant-engine-debug") << "Set incomplete because utility "
 595                                             << util->identify().c_str()
 596                                             << " was incomplete." << std::endl;
 597                 setIncomplete = true;
 598               }
 599             }
 600             if (d_conflict_c.get())
 601             {
 602               // we reported a conflicting lemma, should return
 603               setIncomplete = true;
 604             }
 605             //if we have a chance not to set incomplete
 606             if( !setIncomplete ){
 607               //check if we should set the incomplete flag
 608               for (QuantifiersModule*& mdl : d_modules)
 609               {
 610                 if (!mdl->checkComplete())
 611                 {
 612                   Trace("quant-engine-debug")
 613                       << "Set incomplete because module "
 614                       << mdl->identify().c_str() << " was incomplete."
 615                       << std::endl;
 616                   setIncomplete = true;
 617                   break;
 618                 }
 619               }
 620               if( !setIncomplete ){
 621                 //look at individual quantified formulas, one module must claim completeness for each one
 622                 for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
 623                   bool hasCompleteM = false;
 624                   Node q = d_model->getAssertedQuantifier( i );
 625                   QuantifiersModule * qmd = getOwner( q );
 626                   if( qmd!=NULL ){
 627                     hasCompleteM = qmd->checkCompleteFor( q );
 628                   }else{
 629                     for( unsigned j=0; j<d_modules.size(); j++ ){
 630                       if( d_modules[j]->checkCompleteFor( q ) ){
 631                         qmd = d_modules[j];
 632                         hasCompleteM = true;
 633                         break;
 634                       }
 635                     }
 636                   }
 637                   if( !hasCompleteM ){
 638                     Trace("quant-engine-debug") << "Set incomplete because " << q << " was not fully processed." << std::endl;
 639                     setIncomplete = true;
 640                     break;
 641                   }else{
 642                     Assert(qmd != NULL);
 643                     Trace("quant-engine-debug2") << "Complete for " << q << " due to " << qmd->identify().c_str() << std::endl;
 644                   }
 645                 }
 646               }
 647             }
 648             //if setIncomplete = false, we will answer SAT, otherwise we will run at quant_e QEFFORT_LAST_CALL
 649             if( !setIncomplete ){
 650               break;
 651             }
 652           }
 653         }
 654       }
 655     }
 656     d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
 657     Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
 658     // debug print
 659     if (d_hasAddedLemma)
 660     {
 661       bool debugInstTrace = Trace.isOn("inst-per-quant-round");
 662       if (options::debugInst() || debugInstTrace)
 663       {
 664         Options& sopts = smt::currentSmtEngine()->getOptions();
 665         std::ostream& out = *sopts.getOut();
 666         d_instantiate->debugPrint(out);
 667       }
 668     }
 669     if( Trace.isOn("quant-engine") ){
 670       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
 671       Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2-clSet);
 672       Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma;
 673       Trace("quant-engine") << std::endl;
 674     }
 675
 676     Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl;
 677   }else{
 678     Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl;
 679   }
 680
 681   //SAT case
 682   if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
 683     if( setIncomplete ){
 684       Trace("quant-engine") << "Set incomplete flag." << std::endl;
 685       getOutputChannel().setIncomplete();
 686     }
 687     //output debug stats
 688     d_instantiate->debugPrintModel();
 689   }
 690 }
 691
 692 void QuantifiersEngine::notifyCombineTheories() {
 693   //if allowing theory combination to happen at most once between instantiation rounds
 694   //d_ierCounter = 1;
 695   //d_ierCounterLastLc = -1;
 696 }
 697
 698 bool QuantifiersEngine::reduceQuantifier( Node q ) {
 699   //TODO: this can be unified with preregistration: AlphaEquivalence takes ownership of reducable quants
 700   BoolMap::const_iterator it = d_quants_red.find( q );
 701   if( it==d_quants_red.end() ){
 702     Node lem;
 703     std::map< Node, Node >::iterator itr = d_quants_red_lem.find( q );
 704     if( itr==d_quants_red_lem.end() ){
 705       if (d_qmodules->d_alpha_equiv)
 706       {
 707         Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl;
 708         //add equivalence with another quantified formula
 709         lem = d_qmodules->d_alpha_equiv->reduceQuantifier(q);
 710         if( !lem.isNull() ){
 711           Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
 712           ++(d_statistics.d_red_alpha_equiv);
 713         }
 714       }
 715       d_quants_red_lem[q] = lem;
 716     }else{
 717       lem = itr->second;
 718     }
 719     if( !lem.isNull() ){
 720       getOutputChannel().lemma( lem );
 721     }
 722     d_quants_red[q] = !lem.isNull();
 723     return !lem.isNull();
 724   }else{
 725     return (*it).second;
 726   }
 727 }
 728
 729 void QuantifiersEngine::registerQuantifierInternal(Node f)
 730 {
 731   std::map< Node, bool >::iterator it = d_quants.find( f );
 732   if( it==d_quants.end() ){
 733     Trace("quant") << "QuantifiersEngine : Register quantifier ";
 734     Trace("quant") << " : " << f << std::endl;
 735     unsigned prev_lemma_waiting = d_lemmas_waiting.size();
 736     ++(d_statistics.d_num_quant);
 737     Assert(f.getKind() == FORALL);
 738     // register with utilities
 739     for (unsigned i = 0; i < d_util.size(); i++)
 740     {
 741       d_util[i]->registerQuantifier(f);
 742     }
 743     // compute attributes
 744     d_quant_attr->computeAttributes(f);
 745
 746     for (QuantifiersModule*& mdl : d_modules)
 747     {
 748       Trace("quant-debug") << "check ownership with " << mdl->identify()
 749                            << "..." << std::endl;
 750       mdl->checkOwnership(f);
 751     }
 752     QuantifiersModule* qm = getOwner(f);
 753     Trace("quant") << " Owner : " << (qm == nullptr ? "[none]" : qm->identify())
 754                    << std::endl;
 755     // register with each module
 756     for (QuantifiersModule*& mdl : d_modules)
 757     {
 758       Trace("quant-debug") << "register with " << mdl->identify() << "..."
 759                            << std::endl;
 760       mdl->registerQuantifier(f);
 761       // since this is context-independent, we should not add any lemmas during
 762       // this call
 763       Assert(d_lemmas_waiting.size() == prev_lemma_waiting);
 764     }
 765     Trace("quant-debug") << "...finish." << std::endl;
 766     d_quants[f] = true;
 767     AlwaysAssert(d_lemmas_waiting.size() == prev_lemma_waiting);
 768   }
 769 }
 770
 771 void QuantifiersEngine::preRegisterQuantifier(Node q)
 772 {
 773   NodeSet::const_iterator it = d_quants_prereg.find(q);
 774   if (it != d_quants_prereg.end())
 775   {
 776     return;
 777   }
 778   Trace("quant-debug") << "QuantifiersEngine : Pre-register " << q << std::endl;
 779   d_quants_prereg.insert(q);
 780   // try to reduce
 781   if (reduceQuantifier(q))
 782   {
 783     // if we can reduce it, nothing left to do
 784     return;
 785   }
 786   // ensure that it is registered
 787   registerQuantifierInternal(q);
 788   // register with each module
 789   for (QuantifiersModule*& mdl : d_modules)
 790   {
 791     Trace("quant-debug") << "pre-register with " << mdl->identify() << "..."
 792                          << std::endl;
 793     mdl->preRegisterQuantifier(q);
 794   }
 795   // flush the lemmas
 796   flushLemmas();
 797   Trace("quant-debug") << "...finish pre-register " << q << "..." << std::endl;
 798 }
 799
 800 void QuantifiersEngine::registerPattern( std::vector<Node> & pattern) {
 801   for(std::vector<Node>::iterator p = pattern.begin(); p != pattern.end(); ++p){
 802     std::set< Node > added;
 803     getTermDatabase()->addTerm( *p, added );
 804   }
 805 }
 806
 807 void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
 808   if (reduceQuantifier(f))
 809   {
 810     // if we can reduce it, nothing left to do
 811     return;
 812   }
 813   if( !pol ){
 814     // do skolemization
 815     TrustNode lem = d_skolemize->process(f);
 816     if (!lem.isNull())
 817     {
 818       if (Trace.isOn("quantifiers-sk-debug"))
 819       {
 820         Node slem = Rewriter::rewrite(lem.getNode());
 821         Trace("quantifiers-sk-debug")
 822             << "Skolemize lemma : " << slem << std::endl;
 823       }
 824       getOutputChannel().trustedLemma(
 825           lem, LemmaProperty::PREPROCESS | LemmaProperty::NEEDS_JUSTIFY);
 826     }
 827     return;
 828   }
 829   // ensure the quantified formula is registered
 830   registerQuantifierInternal(f);
 831   // assert it to each module
 832   d_model->assertQuantifier(f);
 833   for (QuantifiersModule*& mdl : d_modules)
 834   {
 835     mdl->assertNode(f);
 836   }
 837   addTermToDatabase(d_term_util->getInstConstantBody(f), true);
 838 }
 839
 840 void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
 841   if( options::incrementalSolving() ){
 842     if( d_presolve_in.find( n )==d_presolve_in.end() ){
 843       d_presolve_in.insert( n );
 844       d_presolve_cache.push_back( n );
 845       d_presolve_cache_wq.push_back( withinQuant );
 846       d_presolve_cache_wic.push_back( withinInstClosure );
 847     }
 848   }
 849   //only wait if we are doing incremental solving
 850   if( !d_presolve || !options::incrementalSolving() ){
 851     std::set< Node > added;
 852     d_term_db->addTerm(n, added, withinQuant, withinInstClosure);
 853
 854     if (!withinQuant)
 855     {
 856       if (d_sygus_tdb && options::sygusEvalUnfold())
 857       {
 858         d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n);
 859       }
 860     }
 861   }
 862 }
 863
 864 void QuantifiersEngine::eqNotifyNewClass(TNode t) {
 865   addTermToDatabase( t );
 866 }
 867
 868 bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
 869   if( doCache ){
 870     if( doRewrite ){
 871       lem = Rewriter::rewrite(lem);
 872     }
 873     Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl;
 874     BoolMap::const_iterator itp = d_lemmas_produced_c.find( lem );
 875     if( itp==d_lemmas_produced_c.end() || !(*itp).second ){
 876       d_lemmas_produced_c[ lem ] = true;
 877       d_lemmas_waiting.push_back( lem );
 878       Trace("inst-add-debug") << "Added lemma" << std::endl;
 879       return true;
 880     }else{
 881       Trace("inst-add-debug") << "Duplicate." << std::endl;
 882       return false;
 883     }
 884   }else{
 885     //do not need to rewrite, will be rewritten after sending
 886     d_lemmas_waiting.push_back( lem );
 887     return true;
 888   }
 889 }
 890
 891 bool QuantifiersEngine::addTrustedLemma(TrustNode tlem,
 892                                         bool doCache,
 893                                         bool doRewrite)
 894 {
 895   Node lem = tlem.getProven();
 896   if (!addLemma(lem, doCache, doRewrite))
 897   {
 898     return false;
 899   }
 900   d_lemmasWaitingPg[lem] = tlem.getGenerator();
 901   return true;
 902 }
 903
 904 bool QuantifiersEngine::removeLemma( Node lem ) {
 905   std::vector< Node >::iterator it = std::find( d_lemmas_waiting.begin(), d_lemmas_waiting.end(), lem );
 906   if( it!=d_lemmas_waiting.end() ){
 907     d_lemmas_waiting.erase( it, it + 1 );
 908     d_lemmas_produced_c[ lem ] = false;
 909     return true;
 910   }else{
 911     return false;
 912   }
 913 }
 914
 915 void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
 916   d_phase_req_waiting[lit] = req;
 917 }
 918
 919 void QuantifiersEngine::markRelevant( Node q ) {
 920   d_model->markRelevant( q );
 921 }
 922 bool QuantifiersEngine::hasAddedLemma() const
 923 {
 924   return !d_lemmas_waiting.empty() || d_hasAddedLemma;
 925 }
 926 bool QuantifiersEngine::theoryEngineNeedsCheck() const
 927 {
 928   return d_te->needCheck();
 929 }
 930
 931 void QuantifiersEngine::setConflict()
 932 {
 933   d_conflict = true;
 934   d_conflict_c = true;
 935 }
 936
 937 bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
 938   Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
 939   //determine if we should perform check, based on instWhenMode
 940   bool performCheck = false;
 941   if (options::instWhenMode() == options::InstWhenMode::FULL)
 942   {
 943     performCheck = ( e >= Theory::EFFORT_FULL );
 944   }
 945   else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY)
 946   {
 947     performCheck = (e >= Theory::EFFORT_FULL) && !theoryEngineNeedsCheck();
 948   }
 949   else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL)
 950   {
 951     performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
 952   }
 953   else if (options::instWhenMode()
 954            == options::InstWhenMode::FULL_DELAY_LAST_CALL)
 955   {
 956     performCheck = ((e == Theory::EFFORT_FULL && !theoryEngineNeedsCheck()
 957                      && d_ierCounter % d_inst_when_phase != 0)
 958                     || e == Theory::EFFORT_LAST_CALL);
 959   }
 960   else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL)
 961   {
 962     performCheck = ( e >= Theory::EFFORT_LAST_CALL );
 963   }
 964   else
 965   {
 966     performCheck = true;
 967   }
 968   return performCheck;
 969 }
 970
 971 options::UserPatMode QuantifiersEngine::getInstUserPatMode()
 972 {
 973   if (options::userPatternsQuant() == options::UserPatMode::INTERLEAVE)
 974   {
 975     return d_ierCounter % 2 == 0 ? options::UserPatMode::USE
 976                                  : options::UserPatMode::RESORT;
 977   }
 978   else
 979   {
 980     return options::userPatternsQuant();
 981   }
 982 }
 983
 984 void QuantifiersEngine::flushLemmas(){
 985   OutputChannel& out = getOutputChannel();
 986   if( !d_lemmas_waiting.empty() ){
 987     //take default output channel if none is provided
 988     d_hasAddedLemma = true;
 989     std::map<Node, ProofGenerator*>::iterator itp;
 990     // Note: Do not use foreach loop here and do not cache size() call.
 991     // New lemmas can be added while iterating over d_lemmas_waiting.
 992     for (size_t i = 0; i < d_lemmas_waiting.size(); ++i)
 993     {
 994       const Node& lemw = d_lemmas_waiting[i];
 995       Trace("qe-lemma") << "Lemma : " << lemw << std::endl;
 996       itp = d_lemmasWaitingPg.find(lemw);
 997       if (itp != d_lemmasWaitingPg.end())
 998       {
 999         TrustNode tlemw = TrustNode::mkTrustLemma(lemw, itp->second);
1000         out.trustedLemma(tlemw, LemmaProperty::PREPROCESS);
1001       }
1002       else
1003       {
1004         out.lemma(lemw, LemmaProperty::PREPROCESS);
1005       }
1006     }
1007     d_lemmas_waiting.clear();
1008   }
1009   if( !d_phase_req_waiting.empty() ){
1010     for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){
1011       Trace("qe-lemma") << "Require phase : " << it->first << " -> " << it->second << std::endl;
1012       out.requirePhase(it->first, it->second);
1013     }
1014     d_phase_req_waiting.clear();
1015   }
1016 }
1017
1018 void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
1019   d_instantiate->getInstantiationTermVectors(q, tvecs);
1020 }
1021
1022 void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
1023   d_instantiate->getInstantiationTermVectors(insts);
1024 }
1025
1026 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
1027   bool printed = false;
1028   // print the skolemizations
1029   if (options::printInstMode() == options::PrintInstMode::LIST)
1030   {
1031     if (d_skolemize->printSkolemization(out))
1032     {
1033       printed = true;
1034     }
1035   }
1036   // print the instantiations
1037   if (d_instantiate->printInstantiations(out))
1038   {
1039     printed = true;
1040   }
1041   if( !printed ){
1042     out << "No instantiations" << std::endl;
1043   }
1044 }
1045
1046 void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
1047   if (d_qmodules->d_synth_e)
1048   {
1049     d_qmodules->d_synth_e->printSynthSolution(out);
1050   }else{
1051     out << "Internal error : module for synth solution not found." << std::endl;
1052   }
1053 }
1054
1055 void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
1056   d_instantiate->getInstantiatedQuantifiedFormulas(qs);
1057 }
1058
1059 QuantifiersEngine::Statistics::Statistics()
1060     : d_time("theory::QuantifiersEngine::time"),
1061       d_qcf_time("theory::QuantifiersEngine::time_qcf"),
1062       d_ematching_time("theory::QuantifiersEngine::time_ematching"),
1063       d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
1064       d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
1065       d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
1066       d_triggers("QuantifiersEngine::Triggers", 0),
1067       d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
1068       d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
1069       d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
1070       d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0),
1071       d_instantiations_user_patterns("QuantifiersEngine::Instantiations_User_Patterns", 0),
1072       d_instantiations_auto_gen("QuantifiersEngine::Instantiations_Auto_Gen", 0),
1073       d_instantiations_guess("QuantifiersEngine::Instantiations_Guess", 0),
1074       d_instantiations_qcf("QuantifiersEngine::Instantiations_Qcf_Conflict", 0),
1075       d_instantiations_qcf_prop("QuantifiersEngine::Instantiations_Qcf_Prop", 0),
1076       d_instantiations_fmf_exh("QuantifiersEngine::Instantiations_Fmf_Exh", 0),
1077       d_instantiations_fmf_mbqi("QuantifiersEngine::Instantiations_Fmf_Mbqi", 0),
1078       d_instantiations_cbqi("QuantifiersEngine::Instantiations_Cbqi", 0),
1079       d_instantiations_rr("QuantifiersEngine::Instantiations_Rewrite_Rules", 0)
1080 {
1081   smtStatisticsRegistry()->registerStat(&d_time);
1082   smtStatisticsRegistry()->registerStat(&d_qcf_time);
1083   smtStatisticsRegistry()->registerStat(&d_ematching_time);
1084   smtStatisticsRegistry()->registerStat(&d_num_quant);
1085   smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
1086   smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
1087   smtStatisticsRegistry()->registerStat(&d_triggers);
1088   smtStatisticsRegistry()->registerStat(&d_simple_triggers);
1089   smtStatisticsRegistry()->registerStat(&d_multi_triggers);
1090   smtStatisticsRegistry()->registerStat(&d_multi_trigger_instantiations);
1091   smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
1092   smtStatisticsRegistry()->registerStat(&d_instantiations_user_patterns);
1093   smtStatisticsRegistry()->registerStat(&d_instantiations_auto_gen);
1094   smtStatisticsRegistry()->registerStat(&d_instantiations_guess);
1095   smtStatisticsRegistry()->registerStat(&d_instantiations_qcf);
1096   smtStatisticsRegistry()->registerStat(&d_instantiations_qcf_prop);
1097   smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_exh);
1098   smtStatisticsRegistry()->registerStat(&d_instantiations_fmf_mbqi);
1099   smtStatisticsRegistry()->registerStat(&d_instantiations_cbqi);
1100   smtStatisticsRegistry()->registerStat(&d_instantiations_rr);
1101 }
1102
1103 QuantifiersEngine::Statistics::~Statistics(){
1104   smtStatisticsRegistry()->unregisterStat(&d_time);
1105   smtStatisticsRegistry()->unregisterStat(&d_qcf_time);
1106   smtStatisticsRegistry()->unregisterStat(&d_ematching_time);
1107   smtStatisticsRegistry()->unregisterStat(&d_num_quant);
1108   smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
1109   smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
1110   smtStatisticsRegistry()->unregisterStat(&d_triggers);
1111   smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
1112   smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
1113   smtStatisticsRegistry()->unregisterStat(&d_multi_trigger_instantiations);
1114   smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
1115   smtStatisticsRegistry()->unregisterStat(&d_instantiations_user_patterns);
1116   smtStatisticsRegistry()->unregisterStat(&d_instantiations_auto_gen);
1117   smtStatisticsRegistry()->unregisterStat(&d_instantiations_guess);
1118   smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf);
1119   smtStatisticsRegistry()->unregisterStat(&d_instantiations_qcf_prop);
1120   smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_exh);
1121   smtStatisticsRegistry()->unregisterStat(&d_instantiations_fmf_mbqi);
1122   smtStatisticsRegistry()->unregisterStat(&d_instantiations_cbqi);
1123   smtStatisticsRegistry()->unregisterStat(&d_instantiations_rr);
1124 }
1125
1126 eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine() const
1127 {
1128   return d_masterEqualityEngine;
1129 }
1130
1131 Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
1132   return d_eq_query->getInternalRepresentative(a, q, index);
1133 }
1134
1135 bool QuantifiersEngine::getSynthSolutions(
1136     std::map<Node, std::map<Node, Node> >& sol_map)
1137 {
1138   return d_qmodules->d_synth_e->getSynthSolutions(sol_map);
1139 }
1140
1141 void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
1142   eq::EqualityEngine* ee = getMasterEqualityEngine();
1143   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
1144   std::map< TypeNode, int > typ_num;
1145   while( !eqcs_i.isFinished() ){
1146     TNode r = (*eqcs_i);
1147     TypeNode tr = r.getType();
1148     if( typ_num.find( tr )==typ_num.end() ){
1149       typ_num[tr] = 0;
1150     }
1151     typ_num[tr]++;
1152     bool firstTime = true;
1153     Trace(c) << "  " << r;
1154     Trace(c) << " : { ";
1155     eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
1156     while( !eqc_i.isFinished() ){
1157       TNode n = (*eqc_i);
1158       if( r!=n ){
1159         if( firstTime ){
1160           Trace(c) << std::endl;
1161           firstTime = false;
1162         }
1163         Trace(c) << "    " << n << std::endl;
1164       }
1165       ++eqc_i;
1166     }
1167     if( !firstTime ){ Trace(c) << "  "; }
1168     Trace(c) << "}" << std::endl;
1169     ++eqcs_i;
1170   }
1171   Trace(c) << std::endl;
1172   for( std::map< TypeNode, int >::iterator it = typ_num.begin(); it != typ_num.end(); ++it ){
1173     Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl;
1174   }
1175 }
1176
1177 }  // namespace theory
1178 }  // namespace CVC4