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 | |
| 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')
| -rw-r--r-- | src/theory/builtin/proof_checker.cpp | 11 | ||||
| -rw-r--r-- | src/theory/builtin/proof_checker.h | 11 |
2 files changed, 22 insertions, 0 deletions
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index a8249ae7c..59f405337 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -59,9 +59,20 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::MACRO_SR_PRED_INTRO, this); pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this); pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this); + pc->registerChecker(PfRule::THEORY_REWRITE, this); pc->registerChecker(PfRule::PREPROCESS, this); } +Node BuiltinProofRuleChecker::applyTheoryRewrite(Node n, bool preRewrite) +{ + TheoryId tid = Theory::theoryOf(n); + Rewriter* rewriter = Rewriter::getInstance(); + Node nkr = preRewrite ? rewriter->preRewrite(tid, n).d_node + : rewriter->postRewrite(tid, n).d_node; + return nkr; +} + + Node BuiltinProofRuleChecker::applySubstitutionRewrite( Node n, const std::vector<Node>& exp, MethodId ids, MethodId idr) { 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. */ |