projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a34f297) | patch
(proof-new) SMT Preprocess proof generator (#4708)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 13 Jul 2020 22:42:57 +0000 (17:42 -0500)
committerGitHub <noreply@github.com>
Mon, 13 Jul 2020 22:42:57 +0000 (17:42 -0500)
commit1cb249c9dd06a049953f001cd6d82c0e6f1246f2
tree000398841f1869d9911e1e496623520ffb6de21atree
parenta34f29798b3f4d1f83e1ced57fe53db53b9956f0commit | diff
 (proof-new) SMT Preprocess proof generator (#4708)

This adds the proof generator for storing proofs of preprocessing. It stores assertions added via preprocessing passes and their rewrites. This utility will eventually live in SmtEngine.

It also adds 2 new proof rules, and fixes an issue in ProofNodeUpdater.
src/CMakeLists.txt diff | blob | history
src/expr/proof_node_updater.cpp diff | blob | history
src/expr/proof_rule.cpp diff | blob | history
src/expr/proof_rule.h diff | blob | history
src/smt/preprocess_proof_generator.cpp [new file with mode: 0644] blob
src/smt/preprocess_proof_generator.h [new file with mode: 0644] blob
src/theory/booleans/proof_checker.cpp diff | blob | history
src/theory/builtin/proof_checker.cpp diff | blob | history
src/theory/trust_node.cpp diff | blob | history
src/theory/trust_node.h diff | blob | history