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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Sat, 8 May 2021 00:25:27 +0000 (19:25 -0500)
committer	GitHub <noreply@github.com>
	Sat, 8 May 2021 00:25:27 +0000 (19:25 -0500)
commit	8e5aba973b06fb581221a82aacdf7d3ca7938a22
tree	ea5db058d5991ec44ca1f0c47054c3f0d733f367	tree
parent	080f0de4379c4e1fe5a016e40c7852a3abb52760	commit \| diff

Add support for datatype update (#6449)

This removes the special case of TUPLE_UPDATE and RECORD_UPDATE in favor of the more general datatype update.

Datatype update is handled analogously to APPLY_SELECTOR / APPLY_TESTER.

36 files changed:

src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5.h		diff \| blob \| history
src/api/cpp/cvc5_kind.h		diff \| blob \| history
src/api/python/cvc5.pxd		diff \| blob \| history
src/api/python/cvc5.pxi		diff \| blob \| history
src/expr/CMakeLists.txt		diff \| blob \| history
src/expr/dtype.cpp		diff \| blob \| history
src/expr/node_manager.cpp		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/expr/record.cpp	[deleted file]	blob \| history
src/expr/record.h	[deleted file]	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/parse_op.cpp		diff \| blob \| history
src/parser/parser.cpp		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.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_type_rules.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes_type_rules.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes_utils.cpp		diff \| blob \| history
src/util/CMakeLists.txt		diff \| blob \| history
src/util/tuple.h	[deleted file]	blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress0/datatypes/list-update-sat.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/list-update.smt2	[new file with mode: 0644]	blob
test/unit/api/datatype_api_black.cpp		diff \| blob \| history
test/unit/api/op_black.cpp		diff \| blob \| history
test/unit/api/solver_black.cpp		diff \| blob \| history
test/unit/api/sort_black.cpp		diff \| blob \| history
test/unit/util/datatype_black.cpp		diff \| blob \| history

RSS Atom