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