diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-12 16:57:42 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-12 16:57:42 -0500 |
| commit | ef71fc3405900226557dc634dcf69f1a0738fea2 (patch) | |
| tree | d7394240230050c1a99bb2e42588891600a6b154 /src/parser/parser.h | |
| parent | dd84f87edba9b0cde271fe7000208c5f8f97b890 (diff) | |
Convert most instances of dataypes in parsers to the new API (#4054)
I am still accessing Expr-level Datatypes for the sygus v1/v2 parsers (within smt2). This will be addressed in two ways in the future:
(1) The sygus v1 parser will be deleted,
(2) The sygus v2 parser will be updated to use a "Grammar" object as an extension of the new API, which will hide all calls to the underlying datatype. (See https://github.com/abdoo8080/CVC4/tree/sygus-api). FYI @abdoo8080 .
Note I've renamed "mkMutualDatatypeTypes" to "bindMutualDatatypeTypes" to be more accurate and follow the updated name conventions in the parser.
The next step will be to handle parametric datatypes, which are not specifically addressed by this PR.
Diffstat (limited to 'src/parser/parser.h')
| -rw-r--r-- | src/parser/parser.h | 19 |
1 files changed, 8 insertions, 11 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index 1197c1ff6..ecea4d3bd 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -592,19 +592,16 @@ public: bool isUnresolvedType(const std::string& name); /** - * Create sorts of mutually-recursive datatypes. - * For each symbol defined by the datatype, if a symbol with name already exists, - * then if doOverload is true, we create overloaded operators. - * else if doOverload is false, the existing expression is shadowed by the new expression. + * Creates and binds sorts of a list of mutually-recursive datatype + * declarations. * - * flags specify information about the datatype, e.g. whether it should be - * printed out as a definition in models or not - * (see enum in expr_manager_template.h). + * For each symbol defined by the datatype, if a symbol with name already + * exists, then if doOverload is true, we create overloaded operators. Else, if + * doOverload is false, the existing expression is shadowed by the new + * expression. */ - std::vector<api::Sort> mkMutualDatatypeTypes( - std::vector<Datatype>& datatypes, - bool doOverload = false, - uint32_t flags = ExprManager::DATATYPE_FLAG_NONE); + std::vector<api::Sort> bindMutualDatatypeTypes( + std::vector<api::DatatypeDecl>& datatypes, bool doOverload = false); /** make flat function type * |