projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 18758ae) | patch
[proofs] Alethe: Add finalize function to insert missing OR steps (#7724)
authorLachnitt <lachnitt@stanford.edu>
Wed, 1 Dec 2021 19:12:37 +0000 (11:12 -0800)
committerGitHub <noreply@github.com>
Wed, 1 Dec 2021 19:12:37 +0000 (19:12 +0000)
commitb2cce731768066e5bdc62838cf14ae9e528da95e
tree6106ae1f6a707a7d3dbad15bc2d462e4ede73f03tree
parent18758ae6ba02fb30744e560bf660c75a3af78008commit | diff
[proofs] Alethe: Add finalize function to insert missing OR steps (#7724)

A post visit that adds an OR step is needed in case a premise is printed as a singleton (cl (or F1 ... Fn)) but used as a clause (cl F1 ... Fn).

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