1 /********************* */ 2 /*! \file theory_engine.h 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 "cvc4_private.h" 18 19 #ifndef __CVC4__THEORY_ENGINE_H 20 #define __CVC4__THEORY_ENGINE_H 21 22 #include <deque> 23 #include <memory> 24 #include <set> 25 #include <unordered_map> 26 #include <vector> 27 #include <utility> 28 29 #include "base/cvc4_assert.h" 30 #include "context/cdhashset.h" 31 #include "expr/node.h" 32 #include "options/options.h" 33 #include "options/smt_options.h" 34 #include "prop/prop_engine.h" 35 #include "smt/command.h" 36 #include "smt_util/lemma_channels.h" 37 #include "theory/atom_requests.h" 38 #include "theory/decision_manager.h" 39 #include "theory/interrupted.h" 40 #include "theory/rewriter.h" 41 #include "theory/shared_terms_database.h" 42 #include "theory/sort_inference.h" 43 #include "theory/substitutions.h" 44 #include "theory/term_registration_visitor.h" 45 #include "theory/theory.h" 46 #include "theory/uf/equality_engine.h" 47 #include "theory/valuation.h" 48 #include "util/hash.h" 49 #include "util/statistics_registry.h" 50 #include "util/unsafe_interrupt_exception.h" 51 52 namespace CVC4 { 53 54 class ResourceManager; 55 class LemmaProofRecipe; 56 57 /** 58 * A pair of a theory and a node. This is used to mark the flow of 59 * propagations between theories. 60 */ 61 struct NodeTheoryPair { 62 Node node; 63 theory::TheoryId theory; 64 size_t timestamp; 65 NodeTheoryPair(TNode node, theory::TheoryId theory, size_t timestamp = 0) nodeNodeTheoryPair66 : node(node), theory(theory), timestamp(timestamp) {} NodeTheoryPairNodeTheoryPair67 NodeTheoryPair() : theory(theory::THEORY_LAST), timestamp() {} 68 // Comparison doesn't take into account the timestamp 69 bool operator == (const NodeTheoryPair& pair) const { 70 return node == pair.node && theory == pair.theory; 71 } 72 };/* struct NodeTheoryPair */ 73 74 struct NodeTheoryPairHashFunction { 75 NodeHashFunction hashFunction; 76 // Hash doesn't take into account the timestamp operatorNodeTheoryPairHashFunction77 size_t operator()(const NodeTheoryPair& pair) const { 78 uint64_t hash = fnv1a::fnv1a_64(NodeHashFunction()(pair.node)); 79 return static_cast<size_t>(fnv1a::fnv1a_64(pair.theory, hash)); 80 } 81 };/* struct NodeTheoryPairHashFunction */ 82 83 84 /* Forward declarations */ 85 namespace theory { 86 class TheoryModel; 87 class TheoryEngineModelBuilder; 88 89 namespace eq { 90 class EqualityEngine; 91 }/* CVC4::theory::eq namespace */ 92 93 namespace quantifiers { 94 class TermDb; 95 } 96 97 class EntailmentCheckParameters; 98 class EntailmentCheckSideEffects; 99 }/* CVC4::theory namespace */ 100 101 class DecisionEngine; 102 class RemoveTermFormulas; 103 104 /** 105 * This is essentially an abstraction for a collection of theories. A 106 * TheoryEngine provides services to a PropEngine, making various 107 * T-solvers look like a single unit to the propositional part of 108 * CVC4. 109 */ 110 class TheoryEngine { 111 112 /** Shared terms database can use the internals notify the theories */ 113 friend class SharedTermsDatabase; 114 friend class theory::quantifiers::TermDb; 115 116 /** Associated PropEngine engine */ 117 prop::PropEngine* d_propEngine; 118 119 /** Access to decision engine */ 120 DecisionEngine* d_decisionEngine; 121 122 /** Our context */ 123 context::Context* d_context; 124 125 /** Our user context */ 126 context::UserContext* d_userContext; 127 128 /** 129 * A table of from theory IDs to theory pointers. Never use this table 130 * directly, use theoryOf() instead. 131 */ 132 theory::Theory* d_theoryTable[theory::THEORY_LAST]; 133 134 /** 135 * A collection of theories that are "active" for the current run. 136 * This set is provided by the user (as a logic string, say, in SMT-LIBv2 137 * format input), or else by default it's all-inclusive. This is important 138 * because we can optimize for single-theory runs (no sharing), can reduce 139 * the cost of walking the DAG on registration, etc. 140 */ 141 const LogicInfo& d_logicInfo; 142 143 /** 144 * The database of shared terms. 145 */ 146 SharedTermsDatabase d_sharedTerms; 147 148 /** 149 * Master equality engine, to share with theories. 150 */ 151 theory::eq::EqualityEngine* d_masterEqualityEngine; 152 153 /** notify class for master equality engine */ 154 class NotifyClass : public theory::eq::EqualityEngineNotify { 155 TheoryEngine& d_te; 156 public: NotifyClass(TheoryEngine & te)157 NotifyClass(TheoryEngine& te): d_te(te) {} eqNotifyTriggerEquality(TNode equality,bool value)158 bool eqNotifyTriggerEquality(TNode equality, bool value) override 159 { 160 return true; 161 } eqNotifyTriggerPredicate(TNode predicate,bool value)162 bool eqNotifyTriggerPredicate(TNode predicate, bool value) override 163 { 164 return true; 165 } eqNotifyTriggerTermEquality(theory::TheoryId tag,TNode t1,TNode t2,bool value)166 bool eqNotifyTriggerTermEquality(theory::TheoryId tag, 167 TNode t1, 168 TNode t2, 169 bool value) override 170 { 171 return true; 172 } eqNotifyConstantTermMerge(TNode t1,TNode t2)173 void eqNotifyConstantTermMerge(TNode t1, TNode t2) override {} eqNotifyNewClass(TNode t)174 void eqNotifyNewClass(TNode t) override { d_te.eqNotifyNewClass(t); } eqNotifyPreMerge(TNode t1,TNode t2)175 void eqNotifyPreMerge(TNode t1, TNode t2) override 176 { 177 d_te.eqNotifyPreMerge(t1, t2); 178 } eqNotifyPostMerge(TNode t1,TNode t2)179 void eqNotifyPostMerge(TNode t1, TNode t2) override 180 { 181 d_te.eqNotifyPostMerge(t1, t2); 182 } eqNotifyDisequal(TNode t1,TNode t2,TNode reason)183 void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override 184 { 185 d_te.eqNotifyDisequal(t1, t2, reason); 186 } 187 };/* class TheoryEngine::NotifyClass */ 188 NotifyClass d_masterEENotify; 189 190 /** 191 * notification methods 192 */ 193 void eqNotifyNewClass(TNode t); 194 void eqNotifyPreMerge(TNode t1, TNode t2); 195 void eqNotifyPostMerge(TNode t1, TNode t2); 196 void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); 197 198 /** 199 * The quantifiers engine 200 */ 201 theory::QuantifiersEngine* d_quantEngine; 202 /** 203 * The decision manager 204 */ 205 std::unique_ptr<theory::DecisionManager> d_decManager; 206 207 /** 208 * Default model object 209 */ 210 theory::TheoryModel* d_curr_model; 211 bool d_aloc_curr_model; 212 /** 213 * Model builder object 214 */ 215 theory::TheoryEngineModelBuilder* d_curr_model_builder; 216 bool d_aloc_curr_model_builder; 217 /** are we in eager model building mode? (see setEagerModelBuilding). */ 218 bool d_eager_model_building; 219 220 typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; 221 typedef std::unordered_map<TNode, Node, TNodeHashFunction> TNodeMap; 222 223 /** 224 * Cache for theory-preprocessing of assertions 225 */ 226 NodeMap d_ppCache; 227 228 /** 229 * Used for "missed-t-propagations" dumping mode only. A set of all 230 * theory-propagable literals. 231 */ 232 context::CDList<TNode> d_possiblePropagations; 233 234 /** 235 * Used for "missed-t-propagations" dumping mode only. A 236 * context-dependent set of those theory-propagable literals that 237 * have been propagated. 238 */ 239 context::CDHashSet<Node, NodeHashFunction> d_hasPropagated; 240 241 242 /** 243 * Statistics for a particular theory. 244 */ 245 class Statistics { 246 mkName(std::string prefix,theory::TheoryId theory,std::string suffix)247 static std::string mkName(std::string prefix, 248 theory::TheoryId theory, 249 std::string suffix) { 250 std::stringstream ss; 251 ss << prefix << theory << suffix; 252 return ss.str(); 253 } 254 255 public: 256 IntStat conflicts, propagations, lemmas, requirePhase, restartDemands; 257 258 Statistics(theory::TheoryId theory); 259 ~Statistics(); 260 };/* class TheoryEngine::Statistics */ 261 262 /** 263 * An output channel for Theory that passes messages 264 * back to a TheoryEngine. 265 */ 266 class EngineOutputChannel : public theory::OutputChannel { 267 friend class TheoryEngine; 268 269 /** 270 * The theory engine we're communicating with. 271 */ 272 TheoryEngine* d_engine; 273 274 /** 275 * The statistics of the theory interractions. 276 */ 277 Statistics d_statistics; 278 279 /** The theory owning this channel. */ 280 theory::TheoryId d_theory; 281 282 public: EngineOutputChannel(TheoryEngine * engine,theory::TheoryId theory)283 EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory) 284 : d_engine(engine), d_statistics(theory), d_theory(theory) {} 285 safePoint(uint64_t amount)286 void safePoint(uint64_t amount) override { 287 spendResource(amount); 288 if (d_engine->d_interrupted) { 289 throw theory::Interrupted(); 290 } 291 } 292 293 void conflict(TNode conflictNode, 294 std::unique_ptr<Proof> pf = nullptr) override; 295 bool propagate(TNode literal) override; 296 297 theory::LemmaStatus lemma(TNode lemma, ProofRule rule, 298 bool removable = false, bool preprocess = false, 299 bool sendAtoms = false) override; 300 301 theory::LemmaStatus splitLemma(TNode lemma, 302 bool removable = false) override; 303 demandRestart()304 void demandRestart() override { 305 NodeManager* curr = NodeManager::currentNM(); 306 Node restartVar = curr->mkSkolem( 307 "restartVar", curr->booleanType(), 308 "A boolean variable asserted to be true to force a restart"); 309 Trace("theory::restart") 310 << "EngineOutputChannel<" << d_theory << ">::restart(" << restartVar 311 << ")" << std::endl; 312 ++d_statistics.restartDemands; 313 lemma(restartVar, RULE_INVALID, true); 314 } 315 requirePhase(TNode n,bool phase)316 void requirePhase(TNode n, bool phase) override { 317 Debug("theory") << "EngineOutputChannel::requirePhase(" << n << ", " 318 << phase << ")" << std::endl; 319 ++d_statistics.requirePhase; 320 d_engine->d_propEngine->requirePhase(n, phase); 321 } 322 setIncomplete()323 void setIncomplete() override { 324 Trace("theory") << "TheoryEngine::setIncomplete()" << std::endl; 325 d_engine->setIncomplete(d_theory); 326 } 327 spendResource(unsigned amount)328 void spendResource(unsigned amount) override { 329 d_engine->spendResource(amount); 330 } 331 handleUserAttribute(const char * attr,theory::Theory * t)332 void handleUserAttribute(const char* attr, theory::Theory* t) override { 333 d_engine->handleUserAttribute(attr, t); 334 } 335 336 private: 337 /** 338 * A helper function for registering lemma recipes with the proof engine 339 */ 340 void registerLemmaRecipe(Node lemma, Node originalLemma, bool preprocess, 341 theory::TheoryId theoryId); 342 }; /* class TheoryEngine::EngineOutputChannel */ 343 344 /** 345 * Output channels for individual theories. 346 */ 347 EngineOutputChannel* d_theoryOut[theory::THEORY_LAST]; 348 349 /** 350 * Are we in conflict. 351 */ 352 context::CDO<bool> d_inConflict; 353 354 /** 355 * Are we in "SAT mode"? In this state, the user can query for the model. 356 * This corresponds to the state in Figure 4.1, page 52 of the SMT-LIB 357 * standard, version 2.6. 358 */ 359 bool d_inSatMode; 360 361 /** 362 * Called by the theories to notify of a conflict. 363 */ 364 void conflict(TNode conflict, theory::TheoryId theoryId); 365 366 /** 367 * Debugging flag to ensure that shutdown() is called before the 368 * destructor. 369 */ 370 bool d_hasShutDown; 371 372 /** 373 * True if a theory has notified us of incompleteness (at this 374 * context level or below). 375 */ 376 context::CDO<bool> d_incomplete; 377 378 /** 379 * Called by the theories to notify that the current branch is incomplete. 380 */ setIncomplete(theory::TheoryId theory)381 void setIncomplete(theory::TheoryId theory) { 382 d_incomplete = true; 383 } 384 385 386 /** 387 * Mapping of propagations from recievers to senders. 388 */ 389 typedef context::CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> PropagationMap; 390 PropagationMap d_propagationMap; 391 392 /** 393 * Timestamp of propagations 394 */ 395 context::CDO<size_t> d_propagationMapTimestamp; 396 397 /** 398 * Literals that are propagated by the theory. Note that these are TNodes. 399 * The theory can only propagate nodes that have an assigned literal in the 400 * SAT solver and are hence referenced in the SAT solver. 401 */ 402 context::CDList<TNode> d_propagatedLiterals; 403 404 /** 405 * The index of the next literal to be propagated by a theory. 406 */ 407 context::CDO<unsigned> d_propagatedLiteralsIndex; 408 409 /** 410 * Called by the output channel to propagate literals and facts 411 * @return false if immediate conflict 412 */ 413 bool propagate(TNode literal, theory::TheoryId theory); 414 415 /** 416 * Internal method to call the propagation routines and collect the 417 * propagated literals. 418 */ 419 void propagate(theory::Theory::Effort effort); 420 421 /** 422 * A variable to mark if we added any lemmas. 423 */ 424 bool d_lemmasAdded; 425 426 /** 427 * A variable to mark if the OutputChannel was "used" by any theory 428 * since the start of the last check. If it has been, we require 429 * a FULL_EFFORT check before exiting and reporting SAT. 430 * 431 * See the documentation for the needCheck() function, below. 432 */ 433 bool d_outputChannelUsed; 434 435 /** Atom requests from lemmas */ 436 AtomRequests d_atomRequests; 437 438 /** 439 * Adds a new lemma, returning its status. 440 * @param node the lemma 441 * @param negated should the lemma be asserted negated 442 * @param removable can the lemma be remove (restrictions apply) 443 * @param needAtoms if not THEORY_LAST, then 444 */ 445 theory::LemmaStatus lemma(TNode node, 446 ProofRule rule, 447 bool negated, 448 bool removable, 449 bool preprocess, 450 theory::TheoryId atomsTo); 451 452 /** Enusre that the given atoms are send to the given theory */ 453 void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory); 454 455 RemoveTermFormulas& d_tform_remover; 456 457 /** sort inference module */ 458 SortInference d_sortInfer; 459 460 /** Time spent in theory combination */ 461 TimerStat d_combineTheoriesTime; 462 463 Node d_true; 464 Node d_false; 465 466 /** Whether we were just interrupted (or not) */ 467 bool d_interrupted; 468 ResourceManager* d_resourceManager; 469 470 /** Container for lemma input and output channels. */ 471 LemmaChannels* d_channels; 472 473 public: 474 475 /** Constructs a theory engine */ 476 TheoryEngine(context::Context* context, context::UserContext* userContext, 477 RemoveTermFormulas& iteRemover, const LogicInfo& logic, 478 LemmaChannels* channels); 479 480 /** Destroys a theory engine */ 481 ~TheoryEngine(); 482 483 void interrupt(); 484 485 /** "Spend" a resource during a search or preprocessing.*/ 486 void spendResource(unsigned amount); 487 488 /** 489 * Adds a theory. Only one theory per TheoryId can be present, so if 490 * there is another theory it will be deleted. 491 */ 492 template <class TheoryClass> addTheory(theory::TheoryId theoryId)493 inline void addTheory(theory::TheoryId theoryId) { 494 Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); 495 d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId); 496 d_theoryTable[theoryId] = 497 new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], 498 theory::Valuation(this), d_logicInfo); 499 } 500 setPropEngine(prop::PropEngine * propEngine)501 inline void setPropEngine(prop::PropEngine* propEngine) { 502 Assert(d_propEngine == NULL); 503 d_propEngine = propEngine; 504 } 505 setDecisionEngine(DecisionEngine * decisionEngine)506 inline void setDecisionEngine(DecisionEngine* decisionEngine) { 507 Assert(d_decisionEngine == NULL); 508 d_decisionEngine = decisionEngine; 509 } 510 511 /** Called when all initialization of options/logic is done */ 512 void finishInit(); 513 514 /** 515 * Get a pointer to the underlying propositional engine. 516 */ getPropEngine()517 inline prop::PropEngine* getPropEngine() const { 518 return d_propEngine; 519 } 520 521 /** 522 * Get a pointer to the underlying sat context. 523 */ getSatContext()524 inline context::Context* getSatContext() const { 525 return d_context; 526 } 527 528 /** 529 * Get a pointer to the underlying user context. 530 */ getUserContext()531 inline context::Context* getUserContext() const { 532 return d_userContext; 533 } 534 535 /** 536 * Get a pointer to the underlying quantifiers engine. 537 */ getQuantifiersEngine()538 theory::QuantifiersEngine* getQuantifiersEngine() const { 539 return d_quantEngine; 540 } 541 /** 542 * Get a pointer to the underlying decision manager. 543 */ getDecisionManager()544 theory::DecisionManager* getDecisionManager() const 545 { 546 return d_decManager.get(); 547 } 548 549 private: 550 /** 551 * Helper for preprocess 552 */ 553 Node ppTheoryRewrite(TNode term); 554 555 /** 556 * Queue of nodes for pre-registration. 557 */ 558 std::queue<TNode> d_preregisterQueue; 559 560 /** 561 * Boolean flag denoting we are in pre-registration. 562 */ 563 bool d_inPreregister; 564 565 /** 566 * Did the theories get any new facts since the last time we called 567 * check() 568 */ 569 context::CDO<bool> d_factsAsserted; 570 571 /** 572 * Map from equality atoms to theories that would like to be notified about them. 573 */ 574 575 576 /** 577 * Assert the formula to the given theory. 578 * @param assertion the assertion to send (not necesserily normalized) 579 * @param original the assertion as it was sent in from the propagating theory 580 * @param toTheoryId the theory to assert to 581 * @param fromTheoryId the theory that sent it 582 */ 583 void assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId); 584 585 /** 586 * Marks a theory propagation from a theory to a theory where a 587 * theory could be the THEORY_SAT_SOLVER for literals coming from 588 * or being propagated to the SAT solver. If the receiving theory 589 * already recieved the literal, the method returns false, otherwise 590 * it returns true. 591 * 592 * @param assertion the normalized assertion being sent 593 * @param originalAssertion the actual assertion that was sent 594 * @param toTheoryId the theory that is on the receiving end 595 * @param fromTheoryId the theory that sent the assertino 596 * @return true if a new assertion, false if theory already got it 597 */ 598 bool markPropagation(TNode assertion, TNode originalAssertions, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId); 599 600 /** 601 * Computes the explanation by travarsing the propagation graph and 602 * asking relevant theories to explain the propagations. Initially 603 * the explanation vector should contain only the element (node, theory) 604 * where the node is the one to be explained, and the theory is the 605 * theory that sent the literal. The lemmaProofRecipe will contain a list 606 * of the explanation steps required to produce the original node. 607 */ 608 void getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* lemmaProofRecipe); 609 610 public: 611 612 /** 613 * Signal the start of a new round of assertion preprocessing 614 */ 615 void preprocessStart(); 616 617 /** 618 * Runs theory specific preprocessing on the non-Boolean parts of 619 * the formula. This is only called on input assertions, after ITEs 620 * have been removed. 621 */ 622 Node preprocess(TNode node); 623 624 /** Notify (preprocessed) assertions. */ 625 void notifyPreprocessedAssertions(const std::vector<Node>& assertions); 626 627 /** Return whether or not we are incomplete (in the current context). */ isIncomplete()628 inline bool isIncomplete() const { return d_incomplete; } 629 630 /** 631 * Returns true if we need another round of checking. If this 632 * returns true, check(FULL_EFFORT) _must_ be called by the 633 * propositional layer before reporting SAT. 634 * 635 * This is especially necessary for incomplete theories that lazily 636 * output some lemmas on FULL_EFFORT check (e.g. quantifier reasoning 637 * outputing quantifier instantiations). In such a case, a lemma can 638 * be asserted that is simplified away (perhaps it's already true). 639 * However, we must maintain the invariant that, if a theory uses the 640 * OutputChannel, it implicitly requests that another check(FULL_EFFORT) 641 * be performed before exit, even if no new facts are on its fact queue, 642 * as it might decide to further instantiate some lemmas, precluding 643 * a SAT response. 644 */ needCheck()645 inline bool needCheck() const { 646 return d_outputChannelUsed || d_lemmasAdded; 647 } 648 649 /** 650 * This is called at shutdown time by the SmtEngine, just before 651 * destruction. It is important because there are destruction 652 * ordering issues between PropEngine and Theory. 653 */ 654 void shutdown(); 655 656 /** 657 * Solve the given literal with a theory that owns it. 658 */ 659 theory::Theory::PPAssertStatus solve(TNode literal, 660 theory::SubstitutionMap& substitutionOut); 661 662 /** 663 * Preregister a Theory atom with the responsible theory (or 664 * theories). 665 */ 666 void preRegister(TNode preprocessed); 667 668 /** 669 * Assert the formula to the appropriate theory. 670 * @param node the assertion 671 */ 672 void assertFact(TNode node); 673 674 /** 675 * Check all (currently-active) theories for conflicts. 676 * @param effort the effort level to use 677 */ 678 void check(theory::Theory::Effort effort); 679 680 /** 681 * Run the combination framework. 682 */ 683 void combineTheories(); 684 685 /** 686 * Calls ppStaticLearn() on all theories, accumulating their 687 * combined contributions in the "learned" builder. 688 */ 689 void ppStaticLearn(TNode in, NodeBuilder<>& learned); 690 691 /** 692 * Calls presolve() on all theories and returns true 693 * if one of the theories discovers a conflict. 694 */ 695 bool presolve(); 696 697 /** 698 * Calls postsolve() on all theories. 699 */ 700 void postsolve(); 701 702 /** 703 * Calls notifyRestart() on all active theories. 704 */ 705 void notifyRestart(); 706 getPropagatedLiterals(std::vector<TNode> & literals)707 void getPropagatedLiterals(std::vector<TNode>& literals) { 708 for (; d_propagatedLiteralsIndex < d_propagatedLiterals.size(); d_propagatedLiteralsIndex = d_propagatedLiteralsIndex + 1) { 709 Debug("getPropagatedLiterals") << "TheoryEngine::getPropagatedLiterals: propagating: " << d_propagatedLiterals[d_propagatedLiteralsIndex] << std::endl; 710 literals.push_back(d_propagatedLiterals[d_propagatedLiteralsIndex]); 711 } 712 } 713 714 /** 715 * Returns the next decision request, or null if none exist. The next 716 * decision request is a literal that this theory engine prefers the SAT 717 * solver to make as its next decision. Decision requests are managed by 718 * the decision manager d_decManager. 719 */ 720 Node getNextDecisionRequest(); 721 722 bool properConflict(TNode conflict) const; 723 bool properPropagation(TNode lit) const; 724 bool properExplanation(TNode node, TNode expl) const; 725 726 /** 727 * Returns an explanation of the node propagated to the SAT solver. 728 */ 729 Node getExplanation(TNode node); 730 731 /** 732 * Returns an explanation of the node propagated to the SAT solver and the theory 733 * that propagated it. 734 */ 735 Node getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe); 736 737 /** 738 * collect model info 739 */ 740 bool collectModelInfo(theory::TheoryModel* m); 741 /** post process model */ 742 void postProcessModel( theory::TheoryModel* m ); 743 744 /** 745 * Get the pointer to the model object used by this theory engine. 746 */ 747 theory::TheoryModel* getModel(); 748 /** 749 * Get the current model for the current set of assertions. This method 750 * should only be called immediately after a satisfiable or unknown 751 * response to a check-sat call, and only if produceModels is true. 752 * 753 * If the model is not already built, this will cause this theory engine 754 * to build to the model. 755 */ 756 theory::TheoryModel* getBuiltModel(); 757 /** set eager model building 758 * 759 * If this method is called, then this TheoryEngine will henceforth build 760 * its model immediately after every satisfiability check that results 761 * in a satisfiable or unknown result. The motivation for this mode is to 762 * accomodate API users that get the model object from the TheoryEngine, 763 * where we want to ensure that this model is always valid. 764 * TODO (#2648): revisit this. 765 */ setEagerModelBuilding()766 void setEagerModelBuilding() { d_eager_model_building = true; } 767 768 /** get synth solutions 769 * 770 * This function adds entries to sol_map that map functions-to-synthesize with 771 * their solutions, for all active conjectures. This should be called 772 * immediately after the solver answers unsat for sygus input. 773 * 774 * For details on what is added to sol_map, see 775 * CegConjecture::getSynthSolutions. 776 */ 777 void getSynthSolutions(std::map<Node, Node>& sol_map); 778 779 /** 780 * Get the model builder 781 */ getModelBuilder()782 theory::TheoryEngineModelBuilder* getModelBuilder() { return d_curr_model_builder; } 783 784 /** 785 * Get the theory associated to a given Node. 786 * 787 * @returns the theory, or NULL if the TNode is 788 * of built-in type. 789 */ theoryOf(TNode node)790 inline theory::Theory* theoryOf(TNode node) const { 791 return d_theoryTable[theory::Theory::theoryOf(node)]; 792 } 793 794 /** 795 * Get the theory associated to a the given theory id. 796 * 797 * @returns the theory 798 */ theoryOf(theory::TheoryId theoryId)799 inline theory::Theory* theoryOf(theory::TheoryId theoryId) const { 800 return d_theoryTable[theoryId]; 801 } 802 isTheoryEnabled(theory::TheoryId theoryId)803 inline bool isTheoryEnabled(theory::TheoryId theoryId) const { 804 return d_logicInfo.isTheoryEnabled(theoryId); 805 } 806 /** get the logic info used by this theory engine */ 807 const LogicInfo& getLogicInfo() const; 808 /** 809 * Returns the equality status of the two terms, from the theory 810 * that owns the domain type. The types of a and b must be the same. 811 */ 812 theory::EqualityStatus getEqualityStatus(TNode a, TNode b); 813 814 /** 815 * Returns the value that a theory that owns the type of var currently 816 * has (or null if none); 817 */ 818 Node getModelValue(TNode var); 819 820 /** 821 * Takes a literal and returns an equivalent literal that is guaranteed to be a SAT literal 822 */ 823 Node ensureLiteral(TNode n); 824 825 /** 826 * Print all instantiations made by the quantifiers module. 827 */ 828 void printInstantiations( std::ostream& out ); 829 830 /** 831 * Print solution for synthesis conjectures found by ce_guided_instantiation module 832 */ 833 void printSynthSolution( std::ostream& out ); 834 835 /** 836 * Get list of quantified formulas that were instantiated 837 */ 838 void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ); 839 840 /** 841 * Get instantiation methods 842 * first inputs forall x.q[x] and returns ( q[a], ..., q[z] ) 843 * second inputs forall x.q[x] and returns ( a, ..., z ) 844 * third and fourth return mappings e.g. forall x.q1[x] -> ( q1[a]...q1[z] ) , ... , forall x.qn[x] -> ( qn[a]...qn[z] ) 845 */ 846 void getInstantiations( Node q, std::vector< Node >& insts ); 847 void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ); 848 void getInstantiations( std::map< Node, std::vector< Node > >& insts ); 849 void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ); 850 851 /** 852 * Get instantiated conjunction, returns q[t1] ^ ... ^ q[tn] where t1...tn are current set of instantiations for q. 853 * Can be used for quantifier elimination when satisfiable and q[t1] ^ ... ^ q[tn] |= q 854 */ 855 Node getInstantiatedConjunction( Node q ); 856 857 /** 858 * Forwards an entailment check according to the given theoryOfMode. 859 * See theory.h for documentation on entailmentCheck(). 860 */ 861 std::pair<bool, Node> entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params = NULL, theory::EntailmentCheckSideEffects* out = NULL); 862 863 private: 864 865 /** Default visitor for pre-registration */ 866 PreRegisterVisitor d_preRegistrationVisitor; 867 868 /** Visitor for collecting shared terms */ 869 SharedTermsVisitor d_sharedTermsVisitor; 870 871 /** Dump the assertions to the dump */ 872 void dumpAssertions(const char* tag); 873 874 /** For preprocessing pass lifting bit-vectors of size 1 to booleans */ 875 public: 876 void staticInitializeBVOptions(const std::vector<Node>& assertions); 877 878 Node ppSimpITE(TNode assertion); 879 /** Returns false if an assertion simplified to false. */ 880 bool donePPSimpITE(std::vector<Node>& assertions); 881 getSharedTermsDatabase()882 SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; } 883 getMasterEqualityEngine()884 theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } 885 getTermFormulaRemover()886 RemoveTermFormulas* getTermFormulaRemover() { return &d_tform_remover; } 887 getSortInference()888 SortInference* getSortInference() { return &d_sortInfer; } 889 890 /** Prints the assertions to the debug stream */ 891 void printAssertions(const char* tag); 892 893 /** Theory alternative is in use. */ 894 bool useTheoryAlternative(const std::string& name); 895 896 /** Enables using a theory alternative by name. */ 897 void enableTheoryAlternative(const std::string& name); 898 899 private: 900 std::set< std::string > d_theoryAlternatives; 901 902 std::map< std::string, std::vector< theory::Theory* > > d_attr_handle; 903 904 public: 905 /** Set user attribute. 906 * 907 * This function is called when an attribute is set by a user. In SMT-LIBv2 908 * this is done via the syntax (! n :attr) 909 */ 910 void setUserAttribute(const std::string& attr, 911 Node n, 912 const std::vector<Node>& node_values, 913 const std::string& str_value); 914 915 /** Handle user attribute. 916 * 917 * Associates theory t with the attribute attr. Theory t will be 918 * notified whenever an attribute of name attr is set. 919 */ 920 void handleUserAttribute(const char* attr, theory::Theory* t); 921 922 /** 923 * Check that the theory assertions are satisfied in the model. 924 * This function is called from the smt engine's checkModel routine. 925 */ 926 void checkTheoryAssertionsWithModel(bool hardFailure); 927 928 private: 929 IntStat d_arithSubstitutionsAdded; 930 931 };/* class TheoryEngine */ 932 933 }/* CVC4 namespace */ 934 935 #endif /* __CVC4__THEORY_ENGINE_H */ 936