Simplify DatatypeDeclarationCommand command (#3928)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 6 Mar 2020 21:55:21 +0000 (15:55 -0600)
committerGitHub <noreply@github.com>
Fri, 6 Mar 2020 21:55:21 +0000 (15:55 -0600)
commit75502e8c943d747df6c9d10a237238e8443d6c38
tree75cccccebb1819680f43cc5a9c16194e511a4ac4
parent89337334236176bff2d561c42b9b55ab9d91bd62
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.
src/parser/cvc/Cvc.g
src/parser/parser.cpp
src/parser/parser.h
src/parser/smt2/Smt2.g
src/printer/ast/ast_printer.cpp
src/printer/cvc/cvc_printer.cpp
src/printer/smt2/smt2_printer.cpp
src/smt/command.cpp
src/smt/command.h
src/smt/smt_engine.cpp