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