src/theory/theory_engine.cpp

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