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

author	ajreynol <andrew.j.reynolds@gmail.com>
	Mon, 15 Feb 2016 19:02:02 +0000 (13:02 -0600)
committer	ajreynol <andrew.j.reynolds@gmail.com>
	Mon, 15 Feb 2016 19:02:02 +0000 (13:02 -0600)
commit	62b673a6b8444c14c169a984dd6e3fc8f685851e
tree	f0703edec34e3512dac340ce0059cba6368d7dd8	tree
parent	7acc2844df65ab6fdbf8166653c71eaa26d4d151	commit \| diff

Eliminate most of the internal representation infrastructure for tuples and records, replace with datatypes throughout, update cvc printer for tuples/records. Minor changes to API for records and tuples.

25 files changed:

src/compat/cvc3_compat.cpp		diff \| blob \| history
src/expr/datatype.cpp		diff \| blob \| history
src/expr/datatype.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.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/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/smt/boolean_terms.cpp		diff \| blob \| history
src/smt/model_postprocessor.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		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/theory/datatypes/type_enumerator.cpp		diff \| blob \| history
src/theory/datatypes/type_enumerator.h		diff \| blob \| history
src/theory/theory_model.cpp		diff \| blob \| history
test/unit/expr/expr_manager_public.h		diff \| blob \| history

RSS Atom