-/********************* */
-/*! \file proof_rule.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Andrew Reynolds, Haniel Barbosa, Gereon Kremer
- ** This file is part of the CVC4 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.\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>
// 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:
// 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(toOriginal(F')) == Rewriter::rewrite(toOriginal(G'))
// 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
// 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)
// 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 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)
- 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)
// 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
} // namespace cvc5
-#endif /* CVC4__EXPR__PROOF_RULE_H */
+#endif /* CVC5__EXPR__PROOF_RULE_H */
projects / cvc5.git / blobdiff