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   // ======== Remove Term Formulas Axiom
 178   // Children: none
 179   // Arguments: (t)
 180   // ---------------------------------------------------------------
 181   // Conclusion: RemoveTermFormulas::getAxiomFor(t).
 182   REMOVE_TERM_FORMULA_AXIOM,
 183
 184   //================================================= Trusted rules
 185   // The rules in this section have the signature of a "trusted rule":
 186   //
 187   // Children: none
 188   // Arguments: (F)
 189   // ---------------------------------------------------------------
 190   // Conclusion: F
 191   //
 192   // where F is an equality of the form t = t' where t was replaced by t'
 193   // based on some preprocessing pass, or otherwise F was added as a new
 194   // assertion by some preprocessing pass.
 195   PREPROCESS,
 196   // where F was added as a new assertion by some preprocessing pass.
 197   PREPROCESS_LEMMA,
 198   // where F is an equality of the form t = Theory::ppRewrite(t) for some
 199   // theory. Notice this is a "trusted" rule.
 200   THEORY_PREPROCESS,
 201   // where F was added as a new assertion by theory preprocessing.
 202   THEORY_PREPROCESS_LEMMA,
 203   // where F is an existential (exists ((x T)) (P x)) used for introducing
 204   // a witness term (witness ((x T)) (P x)).
 205   WITNESS_AXIOM,
 206
 207   //================================================= Boolean rules
 208   // ======== Split
 209   // Children: none
 210   // Arguments: (F)
 211   // ---------------------
 212   // Conclusion: (or F (not F))
 213   SPLIT,
 214   // ======== Equality resolution
 215   // Children: (P1:F1, P2:(= F1 F2))
 216   // Arguments: none
 217   // ---------------------
 218   // Conclusion: (F2)
 219   // Note this can optionally be seen as a macro for EQUIV_ELIM1+RESOLUTION.
 220   EQ_RESOLVE,
 221   // ======== And elimination
 222   // Children: (P:(and F1 ... Fn))
 223   // Arguments: (i)
 224   // ---------------------
 225   // Conclusion: (Fi)
 226   AND_ELIM,
 227   // ======== And introduction
 228   // Children: (P1:F1 ... Pn:Fn))
 229   // Arguments: ()
 230   // ---------------------
 231   // Conclusion: (and P1 ... Pn)
 232   AND_INTRO,
 233   // ======== Not Or elimination
 234   // Children: (P:(not (or F1 ... Fn)))
 235   // Arguments: (i)
 236   // ---------------------
 237   // Conclusion: (not Fi)
 238   NOT_OR_ELIM,
 239   // ======== Implication elimination
 240   // Children: (P:(=> F1 F2))
 241   // Arguments: ()
 242   // ---------------------
 243   // Conclusion: (or (not F1) F2)
 244   IMPLIES_ELIM,
 245   // ======== Not Implication elimination version 1
 246   // Children: (P:(not (=> F1 F2)))
 247   // Arguments: ()
 248   // ---------------------
 249   // Conclusion: (F1)
 250   NOT_IMPLIES_ELIM1,
 251   // ======== Not Implication elimination version 2
 252   // Children: (P:(not (=> F1 F2)))
 253   // Arguments: ()
 254   // ---------------------
 255   // Conclusion: (not F2)
 256   NOT_IMPLIES_ELIM2,
 257   // ======== Equivalence elimination version 1
 258   // Children: (P:(= F1 F2))
 259   // Arguments: ()
 260   // ---------------------
 261   // Conclusion: (or (not F1) F2)
 262   EQUIV_ELIM1,
 263   // ======== Equivalence elimination version 2
 264   // Children: (P:(= F1 F2))
 265   // Arguments: ()
 266   // ---------------------
 267   // Conclusion: (or F1 (not F2))
 268   EQUIV_ELIM2,
 269   // ======== Not Equivalence elimination version 1
 270   // Children: (P:(not (= F1 F2)))
 271   // Arguments: ()
 272   // ---------------------
 273   // Conclusion: (or F1 F2)
 274   NOT_EQUIV_ELIM1,
 275   // ======== Not Equivalence elimination version 2
 276   // Children: (P:(not (= F1 F2)))
 277   // Arguments: ()
 278   // ---------------------
 279   // Conclusion: (or (not F1) (not F2))
 280   NOT_EQUIV_ELIM2,
 281   // ======== XOR elimination version 1
 282   // Children: (P:(xor F1 F2)))
 283   // Arguments: ()
 284   // ---------------------
 285   // Conclusion: (or F1 F2)
 286   XOR_ELIM1,
 287   // ======== XOR elimination version 2
 288   // Children: (P:(xor F1 F2)))
 289   // Arguments: ()
 290   // ---------------------
 291   // Conclusion: (or (not F1) (not F2))
 292   XOR_ELIM2,
 293   // ======== Not XOR elimination version 1
 294   // Children: (P:(not (xor F1 F2)))
 295   // Arguments: ()
 296   // ---------------------
 297   // Conclusion: (or F1 (not F2))
 298   NOT_XOR_ELIM1,
 299   // ======== Not XOR elimination version 2
 300   // Children: (P:(not (xor F1 F2)))
 301   // Arguments: ()
 302   // ---------------------
 303   // Conclusion: (or (not F1) F2)
 304   NOT_XOR_ELIM2,
 305   // ======== ITE elimination version 1
 306   // Children: (P:(ite C F1 F2))
 307   // Arguments: ()
 308   // ---------------------
 309   // Conclusion: (or (not C) F1)
 310   ITE_ELIM1,
 311   // ======== ITE elimination version 2
 312   // Children: (P:(ite C F1 F2))
 313   // Arguments: ()
 314   // ---------------------
 315   // Conclusion: (or C F2)
 316   ITE_ELIM2,
 317   // ======== Not ITE elimination version 1
 318   // Children: (P:(not (ite C F1 F2)))
 319   // Arguments: ()
 320   // ---------------------
 321   // Conclusion: (or (not C) (not F1))
 322   NOT_ITE_ELIM1,
 323   // ======== Not ITE elimination version 1
 324   // Children: (P:(not (ite C F1 F2)))
 325   // Arguments: ()
 326   // ---------------------
 327   // Conclusion: (or C (not F2))
 328   NOT_ITE_ELIM2,
 329   // ======== Not ITE elimination version 1
 330   // Children: (P1:P P2:(not P))
 331   // Arguments: ()
 332   // ---------------------
 333   // Conclusion: (false)
 334   CONTRA,
 335
 336   //================================================= De Morgan rules
 337   // ======== Not And
 338   // Children: (P:(not (and F1 ... Fn))
 339   // Arguments: ()
 340   // ---------------------
 341   // Conclusion: (or (not F1) ... (not Fn))
 342   NOT_AND,
 343   //================================================= CNF rules
 344   // ======== CNF And Pos
 345   // Children: ()
 346   // Arguments: ((and F1 ... Fn), i)
 347   // ---------------------
 348   // Conclusion: (or (not (and F1 ... Fn)) Fi)
 349   CNF_AND_POS,
 350   // ======== CNF And Neg
 351   // Children: ()
 352   // Arguments: ((and F1 ... Fn))
 353   // ---------------------
 354   // Conclusion: (or (and F1 ... Fn) (not F1) ... (not Fn))
 355   CNF_AND_NEG,
 356   // ======== CNF Or Pos
 357   // Children: ()
 358   // Arguments: ((or F1 ... Fn))
 359   // ---------------------
 360   // Conclusion: (or (not (or F1 ... Fn)) F1 ... Fn)
 361   CNF_OR_POS,
 362   // ======== CNF Or Neg
 363   // Children: ()
 364   // Arguments: ((or F1 ... Fn), i)
 365   // ---------------------
 366   // Conclusion: (or (or F1 ... Fn) (not Fi))
 367   CNF_OR_NEG,
 368   // ======== CNF Implies Pos
 369   // Children: ()
 370   // Arguments: ((implies F1 F2))
 371   // ---------------------
 372   // Conclusion: (or (not (implies F1 F2)) (not F1) F2)
 373   CNF_IMPLIES_POS,
 374   // ======== CNF Implies Neg version 1
 375   // Children: ()
 376   // Arguments: ((implies F1 F2))
 377   // ---------------------
 378   // Conclusion: (or (implies F1 F2) F1)
 379   CNF_IMPLIES_NEG1,
 380   // ======== CNF Implies Neg version 2
 381   // Children: ()
 382   // Arguments: ((implies F1 F2))
 383   // ---------------------
 384   // Conclusion: (or (implies F1 F2) (not F2))
 385   CNF_IMPLIES_NEG2,
 386   // ======== CNF Equiv Pos version 1
 387   // Children: ()
 388   // Arguments: ((= F1 F2))
 389   // ---------------------
 390   // Conclusion: (or (not (= F1 F2)) (not F1) F2)
 391   CNF_EQUIV_POS1,
 392   // ======== CNF Equiv Pos version 2
 393   // Children: ()
 394   // Arguments: ((= F1 F2))
 395   // ---------------------
 396   // Conclusion: (or (not (= F1 F2)) F1 (not F2))
 397   CNF_EQUIV_POS2,
 398   // ======== CNF Equiv Neg version 1
 399   // Children: ()
 400   // Arguments: ((= F1 F2))
 401   // ---------------------
 402   // Conclusion: (or (= F1 F2) F1 F2)
 403   CNF_EQUIV_NEG1,
 404   // ======== CNF Equiv Neg version 2
 405   // Children: ()
 406   // Arguments: ((= F1 F2))
 407   // ---------------------
 408   // Conclusion: (or (= F1 F2) (not F1) (not F2))
 409   CNF_EQUIV_NEG2,
 410   // ======== CNF Xor Pos version 1
 411   // Children: ()
 412   // Arguments: ((xor F1 F2))
 413   // ---------------------
 414   // Conclusion: (or (not (xor F1 F2)) F1 F2)
 415   CNF_XOR_POS1,
 416   // ======== CNF Xor Pos version 2
 417   // Children: ()
 418   // Arguments: ((xor F1 F2))
 419   // ---------------------
 420   // Conclusion: (or (not (xor F1 F2)) (not F1) (not F2))
 421   CNF_XOR_POS2,
 422   // ======== CNF Xor Neg version 1
 423   // Children: ()
 424   // Arguments: ((xor F1 F2))
 425   // ---------------------
 426   // Conclusion: (or (xor F1 F2) (not F1) F2)
 427   CNF_XOR_NEG1,
 428   // ======== CNF Xor Neg version 2
 429   // Children: ()
 430   // Arguments: ((xor F1 F2))
 431   // ---------------------
 432   // Conclusion: (or (xor F1 F2) F1 (not F2))
 433   CNF_XOR_NEG2,
 434   // ======== CNF ITE Pos version 1
 435   // Children: ()
 436   // Arguments: ((ite C F1 F2))
 437   // ---------------------
 438   // Conclusion: (or (not (ite C F1 F2)) (not C) F1)
 439   CNF_ITE_POS1,
 440   // ======== CNF ITE Pos version 2
 441   // Children: ()
 442   // Arguments: ((ite C F1 F2))
 443   // ---------------------
 444   // Conclusion: (or (not (ite C F1 F2)) C F2)
 445   CNF_ITE_POS2,
 446   // ======== CNF ITE Pos version 3
 447   // Children: ()
 448   // Arguments: ((ite C F1 F2))
 449   // ---------------------
 450   // Conclusion: (or (not (ite C F1 F2)) F1 F2)
 451   CNF_ITE_POS3,
 452   // ======== CNF ITE Neg version 1
 453   // Children: ()
 454   // Arguments: ((ite C F1 F2))
 455   // ---------------------
 456   // Conclusion: (or (ite C F1 F2) (not C) (not F1))
 457   CNF_ITE_NEG1,
 458   // ======== CNF ITE Neg version 2
 459   // Children: ()
 460   // Arguments: ((ite C F1 F2))
 461   // ---------------------
 462   // Conclusion: (or (ite C F1 F2) C (not F2))
 463   CNF_ITE_NEG2,
 464   // ======== CNF ITE Neg version 3
 465   // Children: ()
 466   // Arguments: ((ite C F1 F2))
 467   // ---------------------
 468   // Conclusion: (or (ite C F1 F2) (not F1) (not F2))
 469   CNF_ITE_NEG3,
 470
 471   //================================================= Equality rules
 472   // ======== Reflexive
 473   // Children: none
 474   // Arguments: (t)
 475   // ---------------------
 476   // Conclusion: (= t t)
 477   REFL,
 478   // ======== Symmetric
 479   // Children: (P:(= t1 t2)) or (P:(not (= t1 t2)))
 480   // Arguments: none
 481   // -----------------------
 482   // Conclusion: (= t2 t1) or (not (= t2 t1))
 483   SYMM,
 484   // ======== Transitivity
 485   // Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn))
 486   // Arguments: none
 487   // -----------------------
 488   // Conclusion: (= t1 tn)
 489   TRANS,
 490   // ======== Congruence
 491   // Children: (P1:(= t1 s1), ..., Pn:(= tn sn))
 492   // Arguments: (<kind> f?)
 493   // ---------------------------------------------
 494   // Conclusion: (= (<kind> f? t1 ... tn) (<kind> f? s1 ... sn))
 495   // Notice that f must be provided iff <kind> is a parameterized kind, e.g.
 496   // APPLY_UF. The actual node for <kind> is constructible via
 497   // ProofRuleChecker::mkKindNode.
 498   CONG,
 499   // ======== True intro
 500   // Children: (P:F)
 501   // Arguments: none
 502   // ----------------------------------------
 503   // Conclusion: (= F true)
 504   TRUE_INTRO,
 505   // ======== True elim
 506   // Children: (P:(= F true)
 507   // Arguments: none
 508   // ----------------------------------------
 509   // Conclusion: F
 510   TRUE_ELIM,
 511   // ======== False intro
 512   // Children: (P:(not F))
 513   // Arguments: none
 514   // ----------------------------------------
 515   // Conclusion: (= F false)
 516   FALSE_INTRO,
 517   // ======== False elim
 518   // Children: (P:(= F false)
 519   // Arguments: none
 520   // ----------------------------------------
 521   // Conclusion: (not F)
 522   FALSE_ELIM,
 523
 524   //================================================= Quantifiers rules
 525   // ======== Witness intro
 526   // Children: (P:F[t])
 527   // Arguments: (t)
 528   // ----------------------------------------
 529   // Conclusion: (= t (witness ((x T)) F[x]))
 530   // where x is a BOUND_VARIABLE unique to the pair F,t.
 531   WITNESS_INTRO,
 532   // ======== Exists intro
 533   // Children: (P:F[t])
 534   // Arguments: (t)
 535   // ----------------------------------------
 536   // Conclusion: (exists ((x T)) F[x])
 537   // where x is a BOUND_VARIABLE unique to the pair F,t.
 538   EXISTS_INTRO,
 539   // ======== Skolemize
 540   // Children: (P:(exists ((x1 T1) ... (xn Tn)) F))
 541   // Arguments: none
 542   // ----------------------------------------
 543   // Conclusion: F*sigma
 544   // sigma maps x1 ... xn to their representative skolems obtained by
 545   // SkolemManager::mkSkolemize, returned in the skolems argument of that
 546   // method.
 547   SKOLEMIZE,
 548   // ======== Instantiate
 549   // Children: (P:(forall ((x1 T1) ... (xn Tn)) F))
 550   // Arguments: (t1 ... tn)
 551   // ----------------------------------------
 552   // Conclusion: F*sigma
 553   // sigma maps x1 ... xn to t1 ... tn.
 554   INSTANTIATE,
 555
 556   //================================================= String rules
 557   //======================== Core solver
 558   // ======== Concat eq
 559   // Children: (P1:(= (str.++ t1 ... tn t) (str.++ t1 ... tn s)))
 560   // Arguments: (b), indicating if reverse direction
 561   // ---------------------
 562   // Conclusion: (= t s)
 563   //
 564   // Notice that t or s may be empty, in which case they are implicit in the
 565   // concatenation above. For example, if
 566   // P1 concludes (= x (str.++ x z)), then
 567   // (CONCAT_EQ P1 :args false) concludes (= "" z)
 568   //
 569   // Also note that constants are split, such that if
 570   // P1 concludes (= (str.++ "abc" x) (str.++ "a" y)), then
 571   // (CONCAT_EQ P1 :args false) concludes (= (str.++ "bc" x) y)
 572   // This splitting is done only for constants such that Word::splitConstant
 573   // returns non-null.
 574   CONCAT_EQ,
 575   // ======== Concat unify
 576   // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
 577   //            P2:(= (str.len t1) (str.len s1)))
 578   // Arguments: (b), indicating if reverse direction
 579   // ---------------------
 580   // Conclusion: (= t1 s1)
 581   CONCAT_UNIFY,
 582   // ======== Concat conflict
 583   // Children: (P1:(= (str.++ c1 t) (str.++ c2 s)))
 584   // Arguments: (b), indicating if reverse direction
 585   // ---------------------
 586   // Conclusion: false
 587   // Where c1, c2 are constants such that Word::splitConstant(c1,c2,index,b)
 588   // is null, in other words, neither is a prefix of the other.
 589   CONCAT_CONFLICT,
 590   // ======== Concat split
 591   // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
 592   //            P2:(not (= (str.len t1) (str.len s1))))
 593   // Arguments: (false)
 594   // ---------------------
 595   // Conclusion: (or (= t1 (str.++ s1 r_t)) (= s1 (str.++ t1 r_s)))
 596   // where
 597   //   r_t = (witness ((z String)) (= z (suf t1 (str.len s1)))),
 598   //   r_s = (witness ((z String)) (= z (suf s1 (str.len t1)))).
 599   //
 600   // or the reverse form of the above:
 601   //
 602   // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
 603   //            P2:(not (= (str.len t2) (str.len s2))))
 604   // Arguments: (true)
 605   // ---------------------
 606   // Conclusion: (or (= t2 (str.++ r_t s2)) (= s2 (str.++ r_s t2)))
 607   // where
 608   //   r_t = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len
 609   //   s2))))), r_s = (witness ((z String)) (= z (pre s2 (- (str.len s2)
 610   //   (str.len t2))))).
 611   //
 612   // Above, (suf x n) is shorthand for (str.substr x n (- (str.len x) n)) and
 613   // (pre x n) is shorthand for (str.substr x 0 n).
 614   CONCAT_SPLIT,
 615   // ======== Concat constant split
 616   // Children: (P1:(= (str.++ t1 t2) (str.++ c s2)),
 617   //            P2:(not (= (str.len t1) 0)))
 618   // Arguments: (false)
 619   // ---------------------
 620   // Conclusion: (= t1 (str.++ c r))
 621   // where
 622   //   r = (witness ((z String)) (= z (suf t1 1))).
 623   //
 624   // or the reverse form of the above:
 625   //
 626   // Children: (P1:(= (str.++ t1 t2) (str.++ s1 c)),
 627   //            P2:(not (= (str.len t2) 0)))
 628   // Arguments: (true)
 629   // ---------------------
 630   // Conclusion: (= t2 (str.++ r c))
 631   // where
 632   //   r = (witness ((z String)) (= z (pre t2 (- (str.len t2) 1)))).
 633   CONCAT_CSPLIT,
 634   // ======== Concat length propagate
 635   // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
 636   //            P2:(> (str.len t1) (str.len s1)))
 637   // Arguments: (false)
 638   // ---------------------
 639   // Conclusion: (= t1 (str.++ s1 r_t))
 640   // where
 641   //   r_t = (witness ((z String)) (= z (suf t1 (str.len s1))))
 642   //
 643   // or the reverse form of the above:
 644   //
 645   // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
 646   //            P2:(> (str.len t2) (str.len s2)))
 647   // Arguments: (false)
 648   // ---------------------
 649   // Conclusion: (= t2 (str.++ r_t s2))
 650   // where
 651   //   r_t = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len
 652   //   s2))))).
 653   CONCAT_LPROP,
 654   // ======== Concat constant propagate
 655   // Children: (P1:(= (str.++ t1 w1 t2) (str.++ w2 s)),
 656   //            P2:(not (= (str.len t1) 0)))
 657   // Arguments: (false)
 658   // ---------------------
 659   // Conclusion: (= t1 (str.++ w3 r))
 660   // where
 661   //   w1, w2, w3, w4 are words,
 662   //   w3 is (pre w2 p),
 663   //   w4 is (suf w2 p),
 664   //   p = Word::overlap((suf w2 1), w1),
 665   //   r = (witness ((z String)) (= z (suf t1 (str.len w3)))).
 666   // In other words, w4 is the largest suffix of (suf w2 1) that can contain a
 667   // prefix of w1; since t1 is non-empty, w3 must therefore be contained in t1.
 668   //
 669   // or the reverse form of the above:
 670   //
 671   // Children: (P1:(= (str.++ t1 w1 t2) (str.++ s w2)),
 672   //            P2:(not (= (str.len t2) 0)))
 673   // Arguments: (true)
 674   // ---------------------
 675   // Conclusion: (= t2 (str.++ r w3))
 676   // where
 677   //   w1, w2, w3, w4 are words,
 678   //   w3 is (suf w2 (- (str.len w2) p)),
 679   //   w4 is (pre w2 (- (str.len w2) p)),
 680   //   p = Word::roverlap((pre w2 (- (str.len w2) 1)), w1),
 681   //   r = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len w3))))).
 682   // In other words, w4 is the largest prefix of (pre w2 (- (str.len w2) 1))
 683   // that can contain a suffix of w1; since t2 is non-empty, w3 must therefore
 684   // be contained in t2.
 685   CONCAT_CPROP,
 686   // ======== String decompose
 687   // Children: (P1: (>= (str.len t) n)
 688   // Arguments: (false)
 689   // ---------------------
 690   // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w1) n))
 691   // or
 692   // Children: (P1: (>= (str.len t) n)
 693   // Arguments: (true)
 694   // ---------------------
 695   // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w2) n))
 696   // where
 697   //   w1 is (witness ((z String)) (= z (pre t n)))
 698   //   w2 is (witness ((z String)) (= z (suf t n)))
 699   STRING_DECOMPOSE,
 700   // ======== Length positive
 701   // Children: none
 702   // Arguments: (t)
 703   // ---------------------
 704   // Conclusion: (or (and (= (str.len t) 0) (= t "")) (> (str.len t 0)))
 705   STRING_LENGTH_POS,
 706   // ======== Length non-empty
 707   // Children: (P1:(not (= t "")))
 708   // Arguments: none
 709   // ---------------------
 710   // Conclusion: (not (= (str.len t) 0))
 711   STRING_LENGTH_NON_EMPTY,
 712   //======================== Extended functions
 713   // ======== Reduction
 714   // Children: none
 715   // Arguments: (t)
 716   // ---------------------
 717   // Conclusion: (and R (= t w))
 718   // where w = strings::StringsPreprocess::reduce(t, R, ...).
 719   // In other words, R is the reduction predicate for extended term t, and w is
 720   //   (witness ((z T)) (= z t))
 721   // Notice that the free variables of R are w and the free variables of t.
 722   STRING_REDUCTION,
 723   // ======== Eager Reduction
 724   // Children: none
 725   // Arguments: (t, id?)
 726   // ---------------------
 727   // Conclusion: R
 728   // where R = strings::TermRegistry::eagerReduce(t, id).
 729   STRING_EAGER_REDUCTION,
 730   //======================== Regular expressions
 731   // ======== Regular expression intersection
 732   // Children: (P:(str.in.re t R1), P:(str.in.re t R2))
 733   // Arguments: none
 734   // ---------------------
 735   // Conclusion: (str.in.re t (re.inter R1 R2)).
 736   RE_INTER,
 737   // ======== Regular expression unfold positive
 738   // Children: (P:(str.in.re t R))
 739   // Arguments: none
 740   // ---------------------
 741   // Conclusion:(RegExpOpr::reduceRegExpPos((str.in.re t R))),
 742   // corresponding to the one-step unfolding of the premise.
 743   RE_UNFOLD_POS,
 744   // ======== Regular expression unfold negative
 745   // Children: (P:(not (str.in.re t R)))
 746   // Arguments: none
 747   // ---------------------
 748   // Conclusion:(RegExpOpr::reduceRegExpNeg((not (str.in.re t R)))),
 749   // corresponding to the one-step unfolding of the premise.
 750   RE_UNFOLD_NEG,
 751   // ======== Regular expression unfold negative concat fixed
 752   // Children: (P:(not (str.in.re t R)))
 753   // Arguments: none
 754   // ---------------------
 755   // Conclusion:(RegExpOpr::reduceRegExpNegConcatFixed((not (str.in.re t
 756   // R)),L,i)) where RegExpOpr::getRegExpConcatFixed((not (str.in.re t R)), i) =
 757   // L. corresponding to the one-step unfolding of the premise, optimized for
 758   // fixed length of component i of the regular expression concatenation R.
 759   RE_UNFOLD_NEG_CONCAT_FIXED,
 760   // ======== Regular expression elimination
 761   // Children: (P:F)
 762   // Arguments: none
 763   // ---------------------
 764   // Conclusion: R
 765   // where R = strings::RegExpElimination::eliminate(F).
 766   RE_ELIM,
 767   //======================== Code points
 768   // Children: none
 769   // Arguments: (t, s)
 770   // ---------------------
 771   // Conclusion:(or (= (str.code t) (- 1))
 772   //                (not (= (str.code t) (str.code s)))
 773   //                (not (= t s)))
 774   STRING_CODE_INJ,
 775   //======================== Sequence unit
 776   // Children: (P:(= (seq.unit x) (seq.unit y)))
 777   // Arguments: none
 778   // ---------------------
 779   // Conclusion:(= x y)
 780   // Also applies to the case where (seq.unit y) is a constant sequence
 781   // of length one.
 782   STRING_SEQ_UNIT_INJ,
 783   // ======== String Trust
 784   // Children: none
 785   // Arguments: (Q)
 786   // ---------------------
 787   // Conclusion: (Q)
 788   STRING_TRUST,
 789
 790   //================================================= Arithmetic rules
 791   // ======== Adding Inequalities
 792   // Note: an ArithLiteral is a term of the form (>< poly const)
 793   // where
 794   //   >< is >=, >, ==, <, <=, or not(== ...).
 795   //   poly is a polynomial
 796   //   const is a rational constant
 797
 798   // Children: (P1:l1, ..., Pn:ln)
 799   //           where each li is an ArithLiteral
 800   //           not(= ...) is dis-allowed!
 801   //
 802   // Arguments: (k1, ..., kn), non-zero reals
 803   // ---------------------
 804   // Conclusion: (>< (* k t1) (* k t2))
 805   //    where >< is the fusion of the combination of the ><i, (flipping each it
 806   //    its ki is negative). >< is always one of <, <=
 807   //    NB: this implies that lower bounds must have negative ki,
 808   //                      and upper bounds must have positive ki.
 809   //    t1 is the sum of the polynomials.
 810   //    t2 is the sum of the constants.
 811   ARITH_SCALE_SUM_UPPER_BOUNDS,
 812
 813   // ======== Tightening Strict Integer Upper Bounds
 814   // Children: (P:(< i c))
 815   //         where i has integer type.
 816   // Arguments: none
 817   // ---------------------
 818   // Conclusion: (<= i greatestIntLessThan(c)})
 819   INT_TIGHT_UB,
 820
 821   // ======== Tightening Strict Integer Lower Bounds
 822   // Children: (P:(> i c))
 823   //         where i has integer type.
 824   // Arguments: none
 825   // ---------------------
 826   // Conclusion: (>= i leastIntGreaterThan(c)})
 827   INT_TIGHT_LB,
 828
 829   // ======== Trichotomy of the reals
 830   // Children: (A B)
 831   // Arguments: (C)
 832   // ---------------------
 833   // Conclusion: (C),
 834   //                 where (not A) (not B) and C
 835   //                   are (> x c) (< x c) and (= x c)
 836   //                   in some order
 837   //                 note that "not" here denotes arithmetic negation, flipping
 838   //                 >= to <, etc.
 839   ARITH_TRICHOTOMY,
 840
 841   // ======== Arithmetic operator elimination
 842   // Children: none
 843   // Arguments: (t)
 844   // ---------------------
 845   // Conclusion: arith::OperatorElim::getAxiomFor(t)
 846   ARITH_OP_ELIM_AXIOM,
 847
 848   // ======== Int Trust
 849   // Children: (P1 ... Pn)
 850   // Arguments: (Q)
 851   // ---------------------
 852   // Conclusion: (Q)
 853   INT_TRUST,
 854
 855   //================================================= Unknown rule
 856   UNKNOWN,
 857 };
 858
 859 /**
 860  * Converts a proof rule to a string. Note: This function is also used in
 861  * `safe_print()`. Changing this function name or signature will result in
 862  * `safe_print()` printing "<unsupported>" instead of the proper strings for
 863  * the enum values.
 864  *
 865  * @param id The proof rule
 866  * @return The name of the proof rule
 867  */
 868 const char* toString(PfRule id);
 869
 870 /**
 871  * Writes a proof rule name to a stream.
 872  *
 873  * @param out The stream to write to
 874  * @param id The proof rule to write to the stream
 875  * @return The stream
 876  */
 877 std::ostream& operator<<(std::ostream& out, PfRule id);
 878
 879 /** Hash function for proof rules */
 880 struct PfRuleHashFunction
 881 {
 882   size_t operator()(PfRule id) const;
 883 }; /* struct PfRuleHashFunction */
 884
 885 }  // namespace CVC4
 886
 887 #endif /* CVC4__EXPR__PROOF_RULE_H */