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