projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 80493d9) | patch
(proof-new) Term conversion proof generator utility (#4603)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 12 Jun 2020 19:13:12 +0000 (14:13 -0500)
committerGitHub <noreply@github.com>
Fri, 12 Jun 2020 19:13:12 +0000 (14:13 -0500)
commita3efc3697434902c5b147ee16c34d7291734206f
treed8897be26f750eb5c414ad6ae40566df2e5dec4dtree
parent80493d9fa63169f02ff8b3c71622c49c6e068357commit | diff
(proof-new) Term conversion proof generator utility (#4603)

This utility is used for constructing any proof where a term is "converted" into another by small step rewrites. This utility will be used to construct the skeleton of the proofs of rewrites, preprocessing steps, expand definitions, results of substitutions, and so on.
src/expr/CMakeLists.txt diff | blob | history
src/expr/term_conversion_proof_generator.cpp [new file with mode: 0644] blob
src/expr/term_conversion_proof_generator.h [new file with mode: 0644] blob