src/theory/trust_node.h

   1 /*********************                                                        */
   2 /*! \file trust_node.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   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 trust node utility
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__TRUST_NODE_H
  18 #define CVC4__THEORY__TRUST_NODE_H
  19
  20 #include "expr/node.h"
  21 #include "expr/proof_node.h"
  22
  23 namespace CVC4 {
  24
  25 class ProofGenerator;
  26
  27 namespace theory {
  28
  29 /** A kind for trust nodes */
  30 enum class TrustNodeKind : uint32_t
  31 {
  32   CONFLICT,
  33   LEMMA,
  34   PROP_EXP,
  35   REWRITE,
  36   INVALID
  37 };
  38 /**
  39  * Converts a proof rule to a string. Note: This function is also used in
  40  * `safe_print()`. Changing this function name or signature will result in
  41  * `safe_print()` printing "<unsupported>" instead of the proper strings for
  42  * the enum values.
  43  *
  44  * Returns a string with static lifetime: it should not be freed.
  45  *
  46  * @param tnk The trust node kind
  47  * @return The name of the trust node kind
  48  */
  49 const char* toString(TrustNodeKind tnk);
  50
  51 /**
  52  * Writes a trust node kind name to a stream.
  53  *
  54  * @param out The stream to write to
  55  * @param tnk The trust node kind to write to the stream
  56  * @return The stream
  57  */
  58 std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk);
  59
  60 /**
  61  * A trust node is a pair (F, G) where F is a formula and G is a proof
  62  * generator that can construct a proof for F if asked.
  63  *
  64  * More generally, a trust node is any node that can be used for a specific
  65  * purpose that requires justification, such as being passed to
  66  * OutputChannel::lemma. That justification is intended to be given by the
  67  * generator that is required to construct this object.
  68  *
  69  * They are intended to be constructed by ProofGenerator objects themselves (a
  70  * proof generator wraps itself in TrustNode it returns) and passed
  71  * to ProofOutputChannel by theory solvers.
  72  *
  73  * The static functions for constructing them check that the generator, if
  74  * provided, is capable of proving the given conflict or lemma, or an assertion
  75  * failure occurs. Otherwise an assertion error is given.
  76  *
  77  * While this is not enforced, a `TrustNode` generally encapsulates a **closed** proof
  78  * of the formula: one without free assumptions.
  79  */
  80 class TrustNode
  81 {
  82  public:
  83   TrustNode() : d_tnk(TrustNodeKind::INVALID), d_gen(nullptr) {}
  84   /** Make a proven node for conflict */
  85   static TrustNode mkTrustConflict(Node conf, ProofGenerator* g = nullptr);
  86   /** Make a proven node for lemma */
  87   static TrustNode mkTrustLemma(Node lem, ProofGenerator* g = nullptr);
  88   /** Make a proven node for explanation of propagated literal */
  89   static TrustNode mkTrustPropExp(TNode lit,
  90                                   Node exp,
  91                                   ProofGenerator* g = nullptr);
  92   /** Make a proven node for rewrite */
  93   static TrustNode mkTrustRewrite(TNode n,
  94                                   Node nr,
  95                                   ProofGenerator* g = nullptr);
  96   /** The null proven node */
  97   static TrustNode null();
  98   ~TrustNode() {}
  99   /** get kind */
 100   TrustNodeKind getKind() const;
 101   /** get node
 102    *
 103    * This is the node that is used in a common interface, either:
 104    * (1) A T-unsat conjunction conf to pass to OutputChannel::conflict,
 105    * (2) A valid T-formula lem to pass to OutputChannel::lemma,
 106    * (3) A conjunction of literals exp to return in Theory::explain(lit), or
 107    * (4) A result of rewriting a term n into an equivalent one nr.
 108    *
 109    * Notice that this node does not necessarily correspond to a valid formula.
 110    * The call getProven() below retrieves a valid formula corresponding to
 111    * the above calls.
 112    */
 113   Node getNode() const;
 114   /** get proven
 115    *
 116    * This is the corresponding formula that is proven by the proof generator
 117    * for the above cases:
 118    * (1) (not conf), for conflicts,
 119    * (2) lem, for lemmas,
 120    * (3) (=> exp lit), for propagations from explanations,
 121    * (4) (= n nr), for results of rewriting.
 122    *
 123    * When constructing this trust node, the proof generator should be able to
 124    * provide a proof for this fact.
 125    */
 126   Node getProven() const;
 127   /** get generator */
 128   ProofGenerator* getGenerator() const;
 129   /** is null? */
 130   bool isNull() const;
 131   /**
 132    * Gets the proof node for this trust node, which is obtained by
 133    * calling the generator's getProofFor method on the proven node.
 134    */
 135   std::shared_ptr<ProofNode> toProofNode() const;
 136
 137   /** Get the proven formula corresponding to a conflict call */
 138   static Node getConflictProven(Node conf);
 139   /** Get the proven formula corresponding to a lemma call */
 140   static Node getLemmaProven(Node lem);
 141   /** Get the proven formula corresponding to explanations for propagation */
 142   static Node getPropExpProven(TNode lit, Node exp);
 143   /** Get the proven formula corresponding to a rewrite */
 144   static Node getRewriteProven(TNode n, Node nr);
 145   /** For debugging */
 146   std::string identifyGenerator() const;
 147
 148   /**
 149    * debug check closed on Trace c, context ctx is string for debugging
 150    *
 151    * @param reqNullGen Whether we consider a null generator to be a failure.
 152    */
 153   void debugCheckClosed(const char* c, const char* ctx, bool reqNullGen = true);
 154
 155  private:
 156   TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g = nullptr);
 157   /** The kind */
 158   TrustNodeKind d_tnk;
 159   /** The proven node */
 160   Node d_proven;
 161   /** The generator */
 162   ProofGenerator* d_gen;
 163 };
 164
 165 /**
 166  * Writes a trust node to a stream.
 167  *
 168  * @param out The stream to write to
 169  * @param n The trust node to write to the stream
 170  * @return The stream
 171  */
 172 std::ostream& operator<<(std::ostream& out, TrustNode n);
 173
 174 }  // namespace theory
 175 }  // namespace CVC4
 176
 177 #endif /* CVC4__THEORY__TRUST_NODE_H */