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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 13 May 2011 22:02:52 +0000 (22:02 +0000)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 13 May 2011 22:02:52 +0000 (22:02 +0000)
commit	8d54316e7ff784a8d66da9ecc2d289ab463761c2
tree	c7b5351b372cb360780ce62935fb2cfb5792299a	tree
parent	69c9ec0e1e42f3f2f2f79d3e98398c5cd1559c66	commit \| diff

added support for parametric datatypes, updated cvc parser to handle parametric datatypes, type ascriptions are not implemented yet

18 files changed:

src/expr/declaration_scope.cpp		diff \| blob \| history
src/expr/declaration_scope.h		diff \| blob \| history
src/expr/expr_manager_template.cpp		diff \| blob \| history
src/expr/expr_manager_template.h		diff \| blob \| history
src/expr/node_manager.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/parser/cvc/Cvc.g		diff \| blob \| history
src/parser/parser.cpp		diff \| blob \| history
src/parser/parser.h		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.h		diff \| blob \| history
src/theory/datatypes/kinds		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes_type_rules.h		diff \| blob \| history
src/util/datatype.cpp		diff \| blob \| history
src/util/datatype.h		diff \| blob \| history