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/cvc/Cvc.g | |
| 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/cvc/Cvc.g')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index e3d0e0696..64eb56c74 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -757,7 +757,7 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd] END_TOK { PARSER_STATE->popScope(); cmd->reset(new DatatypeDeclarationCommand( - PARSER_STATE->mkMutualDatatypeTypes(dts))); + api::sortVectorToTypes(PARSER_STATE->mkMutualDatatypeTypes(dts)))); } | CONTEXT_TOK |