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/expr_manager_template.h | |
| 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/expr_manager_template.h')
| -rw-r--r-- | src/expr/expr_manager_template.h | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 3f180e951..2b9a85aca 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -435,11 +435,6 @@ class CVC4_PUBLIC ExprManager { std::set<Type>& unresolvedTypes, uint32_t flags = DATATYPE_FLAG_NONE); - /** - * Make a type representing a constructor with the given parameterization. - */ - ConstructorType mkConstructorType(const DatatypeConstructor& constructor, Type range) const; - /** Make a type representing a selector with the given parameterization. */ SelectorType mkSelectorType(Type domain, Type range) const; |