diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-01 22:27:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-01 22:27:08 -0500 |
| commit | 5be889668bfb52d6705c2dc37ec05c291c7c9445 (patch) | |
| tree | 4edbfeabcd3f5cf034ffd8b99b01a539820a5a99 /src/expr/lazy_proof.cpp | |
| parent | 230d27bad9b4cd49bad1164145cf83c9f04e9aca (diff) | |
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.
Diffstat (limited to 'src/expr/lazy_proof.cpp')
0 files changed, 0 insertions, 0 deletions