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