Internal simplifications to constructing datatypes (#8519)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 1 Apr 2022 18:16:43 +0000 (13:16 -0500)
committerGitHub <noreply@github.com>
Fri, 1 Apr 2022 18:16:43 +0000 (18:16 +0000)
commitee689a569dfe33fc7245c5133ff5de5de57cd1d9
tree702abad53dc64b44250a011a3c4a19b025098340
parent4c682ca762dd54d1ac9e0b5ef116d98eaa045429
Internal simplifications to constructing datatypes (#8519)

In preparation for #8511.

This makes it so that unresolved sorts are automatically inferred when constructing datatypes at the NodeManager level. This is in preparation for simplifying the API.

Changes:
(1) NodeManager is cleaned so that unresolved types are automatically inferred and are not a part of its public interface. Internal code generating datatypes is simplified as a result.
(2) Adds necessary utilities to TypeNode and cleans an unused flag
(3) The parser is cleaned to not track unresolved sorts in an ad-hoc manner.
(4) The API is patched to use the simpler interface.
20 files changed:
src/api/cpp/cvc5.cpp
src/expr/dtype.cpp
src/expr/dtype.h
src/expr/dtype_cons.cpp
src/expr/dtype_cons.h
src/expr/dtype_selector.cpp
src/expr/node_manager_attributes.h
src/expr/node_manager_template.cpp
src/expr/node_manager_template.h
src/expr/type_node.cpp
src/expr/type_node.h
src/parser/parser.cpp
src/parser/parser.h
src/preprocessing/passes/synth_rew_rules.cpp
src/theory/datatypes/sygus_datatype_utils.cpp
src/theory/quantifiers/sygus/cegis_unif.cpp
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
test/unit/node/type_cardinality_black.cpp
test/unit/util/datatype_black.cpp