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