projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2cc0e2c) | patch
Sets subtypes (#1095)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 4 May 2018 00:00:40 +0000 (19:00 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Fri, 4 May 2018 00:00:40 +0000 (17:00 -0700)
commit4873b5e515d8b3e5e70c42c50e8f680b26ba2331
tree0472c0e4dc6e4de4a1b1fba8cd08dff10c06111atree
parent2cc0e2c6a691fb6d30ed8879832b49bc1f277d77commit | diff
Sets subtypes (#1095)

Make sets theory properly handle equalities between (Set T1) and (Set T2) whenever equalities between T1 and T2 are also handled. Generalizes previous approach for type correctness conditions. Add regression.
src/theory/sets/theory_sets_private.cpp diff | blob | history
src/theory/sets/theory_sets_private.h diff | blob | history
test/regress/Makefile.tests diff | blob | history
test/regress/regress0/sets/sets-of-sets-subtypes.smt2 [new file with mode: 0644] blob