src/theory/theory_engine.cpp

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