projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 90b909a) | patch
Better infrastructure for proving constant disequality.
authorGuy <katz911@gmail.com>
Fri, 3 Jun 2016 21:27:00 +0000 (14:27 -0700)
committerGuy <katz911@gmail.com>
Fri, 3 Jun 2016 21:27:00 +0000 (14:27 -0700)
commit8bfab32eed06973d53ce8ae066a9a26d4ae8a489
tree4fb698b165bfe4aa80560d91f7334f27965dc641tree
parent90b909a89c78c75afae69e119feea20b478c0795commit | diff
Better infrastructure for proving constant disequality.
Added support for the BV case
proofs/signatures/th_bv.plf diff | blob | history
src/proof/bitvector_proof.cpp diff | blob | history
src/proof/bitvector_proof.h diff | blob | history
src/proof/theory_proof.cpp diff | blob | history
src/proof/theory_proof.h diff | blob | history