diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-14 11:30:47 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-14 11:30:47 -0500 |
commit | c6e3264f83df54a886b28c14e2a911c176d89551 (patch) | |
tree | b4f6ca2f4c1cedf6752dbcc90cc1eec1543011df /src/theory/builtin/proof_checker.h | |
parent | c13527bfa6b47ff4675b429b5e7bb7c6f43ff595 (diff) |
(proof-new) Skeleton proof support in the Rewriter (#4730)
This adds support for skeleton proofs in the rewriter (REWRITE -> THEORY_REWRITE).
It adds "extended equality rewrite" as a new method of the rewriter/theory rewriters.
The unit test of this feature should be added on a followup PR.
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Diffstat (limited to 'src/theory/builtin/proof_checker.h')
-rw-r--r-- | src/theory/builtin/proof_checker.h | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index 6dc7023d5..7e46587b7 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -77,6 +77,17 @@ class BuiltinProofRuleChecker : public ProofRuleChecker */ static Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE); /** + * Apply small-step rewrite on n in skolem form (either pre- or + * post-rewrite). This encapsulates the exact behavior of a THEORY_REWRITE + * step in a proof. + * + * @param n The node to rewrite + * @param preRewrite If true, performs a pre-rewrite or a post-rewrite + * otherwise + * @return The rewritten form of n + */ + static Node applyTheoryRewrite(Node n, bool preRewrite); + /** * Get substitution. Updates vars/subs to the substitution specified by * exp (e.g. as an equality) for the substitution method ids. */ |