src/theory/theory.h

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