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/builtin/proof_checker.cpp | |
| 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/builtin/proof_checker.cpp')
| -rw-r--r-- | src/theory/builtin/proof_checker.cpp | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 73d39f417..4e2e78bae 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -34,6 +34,8 @@ const char* toString(MethodId id) case MethodId::RW_REWRITE_EQ_EXT: return "RW_REWRITE_EQ_EXT"; case MethodId::RW_EVALUATE: return "RW_EVALUATE"; case MethodId::RW_IDENTITY: return "RW_IDENTITY"; + case MethodId::RW_REWRITE_THEORY_PRE: return "RW_REWRITE_THEORY_PRE"; + case MethodId::RW_REWRITE_THEORY_POST: return "RW_REWRITE_THEORY_POST"; case MethodId::SB_DEFAULT: return "SB_DEFAULT"; case MethodId::SB_LITERAL: return "SB_LITERAL"; case MethodId::SB_FORMULA: return "SB_FORMULA"; @@ -76,7 +78,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 3); pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1); pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1); - pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1); + pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 3); } Node BuiltinProofRuleChecker::applySubstitutionRewrite( @@ -282,6 +284,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, exp.push_back(children[i]); } Node res = applySubstitution(args[0], exp, ids); + if (res.isNull()) + { + return Node::null(); + } return args[0].eqNode(res); } else if (id == PfRule::REWRITE) @@ -294,6 +300,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, return Node::null(); } Node res = applyRewrite(args[0], idr); + if (res.isNull()) + { + return Node::null(); + } return args[0].eqNode(res); } else if (id == PfRule::EVALUATE) @@ -301,6 +311,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, Assert(children.empty()); Assert(args.size() == 1); Node res = applyRewrite(args[0], MethodId::RW_EVALUATE); + if (res.isNull()) + { + return Node::null(); + } return args[0].eqNode(res); } else if (id == PfRule::MACRO_SR_EQ_INTRO) @@ -312,6 +326,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, return Node::null(); } Node res = applySubstitutionRewrite(args[0], children, ids, idr); + if (res.isNull()) + { + return Node::null(); + } return args[0].eqNode(res); } else if (id == PfRule::MACRO_SR_PRED_INTRO) |