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

author	Morgan Deters <mdeters@gmail.com>
	Wed, 6 Oct 2010 08:31:35 +0000 (08:31 +0000)
committer	Morgan Deters <mdeters@gmail.com>
	Wed, 6 Oct 2010 08:31:35 +0000 (08:31 +0000)
commit	ce4a5fe6a2529f11eaff66b6cdcdb32ef5309323
tree	4ff6643e38469ceb84cd6791c5cbc295f625a735	tree
parent	4c9f8d2b58d274e5bfea5fa28b02f005af71ef39	commit \| diff

declare-sort, define-sort working but not thoroughly tested; define-fun half working (just need to decide where to expand)

30 files changed:

src/context/cdmap.h		diff \| blob \| history
src/context/cdmap_forward.h	[new file with mode: 0644]	blob
src/context/cdset.h		diff \| blob \| history
src/expr/Makefile.am		diff \| blob \| history
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/expr_template.cpp		diff \| blob \| history
src/expr/expr_template.h		diff \| blob \| history
src/expr/mkmetakind		diff \| blob \| history
src/expr/node.cpp		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_manager.cpp		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/parser.cpp		diff \| blob \| history
src/parser/parser.h		diff \| blob \| history
src/parser/smt/smt.cpp		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/theory/builtin/kinds		diff \| blob \| history
src/theory/builtin/theory_builtin_type_rules.h		diff \| blob \| history
src/theory/bv/kinds		diff \| blob \| history
src/theory/uf/kinds		diff \| blob \| history
src/util/hash.h		diff \| blob \| history