git.libre-soc.org Git - cvc5.git/commit

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Sat, 21 Jul 2018 14:19:31 +0000 (09:19 -0500)
committer	GitHub <noreply@github.com>
	Sat, 21 Jul 2018 14:19:31 +0000 (09:19 -0500)
commit	0d12fcbb5f1c047f951a69aa6ef4ae127f499312
tree	d177dd93a13a8ae4ac5c9a22ab8c5aa97537d19d	tree
parent	585d2ac394e99a155ed40aa2da2fb550ff60fc7b	commit \| diff

Optimizations and fixes for computing whether a type is finite (#2179)

src/expr/type_node.cpp		diff \| blob \| history
src/options/quantifiers_options.toml		diff \| blob \| history
src/theory/datatypes/datatypes_sygus.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/type_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/term_enumeration.cpp		diff \| blob \| history
src/util/cardinality.h		diff \| blob \| history
test/regress/Makefile.tests		diff \| blob \| history
test/regress/regress1/sygus/array_search_5-Q-easy.sy	[new file with mode: 0644]	blob