src/expr/proof_rule.h

   1 /*********************                                                        */
   2 /*! \file proof_rule.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Haniel Barbosa, 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 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   //   Rewriter{idr}(t*sigma{ids}(Fn)*...*sigma{ids}(F1))
 106   //
 107   // In other words, from the point of view of Skolem forms, this rule
 108   // transforms t to t' by standard substitution + rewriting.
 109   //
 110   // The argument ids and idr is optional and specify the identifier of the
 111   // substitution and rewriter respectively to be used. For details, see
 112   // theory/builtin/proof_checker.h.
 113   MACRO_SR_EQ_INTRO,
 114   // ======== Substitution + Rewriting predicate introduction
 115   //
 116   // In this rule, we provide a formula F and conclude it, under the condition
 117   // that it rewrites to true under a proven substitution.
 118   //
 119   // Children: (P1:F1, ..., Pn:Fn)
 120   // Arguments: (F, (ids (idr)?)?)
 121   // ---------------------------------------------------------------
 122   // Conclusion: F
 123   // where
 124   //   Rewriter{idr}(toWitness(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true
 125   // where ids and idr are method identifiers.
 126   //
 127   // Notice that we apply rewriting on the witness form of F, meaning that this
 128   // rule may conclude an F whose Skolem form is justified by the definition of
 129   // its (fresh) Skolem variables. Furthermore, notice that the rewriting and
 130   // substitution is applied only within the side condition, meaning the
 131   // rewritten form of the witness form of F does not escape this rule.
 132   MACRO_SR_PRED_INTRO,
 133   // ======== Substitution + Rewriting predicate elimination
 134   //
 135   // In this rule, if we have proven a formula F, then we may conclude its
 136   // rewritten form under a proven substitution.
 137   //
 138   // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
 139   // Arguments: ((ids (idr)?)?)
 140   // ----------------------------------------
 141   // Conclusion: F'
 142   // where
 143   //   F' is
 144   //   Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)).
 145   // where ids and idr are method identifiers.
 146   //
 147   // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
 148   MACRO_SR_PRED_ELIM,
 149   // ======== Substitution + Rewriting predicate transform
 150   //
 151   // In this rule, if we have proven a formula F, then we may provide a formula
 152   // G and conclude it if F and G are equivalent after rewriting under a proven
 153   // substitution.
 154   //
 155   // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
 156   // Arguments: (G, (ids (idr)?)?)
 157   // ----------------------------------------
 158   // Conclusion: G
 159   // where
 160   //   Rewriter{idr}(toWitness(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)) ==
 161   //   Rewriter{idr}(toWitness(G)*sigma{ids}(Fn)*...*sigma{ids}(F1))
 162   //
 163   // Notice that we apply rewriting on the witness form of F and G, similar to
 164   // MACRO_SR_PRED_INTRO.
 165   MACRO_SR_PRED_TRANSFORM,
 166   // ======== Theory Rewrite
 167   // Children: none
 168   // Arguments: (t, preRewrite?)
 169   // ----------------------------------------
 170   // Conclusion: (= t t')
 171   // where
 172   //  t' is the result of applying either a pre-rewrite or a post-rewrite step
 173   //  to t (depending on the second argument).
 174   THEORY_REWRITE,
 175
 176   //================================================= Processing rules
 177   // ======== Preprocess
 178   // Children: none
 179   // Arguments: (F)
 180   // ---------------------------------------------------------------
 181   // Conclusion: F
 182   // where F is an equality of the form t = t' where t was replaced by t'
 183   // based on some preprocessing pass, or otherwise F was added as a new
 184   // assertion by some preprocessing pass.
 185   PREPROCESS,
 186   //================================================= Boolean rules
 187   // ======== Split
 188   // Children: none
 189   // Arguments: (F)
 190   // ---------------------
 191   // Conclusion: (or F (not F))
 192   SPLIT,
 193   // ======== Equality resolution
 194   // Children: (P1:F1, P2:(= F1 F2))
 195   // Arguments: none
 196   // ---------------------
 197   // Conclusion: (F2)
 198   // Note this can optionally be seen as a macro for EQUIV_ELIM1+RESOLUTION.
 199   EQ_RESOLVE,
 200   // ======== And elimination
 201   // Children: (P:(and F1 ... Fn))
 202   // Arguments: (i)
 203   // ---------------------
 204   // Conclusion: (Fi)
 205   AND_ELIM,
 206   // ======== And introduction
 207   // Children: (P1:F1 ... Pn:Fn))
 208   // Arguments: ()
 209   // ---------------------
 210   // Conclusion: (and P1 ... Pn)
 211   AND_INTRO,
 212   // ======== Not Or elimination
 213   // Children: (P:(not (or F1 ... Fn)))
 214   // Arguments: (i)
 215   // ---------------------
 216   // Conclusion: (not Fi)
 217   NOT_OR_ELIM,
 218   // ======== Implication elimination
 219   // Children: (P:(=> F1 F2))
 220   // Arguments: ()
 221   // ---------------------
 222   // Conclusion: (or (not F1) F2)
 223   IMPLIES_ELIM,
 224   // ======== Not Implication elimination version 1
 225   // Children: (P:(not (=> F1 F2)))
 226   // Arguments: ()
 227   // ---------------------
 228   // Conclusion: (F1)
 229   NOT_IMPLIES_ELIM1,
 230   // ======== Not Implication elimination version 2
 231   // Children: (P:(not (=> F1 F2)))
 232   // Arguments: ()
 233   // ---------------------
 234   // Conclusion: (not F2)
 235   NOT_IMPLIES_ELIM2,
 236   // ======== Equivalence elimination version 1
 237   // Children: (P:(= F1 F2))
 238   // Arguments: ()
 239   // ---------------------
 240   // Conclusion: (or (not F1) F2)
 241   EQUIV_ELIM1,
 242   // ======== Equivalence elimination version 2
 243   // Children: (P:(= F1 F2))
 244   // Arguments: ()
 245   // ---------------------
 246   // Conclusion: (or F1 (not F2))
 247   EQUIV_ELIM2,
 248   // ======== Not Equivalence elimination version 1
 249   // Children: (P:(not (= F1 F2)))
 250   // Arguments: ()
 251   // ---------------------
 252   // Conclusion: (or F1 F2)
 253   NOT_EQUIV_ELIM1,
 254   // ======== Not Equivalence elimination version 2
 255   // Children: (P:(not (= F1 F2)))
 256   // Arguments: ()
 257   // ---------------------
 258   // Conclusion: (or (not F1) (not F2))
 259   NOT_EQUIV_ELIM2,
 260   // ======== XOR elimination version 1
 261   // Children: (P:(xor F1 F2)))
 262   // Arguments: ()
 263   // ---------------------
 264   // Conclusion: (or F1 F2)
 265   XOR_ELIM1,
 266   // ======== XOR elimination version 2
 267   // Children: (P:(xor F1 F2)))
 268   // Arguments: ()
 269   // ---------------------
 270   // Conclusion: (or (not F1) (not F2))
 271   XOR_ELIM2,
 272   // ======== Not XOR elimination version 1
 273   // Children: (P:(not (xor F1 F2)))
 274   // Arguments: ()
 275   // ---------------------
 276   // Conclusion: (or F1 (not F2))
 277   NOT_XOR_ELIM1,
 278   // ======== Not XOR elimination version 2
 279   // Children: (P:(not (xor F1 F2)))
 280   // Arguments: ()
 281   // ---------------------
 282   // Conclusion: (or (not F1) F2)
 283   NOT_XOR_ELIM2,
 284   // ======== ITE elimination version 1
 285   // Children: (P:(ite C F1 F2))
 286   // Arguments: ()
 287   // ---------------------
 288   // Conclusion: (or (not C) F1)
 289   ITE_ELIM1,
 290   // ======== ITE elimination version 2
 291   // Children: (P:(ite C F1 F2))
 292   // Arguments: ()
 293   // ---------------------
 294   // Conclusion: (or C F2)
 295   ITE_ELIM2,
 296   // ======== Not ITE elimination version 1
 297   // Children: (P:(not (ite C F1 F2)))
 298   // Arguments: ()
 299   // ---------------------
 300   // Conclusion: (or (not C) (not F1))
 301   NOT_ITE_ELIM1,
 302   // ======== Not ITE elimination version 1
 303   // Children: (P:(not (ite C F1 F2)))
 304   // Arguments: ()
 305   // ---------------------
 306   // Conclusion: (or C (not F2))
 307   NOT_ITE_ELIM2,
 308   // ======== Not ITE elimination version 1
 309   // Children: (P1:P P2:(not P))
 310   // Arguments: ()
 311   // ---------------------
 312   // Conclusion: (false)
 313   CONTRA,
 314
 315   //================================================= De Morgan rules
 316   // ======== Not And
 317   // Children: (P:(not (and F1 ... Fn))
 318   // Arguments: ()
 319   // ---------------------
 320   // Conclusion: (or (not F1) ... (not Fn))
 321   NOT_AND,
 322   //================================================= CNF rules
 323   // ======== CNF And Pos
 324   // Children: ()
 325   // Arguments: ((and F1 ... Fn), i)
 326   // ---------------------
 327   // Conclusion: (or (not (and F1 ... Fn)) Fi)
 328   CNF_AND_POS,
 329   // ======== CNF And Neg
 330   // Children: ()
 331   // Arguments: ((and F1 ... Fn))
 332   // ---------------------
 333   // Conclusion: (or (and F1 ... Fn) (not F1) ... (not Fn))
 334   CNF_AND_NEG,
 335   // ======== CNF Or Pos
 336   // Children: ()
 337   // Arguments: ((or F1 ... Fn))
 338   // ---------------------
 339   // Conclusion: (or (not (or F1 ... Fn)) F1 ... Fn)
 340   CNF_OR_POS,
 341   // ======== CNF Or Neg
 342   // Children: ()
 343   // Arguments: ((or F1 ... Fn), i)
 344   // ---------------------
 345   // Conclusion: (or (or F1 ... Fn) (not Fi))
 346   CNF_OR_NEG,
 347   // ======== CNF Implies Pos
 348   // Children: ()
 349   // Arguments: ((implies F1 F2))
 350   // ---------------------
 351   // Conclusion: (or (not (implies F1 F2)) (not F1) F2)
 352   CNF_IMPLIES_POS,
 353   // ======== CNF Implies Neg version 1
 354   // Children: ()
 355   // Arguments: ((implies F1 F2))
 356   // ---------------------
 357   // Conclusion: (or (implies F1 F2) F1)
 358   CNF_IMPLIES_NEG1,
 359   // ======== CNF Implies Neg version 2
 360   // Children: ()
 361   // Arguments: ((implies F1 F2))
 362   // ---------------------
 363   // Conclusion: (or (implies F1 F2) (not F2))
 364   CNF_IMPLIES_NEG2,
 365   // ======== CNF Equiv Pos version 1
 366   // Children: ()
 367   // Arguments: ((= F1 F2))
 368   // ---------------------
 369   // Conclusion: (or (not (= F1 F2)) (not F1) F2)
 370   CNF_EQUIV_POS1,
 371   // ======== CNF Equiv Pos version 2
 372   // Children: ()
 373   // Arguments: ((= F1 F2))
 374   // ---------------------
 375   // Conclusion: (or (not (= F1 F2)) F1 (not F2))
 376   CNF_EQUIV_POS2,
 377   // ======== CNF Equiv Neg version 1
 378   // Children: ()
 379   // Arguments: ((= F1 F2))
 380   // ---------------------
 381   // Conclusion: (or (= F1 F2) F1 F2)
 382   CNF_EQUIV_NEG1,
 383   // ======== CNF Equiv Neg version 2
 384   // Children: ()
 385   // Arguments: ((= F1 F2))
 386   // ---------------------
 387   // Conclusion: (or (= F1 F2) (not F1) (not F2))
 388   CNF_EQUIV_NEG2,
 389   // ======== CNF Xor Pos version 1
 390   // Children: ()
 391   // Arguments: ((xor F1 F2))
 392   // ---------------------
 393   // Conclusion: (or (not (xor F1 F2)) F1 F2)
 394   CNF_XOR_POS1,
 395   // ======== CNF Xor Pos version 2
 396   // Children: ()
 397   // Arguments: ((xor F1 F2))
 398   // ---------------------
 399   // Conclusion: (or (not (xor F1 F2)) (not F1) (not F2))
 400   CNF_XOR_POS2,
 401   // ======== CNF Xor Neg version 1
 402   // Children: ()
 403   // Arguments: ((xor F1 F2))
 404   // ---------------------
 405   // Conclusion: (or (xor F1 F2) (not F1) F2)
 406   CNF_XOR_NEG1,
 407   // ======== CNF Xor Neg version 2
 408   // Children: ()
 409   // Arguments: ((xor F1 F2))
 410   // ---------------------
 411   // Conclusion: (or (xor F1 F2) F1 (not F2))
 412   CNF_XOR_NEG2,
 413   // ======== CNF ITE Pos version 1
 414   // Children: ()
 415   // Arguments: ((ite C F1 F2))
 416   // ---------------------
 417   // Conclusion: (or (not (ite C F1 F2)) (not C) F1)
 418   CNF_ITE_POS1,
 419   // ======== CNF ITE Pos version 2
 420   // Children: ()
 421   // Arguments: ((ite C F1 F2))
 422   // ---------------------
 423   // Conclusion: (or (not (ite C F1 F2)) C F2)
 424   CNF_ITE_POS2,
 425   // ======== CNF ITE Pos version 3
 426   // Children: ()
 427   // Arguments: ((ite C F1 F2))
 428   // ---------------------
 429   // Conclusion: (or (not (ite C F1 F2)) F1 F2)
 430   CNF_ITE_POS3,
 431   // ======== CNF ITE Neg version 1
 432   // Children: ()
 433   // Arguments: ((ite C F1 F2))
 434   // ---------------------
 435   // Conclusion: (or (ite C F1 F2) (not C) (not F1))
 436   CNF_ITE_NEG1,
 437   // ======== CNF ITE Neg version 2
 438   // Children: ()
 439   // Arguments: ((ite C F1 F2))
 440   // ---------------------
 441   // Conclusion: (or (ite C F1 F2) C (not F2))
 442   CNF_ITE_NEG2,
 443   // ======== CNF ITE Neg version 3
 444   // Children: ()
 445   // Arguments: ((ite C F1 F2))
 446   // ---------------------
 447   // Conclusion: (or (ite C F1 F2) (not F1) (not F2))
 448   CNF_ITE_NEG3,
 449
 450   //================================================= Equality rules
 451   // ======== Reflexive
 452   // Children: none
 453   // Arguments: (t)
 454   // ---------------------
 455   // Conclusion: (= t t)
 456   REFL,
 457   // ======== Symmetric
 458   // Children: (P:(= t1 t2)) or (P:(not (= t1 t2)))
 459   // Arguments: none
 460   // -----------------------
 461   // Conclusion: (= t2 t1) or (not (= t2 t1))
 462   SYMM,
 463   // ======== Transitivity
 464   // Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn))
 465   // Arguments: none
 466   // -----------------------
 467   // Conclusion: (= t1 tn)
 468   TRANS,
 469   // ======== Congruence  (subsumed by Substitute?)
 470   // Children: (P1:(= t1 s1), ..., Pn:(= tn sn))
 471   // Arguments: (f)
 472   // ---------------------------------------------
 473   // Conclusion: (= (f t1 ... tn) (f s1 ... sn))
 474   CONG,
 475   // ======== True intro
 476   // Children: (P:F)
 477   // Arguments: none
 478   // ----------------------------------------
 479   // Conclusion: (= F true)
 480   TRUE_INTRO,
 481   // ======== True elim
 482   // Children: (P:(= F true)
 483   // Arguments: none
 484   // ----------------------------------------
 485   // Conclusion: F
 486   TRUE_ELIM,
 487   // ======== False intro
 488   // Children: (P:(not F))
 489   // Arguments: none
 490   // ----------------------------------------
 491   // Conclusion: (= F false)
 492   FALSE_INTRO,
 493   // ======== False elim
 494   // Children: (P:(= F false)
 495   // Arguments: none
 496   // ----------------------------------------
 497   // Conclusion: (not F)
 498   FALSE_ELIM,
 499
 500   //================================================= Quantifiers rules
 501   // ======== Witness intro
 502   // Children: (P:F[t])
 503   // Arguments: (t)
 504   // ----------------------------------------
 505   // Conclusion: (= t (witness ((x T)) F[x]))
 506   // where x is a BOUND_VARIABLE unique to the pair F,t.
 507   WITNESS_INTRO,
 508   // ======== Exists intro
 509   // Children: (P:F[t])
 510   // Arguments: (t)
 511   // ----------------------------------------
 512   // Conclusion: (exists ((x T)) F[x])
 513   // where x is a BOUND_VARIABLE unique to the pair F,t.
 514   EXISTS_INTRO,
 515   // ======== Skolemize
 516   // Children: (P:(exists ((x1 T1) ... (xn Tn)) F))
 517   // Arguments: none
 518   // ----------------------------------------
 519   // Conclusion: F*sigma
 520   // sigma maps x1 ... xn to their representative skolems obtained by
 521   // SkolemManager::mkSkolemize, returned in the skolems argument of that
 522   // method.
 523   SKOLEMIZE,
 524   // ======== Instantiate
 525   // Children: (P:(forall ((x1 T1) ... (xn Tn)) F))
 526   // Arguments: (t1 ... tn)
 527   // ----------------------------------------
 528   // Conclusion: F*sigma
 529   // sigma maps x1 ... xn to t1 ... tn.
 530   INSTANTIATE,
 531
 532   // ======== Adding Inequalities
 533   // Note: an ArithLiteral is a term of the form (>< poly const)
 534   // where
 535   //   >< is >=, >, ==, <, <=, or not(== ...).
 536   //   poly is a polynomial
 537   //   const is a rational constant
 538
 539   // Children: (P1:l1, ..., Pn:ln)
 540   //           where each li is an ArithLiteral
 541   //           not(= ...) is dis-allowed!
 542   //
 543   // Arguments: (k1, ..., kn), non-zero reals
 544   // ---------------------
 545   // Conclusion: (>< (* k t1) (* k t2))
 546   //    where >< is the fusion of the combination of the ><i, (flipping each it
 547   //    its ki is negative). >< is always one of <, <=
 548   //    NB: this implies that lower bounds must have negative ki,
 549   //                      and upper bounds must have positive ki.
 550   //    t1 is the sum of the polynomials.
 551   //    t2 is the sum of the constants.
 552   ARITH_SCALE_SUM_UPPER_BOUNDS,
 553
 554   // ======== Tightening Strict Integer Upper Bounds
 555   // Children: (P:(< i c))
 556   //         where i has integer type.
 557   // Arguments: none
 558   // ---------------------
 559   // Conclusion: (<= i greatestIntLessThan(c)})
 560   INT_TIGHT_UB,
 561
 562   // ======== Tightening Strict Integer Lower Bounds
 563   // Children: (P:(> i c))
 564   //         where i has integer type.
 565   // Arguments: none
 566   // ---------------------
 567   // Conclusion: (>= i leastIntGreaterThan(c)})
 568   INT_TIGHT_LB,
 569
 570   // ======== Trichotomy of the reals
 571   // Children: (A B)
 572   // Arguments: (C)
 573   // ---------------------
 574   // Conclusion: (C),
 575   //                 where (not A) (not B) and C
 576   //                   are (> x c) (< x c) and (= x c)
 577   //                   in some order
 578   //                 note that "not" here denotes arithmetic negation, flipping
 579   //                 >= to <, etc.
 580   ARITH_TRICHOTOMY,
 581
 582   // ======== Arithmetic operator elimination
 583   // Children: none
 584   // Arguments: (t)
 585   // ---------------------
 586   // Conclusion: arith::OperatorElim::getAxiomFor(t)
 587   ARITH_OP_ELIM_AXIOM,
 588
 589   // ======== Int Trust
 590   // Children: (P1 ... Pn)
 591   // Arguments: (Q)
 592   // ---------------------
 593   // Conclusion: (Q)
 594   INT_TRUST,
 595
 596   //================================================= Unknown rule
 597   UNKNOWN,
 598 };
 599
 600 /**
 601  * Converts a proof rule to a string. Note: This function is also used in
 602  * `safe_print()`. Changing this function name or signature will result in
 603  * `safe_print()` printing "<unsupported>" instead of the proper strings for
 604  * the enum values.
 605  *
 606  * @param id The proof rule
 607  * @return The name of the proof rule
 608  */
 609 const char* toString(PfRule id);
 610
 611 /**
 612  * Writes a proof rule name to a stream.
 613  *
 614  * @param out The stream to write to
 615  * @param id The proof rule to write to the stream
 616  * @return The stream
 617  */
 618 std::ostream& operator<<(std::ostream& out, PfRule id);
 619
 620 }  // namespace CVC4
 621
 622 #endif /* CVC4__EXPR__PROOF_RULE_H */