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