src/theory/theory.h

   1 /*********************                                                        */
   2 /*! \file theory.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Dejan Jovanovic, Tim King
   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 Base of the theory interface.
  13  **
  14  ** Base of the theory interface.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__THEORY__THEORY_H
  20 #define CVC4__THEORY__THEORY_H
  21
  22 #include <iosfwd>
  23 #include <map>
  24 #include <set>
  25 #include <string>
  26 #include <unordered_set>
  27
  28 #include "context/cdhashset.h"
  29 #include "context/cdlist.h"
  30 #include "context/cdo.h"
  31 #include "context/context.h"
  32 #include "expr/node.h"
  33 #include "lib/ffs.h"
  34 #include "options/options.h"
  35 #include "options/theory_options.h"
  36 #include "options/theoryof_mode.h"
  37 #include "smt/command.h"
  38 #include "smt/dump.h"
  39 #include "smt/logic_request.h"
  40 #include "theory/assertion.h"
  41 #include "theory/care_graph.h"
  42 #include "theory/decision_manager.h"
  43 #include "theory/logic_info.h"
  44 #include "theory/output_channel.h"
  45 #include "theory/valuation.h"
  46 #include "util/statistics_registry.h"
  47
  48 namespace CVC4 {
  49
  50 class TheoryEngine;
  51
  52 namespace theory {
  53
  54 class QuantifiersEngine;
  55 class TheoryModel;
  56 class SubstitutionMap;
  57 class ExtTheory;
  58
  59 class EntailmentCheckParameters;
  60 class EntailmentCheckSideEffects;
  61
  62 namespace rrinst {
  63   class CandidateGenerator;
  64 }/* CVC4::theory::rrinst namespace */
  65
  66 namespace eq {
  67   class EqualityEngine;
  68 }/* CVC4::theory::eq namespace */
  69
  70 /**
  71  * Base class for T-solvers.  Abstract DPLL(T).
  72  *
  73  * This is essentially an interface class.  The TheoryEngine has
  74  * pointers to Theory.  Note that only one specific Theory type (e.g.,
  75  * TheoryUF) can exist per NodeManager, because of how the
  76  * RegisteredAttr works.  (If you need multiple instances of the same
  77  * theory, you'll have to write a multiplexed theory that dispatches
  78  * all calls to them.)
  79  */
  80 class Theory {
  81
  82 private:
  83
  84   friend class ::CVC4::TheoryEngine;
  85
  86   // Disallow default construction, copy, assignment.
  87   Theory() = delete;
  88   Theory(const Theory&) = delete;
  89   Theory& operator=(const Theory&) = delete;
  90
  91   /** An integer identifying the type of the theory. */
  92   TheoryId d_id;
  93
  94   /** Name of this theory instance. Along with the TheoryId this should provide
  95    * an unique string identifier for each instance of a Theory class. We need
  96    * this to ensure unique statistics names over multiple theory instances. */
  97   std::string d_instanceName;
  98
  99   /** The SAT search context for the Theory. */
 100   context::Context* d_satContext;
 101
 102   /** The user level assertion context for the Theory. */
 103   context::UserContext* d_userContext;
 104
 105   /** Information about the logic we're operating within. */
 106   const LogicInfo& d_logicInfo;
 107
 108   /**
 109    * The assertFact() queue.
 110    *
 111    * These can not be TNodes as some atoms (such as equalities) are sent
 112    * across theories without being stored in a global map.
 113    */
 114   context::CDList<Assertion> d_facts;
 115
 116   /** Index into the head of the facts list */
 117   context::CDO<unsigned> d_factsHead;
 118
 119   /** Add shared term to the theory. */
 120   void addSharedTermInternal(TNode node);
 121
 122   /** Indices for splitting on the shared terms. */
 123   context::CDO<unsigned> d_sharedTermsIndex;
 124
 125   /** The care graph the theory will use during combination. */
 126   CareGraph* d_careGraph;
 127
 128   /**
 129    * Pointer to the quantifiers engine (or NULL, if quantifiers are not
 130    * supported or not enabled). Not owned by the theory.
 131    */
 132   QuantifiersEngine* d_quantEngine;
 133
 134   /** Pointer to the decision manager. */
 135   DecisionManager* d_decManager;
 136
 137   /** Extended theory module or NULL. Owned by the theory. */
 138   ExtTheory* d_extTheory;
 139
 140  protected:
 141
 142
 143   // === STATISTICS ===
 144   /** time spent in check calls */
 145   TimerStat d_checkTime;
 146   /** time spent in theory combination */
 147   TimerStat d_computeCareGraphTime;
 148
 149   /**
 150    * The only method to add suff to the care graph.
 151    */
 152   void addCarePair(TNode t1, TNode t2);
 153
 154   /**
 155    * The function should compute the care graph over the shared terms.
 156    * The default function returns all the pairs among the shared variables.
 157    */
 158   virtual void computeCareGraph();
 159
 160   /**
 161    * A list of shared terms that the theory has.
 162    */
 163   context::CDList<TNode> d_sharedTerms;
 164
 165   /**
 166    * Helper function for computeRelevantTerms
 167    */
 168   void collectTerms(TNode n,
 169                     std::set<Kind>& irrKinds,
 170                     std::set<Node>& termSet) const;
 171
 172   /**
 173    * Scans the current set of assertions and shared terms top-down
 174    * until a theory-leaf is reached, and adds all terms found to
 175    * termSet.  This is used by collectModelInfo to delimit the set of
 176    * terms that should be used when constructing a model.
 177    *
 178    * irrKinds: The kinds of terms that appear in assertions that should *not*
 179    * be included in termSet. Note that the kinds EQUAL and NOT are always
 180    * treated as irrelevant kinds.
 181    *
 182    * includeShared: Whether to include shared terms in termSet. Notice that
 183    * shared terms are not influenced by irrKinds.
 184    */
 185   void computeRelevantTerms(std::set<Node>& termSet,
 186                             std::set<Kind>& irrKinds,
 187                             bool includeShared = true) const;
 188   /** same as above, but with empty irrKinds */
 189   void computeRelevantTerms(std::set<Node>& termSet, bool includeShared = true) const;
 190
 191   /**
 192    * Construct a Theory.
 193    *
 194    * The pair <id, instance> is assumed to uniquely identify this Theory
 195    * w.r.t. the SmtEngine.
 196    */
 197   Theory(TheoryId id,
 198          context::Context* satContext,
 199          context::UserContext* userContext,
 200          OutputChannel& out,
 201          Valuation valuation,
 202          const LogicInfo& logicInfo,
 203          std::string instance = "");  // taking : No default.
 204
 205   /**
 206    * This is called at shutdown time by the TheoryEngine, just before
 207    * destruction.  It is important because there are destruction
 208    * ordering issues between PropEngine and Theory (based on what
 209    * hard-links to Nodes are outstanding).  As the fact queue might be
 210    * nonempty, we ensure here that it's clear.  If you overload this,
 211    * you must make an explicit call here to this->Theory::shutdown()
 212    * too.
 213    */
 214   virtual void shutdown() { }
 215
 216   /**
 217    * The output channel for the Theory.
 218    */
 219   OutputChannel* d_out;
 220
 221   /**
 222    * The valuation proxy for the Theory to communicate back with the
 223    * theory engine (and other theories).
 224    */
 225   Valuation d_valuation;
 226
 227   /**
 228    * Whether proofs are enabled
 229    *
 230    */
 231   bool d_proofsEnabled;
 232
 233   /**
 234    * Returns the next assertion in the assertFact() queue.
 235    *
 236    * @return the next assertion in the assertFact() queue
 237    */
 238   inline Assertion get();
 239
 240   const LogicInfo& getLogicInfo() const {
 241     return d_logicInfo;
 242   }
 243
 244   /**
 245    * The theory that owns the uninterpreted sort.
 246    */
 247   static TheoryId s_uninterpretedSortOwner;
 248
 249   void printFacts(std::ostream& os) const;
 250   void debugPrintFacts() const;
 251
 252 public:
 253
 254   /**
 255    * Return the ID of the theory responsible for the given type.
 256    */
 257   static inline TheoryId theoryOf(TypeNode typeNode) {
 258     Trace("theory::internal") << "theoryOf(" << typeNode << ")" << std::endl;
 259     TheoryId id;
 260     if (typeNode.getKind() == kind::TYPE_CONSTANT) {
 261       id = typeConstantToTheoryId(typeNode.getConst<TypeConstant>());
 262     } else {
 263       id = kindToTheoryId(typeNode.getKind());
 264     }
 265     if (id == THEORY_BUILTIN) {
 266       Trace("theory::internal") << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner << std::endl;
 267       return s_uninterpretedSortOwner;
 268     }
 269     return id;
 270   }
 271
 272   /**
 273    * Returns the ID of the theory responsible for the given node.
 274    */
 275   static TheoryId theoryOf(TheoryOfMode mode, TNode node);
 276
 277   /**
 278    * Returns the ID of the theory responsible for the given node.
 279    */
 280   static inline TheoryId theoryOf(TNode node) {
 281     return theoryOf(options::theoryOfMode(), node);
 282   }
 283
 284   /**
 285    * Set the owner of the uninterpreted sort.
 286    */
 287   static void setUninterpretedSortOwner(TheoryId theory) {
 288     s_uninterpretedSortOwner = theory;
 289   }
 290
 291   /**
 292    * Get the owner of the uninterpreted sort.
 293    */
 294   static TheoryId getUninterpretedSortOwner() {
 295     return s_uninterpretedSortOwner;
 296   }
 297
 298   /**
 299    * Checks if the node is a leaf node of this theory
 300    */
 301   inline bool isLeaf(TNode node) const {
 302     return node.getNumChildren() == 0 || theoryOf(node) != d_id;
 303   }
 304
 305   /**
 306    * Checks if the node is a leaf node of a theory.
 307    */
 308   inline static bool isLeafOf(TNode node, TheoryId theoryId) {
 309     return node.getNumChildren() == 0 || theoryOf(node) != theoryId;
 310   }
 311
 312   /** Returns true if the assertFact queue is empty*/
 313   bool done() const { return d_factsHead == d_facts.size(); }
 314   /**
 315    * Destructs a Theory.
 316    */
 317   virtual ~Theory();
 318
 319   /**
 320    * Subclasses of Theory may add additional efforts.  DO NOT CHECK
 321    * equality with one of these values (e.g. if STANDARD xxx) but
 322    * rather use range checks (or use the helper functions below).
 323    * Normally we call QUICK_CHECK or STANDARD; at the leaves we call
 324    * with FULL_EFFORT.
 325    */
 326   enum Effort {
 327     /**
 328      * Standard effort where theory need not do anything
 329      */
 330     EFFORT_STANDARD = 50,
 331     /**
 332      * Full effort requires the theory make sure its assertions are satisfiable or not
 333      */
 334     EFFORT_FULL = 100,
 335     /**
 336      * Combination effort means that the individual theories are already satisfied, and
 337      * it is time to put some effort into propagation of shared term equalities
 338      */
 339     EFFORT_COMBINATION = 150,
 340     /**
 341      * Last call effort, reserved for quantifiers.
 342      */
 343     EFFORT_LAST_CALL = 200
 344   };/* enum Effort */
 345
 346   static inline bool standardEffortOrMore(Effort e) CVC4_CONST_FUNCTION
 347     { return e >= EFFORT_STANDARD; }
 348   static inline bool standardEffortOnly(Effort e) CVC4_CONST_FUNCTION
 349     { return e >= EFFORT_STANDARD && e <  EFFORT_FULL; }
 350   static inline bool fullEffort(Effort e) CVC4_CONST_FUNCTION
 351     { return e == EFFORT_FULL; }
 352   static inline bool combination(Effort e) CVC4_CONST_FUNCTION
 353     { return e == EFFORT_COMBINATION; }
 354
 355   /**
 356    * Get the id for this Theory.
 357    */
 358   TheoryId getId() const {
 359     return d_id;
 360   }
 361
 362   /**
 363    * Get the SAT context associated to this Theory.
 364    */
 365   context::Context* getSatContext() const {
 366     return d_satContext;
 367   }
 368
 369   /**
 370    * Get the context associated to this Theory.
 371    */
 372   context::UserContext* getUserContext() const {
 373     return d_userContext;
 374   }
 375
 376   /**
 377    * Set the output channel associated to this theory.
 378    */
 379   void setOutputChannel(OutputChannel& out) {
 380     d_out = &out;
 381   }
 382
 383   /**
 384    * Get the output channel associated to this theory.
 385    */
 386   OutputChannel& getOutputChannel() {
 387     return *d_out;
 388   }
 389
 390   /**
 391    * Get the valuation associated to this theory.
 392    */
 393   Valuation& getValuation() {
 394     return d_valuation;
 395   }
 396
 397   /**
 398    * Get the quantifiers engine associated to this theory.
 399    */
 400   QuantifiersEngine* getQuantifiersEngine() {
 401     return d_quantEngine;
 402   }
 403
 404   /**
 405    * Get the quantifiers engine associated to this theory (const version).
 406    */
 407   const QuantifiersEngine* getQuantifiersEngine() const {
 408     return d_quantEngine;
 409   }
 410
 411   /** Get the decision manager associated to this theory. */
 412   DecisionManager* getDecisionManager() { return d_decManager; }
 413
 414   /**
 415    * Finish theory initialization.  At this point, options and the logic
 416    * setting are final, and the master equality engine and quantifiers
 417    * engine (if any) are initialized.  This base class implementation
 418    * does nothing.
 419    */
 420   virtual void finishInit() { }
 421
 422   /**
 423    * Some theories have kinds that are effectively definitions and
 424    * should be expanded before they are handled.  Definitions allow
 425    * a much wider range of actions than the normal forms given by the
 426    * rewriter; they can enable other theories and create new terms.
 427    * However no assumptions can be made about subterms having been
 428    * expanded or rewritten.  Where possible rewrite rules should be
 429    * used, definitions should only be used when rewrites are not
 430    * possible, for example in handling under-specified operations
 431    * using partially defined functions.
 432    *
 433    * Some theories like sets use expandDefinition as a "context
 434    * independent preRegisterTerm".  This is required for cases where
 435    * a theory wants to be notified about a term before preprocessing
 436    * and simplification but doesn't necessarily want to rewrite it.
 437    */
 438   virtual Node expandDefinition(LogicRequest &logicRequest, Node node) {
 439     // by default, do nothing
 440     return node;
 441   }
 442
 443   /**
 444    * Pre-register a term.  Done one time for a Node per SAT context level.
 445    */
 446   virtual void preRegisterTerm(TNode) { }
 447
 448   /**
 449    * Assert a fact in the current context.
 450    */
 451   void assertFact(TNode assertion, bool isPreregistered) {
 452     Trace("theory") << "Theory<" << getId() << ">::assertFact["
 453                     << d_satContext->getLevel() << "](" << assertion << ", "
 454                     << (isPreregistered ? "true" : "false") << ")" << std::endl;
 455     d_facts.push_back(Assertion(assertion, isPreregistered));
 456   }
 457
 458   /**
 459    * This method is called to notify a theory that the node n should
 460    * be considered a "shared term" by this theory
 461    */
 462   virtual void addSharedTerm(TNode n) { }
 463
 464   /**
 465    * Called to set the master equality engine.
 466    */
 467   virtual void setMasterEqualityEngine(eq::EqualityEngine* eq) { }
 468
 469   /** Called to set the quantifiers engine. */
 470   void setQuantifiersEngine(QuantifiersEngine* qe);
 471   /** Called to set the decision manager. */
 472   void setDecisionManager(DecisionManager* dm);
 473
 474   /** Setup an ExtTheory module for this Theory. Can only be called once. */
 475   void setupExtTheory();
 476
 477   /**
 478    * Return the current theory care graph. Theories should overload
 479    * computeCareGraph to do the actual computation, and use addCarePair to add
 480    * pairs to the care graph.
 481    */
 482   void getCareGraph(CareGraph* careGraph);
 483
 484   /**
 485    * Return the status of two terms in the current context. Should be
 486    * implemented in sub-theories to enable more efficient theory-combination.
 487    */
 488   virtual EqualityStatus getEqualityStatus(TNode a, TNode b) {
 489     return EQUALITY_UNKNOWN;
 490   }
 491
 492   /**
 493    * Return the model value of the give shared term (or null if not available).
 494    */
 495   virtual Node getModelValue(TNode var) { return Node::null(); }
 496
 497   /**
 498    * Check the current assignment's consistency.
 499    *
 500    * An implementation of check() is required to either:
 501    * - return a conflict on the output channel,
 502    * - be interrupted,
 503    * - throw an exception
 504    * - or call get() until done() is true.
 505    */
 506   virtual void check(Effort level = EFFORT_FULL) { }
 507
 508   /** Needs last effort check? */
 509   virtual bool needsCheckLastEffort() { return false; }
 510
 511   /** T-propagate new literal assignments in the current context. */
 512   virtual void propagate(Effort level = EFFORT_FULL) { }
 513
 514   /**
 515    * Return an explanation for the literal represented by parameter n
 516    * (which was previously propagated by this theory).
 517    */
 518   virtual Node explain(TNode n) {
 519     Unimplemented("Theory %s propagated a node but doesn't implement the "
 520                   "Theory::explain() interface!", identify().c_str());
 521   }
 522
 523   /**
 524    * Get all relevant information in this theory regarding the current
 525    * model.  This should be called after a call to check( FULL_EFFORT )
 526    * for all theories with no conflicts and no lemmas added.
 527    *
 528    * This method returns true if and only if the equality engine of m is
 529    * consistent as a result of this call.
 530    */
 531   virtual bool collectModelInfo(TheoryModel* m) { return true; }
 532   /** if theories want to do something with model after building, do it here */
 533   virtual void postProcessModel( TheoryModel* m ){ }
 534   /**
 535    * Statically learn from assertion "in," which has been asserted
 536    * true at the top level.  The theory should only add (via
 537    * ::operator<< or ::append()) to the "learned" builder---it should
 538    * *never* clear it.  It is a conjunction to add to the formula at
 539    * the top-level and may contain other theories' contributions.
 540    */
 541   virtual void ppStaticLearn(TNode in, NodeBuilder<>& learned) { }
 542
 543   enum PPAssertStatus {
 544     /** Atom has been solved  */
 545     PP_ASSERT_STATUS_SOLVED,
 546     /** Atom has not been solved */
 547     PP_ASSERT_STATUS_UNSOLVED,
 548     /** Atom is inconsistent */
 549     PP_ASSERT_STATUS_CONFLICT
 550   };
 551
 552   /**
 553    * Given a literal, add the solved substitutions to the map, if any.
 554    * The method should return true if the literal can be safely removed.
 555    */
 556   virtual PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
 557
 558   /**
 559    * Given an atom of the theory coming from the input formula, this
 560    * method can be overridden in a theory implementation to rewrite
 561    * the atom into an equivalent form.  This is only called just
 562    * before an input atom to the engine.
 563    */
 564   virtual Node ppRewrite(TNode atom) { return atom; }
 565
 566   /**
 567    * Notify preprocessed assertions. Called on new assertions after
 568    * preprocessing before they are asserted to theory engine.
 569    */
 570   virtual void ppNotifyAssertions(const std::vector<Node>& assertions) {}
 571
 572   /**
 573    * A Theory is called with presolve exactly one time per user
 574    * check-sat.  presolve() is called after preregistration,
 575    * rewriting, and Boolean propagation, (other theories'
 576    * propagation?), but the notified Theory has not yet had its
 577    * check() or propagate() method called.  A Theory may empty its
 578    * assertFact() queue using get().  A Theory can raise conflicts,
 579    * add lemmas, and propagate literals during presolve().
 580    *
 581    * NOTE: The presolve property must be added to the kinds file for
 582    * the theory.
 583    */
 584   virtual void presolve() { }
 585
 586   /**
 587    * A Theory is called with postsolve exactly one time per user
 588    * check-sat.  postsolve() is called after the query has completed
 589    * (regardless of whether sat, unsat, or unknown), and after any
 590    * model-querying related to the query has been performed.
 591    * After this call, the theory will not get another check() or
 592    * propagate() call until presolve() is called again.  A Theory
 593    * cannot raise conflicts, add lemmas, or propagate literals during
 594    * postsolve().
 595    */
 596   virtual void postsolve() { }
 597
 598   /**
 599    * Notification sent to the theory wheneven the search restarts.
 600    * Serves as a good time to do some clean-up work, and you can
 601    * assume you're at DL 0 for the purposes of Contexts.  This function
 602    * should not use the output channel.
 603    */
 604   virtual void notifyRestart() { }
 605
 606   /**
 607    * Identify this theory (for debugging, dynamic configuration,
 608    * etc..)
 609    */
 610   virtual std::string identify() const = 0;
 611
 612   /** Set user attribute
 613     * This function is called when an attribute is set by a user.  In SMT-LIBv2 this is done
 614     *  via the syntax (! n :attr)
 615     */
 616   virtual void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value) {
 617     Unimplemented("Theory %s doesn't support Theory::setUserAttribute interface",
 618                   identify().c_str());
 619   }
 620
 621   /** A set of theories */
 622   typedef uint32_t Set;
 623
 624   /** A set of all theories */
 625   static const Set AllTheories = (1 << theory::THEORY_LAST) - 1;
 626
 627   /** Pops a first theory off the set */
 628   static inline TheoryId setPop(Set& set) {
 629     uint32_t i = ffs(set); // Find First Set (bit)
 630     if (i == 0) { return THEORY_LAST; }
 631     TheoryId id = (TheoryId)(i-1);
 632     set = setRemove(id, set);
 633     return id;
 634   }
 635
 636   /** Returns the size of a set of theories */
 637   static inline size_t setSize(Set set) {
 638     size_t count = 0;
 639     while (setPop(set) != THEORY_LAST) {
 640       ++ count;
 641     }
 642     return count;
 643   }
 644
 645   /** Returns the index size of a set of theories */
 646   static inline size_t setIndex(TheoryId id, Set set) {
 647     Assert (setContains(id, set));
 648     size_t count = 0;
 649     while (setPop(set) != id) {
 650       ++ count;
 651     }
 652     return count;
 653   }
 654
 655   /** Add the theory to the set. If no set specified, just returns a singleton set */
 656   static inline Set setInsert(TheoryId theory, Set set = 0) {
 657     return set | (1 << theory);
 658   }
 659
 660   /** Add the theory to the set. If no set specified, just returns a singleton set */
 661   static inline Set setRemove(TheoryId theory, Set set = 0) {
 662     return setDifference(set, setInsert(theory));
 663   }
 664
 665   /** Check if the set contains the theory */
 666   static inline bool setContains(TheoryId theory, Set set) {
 667     return set & (1 << theory);
 668   }
 669
 670   static inline Set setComplement(Set a) {
 671     return (~a) & AllTheories;
 672   }
 673
 674   static inline Set setIntersection(Set a, Set b) {
 675     return a & b;
 676   }
 677
 678   static inline Set setUnion(Set a, Set b) {
 679     return a | b;
 680   }
 681
 682   /** a - b  */
 683   static inline Set setDifference(Set a, Set b) {
 684     return (~b) & a;
 685   }
 686
 687   static inline std::string setToString(theory::Theory::Set theorySet) {
 688     std::stringstream ss;
 689     ss << "[";
 690     for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
 691       if (theory::Theory::setContains((theory::TheoryId)theoryId, theorySet)) {
 692         ss << (theory::TheoryId) theoryId << " ";
 693       }
 694     }
 695     ss << "]";
 696     return ss.str();
 697   }
 698
 699   typedef context::CDList<Assertion>::const_iterator assertions_iterator;
 700
 701   /**
 702    * Provides access to the facts queue, primarily intended for theory
 703    * debugging purposes.
 704    *
 705    * @return the iterator to the beginning of the fact queue
 706    */
 707   assertions_iterator facts_begin() const {
 708     return d_facts.begin();
 709   }
 710
 711   /**
 712    * Provides access to the facts queue, primarily intended for theory
 713    * debugging purposes.
 714    *
 715    * @return the iterator to the end of the fact queue
 716    */
 717   assertions_iterator facts_end() const {
 718     return d_facts.end();
 719   }
 720   /**
 721    * Whether facts have been asserted to this theory.
 722    *
 723    * @return true iff facts have been asserted to this theory.
 724    */
 725   bool hasFacts() {
 726     return !d_facts.empty();
 727   }
 728
 729   /** Return total number of facts asserted to this theory */
 730   size_t numAssertions() {
 731     return d_facts.size();
 732   }
 733
 734   typedef context::CDList<TNode>::const_iterator shared_terms_iterator;
 735
 736   /**
 737    * Provides access to the shared terms, primarily intended for theory
 738    * debugging purposes.
 739    *
 740    * @return the iterator to the beginning of the shared terms list
 741    */
 742   shared_terms_iterator shared_terms_begin() const {
 743     return d_sharedTerms.begin();
 744   }
 745
 746   /**
 747    * Provides access to the facts queue, primarily intended for theory
 748    * debugging purposes.
 749    *
 750    * @return the iterator to the end of the shared terms list
 751    */
 752   shared_terms_iterator shared_terms_end() const {
 753     return d_sharedTerms.end();
 754   }
 755
 756
 757   /**
 758    * This is a utility function for constructing a copy of the currently shared terms
 759    * in a queriable form.  As this is
 760    */
 761   std::unordered_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
 762
 763   /**
 764    * This allows the theory to be queried for whether a literal, lit, is
 765    * entailed by the theory.  This returns a pair of a Boolean and a node E.
 766    *
 767    * If the Boolean is true, then E is a formula that entails lit and E is propositionally
 768    * entailed by the assertions to the theory.
 769    *
 770    * If the Boolean is false, it is "unknown" if lit is entailed and E may be
 771    * any node.
 772    *
 773    * The literal lit is either an atom a or (not a), which must belong to the theory:
 774    *   There is some TheoryOfMode m s.t. Theory::theoryOf(m, a) == this->getId().
 775    *
 776    * There are NO assumptions that a or the subterms of a have been
 777    * preprocessed in any form.  This includes ppRewrite, rewriting,
 778    * preregistering, registering, definition expansion or ITE removal!
 779    *
 780    * Theories are free to limit the amount of effort they use and so may
 781    * always opt to return "unknown".  Both "unknown" and "not entailed",
 782    * may return for E a non-boolean Node (e.g. Node::null()).  (There is no explicit output
 783    * for the negation of lit is entailed.)
 784    *
 785    * If lit is theory valid, the return result may be the Boolean constant
 786    * true for E.
 787    *
 788    * If lit is entailed by multiple assertions on the theory's getFact()
 789    * queue, a_1, a_2, ... and a_k, this may return E=(and a_1 a_2 ... a_k) or
 790    * another theory entailed explanation E=(and (and a_1 a_2) (and a3 a_4) ... a_k)
 791    *
 792    * If lit is entailed by a single assertion on the theory's getFact()
 793    * queue, say a, this may return E=a.
 794    *
 795    * The theory may always return false!
 796    *
 797    * The search is controlled by the parameter params.  For default behavior,
 798    * this may be left NULL.
 799    *
 800    * Theories that want parameters extend the virtual EntailmentCheckParameters
 801    * class.  Users ask the theory for an appropriate subclass from the theory
 802    * and configure that.  How this is implemented is on a per theory basis.
 803    *
 804    * The search may provide additional output to guide the user of
 805    * this function.  This output is stored in a EntailmentCheckSideEffects*
 806    * output parameter.  The implementation of this is theory specific.  For
 807    * no output, this is NULL.
 808    *
 809    * Theories may not touch their output stream during an entailment check.
 810    *
 811    * @param  lit     a literal belonging to the theory.
 812    * @param  params  the control parameters for the entailment check.
 813    * @param  out     a theory specific output object of the entailment search.
 814    * @return         a pair <b,E> s.t. if b is true, then a formula E such that
 815    * E |= lit in the theory.
 816    */
 817   virtual std::pair<bool, Node> entailmentCheck(
 818       TNode lit, const EntailmentCheckParameters* params = NULL,
 819       EntailmentCheckSideEffects* out = NULL);
 820
 821   /* equality engine TODO: use? */
 822   virtual eq::EqualityEngine* getEqualityEngine() { return NULL; }
 823
 824   /* Get extended theory if one has been installed. */
 825   ExtTheory* getExtTheory();
 826
 827   /* get current substitution at an effort
 828    *   input : vars
 829    *   output : subs, exp
 830    *   where ( exp[vars[i]] => vars[i] = subs[i] ) holds for all i
 831    */
 832   virtual bool getCurrentSubstitution(int effort, std::vector<Node>& vars,
 833                                       std::vector<Node>& subs,
 834                                       std::map<Node, std::vector<Node> >& exp) {
 835     return false;
 836   }
 837
 838   /* is extended function reduced */
 839   virtual bool isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp ) { return n.isConst(); }
 840
 841   /**
 842    * Get reduction for node
 843    * If return value is not 0, then n is reduced.
 844    * If return value <0 then n is reduced SAT-context-independently (e.g. by a
 845    *  lemma that persists at this user-context level).
 846    * If nr is non-null, then ( n = nr ) should be added as a lemma by caller,
 847    *  and return value should be <0.
 848    */
 849   virtual int getReduction( int effort, Node n, Node& nr ) { return 0; }
 850
 851   /** Turn on proof-production mode. */
 852   void produceProofs() { d_proofsEnabled = true; }
 853
 854 };/* class Theory */
 855
 856 std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
 857
 858
 859 inline theory::Assertion Theory::get() {
 860   Assert( !done(), "Theory::get() called with assertion queue empty!" );
 861
 862   // Get the assertion
 863   Assertion fact = d_facts[d_factsHead];
 864   d_factsHead = d_factsHead + 1;
 865
 866   Trace("theory") << "Theory::get() => " << fact << " (" << d_facts.size() - d_factsHead << " left)" << std::endl;
 867
 868   if(Dump.isOn("state")) {
 869     Dump("state") << AssertCommand(fact.assertion.toExpr());
 870   }
 871
 872   return fact;
 873 }
 874
 875 inline std::ostream& operator<<(std::ostream& out,
 876                                 const CVC4::theory::Theory& theory) {
 877   return out << theory.identify();
 878 }
 879
 880 inline std::ostream& operator << (std::ostream& out, theory::Theory::PPAssertStatus status) {
 881   switch (status) {
 882   case theory::Theory::PP_ASSERT_STATUS_SOLVED:
 883     out << "SOLVE_STATUS_SOLVED"; break;
 884   case theory::Theory::PP_ASSERT_STATUS_UNSOLVED:
 885     out << "SOLVE_STATUS_UNSOLVED"; break;
 886   case theory::Theory::PP_ASSERT_STATUS_CONFLICT:
 887     out << "SOLVE_STATUS_CONFLICT"; break;
 888   default:
 889     Unhandled();
 890   }
 891   return out;
 892 }
 893
 894 class EntailmentCheckParameters {
 895 private:
 896   TheoryId d_tid;
 897 protected:
 898   EntailmentCheckParameters(TheoryId tid);
 899 public:
 900   TheoryId getTheoryId() const;
 901   virtual ~EntailmentCheckParameters();
 902 };/* class EntailmentCheckParameters */
 903
 904 class EntailmentCheckSideEffects {
 905 private:
 906   TheoryId d_tid;
 907 protected:
 908   EntailmentCheckSideEffects(TheoryId tid);
 909 public:
 910   TheoryId getTheoryId() const;
 911   virtual ~EntailmentCheckSideEffects();
 912 };/* class EntailmentCheckSideEffects */
 913
 914 }/* CVC4::theory namespace */
 915 }/* CVC4 namespace */
 916
 917 #endif /* CVC4__THEORY__THEORY_H */