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