src/theory/theory_engine.cpp

   1 /*********************                                                        */
   2 /*! \file theory_engine.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Dejan Jovanovic, Andrew Reynolds, 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/proof_options.h"
  32 #include "options/quantifiers_options.h"
  33 #include "options/theory_options.h"
  34 #include "preprocessing/assertion_pipeline.h"
  35 #include "proof/cnf_proof.h"
  36 #include "proof/lemma_proof.h"
  37 #include "proof/proof_manager.h"
  38 #include "proof/theory_proof.h"
  39 #include "smt/logic_exception.h"
  40 #include "smt/term_formula_removal.h"
  41 #include "theory/arith/arith_ite_utils.h"
  42 #include "theory/bv/theory_bv_utils.h"
  43 #include "theory/care_graph.h"
  44 #include "theory/decision_manager.h"
  45 #include "theory/ee_manager_distributed.h"
  46 #include "theory/quantifiers/first_order_model.h"
  47 #include "theory/quantifiers/fmf/model_engine.h"
  48 #include "theory/quantifiers/theory_quantifiers.h"
  49 #include "theory/quantifiers_engine.h"
  50 #include "theory/relevance_manager.h"
  51 #include "theory/rewriter.h"
  52 #include "theory/theory.h"
  53 #include "theory/theory_model.h"
  54 #include "theory/theory_traits.h"
  55 #include "theory/uf/equality_engine.h"
  56 #include "util/resource_manager.h"
  57
  58 using namespace std;
  59
  60 using namespace CVC4::preprocessing;
  61 using namespace CVC4::theory;
  62
  63 namespace CVC4 {
  64
  65 /* -------------------------------------------------------------------------- */
  66
  67 namespace theory {
  68
  69 /**
  70  * IMPORTANT: The order of the theories is important. For example, strings
  71  *            depends on arith, quantifiers needs to come as the very last.
  72  *            Do not change this order.
  73  */
  74
  75 #define CVC4_FOR_EACH_THEORY                                     \
  76   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BUILTIN)   \
  77   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BOOL)      \
  78   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_UF)        \
  79   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_ARITH)     \
  80   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BV)        \
  81   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_FP)        \
  82   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_ARRAYS)    \
  83   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_DATATYPES) \
  84   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SEP)       \
  85   CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SETS)      \
  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   // initialize the quantifiers engine
 135   if (d_logicInfo.isQuantified())
 136   {
 137     // initialize the quantifiers engine
 138     d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
 139   }
 140
 141   // Initialize the equality engine architecture for all theories, which
 142   // includes the master equality engine.
 143   d_eeDistributed.reset(new EqEngineManagerDistributed(*this));
 144   d_eeDistributed->initializeTheories();
 145
 146   // Initialize the model and model builder.
 147   if (d_logicInfo.isQuantified())
 148   {
 149     d_curr_model_builder = d_quantEngine->getModelBuilder();
 150     d_curr_model = d_quantEngine->getModel();
 151   } else {
 152     d_curr_model = new theory::TheoryModel(
 153         d_userContext, "DefaultModel", options::assignFunctionValues());
 154     d_aloc_curr_model = true;
 155   }
 156   // create the relevance filter if any option requires it
 157   if (options::relevanceFilter())
 158   {
 159     d_relManager.reset(
 160         new RelevanceManager(d_userContext, theory::Valuation(this)));
 161   }
 162
 163   //make the default builder, e.g. in the case that the quantifiers engine does not have a model builder
 164   if( d_curr_model_builder==NULL ){
 165     d_curr_model_builder = new theory::TheoryEngineModelBuilder(this);
 166     d_aloc_curr_model_builder = true;
 167   }
 168
 169   // Initialize the model
 170   d_eeDistributed->initializeModel(d_curr_model);
 171
 172   // set the core equality engine on quantifiers engine
 173   if (d_logicInfo.isQuantified())
 174   {
 175     d_quantEngine->setMasterEqualityEngine(
 176         d_eeDistributed->getCoreEqualityEngine());
 177   }
 178
 179   // finish initializing the theories
 180   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
 181     Theory* t = d_theoryTable[theoryId];
 182     if (t == nullptr)
 183     {
 184       continue;
 185     }
 186     // setup the pointers to the utilities
 187     const EeTheoryInfo* eeti = d_eeDistributed->getEeTheoryInfo(theoryId);
 188     Assert(eeti != nullptr);
 189     // the theory's official equality engine is the one specified by the
 190     // equality engine manager
 191     t->setEqualityEngine(eeti->d_usedEe);
 192     // set the quantifiers engine
 193     t->setQuantifiersEngine(d_quantEngine);
 194     // set the decision manager for the theory
 195     t->setDecisionManager(d_decManager.get());
 196     // finish initializing the theory
 197     t->finishInit();
 198   }
 199 }
 200
 201 TheoryEngine::TheoryEngine(context::Context* context,
 202                            context::UserContext* userContext,
 203                            ResourceManager* rm,
 204                            RemoveTermFormulas& iteRemover,
 205                            const LogicInfo& logicInfo)
 206     : d_propEngine(nullptr),
 207       d_context(context),
 208       d_userContext(userContext),
 209       d_logicInfo(logicInfo),
 210       d_sharedTerms(this, context),
 211       d_eeDistributed(nullptr),
 212       d_quantEngine(nullptr),
 213       d_decManager(new DecisionManager(userContext)),
 214       d_relManager(nullptr),
 215       d_curr_model(nullptr),
 216       d_aloc_curr_model(false),
 217       d_curr_model_builder(nullptr),
 218       d_aloc_curr_model_builder(false),
 219       d_eager_model_building(false),
 220       d_possiblePropagations(context),
 221       d_hasPropagated(context),
 222       d_inConflict(context, false),
 223       d_inSatMode(false),
 224       d_hasShutDown(false),
 225       d_incomplete(context, false),
 226       d_propagationMap(context),
 227       d_propagationMapTimestamp(context, 0),
 228       d_propagatedLiterals(context),
 229       d_propagatedLiteralsIndex(context, 0),
 230       d_atomRequests(context),
 231       d_tpp(*this, iteRemover),
 232       d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
 233       d_true(),
 234       d_false(),
 235       d_interrupted(false),
 236       d_resourceManager(rm),
 237       d_inPreregister(false),
 238       d_factsAsserted(context, false),
 239       d_preRegistrationVisitor(this, context),
 240       d_sharedTermsVisitor(d_sharedTerms),
 241       d_attr_handle(),
 242       d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
 243 {
 244   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST;
 245       ++ theoryId)
 246   {
 247     d_theoryTable[theoryId] = NULL;
 248     d_theoryOut[theoryId] = NULL;
 249   }
 250
 251   smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime);
 252   d_true = NodeManager::currentNM()->mkConst<bool>(true);
 253   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 254
 255 #ifdef CVC4_PROOF
 256   ProofManager::currentPM()->initTheoryProofEngine();
 257 #endif
 258
 259   smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded);
 260 }
 261
 262 TheoryEngine::~TheoryEngine() {
 263   Assert(d_hasShutDown);
 264
 265   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
 266     if(d_theoryTable[theoryId] != NULL) {
 267       delete d_theoryTable[theoryId];
 268       delete d_theoryOut[theoryId];
 269     }
 270   }
 271
 272   if( d_aloc_curr_model_builder ){
 273     delete d_curr_model_builder;
 274   }
 275   if( d_aloc_curr_model ){
 276     delete d_curr_model;
 277   }
 278
 279   delete d_quantEngine;
 280
 281   smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
 282   smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
 283 }
 284
 285 void TheoryEngine::interrupt() { d_interrupted = true; }
 286 void TheoryEngine::preRegister(TNode preprocessed) {
 287
 288   Debug("theory") << "TheoryEngine::preRegister( " << preprocessed << ")" << std::endl;
 289   if(Dump.isOn("missed-t-propagations")) {
 290     d_possiblePropagations.push_back(preprocessed);
 291   }
 292   d_preregisterQueue.push(preprocessed);
 293
 294   if (!d_inPreregister) {
 295     // We're in pre-register
 296     d_inPreregister = true;
 297
 298     // Process the pre-registration queue
 299     while (!d_preregisterQueue.empty()) {
 300       // Get the next atom to pre-register
 301       preprocessed = d_preregisterQueue.front();
 302       d_preregisterQueue.pop();
 303
 304       if (d_logicInfo.isSharingEnabled() && preprocessed.getKind() == kind::EQUAL) {
 305         // When sharing is enabled, we propagate from the shared terms manager also
 306         d_sharedTerms.addEqualityToPropagate(preprocessed);
 307       }
 308
 309       // the atom should not have free variables
 310       Debug("theory") << "TheoryEngine::preRegister: " << preprocessed
 311                       << std::endl;
 312       Assert(!expr::hasFreeVar(preprocessed));
 313       // Pre-register the terms in the atom
 314       Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
 315       theories = Theory::setRemove(THEORY_BOOL, theories);
 316       // Remove the top theory, if any more that means multiple theories were involved
 317       bool multipleTheories = Theory::setRemove(Theory::theoryOf(preprocessed), theories);
 318       TheoryId i;
 319       // These checks don't work with finite model finding, because it
 320       // uses Rational constants to represent cardinality constraints,
 321       // even though arithmetic isn't actually involved.
 322       if(!options::finiteModelFind()) {
 323         while((i = Theory::setPop(theories)) != THEORY_LAST) {
 324           if(!d_logicInfo.isTheoryEnabled(i)) {
 325             LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy();
 326             newLogicInfo.enableTheory(i);
 327             newLogicInfo.lock();
 328             stringstream ss;
 329             ss << "The logic was specified as " << d_logicInfo.getLogicString()
 330                << ", which doesn't include " << i
 331                << ", but found a term in that theory." << endl
 332                << "You might want to extend your logic to "
 333                << newLogicInfo.getLogicString() << endl;
 334             throw LogicException(ss.str());
 335           }
 336         }
 337       }
 338       if (multipleTheories) {
 339         // Collect the shared terms if there are multiple theories
 340         NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed);
 341       }
 342     }
 343
 344     // Leaving pre-register
 345     d_inPreregister = false;
 346   }
 347 }
 348
 349 void TheoryEngine::printAssertions(const char* tag) {
 350   if (Trace.isOn(tag)) {
 351
 352     for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
 353       Theory* theory = d_theoryTable[theoryId];
 354       if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
 355         Trace(tag) << "--------------------------------------------" << endl;
 356         Trace(tag) << "Assertions of " << theory->getId() << ": " << endl;
 357         {
 358           context::CDList<Assertion>::const_iterator it = theory->facts_begin(),
 359                                                      it_end =
 360                                                          theory->facts_end();
 361           for (unsigned i = 0; it != it_end; ++it, ++i)
 362           {
 363             if ((*it).d_isPreregistered)
 364             {
 365               Trace(tag) << "[" << i << "]: ";
 366             }
 367             else
 368             {
 369               Trace(tag) << "(" << i << "): ";
 370             }
 371             Trace(tag) << (*it).d_assertion << endl;
 372           }
 373         }
 374
 375         if (d_logicInfo.isSharingEnabled()) {
 376           Trace(tag) << "Shared terms of " << theory->getId() << ": " << endl;
 377           context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
 378           for (unsigned i = 0; it != it_end; ++ it, ++i) {
 379               Trace(tag) << "[" << i << "]: " << (*it) << endl;
 380           }
 381         }
 382       }
 383     }
 384   }
 385 }
 386
 387 void TheoryEngine::dumpAssertions(const char* tag) {
 388   if (Dump.isOn(tag)) {
 389     Dump(tag) << CommentCommand("Starting completeness check");
 390     for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
 391       Theory* theory = d_theoryTable[theoryId];
 392       if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
 393         Dump(tag) << CommentCommand("Completeness check");
 394         Dump(tag) << PushCommand();
 395
 396         // Dump the shared terms
 397         if (d_logicInfo.isSharingEnabled()) {
 398           Dump(tag) << CommentCommand("Shared terms");
 399           context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
 400           for (unsigned i = 0; it != it_end; ++ it, ++i) {
 401               stringstream ss;
 402               ss << (*it);
 403               Dump(tag) << CommentCommand(ss.str());
 404           }
 405         }
 406
 407         // Dump the assertions
 408         Dump(tag) << CommentCommand("Assertions");
 409         context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
 410         for (; it != it_end; ++ it) {
 411           // Get the assertion
 412           Node assertionNode = (*it).d_assertion;
 413           // Purify all the terms
 414
 415           if ((*it).d_isPreregistered)
 416           {
 417             Dump(tag) << CommentCommand("Preregistered");
 418           }
 419           else
 420           {
 421             Dump(tag) << CommentCommand("Shared assertion");
 422           }
 423           Dump(tag) << AssertCommand(assertionNode.toExpr());
 424         }
 425         Dump(tag) << CheckSatCommand();
 426
 427         Dump(tag) << PopCommand();
 428       }
 429     }
 430   }
 431 }
 432
 433 /**
 434  * Check all (currently-active) theories for conflicts.
 435  * @param effort the effort level to use
 436  */
 437 void TheoryEngine::check(Theory::Effort effort) {
 438   // spendResource();
 439
 440   // Reset the interrupt flag
 441   d_interrupted = false;
 442
 443 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 444 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 445 #endif
 446 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 447     if (theory::TheoryTraits<THEORY>::hasCheck && d_logicInfo.isTheoryEnabled(THEORY)) { \
 448        theoryOf(THEORY)->check(effort); \
 449        if (d_inConflict) { \
 450          Debug("conflict") << THEORY << " in conflict. " << std::endl; \
 451          break; \
 452        } \
 453     }
 454
 455   // Do the checking
 456   try {
 457
 458     // Mark the output channel unused (if this is FULL_EFFORT, and nothing
 459     // is done by the theories, no additional check will be needed)
 460     d_outputChannelUsed = false;
 461
 462     // Mark the lemmas flag (no lemmas added)
 463     d_lemmasAdded = false;
 464
 465     Debug("theory") << "TheoryEngine::check(" << effort << "): d_factsAsserted = " << (d_factsAsserted ? "true" : "false") << endl;
 466
 467     // If in full effort, we have a fake new assertion just to jumpstart the checking
 468     if (Theory::fullEffort(effort)) {
 469       d_factsAsserted = true;
 470       // Reset round for the relevance manager, which notice only sets a flag
 471       // to indicate that its information must be recomputed.
 472       if (d_relManager != nullptr)
 473       {
 474         d_relManager->resetRound();
 475       }
 476     }
 477
 478     // Check until done
 479     while (d_factsAsserted && !d_inConflict && !d_lemmasAdded) {
 480
 481       Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << endl;
 482
 483       Trace("theory::assertions") << endl;
 484       if (Trace.isOn("theory::assertions")) {
 485         printAssertions("theory::assertions");
 486       }
 487
 488       if(Theory::fullEffort(effort)) {
 489         Trace("theory::assertions::fulleffort") << endl;
 490         if (Trace.isOn("theory::assertions::fulleffort")) {
 491           printAssertions("theory::assertions::fulleffort");
 492         }
 493       }
 494
 495       // Note that we've discharged all the facts
 496       d_factsAsserted = false;
 497
 498       // Do the checking
 499       CVC4_FOR_EACH_THEORY;
 500
 501       if(Dump.isOn("missed-t-conflicts")) {
 502         Dump("missed-t-conflicts")
 503             << CommentCommand("Completeness check for T-conflicts; expect sat")
 504             << CheckSatCommand();
 505       }
 506
 507       Debug("theory") << "TheoryEngine::check(" << effort << "): running propagation after the initial check" << endl;
 508
 509       // We are still satisfiable, propagate as much as possible
 510       propagate(effort);
 511
 512       // We do combination if all has been processed and we are in fullcheck
 513       if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() && !d_factsAsserted && !d_lemmasAdded && !d_inConflict) {
 514         // Do the combination
 515         Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << endl;
 516         combineTheories();
 517         if(d_logicInfo.isQuantified()){
 518           d_quantEngine->notifyCombineTheories();
 519         }
 520       }
 521     }
 522
 523     // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
 524     if( Theory::fullEffort(effort) && ! d_inConflict && ! needCheck() ) {
 525       Trace("theory::assertions-model") << endl;
 526       if (Trace.isOn("theory::assertions-model")) {
 527         printAssertions("theory::assertions-model");
 528       }
 529       //checks for theories requiring the model go at last call
 530       d_curr_model->reset();
 531       // !!! temporary, will be part of distributed model manager
 532       context::Context* meec = d_eeDistributed->getModelEqualityEngineContext();
 533       meec->pop();
 534       meec->push();
 535       for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
 536         if( theoryId!=THEORY_QUANTIFIERS ){
 537           Theory* theory = d_theoryTable[theoryId];
 538           if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
 539             if( theory->needsCheckLastEffort() ){
 540               if( !d_curr_model->isBuilt() ){
 541                 if( !d_curr_model_builder->buildModel(d_curr_model) ){
 542                   break;
 543                 }
 544               }
 545               theory->check(Theory::EFFORT_LAST_CALL);
 546             }
 547           }
 548         }
 549       }
 550       if (!d_inConflict)
 551       {
 552         if(d_logicInfo.isQuantified()) {
 553           // quantifiers engine must check at last call effort
 554           d_quantEngine->check(Theory::EFFORT_LAST_CALL);
 555         }
 556       }
 557       if (!d_inConflict && !needCheck())
 558       {
 559         // If d_eager_model_building is false, then we only mark that we
 560         // are in "SAT mode". We build the model later only if the user asks
 561         // for it via getBuiltModel.
 562         d_inSatMode = true;
 563         if (d_eager_model_building && !d_curr_model->isBuilt())
 564         {
 565           d_curr_model_builder->buildModel(d_curr_model);
 566         }
 567       }
 568     }
 569
 570     Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas");
 571     Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl;
 572
 573     if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) {
 574       // case where we are about to answer SAT, the master equality engine,
 575       // if it exists, must be consistent.
 576       eq::EqualityEngine* mee = d_eeDistributed->getCoreEqualityEngine();
 577       if (mee != NULL)
 578       {
 579         AlwaysAssert(mee->consistent());
 580       }
 581       if (d_curr_model->isBuilt())
 582       {
 583         // model construction should always succeed unless lemmas were added
 584         AlwaysAssert(d_curr_model->isBuiltSuccess());
 585         if (options::produceModels())
 586         {
 587           // Do post-processing of model from the theories (used for THEORY_SEP
 588           // to construct heap model)
 589           postProcessModel(d_curr_model);
 590           // also call the model builder's post-process model
 591           d_curr_model_builder->postProcessModel(d_incomplete.get(),
 592                                                  d_curr_model);
 593         }
 594       }
 595     }
 596   } catch(const theory::Interrupted&) {
 597     Trace("theory") << "TheoryEngine::check() => interrupted" << endl;
 598   }
 599   // If fulleffort, check all theories
 600   if(Dump.isOn("theory::fullcheck") && Theory::fullEffort(effort)) {
 601     if (!d_inConflict && !needCheck()) {
 602       dumpAssertions("theory::fullcheck");
 603     }
 604   }
 605 }
 606
 607 void TheoryEngine::combineTheories() {
 608
 609   Trace("combineTheories") << "TheoryEngine::combineTheories()" << endl;
 610
 611   TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime);
 612
 613   // Care graph we'll be building
 614   CareGraph careGraph;
 615
 616 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 617 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 618 #endif
 619 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 620   if (theory::TheoryTraits<THEORY>::isParametric && d_logicInfo.isTheoryEnabled(THEORY)) { \
 621     theoryOf(THEORY)->getCareGraph(&careGraph); \
 622   }
 623
 624   // Call on each parametric theory to give us its care graph
 625   CVC4_FOR_EACH_THEORY;
 626
 627   Trace("combineTheories") << "TheoryEngine::combineTheories(): care graph size = " << careGraph.size() << endl;
 628
 629   // Now add splitters for the ones we are interested in
 630   CareGraph::const_iterator care_it = careGraph.begin();
 631   CareGraph::const_iterator care_it_end = careGraph.end();
 632
 633   for (; care_it != care_it_end; ++ care_it) {
 634     const CarePair& carePair = *care_it;
 635
 636     Debug("combineTheories")
 637         << "TheoryEngine::combineTheories(): checking " << carePair.d_a << " = "
 638         << carePair.d_b << " from " << carePair.d_theory << endl;
 639
 640     Assert(d_sharedTerms.isShared(carePair.d_a) || carePair.d_a.isConst());
 641     Assert(d_sharedTerms.isShared(carePair.d_b) || carePair.d_b.isConst());
 642
 643     // The equality in question (order for no repetition)
 644     Node equality = carePair.d_a.eqNode(carePair.d_b);
 645     // EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b);
 646     // Debug("combineTheories") << "TheoryEngine::combineTheories(): " <<
 647     //   (es == EQUALITY_TRUE_AND_PROPAGATED ? "EQUALITY_TRUE_AND_PROPAGATED" :
 648     //   es == EQUALITY_FALSE_AND_PROPAGATED ? "EQUALITY_FALSE_AND_PROPAGATED" :
 649     //   es == EQUALITY_TRUE ? "EQUALITY_TRUE" :
 650     //   es == EQUALITY_FALSE ? "EQUALITY_FALSE" :
 651     //   es == EQUALITY_TRUE_IN_MODEL ? "EQUALITY_TRUE_IN_MODEL" :
 652     //   es == EQUALITY_FALSE_IN_MODEL ? "EQUALITY_FALSE_IN_MODEL" :
 653     //   es == EQUALITY_UNKNOWN ? "EQUALITY_UNKNOWN" :
 654     //    "Unexpected case") << endl;
 655
 656     // We need to split on it
 657     Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl;
 658
 659     lemma(equality.orNode(equality.notNode()),
 660           RULE_INVALID,
 661           false,
 662           LemmaProperty::NONE,
 663           carePair.d_theory);
 664
 665     // This code is supposed to force preference to follow what the theory models already have
 666     // but it doesn't seem to make a big difference - need to explore more -Clark
 667     // if (true) {
 668     //   if (es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL) {
 669     Node e = ensureLiteral(equality);
 670     d_propEngine->requirePhase(e, true);
 671     //   }
 672     //   else if (es == EQUALITY_FALSE_IN_MODEL) {
 673     //     Node e = ensureLiteral(equality);
 674     //     d_propEngine->requirePhase(e, false);
 675     //   }
 676     // }
 677   }
 678 }
 679
 680 void TheoryEngine::propagate(Theory::Effort effort) {
 681   // Reset the interrupt flag
 682   d_interrupted = false;
 683
 684   // Definition of the statement that is to be run by every theory
 685 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 686 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 687 #endif
 688 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 689   if (theory::TheoryTraits<THEORY>::hasPropagate && d_logicInfo.isTheoryEnabled(THEORY)) { \
 690     theoryOf(THEORY)->propagate(effort); \
 691   }
 692
 693   // Reset the interrupt flag
 694   d_interrupted = false;
 695
 696   // Propagate for each theory using the statement above
 697   CVC4_FOR_EACH_THEORY;
 698
 699   if(Dump.isOn("missed-t-propagations")) {
 700     for(unsigned i = 0; i < d_possiblePropagations.size(); ++i) {
 701       Node atom = d_possiblePropagations[i];
 702       bool value;
 703       if(d_propEngine->hasValue(atom, value)) {
 704         continue;
 705       }
 706       // Doesn't have a value, check it (and the negation)
 707       if(d_hasPropagated.find(atom) == d_hasPropagated.end()) {
 708         Dump("missed-t-propagations")
 709           << CommentCommand("Completeness check for T-propagations; expect invalid")
 710           << EchoCommand(atom.toString())
 711           << QueryCommand(atom.toExpr())
 712           << EchoCommand(atom.notNode().toString())
 713           << QueryCommand(atom.notNode().toExpr());
 714       }
 715     }
 716   }
 717 }
 718
 719 Node TheoryEngine::getNextDecisionRequest()
 720 {
 721   return d_decManager->getNextDecisionRequest();
 722 }
 723
 724 bool TheoryEngine::properConflict(TNode conflict) const {
 725   bool value;
 726   if (conflict.getKind() == kind::AND) {
 727     for (unsigned i = 0; i < conflict.getNumChildren(); ++ i) {
 728       if (! getPropEngine()->hasValue(conflict[i], value)) {
 729         Debug("properConflict") << "Bad conflict is due to unassigned atom: "
 730                                 << conflict[i] << endl;
 731         return false;
 732       }
 733       if (! value) {
 734         Debug("properConflict") << "Bad conflict is due to false atom: "
 735                                 << conflict[i] << endl;
 736         return false;
 737       }
 738       if (conflict[i] != Rewriter::rewrite(conflict[i])) {
 739         Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
 740                                 << conflict[i] << " vs " << Rewriter::rewrite(conflict[i]) << endl;
 741         return false;
 742       }
 743     }
 744   } else {
 745     if (! getPropEngine()->hasValue(conflict, value)) {
 746       Debug("properConflict") << "Bad conflict is due to unassigned atom: "
 747                               << conflict << endl;
 748       return false;
 749     }
 750     if(! value) {
 751       Debug("properConflict") << "Bad conflict is due to false atom: "
 752                               << conflict << endl;
 753       return false;
 754     }
 755     if (conflict != Rewriter::rewrite(conflict)) {
 756       Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
 757                               << conflict << " vs " << Rewriter::rewrite(conflict) << endl;
 758       return false;
 759     }
 760   }
 761   return true;
 762 }
 763
 764 bool TheoryEngine::properPropagation(TNode lit) const {
 765   if(!getPropEngine()->isSatLiteral(lit)) {
 766     return false;
 767   }
 768   bool b;
 769   return !getPropEngine()->hasValue(lit, b);
 770 }
 771
 772 bool TheoryEngine::properExplanation(TNode node, TNode expl) const {
 773   // Explanation must be either a conjunction of true literals that have true SAT values already
 774   // or a singled literal that has a true SAT value already.
 775   if (expl.getKind() == kind::AND) {
 776     for (unsigned i = 0; i < expl.getNumChildren(); ++ i) {
 777       bool value;
 778       if (!d_propEngine->hasValue(expl[i], value) || !value) {
 779         return false;
 780       }
 781     }
 782   } else {
 783     bool value;
 784     return d_propEngine->hasValue(expl, value) && value;
 785   }
 786   return true;
 787 }
 788
 789 bool TheoryEngine::collectModelInfo(theory::TheoryModel* m)
 790 {
 791   //have shared term engine collectModelInfo
 792   //  d_sharedTerms.collectModelInfo( m );
 793   // Consult each active theory to get all relevant information
 794   // concerning the model.
 795   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
 796     if(d_logicInfo.isTheoryEnabled(theoryId)) {
 797       Trace("model-builder") << "  CollectModelInfo on theory: " << theoryId << endl;
 798       if (!d_theoryTable[theoryId]->collectModelInfo(m))
 799       {
 800         return false;
 801       }
 802     }
 803   }
 804   Trace("model-builder") << "  CollectModelInfo boolean variables" << std::endl;
 805   // Get the Boolean variables
 806   vector<TNode> boolVars;
 807   d_propEngine->getBooleanVariables(boolVars);
 808   vector<TNode>::iterator it, iend = boolVars.end();
 809   bool hasValue, value;
 810   for (it = boolVars.begin(); it != iend; ++it) {
 811     TNode var = *it;
 812     hasValue = d_propEngine->hasValue(var, value);
 813     // TODO: Assert that hasValue is true?
 814     if (!hasValue) {
 815       Trace("model-builder-assertions")
 816           << "    has no value : " << var << std::endl;
 817       value = false;
 818     }
 819     Trace("model-builder-assertions") << "(assert" << (value ? " " : " (not ") << var << (value ? ");" : "));") << endl;
 820     if (!m->assertPredicate(var, value))
 821     {
 822       return false;
 823     }
 824   }
 825   return true;
 826 }
 827
 828 void TheoryEngine::postProcessModel( theory::TheoryModel* m ){
 829   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
 830     if(d_logicInfo.isTheoryEnabled(theoryId)) {
 831       Trace("model-builder-debug") << "  PostProcessModel on theory: " << theoryId << endl;
 832       d_theoryTable[theoryId]->postProcessModel( m );
 833     }
 834   }
 835 }
 836
 837 TheoryModel* TheoryEngine::getModel() {
 838   return d_curr_model;
 839 }
 840
 841 TheoryModel* TheoryEngine::getBuiltModel()
 842 {
 843   if (!d_curr_model->isBuilt())
 844   {
 845     // If this method was called, we should be in SAT mode, and produceModels
 846     // should be true.
 847     AlwaysAssert(options::produceModels());
 848     if (!d_inSatMode)
 849     {
 850       // not available, perhaps due to interuption.
 851       return nullptr;
 852     }
 853     // must build model at this point
 854     d_curr_model_builder->buildModel(d_curr_model);
 855   }
 856   return d_curr_model;
 857 }
 858
 859 bool TheoryEngine::getSynthSolutions(
 860     std::map<Node, std::map<Node, Node>>& sol_map)
 861 {
 862   if (d_quantEngine)
 863   {
 864     return d_quantEngine->getSynthSolutions(sol_map);
 865   }
 866   // we are not in a quantified logic, there is no synthesis solution
 867   return false;
 868 }
 869
 870 bool TheoryEngine::presolve() {
 871   // Reset the interrupt flag
 872   d_interrupted = false;
 873
 874   // Reset the decision manager. This clears its decision strategies that are
 875   // no longer valid in this user context.
 876   d_decManager->presolve();
 877
 878   try {
 879     // Definition of the statement that is to be run by every theory
 880 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 881 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 882 #endif
 883 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 884     if (theory::TheoryTraits<THEORY>::hasPresolve) {    \
 885       theoryOf(THEORY)->presolve(); \
 886       if(d_inConflict) { \
 887         return true; \
 888       } \
 889     }
 890
 891     // Presolve for each theory using the statement above
 892     CVC4_FOR_EACH_THEORY;
 893   } catch(const theory::Interrupted&) {
 894     Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl;
 895   }
 896   // return whether we have a conflict
 897   return false;
 898 }/* TheoryEngine::presolve() */
 899
 900 void TheoryEngine::postsolve() {
 901   // no longer in SAT mode
 902   d_inSatMode = false;
 903   // Reset the interrupt flag
 904   d_interrupted = false;
 905   bool CVC4_UNUSED wasInConflict = d_inConflict;
 906
 907   try {
 908     // Definition of the statement that is to be run by every theory
 909 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 910 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 911 #endif
 912 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY)    \
 913   if (theory::TheoryTraits<THEORY>::hasPostsolve) \
 914   {                                               \
 915     theoryOf(THEORY)->postsolve();                \
 916     Assert(!d_inConflict || wasInConflict)        \
 917         << "conflict raised during postsolve()";  \
 918   }
 919
 920     // Postsolve for each theory using the statement above
 921     CVC4_FOR_EACH_THEORY;
 922   } catch(const theory::Interrupted&) {
 923     Trace("theory") << "TheoryEngine::postsolve() => interrupted" << endl;
 924   }
 925 }/* TheoryEngine::postsolve() */
 926
 927
 928 void TheoryEngine::notifyRestart() {
 929   // Reset the interrupt flag
 930   d_interrupted = false;
 931
 932   // Definition of the statement that is to be run by every theory
 933 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 934 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 935 #endif
 936 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 937   if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_logicInfo.isTheoryEnabled(THEORY)) { \
 938     theoryOf(THEORY)->notifyRestart(); \
 939   }
 940
 941   // notify each theory using the statement above
 942   CVC4_FOR_EACH_THEORY;
 943 }
 944
 945 void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
 946   // Reset the interrupt flag
 947   d_interrupted = false;
 948
 949   // Definition of the statement that is to be run by every theory
 950 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 951 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 952 #endif
 953 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 954   if (theory::TheoryTraits<THEORY>::hasPpStaticLearn) { \
 955     theoryOf(THEORY)->ppStaticLearn(in, learned); \
 956   }
 957
 958   // static learning for each theory using the statement above
 959   CVC4_FOR_EACH_THEORY;
 960 }
 961
 962 bool TheoryEngine::isRelevant(Node lit) const
 963 {
 964   if (d_relManager != nullptr)
 965   {
 966     return d_relManager->isRelevant(lit);
 967   }
 968   // otherwise must assume its relevant
 969   return true;
 970 }
 971
 972 void TheoryEngine::shutdown() {
 973   // Set this first; if a Theory shutdown() throws an exception,
 974   // at least the destruction of the TheoryEngine won't confound
 975   // matters.
 976   d_hasShutDown = true;
 977
 978   // Shutdown all the theories
 979   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
 980     if(d_theoryTable[theoryId]) {
 981       theoryOf(theoryId)->shutdown();
 982     }
 983   }
 984
 985   d_tpp.clearCache();
 986 }
 987
 988 theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) {
 989   // Reset the interrupt flag
 990   d_interrupted = false;
 991
 992   TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
 993   Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
 994
 995   if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(atom)) &&
 996      Theory::theoryOf(atom) != THEORY_SAT_SOLVER) {
 997     stringstream ss;
 998     ss << "The logic was specified as " << d_logicInfo.getLogicString()
 999        << ", which doesn't include " << Theory::theoryOf(atom)
1000        << ", but got a preprocessing-time fact for that theory." << endl
1001        << "The fact:" << endl
1002        << literal;
1003     throw LogicException(ss.str());
1004   }
1005
1006   Theory::PPAssertStatus solveStatus = theoryOf(atom)->ppAssert(literal, substitutionOut);
1007   Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl;
1008   return solveStatus;
1009 }
1010
1011 void TheoryEngine::preprocessStart() { d_tpp.clearCache(); }
1012
1013 Node TheoryEngine::preprocess(TNode assertion) {
1014   TrustNode trn = d_tpp.theoryPreprocess(assertion);
1015   if (trn.isNull())
1016   {
1017     // no change
1018     return assertion;
1019   }
1020   return trn.getNode();
1021 }
1022
1023 void TheoryEngine::notifyPreprocessedAssertions(
1024     const std::vector<Node>& assertions) {
1025   // call all the theories
1026   for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
1027        ++theoryId) {
1028     if (d_theoryTable[theoryId]) {
1029       theoryOf(theoryId)->ppNotifyAssertions(assertions);
1030     }
1031   }
1032   if (d_relManager != nullptr)
1033   {
1034     d_relManager->notifyPreprocessedAssertions(assertions);
1035   }
1036 }
1037
1038 bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
1039
1040   // What and where we are asserting
1041   NodeTheoryPair toAssert(assertion, toTheoryId, d_propagationMapTimestamp);
1042   // What and where it came from
1043   NodeTheoryPair toExplain(originalAssertion, fromTheoryId, d_propagationMapTimestamp);
1044
1045   // See if the theory already got this literal
1046   PropagationMap::const_iterator find = d_propagationMap.find(toAssert);
1047   if (find != d_propagationMap.end()) {
1048     // The theory already knows this
1049     Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): already there" << endl;
1050     return false;
1051   }
1052
1053   Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): marking [" << d_propagationMapTimestamp << "] " << assertion << ", " << toTheoryId << " from " << originalAssertion << ", " << fromTheoryId << endl;
1054
1055   // Mark the propagation
1056   d_propagationMap[toAssert] = toExplain;
1057   d_propagationMapTimestamp = d_propagationMapTimestamp + 1;
1058
1059   return true;
1060 }
1061
1062
1063 void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
1064
1065   Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << originalAssertion << "," << toTheoryId << ", " << fromTheoryId << ")" << endl;
1066
1067   Assert(toTheoryId != fromTheoryId);
1068   if(toTheoryId != THEORY_SAT_SOLVER &&
1069      ! d_logicInfo.isTheoryEnabled(toTheoryId)) {
1070     stringstream ss;
1071     ss << "The logic was specified as " << d_logicInfo.getLogicString()
1072        << ", which doesn't include " << toTheoryId
1073        << ", but got an asserted fact to that theory." << endl
1074        << "The fact:" << endl
1075        << assertion;
1076     throw LogicException(ss.str());
1077   }
1078
1079   if (d_inConflict) {
1080     return;
1081   }
1082
1083   // If sharing is disabled, things are easy
1084   if (!d_logicInfo.isSharingEnabled()) {
1085     Assert(assertion == originalAssertion);
1086     if (fromTheoryId == THEORY_SAT_SOLVER) {
1087       // Send to the apropriate theory
1088       theory::Theory* toTheory = theoryOf(toTheoryId);
1089       // We assert it, and we know it's preregistereed
1090       toTheory->assertFact(assertion, true);
1091       // Mark that we have more information
1092       d_factsAsserted = true;
1093     } else {
1094       Assert(toTheoryId == THEORY_SAT_SOLVER);
1095       // Check for propositional conflict
1096       bool value;
1097       if (d_propEngine->hasValue(assertion, value)) {
1098         if (!value) {
1099           Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (no sharing)" << endl;
1100           Trace("dtview::conflict")
1101               << ":THEORY-CONFLICT: " << assertion << std::endl;
1102           d_inConflict = true;
1103         } else {
1104           return;
1105         }
1106       }
1107       d_propagatedLiterals.push_back(assertion);
1108     }
1109     return;
1110   }
1111
1112   // Polarity of the assertion
1113   bool polarity = assertion.getKind() != kind::NOT;
1114
1115   // Atom of the assertion
1116   TNode atom = polarity ? assertion : assertion[0];
1117
1118   // If sending to the shared terms database, it's also simple
1119   if (toTheoryId == THEORY_BUILTIN) {
1120     Assert(atom.getKind() == kind::EQUAL)
1121         << "atom should be an EQUALity, not `" << atom << "'";
1122     if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
1123       d_sharedTerms.assertEquality(atom, polarity, assertion);
1124     }
1125     return;
1126   }
1127
1128   // Things from the SAT solver are already normalized, so they go
1129   // directly to the apropriate theory
1130   if (fromTheoryId == THEORY_SAT_SOLVER) {
1131     // We know that this is normalized, so just send it off to the theory
1132     if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
1133       // Is it preregistered
1134       bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
1135       // We assert it
1136       theoryOf(toTheoryId)->assertFact(assertion, preregistered);
1137       // Mark that we have more information
1138       d_factsAsserted = true;
1139     }
1140     return;
1141   }
1142
1143   // Propagations to the SAT solver are just enqueued for pickup by
1144   // the SAT solver later
1145   if (toTheoryId == THEORY_SAT_SOLVER) {
1146     if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
1147       // Enqueue for propagation to the SAT solver
1148       d_propagatedLiterals.push_back(assertion);
1149       // Check for propositional conflicts
1150       bool value;
1151       if (d_propEngine->hasValue(assertion, value) && !value) {
1152         Trace("theory::propagate")
1153             << "TheoryEngine::assertToTheory(" << assertion << ", "
1154             << toTheoryId << ", " << fromTheoryId << "): conflict (sharing)"
1155             << endl;
1156         Trace("dtview::conflict")
1157             << ":THEORY-CONFLICT: " << assertion << std::endl;
1158         d_inConflict = true;
1159       }
1160     }
1161     return;
1162   }
1163
1164   Assert(atom.getKind() == kind::EQUAL);
1165
1166   // Normalize
1167   Node normalizedLiteral = Rewriter::rewrite(assertion);
1168
1169   // See if it rewrites false directly -> conflict
1170   if (normalizedLiteral.isConst()) {
1171     if (!normalizedLiteral.getConst<bool>()) {
1172       // Mark the propagation for explanations
1173       if (markPropagation(normalizedLiteral, originalAssertion, toTheoryId, fromTheoryId)) {
1174         // Get the explanation (conflict will figure out where it came from)
1175         conflict(normalizedLiteral, toTheoryId);
1176       } else {
1177         Unreachable();
1178       }
1179       return;
1180     }
1181   }
1182
1183   // Try and assert (note that we assert the non-normalized one)
1184   if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
1185     // Check if has been pre-registered with the theory
1186     bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
1187     // Assert away
1188     theoryOf(toTheoryId)->assertFact(assertion, preregistered);
1189     d_factsAsserted = true;
1190   }
1191
1192   return;
1193 }
1194
1195 void TheoryEngine::assertFact(TNode literal)
1196 {
1197   Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << endl;
1198
1199   // spendResource();
1200
1201   // If we're in conflict, nothing to do
1202   if (d_inConflict) {
1203     return;
1204   }
1205
1206   // Get the atom
1207   bool polarity = literal.getKind() != kind::NOT;
1208   TNode atom = polarity ? literal : literal[0];
1209
1210   if (d_logicInfo.isSharingEnabled()) {
1211
1212     // If any shared terms, it's time to do sharing work
1213     if (d_sharedTerms.hasSharedTerms(atom)) {
1214       // Notify the theories the shared terms
1215       SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom);
1216       SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom);
1217       for (; it != it_end; ++ it) {
1218         TNode term = *it;
1219         Theory::Set theories = d_sharedTerms.getTheoriesToNotify(atom, term);
1220         for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++ id) {
1221           if (Theory::setContains(id, theories)) {
1222             theoryOf(id)->addSharedTerm(term);
1223           }
1224         }
1225         d_sharedTerms.markNotified(term, theories);
1226       }
1227     }
1228
1229     // If it's an equality, assert it to the shared term manager, even though the terms are not
1230     // yet shared. As the terms become shared later, the shared terms manager will then add them
1231     // to the assert the equality to the interested theories
1232     if (atom.getKind() == kind::EQUAL) {
1233       // Assert it to the the owning theory
1234       assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
1235       // Shared terms manager will assert to interested theories directly, as the terms become shared
1236       assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ THEORY_SAT_SOLVER);
1237
1238       // Now, let's check for any atom triggers from lemmas
1239       AtomRequests::atom_iterator it = d_atomRequests.getAtomIterator(atom);
1240       while (!it.done()) {
1241         const AtomRequests::Request& request = it.get();
1242         Node toAssert =
1243             polarity ? (Node)request.d_atom : request.d_atom.notNode();
1244         Debug("theory::atoms") << "TheoryEngine::assertFact(" << literal << "): sending requested " << toAssert << endl;
1245         assertToTheory(
1246             toAssert, literal, request.d_toTheory, THEORY_SAT_SOLVER);
1247         it.next();
1248       }
1249
1250     } else {
1251       // Not an equality, just assert to the appropriate theory
1252       assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
1253     }
1254   } else {
1255     // Assert the fact to the appropriate theory directly
1256     assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
1257   }
1258 }
1259
1260 bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
1261
1262   Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl;
1263
1264   Trace("dtview::prop") << std::string(d_context->getLevel(), ' ')
1265                         << ":THEORY-PROP: " << literal << endl;
1266
1267   // spendResource();
1268
1269   if(Dump.isOn("t-propagations")) {
1270     Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid")
1271                            << QueryCommand(literal.toExpr());
1272   }
1273   if(Dump.isOn("missed-t-propagations")) {
1274     d_hasPropagated.insert(literal);
1275   }
1276
1277   // Get the atom
1278   bool polarity = literal.getKind() != kind::NOT;
1279   TNode atom = polarity ? literal : literal[0];
1280
1281   if (d_logicInfo.isSharingEnabled() && atom.getKind() == kind::EQUAL) {
1282     if (d_propEngine->isSatLiteral(literal)) {
1283       // We propagate SAT literals to SAT
1284       assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
1285     }
1286     if (theory != THEORY_BUILTIN) {
1287       // Assert to the shared terms database
1288       assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory);
1289     }
1290   } else {
1291     // We could be propagating a unit-clause lemma. In this case, we need to provide a
1292     // recipe.
1293     // TODO: Consider putting this someplace else? This is the only refence to the proof
1294     // manager in this class.
1295
1296     PROOF({
1297         LemmaProofRecipe proofRecipe;
1298         proofRecipe.addBaseAssertion(literal);
1299
1300         Node emptyNode;
1301         LemmaProofRecipe::ProofStep proofStep(theory, emptyNode);
1302         proofStep.addAssertion(literal);
1303         proofRecipe.addStep(proofStep);
1304
1305         ProofManager::getCnfProof()->setProofRecipe(&proofRecipe);
1306       });
1307
1308     // Just send off to the SAT solver
1309     Assert(d_propEngine->isSatLiteral(literal));
1310     assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
1311   }
1312
1313   return !d_inConflict;
1314 }
1315
1316 const LogicInfo& TheoryEngine::getLogicInfo() const { return d_logicInfo; }
1317
1318 theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
1319   Assert(a.getType().isComparableTo(b.getType()));
1320   if (d_sharedTerms.isShared(a) && d_sharedTerms.isShared(b)) {
1321     if (d_sharedTerms.areEqual(a,b)) {
1322       return EQUALITY_TRUE_AND_PROPAGATED;
1323     }
1324     else if (d_sharedTerms.areDisequal(a,b)) {
1325       return EQUALITY_FALSE_AND_PROPAGATED;
1326     }
1327   }
1328   return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
1329 }
1330
1331 Node TheoryEngine::getModelValue(TNode var) {
1332   if (var.isConst())
1333   {
1334     // the model value of a constant must be itself
1335     return var;
1336   }
1337   Assert(d_sharedTerms.isShared(var));
1338   return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
1339 }
1340
1341
1342 Node TheoryEngine::ensureLiteral(TNode n) {
1343   Debug("ensureLiteral") << "rewriting: " << n << std::endl;
1344   Node rewritten = Rewriter::rewrite(n);
1345   Debug("ensureLiteral") << "      got: " << rewritten << std::endl;
1346   Node preprocessed = preprocess(rewritten);
1347   Debug("ensureLiteral") << "preprocessed: " << preprocessed << std::endl;
1348   d_propEngine->ensureLiteral(preprocessed);
1349   return preprocessed;
1350 }
1351
1352
1353 void TheoryEngine::printInstantiations( std::ostream& out ) {
1354   if( d_quantEngine ){
1355     d_quantEngine->printInstantiations( out );
1356   }else{
1357     out << "Internal error : instantiations not available when quantifiers are not present." << std::endl;
1358     Assert(false);
1359   }
1360 }
1361
1362 void TheoryEngine::printSynthSolution( std::ostream& out ) {
1363   if( d_quantEngine ){
1364     d_quantEngine->printSynthSolution( out );
1365   }else{
1366     out << "Internal error : synth solution not available when quantifiers are not present." << std::endl;
1367     Assert(false);
1368   }
1369 }
1370
1371 void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
1372   if( d_quantEngine ){
1373     d_quantEngine->getInstantiatedQuantifiedFormulas( qs );
1374   }else{
1375     Assert(false);
1376   }
1377 }
1378
1379 void TheoryEngine::getInstantiations( Node q, std::vector< Node >& insts ) {
1380   if( d_quantEngine ){
1381     d_quantEngine->getInstantiations( q, insts );
1382   }else{
1383     Assert(false);
1384   }
1385 }
1386
1387 void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
1388   if( d_quantEngine ){
1389     d_quantEngine->getInstantiationTermVectors( q, tvecs );
1390   }else{
1391     Assert(false);
1392   }
1393 }
1394
1395 void TheoryEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
1396   if( d_quantEngine ){
1397     d_quantEngine->getInstantiations( insts );
1398   }else{
1399     Assert(false);
1400   }
1401 }
1402
1403 void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
1404   if( d_quantEngine ){
1405     d_quantEngine->getInstantiationTermVectors( insts );
1406   }else{
1407     Assert(false);
1408   }
1409 }
1410
1411 Node TheoryEngine::getInstantiatedConjunction( Node q ) {
1412   if( d_quantEngine ){
1413     return d_quantEngine->getInstantiatedConjunction( q );
1414   }else{
1415     Assert(false);
1416     return Node::null();
1417   }
1418 }
1419
1420
1421 static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
1422
1423   std::set<TNode> all;
1424   for (unsigned i = 0; i < explanation.size(); ++ i) {
1425     Assert(explanation[i].d_theory == THEORY_SAT_SOLVER);
1426     all.insert(explanation[i].d_node);
1427   }
1428
1429   if (all.size() == 0) {
1430     // Normalize to true
1431     return NodeManager::currentNM()->mkConst<bool>(true);
1432   }
1433
1434   if (all.size() == 1) {
1435     // All the same, or just one
1436     return explanation[0].d_node;
1437   }
1438
1439   NodeBuilder<> conjunction(kind::AND);
1440   std::set<TNode>::const_iterator it = all.begin();
1441   std::set<TNode>::const_iterator it_end = all.end();
1442   while (it != it_end) {
1443     conjunction << *it;
1444     ++ it;
1445   }
1446
1447   return conjunction;
1448 }
1449
1450 Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe) {
1451   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << endl;
1452
1453   bool polarity = node.getKind() != kind::NOT;
1454   TNode atom = polarity ? node : node[0];
1455
1456   // If we're not in shared mode, explanations are simple
1457   if (!d_logicInfo.isSharingEnabled()) {
1458     Debug("theory::explain") << "TheoryEngine::getExplanation: sharing is NOT enabled. "
1459                              << " Responsible theory is: "
1460                              << theoryOf(atom)->getId() << std::endl;
1461
1462     TrustNode texplanation = theoryOf(atom)->explain(node);
1463     Node explanation = texplanation.getNode();
1464     Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
1465     PROOF({
1466         if(proofRecipe) {
1467           Node emptyNode;
1468           LemmaProofRecipe::ProofStep proofStep(theoryOf(atom)->getId(), emptyNode);
1469           proofStep.addAssertion(node);
1470           proofRecipe->addBaseAssertion(node);
1471
1472           if (explanation.getKind() == kind::AND) {
1473             // If the explanation is a conjunction, the recipe for the corresponding lemma is
1474             // the negation of its conjuncts.
1475             Node flat = flattenAnd(explanation);
1476             for (unsigned i = 0; i < flat.getNumChildren(); ++i) {
1477               if (flat[i].isConst() && flat[i].getConst<bool>()) {
1478                 ++ i;
1479                 continue;
1480               }
1481               if (flat[i].getKind() == kind::NOT &&
1482                   flat[i][0].isConst() && !flat[i][0].getConst<bool>()) {
1483                 ++ i;
1484                 continue;
1485               }
1486               Debug("theory::explain") << "TheoryEngine::getExplanationAndRecipe: adding recipe assertion: "
1487                                        << flat[i].negate() << std::endl;
1488               proofStep.addAssertion(flat[i].negate());
1489               proofRecipe->addBaseAssertion(flat[i].negate());
1490             }
1491           } else {
1492             // The recipe for proving it is by negating it. "True" is not an acceptable reason.
1493             if (!((explanation.isConst() && explanation.getConst<bool>()) ||
1494                   (explanation.getKind() == kind::NOT &&
1495                    explanation[0].isConst() && !explanation[0].getConst<bool>()))) {
1496               proofStep.addAssertion(explanation.negate());
1497               proofRecipe->addBaseAssertion(explanation.negate());
1498             }
1499           }
1500
1501           proofRecipe->addStep(proofStep);
1502         }
1503       });
1504
1505     return explanation;
1506   }
1507
1508   Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled" << std::endl;
1509
1510   // Initial thing to explain
1511   NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp);
1512   Assert(d_propagationMap.find(toExplain) != d_propagationMap.end());
1513
1514   NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain];
1515   Debug("theory::explain")
1516       << "TheoryEngine::getExplanation: explainer for node "
1517       << nodeExplainerPair.d_node
1518       << " is theory: " << nodeExplainerPair.d_theory << std::endl;
1519   TheoryId explainer = nodeExplainerPair.d_theory;
1520
1521   // Create the workplace for explanations
1522   std::vector<NodeTheoryPair> explanationVector;
1523   explanationVector.push_back(d_propagationMap[toExplain]);
1524   // Process the explanation
1525   if (proofRecipe) {
1526     Node emptyNode;
1527     LemmaProofRecipe::ProofStep proofStep(explainer, emptyNode);
1528     proofStep.addAssertion(node);
1529     proofRecipe->addStep(proofStep);
1530     proofRecipe->addBaseAssertion(node);
1531   }
1532
1533   getExplanation(explanationVector, proofRecipe);
1534   Node explanation = mkExplanation(explanationVector);
1535
1536   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
1537
1538   return explanation;
1539 }
1540
1541 Node TheoryEngine::getExplanation(TNode node) {
1542   LemmaProofRecipe *dontCareRecipe = NULL;
1543   return getExplanationAndRecipe(node, dontCareRecipe);
1544 }
1545
1546 struct AtomsCollect {
1547
1548   std::vector<TNode> d_atoms;
1549   std::unordered_set<TNode, TNodeHashFunction> d_visited;
1550
1551 public:
1552
1553   typedef void return_type;
1554
1555   bool alreadyVisited(TNode current, TNode parent) {
1556     // Check if already visited
1557     if (d_visited.find(current) != d_visited.end()) return true;
1558     // Don't visit non-boolean
1559     if (!current.getType().isBoolean()) return true;
1560     // New node
1561     return false;
1562   }
1563
1564   void visit(TNode current, TNode parent) {
1565     if (Theory::theoryOf(current) != theory::THEORY_BOOL) {
1566       d_atoms.push_back(current);
1567     }
1568     d_visited.insert(current);
1569   }
1570
1571   void start(TNode node) {}
1572   void done(TNode node) {}
1573
1574   std::vector<TNode> getAtoms() const {
1575     return d_atoms;
1576   }
1577 };
1578
1579 void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId atomsTo) {
1580   for (unsigned i = 0; i < atoms.size(); ++ i) {
1581
1582     // Non-equality atoms are either owned by theory or they don't make sense
1583     if (atoms[i].getKind() != kind::EQUAL) {
1584       continue;
1585     }
1586
1587     // The equality
1588     Node eq = atoms[i];
1589     // Simple normalization to not repeat stuff
1590     if (eq[0] > eq[1]) {
1591       eq = eq[1].eqNode(eq[0]);
1592     }
1593
1594     // Rewrite the equality
1595     Node eqNormalized = Rewriter::rewrite(atoms[i]);
1596
1597     Debug("theory::atoms") << "TheoryEngine::ensureLemmaAtoms(): " << eq << " with nf " << eqNormalized << endl;
1598
1599     // If the equality is a boolean constant, we send immediately
1600     if (eqNormalized.isConst()) {
1601       if (eqNormalized.getConst<bool>()) {
1602         assertToTheory(eq, eqNormalized, /** to */ atomsTo, /** Sat solver */ theory::THEORY_SAT_SOLVER);
1603       } else {
1604         assertToTheory(eq.notNode(), eqNormalized.notNode(), /** to */ atomsTo, /** Sat solver */ theory::THEORY_SAT_SOLVER);
1605       }
1606       continue;
1607     }else if( eqNormalized.getKind() != kind::EQUAL){
1608       Assert(eqNormalized.getKind() == kind::BOOLEAN_TERM_VARIABLE
1609              || (eqNormalized.getKind() == kind::NOT
1610                  && eqNormalized[0].getKind() == kind::BOOLEAN_TERM_VARIABLE));
1611       // this happens for Boolean term equalities V = true that are rewritten to V, we should skip
1612       //  TODO : revisit this
1613       continue;
1614     }
1615
1616     // If the normalization did the just flips, keep the flip
1617     if (eqNormalized[0] == eq[1] && eqNormalized[1] == eq[0]) {
1618       eq = eqNormalized;
1619     }
1620
1621     // Check if the equality is already known by the sat solver
1622     if (d_propEngine->isSatLiteral(eqNormalized)) {
1623       bool value;
1624       if (d_propEngine->hasValue(eqNormalized, value)) {
1625         if (value) {
1626           assertToTheory(eq, eqNormalized, atomsTo, theory::THEORY_SAT_SOLVER);
1627           continue;
1628         } else {
1629           assertToTheory(eq.notNode(), eqNormalized.notNode(), atomsTo, theory::THEORY_SAT_SOLVER);
1630           continue;
1631         }
1632       }
1633     }
1634
1635     // If the theory is asking about a different form, or the form is ok but if will go to a different theory
1636     // then we must figure it out
1637     if (eqNormalized != eq || Theory::theoryOf(eq) != atomsTo) {
1638       // If you get eqNormalized, send atoms[i] to atomsTo
1639       d_atomRequests.add(eqNormalized, eq, atomsTo);
1640     }
1641   }
1642 }
1643
1644 theory::LemmaStatus TheoryEngine::lemma(TNode node,
1645                                         ProofRule rule,
1646                                         bool negated,
1647                                         theory::LemmaProperty p,
1648                                         theory::TheoryId atomsTo)
1649 {
1650   // For resource-limiting (also does a time check).
1651   // spendResource();
1652
1653   // Do we need to check atoms
1654   if (atomsTo != theory::THEORY_LAST) {
1655     Debug("theory::atoms") << "TheoryEngine::lemma(" << node << ", " << atomsTo << ")" << endl;
1656     AtomsCollect collectAtoms;
1657     NodeVisitor<AtomsCollect>::run(collectAtoms, node);
1658     ensureLemmaAtoms(collectAtoms.getAtoms(), atomsTo);
1659   }
1660
1661   if(Dump.isOn("t-lemmas")) {
1662     Node n = node;
1663     if (!negated) {
1664       n = node.negate();
1665     }
1666     Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
1667                      << CheckSatCommand(n.toExpr());
1668   }
1669   bool removable = isLemmaPropertyRemovable(p);
1670   bool preprocess = isLemmaPropertyPreprocess(p);
1671
1672   // call preprocessor
1673   std::vector<TrustNode> newLemmas;
1674   std::vector<Node> newSkolems;
1675   TrustNode tlemma = d_tpp.preprocess(node, newLemmas, newSkolems, preprocess);
1676
1677   // !!!!!!! temporary, until this method is fully updated from proof-new
1678   if (tlemma.isNull())
1679   {
1680     tlemma = TrustNode::mkTrustLemma(node);
1681   }
1682
1683   // must use an assertion pipeline due to decision engine below
1684   AssertionPipeline lemmas;
1685   // make the assertion pipeline
1686   lemmas.push_back(tlemma.getNode());
1687   lemmas.updateRealAssertionsEnd();
1688   Assert(newSkolems.size() == newLemmas.size());
1689   for (size_t i = 0, nsize = newLemmas.size(); i < nsize; i++)
1690   {
1691     // store skolem mapping here
1692     IteSkolemMap& imap = lemmas.getIteSkolemMap();
1693     imap[newSkolems[i]] = lemmas.size();
1694     lemmas.push_back(newLemmas[i].getNode());
1695   }
1696
1697   // If specified, we must add this lemma to the set of those that need to be
1698   // justified, where note we pass all auxiliary lemmas in lemmas, since these
1699   // by extension must be justified as well.
1700   if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p))
1701   {
1702     d_relManager->notifyPreprocessedAssertions(lemmas.ref());
1703   }
1704
1705   // assert lemmas to prop engine
1706   for (size_t i = 0, lsize = lemmas.size(); i < lsize; ++i)
1707   {
1708     d_propEngine->assertLemma(
1709         lemmas[i], i == 0 && negated, removable, rule, node);
1710   }
1711
1712   // WARNING: Below this point don't assume lemmas[0] to be not negated.
1713   if(negated) {
1714     lemmas.replace(0, lemmas[0].notNode());
1715     negated = false;
1716   }
1717
1718   // assert to decision engine
1719   if (!removable)
1720   {
1721     d_propEngine->addAssertionsToDecisionEngine(lemmas);
1722   }
1723
1724   // Mark that we added some lemmas
1725   d_lemmasAdded = true;
1726
1727   // Lemma analysis isn't online yet; this lemma may only live for this
1728   // user level.
1729   Node retLemma = lemmas[0];
1730   if (lemmas.size() > 1)
1731   {
1732     // the returned lemma is the conjunction of all additional lemmas.
1733     retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas.ref());
1734   }
1735   return theory::LemmaStatus(retLemma, d_userContext->getLevel());
1736 }
1737
1738 void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
1739
1740   Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << endl;
1741
1742   Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl;
1743
1744   // Mark that we are in conflict
1745   d_inConflict = true;
1746
1747   if(Dump.isOn("t-conflicts")) {
1748     Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat")
1749                         << CheckSatCommand(conflict.toExpr());
1750   }
1751
1752   LemmaProofRecipe* proofRecipe = NULL;
1753   PROOF({
1754       proofRecipe = new LemmaProofRecipe;
1755       Node emptyNode;
1756       LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode);
1757
1758       if (conflict.getKind() == kind::AND) {
1759         for (unsigned i = 0; i < conflict.getNumChildren(); ++i) {
1760           proofStep.addAssertion(conflict[i].negate());
1761         }
1762       } else {
1763         proofStep.addAssertion(conflict.negate());
1764       }
1765
1766       proofRecipe->addStep(proofStep);
1767     });
1768
1769   // In the multiple-theories case, we need to reconstruct the conflict
1770   if (d_logicInfo.isSharingEnabled()) {
1771     // Create the workplace for explanations
1772     std::vector<NodeTheoryPair> explanationVector;
1773     explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
1774
1775     // Process the explanation
1776     getExplanation(explanationVector, proofRecipe);
1777     PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe));
1778     Node fullConflict = mkExplanation(explanationVector);
1779     Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
1780     Assert(properConflict(fullConflict));
1781     lemma(fullConflict,
1782           RULE_CONFLICT,
1783           true,
1784           LemmaProperty::REMOVABLE,
1785           THEORY_LAST);
1786   } else {
1787     // When only one theory, the conflict should need no processing
1788     Assert(properConflict(conflict));
1789     PROOF({
1790         if (conflict.getKind() == kind::AND) {
1791           // If the conflict is a conjunction, the corresponding lemma is derived by negating
1792           // its conjuncts.
1793           for (unsigned i = 0; i < conflict.getNumChildren(); ++i) {
1794             if (conflict[i].isConst() && conflict[i].getConst<bool>()) {
1795               ++ i;
1796               continue;
1797             }
1798             if (conflict[i].getKind() == kind::NOT &&
1799                 conflict[i][0].isConst() && !conflict[i][0].getConst<bool>()) {
1800               ++ i;
1801               continue;
1802             }
1803             proofRecipe->getStep(0)->addAssertion(conflict[i].negate());
1804             proofRecipe->addBaseAssertion(conflict[i].negate());
1805           }
1806         } else {
1807           proofRecipe->getStep(0)->addAssertion(conflict.negate());
1808           proofRecipe->addBaseAssertion(conflict.negate());
1809         }
1810
1811         ProofManager::getCnfProof()->setProofRecipe(proofRecipe);
1812       });
1813
1814     lemma(conflict, RULE_CONFLICT, true, LemmaProperty::REMOVABLE, THEORY_LAST);
1815   }
1816
1817   PROOF({
1818       delete proofRecipe;
1819       proofRecipe = NULL;
1820     });
1821 }
1822
1823 SharedTermsDatabase* TheoryEngine::getSharedTermsDatabase()
1824 {
1825   return &d_sharedTerms;
1826 }
1827
1828 void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) {
1829   Assert(explanationVector.size() > 0);
1830
1831   unsigned i = 0; // Index of the current literal we are processing
1832   unsigned j = 0; // Index of the last literal we are keeping
1833
1834   std::unique_ptr<std::set<Node>> inputAssertions = nullptr;
1835   PROOF({
1836     if (proofRecipe)
1837     {
1838       inputAssertions.reset(
1839           new std::set<Node>(proofRecipe->getStep(0)->getAssertions()));
1840     }
1841   });
1842   // cache of nodes we have already explained by some theory
1843   std::unordered_map<Node, size_t, NodeHashFunction> cache;
1844
1845   while (i < explanationVector.size()) {
1846     // Get the current literal to explain
1847     NodeTheoryPair toExplain = explanationVector[i];
1848
1849     Debug("theory::explain")
1850         << "[i=" << i << "] TheoryEngine::explain(): processing ["
1851         << toExplain.d_timestamp << "] " << toExplain.d_node << " sent from "
1852         << toExplain.d_theory << endl;
1853
1854     if (cache.find(toExplain.d_node) != cache.end()
1855         && cache[toExplain.d_node] < toExplain.d_timestamp)
1856     {
1857       ++i;
1858       continue;
1859     }
1860     cache[toExplain.d_node] = toExplain.d_timestamp;
1861
1862     // If a true constant or a negation of a false constant we can ignore it
1863     if (toExplain.d_node.isConst() && toExplain.d_node.getConst<bool>())
1864     {
1865       ++ i;
1866       continue;
1867     }
1868     if (toExplain.d_node.getKind() == kind::NOT && toExplain.d_node[0].isConst()
1869         && !toExplain.d_node[0].getConst<bool>())
1870     {
1871       ++ i;
1872       continue;
1873     }
1874
1875     // If from the SAT solver, keep it
1876     if (toExplain.d_theory == THEORY_SAT_SOLVER)
1877     {
1878       Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl;
1879       explanationVector[j++] = explanationVector[i++];
1880       continue;
1881     }
1882
1883     // If an and, expand it
1884     if (toExplain.d_node.getKind() == kind::AND)
1885     {
1886       Debug("theory::explain")
1887           << "TheoryEngine::explain(): expanding " << toExplain.d_node
1888           << " got from " << toExplain.d_theory << endl;
1889       for (unsigned k = 0; k < toExplain.d_node.getNumChildren(); ++k)
1890       {
1891         NodeTheoryPair newExplain(
1892             toExplain.d_node[k], toExplain.d_theory, toExplain.d_timestamp);
1893         explanationVector.push_back(newExplain);
1894       }
1895       ++ i;
1896       continue;
1897     }
1898
1899     // See if it was sent to the theory by another theory
1900     PropagationMap::const_iterator find = d_propagationMap.find(toExplain);
1901     if (find != d_propagationMap.end()) {
1902       Debug("theory::explain")
1903           << "\tTerm was propagated by another theory (theory = "
1904           << getTheoryString((*find).second.d_theory) << ")" << std::endl;
1905       // There is some propagation, check if its a timely one
1906       if ((*find).second.d_timestamp < toExplain.d_timestamp)
1907       {
1908         Debug("theory::explain")
1909             << "\tRelevant timetsamp, pushing " << (*find).second.d_node
1910             << "to index = " << explanationVector.size() << std::endl;
1911         explanationVector.push_back((*find).second);
1912         ++i;
1913
1914         PROOF({
1915           if (toExplain.d_node != (*find).second.d_node)
1916           {
1917             Debug("pf::explain")
1918                 << "TheoryEngine::getExplanation: Rewrite alert! toAssert = "
1919                 << toExplain.d_node << ", toExplain = " << (*find).second.d_node
1920                 << std::endl;
1921
1922             if (proofRecipe)
1923             {
1924               proofRecipe->addRewriteRule(toExplain.d_node,
1925                                           (*find).second.d_node);
1926             }
1927           }
1928         })
1929
1930         continue;
1931       }
1932     }
1933
1934     Node explanation;
1935     if (toExplain.d_theory == THEORY_BUILTIN)
1936     {
1937       explanation = d_sharedTerms.explain(toExplain.d_node);
1938       Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl;
1939     }
1940     else
1941     {
1942       TrustNode texp = theoryOf(toExplain.d_theory)->explain(toExplain.d_node);
1943       explanation = texp.getNode();
1944       Debug("theory::explain") << "\tTerm was propagated by owner theory: "
1945                                << theoryOf(toExplain.d_theory)->getId()
1946                                << ". Explanation: " << explanation << std::endl;
1947     }
1948
1949     Debug("theory::explain")
1950         << "TheoryEngine::explain(): got explanation " << explanation
1951         << " got from " << toExplain.d_theory << endl;
1952     Assert(explanation != toExplain.d_node)
1953         << "wasn't sent to you, so why are you explaining it trivially";
1954     // Mark the explanation
1955     NodeTheoryPair newExplain(
1956         explanation, toExplain.d_theory, toExplain.d_timestamp);
1957     explanationVector.push_back(newExplain);
1958
1959     ++ i;
1960
1961     PROOF({
1962       if (proofRecipe && inputAssertions)
1963       {
1964         // If we're expanding the target node of the explanation (this is the
1965         // first expansion...), we don't want to add it as a separate proof
1966         // step. It is already part of the assertions.
1967         if (!ContainsKey(*inputAssertions, toExplain.d_node))
1968         {
1969           LemmaProofRecipe::ProofStep proofStep(toExplain.d_theory,
1970                                                 toExplain.d_node);
1971           if (explanation.getKind() == kind::AND)
1972           {
1973             Node flat = flattenAnd(explanation);
1974             for (unsigned k = 0; k < flat.getNumChildren(); ++k)
1975             {
1976               // If a true constant or a negation of a false constant we can
1977               // ignore it
1978               if (!((flat[k].isConst() && flat[k].getConst<bool>())
1979                     || (flat[k].getKind() == kind::NOT && flat[k][0].isConst()
1980                         && !flat[k][0].getConst<bool>())))
1981               {
1982                 proofStep.addAssertion(flat[k].negate());
1983               }
1984             }
1985           }
1986           else
1987           {
1988             if (!((explanation.isConst() && explanation.getConst<bool>())
1989                   || (explanation.getKind() == kind::NOT
1990                       && explanation[0].isConst()
1991                       && !explanation[0].getConst<bool>())))
1992             {
1993               proofStep.addAssertion(explanation.negate());
1994             }
1995           }
1996           proofRecipe->addStep(proofStep);
1997         }
1998       }
1999     });
2000   }
2001
2002   // Keep only the relevant literals
2003   explanationVector.resize(j);
2004
2005   PROOF({
2006       if (proofRecipe) {
2007         // The remaining literals are the base of the proof
2008         for (unsigned k = 0; k < explanationVector.size(); ++k) {
2009           proofRecipe->addBaseAssertion(explanationVector[k].d_node.negate());
2010         }
2011       }
2012     });
2013 }
2014
2015 void TheoryEngine::setUserAttribute(const std::string& attr,
2016                                     Node n,
2017                                     const std::vector<Node>& node_values,
2018                                     const std::string& str_value)
2019 {
2020   Trace("te-attr") << "set user attribute " << attr << " " << n << endl;
2021   if( d_attr_handle.find( attr )!=d_attr_handle.end() ){
2022     for( size_t i=0; i<d_attr_handle[attr].size(); i++ ){
2023       d_attr_handle[attr][i]->setUserAttribute(attr, n, node_values, str_value);
2024     }
2025   } else {
2026     //unhandled exception?
2027   }
2028 }
2029
2030 void TheoryEngine::handleUserAttribute(const char* attr, Theory* t) {
2031   Trace("te-attr") << "Handle user attribute " << attr << " " << t << endl;
2032   std::string str( attr );
2033   d_attr_handle[ str ].push_back( t );
2034 }
2035
2036 void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
2037   for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
2038     Theory* theory = d_theoryTable[theoryId];
2039     if(theory && d_logicInfo.isTheoryEnabled(theoryId)) {
2040       for(context::CDList<Assertion>::const_iterator it = theory->facts_begin(),
2041             it_end = theory->facts_end();
2042           it != it_end;
2043           ++it) {
2044         Node assertion = (*it).d_assertion;
2045         if (!isRelevant(assertion))
2046         {
2047           // not relevant, skip
2048           continue;
2049         }
2050         Node val = getModel()->getValue(assertion);
2051         if (val != d_true)
2052         {
2053           std::stringstream ss;
2054           ss << " " << theoryId
2055              << " has an asserted fact that the model doesn't satisfy." << endl
2056              << "The fact: " << assertion << endl
2057              << "Model value: " << val << endl;
2058           if (hardFailure)
2059           {
2060             if (val == d_false)
2061             {
2062               // Always an error if it is false
2063               InternalError() << ss.str();
2064             }
2065             else
2066             {
2067               // Otherwise just a warning. Notice this case may happen for
2068               // assertions with unevaluable operators, e.g. transcendental
2069               // functions. It also may happen for separation logic, where
2070               // check-model support is limited.
2071               Warning() << ss.str();
2072             }
2073           }
2074         }
2075       }
2076     }
2077   }
2078 }
2079
2080 std::pair<bool, Node> TheoryEngine::entailmentCheck(options::TheoryOfMode mode,
2081                                                     TNode lit)
2082 {
2083   TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit;
2084   if( atom.getKind()==kind::AND || atom.getKind()==kind::OR || atom.getKind()==kind::IMPLIES ){
2085     //Boolean connective, recurse
2086     std::vector< Node > children;
2087     bool pol = (lit.getKind()!=kind::NOT);
2088     bool is_conjunction = pol==(lit.getKind()==kind::AND);
2089     for( unsigned i=0; i<atom.getNumChildren(); i++ ){
2090       Node ch = atom[i];
2091       if( pol==( lit.getKind()==kind::IMPLIES && i==0 ) ){
2092         ch = atom[i].negate();
2093       }
2094       std::pair<bool, Node> chres = entailmentCheck(mode, ch);
2095       if( chres.first ){
2096         if( !is_conjunction ){
2097           return chres;
2098         }else{
2099           children.push_back( chres.second );
2100         }
2101       }else if( !chres.first && is_conjunction ){
2102         return std::pair<bool, Node>(false, Node::null());
2103       }
2104     }
2105     if( is_conjunction ){
2106       return std::pair<bool, Node>(true, NodeManager::currentNM()->mkNode(kind::AND, children));
2107     }else{
2108       return std::pair<bool, Node>(false, Node::null());
2109     }
2110   }else if( atom.getKind()==kind::ITE || ( atom.getKind()==kind::EQUAL && atom[0].getType().isBoolean() ) ){
2111     bool pol = (lit.getKind()!=kind::NOT);
2112     for( unsigned r=0; r<2; r++ ){
2113       Node ch = atom[0];
2114       if( r==1 ){
2115         ch = ch.negate();
2116       }
2117       std::pair<bool, Node> chres = entailmentCheck(mode, ch);
2118       if( chres.first ){
2119         Node ch2 = atom[ atom.getKind()==kind::ITE ? r+1 : 1 ];
2120         if( pol==( atom.getKind()==kind::ITE ? true : r==1 ) ){
2121           ch2 = ch2.negate();
2122         }
2123         std::pair<bool, Node> chres2 = entailmentCheck(mode, ch2);
2124         if( chres2.first ){
2125           return std::pair<bool, Node>(true, NodeManager::currentNM()->mkNode(kind::AND, chres.second, chres2.second));
2126         }else{
2127           break;
2128         }
2129       }
2130     }
2131     return std::pair<bool, Node>(false, Node::null());
2132   }else{
2133     //it is a theory atom
2134     theory::TheoryId tid = theory::Theory::theoryOf(mode, atom);
2135     theory::Theory* th = theoryOf(tid);
2136
2137     Assert(th != NULL);
2138     Trace("theory-engine-entc") << "Entailment check : " << lit << std::endl;
2139
2140     std::pair<bool, Node> chres = th->entailmentCheck(lit);
2141     return chres;
2142   }
2143 }
2144
2145 void TheoryEngine::spendResource(ResourceManager::Resource r)
2146 {
2147   d_resourceManager->spendResource(r);
2148 }
2149
2150 }/* CVC4 namespace */