Fix errors and reduce warnings on clang (merge from mdeters/clang)

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
    */