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

author	Morgan Deters <mdeters@gmail.com>
	Tue, 28 Aug 2012 01:10:16 +0000 (01:10 +0000)
committer	Morgan Deters <mdeters@gmail.com>
	Tue, 28 Aug 2012 01:10:16 +0000 (01:10 +0000)
commit	cf287f593931a1c4fc141e18845b4c5d36879889
tree	4dad0f555b7db01fbeedcd9eace394cd8f7a0fb4	tree
parent	b7b1c1d99ffa333704af2c8ecd60b1af8833a28b	commit \| diff

Improved compatibility layer, now supports quantifiers. Also incorporates
numerous bugfixes, and the cvc3 system test is enabled.

23 files changed:

src/compat/cvc3_compat.cpp		diff \| blob \| history
src/compat/cvc3_compat.h		diff \| blob \| history
src/expr/expr_template.cpp		diff \| blob \| history
src/expr/expr_template.h		diff \| blob \| history
src/expr/type.cpp		diff \| blob \| history
src/expr/type.h		diff \| blob \| history
src/expr/type_node.cpp		diff \| blob \| history
src/options/Makefile.am		diff \| blob \| history
src/options/base_options		diff \| blob \| history
src/options/base_options_handlers.h		diff \| blob \| history
src/options/option_exception.h		diff \| blob \| history
src/smt/options		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/smt/smt_options_template.cpp		diff \| blob \| history
src/theory/arrays/kinds		diff \| blob \| history
src/theory/arrays/theory_arrays_type_rules.h		diff \| blob \| history
src/theory/bv/kinds		diff \| blob \| history
src/util/Makefile.am		diff \| blob \| history
src/util/rational_cln_imp.h		diff \| blob \| history
src/util/rational_gmp_imp.h		diff \| blob \| history
test/system/Makefile.am		diff \| blob \| history
test/system/cvc3_main.cpp		diff \| blob \| history