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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 20 Oct 2021 16:49:53 +0000 (11:49 -0500)
committer	GitHub <noreply@github.com>
	Wed, 20 Oct 2021 16:49:53 +0000 (16:49 +0000)
commit	90e615eb3920bd60173e967c85cbcaf4f34a032c
tree	77f0fb0dbadabc96d8cbc0ba5600fc3ffb0e5634	tree
parent	b038b34584f37c40a6dc4a476e8f486cf6977b81	commit \| diff

Use codatatype bound variables for codatatype values (#7425)

Previously, we had conflated codatatype bound variables and uninterpreted constants (as they have the same functionality). However, we should separate these concepts so we can ensure that uninterpreted constants are only used for uninterpreted sorts.

13 files changed:

src/expr/CMakeLists.txt		diff \| blob \| history
src/expr/codatatype_bound_variable.cpp	[new file with mode: 0644]	blob
src/expr/codatatype_bound_variable.h	[new file with mode: 0644]	blob
src/expr/uninterpreted_constant.cpp		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.cpp		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.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/theory_model_builder.cpp		diff \| blob \| history
test/python/unit/api/test_solver.py		diff \| blob \| history
test/unit/api/solver_black.cpp		diff \| blob \| history

RSS Atom