src/theory/theory_engine.cpp

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