src/theory/theory.h

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