src/theory/theory_engine.cpp

   1 /*********************                                                        */
   2 /*! \file theory_engine.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
   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 The theory engine
  13  **
  14  ** The theory engine.
  15  **/
  16
  17 #include "theory/theory_engine.h"
  18
  19 #include <list>
  20 #include <vector>
  21
  22 #include "base/map_util.h"
  23 #include "decision/decision_engine.h"
  24 #include "expr/attribute.h"
  25 #include "expr/node.h"
  26 #include "expr/node_algorithm.h"
  27 #include "expr/node_builder.h"
  28 #include "expr/node_visitor.h"
  29 #include "options/bv_options.h"
  30 #include "options/options.h"
  31 #include "options/quantifiers_options.h"
  32 #include "options/theory_options.h"
  33 #include "preprocessing/assertion_pipeline.h"
  34 #include "printer/printer.h"
  35 #include "smt/dump.h"
  36 #include "smt/logic_exception.h"
  37 #include "smt/term_formula_removal.h"
  38 #include "theory/arith/arith_ite_utils.h"
  39 #include "theory/bv/theory_bv_utils.h"
  40 #include "theory/care_graph.h"
  41 #include "theory/combination_care_graph.h"
  42 #include "theory/decision_manager.h"
  43 #include "theory/quantifiers/first_order_model.h"
  44 #include "theory/quantifiers/fmf/model_engine.h"
  45 #include "theory/quantifiers/theory_quantifiers.h"
  46 #include "theory/quantifiers_engine.h"
  47 #include "theory/relevance_manager.h"
  48 #include "theory/rewriter.h"
  49 #include "theory/theory.h"
  50 #include "theory/theory_engine_proof_generator.h"
  51 #include "theory/theory_id.h"
  52 #include "theory/theory_model.h"
  53 #include "theory/theory_traits.h"
  54 #include "theory/uf/equality_engine.h"
  55 #include "util/resource_manager.h"
  56
  57 using namespace std;
  58
  59 using namespace CVC4::preprocessing;
  60 using namespace CVC4::theory;
  61
  62 namespace CVC4 {
  63
  64 /* -------------------------------------------------------------------------- */
  65
  66 namespace theory {
  67
  68 /**
  69  * IMPORTANT: The order of the theories is important. For example, strings
  70  *            depends on arith, quantifiers needs to come as the very last.
  71  *            Do not change this order.
  72  */
  73
  74 #define CVC4_FOR_EACH_THEORY                                     \
  75   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BUILTIN)   \
  76   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BOOL)      \
  77   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_UF)        \
  78   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_ARITH)     \
  79   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BV)        \
  80   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_FP)        \
  81   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_ARRAYS)    \
  82   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_DATATYPES) \
  83   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SEP)       \
  84   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SETS)      \
  85   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BAGS)      \
  86   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_STRINGS)   \
  87   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_QUANTIFIERS)
  88
  89 }  // namespace theory
  90
  91 /* -------------------------------------------------------------------------- */
  92
  93 inline void flattenAnd(Node n, std::vector<TNode>& out){
  94   Assert(n.getKind() == kind::AND);
  95   for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){
  96     Node curr = *i;
  97     if(curr.getKind() == kind::AND){
  98       flattenAnd(curr, out);
  99     }else{
 100       out.push_back(curr);
 101     }
 102   }
 103 }
 104
 105 inline Node flattenAnd(Node n){
 106   std::vector<TNode> out;
 107   flattenAnd(n, out);
 108   return NodeManager::currentNM()->mkNode(kind::AND, out);
 109 }
 110
 111 /**
 112  * Compute the string for a given theory id. In this module, we use
 113  * THEORY_SAT_SOLVER as an id, which is not a normal id but maps to
 114  * THEORY_LAST. Thus, we need our own string conversion here.
 115  *
 116  * @param id The theory id
 117  * @return The string corresponding to the theory id
 118  */
 119 std::string getTheoryString(theory::TheoryId id)
 120 {
 121   if (id == theory::THEORY_SAT_SOLVER)
 122   {
 123     return "THEORY_SAT_SOLVER";
 124   }
 125   else
 126   {
 127     std::stringstream ss;
 128     ss << id;
 129     return ss.str();
 130   }
 131 }
 132
 133 void TheoryEngine::finishInit() {
 134   // NOTE: This seems to be required since
 135   // theory::TheoryTraits<THEORY>::isParametric cannot be accessed without
 136   // using the CVC4_FOR_EACH_THEORY_STATEMENT macro. -AJR
 137   std::vector<theory::Theory*> paraTheories;
 138 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 139 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 140 #endif
 141 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY)   \
 142   if (theory::TheoryTraits<THEORY>::isParametric \
 143       && d_logicInfo.isTheoryEnabled(THEORY))    \
 144   {                                              \
 145     paraTheories.push_back(theoryOf(THEORY));    \
 146   }
 147   // Collect the parametric theories, which are given to the theory combination
 148   // manager below
 149   CVC4_FOR_EACH_THEORY;
 150
 151   // Initialize the theory combination architecture
 152   if (options::tcMode() == options::TcMode::CARE_GRAPH)
 153   {
 154     d_tc.reset(new CombinationCareGraph(*this, paraTheories, d_pnm));
 155   }
 156   else
 157   {
 158     Unimplemented() << "TheoryEngine::finishInit: theory combination mode "
 159                     << options::tcMode() << " not supported";
 160   }
 161   // create the relevance filter if any option requires it
 162   if (options::relevanceFilter())
 163   {
 164     d_relManager.reset(
 165         new RelevanceManager(d_userContext, theory::Valuation(this)));
 166   }
 167
 168   // initialize the quantifiers engine
 169   if (d_logicInfo.isQuantified())
 170   {
 171     // initialize the quantifiers engine
 172     d_quantEngine = new QuantifiersEngine(this, *d_decManager.get(), d_pnm);
 173   }
 174   // initialize the theory combination manager, which decides and allocates the
 175   // equality engines to use for all theories.
 176   d_tc->finishInit();
 177
 178   // set the core equality engine on quantifiers engine
 179   if (d_logicInfo.isQuantified())
 180   {
 181     d_quantEngine->setMasterEqualityEngine(d_tc->getCoreEqualityEngine());
 182   }
 183
 184   // finish initializing the theories by linking them with the appropriate
 185   // utilities and then calling their finishInit method.
 186   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
 187     Theory* t = d_theoryTable[theoryId];
 188     if (t == nullptr)
 189     {
 190       continue;
 191     }
 192     // setup the pointers to the utilities
 193     const EeTheoryInfo* eeti = d_tc->getEeTheoryInfo(theoryId);
 194     Assert(eeti != nullptr);
 195     // the theory's official equality engine is the one specified by the
 196     // equality engine manager
 197     t->setEqualityEngine(eeti->d_usedEe);
 198     // set the quantifiers engine
 199     t->setQuantifiersEngine(d_quantEngine);
 200     // set the decision manager for the theory
 201     t->setDecisionManager(d_decManager.get());
 202     // finish initializing the theory
 203     t->finishInit();
 204   }
 205
 206   // finish initializing the quantifiers engine
 207   if (d_logicInfo.isQuantified())
 208   {
 209     d_quantEngine->finishInit();
 210   }
 211 }
 212
 213 TheoryEngine::TheoryEngine(context::Context* context,
 214                            context::UserContext* userContext,
 215                            ResourceManager* rm,
 216                            RemoveTermFormulas& iteRemover,
 217                            const LogicInfo& logicInfo,
 218                            OutputManager& outMgr)
 219     : d_propEngine(nullptr),
 220       d_context(context),
 221       d_userContext(userContext),
 222       d_logicInfo(logicInfo),
 223       d_outMgr(outMgr),
 224       d_pnm(nullptr),
 225       d_lazyProof(
 226           d_pnm != nullptr ? new LazyCDProof(
 227               d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof")
 228                            : nullptr),
 229       d_tepg(new TheoryEngineProofGenerator(d_pnm, d_userContext)),
 230       d_sharedTerms(this, context),
 231       d_tc(nullptr),
 232       d_quantEngine(nullptr),
 233       d_decManager(new DecisionManager(userContext)),
 234       d_relManager(nullptr),
 235       d_preRegistrationVisitor(this, context),
 236       d_sharedTermsVisitor(d_sharedTerms),
 237       d_eager_model_building(false),
 238       d_inConflict(context, false),
 239       d_inSatMode(false),
 240       d_hasShutDown(false),
 241       d_incomplete(context, false),
 242       d_propagationMap(context),
 243       d_propagationMapTimestamp(context, 0),
 244       d_propagatedLiterals(context),
 245       d_propagatedLiteralsIndex(context, 0),
 246       d_atomRequests(context),
 247       d_tpp(*this, iteRemover),
 248       d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
 249       d_true(),
 250       d_false(),
 251       d_interrupted(false),
 252       d_resourceManager(rm),
 253       d_inPreregister(false),
 254       d_factsAsserted(context, false),
 255       d_attr_handle(),
 256       d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
 257 {
 258   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST;
 259       ++ theoryId)
 260   {
 261     d_theoryTable[theoryId] = NULL;
 262     d_theoryOut[theoryId] = NULL;
 263   }
 264
 265   smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime);
 266   d_true = NodeManager::currentNM()->mkConst<bool>(true);
 267   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 268
 269   smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded);
 270 }
 271
 272 TheoryEngine::~TheoryEngine() {
 273   Assert(d_hasShutDown);
 274
 275   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
 276     if(d_theoryTable[theoryId] != NULL) {
 277       delete d_theoryTable[theoryId];
 278       delete d_theoryOut[theoryId];
 279     }
 280   }
 281
 282   delete d_quantEngine;
 283
 284   smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
 285   smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
 286 }
 287
 288 void TheoryEngine::interrupt() { d_interrupted = true; }
 289 void TheoryEngine::preRegister(TNode preprocessed) {
 290   Debug("theory") << "TheoryEngine::preRegister( " << preprocessed << ")"
 291                   << std::endl;
 292   d_preregisterQueue.push(preprocessed);
 293
 294   if (!d_inPreregister) {
 295     // We're in pre-register
 296     d_inPreregister = true;
 297
 298     // Process the pre-registration queue
 299     while (!d_preregisterQueue.empty()) {
 300       // Get the next atom to pre-register
 301       preprocessed = d_preregisterQueue.front();
 302       d_preregisterQueue.pop();
 303
 304       if (d_logicInfo.isSharingEnabled() && preprocessed.getKind() == kind::EQUAL) {
 305         // When sharing is enabled, we propagate from the shared terms manager also
 306         d_sharedTerms.addEqualityToPropagate(preprocessed);
 307       }
 308
 309       // the atom should not have free variables
 310       Debug("theory") << "TheoryEngine::preRegister: " << preprocessed
 311                       << std::endl;
 312       Assert(!expr::hasFreeVar(preprocessed));
 313
 314       // Pre-register the terms in the atom
 315       theory::TheoryIdSet theories = NodeVisitor<PreRegisterVisitor>::run(
 316           d_preRegistrationVisitor, preprocessed);
 317       theories = TheoryIdSetUtil::setRemove(THEORY_BOOL, theories);
 318       // Remove the top theory, if any more that means multiple theories were
 319       // involved
 320       bool multipleTheories =
 321           TheoryIdSetUtil::setRemove(Theory::theoryOf(preprocessed), theories);
 322       if (Configuration::isAssertionBuild())
 323       {
 324         TheoryId i;
 325         // This should never throw an exception, since theories should be
 326         // guaranteed to be initialized.
 327         // These checks don't work with finite model finding, because it
 328         // uses Rational constants to represent cardinality constraints,
 329         // even though arithmetic isn't actually involved.
 330         if (!options::finiteModelFind())
 331         {
 332           while ((i = TheoryIdSetUtil::setPop(theories)) != THEORY_LAST)
 333           {
 334             if (!d_logicInfo.isTheoryEnabled(i))
 335             {
 336               LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy();
 337               newLogicInfo.enableTheory(i);
 338               newLogicInfo.lock();
 339               std::stringstream ss;
 340               ss << "The logic was specified as " << d_logicInfo.getLogicString()
 341                 << ", which doesn't include " << i
 342                 << ", but found a term in that theory." << std::endl
 343                 << "You might want to extend your logic to "
 344                 << newLogicInfo.getLogicString() << std::endl;
 345               throw LogicException(ss.str());
 346             }
 347           }
 348         }
 349       }
 350       if (multipleTheories) {
 351         // Collect the shared terms if there are multiple theories
 352         NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor,
 353                                              preprocessed);
 354       }
 355     }
 356
 357     // Leaving pre-register
 358     d_inPreregister = false;
 359   }
 360 }
 361
 362 void TheoryEngine::printAssertions(const char* tag) {
 363   if (Trace.isOn(tag)) {
 364
 365     for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
 366       Theory* theory = d_theoryTable[theoryId];
 367       if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
 368         Trace(tag) << "--------------------------------------------" << endl;
 369         Trace(tag) << "Assertions of " << theory->getId() << ": " << endl;
 370         {
 371           context::CDList<Assertion>::const_iterator it = theory->facts_begin(),
 372                                                      it_end =
 373                                                          theory->facts_end();
 374           for (unsigned i = 0; it != it_end; ++it, ++i)
 375           {
 376             if ((*it).d_isPreregistered)
 377             {
 378               Trace(tag) << "[" << i << "]: ";
 379             }
 380             else
 381             {
 382               Trace(tag) << "(" << i << "): ";
 383             }
 384             Trace(tag) << (*it).d_assertion << endl;
 385           }
 386         }
 387
 388         if (d_logicInfo.isSharingEnabled()) {
 389           Trace(tag) << "Shared terms of " << theory->getId() << ": " << endl;
 390           context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
 391           for (unsigned i = 0; it != it_end; ++ it, ++i) {
 392               Trace(tag) << "[" << i << "]: " << (*it) << endl;
 393           }
 394         }
 395       }
 396     }
 397   }
 398 }
 399
 400 void TheoryEngine::dumpAssertions(const char* tag) {
 401   if (Dump.isOn(tag)) {
 402     const Printer& printer = d_outMgr.getPrinter();
 403     std::ostream& out = d_outMgr.getDumpOut();
 404     printer.toStreamCmdComment(out, "Starting completeness check");
 405     for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
 406       Theory* theory = d_theoryTable[theoryId];
 407       if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
 408         printer.toStreamCmdComment(out, "Completeness check");
 409         printer.toStreamCmdPush(out);
 410
 411         // Dump the shared terms
 412         if (d_logicInfo.isSharingEnabled()) {
 413           printer.toStreamCmdComment(out, "Shared terms");
 414           context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
 415           for (unsigned i = 0; it != it_end; ++ it, ++i) {
 416               stringstream ss;
 417               ss << (*it);
 418               printer.toStreamCmdComment(out, ss.str());
 419           }
 420         }
 421
 422         // Dump the assertions
 423         printer.toStreamCmdComment(out, "Assertions");
 424         context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
 425         for (; it != it_end; ++ it) {
 426           // Get the assertion
 427           Node assertionNode = (*it).d_assertion;
 428           // Purify all the terms
 429
 430           if ((*it).d_isPreregistered)
 431           {
 432             printer.toStreamCmdComment(out, "Preregistered");
 433           }
 434           else
 435           {
 436             printer.toStreamCmdComment(out, "Shared assertion");
 437           }
 438           printer.toStreamCmdAssert(out, assertionNode);
 439         }
 440         printer.toStreamCmdCheckSat(out);
 441
 442         printer.toStreamCmdPop(out);
 443       }
 444     }
 445   }
 446 }
 447
 448 /**
 449  * Check all (currently-active) theories for conflicts.
 450  * @param effort the effort level to use
 451  */
 452 void TheoryEngine::check(Theory::Effort effort) {
 453   // spendResource();
 454
 455   // Reset the interrupt flag
 456   d_interrupted = false;
 457
 458 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 459 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 460 #endif
 461 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY)                      \
 462   if (theory::TheoryTraits<THEORY>::hasCheck                        \
 463       && d_logicInfo.isTheoryEnabled(THEORY))                       \
 464   {                                                                 \
 465     theoryOf(THEORY)->check(effort);                                \
 466     if (d_inConflict)                                               \
 467     {                                                               \
 468       Debug("conflict") << THEORY << " in conflict. " << std::endl; \
 469       break;                                                        \
 470     }                                                               \
 471   }
 472
 473   // Do the checking
 474   try {
 475
 476     // Mark the output channel unused (if this is FULL_EFFORT, and nothing
 477     // is done by the theories, no additional check will be needed)
 478     d_outputChannelUsed = false;
 479
 480     // Mark the lemmas flag (no lemmas added)
 481     d_lemmasAdded = false;
 482
 483     Debug("theory") << "TheoryEngine::check(" << effort << "): d_factsAsserted = " << (d_factsAsserted ? "true" : "false") << endl;
 484
 485     // If in full effort, we have a fake new assertion just to jumpstart the checking
 486     if (Theory::fullEffort(effort)) {
 487       d_factsAsserted = true;
 488       // Reset round for the relevance manager, which notice only sets a flag
 489       // to indicate that its information must be recomputed.
 490       if (d_relManager != nullptr)
 491       {
 492         d_relManager->resetRound();
 493       }
 494       d_tc->resetRound();
 495     }
 496
 497     // Check until done
 498     while (d_factsAsserted && !d_inConflict && !d_lemmasAdded) {
 499
 500       Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << endl;
 501
 502       Trace("theory::assertions") << endl;
 503       if (Trace.isOn("theory::assertions")) {
 504         printAssertions("theory::assertions");
 505       }
 506
 507       if(Theory::fullEffort(effort)) {
 508         Trace("theory::assertions::fulleffort") << endl;
 509         if (Trace.isOn("theory::assertions::fulleffort")) {
 510           printAssertions("theory::assertions::fulleffort");
 511         }
 512       }
 513
 514       // Note that we've discharged all the facts
 515       d_factsAsserted = false;
 516
 517       // Do the checking
 518       CVC4_FOR_EACH_THEORY;
 519
 520       Debug("theory") << "TheoryEngine::check(" << effort << "): running propagation after the initial check" << endl;
 521
 522       // We are still satisfiable, propagate as much as possible
 523       propagate(effort);
 524
 525       // We do combination if all has been processed and we are in fullcheck
 526       if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() && !d_factsAsserted && !d_lemmasAdded && !d_inConflict) {
 527         // Do the combination
 528         Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << endl;
 529         {
 530           TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime);
 531           d_tc->combineTheories();
 532         }
 533         if(d_logicInfo.isQuantified()){
 534           d_quantEngine->notifyCombineTheories();
 535         }
 536       }
 537     }
 538
 539     // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
 540     if( Theory::fullEffort(effort) && ! d_inConflict && ! needCheck() ) {
 541       Trace("theory::assertions-model") << endl;
 542       if (Trace.isOn("theory::assertions-model")) {
 543         printAssertions("theory::assertions-model");
 544       }
 545       // reset the model in the combination engine
 546       d_tc->resetModel();
 547       //checks for theories requiring the model go at last call
 548       for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
 549         if( theoryId!=THEORY_QUANTIFIERS ){
 550           Theory* theory = d_theoryTable[theoryId];
 551           if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
 552             if( theory->needsCheckLastEffort() ){
 553               if (!d_tc->buildModel())
 554               {
 555                 break;
 556               }
 557               theory->check(Theory::EFFORT_LAST_CALL);
 558             }
 559           }
 560         }
 561       }
 562       if (!d_inConflict)
 563       {
 564         if(d_logicInfo.isQuantified()) {
 565           // quantifiers engine must check at last call effort
 566           d_quantEngine->check(Theory::EFFORT_LAST_CALL);
 567         }
 568       }
 569       if (!d_inConflict && !needCheck())
 570       {
 571         // If d_eager_model_building is false, then we only mark that we
 572         // are in "SAT mode". We build the model later only if the user asks
 573         // for it via getBuiltModel.
 574         d_inSatMode = true;
 575         if (d_eager_model_building)
 576         {
 577           d_tc->buildModel();
 578         }
 579       }
 580     }
 581
 582     Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas");
 583     Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl;
 584
 585     if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) {
 586       // Do post-processing of model from the theories (e.g. used for THEORY_SEP
 587       // to construct heap model)
 588       d_tc->postProcessModel(d_incomplete.get());
 589     }
 590   } catch(const theory::Interrupted&) {
 591     Trace("theory") << "TheoryEngine::check() => interrupted" << endl;
 592   }
 593   // If fulleffort, check all theories
 594   if(Dump.isOn("theory::fullcheck") && Theory::fullEffort(effort)) {
 595     if (!d_inConflict && !needCheck()) {
 596       dumpAssertions("theory::fullcheck");
 597     }
 598   }
 599 }
 600
 601 void TheoryEngine::propagate(Theory::Effort effort)
 602 {
 603   // Reset the interrupt flag
 604   d_interrupted = false;
 605
 606   // Definition of the statement that is to be run by every theory
 607 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 608 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 609 #endif
 610 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 611   if (theory::TheoryTraits<THEORY>::hasPropagate && d_logicInfo.isTheoryEnabled(THEORY)) { \
 612     theoryOf(THEORY)->propagate(effort); \
 613   }
 614
 615   // Reset the interrupt flag
 616   d_interrupted = false;
 617
 618   // Propagate for each theory using the statement above
 619   CVC4_FOR_EACH_THEORY;
 620 }
 621
 622 Node TheoryEngine::getNextDecisionRequest()
 623 {
 624   return d_decManager->getNextDecisionRequest();
 625 }
 626
 627 bool TheoryEngine::properConflict(TNode conflict) const {
 628   bool value;
 629   if (conflict.getKind() == kind::AND) {
 630     for (unsigned i = 0; i < conflict.getNumChildren(); ++ i) {
 631       if (! getPropEngine()->hasValue(conflict[i], value)) {
 632         Debug("properConflict") << "Bad conflict is due to unassigned atom: "
 633                                 << conflict[i] << endl;
 634         return false;
 635       }
 636       if (! value) {
 637         Debug("properConflict") << "Bad conflict is due to false atom: "
 638                                 << conflict[i] << endl;
 639         return false;
 640       }
 641       if (conflict[i] != Rewriter::rewrite(conflict[i])) {
 642         Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
 643                                 << conflict[i] << " vs " << Rewriter::rewrite(conflict[i]) << endl;
 644         return false;
 645       }
 646     }
 647   } else {
 648     if (! getPropEngine()->hasValue(conflict, value)) {
 649       Debug("properConflict") << "Bad conflict is due to unassigned atom: "
 650                               << conflict << endl;
 651       return false;
 652     }
 653     if(! value) {
 654       Debug("properConflict") << "Bad conflict is due to false atom: "
 655                               << conflict << endl;
 656       return false;
 657     }
 658     if (conflict != Rewriter::rewrite(conflict)) {
 659       Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
 660                               << conflict << " vs " << Rewriter::rewrite(conflict) << endl;
 661       return false;
 662     }
 663   }
 664   return true;
 665 }
 666
 667 TheoryModel* TheoryEngine::getModel()
 668 {
 669   Assert(d_tc != nullptr);
 670   TheoryModel* m = d_tc->getModel();
 671   Assert(m != nullptr);
 672   return m;
 673 }
 674
 675 TheoryModel* TheoryEngine::getBuiltModel()
 676 {
 677   Assert(d_tc != nullptr);
 678   // If this method was called, we should be in SAT mode, and produceModels
 679   // should be true.
 680   AlwaysAssert(options::produceModels());
 681   if (!d_inSatMode)
 682   {
 683     // not available, perhaps due to interuption.
 684     return nullptr;
 685   }
 686   // must build model at this point
 687   if (!d_tc->buildModel())
 688   {
 689     return nullptr;
 690   }
 691   return d_tc->getModel();
 692 }
 693
 694 bool TheoryEngine::buildModel()
 695 {
 696   Assert(d_tc != nullptr);
 697   return d_tc->buildModel();
 698 }
 699
 700 bool TheoryEngine::getSynthSolutions(
 701     std::map<Node, std::map<Node, Node>>& sol_map)
 702 {
 703   if (d_quantEngine)
 704   {
 705     return d_quantEngine->getSynthSolutions(sol_map);
 706   }
 707   // we are not in a quantified logic, there is no synthesis solution
 708   return false;
 709 }
 710
 711 bool TheoryEngine::presolve() {
 712   // Reset the interrupt flag
 713   d_interrupted = false;
 714
 715   // Reset the decision manager. This clears its decision strategies that are
 716   // no longer valid in this user context.
 717   d_decManager->presolve();
 718
 719   try {
 720     // Definition of the statement that is to be run by every theory
 721 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 722 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 723 #endif
 724 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 725     if (theory::TheoryTraits<THEORY>::hasPresolve) {    \
 726       theoryOf(THEORY)->presolve(); \
 727       if(d_inConflict) { \
 728         return true; \
 729       } \
 730     }
 731
 732     // Presolve for each theory using the statement above
 733     CVC4_FOR_EACH_THEORY;
 734   } catch(const theory::Interrupted&) {
 735     Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl;
 736   }
 737   // return whether we have a conflict
 738   return false;
 739 }/* TheoryEngine::presolve() */
 740
 741 void TheoryEngine::postsolve() {
 742   // no longer in SAT mode
 743   d_inSatMode = false;
 744   // Reset the interrupt flag
 745   d_interrupted = false;
 746   bool CVC4_UNUSED wasInConflict = d_inConflict;
 747
 748   try {
 749     // Definition of the statement that is to be run by every theory
 750 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 751 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 752 #endif
 753 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY)    \
 754   if (theory::TheoryTraits<THEORY>::hasPostsolve) \
 755   {                                               \
 756     theoryOf(THEORY)->postsolve();                \
 757     Assert(!d_inConflict || wasInConflict)        \
 758         << "conflict raised during postsolve()";  \
 759   }
 760
 761     // Postsolve for each theory using the statement above
 762     CVC4_FOR_EACH_THEORY;
 763   } catch(const theory::Interrupted&) {
 764     Trace("theory") << "TheoryEngine::postsolve() => interrupted" << endl;
 765   }
 766 }/* TheoryEngine::postsolve() */
 767
 768
 769 void TheoryEngine::notifyRestart() {
 770   // Reset the interrupt flag
 771   d_interrupted = false;
 772
 773   // Definition of the statement that is to be run by every theory
 774 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 775 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 776 #endif
 777 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 778   if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_logicInfo.isTheoryEnabled(THEORY)) { \
 779     theoryOf(THEORY)->notifyRestart(); \
 780   }
 781
 782   // notify each theory using the statement above
 783   CVC4_FOR_EACH_THEORY;
 784 }
 785
 786 void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
 787   // Reset the interrupt flag
 788   d_interrupted = false;
 789
 790   // Definition of the statement that is to be run by every theory
 791 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 792 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 793 #endif
 794 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 795   if (theory::TheoryTraits<THEORY>::hasPpStaticLearn) { \
 796     theoryOf(THEORY)->ppStaticLearn(in, learned); \
 797   }
 798
 799   // static learning for each theory using the statement above
 800   CVC4_FOR_EACH_THEORY;
 801 }
 802
 803 bool TheoryEngine::isRelevant(Node lit) const
 804 {
 805   if (d_relManager != nullptr)
 806   {
 807     return d_relManager->isRelevant(lit);
 808   }
 809   // otherwise must assume its relevant
 810   return true;
 811 }
 812
 813 void TheoryEngine::shutdown() {
 814   // Set this first; if a Theory shutdown() throws an exception,
 815   // at least the destruction of the TheoryEngine won't confound
 816   // matters.
 817   d_hasShutDown = true;
 818
 819   // Shutdown all the theories
 820   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
 821     if(d_theoryTable[theoryId]) {
 822       theoryOf(theoryId)->shutdown();
 823     }
 824   }
 825
 826   d_tpp.clearCache();
 827 }
 828
 829 theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) {
 830   // Reset the interrupt flag
 831   d_interrupted = false;
 832
 833   TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
 834   Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
 835
 836   if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(atom)) &&
 837      Theory::theoryOf(atom) != THEORY_SAT_SOLVER) {
 838     stringstream ss;
 839     ss << "The logic was specified as " << d_logicInfo.getLogicString()
 840        << ", which doesn't include " << Theory::theoryOf(atom)
 841        << ", but got a preprocessing-time fact for that theory." << endl
 842        << "The fact:" << endl
 843        << literal;
 844     throw LogicException(ss.str());
 845   }
 846
 847   Theory::PPAssertStatus solveStatus = theoryOf(atom)->ppAssert(literal, substitutionOut);
 848   Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl;
 849   return solveStatus;
 850 }
 851
 852 void TheoryEngine::preprocessStart() { d_tpp.clearCache(); }
 853
 854 Node TheoryEngine::preprocess(TNode assertion) {
 855   TrustNode trn = d_tpp.theoryPreprocess(assertion);
 856   if (trn.isNull())
 857   {
 858     // no change
 859     return assertion;
 860   }
 861   return trn.getNode();
 862 }
 863
 864 void TheoryEngine::notifyPreprocessedAssertions(
 865     const std::vector<Node>& assertions) {
 866   // call all the theories
 867   for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
 868        ++theoryId) {
 869     if (d_theoryTable[theoryId]) {
 870       theoryOf(theoryId)->ppNotifyAssertions(assertions);
 871     }
 872   }
 873   if (d_relManager != nullptr)
 874   {
 875     d_relManager->notifyPreprocessedAssertions(assertions);
 876   }
 877 }
 878
 879 bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
 880
 881   // What and where we are asserting
 882   NodeTheoryPair toAssert(assertion, toTheoryId, d_propagationMapTimestamp);
 883   // What and where it came from
 884   NodeTheoryPair toExplain(originalAssertion, fromTheoryId, d_propagationMapTimestamp);
 885
 886   // See if the theory already got this literal
 887   PropagationMap::const_iterator find = d_propagationMap.find(toAssert);
 888   if (find != d_propagationMap.end()) {
 889     // The theory already knows this
 890     Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): already there" << endl;
 891     return false;
 892   }
 893
 894   Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): marking [" << d_propagationMapTimestamp << "] " << assertion << ", " << toTheoryId << " from " << originalAssertion << ", " << fromTheoryId << endl;
 895
 896   // Mark the propagation
 897   d_propagationMap[toAssert] = toExplain;
 898   d_propagationMapTimestamp = d_propagationMapTimestamp + 1;
 899
 900   return true;
 901 }
 902
 903
 904 void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
 905
 906   Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << originalAssertion << "," << toTheoryId << ", " << fromTheoryId << ")" << endl;
 907
 908   Assert(toTheoryId != fromTheoryId);
 909   if(toTheoryId != THEORY_SAT_SOLVER &&
 910      ! d_logicInfo.isTheoryEnabled(toTheoryId)) {
 911     stringstream ss;
 912     ss << "The logic was specified as " << d_logicInfo.getLogicString()
 913        << ", which doesn't include " << toTheoryId
 914        << ", but got an asserted fact to that theory." << endl
 915        << "The fact:" << endl
 916        << assertion;
 917     throw LogicException(ss.str());
 918   }
 919
 920   if (d_inConflict) {
 921     return;
 922   }
 923
 924   // If sharing is disabled, things are easy
 925   if (!d_logicInfo.isSharingEnabled()) {
 926     Assert(assertion == originalAssertion);
 927     if (fromTheoryId == THEORY_SAT_SOLVER) {
 928       // Send to the apropriate theory
 929       theory::Theory* toTheory = theoryOf(toTheoryId);
 930       // We assert it, and we know it's preregistereed
 931       toTheory->assertFact(assertion, true);
 932       // Mark that we have more information
 933       d_factsAsserted = true;
 934     } else {
 935       Assert(toTheoryId == THEORY_SAT_SOLVER);
 936       // Check for propositional conflict
 937       bool value;
 938       if (d_propEngine->hasValue(assertion, value)) {
 939         if (!value) {
 940           Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (no sharing)" << endl;
 941           Trace("dtview::conflict")
 942               << ":THEORY-CONFLICT: " << assertion << std::endl;
 943           d_inConflict = true;
 944         } else {
 945           return;
 946         }
 947       }
 948       d_propagatedLiterals.push_back(assertion);
 949     }
 950     return;
 951   }
 952
 953   // Polarity of the assertion
 954   bool polarity = assertion.getKind() != kind::NOT;
 955
 956   // Atom of the assertion
 957   TNode atom = polarity ? assertion : assertion[0];
 958
 959   // If sending to the shared terms database, it's also simple
 960   if (toTheoryId == THEORY_BUILTIN) {
 961     Assert(atom.getKind() == kind::EQUAL)
 962         << "atom should be an EQUALity, not `" << atom << "'";
 963     if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
 964       d_sharedTerms.assertEquality(atom, polarity, assertion);
 965     }
 966     return;
 967   }
 968
 969   // Things from the SAT solver are already normalized, so they go
 970   // directly to the apropriate theory
 971   if (fromTheoryId == THEORY_SAT_SOLVER) {
 972     // We know that this is normalized, so just send it off to the theory
 973     if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
 974       // Is it preregistered
 975       bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
 976       // We assert it
 977       theoryOf(toTheoryId)->assertFact(assertion, preregistered);
 978       // Mark that we have more information
 979       d_factsAsserted = true;
 980     }
 981     return;
 982   }
 983
 984   // Propagations to the SAT solver are just enqueued for pickup by
 985   // the SAT solver later
 986   if (toTheoryId == THEORY_SAT_SOLVER) {
 987     if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
 988       // Enqueue for propagation to the SAT solver
 989       d_propagatedLiterals.push_back(assertion);
 990       // Check for propositional conflicts
 991       bool value;
 992       if (d_propEngine->hasValue(assertion, value) && !value) {
 993         Trace("theory::propagate")
 994             << "TheoryEngine::assertToTheory(" << assertion << ", "
 995             << toTheoryId << ", " << fromTheoryId << "): conflict (sharing)"
 996             << endl;
 997         Trace("dtview::conflict")
 998             << ":THEORY-CONFLICT: " << assertion << std::endl;
 999         d_inConflict = true;
1000       }
1001     }
1002     return;
1003   }
1004
1005   Assert(atom.getKind() == kind::EQUAL);
1006
1007   // Normalize
1008   Node normalizedLiteral = Rewriter::rewrite(assertion);
1009
1010   // See if it rewrites false directly -> conflict
1011   if (normalizedLiteral.isConst()) {
1012     if (!normalizedLiteral.getConst<bool>()) {
1013       // Mark the propagation for explanations
1014       if (markPropagation(normalizedLiteral, originalAssertion, toTheoryId, fromTheoryId)) {
1015         // special case, trust node has no proof generator
1016         TrustNode trnn = TrustNode::mkTrustConflict(normalizedLiteral);
1017         // Get the explanation (conflict will figure out where it came from)
1018         conflict(trnn, toTheoryId);
1019       } else {
1020         Unreachable();
1021       }
1022       return;
1023     }
1024   }
1025
1026   // Try and assert (note that we assert the non-normalized one)
1027   if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
1028     // Check if has been pre-registered with the theory
1029     bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
1030     // Assert away
1031     theoryOf(toTheoryId)->assertFact(assertion, preregistered);
1032     d_factsAsserted = true;
1033   }
1034
1035   return;
1036 }
1037
1038 void TheoryEngine::assertFact(TNode literal)
1039 {
1040   Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << endl;
1041
1042   // spendResource();
1043
1044   // If we're in conflict, nothing to do
1045   if (d_inConflict) {
1046     return;
1047   }
1048
1049   // Get the atom
1050   bool polarity = literal.getKind() != kind::NOT;
1051   TNode atom = polarity ? literal : literal[0];
1052
1053   if (d_logicInfo.isSharingEnabled()) {
1054     // If any shared terms, it's time to do sharing work
1055     if (d_sharedTerms.hasSharedTerms(atom)) {
1056       // Notify the theories the shared terms
1057       SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom);
1058       SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom);
1059       for (; it != it_end; ++ it) {
1060         TNode term = *it;
1061         theory::TheoryIdSet theories =
1062             d_sharedTerms.getTheoriesToNotify(atom, term);
1063         for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++ id) {
1064           if (TheoryIdSetUtil::setContains(id, theories))
1065           {
1066             theoryOf(id)->addSharedTerm(term);
1067           }
1068         }
1069         d_sharedTerms.markNotified(term, theories);
1070       }
1071     }
1072
1073     // If it's an equality, assert it to the shared term manager, even though the terms are not
1074     // yet shared. As the terms become shared later, the shared terms manager will then add them
1075     // to the assert the equality to the interested theories
1076     if (atom.getKind() == kind::EQUAL) {
1077       // Assert it to the the owning theory
1078       assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
1079       // Shared terms manager will assert to interested theories directly, as
1080       // the terms become shared
1081       assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ THEORY_SAT_SOLVER);
1082
1083       // Now, let's check for any atom triggers from lemmas
1084       AtomRequests::atom_iterator it = d_atomRequests.getAtomIterator(atom);
1085       while (!it.done()) {
1086         const AtomRequests::Request& request = it.get();
1087         Node toAssert =
1088             polarity ? (Node)request.d_atom : request.d_atom.notNode();
1089         Debug("theory::atoms") << "TheoryEngine::assertFact(" << literal << "): sending requested " << toAssert << endl;
1090         assertToTheory(
1091             toAssert, literal, request.d_toTheory, THEORY_SAT_SOLVER);
1092         it.next();
1093       }
1094
1095     } else {
1096       // Not an equality, just assert to the appropriate theory
1097       assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
1098     }
1099   } else {
1100     // Assert the fact to the appropriate theory directly
1101     assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
1102   }
1103 }
1104
1105 bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
1106   Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl;
1107
1108   Trace("dtview::prop") << std::string(d_context->getLevel(), ' ')
1109                         << ":THEORY-PROP: " << literal << endl;
1110
1111   // spendResource();
1112
1113   // Get the atom
1114   bool polarity = literal.getKind() != kind::NOT;
1115   TNode atom = polarity ? literal : literal[0];
1116
1117   if (d_logicInfo.isSharingEnabled() && atom.getKind() == kind::EQUAL) {
1118     if (d_propEngine->isSatLiteral(literal)) {
1119       // We propagate SAT literals to SAT
1120       assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
1121     }
1122     if (theory != THEORY_BUILTIN) {
1123       // Assert to the shared terms database
1124       assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory);
1125     }
1126   } else {
1127     // Just send off to the SAT solver
1128     Assert(d_propEngine->isSatLiteral(literal));
1129     assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
1130   }
1131
1132   return !d_inConflict;
1133 }
1134
1135 const LogicInfo& TheoryEngine::getLogicInfo() const { return d_logicInfo; }
1136
1137 theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
1138   Assert(a.getType().isComparableTo(b.getType()));
1139   if (d_sharedTerms.isShared(a) && d_sharedTerms.isShared(b)) {
1140     if (d_sharedTerms.areEqual(a,b)) {
1141       return EQUALITY_TRUE_AND_PROPAGATED;
1142     }
1143     else if (d_sharedTerms.areDisequal(a,b)) {
1144       return EQUALITY_FALSE_AND_PROPAGATED;
1145     }
1146   }
1147   return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
1148 }
1149
1150 Node TheoryEngine::getModelValue(TNode var) {
1151   if (var.isConst())
1152   {
1153     // the model value of a constant must be itself
1154     return var;
1155   }
1156   Assert(d_sharedTerms.isShared(var));
1157   return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
1158 }
1159
1160
1161 Node TheoryEngine::ensureLiteral(TNode n) {
1162   Debug("ensureLiteral") << "rewriting: " << n << std::endl;
1163   Node rewritten = Rewriter::rewrite(n);
1164   Debug("ensureLiteral") << "      got: " << rewritten << std::endl;
1165   Node preprocessed = preprocess(rewritten);
1166   Debug("ensureLiteral") << "preprocessed: " << preprocessed << std::endl;
1167   d_propEngine->ensureLiteral(preprocessed);
1168   return preprocessed;
1169 }
1170
1171
1172 void TheoryEngine::printInstantiations( std::ostream& out ) {
1173   if( d_quantEngine ){
1174     d_quantEngine->printInstantiations( out );
1175   }else{
1176     out << "Internal error : instantiations not available when quantifiers are not present." << std::endl;
1177     Assert(false);
1178   }
1179 }
1180
1181 void TheoryEngine::printSynthSolution( std::ostream& out ) {
1182   if( d_quantEngine ){
1183     d_quantEngine->printSynthSolution( out );
1184   }else{
1185     out << "Internal error : synth solution not available when quantifiers are not present." << std::endl;
1186     Assert(false);
1187   }
1188 }
1189
1190 void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
1191   if( d_quantEngine ){
1192     d_quantEngine->getInstantiatedQuantifiedFormulas( qs );
1193   }else{
1194     Assert(false);
1195   }
1196 }
1197
1198 void TheoryEngine::getInstantiations( Node q, std::vector< Node >& insts ) {
1199   if( d_quantEngine ){
1200     d_quantEngine->getInstantiations( q, insts );
1201   }else{
1202     Assert(false);
1203   }
1204 }
1205
1206 void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
1207   if( d_quantEngine ){
1208     d_quantEngine->getInstantiationTermVectors( q, tvecs );
1209   }else{
1210     Assert(false);
1211   }
1212 }
1213
1214 void TheoryEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
1215   if( d_quantEngine ){
1216     d_quantEngine->getInstantiations( insts );
1217   }else{
1218     Assert(false);
1219   }
1220 }
1221
1222 void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
1223   if( d_quantEngine ){
1224     d_quantEngine->getInstantiationTermVectors( insts );
1225   }else{
1226     Assert(false);
1227   }
1228 }
1229
1230 Node TheoryEngine::getInstantiatedConjunction( Node q ) {
1231   if( d_quantEngine ){
1232     return d_quantEngine->getInstantiatedConjunction( q );
1233   }else{
1234     Assert(false);
1235     return Node::null();
1236   }
1237 }
1238
1239
1240 static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
1241
1242   std::set<TNode> all;
1243   for (unsigned i = 0; i < explanation.size(); ++ i) {
1244     Assert(explanation[i].d_theory == THEORY_SAT_SOLVER);
1245     all.insert(explanation[i].d_node);
1246   }
1247
1248   if (all.size() == 0) {
1249     // Normalize to true
1250     return NodeManager::currentNM()->mkConst<bool>(true);
1251   }
1252
1253   if (all.size() == 1) {
1254     // All the same, or just one
1255     return explanation[0].d_node;
1256   }
1257
1258   NodeBuilder<> conjunction(kind::AND);
1259   std::set<TNode>::const_iterator it = all.begin();
1260   std::set<TNode>::const_iterator it_end = all.end();
1261   while (it != it_end) {
1262     conjunction << *it;
1263     ++ it;
1264   }
1265
1266   return conjunction;
1267 }
1268
1269 TrustNode TheoryEngine::getExplanation(TNode node)
1270 {
1271   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
1272                            << "): current propagation index = "
1273                            << d_propagationMapTimestamp << endl;
1274
1275   bool polarity = node.getKind() != kind::NOT;
1276   TNode atom = polarity ? node : node[0];
1277
1278   // If we're not in shared mode, explanations are simple
1279   if (!d_logicInfo.isSharingEnabled())
1280   {
1281     Debug("theory::explain")
1282         << "TheoryEngine::getExplanation: sharing is NOT enabled. "
1283         << " Responsible theory is: " << theoryOf(atom)->getId() << std::endl;
1284
1285     TrustNode texplanation = theoryOf(atom)->explain(node);
1286     Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
1287                              << ") => " << texplanation.getNode() << endl;
1288     return texplanation;
1289   }
1290
1291   Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled"
1292                            << std::endl;
1293
1294   // Initial thing to explain
1295   NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp);
1296   Assert(d_propagationMap.find(toExplain) != d_propagationMap.end());
1297
1298   NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain];
1299   Debug("theory::explain")
1300       << "TheoryEngine::getExplanation: explainer for node "
1301       << nodeExplainerPair.d_node
1302       << " is theory: " << nodeExplainerPair.d_theory << std::endl;
1303
1304   // Create the workplace for explanations
1305   std::vector<NodeTheoryPair> explanationVector;
1306   explanationVector.push_back(d_propagationMap[toExplain]);
1307   // Process the explanation
1308   TrustNode texplanation = getExplanation(explanationVector);
1309   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => "
1310                            << texplanation.getNode() << endl;
1311   return texplanation;
1312 }
1313
1314 struct AtomsCollect {
1315
1316   std::vector<TNode> d_atoms;
1317   std::unordered_set<TNode, TNodeHashFunction> d_visited;
1318
1319 public:
1320
1321   typedef void return_type;
1322
1323   bool alreadyVisited(TNode current, TNode parent) {
1324     // Check if already visited
1325     if (d_visited.find(current) != d_visited.end()) return true;
1326     // Don't visit non-boolean
1327     if (!current.getType().isBoolean()) return true;
1328     // New node
1329     return false;
1330   }
1331
1332   void visit(TNode current, TNode parent) {
1333     if (Theory::theoryOf(current) != theory::THEORY_BOOL) {
1334       d_atoms.push_back(current);
1335     }
1336     d_visited.insert(current);
1337   }
1338
1339   void start(TNode node) {}
1340   void done(TNode node) {}
1341
1342   std::vector<TNode> getAtoms() const {
1343     return d_atoms;
1344   }
1345 };
1346
1347 void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId atomsTo) {
1348   for (unsigned i = 0; i < atoms.size(); ++ i) {
1349
1350     // Non-equality atoms are either owned by theory or they don't make sense
1351     if (atoms[i].getKind() != kind::EQUAL) {
1352       continue;
1353     }
1354
1355     // The equality
1356     Node eq = atoms[i];
1357     // Simple normalization to not repeat stuff
1358     if (eq[0] > eq[1]) {
1359       eq = eq[1].eqNode(eq[0]);
1360     }
1361
1362     // Rewrite the equality
1363     Node eqNormalized = Rewriter::rewrite(atoms[i]);
1364
1365     Debug("theory::atoms") << "TheoryEngine::ensureLemmaAtoms(): " << eq << " with nf " << eqNormalized << endl;
1366
1367     // If the equality is a boolean constant, we send immediately
1368     if (eqNormalized.isConst()) {
1369       if (eqNormalized.getConst<bool>()) {
1370         assertToTheory(eq, eqNormalized, /** to */ atomsTo, /** Sat solver */ theory::THEORY_SAT_SOLVER);
1371       } else {
1372         assertToTheory(eq.notNode(), eqNormalized.notNode(), /** to */ atomsTo, /** Sat solver */ theory::THEORY_SAT_SOLVER);
1373       }
1374       continue;
1375     }else if( eqNormalized.getKind() != kind::EQUAL){
1376       Assert(eqNormalized.getKind() == kind::BOOLEAN_TERM_VARIABLE
1377              || (eqNormalized.getKind() == kind::NOT
1378                  && eqNormalized[0].getKind() == kind::BOOLEAN_TERM_VARIABLE));
1379       // this happens for Boolean term equalities V = true that are rewritten to V, we should skip
1380       //  TODO : revisit this
1381       continue;
1382     }
1383
1384     // If the normalization did the just flips, keep the flip
1385     if (eqNormalized[0] == eq[1] && eqNormalized[1] == eq[0]) {
1386       eq = eqNormalized;
1387     }
1388
1389     // Check if the equality is already known by the sat solver
1390     if (d_propEngine->isSatLiteral(eqNormalized)) {
1391       bool value;
1392       if (d_propEngine->hasValue(eqNormalized, value)) {
1393         if (value) {
1394           assertToTheory(eq, eqNormalized, atomsTo, theory::THEORY_SAT_SOLVER);
1395           continue;
1396         } else {
1397           assertToTheory(eq.notNode(), eqNormalized.notNode(), atomsTo, theory::THEORY_SAT_SOLVER);
1398           continue;
1399         }
1400       }
1401     }
1402
1403     // If the theory is asking about a different form, or the form is ok but if will go to a different theory
1404     // then we must figure it out
1405     if (eqNormalized != eq || Theory::theoryOf(eq) != atomsTo) {
1406       // If you get eqNormalized, send atoms[i] to atomsTo
1407       d_atomRequests.add(eqNormalized, eq, atomsTo);
1408     }
1409   }
1410 }
1411
1412 theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
1413                                         theory::LemmaProperty p,
1414                                         theory::TheoryId atomsTo,
1415                                         theory::TheoryId from)
1416 {
1417   // For resource-limiting (also does a time check).
1418   // spendResource();
1419   Assert(tlemma.getKind() == TrustNodeKind::LEMMA
1420          || tlemma.getKind() == TrustNodeKind::CONFLICT);
1421   // get the node
1422   Node node = tlemma.getNode();
1423   Node lemma = tlemma.getProven();
1424
1425   // when proofs are enabled, we ensure the trust node has a generator by
1426   // adding a trust step to the lazy proof maintained by this class
1427   if (isProofEnabled())
1428   {
1429     // ensure proof: set THEORY_LEMMA if no generator is provided
1430     if (tlemma.getGenerator() == nullptr)
1431     {
1432       // internal lemmas should have generators
1433       Assert(from != THEORY_LAST);
1434       // add theory lemma step to proof
1435       Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(from);
1436       d_lazyProof->addStep(lemma, PfRule::THEORY_LEMMA, {}, {lemma, tidn});
1437       // update the trust node
1438       tlemma = TrustNode::mkTrustLemma(lemma, d_lazyProof.get());
1439     }
1440     // ensure closed
1441     tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_initial");
1442   }
1443
1444   // Do we need to check atoms
1445   if (atomsTo != theory::THEORY_LAST) {
1446     Debug("theory::atoms") << "TheoryEngine::lemma(" << node << ", " << atomsTo << ")" << endl;
1447     AtomsCollect collectAtoms;
1448     NodeVisitor<AtomsCollect>::run(collectAtoms, node);
1449     ensureLemmaAtoms(collectAtoms.getAtoms(), atomsTo);
1450   }
1451
1452   if(Dump.isOn("t-lemmas")) {
1453     // we dump the negation of the lemma, to show validity of the lemma
1454     Node n = lemma.negate();
1455     const Printer& printer = d_outMgr.getPrinter();
1456     std::ostream& out = d_outMgr.getDumpOut();
1457     printer.toStreamCmdComment(out, "theory lemma: expect valid");
1458     printer.toStreamCmdCheckSat(out, n);
1459   }
1460   bool removable = isLemmaPropertyRemovable(p);
1461   bool preprocess = isLemmaPropertyPreprocess(p);
1462
1463   // call preprocessor
1464   std::vector<TrustNode> newLemmas;
1465   std::vector<Node> newSkolems;
1466   TrustNode tplemma =
1467       d_tpp.preprocess(lemma, newLemmas, newSkolems, preprocess);
1468   // the preprocessed lemma
1469   Node lemmap;
1470   if (tplemma.isNull())
1471   {
1472     lemmap = lemma;
1473   }
1474   else
1475   {
1476     Assert(tplemma.getKind() == TrustNodeKind::REWRITE);
1477     lemmap = tplemma.getNode();
1478
1479     // must update the trust lemma
1480     if (lemmap != lemma)
1481     {
1482       // process the preprocessing
1483       if (isProofEnabled())
1484       {
1485         Assert(d_lazyProof != nullptr);
1486         // add the original proof to the lazy proof
1487         d_lazyProof->addLazyStep(tlemma.getProven(), tlemma.getGenerator());
1488         // only need to do anything if lemmap changed in a non-trivial way
1489         if (!CDProof::isSame(lemmap, lemma))
1490         {
1491           d_lazyProof->addLazyStep(tplemma.getProven(),
1492                                    tplemma.getGenerator(),
1493                                    true,
1494                                    "TheoryEngine::lemma_pp",
1495                                    false,
1496                                    PfRule::PREPROCESS_LEMMA);
1497           // ---------- from d_lazyProof -------------- from theory preprocess
1498           // lemma                       lemma = lemmap
1499           // ------------------------------------------ MACRO_SR_PRED_TRANSFORM
1500           // lemmap
1501           std::vector<Node> pfChildren;
1502           pfChildren.push_back(lemma);
1503           pfChildren.push_back(tplemma.getProven());
1504           std::vector<Node> pfArgs;
1505           pfArgs.push_back(lemmap);
1506           d_lazyProof->addStep(
1507               lemmap, PfRule::MACRO_SR_PRED_TRANSFORM, pfChildren, pfArgs);
1508         }
1509       }
1510       tlemma = TrustNode::mkTrustLemma(lemmap, d_lazyProof.get());
1511     }
1512   }
1513
1514   // must use an assertion pipeline due to decision engine below
1515   AssertionPipeline lemmas;
1516   // make the assertion pipeline
1517   lemmas.push_back(lemmap);
1518   lemmas.updateRealAssertionsEnd();
1519   Assert(newSkolems.size() == newLemmas.size());
1520   for (size_t i = 0, nsize = newLemmas.size(); i < nsize; i++)
1521   {
1522     // store skolem mapping here
1523     IteSkolemMap& imap = lemmas.getIteSkolemMap();
1524     imap[newSkolems[i]] = lemmas.size();
1525     lemmas.push_back(newLemmas[i].getNode());
1526   }
1527
1528   // If specified, we must add this lemma to the set of those that need to be
1529   // justified, where note we pass all auxiliary lemmas in lemmas, since these
1530   // by extension must be justified as well.
1531   if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p))
1532   {
1533     d_relManager->notifyPreprocessedAssertions(lemmas.ref());
1534   }
1535
1536   // do final checks on the lemmas we are about to send
1537   if (isProofEnabled())
1538   {
1539     Assert(tlemma.getGenerator() != nullptr);
1540     // ensure closed, make the proof node eagerly here to debug
1541     tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma");
1542     for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
1543     {
1544       Assert(newLemmas[i].getGenerator() != nullptr);
1545       newLemmas[i].debugCheckClosed("te-proof-debug",
1546                                     "TheoryEngine::lemma_new");
1547     }
1548   }
1549
1550   // now, send the lemmas to the prop engine
1551   d_propEngine->assertLemma(tlemma.getProven(), false, removable);
1552   for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
1553   {
1554     d_propEngine->assertLemma(newLemmas[i].getProven(), false, removable);
1555   }
1556
1557   // assert to decision engine
1558   if (!removable)
1559   {
1560     d_propEngine->addAssertionsToDecisionEngine(lemmas);
1561   }
1562
1563   // Mark that we added some lemmas
1564   d_lemmasAdded = true;
1565
1566   // Lemma analysis isn't online yet; this lemma may only live for this
1567   // user level.
1568   Node retLemma = lemmas[0];
1569   if (lemmas.size() > 1)
1570   {
1571     // the returned lemma is the conjunction of all additional lemmas.
1572     retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas.ref());
1573   }
1574   return theory::LemmaStatus(retLemma, d_userContext->getLevel());
1575 }
1576
1577 void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId)
1578 {
1579   Assert(tconflict.getKind() == TrustNodeKind::CONFLICT);
1580   TNode conflict = tconflict.getNode();
1581   Trace("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", "
1582                             << theoryId << ")" << endl;
1583   Trace("te-proof-debug") << "Check closed conflict" << std::endl;
1584   // doesn't require proof generator, yet, since THEORY_LEMMA is added below
1585   tconflict.debugCheckClosed(
1586       "te-proof-debug", "TheoryEngine::conflict_initial", false);
1587
1588   Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl;
1589
1590   // Mark that we are in conflict
1591   d_inConflict = true;
1592
1593   if(Dump.isOn("t-conflicts")) {
1594     const Printer& printer = d_outMgr.getPrinter();
1595     std::ostream& out = d_outMgr.getDumpOut();
1596     printer.toStreamCmdComment(out, "theory conflict: expect unsat");
1597     printer.toStreamCmdCheckSat(out, conflict);
1598   }
1599
1600   // In the multiple-theories case, we need to reconstruct the conflict
1601   if (d_logicInfo.isSharingEnabled()) {
1602     // Create the workplace for explanations
1603     std::vector<NodeTheoryPair> vec;
1604     vec.push_back(
1605         NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
1606
1607     // Process the explanation
1608     TrustNode tncExp = getExplanation(vec);
1609     Trace("te-proof-debug")
1610         << "Check closed conflict explained with sharing" << std::endl;
1611     tncExp.debugCheckClosed("te-proof-debug",
1612                             "TheoryEngine::conflict_explained_sharing");
1613     Node fullConflict = tncExp.getNode();
1614
1615     if (isProofEnabled())
1616     {
1617       Trace("te-proof-debug") << "Process conflict: " << conflict << std::endl;
1618       Trace("te-proof-debug") << "Conflict " << tconflict << " from "
1619                               << tconflict.identifyGenerator() << std::endl;
1620       Trace("te-proof-debug") << "Explanation " << tncExp << " from "
1621                               << tncExp.identifyGenerator() << std::endl;
1622       Assert(d_lazyProof != nullptr);
1623       if (tconflict.getGenerator() != nullptr)
1624       {
1625         d_lazyProof->addLazyStep(tconflict.getProven(),
1626                                  tconflict.getGenerator());
1627       }
1628       else
1629       {
1630         // add theory lemma step
1631         Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
1632         Node conf = tconflict.getProven();
1633         d_lazyProof->addStep(conf, PfRule::THEORY_LEMMA, {}, {conf, tidn});
1634       }
1635       // store the explicit step, which should come from a different
1636       // generator, e.g. d_tepg.
1637       Node proven = tncExp.getProven();
1638       Assert(tncExp.getGenerator() != d_lazyProof.get());
1639       Trace("te-proof-debug") << "add lazy step " << tncExp.identifyGenerator()
1640                               << " for " << proven << std::endl;
1641       d_lazyProof->addLazyStep(proven, tncExp.getGenerator());
1642       pfgEnsureClosed(proven,
1643                       d_lazyProof.get(),
1644                       "te-proof-debug",
1645                       "TheoryEngine::conflict_during");
1646       Node fullConflictNeg = fullConflict.notNode();
1647       std::vector<Node> children;
1648       children.push_back(proven);
1649       std::vector<Node> args;
1650       args.push_back(fullConflictNeg);
1651       if (conflict == d_false)
1652       {
1653         AlwaysAssert(proven == fullConflictNeg);
1654       }
1655       else
1656       {
1657         if (fullConflict != conflict)
1658         {
1659           // ------------------------- explained  ---------- from theory
1660           // fullConflict => conflict              ~conflict
1661           // --------------------------------------------
1662           // MACRO_SR_PRED_TRANSFORM ~fullConflict
1663           children.push_back(conflict.notNode());
1664           args.push_back(mkMethodId(MethodId::SB_LITERAL));
1665           d_lazyProof->addStep(
1666               fullConflictNeg, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
1667         }
1668       }
1669     }
1670     // pass the processed trust node
1671     TrustNode tconf =
1672         TrustNode::mkTrustConflict(fullConflict, d_lazyProof.get());
1673     Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
1674     Assert(properConflict(fullConflict));
1675     Trace("te-proof-debug")
1676         << "Check closed conflict with sharing" << std::endl;
1677     tconf.debugCheckClosed("te-proof-debug", "TheoryEngine::conflict:sharing");
1678     lemma(tconf, LemmaProperty::REMOVABLE);
1679   } else {
1680     // When only one theory, the conflict should need no processing
1681     Assert(properConflict(conflict));
1682     // pass the trust node that was sent from the theory
1683     lemma(tconflict, LemmaProperty::REMOVABLE, THEORY_LAST, theoryId);
1684   }
1685 }
1686
1687 theory::TrustNode TheoryEngine::getExplanation(
1688     std::vector<NodeTheoryPair>& explanationVector)
1689 {
1690   Assert(explanationVector.size() > 0);
1691
1692   unsigned i = 0; // Index of the current literal we are processing
1693   unsigned j = 0; // Index of the last literal we are keeping
1694
1695   // cache of nodes we have already explained by some theory
1696   std::unordered_map<Node, size_t, NodeHashFunction> cache;
1697
1698   while (i < explanationVector.size()) {
1699     // Get the current literal to explain
1700     NodeTheoryPair toExplain = explanationVector[i];
1701
1702     Debug("theory::explain")
1703         << "[i=" << i << "] TheoryEngine::explain(): processing ["
1704         << toExplain.d_timestamp << "] " << toExplain.d_node << " sent from "
1705         << toExplain.d_theory << endl;
1706
1707     if (cache.find(toExplain.d_node) != cache.end()
1708         && cache[toExplain.d_node] < toExplain.d_timestamp)
1709     {
1710       ++i;
1711       continue;
1712     }
1713     cache[toExplain.d_node] = toExplain.d_timestamp;
1714
1715     // If a true constant or a negation of a false constant we can ignore it
1716     if (toExplain.d_node.isConst() && toExplain.d_node.getConst<bool>())
1717     {
1718       ++ i;
1719       continue;
1720     }
1721     if (toExplain.d_node.getKind() == kind::NOT && toExplain.d_node[0].isConst()
1722         && !toExplain.d_node[0].getConst<bool>())
1723     {
1724       ++ i;
1725       continue;
1726     }
1727
1728     // If from the SAT solver, keep it
1729     if (toExplain.d_theory == THEORY_SAT_SOLVER)
1730     {
1731       Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl;
1732       explanationVector[j++] = explanationVector[i++];
1733       continue;
1734     }
1735
1736     // If an and, expand it
1737     if (toExplain.d_node.getKind() == kind::AND)
1738     {
1739       Debug("theory::explain")
1740           << "TheoryEngine::explain(): expanding " << toExplain.d_node
1741           << " got from " << toExplain.d_theory << endl;
1742       for (unsigned k = 0; k < toExplain.d_node.getNumChildren(); ++k)
1743       {
1744         NodeTheoryPair newExplain(
1745             toExplain.d_node[k], toExplain.d_theory, toExplain.d_timestamp);
1746         explanationVector.push_back(newExplain);
1747       }
1748       ++ i;
1749       continue;
1750     }
1751
1752     // See if it was sent to the theory by another theory
1753     PropagationMap::const_iterator find = d_propagationMap.find(toExplain);
1754     if (find != d_propagationMap.end()) {
1755       Debug("theory::explain")
1756           << "\tTerm was propagated by another theory (theory = "
1757           << getTheoryString((*find).second.d_theory) << ")" << std::endl;
1758       // There is some propagation, check if its a timely one
1759       if ((*find).second.d_timestamp < toExplain.d_timestamp)
1760       {
1761         Debug("theory::explain")
1762             << "\tRelevant timetsamp, pushing " << (*find).second.d_node
1763             << "to index = " << explanationVector.size() << std::endl;
1764         explanationVector.push_back((*find).second);
1765         ++i;
1766
1767         continue;
1768       }
1769     }
1770
1771     Node explanation;
1772     if (toExplain.d_theory == THEORY_BUILTIN)
1773     {
1774       explanation = d_sharedTerms.explain(toExplain.d_node);
1775       Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl;
1776     }
1777     else
1778     {
1779       TrustNode texp = theoryOf(toExplain.d_theory)->explain(toExplain.d_node);
1780       explanation = texp.getNode();
1781       Debug("theory::explain") << "\tTerm was propagated by owner theory: "
1782                                << theoryOf(toExplain.d_theory)->getId()
1783                                << ". Explanation: " << explanation << std::endl;
1784     }
1785
1786     Debug("theory::explain")
1787         << "TheoryEngine::explain(): got explanation " << explanation
1788         << " got from " << toExplain.d_theory << endl;
1789     Assert(explanation != toExplain.d_node)
1790         << "wasn't sent to you, so why are you explaining it trivially";
1791     // Mark the explanation
1792     NodeTheoryPair newExplain(
1793         explanation, toExplain.d_theory, toExplain.d_timestamp);
1794     explanationVector.push_back(newExplain);
1795
1796     ++ i;
1797   }
1798
1799   // Keep only the relevant literals
1800   explanationVector.resize(j);
1801
1802   Node expNode = mkExplanation(explanationVector);
1803   return theory::TrustNode::mkTrustLemma(expNode, nullptr);
1804 }
1805
1806 bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; }
1807
1808 void TheoryEngine::setUserAttribute(const std::string& attr,
1809                                     Node n,
1810                                     const std::vector<Node>& node_values,
1811                                     const std::string& str_value)
1812 {
1813   Trace("te-attr") << "set user attribute " << attr << " " << n << endl;
1814   if( d_attr_handle.find( attr )!=d_attr_handle.end() ){
1815     for( size_t i=0; i<d_attr_handle[attr].size(); i++ ){
1816       d_attr_handle[attr][i]->setUserAttribute(attr, n, node_values, str_value);
1817     }
1818   } else {
1819     //unhandled exception?
1820   }
1821 }
1822
1823 void TheoryEngine::handleUserAttribute(const char* attr, Theory* t) {
1824   Trace("te-attr") << "Handle user attribute " << attr << " " << t << endl;
1825   std::string str( attr );
1826   d_attr_handle[ str ].push_back( t );
1827 }
1828
1829 void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
1830   for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
1831     Theory* theory = d_theoryTable[theoryId];
1832     if(theory && d_logicInfo.isTheoryEnabled(theoryId)) {
1833       for(context::CDList<Assertion>::const_iterator it = theory->facts_begin(),
1834             it_end = theory->facts_end();
1835           it != it_end;
1836           ++it) {
1837         Node assertion = (*it).d_assertion;
1838         if (!isRelevant(assertion))
1839         {
1840           // not relevant, skip
1841           continue;
1842         }
1843         Node val = d_tc->getModel()->getValue(assertion);
1844         if (val != d_true)
1845         {
1846           std::stringstream ss;
1847           ss << " " << theoryId
1848              << " has an asserted fact that the model doesn't satisfy." << endl
1849              << "The fact: " << assertion << endl
1850              << "Model value: " << val << endl;
1851           if (hardFailure)
1852           {
1853             if (val == d_false)
1854             {
1855               // Always an error if it is false
1856               InternalError() << ss.str();
1857             }
1858             else
1859             {
1860               // Otherwise just a warning. Notice this case may happen for
1861               // assertions with unevaluable operators, e.g. transcendental
1862               // functions. It also may happen for separation logic, where
1863               // check-model support is limited.
1864               Warning() << ss.str();
1865             }
1866           }
1867         }
1868       }
1869     }
1870   }
1871 }
1872
1873 std::pair<bool, Node> TheoryEngine::entailmentCheck(options::TheoryOfMode mode,
1874                                                     TNode lit)
1875 {
1876   TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit;
1877   if( atom.getKind()==kind::AND || atom.getKind()==kind::OR || atom.getKind()==kind::IMPLIES ){
1878     //Boolean connective, recurse
1879     std::vector< Node > children;
1880     bool pol = (lit.getKind()!=kind::NOT);
1881     bool is_conjunction = pol==(lit.getKind()==kind::AND);
1882     for( unsigned i=0; i<atom.getNumChildren(); i++ ){
1883       Node ch = atom[i];
1884       if( pol==( lit.getKind()==kind::IMPLIES && i==0 ) ){
1885         ch = atom[i].negate();
1886       }
1887       std::pair<bool, Node> chres = entailmentCheck(mode, ch);
1888       if( chres.first ){
1889         if( !is_conjunction ){
1890           return chres;
1891         }else{
1892           children.push_back( chres.second );
1893         }
1894       }else if( !chres.first && is_conjunction ){
1895         return std::pair<bool, Node>(false, Node::null());
1896       }
1897     }
1898     if( is_conjunction ){
1899       return std::pair<bool, Node>(true, NodeManager::currentNM()->mkNode(kind::AND, children));
1900     }else{
1901       return std::pair<bool, Node>(false, Node::null());
1902     }
1903   }else if( atom.getKind()==kind::ITE || ( atom.getKind()==kind::EQUAL && atom[0].getType().isBoolean() ) ){
1904     bool pol = (lit.getKind()!=kind::NOT);
1905     for( unsigned r=0; r<2; r++ ){
1906       Node ch = atom[0];
1907       if( r==1 ){
1908         ch = ch.negate();
1909       }
1910       std::pair<bool, Node> chres = entailmentCheck(mode, ch);
1911       if( chres.first ){
1912         Node ch2 = atom[ atom.getKind()==kind::ITE ? r+1 : 1 ];
1913         if( pol==( atom.getKind()==kind::ITE ? true : r==1 ) ){
1914           ch2 = ch2.negate();
1915         }
1916         std::pair<bool, Node> chres2 = entailmentCheck(mode, ch2);
1917         if( chres2.first ){
1918           return std::pair<bool, Node>(true, NodeManager::currentNM()->mkNode(kind::AND, chres.second, chres2.second));
1919         }else{
1920           break;
1921         }
1922       }
1923     }
1924     return std::pair<bool, Node>(false, Node::null());
1925   }else{
1926     //it is a theory atom
1927     theory::TheoryId tid = theory::Theory::theoryOf(mode, atom);
1928     theory::Theory* th = theoryOf(tid);
1929
1930     Assert(th != NULL);
1931     Trace("theory-engine-entc") << "Entailment check : " << lit << std::endl;
1932
1933     std::pair<bool, Node> chres = th->entailmentCheck(lit);
1934     return chres;
1935   }
1936 }
1937
1938 void TheoryEngine::spendResource(ResourceManager::Resource r)
1939 {
1940   d_resourceManager->spendResource(r);
1941 }
1942
1943 }/* CVC4 namespace */