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