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

author	Morgan Deters <mdeters@gmail.com>
	Sat, 14 Jul 2012 22:53:58 +0000 (22:53 +0000)
committer	Morgan Deters <mdeters@gmail.com>
	Sat, 14 Jul 2012 22:53:58 +0000 (22:53 +0000)
commit	4941b3c516361183b4623f5660128e4f1bcce809
tree	5a996a0778b9a78b27b041fa582ff5585b710013	tree
parent	1c42109395b566a0068cc3ae9067fc87ab8f8e7b	commit \| diff

Type enumerator infrastructure and uninterpreted constant support. No support yet for enumerating arrays, or for enumerating non-trivial datatypes.

33 files changed:

src/expr/mkexpr		diff \| blob \| history
src/expr/mkkind		diff \| blob \| history
src/expr/mkmetakind		diff \| blob \| history
src/expr/type.h		diff \| blob \| history
src/theory/Makefile.am		diff \| blob \| history
src/theory/arith/Makefile.am		diff \| blob \| history
src/theory/arith/kinds		diff \| blob \| history
src/theory/arith/type_enumerator.h	[new file with mode: 0644]	blob
src/theory/arrays/Makefile.am		diff \| blob \| history
src/theory/arrays/kinds		diff \| blob \| history
src/theory/arrays/type_enumerator.h	[new file with mode: 0644]	blob
src/theory/booleans/Makefile.am		diff \| blob \| history
src/theory/booleans/kinds		diff \| blob \| history
src/theory/booleans/type_enumerator.h	[new file with mode: 0644]	blob
src/theory/builtin/Makefile.am		diff \| blob \| history
src/theory/builtin/kinds		diff \| blob \| history
src/theory/builtin/type_enumerator.h	[new file with mode: 0644]	blob
src/theory/bv/Makefile.am		diff \| blob \| history
src/theory/bv/kinds		diff \| blob \| history
src/theory/bv/type_enumerator.h	[new file with mode: 0644]	blob
src/theory/datatypes/Makefile.am		diff \| blob \| history
src/theory/datatypes/kinds		diff \| blob \| history
src/theory/datatypes/type_enumerator.h	[new file with mode: 0644]	blob
src/theory/mkinstantiator		diff \| blob \| history
src/theory/mkrewriter		diff \| blob \| history
src/theory/mktheorytraits		diff \| blob \| history
src/theory/type_enumerator.h	[new file with mode: 0644]	blob
src/theory/type_enumerator_template.cpp	[new file with mode: 0644]	blob
src/util/Makefile.am		diff \| blob \| history
src/util/uninterpreted_constant.cpp	[new file with mode: 0644]	blob
src/util/uninterpreted_constant.h	[new file with mode: 0644]	blob
test/unit/Makefile.am		diff \| blob \| history
test/unit/theory/type_enumerator_white.h	[new file with mode: 0644]	blob

RSS Atom