diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-15 17:09:40 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-15 17:09:40 -0500 |
commit | 912b65006615fe4074cde54b080f48e3d6c12042 (patch) | |
tree | 99b1d0ad565ac79d7ebaaa305a42d5052d06b206 /src/expr/proof_rule.h | |
parent | eacb636406e609299b6e5b64e93f1cf5b73f4ba3 (diff) |
Add ProofNode data structure (#4311)
This is the core data structure for proofs in the new proofs infrastructure. PfRule is a global enumeration of ids of proof nodes (analogous to Kind for Nodes).
Diffstat (limited to 'src/expr/proof_rule.h')
-rw-r--r-- | src/expr/proof_rule.h | 78 |
1 files changed, 78 insertions, 0 deletions
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h new file mode 100644 index 000000000..16f4ca971 --- /dev/null +++ b/src/expr/proof_rule.h @@ -0,0 +1,78 @@ +/********************* */ +/*! \file proof_rule.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__PROOF_RULE_H +#define CVC4__EXPR__PROOF_RULE_H + +#include <iosfwd> + +namespace CVC4 { + +/** + * An enumeration for proof rules. This enumeration is analogous to Kind for + * Node objects. In the documentation below, P:F denotes a ProofNode that + * proves formula F. + * + * Conceptually, the following proof rules form a calculus whose target + * user is the Node-level theory solvers. This means that the rules below + * are designed to reason about, among other things, common operations on Node + * objects like Rewriter::rewrite or Node::substitute. It is intended to be + * translated or printed in other formats. + * + * The following PfRule values include core rules and those categorized by + * theory, including the theory of equality. + * + * The "core rules" include ASSUME, which represents an open leaf in a proof. + * The core rules additionally correspond to generic operations that are done + * internally on nodes, e.g. calling Rewriter::rewrite. + */ +enum class PfRule : uint32_t +{ + //================================================= Core rules + // ======== Assumption (a leaf) + // Children: none + // Arguments: (F) + // -------------- + // Conclusion F + ASSUME, + + //================================================= Unknown rule + UNKNOWN, +}; + +/** + * Converts a proof rule to a string. Note: This function is also used in + * `safe_print()`. Changing this function name or signature will result in + * `safe_print()` printing "<unsupported>" instead of the proper strings for + * the enum values. + * + * @param id The proof rule + * @return The name of the proof rule + */ +const char* toString(PfRule id); + +/** + * Writes a proof rule name to a stream. + * + * @param out The stream to write to + * @param id The proof rule to write to the stream + * @return The stream + */ +std::ostream& operator<<(std::ostream& out, PfRule id); + +} // namespace CVC4 + +#endif /* CVC4__EXPR__PROOF_RULE_H */ |