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/smt/smt_engine.cpp | |
| 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/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 43459dcec..180b33fe0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -683,7 +683,8 @@ class SmtEnginePrivate : public NodeManagerListener { { if ((flags & ExprManager::DATATYPE_FLAG_PLACEHOLDER) == 0) { - DatatypeDeclarationCommand c(dtts); + std::vector<Type> types(dtts.begin(), dtts.end()); + DatatypeDeclarationCommand c(types); d_smt.addToModelCommandAndDump(c); } } |