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