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/theory/rewriter.h | |
| 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/theory/rewriter.h')
| -rw-r--r-- | src/theory/rewriter.h | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index f38f3b174..e36426a81 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -83,15 +83,12 @@ class Rewriter { * to setProofNodeManager prior to this call. * * @param node The node to rewrite. - * @param elimTheoryRewrite Whether we also want fine-grained proofs for - * THEORY_REWRITE steps. * @param isExtEq Whether node is an equality which we are applying * rewriteEqualityExt on. * @return The trust node of kind TrustNodeKind::REWRITE that contains the * rewritten form of node. */ TrustNode rewriteWithProof(TNode node, - bool elimTheoryRewrite = false, bool isExtEq = false); /** Set proof node manager */ |