projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3b79066) | patch
(proof-new) Separate explanation stages in proof equality engine (#5356)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 12 Nov 2020 18:15:54 +0000 (12:15 -0600)
committerGitHub <noreply@github.com>
Thu, 12 Nov 2020 18:15:54 +0000 (12:15 -0600)
commita19e20cd3049134b15dbdcf7854a8854a77ccc43
tree81fced96b49a3d64e390b7cf6f108ea9d0f4e58btree
parent3b79066c39054efb95fdb71c3727482764e8a064commit | diff
(proof-new) Separate explanation stages in proof equality engine (#5356)

This fixes potential cycles in assertLemma commands in the proof equality engine by using separate proof data structures for the topmost 2 stages of proof generation for equality engine proofs. This fix is required to support datatype proofs for lemmas.

This PR also removes support for the ProofStepBuffer interface in ProofEqEngine, since it is unused, and suffers similar issues and would require a different unique fix.
src/theory/uf/proof_equality_engine.cpp diff | blob | history
src/theory/uf/proof_equality_engine.h diff | blob | history