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

author	Morgan Deters <mdeters@gmail.com>
	Thu, 7 Oct 2010 07:16:49 +0000 (07:16 +0000)
committer	Morgan Deters <mdeters@gmail.com>
	Thu, 7 Oct 2010 07:16:49 +0000 (07:16 +0000)
commit	2d7ff62cd52c5c56f29b6567489310cc45767236
tree	afb975f93b219e7b7a670a4dfc2897e425fd9bf7	tree
parent	ce4a5fe6a2529f11eaff66b6cdcdb32ef5309323	commit \| diff

SMT-LIBv2 (define-fun...) command now functional; does eager expansion at preprocessing time

21 files changed:

src/expr/command.cpp		diff \| blob \| history
src/expr/command.h		diff \| blob \| history
src/expr/expr_template.cpp		diff \| blob \| history
src/expr/expr_template.h		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_value.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/expr/type_node.h		diff \| blob \| history
src/main/getopt.cpp		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/smt/Makefile.am		diff \| blob \| history
src/smt/bad_option.h	[deleted file]	blob \| history
src/smt/bad_option_exception.h	[new file with mode: 0644]	blob
src/smt/no_such_function_exception.h	[new file with mode: 0644]	blob
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/util/options.h		diff \| blob \| history
test/regress/regress0/Makefile.am		diff \| blob \| history
test/regress/regress0/simple-rdl-definefun.smt2	[new file with mode: 0644]	blob