src/expr/term_conversion_proof_generator.h

   1 /*********************                                                        */
   2 /*! \file term_conversion_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 Term conversion proof generator utility
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H
  18 #define CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H
  19
  20 #include "context/cdhashmap.h"
  21 #include "expr/lazy_proof.h"
  22 #include "expr/proof_generator.h"
  23 #include "expr/proof_node_manager.h"
  24
  25 namespace CVC4 {
  26
  27 /**
  28  * The term conversion proof generator.
  29  *
  30  * This class is used for proofs of t = t', where t' is obtained from t by
  31  * applying (context-free) small step rewrites on subterms of t. Its main
  32  * interface functions are:
  33  * (1) addRewriteStep(t,s,<justification>) which notifies this class that t
  34  * rewrites to s, where justification is either a proof generator or proof
  35  * step,
  36  * (2) getProofFor(f) where f is any equality that can be justified by the
  37  * rewrite steps given above.
  38  *
  39  * For example, say we make the following calls:
  40  *   addRewriteStep(a,b,P1)
  41  *   addRewriteStep(f(a),c,P2)
  42  *   addRewriteStep(c,d,P3)
  43  * where P1 and P2 are proof steps. Afterwards, this class may justify any
  44  * equality t = s where s is obtained by applying the rewrites a->b, f(a)->c,
  45  * c->d, based on the strategy outlined below [***]. For example, the call to:
  46  *   getProofFor(g(f(a),h(a),f(e)) = g(d,h(b),f(e)))
  47  * will return the proof:
  48  *   CONG(
  49  *     TRANS(P2,P3),     ; f(a)=d
  50  *     CONG(P1 :args h), ; h(a)=h(b)
  51  *     REFL(:args f(e))  ; f(e)=f(e)
  52  *   :args g)
  53  *
  54  * [***] This class traverses the left hand side of a given equality-to-prove
  55  * (the term g(f(a),h(a),e) in the above example) and "replays" the rewrite
  56  * steps to obtain its rewritten form. To do so, it applies any available
  57  * rewrite step both at pre-rewrite (pre-order traversal) and post-rewrite
  58  * (post-order traversal). It thus does not require the user of this class to
  59  * distinguish whether a rewrite is a pre-rewrite or a post-rewrite during
  60  * addRewriteStep. In particular, notice that in the above example, we realize
  61  * that f(a) --> c at pre-rewrite instead of post-rewriting a --> b and then
  62  * ending with f(a)=f(b).
  63  */
  64 class TConvProofGenerator : public ProofGenerator
  65 {
  66  public:
  67   /** Constructor
  68    *
  69    * @param pnm The proof node manager for constructing ProofNode objects.
  70    * @param c The context that this class depends on. If none is provided,
  71    * this class is context-independent.
  72    */
  73   TConvProofGenerator(ProofNodeManager* pnm, context::Context* c = nullptr);
  74   ~TConvProofGenerator();
  75   /**
  76    * Add rewrite step t --> s based on proof generator.
  77    */
  78   void addRewriteStep(Node t, Node s, ProofGenerator* pg);
  79   /** Same as above, for a single step */
  80   void addRewriteStep(Node t, Node s, ProofStep ps);
  81   /** Same as above, with explicit arguments */
  82   void addRewriteStep(Node t,
  83                       Node s,
  84                       PfRule id,
  85                       const std::vector<Node>& children,
  86                       const std::vector<Node>& args);
  87   /** Has rewrite step for term t */
  88   bool hasRewriteStep(Node t) const;
  89   /**
  90    * Get rewrite step for term t, returns the s provided in a call to
  91    * addRewriteStep if one exists, or null otherwise.
  92    */
  93   Node getRewriteStep(Node t) const;
  94   /**
  95    * Get the proof for formula f. It should be the case that f is of the form
  96    * t = t', where t' is the result of rewriting t based on the rewrite steps
  97    * registered to this class.
  98    *
  99    * @param f The fact to get the proof for.
 100    * @return The proof for f.
 101    */
 102   std::shared_ptr<ProofNode> getProofFor(Node f) override;
 103   /** Identify this generator (for debugging, etc..) */
 104   std::string identify() const override;
 105
 106  protected:
 107   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
 108   /** A dummy context used by this class if none is provided */
 109   context::Context d_context;
 110   /** The (lazy) context dependent proof object. */
 111   LazyCDProof d_proof;
 112   /** map to rewritten forms */
 113   NodeNodeMap d_rewriteMap;
 114   /**
 115    * Get the proof for term t. Returns a proof of t = t' where t' is the
 116    * result of rewriting t based on the rewrite steps registered to this class.
 117    */
 118   std::shared_ptr<ProofNode> getProofForRewriting(Node t);
 119 };
 120
 121 }  // namespace CVC4
 122
 123 #endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */