src/theory/theory.h

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