src/theory/theory.h

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