projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 738676c) | patch
(proof-new) Witness axiom reconstruction for purification skolems (#5289)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 18 Oct 2020 23:42:46 +0000 (18:42 -0500)
committerGitHub <noreply@github.com>
Sun, 18 Oct 2020 23:42:46 +0000 (18:42 -0500)
commit912ada0fb5368f3420b455b8bc76e88db164c37c
tree0452820fe6d4df223681bcc28817b7d928261e81tree
parent738676c39badd9a03db0feaa00bb4bd467f0600acommit | diff
 (proof-new) Witness axiom reconstruction for purification skolems (#5289)

This formalizes the proofs of existentials that justify purification variables, e.g. those with witness form witness x. x = t for the term t they purify.

This PR generalizes EXISTS_INTRO to do this, and makes some simplifications to SkolemManager.
src/expr/proof_rule.h diff | blob | history
src/expr/skolem_manager.cpp diff | blob | history
src/expr/skolem_manager.h diff | blob | history
src/smt/witness_form.cpp diff | blob | history
src/smt/witness_form.h diff | blob | history
src/theory/quantifiers/proof_checker.cpp diff | blob | history