projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cb835bd) | patch
Added functionality to retrieve a lemma's "weakest implicant" in the unsat core....
authorGuy <katz911@gmail.com>
Tue, 26 Jul 2016 20:09:31 +0000 (13:09 -0700)
committerGuy <katz911@gmail.com>
Tue, 26 Jul 2016 20:09:31 +0000 (13:09 -0700)
commit319bbda7ad32e6e9ee009c27003f6f1c0a8d7b20
tree9648cdfb58b5f132d9a40a919dac792ad6da3c34tree
parentcb835bd526296d97f8ceb001569493723a59f86bcommit | 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.
src/proof/proof_manager.cpp diff | blob | history
src/proof/proof_manager.h diff | blob | history
src/proof/sat_proof.h diff | blob | history
src/proof/sat_proof_implementation.h diff | blob | history