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