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

author	Morgan Deters <mdeters@cs.nyu.edu>
	Mon, 28 Jan 2013 22:31:57 +0000 (17:31 -0500)
committer	Morgan Deters <mdeters@cs.nyu.edu>
	Fri, 22 Mar 2013 22:54:52 +0000 (18:54 -0400)
commit	f44a81d1b62058fa56af952aa92be965690481e5
tree	dc4b56e27701abd61ebd69675f86a9366d90998f	tree
parent	36816ad2537a2e6163037e9592c513b9a69aa9dc	commit \| diff

Support for Boolean term conversion in datatypes.

30 files changed:

NEWS		diff \| blob \| history
src/expr/expr_manager_template.cpp		diff \| blob \| history
src/expr/node_builder.h		diff \| blob \| history
src/expr/type_node.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/smt/boolean_terms.cpp		diff \| blob \| history
src/smt/boolean_terms.h		diff \| blob \| history
src/smt/model_postprocessor.cpp		diff \| blob \| history
src/smt/model_postprocessor.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/theory/booleans/Makefile.am		diff \| blob \| history
src/theory/booleans/boolean_term_conversion_mode.cpp	[new file with mode: 0644]	blob
src/theory/booleans/boolean_term_conversion_mode.h	[new file with mode: 0644]	blob
src/theory/booleans/options		diff \| blob \| history
src/theory/booleans/options_handlers.h	[new file with mode: 0644]	blob
src/theory/builtin/theory_builtin_type_rules.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/type_enumerator.h		diff \| blob \| history
src/theory/model.cpp		diff \| blob \| history
src/util/datatype.cpp		diff \| blob \| history
src/util/datatype.h		diff \| blob \| history
test/regress/regress0/datatypes/Makefile.am		diff \| blob \| history
test/regress/regress0/datatypes/boolean-terms-datatype.cvc	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/boolean-terms-record.cvc	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/boolean-terms-tuple.cvc	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/pair-real-bool.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/some-boolean-tests.cvc	[new file with mode: 0644]	blob

RSS Atom