diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-20 19:12:07 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-20 19:12:07 -0500 |
| commit | 6940f336d9c63c4844438d6921a38f2c561a4195 (patch) | |
| tree | 57ce7cf87d4e5540e9c138606bea54482e51ff38 /src/expr | |
| parent | 020565a54621169437a237b0d14478f0c44936a0 (diff) | |
(proof-new) Fixes for proofs in rewriter (#5307)
This PR fixes proofs in the rewriter so that we use attributes for marking whether a node has been rewritten with proofs instead of consulting the provided TConvProofGenerator for hasRewriteStep. This additionally marks TRUST_REWRITE steps if a rewriter happens to be nondeterministic (e.g. quantifiers). It furthermore decouples rewriteWithProof from reconstruction for theory rewrite steps.
The proof postprocessor is additionally updated so that extended equality REWRITE steps are converted to THEORY_REWRITE steps with identifier RW_REWRITE_EQ_EXT for consistency, since eliminating REWRITE should result in THEORY_REWRITE only. This required generalizing the argument to THEORY_REWRITE to be a MethodId instead of a Boolean.
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/proof_rule.h | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index e24d5c522..2b5565318 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -201,16 +201,17 @@ enum class PfRule : uint32_t THEORY_LEMMA, // ======== Theory Rewrite // Children: none - // Arguments: (F, tid, preRewrite?) + // Arguments: (F, tid, rid) // ---------------------------------------- // Conclusion: F // where F is an equality of the form (= t t') where t' is obtained by - // applying the theory rewriter with identifier tid in either its prewrite - // (when preRewrite is true) or postrewrite method. Notice that the checker - // for this rule does not replay the rewrite to ensure correctness, since - // theory rewriter methods are not static. For example, the quantifiers - // rewriter involves constructing new bound variables that are not guaranteed - // to be consistent on each call. + // applying the kind of rewriting given by the method identifier rid, which + // is one of: + // { RW_REWRITE_THEORY_PRE, RW_REWRITE_THEORY_POST, RW_REWRITE_EQ_EXT } + // Notice that the checker for this rule does not replay the rewrite to ensure + // correctness, since theory rewriter methods are not static. For example, + // the quantifiers rewriter involves constructing new bound variables that are + // not guaranteed to be consistent on each call. THEORY_REWRITE, // The rules in this section have the signature of a "trusted rule": // |