diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-29 13:27:44 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-29 13:27:44 -0600 |
| commit | ce1b2f2fb06150599c231bf0d59b52a07e74c3f5 (patch) | |
| tree | 53fee982175e433e70ca5abe60a81b763c42f81f /src/smt/proof_post_processor.cpp | |
| parent | 145b99d771e182fba70402398702ed12e3303682 (diff) | |
(proof-new) Distinguish pre vs post rewrites in term conversion proof generator (#5833)
This is work towards resolving two kinds of failures on proof-new:
(1) Functional issues with proofs from the rewriter, in particular when a term pre-rewrites and post-rewrites to different things,
(2) Conversion issues in theory-preprocessing, where all steps are assumed to be post-rewrites but some are in fact pre-rewrites. This leads to the term conversion proof generator proving something different than what is expected.
A followup PR will simplify and fix proofs for theory-preprocessing.
Diffstat (limited to 'src/smt/proof_post_processor.cpp')
| -rw-r--r-- | src/smt/proof_post_processor.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index a620a4d22..a57a6d920 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -806,7 +806,8 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // add previous rewrite steps for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++) { - tcg.addRewriteStep(vvec[j], svec[j], pgs[j]); + // substitutions are pre-rewrites + tcg.addRewriteStep(vvec[j], svec[j], pgs[j], true); } // get the proof for the update to the current substitution Node seqss = subs.eqNode(ss); @@ -851,7 +852,8 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, true); for (unsigned j = 0, nvars = vvec.size(); j < nvars; j++) { - tcpg.addRewriteStep(vvec[j], svec[j], pgs[j]); + // substitutions are pre-rewrites + tcpg.addRewriteStep(vvec[j], svec[j], pgs[j], true); } // add the proof constructed by the term conversion utility std::shared_ptr<ProofNode> pfn = tcpg.getProofFor(eq); |