projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b9eee8d) | patch
(proof-new) Proofs for skolemization (#5339)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 12 Nov 2020 16:33:32 +0000 (10:33 -0600)
committerGitHub <noreply@github.com>
Thu, 12 Nov 2020 16:33:32 +0000 (10:33 -0600)
commit4f367612a386d21315cee7d377176bc83a1402c5
tree6b572e49d2cddecf11ce8fedf74084df5c449420tree
parentb9eee8d69e9de4641514c35d49c495bd5adead5fcommit | diff
(proof-new) Proofs for skolemization (#5339)

This adds support for proofs in the quantifiers module that performs skolemization.

Also fixes a bug in the proof checker for skolemization.
src/theory/quantifiers/proof_checker.cpp diff | blob | history
src/theory/quantifiers/skolemize.cpp diff | blob | history
src/theory/quantifiers/skolemize.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history