Datatypes with nested recursion are not handled in TheoryDatatypes unless option...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 5 Jun 2020 22:57:25 +0000 (17:57 -0500)
committerGitHub <noreply@github.com>
Fri, 5 Jun 2020 22:57:25 +0000 (17:57 -0500)
commitc8015e6dc858a3fd13234ec4acb22c80cb339ddc
tree0a5e7c4fc112f3753eae8dc8e6283933373aa840
parent5c4b9e1a6ffa97a0a1f8af41069f29764eb6c74b
Datatypes with nested recursion are not handled in TheoryDatatypes unless option is set (#3707)

Towards experimental support for non-simply recursive datatypes (https://github.com/ajreynol/CVC4/tree/dtNonSimpleRec). Builds a check for non-simple recursion in the DType class. If a term of a datatype type is registered to TheoryDatatypes for a datatype that has nested recursion, we throw a LogicException unless the option dtNestedRec is set to true. Also includes a bug discovered in the TypeMatcher utility and another in expr::getComponentTypes.

It also adds a unit test using the new API for a simple parametric datatype example as well, not related to nested recursion, as this was previously missing.
12 files changed:
src/api/cvc4cpp.cpp
src/api/cvc4cpp.h
src/expr/datatype.cpp
src/expr/datatype.h
src/expr/dtype.cpp
src/expr/dtype.h
src/expr/node_algorithm.cpp
src/expr/type_matcher.cpp
src/options/datatypes_options.toml
src/theory/datatypes/theory_datatypes.cpp
test/unit/api/datatype_api_black.h
test/unit/parser/parser_black.h