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
  24 namespace CVC4 {
  25
  26 class ProofNodeManager;
  27 class TermContext;
  28
  29 /** A policy for how rewrite steps are applied in TConvProofGenerator */
  30 enum class TConvPolicy : uint32_t
  31 {
  32   // steps are applied to fix-point, common use case is PfRule::REWRITE
  33   FIXPOINT,
  34   // steps are applied once at pre-rewrite, common use case is PfRule::SUBS
  35   ONCE,
  36 };
  37 /** Writes a term conversion policy name to a stream. */
  38 std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol);
  39
  40 /** A policy for how proofs are cached in TConvProofGenerator */
  41 enum class TConvCachePolicy : uint32_t
  42 {
  43   // proofs are statically cached
  44   STATIC,
  45   // proofs are dynamically cached, cleared when a new rewrite is added
  46   DYNAMIC,
  47   // proofs are never cached
  48   NEVER,
  49 };
  50 /** Writes a term conversion cache policy name to a stream. */
  51 std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol);
  52
  53 /**
  54  * The term conversion proof generator.
  55  *
  56  * This class is used for proofs of t = t', where t' is obtained from t by
  57  * applying (context-free) small step rewrites on subterms of t. Its main
  58  * interface functions are:
  59  * (1) addRewriteStep(t,s,<justification>) which notifies this class that t
  60  * rewrites to s, where justification is either a proof generator or proof
  61  * step,
  62  * (2) getProofFor(f) where f is any equality that can be justified by the
  63  * rewrite steps given above.
  64  *
  65  * For example, say we make the following calls:
  66  *   addRewriteStep(a,b,P1)
  67  *   addRewriteStep(f(a),c,P2)
  68  *   addRewriteStep(c,d,P3)
  69  * where P1 and P2 are proof steps. Afterwards, this class may justify any
  70  * equality t = s where s is obtained by applying the rewrites a->b, f(a)->c,
  71  * c->d, based on the strategy outlined below [***]. For example, the call to:
  72  *   getProofFor(g(f(a),h(a),f(e)) = g(d,h(b),f(e)))
  73  * will return the proof:
  74  *   CONG(
  75  *     TRANS(P2,P3),     ; f(a)=d
  76  *     CONG(P1 :args h), ; h(a)=h(b)
  77  *     REFL(:args f(e))  ; f(e)=f(e)
  78  *   :args g)
  79  *
  80  * [***] This class traverses the left hand side of a given equality-to-prove
  81  * (the term g(f(a),h(a),e) in the above example) and "replays" the rewrite
  82  * steps to obtain its rewritten form. To do so, it applies any available
  83  * rewrite step both at pre-rewrite (pre-order traversal) and post-rewrite
  84  * (post-order traversal). It thus does not require the user of this class to
  85  * distinguish whether a rewrite is a pre-rewrite or a post-rewrite during
  86  * addRewriteStep. In particular, notice that in the above example, we realize
  87  * that f(a) --> c at pre-rewrite instead of post-rewriting a --> b and then
  88  * ending with f(a)=f(b).
  89  *
  90  * This class may additionally be used for term-context-sensitive rewrite
  91  * systems. An example is the term formula removal pass which rewrites
  92  * terms dependending on whether they occur in a "term position", for details
  93  * see RtfTermContext in expr/term_context.h. To use this class in a way
  94  * that takes into account term contexts, the user of the term conversion
  95  * proof generator should:
  96  * (1) Provide a term context callback to the constructor of this class (tccb),
  97  * (2) Register rewrite steps that indicate the term context identifier of
  98  * the rewrite, which is a uint32_t.
  99  *
 100  * For example, RtfTermContext uses hash value 2 to indicate we are in a "term
 101  * position". Say the user of this class calls:
 102  *   addRewriteStep( (and A B), BOOLEAN_TERM_VARIABLE_1, pg, true, 2)
 103  * This indicates that (and A B) should rewrite to BOOLEAN_TERM_VARIABLE_1 if
 104  * (and A B) occurs in a term position, where pg is a proof generator that can
 105  * provide a closed proof of:
 106  *   (= (and A B) BOOLEAN_TERM_VARIABLE_1)
 107  * Subsequently, this class may respond to a call to getProofFor on:
 108  *   (=
 109  *     (or (and A B) (P (and A B)))
 110  *     (or (and A B) (P BOOLEAN_TERM_VARIABLE_1)))
 111  * where P is a predicate Bool -> Bool. The proof returned by this class
 112  * involves congruence and pg's proof of the equivalence above. In particular,
 113  * assuming its proof of the equivalence is P1, this proof is:
 114  *   (CONG{=} (CONG{or} (REFL (and A B)) (CONG{P} P1)))
 115  * Notice the callback provided to this class ensures that the rewrite is
 116  * replayed in the expected way, e.g. the occurrence of (and A B) that is not
 117  * in term position is not rewritten.
 118  */
 119 class TConvProofGenerator : public ProofGenerator
 120 {
 121  public:
 122   /**
 123    * Constructor, which notice does fixpoint rewriting (since this is the
 124    * most common use case) and never caches.
 125    *
 126    * @param pnm The proof node manager for constructing ProofNode objects.
 127    * @param c The context that this class depends on. If none is provided,
 128    * this class is context-independent.
 129    * @param tpol The policy for applying rewrite steps of this class. For
 130    * details, see d_policy.
 131    * @param cpol The caching policy for this generator.
 132    * @param name The name of this generator (for debugging).
 133    * @param tccb The term context callback that this class depends on. If this
 134    * is non-null, then this class stores a term-context-sensitive rewrite
 135    * system. The rewrite steps should be given term context identifiers.
 136    */
 137   TConvProofGenerator(ProofNodeManager* pnm,
 138                       context::Context* c = nullptr,
 139                       TConvPolicy pol = TConvPolicy::FIXPOINT,
 140                       TConvCachePolicy cpol = TConvCachePolicy::NEVER,
 141                       std::string name = "TConvProofGenerator",
 142                       TermContext* tccb = nullptr,
 143                       bool rewriteOps = false);
 144   ~TConvProofGenerator();
 145   /**
 146    * Add rewrite step t --> s based on proof generator.
 147    *
 148    * @param isPre Whether the rewrite is applied at prerewrite (pre-order
 149    * traversal).
 150    * @param trustId If a null proof generator is provided, we add a step to
 151    * the proof that has trustId as the rule and expected as the sole argument.
 152    * @param isClosed whether to expect that pg can provide a closed proof for
 153    * this fact.
 154    * @param tctx The term context identifier for the rewrite step. This
 155    * value should correspond to one generated by the term context callback
 156    * class provided in the argument tccb provided to the constructor of this
 157    * class.
 158    */
 159   void addRewriteStep(Node t,
 160                       Node s,
 161                       ProofGenerator* pg,
 162                       bool isPre = false,
 163                       PfRule trustId = PfRule::ASSUME,
 164                       bool isClosed = false,
 165                       uint32_t tctx = 0);
 166   /** Same as above, for a single step */
 167   void addRewriteStep(
 168       Node t, Node s, ProofStep ps, bool isPre = false, uint32_t tctx = 0);
 169   /** Same as above, with explicit arguments */
 170   void addRewriteStep(Node t,
 171                       Node s,
 172                       PfRule id,
 173                       const std::vector<Node>& children,
 174                       const std::vector<Node>& args,
 175                       bool isPre = false,
 176                       uint32_t tctx = 0);
 177   /** Has rewrite step for term t */
 178   bool hasRewriteStep(Node t, uint32_t tctx = 0, bool isPre = false) const;
 179   /**
 180    * Get rewrite step for term t, returns the s provided in a call to
 181    * addRewriteStep if one exists, or null otherwise.
 182    */
 183   Node getRewriteStep(Node t, uint32_t tctx = 0, bool isPre = false) const;
 184   /**
 185    * Get the proof for formula f. It should be the case that f is of the form
 186    * t = t', where t' is the result of rewriting t based on the rewrite steps
 187    * registered to this class.
 188    *
 189    * @param f The equality fact to get the proof for.
 190    * @return The proof for f.
 191    */
 192   std::shared_ptr<ProofNode> getProofFor(Node f) override;
 193   /** Identify this generator (for debugging, etc..) */
 194   std::string identify() const override;
 195
 196  protected:
 197   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
 198   /** A dummy context used by this class if none is provided */
 199   context::Context d_context;
 200   /** The (lazy) context dependent proof object. */
 201   LazyCDProof d_proof;
 202   /** map to rewritten forms */
 203   NodeNodeMap d_preRewriteMap;
 204   NodeNodeMap d_postRewriteMap;
 205   /**
 206    * Policy for how rewrites are applied to terms. As a simple example, say we
 207    * have registered the rewrite steps:
 208    *   addRewriteStep( a, f(c), p1 )
 209    *   addRewriteStep( c, d, p2 )
 210    * Then getProofForRewriting(f(a,c),pf) returns a proof of:
 211    *   f(a,c) = f(f(d),d) if d_policy is FIXPOINT,
 212    *   f(a,c) = f(f(c),d) if d_policy is ONCE.
 213    */
 214   TConvPolicy d_policy;
 215   /** The cache policy */
 216   TConvCachePolicy d_cpolicy;
 217   /** Name identifier */
 218   std::string d_name;
 219   /** The cache for terms */
 220   std::map<Node, std::shared_ptr<ProofNode> > d_cache;
 221   /** An (optional) term context object */
 222   TermContext* d_tcontext;
 223   /**
 224    * Whether we rewrite operators. If this flag is true, then the main
 225    * traversal algorithm of this proof generator traverses operators of
 226    * APPLY_UF and uses HO_CONG to justify rewriting of subterms when necessary.
 227    */
 228   bool d_rewriteOps;
 229   /** Get rewrite step for (hash value of) term. */
 230   Node getRewriteStepInternal(Node thash, bool isPre) const;
 231   /**
 232    * Adds a proof of t = t' to the proof pf where t' is the result of rewriting
 233    * t based on the rewrite steps registered to this class. This method then
 234    * returns the proved equality t = t'.
 235    */
 236   Node getProofForRewriting(Node t, LazyCDProof& pf, TermContext* tc = nullptr);
 237   /**
 238    * Register rewrite step, returns the equality t=s if t is distinct from s
 239    * and a rewrite step has not already been registered for t.
 240    */
 241   Node registerRewriteStep(Node t, Node s, uint32_t tctx, bool isPre);
 242   /** cache that r is the rewritten form of cur, pf can provide a proof */
 243   void doCache(Node curHash, Node cur, Node r, LazyCDProof& pf);
 244   /** get debug information on this generator */
 245   std::string toStringDebug() const;
 246 };
 247
 248 }  // namespace CVC4
 249
 250 #endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */