summaryrefslogtreecommitdiff
path: root/src/expr/type.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/type.cpp')
-rw-r--r--src/expr/type.cpp191
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();
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback