projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 517b6ba) | patch
[BV Proofs] Option for proof format (#2777)
authorAlex Ozdemir <aozdemir@hmc.edu>
Wed, 9 Jan 2019 18:19:22 +0000 (19:19 +0100)
committerAndres Noetzli <andres.noetzli@gmail.com>
Wed, 9 Jan 2019 18:19:22 +0000 (10:19 -0800)
commit1df477011ed5d35f222340580cba916af3ba73b5
treef937ddc250589678d584577bd48e624eec8d8d8ctree
parent517b6ba3bb029470bdb3f230188af1f398b14a91commit | diff
[BV Proofs] Option for proof format (#2777)

We're building out a system whereby (eager) BV proofs can be emitted in
one of three formats. Let's add an option for specifying which!

My testing mechanism was not very thorough: I verified that I could specify each of the following option values:
* `er`
* `lrat`
* `drat`
* `help`

and that I could not provide random other option values.
src/options/bv_bitblast_mode.cpp diff | blob | history
src/options/bv_bitblast_mode.h diff | blob | history
src/options/bv_options.toml diff | blob | history
src/options/options_handler.cpp diff | blob | history
src/options/options_handler.h diff | blob | history