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