From: Dejan Jovanović Date: Mon, 26 Apr 2010 23:16:18 +0000 (+0000) Subject: Some cleanup. Also added the integer and real types. X-Git-Tag: cvc5-1.0.0~9108 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0320f444cd5fc1c1abf28ac1131d2fcde0fc5c06;p=cvc5.git Some cleanup. Also added the integer and real types. --- diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index cbfcdd110..39c1c91b9 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -311,10 +311,6 @@ public: template 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& children); @@ -446,9 +442,15 @@ public: 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(); @@ -607,6 +609,16 @@ inline TypeNode NodeManager::booleanType() { return TypeNode(mkTypeConst(BOOLEAN_TYPE)); } +/** Get the (singleton) type for integers. */ +inline TypeNode NodeManager::integerType() { + return TypeNode(mkTypeConst(INTEGER_TYPE)); +} + +/** Get the (singleton) type for reals. */ +inline TypeNode NodeManager::realType() { + return TypeNode(mkTypeConst(REAL_TYPE)); +} + /** Get the (singleton) type for sorts. */ inline TypeNode NodeManager::kindType() { return TypeNode(mkTypeConst(KIND_TYPE)); @@ -648,14 +660,6 @@ NodeManager::mkPredicateType(const std::vector& sorts) { 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); @@ -749,6 +753,17 @@ inline bool NodeManager::hasOperator(Kind k) { } } +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); } @@ -854,17 +869,6 @@ inline Node NodeManager::mkVar(const TypeNode& type) { 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); diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 98a7e88e7..c76349fe3 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -84,13 +84,8 @@ bool Type::operator!=(const Type& t) const { 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? */ @@ -100,12 +95,38 @@ bool Type::isBoolean() const { } /** 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); @@ -120,7 +141,7 @@ bool Type::isPredicate() const { } /** Cast to a function type */ -Type::operator FunctionType() const { +Type::operator FunctionType() const throw (AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isFunction()); return FunctionType(*this); @@ -133,7 +154,7 @@ bool Type::isSort() const { } /** Cast to a sort type */ -Type::operator SortType() const { +Type::operator SortType() const throw (AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isSort()); return SortType(*this); @@ -146,7 +167,7 @@ bool Type::isKind() const { } /** Cast to a kind type */ -Type::operator KindType() const { +Type::operator KindType() const throw (AssertionException) { NodeManagerScope nms(d_nodeManager); Assert(isKind()); return KindType(*this); @@ -170,45 +191,46 @@ Type FunctionType::getRangeType() const { 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 */ diff --git a/src/expr/type.h b/src/expr/type.h index 5cbe0613a..c61b67f77 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -1,7 +1,7 @@ /********************* */ /** 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) @@ -32,6 +32,8 @@ class NodeManager; class TypeNode; class BooleanType; +class IntegerType; +class RealType; class FunctionType; class KindType; class SortType; @@ -52,14 +54,16 @@ protected: 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); @@ -79,71 +83,159 @@ public: /** 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. */ @@ -152,20 +244,13 @@ class CVC4_PUBLIC FunctionType : public Type { public: /** Construct from the base type */ - FunctionType(const Type& type); + FunctionType(const Type& type) throw (AssertionException); /** Get the argument types */ std::vector 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; - }; /** @@ -176,13 +261,10 @@ class CVC4_PUBLIC SortType : public Type { 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; }; /** @@ -193,11 +275,7 @@ class CVC4_PUBLIC KindType : public Type { 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); }; /** diff --git a/src/expr/type_constant.h b/src/expr/type_constant.h index 86698459b..a847bc827 100644 --- a/src/expr/type_constant.h +++ b/src/expr/type_constant.h @@ -1,26 +1,67 @@ -/* - * 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_ */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 87b6ed58a..08e50844b 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -23,6 +23,14 @@ bool TypeNode::isBoolean() const { return getKind() == kind::TYPE_CONSTANT && getConst() == BOOLEAN_TYPE; } +bool TypeNode::isInteger() const { + return getKind() == kind::TYPE_CONSTANT && getConst() == INTEGER_TYPE; +} + +bool TypeNode::isReal() const { + return getKind() == kind::TYPE_CONSTANT && getConst() == REAL_TYPE; +} + /** Is this a function type? */ bool TypeNode::isFunction() const { return getKind() == kind::FUNCTION_TYPE; diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 7747b93e1..12df5513f 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -38,14 +38,14 @@ class NodeValue; }/* 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; @@ -104,14 +104,6 @@ public: 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 @@ -292,9 +284,23 @@ public: */ 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;