(proof-new) Use deep copy for final lemma step in proof equality engine (#5013)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 11 Sep 2020 19:38:13 +0000 (14:38 -0500)
committerGitHub <noreply@github.com>
Fri, 11 Sep 2020 19:38:13 +0000 (14:38 -0500)
commitbff3b0cbcc38cae5548bc4b36af5bb1c0f66c149
treec7c980ff07ebf1895633a9e22ca14010c8089d4f
parentedf2e3ff7b751001901d377c3aacd044a3e15ef4
(proof-new) Use deep copy for final lemma step in proof equality engine (#5013)

Previously, strings on proof-new used a ProofStepBuffer for deriving the final conclusion of lemmas in proof equality engine (assertLemma). This was recently changed to use the more standard ProofGenerator interface of assertLemma. However, there was a bug in this method: the steps from this proof need to be deep copied into the proof we are generating or otherwise the explanation of these literals are not connected in the CDProof. This updates the proof equality engine so that it instructs the proof generator to do a deep copy in this case. Notice this is very rarely more than a single step.
src/expr/proof_generator.cpp
src/expr/proof_generator.h
src/theory/uf/proof_equality_engine.cpp