src/theory/theory_engine.cpp

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