src/theory/output_channel.h

   1 /*********************                                                        */
   2 /*! \file output_channel.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Tim King, Liana Hadarean
   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 The theory output channel interface
  13  **
  14  ** The theory output channel interface.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__THEORY__OUTPUT_CHANNEL_H
  20 #define CVC4__THEORY__OUTPUT_CHANNEL_H
  21
  22 #include <memory>
  23
  24 #include "expr/proof_node.h"
  25 #include "proof/proof_manager.h"
  26 #include "smt/logic_exception.h"
  27 #include "theory/interrupted.h"
  28 #include "theory/trust_node.h"
  29 #include "util/proof.h"
  30 #include "util/resource_manager.h"
  31
  32 namespace CVC4 {
  33 namespace theory {
  34
  35 class Theory;
  36
  37 /**
  38  * A LemmaStatus, returned from OutputChannel::lemma(), provides information
  39  * about the lemma added.  In particular, it contains the T-rewritten lemma
  40  * for inspection and the user-level at which the lemma will reside.
  41  */
  42 class LemmaStatus {
  43  public:
  44   LemmaStatus(TNode rewrittenLemma, unsigned level)
  45       : d_rewrittenLemma(rewrittenLemma), d_level(level) {}
  46
  47   /** Get the T-rewritten form of the lemma. */
  48   TNode getRewrittenLemma() const { return d_rewrittenLemma; }
  49   /**
  50    * Get the user-level at which the lemma resides.  After this user level
  51    * is popped, the lemma is un-asserted from the SAT layer.  This level
  52    * will be 0 if the lemma didn't reach the SAT layer at all.
  53    */
  54   unsigned getLevel() const { return d_level; }
  55  private:
  56   Node d_rewrittenLemma;
  57   unsigned d_level;
  58 }; /* class LemmaStatus */
  59
  60 /**
  61  * Generic "theory output channel" interface.
  62  *
  63  * All methods can throw unrecoverable CVC4::Exception's unless otherwise
  64  * documented.
  65  */
  66 class OutputChannel {
  67  public:
  68   /** Construct an OutputChannel. */
  69   OutputChannel() {}
  70
  71   /**
  72    * Destructs an OutputChannel.  This implementation does nothing,
  73    * but we need a virtual destructor for safety in case subclasses
  74    * have a destructor.
  75    */
  76   virtual ~OutputChannel() {}
  77
  78   OutputChannel(const OutputChannel&) = delete;
  79   OutputChannel& operator=(const OutputChannel&) = delete;
  80
  81   /**
  82    * With safePoint(), the theory signals that it is at a safe point
  83    * and can be interrupted.
  84    *
  85    * @throws Interrupted if the theory can be safely interrupted.
  86    */
  87   virtual void safePoint(ResourceManager::Resource r) {}
  88
  89   /**
  90    * Indicate a theory conflict has arisen.
  91    *
  92    * @param n - a conflict at the current decision level.  This should
  93    * be an AND-kinded node of literals that are TRUE in the current
  94    * assignment and are in conflict (i.e., at least one must be
  95    * assigned false), or else a literal by itself (in the case of a
  96    * unit conflict) which is assigned TRUE (and T-conflicting) in the
  97    * current assignment.
  98    * @param pf - a proof of the conflict. This is only non-null if proofs
  99    * are enabled.
 100    */
 101   virtual void conflict(TNode n, std::unique_ptr<Proof> pf = nullptr) = 0;
 102
 103   /**
 104    * Propagate a theory literal.
 105    *
 106    * @param n - a theory consequence at the current decision level
 107    * @return false if an immediate conflict was encountered
 108    */
 109   virtual bool propagate(TNode n) = 0;
 110
 111   /**
 112    * Tell the core that a valid theory lemma at decision level 0 has
 113    * been detected.  (This requests a split.)
 114    *
 115    * @param n - a theory lemma valid at decision level 0
 116    * @param rule - the proof rule for this lemma
 117    * @param removable - whether the lemma can be removed at any point
 118    * @param preprocess - whether to apply more aggressive preprocessing
 119    * @param sendAtoms - whether to ensure atoms are sent to the theory
 120    * @return the "status" of the lemma, including user level at which
 121    * the lemma resides; the lemma will be removed when this user level pops
 122    */
 123   virtual LemmaStatus lemma(TNode n, ProofRule rule, bool removable = false,
 124                             bool preprocess = false,
 125                             bool sendAtoms = false) = 0;
 126
 127   /**
 128    * Variant of the lemma function that does not require providing a proof rule.
 129    */
 130   virtual LemmaStatus lemma(TNode n, bool removable = false,
 131                             bool preprocess = false, bool sendAtoms = false) {
 132     return lemma(n, RULE_INVALID, removable, preprocess, sendAtoms);
 133   }
 134
 135   /**
 136    * Request a split on a new theory atom.  This is equivalent to
 137    * calling lemma({OR n (NOT n)}).
 138    *
 139    * @param n - a theory atom; must be of Boolean type
 140    */
 141   LemmaStatus split(TNode n) { return splitLemma(n.orNode(n.notNode())); }
 142
 143   virtual LemmaStatus splitLemma(TNode n, bool removable = false) = 0;
 144
 145   /**
 146    * If a decision is made on n, it must be in the phase specified.
 147    * Note that this is enforced *globally*, i.e., it is completely
 148    * context-INdependent.  If you ever requirePhase() on a literal,
 149    * it is phase-locked forever and ever.  If it is to ever have the
 150    * other phase as its assignment, it will be because it has been
 151    * propagated that way (or it's a unit, at decision level 0).
 152    *
 153    * @param n - a theory atom with a SAT literal assigned; must have
 154    * been pre-registered
 155    * @param phase - the phase to decide on n
 156    */
 157   virtual void requirePhase(TNode n, bool phase) = 0;
 158
 159   /**
 160    * Notification from a theory that it realizes it is incomplete at
 161    * this context level.  If SAT is later determined by the
 162    * TheoryEngine, it should actually return an UNKNOWN result.
 163    */
 164   virtual void setIncomplete() = 0;
 165
 166   /**
 167    * "Spend" a "resource."  The meaning is specific to the context in
 168    * which the theory is operating, and may even be ignored.  The
 169    * intended meaning is that if the user has set a limit on the "units
 170    * of resource" that can be expended in a search, and that limit is
 171    * exceeded, then the search is terminated.  Note that the check for
 172    * termination occurs in the main search loop, so while theories
 173    * should call OutputChannel::spendResource() during particularly
 174    * long-running operations, they cannot rely on resource() to break
 175    * out of infinite or intractable computations.
 176    */
 177   virtual void spendResource(ResourceManager::Resource r) {}
 178
 179   /**
 180    * Handle user attribute.
 181    * Associates theory t with the attribute attr.  Theory t will be
 182    * notified whenever an attribute of name attr is set on a node.
 183    * This can happen through, for example, the SMT-LIBv2 language.
 184    */
 185   virtual void handleUserAttribute(const char* attr, Theory* t) {}
 186
 187   /** Demands that the search restart from sat search level 0.
 188    * Using this leads to non-termination issues.
 189    * It is appropriate for prototyping for theories.
 190    */
 191   virtual void demandRestart() {}
 192
 193   //---------------------------- new proof
 194   /**
 195    * Let pconf be the pair (Node conf, ProofGenerator * pfg). This method
 196    * sends conf on the output channel of this class whose proof can be generated
 197    * by the generator pfg. Apart from pfg, the interface for this method is
 198    * the same as OutputChannel.
 199    */
 200   virtual void trustedConflict(TrustNode pconf)
 201   {
 202     Unreachable() << "OutputChannel::trustedConflict: no implementation"
 203                   << std::endl;
 204   }
 205   /**
 206    * Let plem be the pair (Node lem, ProofGenerator * pfg).
 207    * Send lem on the output channel of this class whose proof can be generated
 208    * by the generator pfg. Apart from pfg, the interface for this method is
 209    * the same as OutputChannel.
 210    */
 211   virtual LemmaStatus trustedLemma(TrustNode lem,
 212                                    bool removable = false,
 213                                    bool preprocess = false,
 214                                    bool sendAtoms = false)
 215   {
 216     Unreachable() << "OutputChannel::trustedLemma: no implementation"
 217                   << std::endl;
 218   }
 219   //---------------------------- end new proof
 220 }; /* class OutputChannel */
 221
 222 }  // namespace theory
 223 }  // namespace CVC4
 224
 225 #endif /* CVC4__THEORY__OUTPUT_CHANNEL_H */