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

author	Andres Noetzli <andres.noetzli@gmail.com>
	Tue, 14 Jul 2020 02:48:07 +0000 (19:48 -0700)
committer	GitHub <noreply@github.com>
	Tue, 14 Jul 2020 02:48:07 +0000 (21:48 -0500)
commit	78c0daa482b35b95c90dd058ee4dd8a981e1337f
tree	c45fe72ac96032b0e6f7ea53798443671ad08d86	tree
parent	84fe644cb1956119b7b35ede06ee93583eae1925	commit \| diff

Use TypeNode/Node in ArrayStoreAll (#4728)

This commit changes ArrayStoreAll to use Node/TypeNode instead of
Expr/Type.

18 files changed:

src/api/cvc4cpp.cpp		diff \| blob \| history
src/expr/array_store_all.cpp		diff \| blob \| history
src/expr/array_store_all.h		diff \| blob \| history
src/expr/expr_template.cpp		diff \| blob \| history
src/expr/type_node.h		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays_rewriter.h		diff \| blob \| history
src/theory/arrays/theory_arrays_type_rules.h		diff \| blob \| history
src/theory/arrays/type_enumerator.h		diff \| blob \| history
src/theory/builtin/theory_builtin_rewriter.cpp		diff \| blob \| history
test/unit/expr/expr_public.h		diff \| blob \| history
test/unit/theory/theory_black.h		diff \| blob \| history
test/unit/theory/type_enumerator_white.h		diff \| blob \| history
test/unit/util/CMakeLists.txt		diff \| blob \| history
test/unit/util/array_store_all_black.h	[deleted file]	blob \| history
test/unit/util/array_store_all_white.h	[new file with mode: 0644]	blob