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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 27 May 2020 23:05:07 +0000 (18:05 -0500)
committer	GitHub <noreply@github.com>
	Wed, 27 May 2020 23:05:07 +0000 (16:05 -0700)
commit	4df14f1e09549be607123c66b7dd206e8e244c89
tree	3104897629ebe9efe4d14983ad89fb0d8778d4f2	tree
parent	449cf281987eb8a2d43a572817db5c870a010c08	commit \| diff

Add the Expr-level sequence datatype (#4526)

This adds the expr-level sequence datatypes. This is required for further progress on sequences. However, note that this class may be deleted in the further when the Expr level is replaced.

12 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/bindings/java/CMakeLists.txt		diff \| blob \| history
src/cvc4.i		diff \| blob \| history
src/expr/CMakeLists.txt		diff \| blob \| history
src/expr/expr.i		diff \| blob \| history
src/expr/expr_manager.i		diff \| blob \| history
src/expr/expr_sequence.cpp	[new file with mode: 0644]	blob
src/expr/expr_sequence.h	[new file with mode: 0644]	blob
src/expr/expr_sequence.i	[new file with mode: 0644]	blob
src/expr/sequence.cpp		diff \| blob \| history
src/expr/sequence.h		diff \| blob \| history
src/theory/strings/kinds		diff \| blob \| history

RSS Atom