projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 86569ce) | patch
(proof-new) Proofs for sets purification lemmas (#6416)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 23 Apr 2021 20:44:39 +0000 (15:44 -0500)
committerGitHub <noreply@github.com>
Fri, 23 Apr 2021 20:44:39 +0000 (20:44 +0000)
commit557e5658048b48b8908675b632fc977f78c71605
tree8ee9393db67c500705622bd450e16f21a5e3f53dtree
parent86569ce68ed002aeb31d102511d3c9bd8384a7eccommit | diff
(proof-new) Proofs for sets purification lemmas (#6416)

This adds proofs for sets purification lemmas, which are of the form (= t (skolem t)) and (member t (skolem (singleton t))). Each can be trivially justified in the internal calculus by MACRO_SR_PRED_INTRO.
src/theory/sets/skolem_cache.cpp diff | blob | history
src/theory/sets/term_registry.cpp diff | blob | history
src/theory/sets/term_registry.h diff | blob | history
src/theory/sets/theory_sets.cpp diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history
src/theory/sets/theory_sets_private.h diff | blob | history