src/theory/theory_engine.cpp

   1 /*********************                                                        */
   2 /*! \file theory_engine.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Dejan Jovanovic
   6  ** Minor contributors (to current version): Christopher L. Conway, Kshitij Bansal, Tim King, Liana Hadarean, Clark Barrett, Andrew Reynolds
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief The theory engine
  13  **
  14  ** The theory engine.
  15  **/
  16
  17 #include <vector>
  18 #include <list>
  19
  20 #include "decision/decision_engine.h"
  21
  22 #include "expr/attribute.h"
  23 #include "expr/node.h"
  24 #include "expr/node_builder.h"
  25 #include "options/options.h"
  26 #include "util/lemma_output_channel.h"
  27
  28 #include "theory/theory.h"
  29 #include "theory/theory_engine.h"
  30 #include "theory/rewriter.h"
  31 #include "theory/theory_traits.h"
  32
  33 #include "smt/logic_exception.h"
  34
  35 #include "util/node_visitor.h"
  36 #include "util/ite_removal.h"
  37
  38 #include "theory/model.h"
  39 #include "theory/quantifiers_engine.h"
  40 #include "theory/quantifiers/theory_quantifiers.h"
  41 #include "theory/quantifiers/options.h"
  42 #include "theory/quantifiers/model_engine.h"
  43 #include "theory/quantifiers/first_order_model.h"
  44
  45 #include "theory/uf/equality_engine.h"
  46
  47 #include "theory/rewriterules/efficient_e_matching.h"
  48
  49 using namespace std;
  50
  51 using namespace CVC4;
  52 using namespace CVC4::theory;
  53
  54 void TheoryEngine::finishInit() {
  55   if (d_logicInfo.isQuantified()) {
  56     d_quantEngine->finishInit();
  57     Assert(d_masterEqualityEngine == 0);
  58     d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master");
  59
  60     for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
  61       if (d_theoryTable[theoryId]) {
  62         d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine);
  63       }
  64     }
  65   }
  66 }
  67
  68 void TheoryEngine::eqNotifyNewClass(TNode t){
  69   d_quantEngine->addTermToDatabase( t );
  70 }
  71
  72 void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
  73   //TODO: add notification to efficient E-matching
  74   if (d_logicInfo.isQuantified()) {
  75     d_quantEngine->getEfficientEMatcher()->merge( t1, t2 );
  76   }
  77 }
  78
  79 void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){
  80
  81 }
  82
  83 void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
  84
  85 }
  86
  87
  88 TheoryEngine::TheoryEngine(context::Context* context,
  89                            context::UserContext* userContext,
  90                            RemoveITE& iteRemover,
  91                            const LogicInfo& logicInfo)
  92 : d_propEngine(NULL),
  93   d_decisionEngine(NULL),
  94   d_context(context),
  95   d_userContext(userContext),
  96   d_logicInfo(logicInfo),
  97   d_sharedTerms(this, context),
  98   d_masterEqualityEngine(NULL),
  99   d_masterEENotify(*this),
 100   d_quantEngine(NULL),
 101   d_curr_model(NULL),
 102   d_curr_model_builder(NULL),
 103   d_ppCache(),
 104   d_possiblePropagations(context),
 105   d_hasPropagated(context),
 106   d_inConflict(context, false),
 107   d_hasShutDown(false),
 108   d_incomplete(context, false),
 109   d_propagationMap(context),
 110   d_propagationMapTimestamp(context, 0),
 111   d_propagatedLiterals(context),
 112   d_propagatedLiteralsIndex(context, 0),
 113   d_atomRequests(context),
 114   d_iteRemover(iteRemover),
 115   d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
 116   d_true(),
 117   d_false(),
 118   d_interrupted(false),
 119   d_inPreregister(false),
 120   d_factsAsserted(context, false),
 121   d_preRegistrationVisitor(this, context),
 122   d_sharedTermsVisitor(d_sharedTerms),
 123   d_unconstrainedSimp(context, logicInfo),
 124   d_bvToBoolPreprocessor()
 125 {
 126   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
 127     d_theoryTable[theoryId] = NULL;
 128     d_theoryOut[theoryId] = NULL;
 129   }
 130
 131   // initialize the quantifiers engine
 132   d_quantEngine = new QuantifiersEngine(context, userContext, this);
 133
 134   // build model information if applicable
 135   d_curr_model = new theory::TheoryModel(userContext, "DefaultModel", true);
 136   d_curr_model_builder = new theory::TheoryEngineModelBuilder(this);
 137
 138   StatisticsRegistry::registerStat(&d_combineTheoriesTime);
 139   d_true = NodeManager::currentNM()->mkConst<bool>(true);
 140   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 141 }
 142
 143 TheoryEngine::~TheoryEngine() {
 144   Assert(d_hasShutDown);
 145
 146   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
 147     if(d_theoryTable[theoryId] != NULL) {
 148       delete d_theoryTable[theoryId];
 149       delete d_theoryOut[theoryId];
 150     }
 151   }
 152
 153   delete d_curr_model_builder;
 154   delete d_curr_model;
 155
 156   delete d_quantEngine;
 157
 158   delete d_masterEqualityEngine;
 159
 160   StatisticsRegistry::unregisterStat(&d_combineTheoriesTime);
 161 }
 162
 163 void TheoryEngine::interrupt() throw(ModalException) {
 164   d_interrupted = true;
 165 }
 166
 167 void TheoryEngine::preRegister(TNode preprocessed) {
 168
 169   if(Dump.isOn("missed-t-propagations")) {
 170     d_possiblePropagations.push_back(preprocessed);
 171   }
 172   d_preregisterQueue.push(preprocessed);
 173
 174   if (!d_inPreregister) {
 175     // We're in pre-register
 176     d_inPreregister = true;
 177
 178     // Process the pre-registration queue
 179     while (!d_preregisterQueue.empty()) {
 180       // Get the next atom to pre-register
 181       preprocessed = d_preregisterQueue.front();
 182       d_preregisterQueue.pop();
 183
 184       if (d_logicInfo.isSharingEnabled() && preprocessed.getKind() == kind::EQUAL) {
 185         // When sharing is enabled, we propagate from the shared terms manager also
 186         d_sharedTerms.addEqualityToPropagate(preprocessed);
 187       }
 188
 189       // Pre-register the terms in the atom
 190       Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
 191       theories = Theory::setRemove(THEORY_BOOL, theories);
 192       // Remove the top theory, if any more that means multiple theories were involved
 193       bool multipleTheories = Theory::setRemove(Theory::theoryOf(preprocessed), theories);
 194       TheoryId i;
 195       // These checks don't work with finite model finding, because it
 196       // uses Rational constants to represent cardinality constraints,
 197       // even though arithmetic isn't actually involved.
 198       if(!options::finiteModelFind()) {
 199         while((i = Theory::setPop(theories)) != THEORY_LAST) {
 200           if(!d_logicInfo.isTheoryEnabled(i)) {
 201             LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy();
 202             newLogicInfo.enableTheory(i);
 203             newLogicInfo.lock();
 204             stringstream ss;
 205             ss << "The logic was specified as " << d_logicInfo.getLogicString()
 206                << ", which doesn't include " << i
 207                << ", but found a term in that theory." << endl
 208                << "You might want to extend your logic to "
 209                << newLogicInfo.getLogicString() << endl;
 210             throw LogicException(ss.str());
 211           }
 212         }
 213       }
 214       if (multipleTheories) {
 215         // Collect the shared terms if there are multipe theories
 216         NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed);
 217       }
 218     }
 219
 220     // Leaving pre-register
 221     d_inPreregister = false;
 222   }
 223 }
 224
 225 void TheoryEngine::printAssertions(const char* tag) {
 226   if (Trace.isOn(tag)) {
 227
 228     for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
 229       Theory* theory = d_theoryTable[theoryId];
 230       if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
 231         Trace(tag) << "--------------------------------------------" << endl;
 232         Trace(tag) << "Assertions of " << theory->getId() << ": " << endl;
 233         context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
 234         for (unsigned i = 0; it != it_end; ++ it, ++i) {
 235             if ((*it).isPreregistered) {
 236               Trace(tag) << "[" << i << "]: ";
 237             } else {
 238               Trace(tag) << "(" << i << "): ";
 239             }
 240             Trace(tag) << (*it).assertion << endl;
 241         }
 242
 243         if (d_logicInfo.isSharingEnabled()) {
 244           Trace(tag) << "Shared terms of " << theory->getId() << ": " << endl;
 245           context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
 246           for (unsigned i = 0; it != it_end; ++ it, ++i) {
 247               Trace(tag) << "[" << i << "]: " << (*it) << endl;
 248           }
 249         }
 250       }
 251     }
 252   }
 253 }
 254
 255 void TheoryEngine::dumpAssertions(const char* tag) {
 256   if (Dump.isOn(tag)) {
 257     Dump(tag) << CommentCommand("Starting completeness check");
 258     for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
 259       Theory* theory = d_theoryTable[theoryId];
 260       if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
 261         Dump(tag) << CommentCommand("Completeness check");
 262         Dump(tag) << PushCommand();
 263
 264         // Dump the shared terms
 265         if (d_logicInfo.isSharingEnabled()) {
 266           Dump(tag) << CommentCommand("Shared terms");
 267           context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
 268           for (unsigned i = 0; it != it_end; ++ it, ++i) {
 269               stringstream ss;
 270               ss << (*it);
 271               Dump(tag) << CommentCommand(ss.str());
 272           }
 273         }
 274
 275         // Dump the assertions
 276         Dump(tag) << CommentCommand("Assertions");
 277         context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
 278         for (; it != it_end; ++ it) {
 279           // Get the assertion
 280           Node assertionNode = (*it).assertion;
 281           // Purify all the terms
 282
 283           if ((*it).isPreregistered) {
 284             Dump(tag) << CommentCommand("Preregistered");
 285           } else {
 286             Dump(tag) << CommentCommand("Shared assertion");
 287           }
 288           Dump(tag) << AssertCommand(assertionNode.toExpr());
 289         }
 290         Dump(tag) << CheckSatCommand();
 291
 292         Dump(tag) << PopCommand();
 293       }
 294     }
 295   }
 296 }
 297
 298 /**
 299  * Check all (currently-active) theories for conflicts.
 300  * @param effort the effort level to use
 301  */
 302 void TheoryEngine::check(Theory::Effort effort) {
 303
 304   d_propEngine->checkTime();
 305
 306   // Reset the interrupt flag
 307   d_interrupted = false;
 308
 309 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 310 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 311 #endif
 312 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 313     if (theory::TheoryTraits<THEORY>::hasCheck && d_logicInfo.isTheoryEnabled(THEORY)) { \
 314        theoryOf(THEORY)->check(effort); \
 315        if (d_inConflict) { \
 316          break; \
 317        } \
 318     }
 319
 320   // Do the checking
 321   try {
 322
 323     // Mark the output channel unused (if this is FULL_EFFORT, and nothing
 324     // is done by the theories, no additional check will be needed)
 325     d_outputChannelUsed = false;
 326
 327     // Mark the lemmas flag (no lemmas added)
 328     d_lemmasAdded = false;
 329
 330     Debug("theory") << "TheoryEngine::check(" << effort << "): d_factsAsserted = " << (d_factsAsserted ? "true" : "false") << endl;
 331
 332     // If in full effort, we have a fake new assertion just to jumpstart the checking
 333     if (Theory::fullEffort(effort)) {
 334       d_factsAsserted = true;
 335     }
 336
 337     // Check until done
 338     while (d_factsAsserted && !d_inConflict && !d_lemmasAdded) {
 339
 340       Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << endl;
 341
 342       Trace("theory::assertions") << endl;
 343       if (Trace.isOn("theory::assertions")) {
 344         printAssertions("theory::assertions");
 345       }
 346
 347       // Note that we've discharged all the facts
 348       d_factsAsserted = false;
 349
 350       // Do the checking
 351       CVC4_FOR_EACH_THEORY;
 352
 353       if(Dump.isOn("missed-t-conflicts")) {
 354         Dump("missed-t-conflicts")
 355             << CommentCommand("Completeness check for T-conflicts; expect sat")
 356             << CheckSatCommand();
 357       }
 358
 359       Debug("theory") << "TheoryEngine::check(" << effort << "): running propagation after the initial check" << endl;
 360
 361       // We are still satisfiable, propagate as much as possible
 362       propagate(effort);
 363
 364       // We do combination if all has been processed and we are in fullcheck
 365       if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() && !d_factsAsserted && !d_lemmasAdded) {
 366         // Do the combination
 367         Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << endl;
 368         combineTheories();
 369       }
 370     }
 371
 372     // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
 373     if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) {
 374       if(d_logicInfo.isQuantified()) {
 375         // quantifiers engine must pass effort last call check
 376         d_quantEngine->check(Theory::EFFORT_LAST_CALL);
 377         // if we have given up, then possibly flip decision
 378         if(options::flipDecision()) {
 379           if(d_incomplete && !d_inConflict && !needCheck()) {
 380             ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->flipDecision();
 381           }
 382         }
 383         // if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built
 384       } else if(options::produceModels()) {
 385         // must build model at this point
 386         d_curr_model_builder->buildModel(d_curr_model, true);
 387       }
 388     }
 389
 390     Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas") << endl;
 391
 392     if(!d_inConflict && Theory::fullEffort(effort) && d_masterEqualityEngine != NULL && !d_lemmasAdded) {
 393       AlwaysAssert(d_masterEqualityEngine->consistent());
 394     }
 395
 396   } catch(const theory::Interrupted&) {
 397     Trace("theory") << "TheoryEngine::check() => interrupted" << endl;
 398   }
 399
 400   // If fulleffort, check all theories
 401   if(Dump.isOn("theory::fullcheck") && Theory::fullEffort(effort)) {
 402     if (!d_inConflict && !needCheck()) {
 403       dumpAssertions("theory::fullcheck");
 404     }
 405   }
 406 }
 407
 408 void TheoryEngine::combineTheories() {
 409
 410   Debug("sharing") << "TheoryEngine::combineTheories()" << endl;
 411
 412   TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime);
 413
 414   // Care graph we'll be building
 415   CareGraph careGraph;
 416
 417 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 418 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 419 #endif
 420 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 421   if (theory::TheoryTraits<THEORY>::isParametric && d_logicInfo.isTheoryEnabled(THEORY)) { \
 422     theoryOf(THEORY)->getCareGraph(careGraph); \
 423   }
 424
 425   // Call on each parametric theory to give us its care graph
 426   CVC4_FOR_EACH_THEORY;
 427
 428   Debug("sharing") << "TheoryEngine::combineTheories(): care graph size = " << careGraph.size() << endl;
 429
 430   // Now add splitters for the ones we are interested in
 431   CareGraph::const_iterator care_it = careGraph.begin();
 432   CareGraph::const_iterator care_it_end = careGraph.end();
 433   for (; care_it != care_it_end; ++ care_it) {
 434     const CarePair& carePair = *care_it;
 435
 436     Debug("sharing") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << endl;
 437
 438     Assert(d_sharedTerms.isShared(carePair.a) || carePair.a.isConst());
 439     Assert(d_sharedTerms.isShared(carePair.b) || carePair.b.isConst());
 440
 441     // The equality in question (order for no repetition)
 442     Node equality = carePair.a.eqNode(carePair.b);
 443
 444     // We need to split on it
 445     Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << endl;
 446     lemma(equality.orNode(equality.notNode()), false, false, carePair.theory);
 447   }
 448 }
 449
 450 void TheoryEngine::propagate(Theory::Effort effort) {
 451   // Reset the interrupt flag
 452   d_interrupted = false;
 453
 454   // Definition of the statement that is to be run by every theory
 455 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 456 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 457 #endif
 458 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 459   if (theory::TheoryTraits<THEORY>::hasPropagate && d_logicInfo.isTheoryEnabled(THEORY)) { \
 460     theoryOf(THEORY)->propagate(effort); \
 461   }
 462
 463   // Reset the interrupt flag
 464   d_interrupted = false;
 465
 466   // Propagate for each theory using the statement above
 467   CVC4_FOR_EACH_THEORY;
 468
 469   if(Dump.isOn("missed-t-propagations")) {
 470     for(unsigned i = 0; i < d_possiblePropagations.size(); ++i) {
 471       Node atom = d_possiblePropagations[i];
 472       bool value;
 473       if(d_propEngine->hasValue(atom, value)) {
 474         continue;
 475       }
 476       // Doesn't have a value, check it (and the negation)
 477       if(d_hasPropagated.find(atom) == d_hasPropagated.end()) {
 478         Dump("missed-t-propagations")
 479           << CommentCommand("Completeness check for T-propagations; expect invalid")
 480           << EchoCommand(atom.toString())
 481           << QueryCommand(atom.toExpr())
 482           << EchoCommand(atom.notNode().toString())
 483           << QueryCommand(atom.notNode().toExpr());
 484       }
 485     }
 486   }
 487 }
 488
 489 Node TheoryEngine::getNextDecisionRequest() {
 490   // Definition of the statement that is to be run by every theory
 491 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 492 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 493 #endif
 494 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 495   if (theory::TheoryTraits<THEORY>::hasGetNextDecisionRequest && d_logicInfo.isTheoryEnabled(THEORY)) { \
 496     Node n = theoryOf(THEORY)->getNextDecisionRequest(); \
 497     if(! n.isNull()) { \
 498       return n; \
 499     } \
 500   }
 501
 502   // Request decision from each theory using the statement above
 503   CVC4_FOR_EACH_THEORY;
 504
 505   return TNode();
 506 }
 507
 508 bool TheoryEngine::properConflict(TNode conflict) const {
 509   bool value;
 510   if (conflict.getKind() == kind::AND) {
 511     for (unsigned i = 0; i < conflict.getNumChildren(); ++ i) {
 512       if (! getPropEngine()->hasValue(conflict[i], value)) {
 513         Debug("properConflict") << "Bad conflict is due to unassigned atom: "
 514                                 << conflict[i] << endl;
 515         return false;
 516       }
 517       if (! value) {
 518         Debug("properConflict") << "Bad conflict is due to false atom: "
 519                                 << conflict[i] << endl;
 520         return false;
 521       }
 522       if (conflict[i] != Rewriter::rewrite(conflict[i])) {
 523         Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
 524                                 << conflict[i] << " vs " << Rewriter::rewrite(conflict[i]) << endl;
 525         return false;
 526       }
 527     }
 528   } else {
 529     if (! getPropEngine()->hasValue(conflict, value)) {
 530       Debug("properConflict") << "Bad conflict is due to unassigned atom: "
 531                               << conflict << endl;
 532       return false;
 533     }
 534     if(! value) {
 535       Debug("properConflict") << "Bad conflict is due to false atom: "
 536                               << conflict << endl;
 537       return false;
 538     }
 539     if (conflict != Rewriter::rewrite(conflict)) {
 540       Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
 541                               << conflict << " vs " << Rewriter::rewrite(conflict) << endl;
 542       return false;
 543     }
 544   }
 545   return true;
 546 }
 547
 548 bool TheoryEngine::properPropagation(TNode lit) const {
 549   if(!getPropEngine()->isSatLiteral(lit)) {
 550     return false;
 551   }
 552   bool b;
 553   return !getPropEngine()->hasValue(lit, b);
 554 }
 555
 556 bool TheoryEngine::properExplanation(TNode node, TNode expl) const {
 557   // Explanation must be either a conjunction of true literals that have true SAT values already
 558   // or a singled literal that has a true SAT value already.
 559   if (expl.getKind() == kind::AND) {
 560     for (unsigned i = 0; i < expl.getNumChildren(); ++ i) {
 561       bool value;
 562       if (!d_propEngine->hasValue(expl[i], value) || !value) {
 563         return false;
 564       }
 565     }
 566   } else {
 567     bool value;
 568     return d_propEngine->hasValue(expl, value) && value;
 569   }
 570   return true;
 571 }
 572
 573 void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){
 574   //have shared term engine collectModelInfo
 575   //  d_sharedTerms.collectModelInfo( m, fullModel );
 576   // Consult each active theory to get all relevant information
 577   // concerning the model.
 578   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
 579     if(d_logicInfo.isTheoryEnabled(theoryId)) {
 580       Trace("model-builder") << "  CollectModelInfo on theory: " << theoryId << endl;
 581       d_theoryTable[theoryId]->collectModelInfo( m, fullModel );
 582     }
 583   }
 584   // Get the Boolean variables
 585   vector<TNode> boolVars;
 586   d_propEngine->getBooleanVariables(boolVars);
 587   vector<TNode>::iterator it, iend = boolVars.end();
 588   bool hasValue, value;
 589   for (it = boolVars.begin(); it != iend; ++it) {
 590     TNode var = *it;
 591     hasValue = d_propEngine->hasValue(var, value);
 592     // TODO: Assert that hasValue is true?
 593     if (!hasValue) {
 594       value = false;
 595     }
 596     Trace("model-builder-assertions") << "(assert" << (value ? " " : " (not ") << var << (value ? ");" : "));") << endl;
 597     m->assertPredicate(var, value);
 598   }
 599 }
 600
 601 /* get model */
 602 TheoryModel* TheoryEngine::getModel() {
 603   Debug("model") << "TheoryEngine::getModel()" << endl;
 604   if( d_logicInfo.isQuantified() ) {
 605     Debug("model") << "Get model from quantifiers engine." << endl;
 606     return d_quantEngine->getModel();
 607   } else {
 608     Debug("model") << "Get default model." << endl;
 609     return d_curr_model;
 610   }
 611 }
 612
 613 bool TheoryEngine::presolve() {
 614   // Reset the interrupt flag
 615   d_interrupted = false;
 616
 617   try {
 618     // Definition of the statement that is to be run by every theory
 619 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 620 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 621 #endif
 622 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 623     if (theory::TheoryTraits<THEORY>::hasPresolve) {    \
 624       theoryOf(THEORY)->presolve(); \
 625       if(d_inConflict) { \
 626         return true; \
 627       } \
 628     }
 629
 630     // Presolve for each theory using the statement above
 631     CVC4_FOR_EACH_THEORY;
 632   } catch(const theory::Interrupted&) {
 633     Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl;
 634   }
 635   // return whether we have a conflict
 636   return false;
 637 }/* TheoryEngine::presolve() */
 638
 639 void TheoryEngine::postsolve() {
 640   // Reset the interrupt flag
 641   d_interrupted = false;
 642
 643   try {
 644     // Definition of the statement that is to be run by every theory
 645 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 646 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 647 #endif
 648 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 649     if (theory::TheoryTraits<THEORY>::hasPostsolve) { \
 650       theoryOf(THEORY)->postsolve(); \
 651       Assert(! d_inConflict, "conflict raised during postsolve()"); \
 652     }
 653
 654     // Postsolve for each theory using the statement above
 655     CVC4_FOR_EACH_THEORY;
 656   } catch(const theory::Interrupted&) {
 657     Trace("theory") << "TheoryEngine::postsolve() => interrupted" << endl;
 658   }
 659 }/* TheoryEngine::postsolve() */
 660
 661
 662 void TheoryEngine::notifyRestart() {
 663   // Reset the interrupt flag
 664   d_interrupted = false;
 665
 666   // Definition of the statement that is to be run by every theory
 667 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 668 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 669 #endif
 670 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 671   if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_logicInfo.isTheoryEnabled(THEORY)) { \
 672     theoryOf(THEORY)->notifyRestart(); \
 673   }
 674
 675   // notify each theory using the statement above
 676   CVC4_FOR_EACH_THEORY;
 677 }
 678
 679 void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
 680   // Reset the interrupt flag
 681   d_interrupted = false;
 682
 683   // Definition of the statement that is to be run by every theory
 684 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 685 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 686 #endif
 687 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
 688   if (theory::TheoryTraits<THEORY>::hasPpStaticLearn) { \
 689     theoryOf(THEORY)->ppStaticLearn(in, learned); \
 690   }
 691
 692   // static learning for each theory using the statement above
 693   CVC4_FOR_EACH_THEORY;
 694 }
 695
 696 void TheoryEngine::shutdown() {
 697   // Set this first; if a Theory shutdown() throws an exception,
 698   // at least the destruction of the TheoryEngine won't confound
 699   // matters.
 700   d_hasShutDown = true;
 701
 702   // Shutdown all the theories
 703   for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
 704     if(d_theoryTable[theoryId]) {
 705       theoryOf(theoryId)->shutdown();
 706     }
 707   }
 708
 709   d_ppCache.clear();
 710 }
 711
 712 theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) {
 713   // Reset the interrupt flag
 714   d_interrupted = false;
 715
 716   TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
 717   Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
 718
 719   if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(atom)) &&
 720      Theory::theoryOf(atom) != THEORY_SAT_SOLVER) {
 721     stringstream ss;
 722     ss << "The logic was specified as " << d_logicInfo.getLogicString()
 723        << ", which doesn't include " << Theory::theoryOf(atom)
 724        << ", but got a preprocessing-time fact for that theory." << endl
 725        << "The fact:" << endl
 726        << literal;
 727     throw LogicException(ss.str());
 728   }
 729
 730   Theory::PPAssertStatus solveStatus = theoryOf(atom)->ppAssert(literal, substitutionOut);
 731   Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl;
 732   return solveStatus;
 733 }
 734
 735 // Recursively traverse a term and call the theory rewriter on its sub-terms
 736 Node TheoryEngine::ppTheoryRewrite(TNode term) {
 737   NodeMap::iterator find = d_ppCache.find(term);
 738   if (find != d_ppCache.end()) {
 739     return (*find).second;
 740   }
 741   unsigned nc = term.getNumChildren();
 742   if (nc == 0) {
 743     return theoryOf(term)->ppRewrite(term);
 744   }
 745   Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
 746
 747   Node newTerm;
 748   if (theoryOf(term)->ppDontRewriteSubterm(term)) {
 749     newTerm = term;
 750   } else {
 751     NodeBuilder<> newNode(term.getKind());
 752     if (term.getMetaKind() == kind::metakind::PARAMETERIZED) {
 753       newNode << term.getOperator();
 754     }
 755     unsigned i;
 756     for (i = 0; i < nc; ++i) {
 757       newNode << ppTheoryRewrite(term[i]);
 758     }
 759     newTerm = Rewriter::rewrite(Node(newNode));
 760   }
 761   Node newTerm2 = theoryOf(newTerm)->ppRewrite(newTerm);
 762   if (newTerm != newTerm2) {
 763     newTerm = ppTheoryRewrite(Rewriter::rewrite(newTerm2));
 764   }
 765   d_ppCache[term] = newTerm;
 766   Trace("theory-pp")<< "ppTheoryRewrite returning " << newTerm << "}" << endl;
 767   return newTerm;
 768 }
 769
 770
 771 void TheoryEngine::preprocessStart()
 772 {
 773   d_ppCache.clear();
 774 }
 775
 776
 777 struct preprocess_stack_element {
 778   TNode node;
 779   bool children_added;
 780   preprocess_stack_element(TNode node)
 781   : node(node), children_added(false) {}
 782 };/* struct preprocess_stack_element */
 783
 784
 785 Node TheoryEngine::preprocess(TNode assertion) {
 786
 787   Trace("theory::preprocess") << "TheoryEngine::preprocess(" << assertion << ")" << endl;
 788
 789   // Do a topological sort of the subexpressions and substitute them
 790   vector<preprocess_stack_element> toVisit;
 791   toVisit.push_back(assertion);
 792
 793   while (!toVisit.empty())
 794   {
 795     // The current node we are processing
 796     preprocess_stack_element& stackHead = toVisit.back();
 797     TNode current = stackHead.node;
 798
 799     Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): processing " << current << endl;
 800
 801     // If node already in the cache we're done, pop from the stack
 802     NodeMap::iterator find = d_ppCache.find(current);
 803     if (find != d_ppCache.end()) {
 804       toVisit.pop_back();
 805       continue;
 806     }
 807
 808     if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(current)) &&
 809        Theory::theoryOf(current) != THEORY_SAT_SOLVER) {
 810       stringstream ss;
 811       ss << "The logic was specified as " << d_logicInfo.getLogicString()
 812          << ", which doesn't include " << Theory::theoryOf(current)
 813          << ", but got a preprocessing-time fact for that theory." << endl
 814          << "The fact:" << endl
 815          << current;
 816       throw LogicException(ss.str());
 817     }
 818
 819     // If this is an atom, we preprocess its terms with the theory ppRewriter
 820     if (Theory::theoryOf(current) != THEORY_BOOL) {
 821       Node ppRewritten = ppTheoryRewrite(current);
 822       d_ppCache[current] = ppRewritten;
 823       Assert(Rewriter::rewrite(d_ppCache[current]) == d_ppCache[current]);
 824       continue;
 825     }
 826
 827     // Not yet substituted, so process
 828     if (stackHead.children_added) {
 829       // Children have been processed, so substitute
 830       NodeBuilder<> builder(current.getKind());
 831       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
 832         builder << current.getOperator();
 833       }
 834       for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
 835         Assert(d_ppCache.find(current[i]) != d_ppCache.end());
 836         builder << d_ppCache[current[i]];
 837       }
 838       // Mark the substitution and continue
 839       Node result = builder;
 840       if (result != current) {
 841         result = Rewriter::rewrite(result);
 842       }
 843       Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): setting " << current << " -> " << result << endl;
 844       d_ppCache[current] = result;
 845       toVisit.pop_back();
 846     } else {
 847       // Mark that we have added the children if any
 848       if (current.getNumChildren() > 0) {
 849         stackHead.children_added = true;
 850         // We need to add the children
 851         for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
 852           TNode childNode = *child_it;
 853           NodeMap::iterator childFind = d_ppCache.find(childNode);
 854           if (childFind == d_ppCache.end()) {
 855             toVisit.push_back(childNode);
 856           }
 857         }
 858       } else {
 859         // No children, so we're done
 860         Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << assertion << "): setting " << current << " -> " << current << endl;
 861         d_ppCache[current] = current;
 862         toVisit.pop_back();
 863       }
 864     }
 865   }
 866
 867   // Return the substituted version
 868   return d_ppCache[assertion];
 869 }
 870
 871 bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
 872
 873   // What and where we are asserting
 874   NodeTheoryPair toAssert(assertion, toTheoryId, d_propagationMapTimestamp);
 875   // What and where it came from
 876   NodeTheoryPair toExplain(originalAssertion, fromTheoryId, d_propagationMapTimestamp);
 877
 878   // See if the theory already got this literal
 879   PropagationMap::const_iterator find = d_propagationMap.find(toAssert);
 880   if (find != d_propagationMap.end()) {
 881     // The theory already knows this
 882     Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): already there" << endl;
 883     return false;
 884   }
 885
 886   Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): marking [" << d_propagationMapTimestamp << "] " << assertion << ", " << toTheoryId << " from " << originalAssertion << ", " << fromTheoryId << endl;
 887
 888   // Mark the propagation
 889   d_propagationMap[toAssert] = toExplain;
 890   d_propagationMapTimestamp = d_propagationMapTimestamp + 1;
 891
 892   return true;
 893 }
 894
 895
 896 void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
 897
 898   Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << endl;
 899
 900   Assert(toTheoryId != fromTheoryId);
 901   if(! d_logicInfo.isTheoryEnabled(toTheoryId) &&
 902      toTheoryId != THEORY_SAT_SOLVER) {
 903     stringstream ss;
 904     ss << "The logic was specified as " << d_logicInfo.getLogicString()
 905        << ", which doesn't include " << toTheoryId
 906        << ", but got an asserted fact to that theory." << endl
 907        << "The fact:" << endl
 908        << assertion;
 909     throw LogicException(ss.str());
 910   }
 911
 912   if (d_inConflict) {
 913     return;
 914   }
 915
 916   // If sharing is disabled, things are easy
 917   if (!d_logicInfo.isSharingEnabled()) {
 918     Assert(assertion == originalAssertion);
 919     if (fromTheoryId == THEORY_SAT_SOLVER) {
 920       // Send to the apropriate theory
 921       theory::Theory* toTheory = theoryOf(toTheoryId);
 922       // We assert it, and we know it's preregistereed
 923       toTheory->assertFact(assertion, true);
 924       // Mark that we have more information
 925       d_factsAsserted = true;
 926     } else {
 927       Assert(toTheoryId == THEORY_SAT_SOLVER);
 928       // Check for propositional conflict
 929       bool value;
 930       if (d_propEngine->hasValue(assertion, value)) {
 931         if (!value) {
 932           Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict" << endl;
 933           d_inConflict = true;
 934         } else {
 935           return;
 936         }
 937       }
 938       d_propagatedLiterals.push_back(assertion);
 939     }
 940     return;
 941   }
 942
 943   // Polarity of the assertion
 944   bool polarity = assertion.getKind() != kind::NOT;
 945
 946   // Atom of the assertion
 947   TNode atom = polarity ? assertion : assertion[0];
 948
 949   // If sending to the shared terms database, it's also simple
 950   if (toTheoryId == THEORY_BUILTIN) {
 951     Assert(atom.getKind() == kind::EQUAL, "atom should be an EQUALity, not `%s'", atom.toString().c_str());
 952     if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
 953       d_sharedTerms.assertEquality(atom, polarity, assertion);
 954     }
 955     return;
 956   }
 957
 958   // Things from the SAT solver are already normalized, so they go
 959   // directly to the apropriate theory
 960   if (fromTheoryId == THEORY_SAT_SOLVER) {
 961     // We know that this is normalized, so just send it off to the theory
 962     if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
 963       // Is it preregistered
 964       bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
 965       // We assert it
 966       theoryOf(toTheoryId)->assertFact(assertion, preregistered);
 967       // Mark that we have more information
 968       d_factsAsserted = true;
 969     }
 970     return;
 971   }
 972
 973   // Propagations to the SAT solver are just enqueued for pickup by
 974   // the SAT solver later
 975   if (toTheoryId == THEORY_SAT_SOLVER) {
 976     if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
 977       // Enqueue for propagation to the SAT solver
 978       d_propagatedLiterals.push_back(assertion);
 979       // Check for propositional conflicts
 980       bool value;
 981       if (d_propEngine->hasValue(assertion, value) && !value) {
 982         d_inConflict = true;
 983       }
 984     }
 985     return;
 986   }
 987
 988   Assert(atom.getKind() == kind::EQUAL);
 989
 990   // Normalize
 991   Node normalizedLiteral = Rewriter::rewrite(assertion);
 992
 993   // See if it rewrites false directly -> conflict
 994   if (normalizedLiteral.isConst()) {
 995     if (!normalizedLiteral.getConst<bool>()) {
 996       // Mark the propagation for explanations
 997       if (markPropagation(normalizedLiteral, originalAssertion, toTheoryId, fromTheoryId)) {
 998         // Get the explanation (conflict will figure out where it came from)
 999         conflict(normalizedLiteral, toTheoryId);
1000       } else {
1001         Unreachable();
1002       }
1003       return;
1004     }
1005   }
1006
1007   // Try and assert (note that we assert the non-normalized one)
1008   if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
1009     // Check if has been pre-registered with the theory
1010     bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
1011     // Assert away
1012     theoryOf(toTheoryId)->assertFact(assertion, preregistered);
1013     d_factsAsserted = true;
1014   }
1015
1016   return;
1017 }
1018
1019 void TheoryEngine::assertFact(TNode literal)
1020 {
1021   Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << endl;
1022
1023   d_propEngine->checkTime();
1024
1025   // If we're in conflict, nothing to do
1026   if (d_inConflict) {
1027     return;
1028   }
1029
1030   // Get the atom
1031   bool polarity = literal.getKind() != kind::NOT;
1032   TNode atom = polarity ? literal : literal[0];
1033
1034   if (d_logicInfo.isSharingEnabled()) {
1035
1036     // If any shared terms, it's time to do sharing work
1037     if (d_sharedTerms.hasSharedTerms(atom)) {
1038       // Notify the theories the shared terms
1039       SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom);
1040       SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom);
1041       for (; it != it_end; ++ it) {
1042         TNode term = *it;
1043         Theory::Set theories = d_sharedTerms.getTheoriesToNotify(atom, term);
1044         for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++ id) {
1045           if (Theory::setContains(id, theories)) {
1046             theoryOf(id)->addSharedTermInternal(term);
1047           }
1048         }
1049         d_sharedTerms.markNotified(term, theories);
1050       }
1051     }
1052
1053     // If it's an equality, assert it to the shared term manager, even though the terms are not
1054     // yet shared. As the terms become shared later, the shared terms manager will then add them
1055     // to the assert the equality to the interested theories
1056     if (atom.getKind() == kind::EQUAL) {
1057       // Assert it to the the owning theory
1058       assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
1059       // Shared terms manager will assert to interested theories directly, as the terms become shared
1060       assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ THEORY_SAT_SOLVER);
1061
1062       // Now, let's check for any atom triggers from lemmas
1063       AtomRequests::atom_iterator it = d_atomRequests.getAtomIterator(atom);
1064       while (!it.done()) {
1065         const AtomRequests::Request& request = it.get();
1066         Node toAssert = polarity ? (Node) request.atom : request.atom.notNode();
1067         Debug("theory::atoms") << "TheoryEngine::assertFact(" << literal << "): sending requested " << toAssert << endl;
1068         assertToTheory(toAssert, literal, request.toTheory, THEORY_SAT_SOLVER);
1069         it.next();
1070       }
1071
1072     } else {
1073       // Not an equality, just assert to the appropriate theory
1074       assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
1075     }
1076   } else {
1077     // Assert the fact to the appropriate theory directly
1078     assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
1079   }
1080 }
1081
1082 bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
1083
1084   Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl;
1085
1086   d_propEngine->checkTime();
1087
1088   if(Dump.isOn("t-propagations")) {
1089     Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid")
1090                            << QueryCommand(literal.toExpr());
1091   }
1092   if(Dump.isOn("missed-t-propagations")) {
1093     d_hasPropagated.insert(literal);
1094   }
1095
1096   // Get the atom
1097   bool polarity = literal.getKind() != kind::NOT;
1098   TNode atom = polarity ? literal : literal[0];
1099
1100   if (d_logicInfo.isSharingEnabled() && atom.getKind() == kind::EQUAL) {
1101     if (d_propEngine->isSatLiteral(literal)) {
1102       // We propagate SAT literals to SAT
1103       assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
1104     }
1105     if (theory != THEORY_BUILTIN) {
1106       // Assert to the shared terms database
1107       assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory);
1108     }
1109   } else {
1110     // Just send off to the SAT solver
1111     Assert(d_propEngine->isSatLiteral(literal));
1112     assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
1113   }
1114
1115   return !d_inConflict;
1116 }
1117
1118
1119 theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
1120   Assert(a.getType().isComparableTo(b.getType()));
1121   if (d_sharedTerms.isShared(a) && d_sharedTerms.isShared(b)) {
1122     if (d_sharedTerms.areEqual(a,b)) {
1123       return EQUALITY_TRUE_AND_PROPAGATED;
1124     }
1125     else if (d_sharedTerms.areDisequal(a,b)) {
1126       return EQUALITY_FALSE_AND_PROPAGATED;
1127     }
1128   }
1129   return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
1130 }
1131
1132 Node TheoryEngine::getModelValue(TNode var) {
1133   Assert(d_sharedTerms.isShared(var));
1134   return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
1135 }
1136
1137 static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
1138
1139   std::set<TNode> all;
1140   for (unsigned i = 0; i < explanation.size(); ++ i) {
1141     Assert(explanation[i].theory == THEORY_SAT_SOLVER);
1142     all.insert(explanation[i].node);
1143   }
1144
1145   if (all.size() == 0) {
1146     // Normalize to true
1147     return NodeManager::currentNM()->mkConst<bool>(true);
1148   }
1149
1150   if (all.size() == 1) {
1151     // All the same, or just one
1152     return explanation[0].node;
1153   }
1154
1155   NodeBuilder<> conjunction(kind::AND);
1156   std::set<TNode>::const_iterator it = all.begin();
1157   std::set<TNode>::const_iterator it_end = all.end();
1158   while (it != it_end) {
1159     conjunction << *it;
1160     ++ it;
1161   }
1162
1163   return conjunction;
1164 }
1165
1166
1167 Node TheoryEngine::getExplanation(TNode node) {
1168   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << endl;
1169
1170   bool polarity = node.getKind() != kind::NOT;
1171   TNode atom = polarity ? node : node[0];
1172
1173   // If we're not in shared mode, explanations are simple
1174   if (!d_logicInfo.isSharingEnabled()) {
1175     Node explanation = theoryOf(atom)->explain(node);
1176     Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
1177     return explanation;
1178   }
1179
1180   // Initial thing to explain
1181   NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp);
1182   Assert(d_propagationMap.find(toExplain) != d_propagationMap.end());
1183   // Create the workplace for explanations
1184   std::vector<NodeTheoryPair> explanationVector;
1185   explanationVector.push_back(d_propagationMap[toExplain]);
1186   // Process the explanation
1187   getExplanation(explanationVector);
1188   Node explanation = mkExplanation(explanationVector);
1189
1190   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
1191
1192   return explanation;
1193 }
1194
1195 struct AtomsCollect {
1196
1197   std::vector<TNode> d_atoms;
1198   std::hash_set<TNode, TNodeHashFunction> d_visited;
1199
1200 public:
1201
1202   typedef void return_type;
1203
1204   bool alreadyVisited(TNode current, TNode parent) {
1205     // Check if already visited
1206     d_visited.find(current) != d_visited.end();
1207     // Don't visit non-boolean
1208     if (!current.getType().isBoolean()) return true;
1209     // New node
1210     return false;
1211   }
1212
1213   void visit(TNode current, TNode parent) {
1214     if (Theory::theoryOf(current) != theory::THEORY_BOOL) {
1215       d_atoms.push_back(current);
1216     }
1217     d_visited.insert(current);
1218   }
1219
1220   void start(TNode node) {}
1221   void done(TNode node) {}
1222
1223   std::vector<TNode> getAtoms() const {
1224     return d_atoms;
1225   }
1226 };
1227
1228 void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId atomsTo) {
1229   for (unsigned i = 0; i < atoms.size(); ++ i) {
1230
1231     // Non-equality atoms are either owned by theory or they don't make sense
1232     if (atoms[i].getKind() != kind::EQUAL) {
1233       continue;
1234     }
1235
1236     // The equality
1237     Node eq = atoms[i];
1238     // Simple normalization to not repeat stuff
1239     if (eq[0] > eq[1]) {
1240       eq = eq[1].eqNode(eq[0]);
1241     }
1242
1243     // Rewrite the equality
1244     Node eqNormalized = Rewriter::rewrite(atoms[i]);
1245
1246     Debug("theory::atoms") << "TheoryEngine::ensureLemmaAtoms(): " << eq << " with nf " << eqNormalized << endl;
1247
1248     // If the equality is a boolean constant, we send immediately
1249     if (eqNormalized.isConst()) {
1250       if (eqNormalized.getConst<bool>()) {
1251         assertToTheory(eq, eqNormalized, /** to */ atomsTo, /** Sat solver */ theory::THEORY_SAT_SOLVER);
1252       } else {
1253         assertToTheory(eq.notNode(), eqNormalized.notNode(), /** to */ atomsTo, /** Sat solver */ theory::THEORY_SAT_SOLVER);
1254       }
1255       continue;
1256     }
1257
1258     Assert(eqNormalized.getKind() == kind::EQUAL);
1259
1260
1261     // If the normalization did the just flips, keep the flip
1262     if (eqNormalized[0] == eq[1] && eqNormalized[1] == eq[0]) {
1263       eq = eqNormalized;
1264     }
1265
1266     // Check if the equality is already known by the sat solver
1267     if (d_propEngine->isSatLiteral(eqNormalized)) {
1268       bool value;
1269       if (d_propEngine->hasValue(eqNormalized, value)) {
1270         if (value) {
1271           assertToTheory(eq, eqNormalized, atomsTo, theory::THEORY_SAT_SOLVER);
1272           continue;
1273         } else {
1274           assertToTheory(eq.notNode(), eqNormalized.notNode(), atomsTo, theory::THEORY_SAT_SOLVER);
1275           continue;
1276         }
1277       }
1278     }
1279
1280     // If the theory is asking about a different form, or the form is ok but if will go to a different theory
1281     // then we must figure it out
1282     if (eqNormalized != eq || Theory::theoryOf(eq) != atomsTo) {
1283       // If you get eqNormalized, send atoms[i] to atomsTo
1284       d_atomRequests.add(eqNormalized, eq, atomsTo);
1285     }
1286   }
1287 }
1288
1289 theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, theory::TheoryId atomsTo) {
1290
1291   // Do we need to check atoms
1292   if (atomsTo != theory::THEORY_LAST) {
1293     Debug("theory::atoms") << "TheoryEngine::lemma(" << node << ", " << atomsTo << ")" << endl;
1294     AtomsCollect collectAtoms;
1295     NodeVisitor<AtomsCollect>::run(collectAtoms, node);
1296     ensureLemmaAtoms(collectAtoms.getAtoms(), atomsTo);
1297   }
1298
1299   if(Dump.isOn("t-lemmas")) {
1300     Node n = node;
1301     if (negated) {
1302       n = node.negate();
1303     }
1304     Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
1305                      << QueryCommand(n.toExpr());
1306   }
1307
1308   // Share with other portfolio threads
1309   if(options::lemmaOutputChannel() != NULL) {
1310     options::lemmaOutputChannel()->notifyNewLemma(node.toExpr());
1311   }
1312
1313   // Remove the ITEs
1314   std::vector<Node> additionalLemmas;
1315   IteSkolemMap iteSkolemMap;
1316   additionalLemmas.push_back(node);
1317   d_iteRemover.run(additionalLemmas, iteSkolemMap);
1318   additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]);
1319
1320   if(Trace.isOn("lemma-ites")) {
1321     Debug("lemma-ites") << "removed ITEs from lemma: " << node << endl;
1322     Debug("lemma-ites") << " + now have the following "
1323                         << additionalLemmas.size() << " lemma(s):" << endl;
1324     for(std::vector<Node>::const_iterator i = additionalLemmas.begin();
1325         i != additionalLemmas.end();
1326         ++i) {
1327       Debug("lemma-ites") << " + " << *i << endl;
1328     }
1329     Debug("lemma-ites") << endl;
1330   }
1331
1332   // assert to prop engine
1333   d_propEngine->assertLemma(additionalLemmas[0], negated, removable);
1334   for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
1335     additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]);
1336     d_propEngine->assertLemma(additionalLemmas[i], false, removable);
1337   }
1338
1339   // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
1340   // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
1341   if(negated) {
1342     // Can't we just get rid of passing around this 'negated' stuff?
1343     // Is it that hard for the propEngine to figure that out itself?
1344     // (I like the use of triple negation <evil laugh>.) --K
1345     additionalLemmas[0] = additionalLemmas[0].notNode();
1346     negated = false;
1347   }
1348   // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
1349   // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
1350
1351   // assert to decision engine
1352   if(!removable) {
1353     d_decisionEngine->addAssertions(additionalLemmas, 1, iteSkolemMap);
1354   }
1355
1356   // Mark that we added some lemmas
1357   d_lemmasAdded = true;
1358
1359   // Lemma analysis isn't online yet; this lemma may only live for this
1360   // user level.
1361   return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel());
1362 }
1363
1364 void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
1365
1366   Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << endl;
1367
1368   // Mark that we are in conflict
1369   d_inConflict = true;
1370
1371   if(Dump.isOn("t-conflicts")) {
1372     Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat")
1373                         << CheckSatCommand(conflict.toExpr());
1374   }
1375
1376   // In the multiple-theories case, we need to reconstruct the conflict
1377   if (d_logicInfo.isSharingEnabled()) {
1378     // Create the workplace for explanations
1379     std::vector<NodeTheoryPair> explanationVector;
1380     explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
1381     // Process the explanation
1382     getExplanation(explanationVector);
1383     Node fullConflict = mkExplanation(explanationVector);
1384     Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
1385     Assert(properConflict(fullConflict));
1386     lemma(fullConflict, true, true, THEORY_LAST);
1387   } else {
1388     // When only one theory, the conflict should need no processing
1389     Assert(properConflict(conflict));
1390     lemma(conflict, true, true, THEORY_LAST);
1391   }
1392 }
1393
1394 void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
1395   d_bvToBoolPreprocessor.liftBoolToBV(assertions, new_assertions);
1396 }
1397
1398 Node TheoryEngine::ppSimpITE(TNode assertion)
1399 {
1400   Node result = d_iteSimplifier.simpITE(assertion);
1401   result = d_iteSimplifier.simplifyWithCare(Rewriter::rewrite(result));
1402   result = Rewriter::rewrite(result);
1403   return result;
1404 }
1405
1406 void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector)
1407 {
1408   Assert(explanationVector.size() > 0);
1409
1410   unsigned i = 0; // Index of the current literal we are processing
1411   unsigned j = 0; // Index of the last literal we are keeping
1412
1413   while (i < explanationVector.size()) {
1414
1415     // Get the current literal to explain
1416     NodeTheoryPair toExplain = explanationVector[i];
1417
1418     Debug("theory::explain") << "TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl;
1419
1420     // If a treu constant or a negation of a false constant we can ignore it
1421     if (toExplain.node.isConst() && toExplain.node.getConst<bool>()) {
1422       ++ i;
1423       continue;
1424     }
1425     if (toExplain.node.getKind() == kind::NOT && toExplain.node[0].isConst() && !toExplain.node[0].getConst<bool>()) {
1426       ++ i;
1427       continue;
1428     }
1429
1430     // If from the SAT solver, keep it
1431     if (toExplain.theory == THEORY_SAT_SOLVER) {
1432       explanationVector[j++] = explanationVector[i++];
1433       continue;
1434     }
1435
1436     // If an and, expand it
1437     if (toExplain.node.getKind() == kind::AND) {
1438       Debug("theory::explain") << "TheoryEngine::explain(): expanding " << toExplain.node << " got from " << toExplain.theory << endl;
1439       for (unsigned k = 0; k < toExplain.node.getNumChildren(); ++ k) {
1440         NodeTheoryPair newExplain(toExplain.node[k], toExplain.theory, toExplain.timestamp);
1441         explanationVector.push_back(newExplain);
1442       }
1443       ++ i;
1444       continue;
1445     }
1446
1447     // See if it was sent to the theory by another theory
1448     PropagationMap::const_iterator find = d_propagationMap.find(toExplain);
1449     if (find != d_propagationMap.end()) {
1450       // There is some propagation, check if its a timely one
1451       if ((*find).second.timestamp < toExplain.timestamp) {
1452         explanationVector.push_back((*find).second);
1453         ++ i;
1454         continue;
1455       }
1456     }
1457
1458     // It was produced by the theory, so ask for an explanation
1459     Node explanation;
1460     if (toExplain.theory == THEORY_BUILTIN) {
1461       explanation = d_sharedTerms.explain(toExplain.node);
1462     } else {
1463       explanation = theoryOf(toExplain.theory)->explain(toExplain.node);
1464     }
1465     Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << endl;
1466     Assert(explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially");
1467     // Mark the explanation
1468     NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp);
1469     explanationVector.push_back(newExplain);
1470     ++ i;
1471   }
1472
1473   // Keep only the relevant literals
1474   explanationVector.resize(j);
1475 }
1476
1477
1478 void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions)
1479 {
1480   d_unconstrainedSimp.processAssertions(assertions);
1481 }
1482
1483
1484 void TheoryEngine::setUserAttribute(const std::string& attr, Node n) {
1485   Trace("te-attr") << "set user attribute " << attr << " " << n << endl;
1486   if( d_attr_handle.find( attr )!=d_attr_handle.end() ){
1487     for( size_t i=0; i<d_attr_handle[attr].size(); i++ ){
1488       d_attr_handle[attr][i]->setUserAttribute(attr, n);
1489     }
1490   } else {
1491     //unhandled exception?
1492   }
1493 }
1494
1495 void TheoryEngine::handleUserAttribute(const char* attr, Theory* t) {
1496   Trace("te-attr") << "Handle user attribute " << attr << " " << t << endl;
1497   std::string str( attr );
1498   d_attr_handle[ str ].push_back( t );
1499 }
1500
1501 void TheoryEngine::checkTheoryAssertionsWithModel() {
1502   for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
1503     if(theoryId != THEORY_REWRITERULES) {
1504       Theory* theory = d_theoryTable[theoryId];
1505       if(theory && d_logicInfo.isTheoryEnabled(theoryId)) {
1506         for(context::CDList<Assertion>::const_iterator it = theory->facts_begin(),
1507               it_end = theory->facts_end();
1508             it != it_end;
1509             ++it) {
1510           Node assertion = (*it).assertion;
1511           Node val = getModel()->getValue(assertion);
1512           if(val != d_true) {
1513             stringstream ss;
1514             ss << theoryId << " has an asserted fact that the model doesn't satisfy." << endl
1515                << "The fact: " << assertion << endl
1516                << "Model value: " << val << endl;
1517             InternalError(ss.str());
1518           }
1519         }
1520       }
1521     }
1522   }
1523 }