diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-06 15:55:21 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-06 15:55:21 -0600 |
| commit | 75502e8c943d747df6c9d10a237238e8443d6c38 (patch) | |
| tree | 75cccccebb1819680f43cc5a9c16194e511a4ac4 /src/parser/parser.h | |
| parent | 89337334236176bff2d561c42b9b55ab9d91bd62 (diff) | |
Simplify DatatypeDeclarationCommand command (#3928)
The new API does not use inheritence for Sorts. The current DatatypeDeclarationCommand uses DatatypeType, which inherits from Type. This commit simplifies the class DatatypeType -> Type and updates the necessary code (e.g. in the printers). Notice we are not yet converting commands Type -> Sort here.
It also makes the main call for constructing datatypes in the parser from DatatypeType -> api::Sort.
This is in preparation for converting Expr-level Datatype to Term-level DatatypeDecl in the parsers.
Diffstat (limited to 'src/parser/parser.h')
| -rw-r--r-- | src/parser/parser.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index 3237c2893..c7efcbacb 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -604,7 +604,7 @@ public: * printed out as a definition in models or not * (see enum in expr_manager_template.h). */ - std::vector<DatatypeType> mkMutualDatatypeTypes( + std::vector<api::Sort> mkMutualDatatypeTypes( std::vector<Datatype>& datatypes, bool doOverload = false, uint32_t flags = ExprManager::DATATYPE_FLAG_NONE); |