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