template <class NodeClass, class T>
NodeClass mkConstInternal(const T&);
- /** Create a type-variable */
- TypeNode mkTypeVar();
- TypeNode mkTypeVar(const std::string& name);
-
/** Create a node with no children. */
TypeNode mkTypeNode(Kind kind, const std::vector<TypeNode>& children);
const AttrKind& attr,
const typename AttrKind::value_type& value);
- /** Get the (singleton) type for booleans. */
+ /** Get the (singleton) type for Booleans. */
inline TypeNode booleanType();
+ /** Get the (singleton) type for integers. */
+ inline TypeNode integerType();
+
+ /** Get the (singleton) type for booleans. */
+ inline TypeNode realType();
+
/** Get the (singleton) type for sorts. */
inline TypeNode kindType();
return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE));
}
+/** Get the (singleton) type for integers. */
+inline TypeNode NodeManager::integerType() {
+ return TypeNode(mkTypeConst<TypeConstant>(INTEGER_TYPE));
+}
+
+/** Get the (singleton) type for reals. */
+inline TypeNode NodeManager::realType() {
+ return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE));
+}
+
/** Get the (singleton) type for sorts. */
inline TypeNode NodeManager::kindType() {
return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE));
return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
}
-inline TypeNode NodeManager::mkSort() {
- return mkTypeVar();
-}
-
-inline TypeNode NodeManager::mkSort(const std::string& name) {
- return mkTypeVar(name);
-}
-
inline TypeNode NodeManager::getType(TNode n) {
TypeNode typeNode;
getAttribute(n, TypeAttr(), typeNode);
}
}
+inline TypeNode NodeManager::mkSort() {
+ TypeNode type = NodeBuilder<0>(this, kind::VARIABLE).constructTypeNode();
+ return type;
+}
+
+inline TypeNode NodeManager::mkSort(const std::string& name) {
+ TypeNode type = mkSort();
+ type.setAttribute(expr::VarNameAttr(), name);
+ return type;
+}
+
inline Node NodeManager::mkNode(Kind kind) {
return NodeBuilder<0>(this, kind);
}
return n;
}
-inline TypeNode NodeManager::mkTypeVar(const std::string& name) {
- TypeNode type = mkTypeVar();
- type.setAttribute(expr::VarNameAttr(), name);
- return type;
-}
-
-inline TypeNode NodeManager::mkTypeVar() {
- TypeNode type = NodeBuilder<0>(this, kind::VARIABLE).constructTypeNode();
- return type;
-}
-
inline Node* NodeManager::mkVarPtr(const TypeNode& type) {
Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
n->setAttribute(TypeAttr(), type);
void Type::toStream(std::ostream& out) const {
NodeManagerScope nms(d_nodeManager);
- // Do the cast by hand
- if (isBoolean()) { out << (BooleanType)*this; return; }
- if (isFunction()) { out << (FunctionType)*this; return; }
- if (isKind()) { out << (KindType)*this; return; }
- if (isSort()) { out << (SortType)*this; return; }
- // We should not get here
- Unreachable("Type not implemented completely");
+ out << *d_typeNode;
+ return;
}
/** Is this the Boolean type? */
}
/** Cast to a Boolean type */
-Type::operator BooleanType() const {
+Type::operator BooleanType() const throw (AssertionException) {
NodeManagerScope nms(d_nodeManager);
Assert(isBoolean());
return BooleanType(*this);
}
+/** Is this the integer type? */
+bool Type::isInteger() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->isInteger();
+}
+
+/** Cast to a integer type */
+Type::operator IntegerType() const throw (AssertionException) {
+ NodeManagerScope nms(d_nodeManager);
+ Assert(isInteger());
+ return IntegerType(*this);
+}
+
+/** Is this the real type? */
+bool Type::isReal() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->isInteger();
+}
+
+/** Cast to a integer type */
+Type::operator RealType() const throw (AssertionException) {
+ NodeManagerScope nms(d_nodeManager);
+ Assert(isReal());
+ return RealType(*this);
+}
+
/** Is this a function type? */
bool Type::isFunction() const {
NodeManagerScope nms(d_nodeManager);
}
/** Cast to a function type */
-Type::operator FunctionType() const {
+Type::operator FunctionType() const throw (AssertionException) {
NodeManagerScope nms(d_nodeManager);
Assert(isFunction());
return FunctionType(*this);
}
/** Cast to a sort type */
-Type::operator SortType() const {
+Type::operator SortType() const throw (AssertionException) {
NodeManagerScope nms(d_nodeManager);
Assert(isSort());
return SortType(*this);
}
/** Cast to a kind type */
-Type::operator KindType() const {
+Type::operator KindType() const throw (AssertionException) {
NodeManagerScope nms(d_nodeManager);
Assert(isKind());
return KindType(*this);
return makeType(d_typeNode->getRangeType());
}
-void BooleanType::toStream(std::ostream& out) const {
- out << "BOOLEAN";
-}
-
std::string SortType::getName() const {
NodeManagerScope nms(d_nodeManager);
return d_typeNode->getAttribute(expr::VarNameAttr());
}
-void SortType::toStream(std::ostream& out) const {
- NodeManagerScope nms(d_nodeManager);
- out << getName();
+BooleanType::BooleanType(const Type& t) throw (AssertionException)
+: Type(t)
+{
+ Assert(isBoolean());
}
-void FunctionType::toStream(std::ostream& out) const {
- NodeManagerScope nms(d_nodeManager);
- unsigned arity = d_typeNode->getNumChildren();
+IntegerType::IntegerType(const Type& t) throw (AssertionException)
+: Type(t)
+{
+ Assert(isInteger());
+}
- if(arity > 2) {
- out << "(";
- }
- unsigned int i;
- for(i=0; i < arity - 1; ++i) {
- if(i > 0) {
- out << ",";
- }
- out << makeType((*d_typeNode)[i]);
- }
- if(arity > 2) {
- out << ")";
- }
- out << " -> ";
- (*d_typeNode)[i].toStream(out);
+RealType::RealType(const Type& t) throw (AssertionException)
+: Type(t)
+{
+ Assert(isReal());
}
-BooleanType::BooleanType(const Type& t) : Type(t) {}
-FunctionType::FunctionType(const Type& t) : Type(t) {}
-KindType::KindType(const Type& t) : Type(t) {}
-SortType::SortType(const Type& t) : Type(t) {}
+FunctionType::FunctionType(const Type& t) throw (AssertionException)
+: Type(t)
+{
+ Assert(isFunction());
+}
+
+KindType::KindType(const Type& t) throw (AssertionException)
+: Type(t)
+{
+ Assert(isKind());
+}
+
+SortType::SortType(const Type& t) throw (AssertionException)
+: Type(t)
+{
+ Assert(isSort());
+}
}/* CVC4 namespace */
/********************* */
/** type.h
** Original author: cconway
- ** Major contributors: mdeters
+ ** Major contributors: mdeters, dejan
** 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)
class TypeNode;
class BooleanType;
+class IntegerType;
+class RealType;
class FunctionType;
class KindType;
class SortType;
NodeManager* d_nodeManager;
/**
- * Construct a new type given the typeNode;
+ * Construct a new type given the typeNode, for internal use only.
+ * @param typeNode the TypeNode to use
+ * @return the Type corresponding to the TypeNode
*/
Type makeType(const TypeNode& typeNode) const;
/**
* Constructor for internal purposes.
* @param em the expression manager that handles this expression
- * @param node the actual expression node pointer for this type
+ * @param typeNode the actual TypeNode pointer for this type
*/
Type(NodeManager* em, TypeNode* typeNode);
/** Default constructor */
Type();
- /** Copy constructor */
+ /**
+ * Copy constructor.
+ * @param t the type to make a copy of
+ */
Type(const Type& t);
- /** Check whether this is a null type */
+ /**
+ * Check whether this is a null type
+ * @return true if type is null
+ */
bool isNull() const;
- /** Assignment operator */
+ /**
+ * Assignment operator.
+ * @param t the type to assign to this type
+ * @return this type after assignment.
+ */
Type& operator=(const Type& t);
- /** Comparison for equality */
+ /**
+ * Comparison for structural equality.
+ * @param t the type to compare to
+ * @returns true if the types are equal
+ */
bool operator==(const Type& t) const;
- /** Comparison for disequality */
+ /**
+ * Comparison for structural disequality.
+ * @param t the type to compare to
+ * @returns true if the types are not equal
+ */
bool operator!=(const Type& t) const;
- /** Is this the Boolean type? */
+ /**
+ * Is this the Boolean type?
+ * @return true if the type is a Boolean type
+ */
bool isBoolean() const;
- /** Cast to a Boolean type */
- operator BooleanType() const;
+ /**
+ * Cast this type to a Boolean type
+ * @return the BooleanType
+ */
+ operator BooleanType() const throw (AssertionException);
+
+ /**
+ * Is this the integer type?
+ * @return true if the type is a integer type
+ */
+ bool isInteger() const;
+
+ /**
+ * Cast this type to a integer type
+ * @return the IntegerType
+ */
+ operator IntegerType() const throw (AssertionException);
+
+ /**
+ * Is this the real type?
+ * @return true if the type is a real type
+ */
+ bool isReal() const;
- /** Is this a function type? */
+ /**
+ * Cast this type to a real type
+ * @return the RealType
+ */
+ operator RealType() const throw (AssertionException);
+
+ /**
+ * Is this a function type?
+ * @return true if the type is a Boolean type
+ */
bool isFunction() const;
- /** Is this a predicate type? NOTE: all predicate types are also
- function types. */
+ /**
+ * Is this a predicate type, i.e. if it's a function type mapping to Boolean.
+ * Aall predicate types are also function types.
+ * @return true if the type is a predicate type
+ */
bool isPredicate() const;
- /** Cast to a function type */
- operator FunctionType() const;
+ /**
+ * Cast this type to a function type
+ * @return the FunctionType
+ */
+ operator FunctionType() const throw (AssertionException);
- /** Is this a sort kind */
+ /**
+ * Is this a sort kind?
+ * @return true if this is a sort kind
+ */
bool isSort() const;
- /** Cast to a sort type */
- operator SortType() const;
+ /**
+ * Cast this type to a sort type
+ * @return the function Type
+ */
+ operator SortType() const throw (AssertionException);
- /** Is this a kind type (i.e., the type of a type)? */
+ /**
+ * Is this a kind type (i.e., the type of a type)?
+ * @return true if this is a kind type
+ */
bool isKind() const;
- /** Cast to a kind type */
- operator KindType() const;
-
- /** Outputs a string representation of this type to the stream. */
- virtual void toStream(std::ostream& out) const;
+ /**
+ * Cast to a kind type
+ * @return the kind type
+ */
+ operator KindType() const throw (AssertionException);
+ /**
+ * Outputs a string representation of this type to the stream.
+ * @param out the stream to output to
+ */
+ void toStream(std::ostream& out) const;
};
/**
- * Singleton class encapsulating the boolean type.
+ * Singleton class encapsulating the Boolean type.
*/
class CVC4_PUBLIC BooleanType : public Type {
public:
/** Construct from the base type */
- BooleanType(const Type& type);
+ BooleanType(const Type& type) throw (AssertionException);
+};
- /** Is this the boolean type? (Returns true.) */
- bool isBoolean() const;
+/**
+ * Singleton class encapsulating the integer type.
+ */
+class CVC4_PUBLIC IntegerType : public Type {
- /** Just outputs BOOLEAN */
- void toStream(std::ostream& out) const;
+public:
+
+ /** Construct from the base type */
+ IntegerType(const Type& type) throw (AssertionException);
};
+/**
+ * Singleton class encapsulating the real type.
+ */
+class CVC4_PUBLIC RealType : public Type {
+
+public:
+
+ /** Construct from the base type */
+ RealType(const Type& type) throw (AssertionException);
+};
+
+
/**
* Class encapsulating a function type.
*/
public:
/** Construct from the base type */
- FunctionType(const Type& type);
+ FunctionType(const Type& type) throw (AssertionException);
/** Get the argument types */
std::vector<Type> getArgTypes() const;
/** Get the range type (i.e., the type of the result). */
Type getRangeType() const;
-
- /**
- * Outputs a string representation of this type to the stream,
- * in the format "D -> R" or "(A, B, C) -> R".
- */
- void toStream(std::ostream& out) const;
-
};
/**
public:
/** Construct from the base type */
- SortType(const Type& type);
+ SortType(const Type& type) throw (AssertionException);
/** Get the name of the sort */
std::string getName() const;
-
- /** Outouts the name of the sort */
- void toStream(std::ostream& out) const;
};
/**
public:
/** Construct from the base type */
- KindType(const Type& type);
-
- /** Is this the kind type? (Returns true.) */
- bool isKind() const;
-
+ KindType(const Type& type) throw (AssertionException);
};
/**
-/*
- * type_constant.h
- *
- * Created on: Apr 5, 2010
- * Author: dejan
- */
+/********************* */
+/** type_constant.h
+ ** Original author: dejan
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Interface for expression types
+ **/
#ifndef __CVC4__TYPE_CONSTANT_H_
#define __CVC4__TYPE_CONSTANT_H_
namespace CVC4 {
+/**
+ * The enumeration for the built-in atomic types.
+ */
enum TypeConstant {
+ /** The Boolean type */
BOOLEAN_TYPE,
+ /** The integer type */
+ INTEGER_TYPE,
+ /** The real type */
+ REAL_TYPE,
+ /** The kind type (type of types) */
KIND_TYPE
};
+/**
+ * We hash the constants with their values.
+ */
struct TypeConstantHashStrategy {
static inline size_t hash(TypeConstant tc) {
return tc;
}
};/* struct BoolHashStrategy */
+inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
+
+ switch(typeConstant) {
+ case BOOLEAN_TYPE:
+ out << "BOOLEAN";
+ break;
+ case INTEGER_TYPE:
+ out << "INTEGER";
+ break;
+ case REAL_TYPE:
+ out << "REAL";
+ break;
+ case KIND_TYPE:
+ out << "KIND";
+ break;
+ default:
+ out << "UNKNOWN_TYPE_CONSTANT";
+ break;
+ }
+ return out;
+}
+
}
#endif /* __CVC4__TYPE_CONSTANT_H_ */
return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == BOOLEAN_TYPE;
}
+bool TypeNode::isInteger() const {
+ return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == INTEGER_TYPE;
+}
+
+bool TypeNode::isReal() const {
+ return getKind() == kind::TYPE_CONSTANT && getConst<TypeConstant>() == REAL_TYPE;
+}
+
/** Is this a function type? */
bool TypeNode::isFunction() const {
return getKind() == kind::FUNCTION_TYPE;
}/* CVC4::expr namespace */
/**
- * Encapsulation of an NodeValue pointer. The reference count is
- * maintained in the NodeValue if ref_count is true.
+ * Encapsulation of an NodeValue pointer for Types. The reference count is
+ * maintained in the NodeValue.
*/
class TypeNode {
/**
* The NodeValue has access to the private constructors, so that the
- * iterators can can create new nodes.
+ * iterators can can create new types.
*/
friend class expr::NodeValue;
return s_null;
}
- /**
- * Returns true if this type is a null type.
- * @return true if null
- */
- bool isNull() const {
- return d_nv == &expr::NodeValue::s_null;
- }
-
/**
* Structural comparison operator for expressions.
* @param typeNode the type node to compare to
*/
void printAst(std::ostream & o, int indent = 0) const;
+ /**
+ * Returns true if this type is a null type.
+ * @return true if null
+ */
+ bool isNull() const {
+ return d_nv == &expr::NodeValue::s_null;
+ }
+
/** Is this the Boolean type? */
bool isBoolean() const;
+ /** Is this the Integer type? */
+ bool isInteger() const;
+
+ /** Is this the Real type? */
+ bool isReal() const;
+
/** Is this a function type? */
bool isFunction() const;
projects / cvc5.git / commitdiff