projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a8e839e) | patch
(proof-new) Updates to assertions pipeline and preprocess generator (#5300)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 19 Oct 2020 17:01:33 +0000 (12:01 -0500)
committerGitHub <noreply@github.com>
Mon, 19 Oct 2020 17:01:33 +0000 (12:01 -0500)
commit3bfdead7da2143fd801fa632165a986b2631ad3d
tree1bb807b6a0c525de1aa167f220d28d97260138c5tree
parenta8e839e29325f06ecd2d5dda7d8f64a44ddafb0ccommit | diff
(proof-new) Updates to assertions pipeline and preprocess generator (#5300)

This updates and improves assertions pipeline and preprocess generator so that they avoid cyclic proofs and have better infrastructure for catching pedantic failures.

This is in preparation for making the non-clausal-simplification pass proof producing.
src/preprocessing/assertion_pipeline.cpp diff | blob | history
src/preprocessing/assertion_pipeline.h diff | blob | history
src/smt/preprocess_proof_generator.cpp diff | blob | history
src/smt/preprocess_proof_generator.h diff | blob | history