projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: afe8452) | patch
better support for proof production when encountering bool terms: handle the new...
authorguykatzz <katz911@gmail.com>
Fri, 17 Mar 2017 21:11:41 +0000 (14:11 -0700)
committerguykatzz <katz911@gmail.com>
Fri, 17 Mar 2017 21:12:04 +0000 (14:12 -0700)
commit768534c0973788cab0097c6485e5113da1d406da
tree32e8eda1c7882f05b16c4bbec4e4095efbec34d3tree
parentafe84522b87b6fc0ad5d0e9a396b61f7b523f674commit | diff
better support for proof production when encountering bool terms: handle the new proof constructs generated by the equality engine.

proof production for bool-array.smt2 passes
12 files changed:
proofs/signatures/smt.plf diff | blob | history
src/Makefile.am diff | blob | history
src/proof/array_proof.cpp diff | blob | history
src/proof/proof_manager.cpp diff | blob | history
src/proof/proof_manager.h diff | blob | history
src/proof/simplify_boolean_node.cpp [new file with mode: 0644] blob
src/proof/simplify_boolean_node.h [new file with mode: 0644] blob
src/proof/theory_proof.cpp diff | blob | history
src/proof/theory_proof.h diff | blob | history
src/proof/uf_proof.cpp diff | blob | history
src/proof/uf_proof.h diff | blob | history
test/regress/regress0/arrays/bool-array.smt2 diff | blob | history