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

author	Morgan Deters <mdeters@gmail.com>
	Tue, 27 Nov 2012 02:13:38 +0000 (02:13 +0000)
committer	Morgan Deters <mdeters@gmail.com>
	Tue, 27 Nov 2012 02:13:38 +0000 (02:13 +0000)
commit	b122cec27ca27d0b48e786191448e0053be78ed0
tree	615981d8623e830894f02fc528b173ac7461f934	tree
parent	3da16da97df7cd2efd4b113db3bfef8b9c138ebe	commit \| diff

Tuples and records merge. Resolves bug 270.

Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together.

(this commit was certified error- and warning-free by the test-and-commit script.)

43 files changed:

src/expr/expr_manager_template.cpp		diff \| blob \| history
src/expr/expr_manager_template.h		diff \| blob \| history
src/expr/mkexpr		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/cvc/Cvc.g		diff \| blob \| history
src/parser/parser.cpp		diff \| blob \| history
src/parser/parser.h		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/smt/Makefile.am		diff \| blob \| history
src/smt/model_postprocessor.cpp	[new file with mode: 0644]	blob
src/smt/model_postprocessor.h	[new file with mode: 0644]	blob
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/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.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes_type_rules.h		diff \| blob \| history
src/theory/datatypes/type_enumerator.h		diff \| blob \| history
src/theory/model.cpp		diff \| blob \| history
src/theory/type_enumerator.h		diff \| blob \| history
src/util/Makefile.am		diff \| blob \| history
src/util/datatype.cpp		diff \| blob \| history
src/util/integer_cln_imp.h		diff \| blob \| history
src/util/record.cpp	[new file with mode: 0644]	blob
src/util/record.h	[new file with mode: 0644]	blob
src/util/record.i	[new file with mode: 0644]	blob
src/util/tuple.h	[new file with mode: 0644]	blob
src/util/tuple.i	[new file with mode: 0644]	blob
src/util/util_model.cpp		diff \| blob \| history
src/util/util_model.h		diff \| blob \| history
test/regress/regress0/datatypes/Makefile.am		diff \| blob \| history
test/regress/regress0/datatypes/bug438.cvc	[new file with mode: 0644]	blob

RSS Atom