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