projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8bfab32) | patch
Support for printing a global let map in LFSC proofs.
authorGuy <katz911@gmail.com>
Wed, 8 Jun 2016 18:52:42 +0000 (11:52 -0700)
committerGuy <katz911@gmail.com>
Wed, 8 Jun 2016 18:52:42 +0000 (11:52 -0700)
commit4b8f92d23f7a75b4148f41e039f7bdc5f165babc
treee2d8abdff6f2d6befa652a09188fff991caf1cf4tree
parent8bfab32eed06973d53ce8ae066a9a26d4ae8a489commit | diff
Support for printing a global let map in LFSC proofs.
Added a flag to enable/disbale this feature (enabled by default).

Also, added some infrastructure for proving rewrite rules.
19 files changed:
proofs/signatures/Makefile.am diff | blob | history
proofs/signatures/th_bv_rewrites.plf [new file with mode: 0644] blob
src/options/proof_options diff | blob | history
src/proof/arith_proof.cpp diff | blob | history
src/proof/arith_proof.h diff | blob | history
src/proof/array_proof.cpp diff | blob | history
src/proof/array_proof.h diff | blob | history
src/proof/bitvector_proof.cpp diff | blob | history
src/proof/bitvector_proof.h diff | blob | history
src/proof/cnf_proof.cpp diff | blob | history
src/proof/cnf_proof.h diff | blob | history
src/proof/proof_manager.cpp diff | blob | history
src/proof/proof_manager.h diff | blob | history
src/proof/proof_utils.h diff | blob | history
src/proof/theory_proof.cpp diff | blob | history
src/proof/theory_proof.h diff | blob | history
src/proof/uf_proof.cpp diff | blob | history
src/proof/uf_proof.h diff | blob | history
src/util/proof.h diff | blob | history