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