diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-25 15:16:43 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-25 17:39:21 -0500 |
commit | 195dffbb7468e814d3dc3226666688869c13ba3d (patch) | |
tree | 4c4915245a90615ea36cbcfbb4a8a6dcc910c384 /src/expr | |
parent | 73760b3c213733fc98d67f9ceeb74d06b01a3777 (diff) |
Fix errors and reduce warnings on clang (merge from mdeters/clang)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/attribute_internals.h | 2 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 2 | ||||
-rw-r--r-- | src/expr/expr_template.h | 2 | ||||
-rw-r--r-- | src/expr/kind_template.h | 2 | ||||
-rw-r--r-- | src/expr/type.cpp | 127 | ||||
-rw-r--r-- | src/expr/type.h | 121 |
6 files changed, 10 insertions, 246 deletions
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index a085161bc..9a14caec5 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -752,7 +752,7 @@ public: table_value_type table_value_type; typedef attr::AttributeTraits<table_value_type, context_dep> traits; uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++; - Assert(traits::cleanup.size() == id);// sanity check + //Assert(traits::cleanup.size() == id);// sanity check traits::cleanup.push_back(attr::getCleanupStrategy<value_t, CleanupStrategy>::fn); return id; diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index b9cae9431..09018cbfd 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -43,7 +43,7 @@ class SmtEngine; class NodeManager; class Options; class IntStat; -class ExprManagerMapCollection; +struct ExprManagerMapCollection; class StatisticsRegistry; namespace expr { diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 442d29ac9..b353ec5dc 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -67,7 +67,7 @@ namespace prop { class TheoryProxy; }/* CVC4::prop namespace */ -class ExprManagerMapCollection; +struct ExprManagerMapCollection; struct ExprHashFunction; diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 47504b0e4..0cab4e628 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -27,7 +27,7 @@ namespace CVC4 { namespace kind { -enum Kind_t { +enum CVC4_PUBLIC Kind_t { UNDEFINED_KIND = -1, /**< undefined */ NULL_EXPR, /**< Null kind */ ${kind_decls} diff --git a/src/expr/type.cpp b/src/expr/type.cpp index cc52b11b9..4e95c0fe2 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -204,111 +204,48 @@ bool Type::isBoolean() const { return d_typeNode->isBoolean(); } -/** Cast to a Boolean type */ -Type::operator BooleanType() const throw(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isBoolean(), this); - 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(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isInteger(), this); - return IntegerType(*this); -} - /** Is this the real type? */ bool Type::isReal() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isReal(); } -/** Cast to a real type */ -Type::operator RealType() const throw(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isReal(), this); - return RealType(*this); -} - /** Is this the string type? */ bool Type::isString() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isString(); } -/** Cast to a string type */ -Type::operator StringType() const throw(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isString(), this); - return StringType(*this); -} - /** Is this the bit-vector type? */ bool Type::isBitVector() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isBitVector(); } -/** Cast to a bit-vector type */ -Type::operator BitVectorType() const throw(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isBitVector(), this); - return BitVectorType(*this); -} - -/** Cast to a Constructor type */ -Type::operator DatatypeType() const throw(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isDatatype(), this); - return DatatypeType(*this); -} - /** Is this a datatype type? */ bool Type::isDatatype() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isDatatype() || d_typeNode->isParametricDatatype(); } -/** Cast to a Constructor type */ -Type::operator ConstructorType() const throw(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isConstructor(), this); - return ConstructorType(*this); -} - /** Is this the Constructor type? */ bool Type::isConstructor() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isConstructor(); } -/** Cast to a Selector type */ -Type::operator SelectorType() const throw(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isSelector(), this); - return SelectorType(*this); -} - /** Is this the Selector type? */ bool Type::isSelector() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isSelector(); } -/** Cast to a Tester type */ -Type::operator TesterType() const throw(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isTester(), this); - return TesterType(*this); -} - /** Is this the Tester type? */ bool Type::isTester() const { NodeManagerScope nms(d_nodeManager); @@ -330,64 +267,30 @@ bool Type::isPredicate() const { return d_typeNode->isPredicate(); } -/** Cast to a function type */ -Type::operator FunctionType() const throw(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isFunction(), this); - return FunctionType(*this); -} - /** Is this a tuple type? */ bool Type::isTuple() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isTuple(); } -/** Cast to a tuple type */ -Type::operator TupleType() const throw(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isTuple(), this); - return TupleType(*this); -} - /** Is this a record type? */ bool Type::isRecord() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isRecord(); } -/** Cast to a record type */ -Type::operator RecordType() const throw(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isRecord(), this); - return RecordType(*this); -} - /** Is this a symbolic expression type? */ bool Type::isSExpr() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isSExpr(); } -/** Cast to a symbolic expression type */ -Type::operator SExprType() const throw(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isSExpr(), this); - return SExprType(*this); -} - /** Is this an array type? */ bool Type::isArray() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isArray(); } -/** Cast to an array type */ -Type::operator ArrayType() const throw(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - return ArrayType(*this); -} - /** Is this a sort kind */ bool Type::isSort() const { NodeManagerScope nms(d_nodeManager); @@ -395,25 +298,11 @@ bool Type::isSort() const { } /** Cast to a sort type */ -Type::operator SortType() const throw(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isSort(), this); - 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 constructor type */ -Type::operator SortConstructorType() const throw(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isSortConstructor(), this); - return SortConstructorType(*this); -} - /** Is this a predicate subtype */ /* - not in release 1.0 bool Type::isPredicateSubtype() const { @@ -422,28 +311,12 @@ bool Type::isPredicateSubtype() const { } */ -/** Cast to a predicate subtype */ -/* - not in release 1.0 -Type::operator PredicateSubtype() const throw(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isPredicateSubtype(), this); - return PredicateSubtype(*this); -} -*/ - /** Is this an integer subrange */ bool Type::isSubrange() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isSubrange(); } -/** Cast to a predicate subtype */ -Type::operator SubrangeType() const throw(IllegalArgumentException) { - NodeManagerScope nms(d_nodeManager); - CheckArgument(isNull() || isSubrange(), this); - return SubrangeType(*this); -} - vector<Type> FunctionType::getArgTypes() const { NodeManagerScope nms(d_nodeManager); vector<Type> args; diff --git a/src/expr/type.h b/src/expr/type.h index 4223d71ab..ce6291cd8 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -30,15 +30,15 @@ namespace CVC4 { class NodeManager; -class ExprManager; -class Expr; +class CVC4_PUBLIC ExprManager; +class CVC4_PUBLIC Expr; class TypeNode; -class ExprManagerMapCollection; +struct CVC4_PUBLIC ExprManagerMapCollection; -class SmtEngine; +class CVC4_PUBLIC SmtEngine; -class Datatype; -class Record; +class CVC4_PUBLIC Datatype; +class CVC4_PUBLIC Record; template <bool ref_count> class NodeTemplate; @@ -240,60 +240,30 @@ public: bool isBoolean() const; /** - * Cast this type to a Boolean type - * @return the BooleanType - */ - operator BooleanType() const throw(IllegalArgumentException); - - /** * 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(IllegalArgumentException); - - /** * Is this the real type? * @return true if the type is a real type */ bool isReal() const; /** - * Cast this type to a real type - * @return the RealType - */ - operator RealType() const throw(IllegalArgumentException); - - /** * Is this the string type? * @return true if the type is the string type */ bool isString() const; /** - * Cast this type to a string type - * @return the StringType - */ - operator StringType() const throw(IllegalArgumentException); - - /** * Is this the bit-vector type? * @return true if the type is a bit-vector type */ bool isBitVector() const; /** - * Cast this type to a bit-vector type - * @return the BitVectorType - */ - operator BitVectorType() const throw(IllegalArgumentException); - - /** * Is this a function type? * @return true if the type is a function type */ @@ -307,132 +277,66 @@ public: bool isPredicate() const; /** - * Cast this type to a function type - * @return the FunctionType - */ - operator FunctionType() const throw(IllegalArgumentException); - - /** * Is this a tuple type? * @return true if the type is a tuple type */ bool isTuple() const; /** - * Cast this type to a tuple type - * @return the TupleType - */ - operator TupleType() const throw(IllegalArgumentException); - - /** * Is this a record type? * @return true if the type is a record type */ bool isRecord() const; /** - * Cast this type to a record type - * @return the RecordType - */ - operator RecordType() const throw(IllegalArgumentException); - - /** * Is this a symbolic expression type? * @return true if the type is a symbolic expression type */ bool isSExpr() const; /** - * Cast this type to a symbolic expression type - * @return the SExprType - */ - operator SExprType() const throw(IllegalArgumentException); - - /** * Is this an array type? * @return true if the type is a array type */ bool isArray() const; /** - * Cast this type to an array type - * @return the ArrayType - */ - operator ArrayType() const throw(IllegalArgumentException); - - /** * Is this a datatype type? * @return true if the type is a datatype type */ bool isDatatype() const; /** - * Cast this type to a datatype type - * @return the DatatypeType - */ - operator DatatypeType() const throw(IllegalArgumentException); - - /** * Is this a constructor type? * @return true if the type is a constructor type */ bool isConstructor() const; /** - * Cast this type to a constructor type - * @return the ConstructorType - */ - operator ConstructorType() const throw(IllegalArgumentException); - - /** * Is this a selector type? * @return true if the type is a selector type */ bool isSelector() const; /** - * Cast this type to a selector type - * @return the SelectorType - */ - operator SelectorType() const throw(IllegalArgumentException); - - /** * Is this a tester type? * @return true if the type is a tester type */ bool isTester() const; /** - * Cast this type to a tester type - * @return the TesterType - */ - operator TesterType() const throw(IllegalArgumentException); - - /** * Is this a sort kind? * @return true if this is a sort kind */ bool isSort() const; /** - * Cast this type to a sort type - * @return the sort type - */ - operator SortType() const throw(IllegalArgumentException); - - /** * Is this a sort constructor kind? * @return true if this is a sort constructor kind */ bool isSortConstructor() const; /** - * Cast this type to a sort constructor type - * @return the sort constructor type - */ - operator SortConstructorType() const throw(IllegalArgumentException); - - /** * Is this a predicate subtype? * @return true if this is a predicate subtype */ @@ -440,25 +344,12 @@ public: //bool isPredicateSubtype() const; /** - * Cast this type to a predicate subtype - * @return the predicate subtype - */ - // not in release 1.0 - //operator PredicateSubtype() const throw(IllegalArgumentException); - - /** * Is this an integer subrange type? * @return true if this is an integer subrange type */ bool isSubrange() const; /** - * Cast this type to an integer subrange type - * @return the integer subrange type - */ - operator SubrangeType() const throw(IllegalArgumentException); - - /** * Outputs a string representation of this type to the stream. * @param out the stream to output to */ |