diff options
Diffstat (limited to 'src/expr/type.cpp')
-rw-r--r-- | src/expr/type.cpp | 191 |
1 files changed, 127 insertions, 64 deletions
diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 43325d6cc..05b69f6f4 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -11,21 +11,25 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Implementation of expression types . + ** \brief Implementation of expression types ** - ** Implementation of expression types + ** Implementation of expression types. **/ +#include <iostream> #include <string> +#include <vector> #include "expr/node_manager.h" #include "expr/type.h" #include "expr/type_node.h" #include "util/Assert.h" +using namespace std; + namespace CVC4 { -std::ostream& operator<<(std::ostream& out, const Type& e) { +ostream& operator<<(ostream& out, const Type& e) { e.toStream(out); return out; } @@ -34,8 +38,8 @@ Type Type::makeType(const TypeNode& typeNode) const { return Type(d_nodeManager, new TypeNode(typeNode)); } -Type::Type(NodeManager* nm, TypeNode* node) -: d_typeNode(node), +Type::Type(NodeManager* nm, TypeNode* node) : + d_typeNode(node), d_nodeManager(nm) { } @@ -44,22 +48,20 @@ Type::~Type() { delete d_typeNode; } -Type::Type() -: d_typeNode(new TypeNode()), - d_nodeManager(NULL) -{ +Type::Type() : + d_typeNode(new TypeNode), + d_nodeManager(NULL) { } -Type::Type(uintptr_t n) -: d_typeNode(new TypeNode()), +Type::Type(uintptr_t n) : + d_typeNode(new TypeNode), d_nodeManager(NULL) { AlwaysAssert(n == 0); } -Type::Type(const Type& t) -: d_typeNode(new TypeNode(*t.d_typeNode)), - d_nodeManager(t.d_nodeManager) -{ +Type::Type(const Type& t) : + d_typeNode(new TypeNode(*t.d_typeNode)), + d_nodeManager(t.d_nodeManager) { } bool Type::isNull() const { @@ -68,7 +70,7 @@ bool Type::isNull() const { Type& Type::operator=(const Type& t) { NodeManagerScope nms(d_nodeManager); - if (this != &t) { + if(this != &t) { *d_typeNode = *t.d_typeNode; d_nodeManager = t.d_nodeManager; } @@ -83,7 +85,36 @@ bool Type::operator!=(const Type& t) const { return *d_typeNode != *t.d_typeNode; } -void Type::toStream(std::ostream& out) const { +Type Type::substitute(const Type& type, const Type& replacement) const { + NodeManagerScope nms(d_nodeManager); + return makeType(d_typeNode->substitute(*type.d_typeNode, + *replacement.d_typeNode)); +} + +Type Type::substitute(const vector<Type>& types, + const vector<Type>& replacements) const { + NodeManagerScope nms(d_nodeManager); + + vector<TypeNode> typesNodes, replacementsNodes; + + for(vector<Type>::const_iterator i = types.begin(), + iend = types.end(); + i != iend; + ++i) { + typesNodes.push_back(*(*i).d_typeNode); + } + + for(vector<Type>::const_iterator i = replacements.begin(), + iend = replacements.end(); + i != iend; + ++i) { + replacementsNodes.push_back(*(*i).d_typeNode); + } + + return makeType(d_typeNode->substitute(typesNodes, replacementsNodes)); +} + +void Type::toStream(ostream& out) const { NodeManagerScope nms(d_nodeManager); out << *d_typeNode; return; @@ -96,7 +127,7 @@ bool Type::isBoolean() const { } /** Cast to a Boolean type */ -Type::operator BooleanType() const throw (AssertionException) { +Type::operator BooleanType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isBoolean()); return BooleanType(*this); @@ -109,7 +140,7 @@ bool Type::isInteger() const { } /** Cast to a integer type */ -Type::operator IntegerType() const throw (AssertionException) { +Type::operator IntegerType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isInteger()); return IntegerType(*this); @@ -122,7 +153,7 @@ bool Type::isReal() const { } /** Cast to a real type */ -Type::operator RealType() const throw (AssertionException) { +Type::operator RealType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isReal()); return RealType(*this); @@ -135,7 +166,7 @@ bool Type::isBitVector() const { } /** Cast to a bit-vector type */ -Type::operator BitVectorType() const throw (AssertionException) { +Type::operator BitVectorType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isBitVector()); return BitVectorType(*this); @@ -157,7 +188,7 @@ bool Type::isPredicate() const { } /** Cast to a function type */ -Type::operator FunctionType() const throw (AssertionException) { +Type::operator FunctionType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isFunction()); return FunctionType(*this); @@ -170,7 +201,7 @@ bool Type::isTuple() const { } /** Cast to a tuple type */ -Type::operator TupleType() const throw (AssertionException) { +Type::operator TupleType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isTuple()); return TupleType(*this); @@ -183,7 +214,7 @@ bool Type::isArray() const { } /** Cast to an array type */ -Type::operator ArrayType() const throw (AssertionException) { +Type::operator ArrayType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); return ArrayType(*this); } @@ -195,12 +226,25 @@ bool Type::isSort() const { } /** Cast to a sort type */ -Type::operator SortType() const throw (AssertionException) { +Type::operator SortType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isSort()); return SortType(*this); } +/** Is this a sort constructor kind */ +bool Type::isSortConstructor() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isSortConstructor(); +} + +/** Cast to a sort type */ +Type::operator SortConstructorType() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isSortConstructor()); + return SortConstructorType(*this); +} + /** Is this a kind type (i.e., the type of a type)? */ bool Type::isKind() const { NodeManagerScope nms(d_nodeManager); @@ -208,18 +252,18 @@ bool Type::isKind() const { } /** Cast to a kind type */ -Type::operator KindType() const throw (AssertionException) { +Type::operator KindType() const throw(AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isKind()); return KindType(*this); } -std::vector<Type> FunctionType::getArgTypes() const { +vector<Type> FunctionType::getArgTypes() const { NodeManagerScope nms(d_nodeManager); - std::vector<Type> args; - std::vector<TypeNode> argNodes = d_typeNode->getArgTypes(); - std::vector<TypeNode>::iterator it = argNodes.begin(); - std::vector<TypeNode>::iterator it_end = argNodes.end(); + vector<Type> args; + vector<TypeNode> argNodes = d_typeNode->getArgTypes(); + vector<TypeNode>::iterator it = argNodes.begin(); + vector<TypeNode>::iterator it_end = argNodes.end(); for(; it != it_end; ++ it) { args.push_back(makeType(*it)); } @@ -232,77 +276,96 @@ Type FunctionType::getRangeType() const { return makeType(d_typeNode->getRangeType()); } -std::vector<Type> TupleType::getTypes() const { +vector<Type> TupleType::getTypes() const { NodeManagerScope nms(d_nodeManager); - std::vector<Type> types; - std::vector<TypeNode> typeNodes = d_typeNode->getTupleTypes(); - std::vector<TypeNode>::iterator it = typeNodes.begin(); - std::vector<TypeNode>::iterator it_end = typeNodes.end(); + vector<Type> types; + vector<TypeNode> typeNodes = d_typeNode->getTupleTypes(); + vector<TypeNode>::iterator it = typeNodes.begin(); + vector<TypeNode>::iterator it_end = typeNodes.end(); for(; it != it_end; ++ it) { types.push_back(makeType(*it)); } return types; } -std::string SortType::getName() const { +string SortType::getName() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->getAttribute(expr::VarNameAttr()); } -BooleanType::BooleanType(const Type& t) throw (AssertionException) -: Type(t) -{ +string SortConstructorType::getName() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getAttribute(expr::VarNameAttr()); +} + +size_t SortConstructorType::getArity() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->getAttribute(expr::SortArityAttr()); +} + +SortType SortConstructorType::instantiate(const vector<Type>& params) const { + NodeManagerScope nms(d_nodeManager); + vector<TypeNode> paramsNodes; + for(vector<Type>::const_iterator i = params.begin(), + iend = params.end(); + i != iend; + ++i) { + paramsNodes.push_back(*getTypeNode(*i)); + } + return SortType(makeType(d_nodeManager->mkSort(*d_typeNode, paramsNodes))); +} + +BooleanType::BooleanType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isBoolean()); } -IntegerType::IntegerType(const Type& t) throw (AssertionException) -: Type(t) -{ +IntegerType::IntegerType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isInteger()); } -RealType::RealType(const Type& t) throw (AssertionException) -: Type(t) -{ +RealType::RealType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isReal()); } -BitVectorType::BitVectorType(const Type& t) throw (AssertionException) -: Type(t) -{ +BitVectorType::BitVectorType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isBitVector()); } -FunctionType::FunctionType(const Type& t) throw (AssertionException) -: Type(t) -{ +FunctionType::FunctionType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isFunction()); } -TupleType::TupleType(const Type& t) throw (AssertionException) -: Type(t) -{ +TupleType::TupleType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isTuple()); } -ArrayType::ArrayType(const Type& t) throw (AssertionException) -: Type(t) -{ +ArrayType::ArrayType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isArray()); } -KindType::KindType(const Type& t) throw (AssertionException) -: Type(t) -{ +KindType::KindType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isKind()); } -SortType::SortType(const Type& t) throw (AssertionException) -: Type(t) -{ +SortType::SortType(const Type& t) throw(AssertionException) : + Type(t) { Assert(isSort()); } +SortConstructorType::SortConstructorType(const Type& t) + throw(AssertionException) : + Type(t) { + Assert(isSortConstructor()); +} + unsigned BitVectorType::getSize() const { return d_typeNode->getBitVectorSize(); } |