diff options
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 65 |
1 files changed, 62 insertions, 3 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 6e8b6c63c..21fc0a4a1 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -2,10 +2,10 @@ /*! \file expr_manager_template.cpp ** \verbatim ** Original author: dejan - ** Major contributors: mdeters, cconway + ** Major contributors: cconway, mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -22,13 +22,15 @@ #include "util/options.h" #include "util/stats.h" +#include <map> + ${includes} // This is a hack, but an important one: if there's an error, the // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 32 "${template}" +#line 34 "${template}" #ifdef CVC4_STATISTICS_ON #define INC_STAT(kind) \ @@ -340,6 +342,63 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const { return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode)))); } +DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) { + NodeManagerScope nms(d_nodeManager); + TypeNode* typeNode = new TypeNode(d_nodeManager->mkTypeConst(datatype)); + Type type(d_nodeManager, typeNode); + DatatypeType dtt(type); + const Datatype& dt = typeNode->getConst<Datatype>(); + if(!dt.isResolved()) { + std::map<std::string, DatatypeType> resolutions; + resolutions.insert(std::make_pair(datatype.getName(), dtt)); + const_cast<Datatype&>(dt).resolve(this, resolutions); + } + return dtt; +} + +std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { + NodeManagerScope nms(d_nodeManager); + std::map<std::string, DatatypeType> resolutions; + std::vector<DatatypeType> dtts; + for(std::vector<Datatype>::const_iterator i = datatypes.begin(), i_end = datatypes.end(); + i != i_end; + ++i) { + TypeNode* typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i)); + Type type(d_nodeManager, typeNode); + DatatypeType dtt(type); + CheckArgument(resolutions.find((*i).getName()) == resolutions.end(), + datatypes, + "cannot construct two datatypes at the same time with the same name `%s'", + (*i).getName().c_str()); + resolutions.insert(std::make_pair((*i).getName(), dtt)); + dtts.push_back(dtt); + } + for(std::vector<DatatypeType>::iterator i = dtts.begin(), i_end = dtts.end(); + i != i_end; + ++i) { + const Datatype& dt = (*i).getDatatype(); + if(!dt.isResolved()) { + const_cast<Datatype&>(dt).resolve(this, resolutions); + } + } + return dtts; +} + +ConstructorType ExprManager::mkConstructorType(const Datatype::Constructor& 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))); +} + +TesterType ExprManager::mkTesterType(Type domain) const { + NodeManagerScope nms(d_nodeManager); + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTesterType(*domain.d_typeNode))); +} + SortType ExprManager::mkSort(const std::string& name) const { NodeManagerScope nms(d_nodeManager); return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name)))); |