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   //================================================= Boolean rules
  75   // ======== Split
  76   // Children: none
  77   // Arguments: (F)
  78   // ---------------------
  79   // Conclusion: (or F (not F))
  80   SPLIT,
  81   // ======== And elimination
  82   // Children: (P:(and F1 ... Fn))
  83   // Arguments: (i)
  84   // ---------------------
  85   // Conclusion: (Fi)
  86   AND_ELIM,
  87   // ======== And introduction
  88   // Children: (P1:F1 ... Pn:Fn))
  89   // Arguments: ()
  90   // ---------------------
  91   // Conclusion: (and P1 ... Pn)
  92   AND_INTRO,
  93   // ======== Not Or elimination
  94   // Children: (P:(not (or F1 ... Fn)))
  95   // Arguments: (i)
  96   // ---------------------
  97   // Conclusion: (not Fi)
  98   NOT_OR_ELIM,
  99   // ======== Implication elimination
 100   // Children: (P:(=> F1 F2))
 101   // Arguments: ()
 102   // ---------------------
 103   // Conclusion: (or (not F1) F2)
 104   IMPLIES_ELIM,
 105   // ======== Not Implication elimination version 1
 106   // Children: (P:(not (=> F1 F2)))
 107   // Arguments: ()
 108   // ---------------------
 109   // Conclusion: (F1)
 110   NOT_IMPLIES_ELIM1,
 111   // ======== Not Implication elimination version 2
 112   // Children: (P:(not (=> F1 F2)))
 113   // Arguments: ()
 114   // ---------------------
 115   // Conclusion: (not F2)
 116   NOT_IMPLIES_ELIM2,
 117   // ======== Equivalence elimination version 1
 118   // Children: (P:(= F1 F2))
 119   // Arguments: ()
 120   // ---------------------
 121   // Conclusion: (or (not F1) F2)
 122   EQUIV_ELIM1,
 123   // ======== Equivalence elimination version 2
 124   // Children: (P:(= F1 F2))
 125   // Arguments: ()
 126   // ---------------------
 127   // Conclusion: (or F1 (not F2))
 128   EQUIV_ELIM2,
 129   // ======== Not Equivalence elimination version 1
 130   // Children: (P:(not (= F1 F2)))
 131   // Arguments: ()
 132   // ---------------------
 133   // Conclusion: (or F1 F2)
 134   NOT_EQUIV_ELIM1,
 135   // ======== Not Equivalence elimination version 2
 136   // Children: (P:(not (= F1 F2)))
 137   // Arguments: ()
 138   // ---------------------
 139   // Conclusion: (or (not F1) (not F2))
 140   NOT_EQUIV_ELIM2,
 141   // ======== XOR elimination version 1
 142   // Children: (P:(xor F1 F2)))
 143   // Arguments: ()
 144   // ---------------------
 145   // Conclusion: (or F1 F2)
 146   XOR_ELIM1,
 147   // ======== XOR elimination version 2
 148   // Children: (P:(xor F1 F2)))
 149   // Arguments: ()
 150   // ---------------------
 151   // Conclusion: (or (not F1) (not F2))
 152   XOR_ELIM2,
 153   // ======== Not XOR elimination version 1
 154   // Children: (P:(not (xor F1 F2)))
 155   // Arguments: ()
 156   // ---------------------
 157   // Conclusion: (or F1 (not F2))
 158   NOT_XOR_ELIM1,
 159   // ======== Not XOR elimination version 2
 160   // Children: (P:(not (xor F1 F2)))
 161   // Arguments: ()
 162   // ---------------------
 163   // Conclusion: (or (not F1) F2)
 164   NOT_XOR_ELIM2,
 165   // ======== ITE elimination version 1
 166   // Children: (P:(ite C F1 F2))
 167   // Arguments: ()
 168   // ---------------------
 169   // Conclusion: (or (not C) F1)
 170   ITE_ELIM1,
 171   // ======== ITE elimination version 2
 172   // Children: (P:(ite C F1 F2))
 173   // Arguments: ()
 174   // ---------------------
 175   // Conclusion: (or C F2)
 176   ITE_ELIM2,
 177   // ======== Not ITE elimination version 1
 178   // Children: (P:(not (ite C F1 F2)))
 179   // Arguments: ()
 180   // ---------------------
 181   // Conclusion: (or (not C) (not F1))
 182   NOT_ITE_ELIM1,
 183   // ======== Not ITE elimination version 1
 184   // Children: (P:(not (ite C F1 F2)))
 185   // Arguments: ()
 186   // ---------------------
 187   // Conclusion: (or C (not F2))
 188   NOT_ITE_ELIM2,
 189   // ======== Not ITE elimination version 1
 190   // Children: (P1:P P2:(not P))
 191   // Arguments: ()
 192   // ---------------------
 193   // Conclusion: (false)
 194   CONTRA,
 195
 196   //================================================= De Morgan rules
 197   // ======== Not And
 198   // Children: (P:(not (and F1 ... Fn))
 199   // Arguments: ()
 200   // ---------------------
 201   // Conclusion: (or (not F1) ... (not Fn))
 202   NOT_AND,
 203   //================================================= CNF rules
 204   // ======== CNF And Pos
 205   // Children: ()
 206   // Arguments: ((and F1 ... Fn), i)
 207   // ---------------------
 208   // Conclusion: (or (not (and F1 ... Fn)) Fi)
 209   CNF_AND_POS,
 210   // ======== CNF And Neg
 211   // Children: ()
 212   // Arguments: ((and F1 ... Fn))
 213   // ---------------------
 214   // Conclusion: (or (and F1 ... Fn) (not F1) ... (not Fn))
 215   CNF_AND_NEG,
 216   // ======== CNF Or Pos
 217   // Children: ()
 218   // Arguments: ((or F1 ... Fn))
 219   // ---------------------
 220   // Conclusion: (or (not (or F1 ... Fn)) F1 ... Fn)
 221   CNF_OR_POS,
 222   // ======== CNF Or Neg
 223   // Children: ()
 224   // Arguments: ((or F1 ... Fn), i)
 225   // ---------------------
 226   // Conclusion: (or (or F1 ... Fn) (not Fi))
 227   CNF_OR_NEG,
 228   // ======== CNF Implies Pos
 229   // Children: ()
 230   // Arguments: ((implies F1 F2))
 231   // ---------------------
 232   // Conclusion: (or (not (implies F1 F2)) (not F1) F2)
 233   CNF_IMPLIES_POS,
 234   // ======== CNF Implies Neg version 1
 235   // Children: ()
 236   // Arguments: ((implies F1 F2))
 237   // ---------------------
 238   // Conclusion: (or (implies F1 F2) F1)
 239   CNF_IMPLIES_NEG1,
 240   // ======== CNF Implies Neg version 2
 241   // Children: ()
 242   // Arguments: ((implies F1 F2))
 243   // ---------------------
 244   // Conclusion: (or (implies F1 F2) (not F2))
 245   CNF_IMPLIES_NEG2,
 246   // ======== CNF Equiv Pos version 1
 247   // Children: ()
 248   // Arguments: ((= F1 F2))
 249   // ---------------------
 250   // Conclusion: (or (not (= F1 F2)) (not F1) F2)
 251   CNF_EQUIV_POS1,
 252   // ======== CNF Equiv Pos version 2
 253   // Children: ()
 254   // Arguments: ((= F1 F2))
 255   // ---------------------
 256   // Conclusion: (or (not (= F1 F2)) F1 (not F2))
 257   CNF_EQUIV_POS2,
 258   // ======== CNF Equiv Neg version 1
 259   // Children: ()
 260   // Arguments: ((= F1 F2))
 261   // ---------------------
 262   // Conclusion: (or (= F1 F2) F1 F2)
 263   CNF_EQUIV_NEG1,
 264   // ======== CNF Equiv Neg version 2
 265   // Children: ()
 266   // Arguments: ((= F1 F2))
 267   // ---------------------
 268   // Conclusion: (or (= F1 F2) (not F1) (not F2))
 269   CNF_EQUIV_NEG2,
 270   // ======== CNF Xor Pos version 1
 271   // Children: ()
 272   // Arguments: ((xor F1 F2))
 273   // ---------------------
 274   // Conclusion: (or (not (xor F1 F2)) F1 F2)
 275   CNF_XOR_POS1,
 276   // ======== CNF Xor Pos version 2
 277   // Children: ()
 278   // Arguments: ((xor F1 F2))
 279   // ---------------------
 280   // Conclusion: (or (not (xor F1 F2)) (not F1) (not F2))
 281   CNF_XOR_POS2,
 282   // ======== CNF Xor Neg version 1
 283   // Children: ()
 284   // Arguments: ((xor F1 F2))
 285   // ---------------------
 286   // Conclusion: (or (xor F1 F2) (not F1) F2)
 287   CNF_XOR_NEG1,
 288   // ======== CNF Xor Neg version 2
 289   // Children: ()
 290   // Arguments: ((xor F1 F2))
 291   // ---------------------
 292   // Conclusion: (or (xor F1 F2) F1 (not F2))
 293   CNF_XOR_NEG2,
 294   // ======== CNF ITE Pos version 1
 295   // Children: ()
 296   // Arguments: ((ite C F1 F2))
 297   // ---------------------
 298   // Conclusion: (or (not (ite C F1 F2)) (not C) F1)
 299   CNF_ITE_POS1,
 300   // ======== CNF ITE Pos version 2
 301   // Children: ()
 302   // Arguments: ((ite C F1 F2))
 303   // ---------------------
 304   // Conclusion: (or (not (ite C F1 F2)) C F2)
 305   CNF_ITE_POS2,
 306   // ======== CNF ITE Pos version 3
 307   // Children: ()
 308   // Arguments: ((ite C F1 F2))
 309   // ---------------------
 310   // Conclusion: (or (not (ite C F1 F2)) F1 F2)
 311   CNF_ITE_POS3,
 312   // ======== CNF ITE Neg version 1
 313   // Children: ()
 314   // Arguments: ((ite C F1 F2))
 315   // ---------------------
 316   // Conclusion: (or (ite C F1 F2) (not C) (not F1))
 317   CNF_ITE_NEG1,
 318   // ======== CNF ITE Neg version 2
 319   // Children: ()
 320   // Arguments: ((ite C F1 F2))
 321   // ---------------------
 322   // Conclusion: (or (ite C F1 F2) C (not F2))
 323   CNF_ITE_NEG2,
 324   // ======== CNF ITE Neg version 3
 325   // Children: ()
 326   // Arguments: ((ite C F1 F2))
 327   // ---------------------
 328   // Conclusion: (or (ite C F1 F2) (not F1) (not F2))
 329   CNF_ITE_NEG3,
 330
 331   //======================== Builtin theory (common node operations)
 332   // ======== Substitution
 333   // Children: (P1:F1, ..., Pn:Fn)
 334   // Arguments: (t, (ids)?)
 335   // ---------------------------------------------------------------
 336   // Conclusion: (= t t*sigma{ids}(Fn)*...*sigma{ids}(F1))
 337   // where sigma{ids}(Fi) are substitutions, which notice are applied in
 338   // reverse order.
 339   // Notice that ids is a MethodId identifier, which determines how to convert
 340   // the formulas F1, ..., Fn into substitutions.
 341   SUBS,
 342   // ======== Rewrite
 343   // Children: none
 344   // Arguments: (t, (idr)?)
 345   // ----------------------------------------
 346   // Conclusion: (= t Rewriter{idr}(t))
 347   // where idr is a MethodId identifier, which determines the kind of rewriter
 348   // to apply, e.g. Rewriter::rewrite.
 349   REWRITE,
 350   // ======== Substitution + Rewriting equality introduction
 351   //
 352   // In this rule, we provide a term t and conclude that it is equal to its
 353   // rewritten form under a (proven) substitution.
 354   //
 355   // Children: (P1:F1, ..., Pn:Fn)
 356   // Arguments: (t, (ids (idr)?)?)
 357   // ---------------------------------------------------------------
 358   // Conclusion: (= t t')
 359   // where
 360   //   t' is
 361   //   toWitness(Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1)))
 362   //   toSkolem(...) converts terms from witness form to Skolem form,
 363   //   toWitness(...) converts terms from Skolem form to witness form.
 364   //
 365   // Notice that:
 366   //   toSkolem(t')=Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1))
 367   // In other words, from the point of view of Skolem forms, this rule
 368   // transforms t to t' by standard substitution + rewriting.
 369   //
 370   // The argument ids and idr is optional and specify the identifier of the
 371   // substitution and rewriter respectively to be used. For details, see
 372   // theory/builtin/proof_checker.h.
 373   MACRO_SR_EQ_INTRO,
 374   // ======== Substitution + Rewriting predicate introduction
 375   //
 376   // In this rule, we provide a formula F and conclude it, under the condition
 377   // that it rewrites to true under a proven substitution.
 378   //
 379   // Children: (P1:F1, ..., Pn:Fn)
 380   // Arguments: (F, (ids (idr)?)?)
 381   // ---------------------------------------------------------------
 382   // Conclusion: F
 383   // where
 384   //   Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true
 385   // where ids and idr are method identifiers.
 386   //
 387   // Notice that we apply rewriting on the witness form of F, meaning that this
 388   // rule may conclude an F whose Skolem form is justified by the definition of
 389   // its (fresh) Skolem variables. Furthermore, notice that the rewriting and
 390   // substitution is applied only within the side condition, meaning the
 391   // rewritten form of the witness form of F does not escape this rule.
 392   MACRO_SR_PRED_INTRO,
 393   // ======== Substitution + Rewriting predicate elimination
 394   //
 395   // In this rule, if we have proven a formula F, then we may conclude its
 396   // rewritten form under a proven substitution.
 397   //
 398   // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
 399   // Arguments: ((ids (idr)?)?)
 400   // ----------------------------------------
 401   // Conclusion: F'
 402   // where
 403   //   F' is
 404   //   toWitness(Rewriter{idr}(toSkolem(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)).
 405   // where ids and idr are method identifiers.
 406   //
 407   // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
 408   MACRO_SR_PRED_ELIM,
 409   // ======== Substitution + Rewriting predicate transform
 410   //
 411   // In this rule, if we have proven a formula F, then we may provide a formula
 412   // G and conclude it if F and G are equivalent after rewriting under a proven
 413   // substitution.
 414   //
 415   // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
 416   // Arguments: (G, (ids (idr)?)?)
 417   // ----------------------------------------
 418   // Conclusion: G
 419   // where
 420   //   Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) ==
 421   //   Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1))
 422   //
 423   // Notice that we apply rewriting on the witness form of F and G, similar to
 424   // MACRO_SR_PRED_INTRO.
 425   MACRO_SR_PRED_TRANSFORM,
 426
 427   //================================================= Unknown rule
 428   UNKNOWN,
 429 };
 430
 431 /**
 432  * Converts a proof rule to a string. Note: This function is also used in
 433  * `safe_print()`. Changing this function name or signature will result in
 434  * `safe_print()` printing "<unsupported>" instead of the proper strings for
 435  * the enum values.
 436  *
 437  * @param id The proof rule
 438  * @return The name of the proof rule
 439  */
 440 const char* toString(PfRule id);
 441
 442 /**
 443  * Writes a proof rule name to a stream.
 444  *
 445  * @param out The stream to write to
 446  * @param id The proof rule to write to the stream
 447  * @return The stream
 448  */
 449 std::ostream& operator<<(std::ostream& out, PfRule id);
 450
 451 }  // namespace CVC4
 452
 453 #endif /* CVC4__EXPR__PROOF_RULE_H */