diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-25 19:04:39 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-25 19:04:39 -0500 |
commit | 34eac85599875517732d53a5cc1acd3ab60479d1 (patch) | |
tree | ebfa9e493b32aba67d85d6d0bb7a6b468fac5fd4 /src/expr/expr_manager_template.h | |
parent | c5eb77b96cd67b8d80ee8901a3f0b5ae7d54aab2 (diff) |
Replace Expr-level datatype with Node-level DType (#4875)
This PR makes two simultaneous changes:
The new API uses Node-level DType instead of Expr-level Datatype. This required converting 2 of the last remaining calls in the parser that used Expr to use the new API.
Internally constructed datatypes (e.g. for sygus) use Node-level DType instead of Expr-level Datatype. Note this required moving a block of code for handling a corner case of sygus from Datatype -> DType.
This PR removes :
ExprManger::mkDatatypeType.
The Expr-level datatype itself. This PR removes all references to its include file.
It also updates one remaining unit test from Expr -> Node.
This PR will enable further removal of other datatype-specific things in the Expr layer.
Diffstat (limited to 'src/expr/expr_manager_template.h')
-rw-r--r-- | src/expr/expr_manager_template.h | 90 |
1 files changed, 0 insertions, 90 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 2b9a85aca..a6fce56a2 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -65,11 +65,6 @@ class CVC4_PUBLIC ExprManager { NodeManager* getNodeManager() const; /** - * Check some things about a newly-created DatatypeType. - */ - void checkResolvedDatatype(DatatypeType dtt) const; - - /** * SmtEngine will use all the internals, so it will grab the * NodeManager. */ @@ -84,10 +79,6 @@ class CVC4_PUBLIC ExprManager { // undefined, private copy constructor and assignment op (disallow copy) ExprManager(const ExprManager&) = delete; ExprManager& operator=(const ExprManager&) = delete; - - /** A list of datatypes owned by this expr manager. */ - std::vector<std::unique_ptr<Datatype> > d_ownedDatatypes; - /** Creates an expression manager. */ ExprManager(); public: @@ -346,18 +337,6 @@ class CVC4_PUBLIC ExprManager { FunctionType mkPredicateType(const std::vector<Type>& sorts); /** - * Make a tuple type with types from - * <code>types[0..types.size()-1]</code>. <code>types</code> must - * have at least one element. - */ - DatatypeType mkTupleType(const std::vector<Type>& types); - - /** - * Make a record type with types from the rec parameter. - */ - DatatypeType mkRecordType(const Record& rec); - - /** * Make a symbolic expressiontype with types from * <code>types[0..types.size()-1]</code>. <code>types</code> may * have any number of elements. @@ -379,68 +358,6 @@ class CVC4_PUBLIC ExprManager { /** Make the type of sequence with the given parameterization. */ SequenceType mkSequenceType(Type elementType) const; - /** Bits for use in mkDatatypeType() flags. - * - * DATATYPE_FLAG_PLACEHOLDER indicates that the type should not be printed - * out as a definition, for example, in models or during dumping. - */ - enum - { - DATATYPE_FLAG_NONE = 0, - DATATYPE_FLAG_PLACEHOLDER = 1 - }; /* enum */ - - /** Make a type representing the given datatype. */ - DatatypeType mkDatatypeType(Datatype& datatype, - uint32_t flags = DATATYPE_FLAG_NONE); - - /** - * Make a set of types representing the given datatypes, which may be - * mutually recursive. - */ - std::vector<DatatypeType> mkMutualDatatypeTypes( - std::vector<Datatype>& datatypes, uint32_t flags = DATATYPE_FLAG_NONE); - - /** - * Make a set of types representing the given datatypes, which may - * be mutually recursive. unresolvedTypes is a set of SortTypes - * that were used as placeholders in the Datatypes for the Datatypes - * of the same name. This is just a more complicated version of the - * above mkMutualDatatypeTypes() function, but is required to handle - * complex types. - * - * For example, unresolvedTypes might contain the single sort "list" - * (with that name reported from SortType::getName()). The - * datatypes list might have the single datatype - * - * DATATYPE - * list = cons(car:ARRAY INT OF list, cdr:list) | nil; - * END; - * - * To represent the Type of the array, the user had to create a - * placeholder type (an uninterpreted sort) to stand for "list" in - * the type of "car". It is this placeholder sort that should be - * passed in unresolvedTypes. If the datatype was of the simpler - * form: - * - * DATATYPE - * list = cons(car:list, cdr:list) | nil; - * END; - * - * then no complicated Type needs to be created, and the above, - * simpler form of mkMutualDatatypeTypes() is enough. - */ - std::vector<DatatypeType> mkMutualDatatypeTypes( - std::vector<Datatype>& datatypes, - std::set<Type>& unresolvedTypes, - uint32_t flags = DATATYPE_FLAG_NONE); - - /** Make a type representing a selector with the given parameterization. */ - SelectorType mkSelectorType(Type domain, Type range) const; - - /** Make a type representing a tester with the given parameterization. */ - TesterType mkTesterType(Type domain) const; - /** Bits for use in mkSort() flags. */ enum { SORT_FLAG_NONE = 0, @@ -573,13 +490,6 @@ class CVC4_PUBLIC ExprManager { * maximal arity as the maximal possible number of children of a node. **/ static bool isNAryKind(Kind fun); - - /** - * Return the datatype at the given index owned by this class. Type nodes are - * associated with datatypes through the DatatypeIndexConstant class. The - * argument index is intended to be a value taken from that class. - */ - const Datatype& getDatatypeForIndex(unsigned index) const; };/* class ExprManager */ ${mkConst_instantiations} |