diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-02 14:32:24 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-02 14:32:24 -0500 |
| commit | f9a4549c3dab3cd91f0d9973b24b7891048ed1d9 (patch) | |
| tree | 245ee9c0d3cf262f6b0ec598978d5b6e51f102b3 /src/theory/rewriter.h | |
| parent | c17f9b25cac7c0d2941ef136466cb750cf4c3e7b (diff) | |
(proof-new) Updates to builtin proof checker (#4962)
This includes support for some trusted rules (whose use is to come). It also modifies THEORY_REWRITE so that it is a "trusted" rule, that is, it is not re-checked. The reason for this is that TheoryRewriter is not deterministic. An example of non-determinism in TheoryRewriter are rules that introduce bound variables (e.g. quantifiers rewriter) since these bound variables are fresh each time it is invoked. Non-deterministic theory rewriters cannot be rechecked, which was leading to failures on proof-new at proof check time. The other way to fix this would be to cache TheoryRewriter responses, but then the checker would only be verifying that the caching was being done properly. This is not worthwhile.
Diffstat (limited to 'src/theory/rewriter.h')
| -rw-r--r-- | src/theory/rewriter.h | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index c57844f23..113749a75 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -80,7 +80,7 @@ class Rewriter { /** * Rewrite with proof production, which is managed by the term conversion * proof generator managed by this class (d_tpg). This method requires a call - * to setProofChecker prior to this call. + * to setProofNodeManager prior to this call. * * @param node The node to rewrite. * @param elimTheoryRewrite Whether we also want fine-grained proofs for @@ -94,8 +94,8 @@ class Rewriter { bool elimTheoryRewrite = false, bool isExtEq = false); - /** Set proof checker */ - void setProofChecker(ProofChecker* pc); + /** Set proof node manager */ + void setProofNodeManager(ProofNodeManager* pnm); /** * Garbage collects the rewrite caches. @@ -189,6 +189,7 @@ class Rewriter { TConvProofGenerator* tcpg = nullptr); /** processes a trust rewrite response */ RewriteResponse processTrustRewriteResponse( + theory::TheoryId theoryId, const TrustRewriteResponse& tresponse, bool isPre, TConvProofGenerator* tcpg); @@ -226,8 +227,6 @@ class Rewriter { RewriteEnvironment d_re; - /** The proof node manager */ - std::unique_ptr<ProofNodeManager> d_pnm; /** The proof generator */ std::unique_ptr<TConvProofGenerator> d_tpg; #ifdef CVC4_ASSERTIONS |