src/theory/theory_engine.cpp

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