src/theory/theory_engine.cpp

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