src/theory/theory_engine.cpp

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