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