src/theory/theory.h

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