-/********************* */
-/*! \file proof_rule.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Haniel Barbosa, Alex Ozdemir
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Proof rule enumeration
- **/
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds, Haniel Barbosa, Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Proof rule enumeration.
+ */
-#include "cvc4_private.h"
+#include "cvc5_private.h"
-#ifndef CVC4__EXPR__PROOF_RULE_H
-#define CVC4__EXPR__PROOF_RULE_H
+#ifndef CVC5__EXPR__PROOF_RULE_H
+#define CVC5__EXPR__PROOF_RULE_H
#include <iosfwd>
-namespace CVC4 {
+namespace cvc5 {
/**
* An enumeration for proof rules. This enumeration is analogous to Kind for
// rewritten form under a (proven) substitution.
//
// Children: (P1:F1, ..., Pn:Fn)
- // Arguments: (t, (ids (idr)?)?)
+ // Arguments: (t, (ids (ida (idr)?)?)?)
// ---------------------------------------------------------------
// Conclusion: (= t t')
// where
// t' is
- // Rewriter{idr}(t*sigma{ids}(Fn)*...*sigma{ids}(F1))
+ // Rewriter{idr}(t*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1))
//
// In other words, from the point of view of Skolem forms, this rule
// transforms t to t' by standard substitution + rewriting.
//
- // The argument ids and idr is optional and specify the identifier of the
- // substitution and rewriter respectively to be used. For details, see
- // theory/builtin/proof_checker.h.
+ // The arguments ids, ida and idr are optional and specify the identifier of
+ // the substitution, the substitution application and rewriter respectively to
+ // be used. For details, see theory/builtin/proof_checker.h.
MACRO_SR_EQ_INTRO,
// ======== Substitution + Rewriting predicate introduction
//
// that it rewrites to true under a proven substitution.
//
// Children: (P1:F1, ..., Pn:Fn)
- // Arguments: (F, (ids (idr)?)?)
+ // Arguments: (F, (ids (ida (idr)?)?)?)
// ---------------------------------------------------------------
// Conclusion: F
// where
- // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true
+ // Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)) == true
// where ids and idr are method identifiers.
//
// More generally, this rule also holds when:
- // Rewriter::rewrite(toWitness(F')) == true
+ // Rewriter::rewrite(toOriginal(F')) == true
// where F' is the result of the left hand side of the equality above. Here,
- // notice that we apply rewriting on the witness form of F', meaning that this
- // rule may conclude an F whose Skolem form is justified by the definition of
- // its (fresh) Skolem variables. For example, this rule may justify the
- // conclusion (= k t) where k is the purification Skolem for t, whose
- // witness form is (witness ((x T)) (= x t)).
+ // notice that we apply rewriting on the original form of F', meaning that
+ // this rule may conclude an F whose Skolem form is justified by the
+ // definition of its (fresh) Skolem variables. For example, this rule may
+ // justify the conclusion (= k t) where k is the purification Skolem for t,
+ // e.g. where the original form of k is t.
//
// Furthermore, notice that the rewriting and substitution is applied only
- // within the side condition, meaning the rewritten form of the witness form
+ // within the side condition, meaning the rewritten form of the original form
// of F does not escape this rule.
MACRO_SR_PRED_INTRO,
// ======== Substitution + Rewriting predicate elimination
// rewritten form under a proven substitution.
//
// Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
- // Arguments: ((ids (idr)?)?)
+ // Arguments: ((ids (ida (idr)?)?)?)
// ----------------------------------------
// Conclusion: F'
// where
// F' is
- // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)).
+ // Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)).
// where ids and idr are method identifiers.
//
// We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
// substitution.
//
// Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
- // Arguments: (G, (ids (idr)?)?)
+ // Arguments: (G, (ids (ida (idr)?)?)?)
// ----------------------------------------
// Conclusion: G
// where
- // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) ==
- // Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1))
+ // Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)) ==
+ // Rewriter{idr}(G*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1))
//
// More generally, this rule also holds when:
- // Rewriter::rewrite(toWitness(F')) == Rewriter::rewrite(toWitness(G'))
+ // Rewriter::rewrite(toOriginal(F')) == Rewriter::rewrite(toOriginal(G'))
// where F' and G' are the result of each side of the equation above. Here,
- // witness forms are used in a similar manner to MACRO_SR_PRED_INTRO above.
+ // original forms are used in a similar manner to MACRO_SR_PRED_INTRO above.
MACRO_SR_PRED_TRANSFORM,
//================================================= Processing rules
// where F is an equality (= t t') that holds by a form of substitution that
// could not be determined by the TrustSubstitutionMap.
TRUST_SUBS_MAP,
+ // ========= SAT Refutation for assumption-based unsat cores
+ // Children: (P1, ..., Pn)
+ // Arguments: none
+ // ---------------------
+ // Conclusion: false
+ // Note: P1, ..., Pn correspond to the unsat core determined by the SAT
+ // solver.
+ SAT_REFUTATION,
//================================================= Boolean rules
// ======== Resolution
// ---------------------
// Conclusion: C2
// where
- // Set representations of C1 and C2 is the same but the number of literals in
- // C2 is the same of that of C1
+ // Set representations of C1 and C2 are the same and the number of literals
+ // in C2 is the same of that of C1
REORDERING,
// ======== N-ary Resolution + Factoring + Reordering
// Children: (P1:C_1, ..., Pm:C_n)
// The result of the chain resolution is C, which is equal, in its set
// representation, to C_n'
MACRO_RESOLUTION,
+ // As above but not checked
+ MACRO_RESOLUTION_TRUST,
// ======== Split
// Children: none
ARRAYS_TRUST,
//================================================= Bit-Vector rules
+ // Note: bitblast() represents the result of the bit-blasted term as a
+ // bit-vector consisting of the output bits of the bit-blasted circuit
+ // representation of the term. Terms are bit-blasted according to the
+ // strategies defined in
+ // theory/bv/bitblast/bitblast_strategies_template.h.
// ======== Bitblast
// Children: none
// Arguments: (t)
// ---------------------
// Conclusion: (= t bitblast(t))
BV_BITBLAST,
+ // ======== Bitblast Bit-Vector Constant
+ // Children: none
+ // Arguments: (= t bitblast(t))
+ // ---------------------
+ // Conclusion: (= t bitblast(t))
+ BV_BITBLAST_CONST,
+ // ======== Bitblast Bit-Vector Variable
+ // Children: none
+ // Arguments: (= t bitblast(t))
+ // ---------------------
+ // Conclusion: (= t bitblast(t))
+ BV_BITBLAST_VAR,
+ // ======== Bitblast Bit-Vector Terms
+ // TODO cvc4-projects issue #275
+ // Children: none
+ // Arguments: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t))
+ // ---------------------
+ // Conclusion: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t))
+ BV_BITBLAST_EQUAL,
+ BV_BITBLAST_ULT,
+ BV_BITBLAST_ULE,
+ BV_BITBLAST_UGT,
+ BV_BITBLAST_UGE,
+ BV_BITBLAST_SLT,
+ BV_BITBLAST_SLE,
+ BV_BITBLAST_SGT,
+ BV_BITBLAST_SGE,
+ BV_BITBLAST_NOT,
+ BV_BITBLAST_CONCAT,
+ BV_BITBLAST_AND,
+ BV_BITBLAST_OR,
+ BV_BITBLAST_XOR,
+ BV_BITBLAST_XNOR,
+ BV_BITBLAST_NAND,
+ BV_BITBLAST_NOR,
+ BV_BITBLAST_COMP,
+ BV_BITBLAST_MULT,
+ BV_BITBLAST_PLUS,
+ BV_BITBLAST_SUB,
+ BV_BITBLAST_NEG,
+ BV_BITBLAST_UDIV,
+ BV_BITBLAST_UREM,
+ BV_BITBLAST_SDIV,
+ BV_BITBLAST_SREM,
+ BV_BITBLAST_SMOD,
+ BV_BITBLAST_SHL,
+ BV_BITBLAST_LSHR,
+ BV_BITBLAST_ASHR,
+ BV_BITBLAST_ULTBV,
+ BV_BITBLAST_SLTBV,
+ BV_BITBLAST_ITE,
+ BV_BITBLAST_EXTRACT,
+ BV_BITBLAST_REPEAT,
+ BV_BITBLAST_ZERO_EXTEND,
+ BV_BITBLAST_SIGN_EXTEND,
+ BV_BITBLAST_ROTATE_RIGHT,
+ BV_BITBLAST_ROTATE_LEFT,
// ======== Eager Atom
// Children: none
// Arguments: (F)
DT_TRUST,
//================================================= Quantifiers rules
- // ======== Witness intro
- // Children: (P:(exists ((x T)) F[x]))
- // Arguments: none
+ // ======== Skolem intro
+ // Children: none
+ // Arguments: (k)
// ----------------------------------------
- // Conclusion: (= k (witness ((x T)) F[x]))
- // where k is the Skolem form of (witness ((x T)) F[x]).
- WITNESS_INTRO,
+ // Conclusion: (= k t)
+ // where t is the original form of skolem k.
+ SKOLEM_INTRO,
// ======== Exists intro
// Children: (P:F[t])
// Arguments: ((exists ((x T)) F[x]))
// Conclusion: F*sigma
// sigma maps x1 ... xn to their representative skolems obtained by
// SkolemManager::mkSkolemize, returned in the skolems argument of that
- // method. Alternatively, can use negated forall as a premise.
+ // method. Alternatively, can use negated forall as a premise. The witness
+ // terms for the returned skolems can be obtained by
+ // SkolemManager::getWitnessForm.
SKOLEMIZE,
// ======== Instantiate
// Children: (P:(forall ((x1 T1) ... (xn Tn)) F))
//
// Arguments: (k1, ..., kn), non-zero reals
// ---------------------
- // Conclusion: (>< (* k t1) (* k t2))
+ // Conclusion: (>< t1 t2)
// where >< is the fusion of the combination of the ><i, (flipping each it
// its ki is negative). >< is always one of <, <=
// NB: this implies that lower bounds must have negative ki,
// and upper bounds must have positive ki.
- // t1 is the sum of the polynomials.
- // t2 is the sum of the constants.
- ARITH_SCALE_SUM_UPPER_BOUNDS,
-
+ // t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n *
+ // poly_n) t2 is the sum of the scaled constants (k_1 * const_1 + ... + k_n
+ // * const_n)
+ MACRO_ARITH_SCALE_SUM_UB,
+ // ======== Sum Upper Bounds
+ // Children: (P1, ... , Pn)
+ // where each Pi has form (><i, Li, Ri)
+ // for ><i in {<, <=, ==}
+ // Conclusion: (>< L R)
+ // where >< is < if any ><i is <, and <= otherwise.
+ // L is (+ L1 ... Ln)
+ // R is (+ R1 ... Rn)
+ ARITH_SUM_UB,
// ======== Tightening Strict Integer Upper Bounds
// Children: (P:(< i c))
// where i has integer type.
// Conclusion: (Q)
INT_TRUST,
+ //======== Multiplication sign inference
+ // Children: none
+ // Arguments: (f1, ..., fk, m)
+ // ---------------------
+ // Conclusion: (=> (and f1 ... fk) (~ m 0))
+ // Where f1, ..., fk are variables compared to zero (less, greater or not
+ // equal), m is a monomial from these variables, and ~ is the comparison (less
+ // or greater) that results from the signs of the variables. All variables
+ // with even exponent in m should be given as not equal to zero while all
+ // variables with odd exponent in m should be given as less or greater than
+ // zero.
+ ARITH_MULT_SIGN,
+ //======== Multiplication with positive factor
+ // Children: none
+ // Arguments: (m, (rel lhs rhs))
+ // ---------------------
+ // Conclusion: (=> (and (> m 0) (rel lhs rhs)) (rel (* m lhs) (* m rhs)))
+ // Where rel is a relation symbol.
+ ARITH_MULT_POS,
+ //======== Multiplication with negative factor
+ // Children: none
+ // Arguments: (m, (rel lhs rhs))
+ // ---------------------
+ // Conclusion: (=> (and (< m 0) (rel lhs rhs)) (rel_inv (* m lhs) (* m rhs)))
+ // Where rel is a relation symbol and rel_inv the inverted relation symbol.
+ ARITH_MULT_NEG,
//======== Multiplication tangent plane
// Children: none
// Arguments: (t, x, y, a, b, sgn)
// ---------------------
// Conclusion:
- // sgn=-1: (= (<= t tplane) (or (and (<= x a) (>= y b)) (and (>= x a) (<= y b)))
- // sgn= 1: (= (>= t tplane) (or (and (<= x a) (<= y b)) (and (>= x a) (>= y b)))
+ // sgn=-1: (= (<= t tplane) (or (and (<= x a) (>= y b)) (and (>= x a) (<= y
+ // b))) sgn= 1: (= (>= t tplane) (or (and (<= x a) (<= y b)) (and (>= x a)
+ // (>= y b)))
// Where x,y are real terms (variables or extended terms), t = (* x y)
// (possibly under rewriting), a,b are real constants, and sgn is either -1
// or 1. tplane is the tangent plane of x*y at (a,b): b*x + a*y - a*b
// Conclusion: (and (>= real.pi l) (<= real.pi u))
// Where l (u) is a valid lower (upper) bound on pi.
ARITH_TRANS_PI,
+
+ //======== Exp at negative values
+ // Children: none
+ // Arguments: (t)
+ // ---------------------
+ // Conclusion: (= (< t 0) (< (exp t) 1))
+ ARITH_TRANS_EXP_NEG,
+ //======== Exp is always positive
+ // Children: none
+ // Arguments: (t)
+ // ---------------------
+ // Conclusion: (> (exp t) 0)
+ ARITH_TRANS_EXP_POSITIVITY,
+ //======== Exp grows super-linearly for positive values
+ // Children: none
+ // Arguments: (t)
+ // ---------------------
+ // Conclusion: (or (<= t 0) (> exp(t) (+ t 1)))
+ ARITH_TRANS_EXP_SUPER_LIN,
+ //======== Exp at zero
+ // Children: none
+ // Arguments: (t)
+ // ---------------------
+ // Conclusion: (= (= t 0) (= (exp t) 1))
+ ARITH_TRANS_EXP_ZERO,
+ //======== Exp is approximated from above for negative values
+ // Children: none
+ // Arguments: (d, t, l, u)
+ // ---------------------
+ // Conclusion: (=> (and (>= t l) (<= t u)) (<= (exp t) (secant exp l u t))
+ // Where d is an even positive number, t an arithmetic term and l (u) a lower
+ // (upper) bound on t. Let p be the d'th taylor polynomial at zero (also
+ // called the Maclaurin series) of the exponential function. (secant exp l u
+ // t) denotes the secant of p from (l, exp(l)) to (u, exp(u)) evaluated at t,
+ // calculated as follows:
+ // (p(l) - p(u)) / (l - u) * (t - l) + p(l)
+ // The lemma states that if t is between l and u, then (exp t) is below the
+ // secant of p from l to u.
+ ARITH_TRANS_EXP_APPROX_ABOVE_NEG,
+ //======== Exp is approximated from above for positive values
+ // Children: none
+ // Arguments: (d, t, l, u)
+ // ---------------------
+ // Conclusion: (=> (and (>= t l) (<= t u)) (<= (exp t) (secant-pos exp l u t))
+ // Where d is an even positive number, t an arithmetic term and l (u) a lower
+ // (upper) bound on t. Let p* be a modification of the d'th taylor polynomial
+ // at zero (also called the Maclaurin series) of the exponential function as
+ // follows where p(d-1) is the regular Maclaurin series of degree d-1:
+ // p* = p(d-1) * (1 + t^n / n!)
+ // (secant-pos exp l u t) denotes the secant of p from (l, exp(l)) to (u,
+ // exp(u)) evaluated at t, calculated as follows:
+ // (p(l) - p(u)) / (l - u) * (t - l) + p(l)
+ // The lemma states that if t is between l and u, then (exp t) is below the
+ // secant of p from l to u.
+ ARITH_TRANS_EXP_APPROX_ABOVE_POS,
+ //======== Exp is approximated from below
+ // Children: none
+ // Arguments: (d, t)
+ // ---------------------
+ // Conclusion: (>= (exp t) (maclaurin exp d t))
+ // Where d is an odd positive number and (maclaurin exp d t) is the d'th
+ // taylor polynomial at zero (also called the Maclaurin series) of the
+ // exponential function evaluated at t. The Maclaurin series for the
+ // exponential function is the following:
+ // e^x = \sum_{n=0}^{\infty} x^n / n!
+ ARITH_TRANS_EXP_APPROX_BELOW,
+
+ //======== Sine is always between -1 and 1
+ // Children: none
+ // Arguments: (t)
+ // ---------------------
+ // Conclusion: (and (<= (sin t) 1) (>= (sin t) (- 1)))
+ ARITH_TRANS_SINE_BOUNDS,
//======== Sine arg shifted to -pi..pi
// Children: none
// Arguments: (x, y, s)
// into -pi..pi and s is a new integer skolem that is the number of phases y
// is shifted.
ARITH_TRANS_SINE_SHIFT,
+ //======== Sine is symmetric with respect to negation of the argument
+ // Children: none
+ // Arguments: (t)
+ // ---------------------
+ // Conclusion: (= (- (sin t) (sin (- t))) 0)
+ ARITH_TRANS_SINE_SYMMETRY,
+ //======== Sine is bounded by the tangent at zero
+ // Children: none
+ // Arguments: (t)
+ // ---------------------
+ // Conclusion: (and
+ // (=> (> t 0) (< (sin t) t))
+ // (=> (< t 0) (> (sin t) t))
+ // )
+ ARITH_TRANS_SINE_TANGENT_ZERO,
+ //======== Sine is bounded by the tangents at -pi and pi
+ // Children: none
+ // Arguments: (t)
+ // ---------------------
+ // Conclusion: (and
+ // (=> (> t -pi) (> (sin t) (- -pi t)))
+ // (=> (< t pi) (< (sin t) (- pi t)))
+ // )
+ ARITH_TRANS_SINE_TANGENT_PI,
+ //======== Sine is approximated from above for negative values
+ // Children: none
+ // Arguments: (d, t, lb, ub, l, u)
+ // ---------------------
+ // Conclusion: (=> (and (>= t lb) (<= t ub)) (<= (sin t) (secant sin l u t))
+ // Where d is an even positive number, t an arithmetic term, lb (ub) a
+ // symbolic lower (upper) bound on t (possibly containing pi) and l (u) the
+ // evaluated lower (upper) bound on t. Let p be the d'th taylor polynomial at
+ // zero (also called the Maclaurin series) of the sine function. (secant sin l
+ // u t) denotes the secant of p from (l, sin(l)) to (u, sin(u)) evaluated at
+ // t, calculated as follows:
+ // (p(l) - p(u)) / (l - u) * (t - l) + p(l)
+ // The lemma states that if t is between l and u, then (sin t) is below the
+ // secant of p from l to u.
+ ARITH_TRANS_SINE_APPROX_ABOVE_NEG,
+ //======== Sine is approximated from above for positive values
+ // Children: none
+ // Arguments: (d, t, c, lb, ub)
+ // ---------------------
+ // Conclusion: (=> (and (>= t lb) (<= t ub)) (<= (sin t) (upper sin c))
+ // Where d is an even positive number, t an arithmetic term, c an arithmetic
+ // constant, and lb (ub) a symbolic lower (upper) bound on t (possibly
+ // containing pi). Let p be the d'th taylor polynomial at zero (also called
+ // the Maclaurin series) of the sine function. (upper sin c) denotes the upper
+ // bound on sin(c) given by p and lb,ub are such that sin(t) is the maximum of
+ // the sine function on (lb,ub).
+ ARITH_TRANS_SINE_APPROX_ABOVE_POS,
+ //======== Sine is approximated from below for negative values
+ // Children: none
+ // Arguments: (d, t, c, lb, ub)
+ // ---------------------
+ // Conclusion: (=> (and (>= t lb) (<= t ub)) (>= (sin t) (lower sin c))
+ // Where d is an even positive number, t an arithmetic term, c an arithmetic
+ // constant, and lb (ub) a symbolic lower (upper) bound on t (possibly
+ // containing pi). Let p be the d'th taylor polynomial at zero (also called
+ // the Maclaurin series) of the sine function. (lower sin c) denotes the lower
+ // bound on sin(c) given by p and lb,ub are such that sin(t) is the minimum of
+ // the sine function on (lb,ub).
+ ARITH_TRANS_SINE_APPROX_BELOW_NEG,
+ //======== Sine is approximated from below for positive values
+ // Children: none
+ // Arguments: (d, t, lb, ub, l, u)
+ // ---------------------
+ // Conclusion: (=> (and (>= t lb) (<= t ub)) (>= (sin t) (secant sin l u t))
+ // Where d is an even positive number, t an arithmetic term, lb (ub) a
+ // symbolic lower (upper) bound on t (possibly containing pi) and l (u) the
+ // evaluated lower (upper) bound on t. Let p be the d'th taylor polynomial at
+ // zero (also called the Maclaurin series) of the sine function. (secant sin l
+ // u t) denotes the secant of p from (l, sin(l)) to (u, sin(u)) evaluated at
+ // t, calculated as follows:
+ // (p(l) - p(u)) / (l - u) * (t - l) + p(l)
+ // The lemma states that if t is between l and u, then (sin t) is above the
+ // secant of p from l to u.
+ ARITH_TRANS_SINE_APPROX_BELOW_POS,
+
+ // ================ CAD Lemmas
+ // We use IRP for IndexedRootPredicate.
+ //
+ // A formula "Interval" describes that a variable (xn is none is given) is
+ // within a particular interval whose bounds are given as IRPs. It is either
+ // an open interval or a point interval:
+ // (IRP k poly) < xn < (IRP k poly)
+ // xn == (IRP k poly)
+ //
+ // A formula "Cell" describes a portion
+ // of the real space in the following form:
+ // Interval(x1) and Interval(x2) and ...
+ // We implicitly assume a Cell to go up to n-1 (and can be empty).
+ //
+ // A formula "Covering" is a set of Intervals, implying that xn can be in
+ // neither of these intervals. To be a covering (of the real line), the union
+ // of these intervals should be the real numbers.
+ // ======== CAD direct conflict
+ // Children (Cell, A)
+ // ---------------------
+ // Conclusion: (false)
+ // A direct interval is generated from an assumption A (in variables x1...xn)
+ // over a Cell (in variables x1...xn). It derives that A evaluates to false
+ // over the Cell. In the actual algorithm, it means that xn can not be in the
+ // topmost interval of the Cell.
+ ARITH_NL_CAD_DIRECT,
+ // ======== CAD recursive interval
+ // Children (Cell, Covering)
+ // ---------------------
+ // Conclusion: (false)
+ // A recursive interval is generated from a Covering (for xn) over a Cell
+ // (in variables x1...xn-1). It generates the conclusion that no xn exists
+ // that extends the Cell and satisfies all assumptions.
+ ARITH_NL_CAD_RECURSIVE,
//================================================= Unknown rule
UNKNOWN,
size_t operator()(PfRule id) const;
}; /* struct PfRuleHashFunction */
-} // namespace CVC4
+} // namespace cvc5
-#endif /* CVC4__EXPR__PROOF_RULE_H */
+#endif /* CVC5__EXPR__PROOF_RULE_H */
projects / cvc5.git / blobdiff