src/expr/proof_rule.h

   1 /*********************                                                        */
   2 /*! \file proof_rule.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-2019 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 Proof rule enumeration
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__EXPR__PROOF_RULE_H
  18 #define CVC4__EXPR__PROOF_RULE_H
  19
  20 #include <iosfwd>
  21
  22 namespace CVC4 {
  23
  24 /**
  25  * An enumeration for proof rules. This enumeration is analogous to Kind for
  26  * Node objects. In the documentation below, P:F denotes a ProofNode that
  27  * proves formula F.
  28  *
  29  * Conceptually, the following proof rules form a calculus whose target
  30  * user is the Node-level theory solvers. This means that the rules below
  31  * are designed to reason about, among other things, common operations on Node
  32  * objects like Rewriter::rewrite or Node::substitute. It is intended to be
  33  * translated or printed in other formats.
  34  *
  35  * The following PfRule values include core rules and those categorized by
  36  * theory, including the theory of equality.
  37  *
  38  * The "core rules" include two distinguished rules which have special status:
  39  * (1) ASSUME, which represents an open leaf in a proof.
  40  * (2) SCOPE, which closes the scope of assumptions.
  41  * The core rules additionally correspond to generic operations that are done
  42  * internally on nodes, e.g. calling Rewriter::rewrite.
  43  */
  44 enum class PfRule : uint32_t
  45 {
  46   //================================================= Core rules
  47   //======================== Assume and Scope
  48   // ======== Assumption (a leaf)
  49   // Children: none
  50   // Arguments: (F)
  51   // --------------
  52   // Conclusion: F
  53   //
  54   // This rule has special status, in that an application of assume is an
  55   // open leaf in a proof that is not (yet) justified. An assume leaf is
  56   // analogous to a free variable in a term, where we say "F is a free
  57   // assumption in proof P" if it contains an application of F that is not
  58   // bound by SCOPE (see below).
  59   ASSUME,
  60   // ======== Scope (a binder for assumptions)
  61   // Children: (P:F)
  62   // Arguments: (F1, ..., Fn)
  63   // --------------
  64   // Conclusion: (=> (and F1 ... Fn) F) or (not (and F1 ... Fn)) if F is false
  65   //
  66   // This rule has a dual purpose with ASSUME. It is a way to close
  67   // assumptions in a proof. We require that F1 ... Fn are free assumptions in
  68   // P and say that F1, ..., Fn are not free in (SCOPE P). In other words, they
  69   // are bound by this application. For example, the proof node:
  70   //   (SCOPE (ASSUME F) :args F)
  71   // has the conclusion (=> F F) and has no free assumptions. More generally, a
  72   // proof with no free assumptions always concludes a valid formula.
  73   SCOPE,
  74
  75   //======================== Builtin theory (common node operations)
  76   // ======== Substitution
  77   // Children: (P1:F1, ..., Pn:Fn)
  78   // Arguments: (t, (ids)?)
  79   // ---------------------------------------------------------------
  80   // Conclusion: (= t t*sigma{ids}(Fn)*...*sigma{ids}(F1))
  81   // where sigma{ids}(Fi) are substitutions, which notice are applied in
  82   // reverse order.
  83   // Notice that ids is a MethodId identifier, which determines how to convert
  84   // the formulas F1, ..., Fn into substitutions.
  85   SUBS,
  86   // ======== Rewrite
  87   // Children: none
  88   // Arguments: (t, (idr)?)
  89   // ----------------------------------------
  90   // Conclusion: (= t Rewriter{idr}(t))
  91   // where idr is a MethodId identifier, which determines the kind of rewriter
  92   // to apply, e.g. Rewriter::rewrite.
  93   REWRITE,
  94   // ======== Substitution + Rewriting equality introduction
  95   //
  96   // In this rule, we provide a term t and conclude that it is equal to its
  97   // rewritten form under a (proven) substitution.
  98   //
  99   // Children: (P1:F1, ..., Pn:Fn)
 100   // Arguments: (t, (ids (idr)?)?)
 101   // ---------------------------------------------------------------
 102   // Conclusion: (= t t')
 103   // where
 104   //   t' is
 105   //   toWitness(Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1)))
 106   //   toSkolem(...) converts terms from witness form to Skolem form,
 107   //   toWitness(...) converts terms from Skolem form to witness form.
 108   //
 109   // Notice that:
 110   //   toSkolem(t')=Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1))
 111   // In other words, from the point of view of Skolem forms, this rule
 112   // transforms t to t' by standard substitution + rewriting.
 113   //
 114   // The argument ids and idr is optional and specify the identifier of the
 115   // substitution and rewriter respectively to be used. For details, see
 116   // theory/builtin/proof_checker.h.
 117   MACRO_SR_EQ_INTRO,
 118   // ======== Substitution + Rewriting predicate introduction
 119   //
 120   // In this rule, we provide a formula F and conclude it, under the condition
 121   // that it rewrites to true under a proven substitution.
 122   //
 123   // Children: (P1:F1, ..., Pn:Fn)
 124   // Arguments: (F, (ids (idr)?)?)
 125   // ---------------------------------------------------------------
 126   // Conclusion: F
 127   // where
 128   //   Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true
 129   // where ids and idr are method identifiers.
 130   //
 131   // Notice that we apply rewriting on the witness form of F, meaning that this
 132   // rule may conclude an F whose Skolem form is justified by the definition of
 133   // its (fresh) Skolem variables. Furthermore, notice that the rewriting and
 134   // substitution is applied only within the side condition, meaning the
 135   // rewritten form of the witness form of F does not escape this rule.
 136   MACRO_SR_PRED_INTRO,
 137   // ======== Substitution + Rewriting predicate elimination
 138   //
 139   // In this rule, if we have proven a formula F, then we may conclude its
 140   // rewritten form under a proven substitution.
 141   //
 142   // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
 143   // Arguments: ((ids (idr)?)?)
 144   // ----------------------------------------
 145   // Conclusion: F'
 146   // where
 147   //   F' is
 148   //   toWitness(Rewriter{idr}(toSkolem(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)).
 149   // where ids and idr are method identifiers.
 150   //
 151   // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
 152   MACRO_SR_PRED_ELIM,
 153   // ======== Substitution + Rewriting predicate transform
 154   //
 155   // In this rule, if we have proven a formula F, then we may provide a formula
 156   // G and conclude it if F and G are equivalent after rewriting under a proven
 157   // substitution.
 158   //
 159   // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
 160   // Arguments: (G, (ids (idr)?)?)
 161   // ----------------------------------------
 162   // Conclusion: G
 163   // where
 164   //   Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) ==
 165   //   Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1))
 166   //
 167   // Notice that we apply rewriting on the witness form of F and G, similar to
 168   // MACRO_SR_PRED_INTRO.
 169   MACRO_SR_PRED_TRANSFORM,
 170
 171   //================================================= Unknown rule
 172   UNKNOWN,
 173 };
 174
 175 /**
 176  * Converts a proof rule to a string. Note: This function is also used in
 177  * `safe_print()`. Changing this function name or signature will result in
 178  * `safe_print()` printing "<unsupported>" instead of the proper strings for
 179  * the enum values.
 180  *
 181  * @param id The proof rule
 182  * @return The name of the proof rule
 183  */
 184 const char* toString(PfRule id);
 185
 186 /**
 187  * Writes a proof rule name to a stream.
 188  *
 189  * @param out The stream to write to
 190  * @param id The proof rule to write to the stream
 191  * @return The stream
 192  */
 193 std::ostream& operator<<(std::ostream& out, PfRule id);
 194
 195 }  // namespace CVC4
 196
 197 #endif /* CVC4__EXPR__PROOF_RULE_H */