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