src/theory/theory.h

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