src/theory/eager_proof_generator.h

   1 /*********************                                                        */
   2 /*! \file eager_proof_generator.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 eager proof generator class
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__EAGER_PROOF_GENERATOR_H
  18 #define CVC4__THEORY__EAGER_PROOF_GENERATOR_H
  19
  20 #include "context/cdhashmap.h"
  21 #include "expr/node.h"
  22 #include "expr/proof_generator.h"
  23 #include "expr/proof_node.h"
  24 #include "theory/trust_node.h"
  25
  26 namespace CVC4 {
  27 namespace theory {
  28
  29 /**
  30  * An eager proof generator, with explicit proof caching.
  31  *
  32  * The intended use of this class is to store proofs for lemmas and conflicts
  33  * at the time they are sent out on the ProofOutputChannel. This means that the
  34  * getProofForConflict and getProofForLemma methods are lookups in a
  35  * (user-context depedent) map, the field d_proofs below.
  36  *
  37  * In detail, the method setProofForConflict(conf, pf) should be called prior to
  38  * calling ProofOutputChannel(TrustNode(conf,X)), where X is this generator.
  39  * Similarly for setProofForLemma.
  40  *
  41  * The intended usage of this class in combination with OutputChannel is
  42  * the following:
  43  * //-----------------------------------------------------------
  44  *   class MyEagerProofGenerator : public EagerProofGenerator
  45  *   {
  46  *     public:
  47  *      TrustNode getProvenConflictByMethodX(...)
  48  *      {
  49  *        // construct a conflict
  50  *        Node conf = [construct conflict];
  51  *        // construct a proof for conf
  52  *        std::shared_ptr<ProofNode> pf = [construct the proof for conf];
  53  *        // wrap the conflict in a trust node
  54  *        return mkTrustNode(conf,pf);
  55  *      }
  56  *   };
  57  *   // [1] Make objects given user context u and output channel out.
  58  *
  59  *   MyEagerProofGenerator epg(u);
  60  *   OutputChannel out;
  61  *
  62  *   // [2] Assume epg realizes there is a conflict. We have it store the proof
  63  *   // internally and return the conflict node paired with epg.
  64  *
  65  *   TrustNode pconf = epg.getProvenConflictByMethodX(...);
  66  *
  67  *   // [3] Send the conflict on the output channel.
  68  *
  69  *   out.trustedConflict(pconf);
  70  *
  71  *   // [4] The trust node has information about what is proven and who can
  72  *   // prove it, where this association is valid in the remainder of the user
  73  *   // context.
  74  *
  75  *   Node conf = pconf.getProven();
  76  *   ProofGenerator * pg = pconf.getGenerator();
  77  *   std::shared_ptr<ProofNode> pf = pg->getProofForConflict(conf);
  78  * //-----------------------------------------------------------
  79  * In other words, the proof generator epg is responsible for creating and
  80  * storing the proof internally, and the proof output channel is responsible for
  81  * maintaining the map that epg is who to ask for the proof of the conflict.
  82  */
  83 class EagerProofGenerator : public ProofGenerator
  84 {
  85   typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
  86       NodeProofNodeMap;
  87
  88  public:
  89   EagerProofGenerator(ProofNodeManager* pnm,
  90                       context::Context* c = nullptr,
  91                       std::string name = "EagerProofGenerator");
  92   ~EagerProofGenerator() {}
  93   /** Get the proof for formula f. */
  94   std::shared_ptr<ProofNode> getProofFor(Node f) override;
  95   /** Can we give the proof for formula f? */
  96   bool hasProofFor(Node f) override;
  97   /**
  98    * Set proof for fact f, called when pf is a proof of f.
  99    *
 100    * @param f The fact proven by pf,
 101    * @param pf The proof to store in this class.
 102    */
 103   void setProofFor(Node f, std::shared_ptr<ProofNode> pf);
 104   /**
 105    * Make trust node: wrap n in a trust node with this generator, and have it
 106    * store the proof pf to lemma or conflict n.
 107    *
 108    * @param n The proven node,
 109    * @param pf The proof of n,
 110    * @param isConflict Whether the returned trust node is a conflict (otherwise
 111    * it is a lemma),
 112    * @return The trust node corresponding to the fact that this generator has
 113    * a proof of n.
 114    */
 115   TrustNode mkTrustNode(Node n,
 116                         std::shared_ptr<ProofNode> pf,
 117                         bool isConflict = false);
 118   /**
 119    * Make trust node from a single step proof. This is a convenience function
 120    * that avoids the need to explictly construct ProofNode by the caller.
 121    *
 122    * @param conc The conclusion of the rule,
 123    * @param id The rule of the proof concluding conc
 124    * @param exp The explanation (premises) to the proof concluding conc,
 125    * @param args The arguments to the proof concluding conc,
 126    * @param isConflict Whether the returned trust node is a conflict (otherwise
 127    * it is a lemma),
 128    * @return The trust node corresponding to the fact that this generator has
 129    * a proof of (children => exp), or of exp if children is empty.
 130    */
 131   TrustNode mkTrustNode(Node conc,
 132                         PfRule id,
 133                         const std::vector<Node>& exp,
 134                         const std::vector<Node>& args,
 135                         bool isConflict = false);
 136   /**
 137    * Make trust node: wrap `exp => n` in a trust node with this generator, and
 138    * have it store the proof `pf` too.
 139    *
 140    * @param n The implication
 141    * @param exp A conjunction of literals that imply it
 142    * @param pf The proof of exp => n,
 143    * @return The trust node corresponding to the fact that this generator has
 144    * a proof of exp => n.
 145    */
 146   TrustNode mkTrustedPropagation(Node n,
 147                                  Node exp,
 148                                  std::shared_ptr<ProofNode> pf);
 149   //--------------------------------------- common proofs
 150   /**
 151    * This returns the trust node corresponding to the splitting lemma
 152    * (or f (not f)) and this generator. The method registers its proof in the
 153    * map maintained by this class.
 154    */
 155   TrustNode mkTrustNodeSplit(Node f);
 156   //--------------------------------------- end common proofs
 157   /** identify */
 158   std::string identify() const override;
 159
 160  protected:
 161   /** Set that pf is the proof for conflict conf */
 162   void setProofForConflict(Node conf, std::shared_ptr<ProofNode> pf);
 163   /** Set that pf is the proof for lemma lem */
 164   void setProofForLemma(Node lem, std::shared_ptr<ProofNode> pf);
 165   /** Set that pf is the proof for explained propagation */
 166   void setProofForPropExp(TNode lit, Node exp, std::shared_ptr<ProofNode> pf);
 167   /** The proof node manager */
 168   ProofNodeManager* d_pnm;
 169   /** Name identifier */
 170   std::string d_name;
 171   /** A dummy context used by this class if none is provided */
 172   context::Context d_context;
 173   /**
 174    * A user-context-dependent map from lemmas and conflicts to proofs provided
 175    * by calls to setProofForConflict and setProofForLemma above.
 176    */
 177   NodeProofNodeMap d_proofs;
 178 };
 179
 180 }  // namespace theory
 181 }  // namespace CVC4
 182
 183 #endif /* CVC4__THEORY__PROOF_GENERATOR_H */