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