src/theory/theory_engine.h

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