projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 33f5149) | patch
[proof-new] A simple proof generator for buffered proof steps (#5069)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Wed, 16 Sep 2020 02:36:21 +0000 (23:36 -0300)
committerGitHub <noreply@github.com>
Wed, 16 Sep 2020 02:36:21 +0000 (23:36 -0300)
commit8a126d59141d2889e3b10b07ece4b10f48511a71
treeb4d5f303a120fbf5eeba3c7cfb0c8ea81eff9555tree
parent33f51490a9df73d8fee25fb88b19a87339b28e95commit | diff
[proof-new] A simple proof generator for buffered proof steps (#5069)

This commit also modifies proof equality engine to use this new proof generator rather than the FactProofGenerator, on which this new one is based.

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
src/expr/CMakeLists.txt diff | blob | history
src/expr/buffered_proof_generator.cpp [new file with mode: 0644] blob
src/expr/buffered_proof_generator.h [new file with mode: 0644] blob
src/theory/uf/proof_equality_engine.cpp diff | blob | history
src/theory/uf/proof_equality_engine.h diff | blob | history