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