projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a663cf1) | patch
Add proof annotation option (#7750)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 7 Dec 2021 22:40:40 +0000 (16:40 -0600)
committerGitHub <noreply@github.com>
Tue, 7 Dec 2021 22:40:40 +0000 (22:40 +0000)
commit0226b383f8f70136843c7c2d21487e10a774f0f0
tree8c4b312121e93cf259d0b8f77e841536da77de0dtree
parenta663cf120b68787fe9399411aac33ea4837fa60ecommit | diff
Add proof annotation option (#7750)

Adds --proof-annotate which enables a useful stat in which we count the number of times a lemma with a given inference id appears in a final proof.

This can be used to determine which lemma schemas are the most useful for showing a problem unsat.
14 files changed:
src/CMakeLists.txt diff | blob | history
src/options/proof_options.toml diff | blob | history
src/proof/annotation_proof_generator.cpp [new file with mode: 0644] blob
src/proof/annotation_proof_generator.h [new file with mode: 0644] blob
src/proof/proof_node_to_sexpr.cpp diff | blob | history
src/proof/proof_rule.cpp diff | blob | history
src/proof/proof_rule.h diff | blob | history
src/smt/proof_final_callback.cpp diff | blob | history
src/smt/proof_final_callback.h diff | blob | history
src/theory/builtin/proof_checker.cpp diff | blob | history
src/theory/inference_id_proof_annotator.cpp [new file with mode: 0644] blob
src/theory/inference_id_proof_annotator.h [new file with mode: 0644] blob
src/theory/theory_inference_manager.cpp diff | blob | history
src/theory/theory_inference_manager.h diff | blob | history