src/theory/output_channel.h

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