diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/dtype.cpp | 10 | ||||
-rw-r--r-- | src/expr/dtype.h | 8 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 11 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 5 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 154 | ||||
-rw-r--r-- | src/expr/node_manager.h | 75 |
6 files changed, 219 insertions, 44 deletions
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 220e12c42..91ae9d158 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -25,6 +25,7 @@ DType::DType(std::string name, bool isCo) d_params(), d_isCo(isCo), d_isTuple(false), + d_isRecord(false), d_constructors(), d_resolved(false), d_self(), @@ -43,6 +44,7 @@ DType::DType(std::string name, const std::vector<TypeNode>& params, bool isCo) d_params(params), d_isCo(isCo), d_isTuple(false), + d_isRecord(false), d_constructors(), d_resolved(false), d_self(), @@ -82,6 +84,8 @@ bool DType::isSygus() const { return !d_sygusType.isNull(); } bool DType::isTuple() const { return d_isTuple; } +bool DType::isRecord() const { return d_isRecord; } + bool DType::isResolved() const { return d_resolved; } const DType& DType::datatypeOf(Node item) @@ -231,6 +235,12 @@ void DType::setTuple() d_isTuple = true; } +void DType::setRecord() +{ + Assert(!d_resolved); + d_isRecord = true; +} + Cardinality DType::getCardinality(TypeNode t) const { Trace("datatypes-init") << "DType::getCardinality " << std::endl; diff --git a/src/expr/dtype.h b/src/expr/dtype.h index fea51cd36..1682614d0 100644 --- a/src/expr/dtype.h +++ b/src/expr/dtype.h @@ -216,6 +216,9 @@ class DType /** set that this datatype is a tuple */ void setTuple(); + /** set that this datatype is a record */ + void setRecord(); + /** Get the name of this DType. */ std::string getName() const; @@ -243,6 +246,9 @@ class DType /** is this a tuple datatype? */ bool isTuple() const; + /** is this a record datatype? */ + bool isRecord() const; + /** * Return the cardinality of this datatype. * The DType must be resolved. @@ -553,6 +559,8 @@ class DType bool d_isCo; /** whether the datatype is a tuple */ bool d_isTuple; + /** whether the datatype is a record */ + bool d_isRecord; /** the constructors of this datatype */ std::vector<std::shared_ptr<DTypeConstructor> > d_constructors; /** whether this datatype has been resolved */ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 445ca9ee7..66824c07a 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -690,7 +690,7 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes( for(std::vector<Datatype*>::iterator i = dt_copies.begin(), i_end = dt_copies.end(); i != i_end; ++i) { TypeNode* typeNode; // register datatype with the node manager - unsigned index = d_nodeManager->registerDatatype((*i)->d_internal); + size_t index = d_nodeManager->registerDatatype((*i)->d_internal); if( (*i)->getNumParameters() == 0 ) { typeNode = new TypeNode(d_nodeManager->mkTypeConst(DatatypeIndexConstant(index))); //typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i)); @@ -760,6 +760,7 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes( } // Lastly, perform the final resolutions and checks. + std::vector<TypeNode> tns; for(std::vector<DatatypeType>::iterator i = dtts.begin(), i_end = dtts.end(); i != i_end; @@ -776,10 +777,11 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes( // Now run some checks, including a check to make sure that no // selector is function-valued. checkResolvedDatatype(*i); + tns.push_back(TypeNode::fromType(*i)); } for(std::vector<NodeManagerListener*>::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) { - (*i)->nmNotifyNewDatatypes(dtts, flags); + (*i)->nmNotifyNewDatatypes(tns, flags); } return dtts; @@ -825,11 +827,6 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const { } } -ConstructorType ExprManager::mkConstructorType(const DatatypeConstructor& constructor, Type range) const { - NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode))); -} - SelectorType ExprManager::mkSelectorType(Type domain, Type range) const { NodeManagerScope nms(d_nodeManager); return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSelectorType(*domain.d_typeNode, *range.d_typeNode))); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 3f180e951..2b9a85aca 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -435,11 +435,6 @@ class CVC4_PUBLIC ExprManager { std::set<Type>& unresolvedTypes, uint32_t flags = DATATYPE_FLAG_NONE); - /** - * Make a type representing a constructor with the given parameterization. - */ - ConstructorType mkConstructorType(const DatatypeConstructor& constructor, Type range) const; - /** Make a type representing a selector with the given parameterization. */ SelectorType mkSelectorType(Type domain, Type range) const; diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index e9f56bf3f..c72de9564 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -149,6 +149,8 @@ NodeManager::~NodeManager() { d_rt_cache.d_children.clear(); d_rt_cache.d_data = dummy; + d_registeredDTypes.clear(); + // clear the datatypes d_ownedDTypes.clear(); Assert(!d_attrManager->inGarbageCollection()); @@ -198,15 +200,15 @@ NodeManager::~NodeManager() { size_t NodeManager::registerDatatype(std::shared_ptr<DType> dt) { - size_t sz = d_ownedDTypes.size(); - d_ownedDTypes.push_back(dt); + size_t sz = d_registeredDTypes.size(); + d_registeredDTypes.push_back(dt); return sz; } -const DType& NodeManager::getDTypeForIndex(unsigned index) const +const DType& NodeManager::getDTypeForIndex(size_t index) const { - Assert(index < d_ownedDTypes.size()); - return *d_ownedDTypes[index]; + Assert(index < d_registeredDTypes.size()); + return *d_registeredDTypes[index]; } void NodeManager::reclaimZombies() { @@ -462,28 +464,132 @@ TypeNode NodeManager::mkSequenceType(TypeNode elementType) return mkTypeNode(kind::SEQUENCE_TYPE, elementType); } -TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor, - TypeNode range) { - vector<TypeNode> sorts; - Debug("datatypes") << "ctor name: " << constructor.getName() << endl; - for(DatatypeConstructor::const_iterator i = constructor.begin(); - i != constructor.end(); - ++i) { - TypeNode selectorType = *(*i).getSelector().getType().d_typeNode; - Debug("datatypes") << selectorType << endl; - TypeNode sort = selectorType[1]; +TypeNode NodeManager::mkDatatypeType(DType& datatype, uint32_t flags) +{ + // Not worth a special implementation; this doesn't need to be fast + // code anyway. + std::vector<DType> datatypes; + datatypes.push_back(datatype); + std::vector<TypeNode> result = mkMutualDatatypeTypes(datatypes, flags); + Assert(result.size() == 1); + return result.front(); +} + +std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes( + const std::vector<DType>& datatypes, uint32_t flags) +{ + std::set<TypeNode> unresolvedTypes; + return mkMutualDatatypeTypes(datatypes, unresolvedTypes, flags); +} - // should be guaranteed here already, but just in case - Assert(!sort.isFunctionLike()); +std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes( + const std::vector<DType>& datatypes, + const std::set<TypeNode>& unresolvedTypes, + uint32_t flags) +{ + NodeManagerScope nms(this); + std::map<std::string, TypeNode> nameResolutions; + std::vector<TypeNode> dtts; - Debug("datatypes") << "ctor sort: " << sort << endl; - sorts.push_back(sort); + // have to build deep copy so that datatypes will live in this class + std::vector<std::shared_ptr<DType> > dt_copies; + for (const DType& dt : datatypes) + { + d_ownedDTypes.push_back(std::unique_ptr<DType>(new DType(dt))); + dt_copies.push_back(std::move(d_ownedDTypes.back())); } - Debug("datatypes") << "ctor range: " << range << endl; - PrettyCheckArgument(!range.isFunctionLike(), range, - "cannot create higher-order function types"); - sorts.push_back(range); - return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts); + + // First do some sanity checks, set up the final Type to be used for + // each datatype, and set up the "named resolutions" used to handle + // simple self- and mutual-recursion, for example in the definition + // "nat = succ(pred:nat) | zero", a named resolution can handle the + // pred selector. + for (const std::shared_ptr<DType>& dtc : dt_copies) + { + TypeNode typeNode; + // register datatype with the node manager + size_t index = registerDatatype(dtc); + if (dtc->getNumParameters() == 0) + { + typeNode = mkTypeConst(DatatypeIndexConstant(index)); + } + else + { + TypeNode cons = mkTypeConst(DatatypeIndexConstant(index)); + std::vector<TypeNode> params; + params.push_back(cons); + for (unsigned int ip = 0; ip < dtc->getNumParameters(); ++ip) + { + params.push_back(dtc->getParameter(ip)); + } + + typeNode = mkTypeNode(kind::PARAMETRIC_DATATYPE, params); + } + AlwaysAssert(nameResolutions.find(dtc->getName()) == nameResolutions.end()) + << "cannot construct two datatypes at the same time " + "with the same name"; + nameResolutions.insert(std::make_pair(dtc->getName(), typeNode)); + dtts.push_back(typeNode); + } + + // Second, set up the type substitution map for complex type + // resolution (e.g. if "list" is the type we're defining, and it has + // a selector of type "ARRAY INT OF list", this can't be taken care + // of using the named resolutions that we set up above. A + // preliminary array type was set up, and now needs to have "list" + // substituted in it for the correct type. + // + // @TODO get rid of named resolutions altogether and handle + // everything with these resolutions? + std::vector<TypeNode> paramTypes; + std::vector<TypeNode> paramReplacements; + std::vector<TypeNode> placeholders; // to hold the "unresolved placeholders" + std::vector<TypeNode> replacements; // to hold our final, resolved types + for (const TypeNode& ut : unresolvedTypes) + { + std::string name = ut.getAttribute(expr::VarNameAttr()); + std::map<std::string, TypeNode>::const_iterator resolver = + nameResolutions.find(name); + AlwaysAssert(resolver != nameResolutions.end()) + << "cannot resolve type " + name + + "; it's not among the datatypes being defined"; + // We will instruct the Datatype to substitute "ut" (the + // unresolved SortType used as a placeholder in complex types) + // with "(*resolver).second" (the TypeNode we created in the + // first step, above). + if (ut.isSort()) + { + placeholders.push_back(ut); + replacements.push_back((*resolver).second); + } + else + { + Assert(ut.isSortConstructor()); + paramTypes.push_back(ut); + paramReplacements.push_back((*resolver).second); + } + } + + // Lastly, perform the final resolutions and checks. + for (const TypeNode& ut : dtts) + { + const DType& dt = ut.getDType(); + if (!dt.isResolved()) + { + const_cast<DType&>(dt).resolve(nameResolutions, + placeholders, + replacements, + paramTypes, + paramReplacements); + } + } + + for (NodeManagerListener* nml : d_listeners) + { + nml->nmNotifyNewDatatypes(dtts, flags); + } + + return dtts; } TypeNode NodeManager::mkConstructorType(const std::vector<TypeNode>& args, diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 84c4b44e0..cfe771ca5 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -66,7 +66,7 @@ class NodeManagerListener { virtual void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) {} virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort, uint32_t flags) {} - virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes, + virtual void nmNotifyNewDatatypes(const std::vector<TypeNode>& datatypes, uint32_t flags) { } @@ -172,8 +172,12 @@ class NodeManager { */ std::vector<NodeManagerListener*> d_listeners; - /** A list of datatypes owned by this node manager. */ - std::vector<std::shared_ptr<DType> > d_ownedDTypes; + /** A list of datatypes registered by its corresponding expr manager. + * !!! this member should be deleted when the Expr-layer is deleted. + */ + std::vector<std::shared_ptr<DType> > d_registeredDTypes; + /** A list of datatypes owned by this node manager */ + std::vector<std::unique_ptr<DType> > d_ownedDTypes; /** * A map of tuple and record types to their corresponding datatype. @@ -407,8 +411,10 @@ public: Assert(elt != d_listeners.end()) << "listener not subscribed"; d_listeners.erase(elt); } - - /** register datatype */ + + /** register that datatype dt was constructed by the expression manager + * !!! this interface should be deleted when the Expr-layer is deleted. + */ size_t registerDatatype(std::shared_ptr<DType> dt); /** * Return the datatype at the given index owned by this class. Type nodes are @@ -420,7 +426,7 @@ public: * would lead to memory leaks. Thus TypeNode are given a DatatypeIndexConstant * which is used as an index to retrieve the DType via this call. */ - const DType& getDTypeForIndex(unsigned index) const; + const DType& getDTypeForIndex(size_t index) const; /** Get a Kind from an operator expression */ static inline Kind operatorToKind(TNode n); @@ -878,8 +884,61 @@ public: /** Make the type of sequences with the given parameterization */ TypeNode mkSequenceType(TypeNode elementType); - /** Make a type representing a constructor with the given parameterization */ - TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range); + /** 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. */ + TypeNode mkDatatypeType(DType& datatype, uint32_t flags = DATATYPE_FLAG_NONE); + + /** + * Make a set of types representing the given datatypes, which may be + * mutually recursive. + */ + std::vector<TypeNode> mkMutualDatatypeTypes( + const std::vector<DType>& 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<TypeNode> mkMutualDatatypeTypes( + const std::vector<DType>& datatypes, + const std::set<TypeNode>& unresolvedTypes, + uint32_t flags = DATATYPE_FLAG_NONE); + /** * Make a type representing a constructor with the given argument (subfield) * types and return type range. |