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