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