projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 62a7f71) | patch
[proofs] Alethe: Removed Steps that are Double-Printed (#7754)
authorLachnitt <lachnitt@stanford.edu>
Thu, 3 Mar 2022 12:57:14 +0000 (04:57 -0800)
committerGitHub <noreply@github.com>
Thu, 3 Mar 2022 12:57:14 +0000 (12:57 +0000)
commitf3ae76033f2a8697aca5f92fed7d98c99c6c6265
treebe9d2728408974ebcd17d27d65a3df4adca2d4dctree
parent62a7f715faf99ff8ab6db34f3c790dfaf337c24ccommit | diff
[proofs] Alethe: Removed Steps that are Double-Printed (#7754)

This PR fixes that some steps are printed more than once. To this end, it deletes that the reference maps in which the steps are stored are constant and optimizes where the steps are added to the maps. It also stores ProofNodes instead of Nodes in the maps.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
src/proof/alethe/alethe_printer.cpp diff | blob | history
src/proof/alethe/alethe_printer.h diff | blob | history