Add methods for constructing datatype types from NodeManager (#4823)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 2 Aug 2020 03:27:08 +0000 (22:27 -0500)
committerGitHub <noreply@github.com>
Sun, 2 Aug 2020 03:27:08 +0000 (22:27 -0500)
commit5be889668bfb52d6705c2dc37ec05c291c7c9445
tree4edbfeabcd3f5cf034ffd8b99b01a539820a5a99
parent230d27bad9b4cd49bad1164145cf83c9f04e9aca
Add methods for constructing datatype types from NodeManager (#4823)

This is work towards eliminating the Expr-level datatype.

This PR implements the required methods for constructing datatype types from NodeManager.

In particular, this PR copies the "mkMutualDatatypeTypes" methods and converts them to Node-level.

The next PRs will be in preparation for using these methods instead of the Expr-level ones.

It also adds a flag d_isRecord to DType, which is required for supporting record printing in the cvc printer, which will be updated in another PR.

It also eliminates an interface for constructing constructor types via Expr-level DatatypeConstructor objects, which was unused.
src/expr/dtype.cpp
src/expr/dtype.h
src/expr/expr_manager_template.cpp
src/expr/expr_manager_template.h
src/expr/node_manager.cpp
src/expr/node_manager.h
src/smt/listeners.cpp
src/smt/listeners.h