projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c0af8cf) | patch
The ProofManager now allows theory solvers to get their lemmas that participate in...
authorGuy <katz911@gmail.com>
Fri, 15 Jul 2016 23:48:25 +0000 (16:48 -0700)
committerGuy <katz911@gmail.com>
Fri, 15 Jul 2016 23:48:25 +0000 (16:48 -0700)
commit378475e685d514ec47347a9f27a2825391f9b207
tree520757bb2da753201e7e643bc47d1a116edf0ef3tree
parentc0af8cf1c1e3edca35bb7ae4edf1831ebdee0abdcommit | diff
The ProofManager now allows theory solvers to get their lemmas that participate in the unsat cores.
Currently this is only limited to lemmas generated via the d_out->lemma() interface, i.e. no propagations
and conflict lemmas.
src/proof/lemma_proof.cpp diff | blob | history
src/proof/lemma_proof.h diff | blob | history
src/proof/proof_manager.cpp diff | blob | history
src/proof/proof_manager.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history