diff options
| author | Guy <katz911@gmail.com> | 2016-07-26 13:09:31 -0700 |
|---|---|---|
| committer | Guy <katz911@gmail.com> | 2016-07-26 13:09:31 -0700 |
| commit | 319bbda7ad32e6e9ee009c27003f6f1c0a8d7b20 (patch) | |
| tree | 9648cdfb58b5f132d9a40a919dac792ad6da3c34 /src/proof/bitvector_proof.h | |
| parent | cb835bd526296d97f8ceb001569493723a59f86b (diff) | |
Added functionality to retrieve a lemma's "weakest implicant" in the unsat core. Currently, lemmas that are not conjunctions and their own weakest implicants; but for lemmas that *are* conjunctions, we may return only a subset of the conjuncts.
Diffstat (limited to 'src/proof/bitvector_proof.h')
0 files changed, 0 insertions, 0 deletions