projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8a0d2b0) | patch
Handle subtypes in sets. Bug fixes for tuples with subtypes.
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 21 Apr 2017 14:26:04 +0000 (09:26 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 21 Apr 2017 14:26:19 +0000 (09:26 -0500)
commita33dac29d9cc8520f62b6e4f4f9138ea4e3fbcd4
treeb92bc3f34aca16a4b4ed6d42b2c2ae909dff17d4tree
parent8a0d2b0577e174d2078026129dd01ea46f7f984acommit | diff
Handle subtypes in sets. Bug fixes for tuples with subtypes.
26 files changed:
src/expr/type_node.cpp diff | blob | history
src/expr/type_node.h diff | blob | history
src/options/sets_options diff | blob | history
src/theory/datatypes/datatypes_rewriter.h diff | blob | history
src/theory/datatypes/theory_datatypes_type_rules.h diff | blob | history
src/theory/quantifiers/macros.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history
src/theory/sets/theory_sets_private.h diff | blob | history
src/theory/sets/theory_sets_type_rules.h diff | blob | history
test/regress/regress0/datatypes/Makefile.am diff | blob | history
test/regress/regress0/datatypes/tuple-no-clash.cvc [new file with mode: 0644] blob
test/regress/regress0/rels/atom_univ2.cvc diff | blob | history
test/regress/regress0/sets/Makefile.am diff | blob | history
test/regress/regress0/sets/complement.cvc diff | blob | history
test/regress/regress0/sets/complement2.cvc diff | blob | history
test/regress/regress0/sets/complement3.cvc diff | blob | history
test/regress/regress0/sets/int-real-univ-unsat.smt2 [new file with mode: 0644] blob
test/regress/regress0/sets/int-real-univ.smt2 [new file with mode: 0644] blob
test/regress/regress0/sets/nonvar-univ.smt2 diff | blob | history
test/regress/regress0/sets/pre-proc-univ.smt2 diff | blob | history
test/regress/regress0/sets/sets-poly-int-real.smt2 [new file with mode: 0644] blob
test/regress/regress0/sets/sets-poly-nonint.smt2 [new file with mode: 0644] blob
test/regress/regress0/sets/sets-tuple-poly.cvc [new file with mode: 0644] blob
test/regress/regress0/sets/univset-simp.smt2 diff | blob | history