diff options
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 64 |
1 files changed, 37 insertions, 27 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 6d8497a60..525f8ead3 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -645,46 +645,52 @@ SetType ExprManager::mkSetType(Type elementType) const { return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode)))); } -DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) { +DatatypeType ExprManager::mkDatatypeType(Datatype*& datatype) { // Not worth a special implementation; this doesn't need to be fast // code anyway. - vector<Datatype> datatypes; + vector<Datatype*> datatypes; datatypes.push_back(datatype); - vector<DatatypeType> result = mkMutualDatatypeTypes(datatypes); + std::vector<DatatypeType> result; + mkMutualDatatypeTypes(datatypes, result); Assert(result.size() == 1); return result.front(); } -std::vector<DatatypeType> -ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { - return mkMutualDatatypeTypes(datatypes, set<Type>()); +void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::vector<DatatypeType>& dtts) { + std::set<Type> unresolvedTypes; + return mkMutualDatatypeTypes(datatypes, unresolvedTypes, dtts); } -std::vector<DatatypeType> -ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, - const std::set<Type>& unresolvedTypes) { +void ExprManager::mkMutualDatatypeTypes(std::vector<Datatype*>& datatypes, std::set<Type>& unresolvedTypes, std::vector<DatatypeType>& dtts) { NodeManagerScope nms(d_nodeManager); std::map<std::string, DatatypeType> nameResolutions; - std::vector<DatatypeType> dtts; + Trace("ajr-temp") << "Build datatypes..." << std::endl; + //std::vector< Datatype* > dt_copies; + //for(std::vector<Datatype*>::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) { + // dt_copies.push_back( new Datatype( **i ) ); + //} + + // 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(std::vector<Datatype>::const_iterator i = datatypes.begin(), - i_end = datatypes.end(); - i != i_end; - ++i) { + for(std::vector<Datatype*>::iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; ++i) { TypeNode* typeNode; - if( (*i).getNumParameters() == 0 ) { - typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i)); + if( (*i)->getNumParameters() == 0 ) { + unsigned index = d_nodeManager->registerDatatype( *i ); + typeNode = new TypeNode(d_nodeManager->mkTypeConst(DatatypeIndexConstant(index))); + //typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i)); } else { - TypeNode cons = d_nodeManager->mkTypeConst(*i); + unsigned index = d_nodeManager->registerDatatype( *i ); + TypeNode cons = d_nodeManager->mkTypeConst(DatatypeIndexConstant(index)); + //TypeNode cons = d_nodeManager->mkTypeConst(*i); std::vector< TypeNode > params; params.push_back( cons ); - for( unsigned int ip = 0; ip < (*i).getNumParameters(); ++ip ) { - params.push_back( TypeNode::fromType( (*i).getParameter( ip ) ) ); + for( unsigned int ip = 0; ip < (*i)->getNumParameters(); ++ip ) { + params.push_back( TypeNode::fromType( (*i)->getParameter( ip ) ) ); } typeNode = new TypeNode(d_nodeManager->mkTypeNode(kind::PARAMETRIC_DATATYPE, params)); @@ -692,15 +698,19 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, Type type(d_nodeManager, typeNode); DatatypeType dtt(type); PrettyCheckArgument( - nameResolutions.find((*i).getName()) == nameResolutions.end(), + nameResolutions.find((*i)->getName()) == nameResolutions.end(), datatypes, "cannot construct two datatypes at the same time " "with the same name `%s'", - (*i).getName().c_str()); - nameResolutions.insert(std::make_pair((*i).getName(), dtt)); + (*i)->getName().c_str()); + nameResolutions.insert(std::make_pair((*i)->getName(), dtt)); dtts.push_back(dtt); + //d_keep_dtt.push_back(dtt); + //d_keep_dt.push_back(*i); + //Assert( dtt.getDatatype()==(*i) ); } + Trace("ajr-temp") << "Set up map..." << std::endl; // 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 @@ -714,10 +724,7 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, std::vector< DatatypeType > paramReplacements; std::vector<Type> placeholders;// to hold the "unresolved placeholders" std::vector<Type> replacements;// to hold our final, resolved types - for(std::set<Type>::const_iterator i = unresolvedTypes.begin(), - i_end = unresolvedTypes.end(); - i != i_end; - ++i) { + for(std::set<Type>::iterator i = unresolvedTypes.begin(), i_end = unresolvedTypes.end(); i != i_end; ++i) { std::string name; if( (*i).isSort() ) { name = SortType(*i).getName(); @@ -746,12 +753,14 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, } } + Trace("ajr-temp") << "Resolve..." << std::endl; // Lastly, perform the final resolutions and checks. for(std::vector<DatatypeType>::iterator i = dtts.begin(), i_end = dtts.end(); i != i_end; ++i) { const Datatype& dt = (*i).getDatatype(); + Trace("ajr-temp") << "Resolve " << dt.getName() << std::endl; if(!dt.isResolved()) { const_cast<Datatype&>(dt).resolve(this, nameResolutions, placeholders, replacements, @@ -763,11 +772,12 @@ ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes, checkResolvedDatatype(*i); } + Trace("ajr-temp") << "Notify..." << std::endl; for(std::vector<NodeManagerListener*>::iterator i = d_nodeManager->d_listeners.begin(); i != d_nodeManager->d_listeners.end(); ++i) { (*i)->nmNotifyNewDatatypes(dtts); } - return dtts; + Trace("ajr-temp") << "Finish..." << std::endl; } void ExprManager::checkResolvedDatatype(DatatypeType dtt) const { |