remove/shuffle some #include dependencies; fix some documentation; apply coding standards

13 files changed, 44 insertions, 51 deletions

diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 0668c5f8f..98aea9707 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -26,14 +26,8 @@
 #ifndef __CVC4__EXPR__ATTRIBUTE_H
 #define __CVC4__EXPR__ATTRIBUTE_H
 
-#include <stdint.h>
-
 #include <string>
-#include <ext/hash_map>
-
-#include "context/cdmap.h"
-#include "expr/node.h"
-#include "util/output.h"
+#include <stdint.h>
 
 // include supporting templates
 #define CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index b5ccb6f79..a77d09c4d 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -25,6 +25,10 @@
 #ifndef __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
 #define __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
 
+#include <ext/hash_map>
+
+#include "context/cdmap.h"
+
 namespace CVC4 {
 namespace expr {
 
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index 83462c355..74869bae7 100644
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -16,14 +16,14 @@
  ** Convenience class for scoping variable and type declarations.
  **/
 
-#ifndef DECLARATION_SCOPE_H_
-#define DECLARATION_SCOPE_H_
+#ifndef DECLARATION_SCOPE_H
+#define DECLARATION_SCOPE_H
+
+#include <ext/hash_map>
 
 #include "expr/expr.h"
 #include "util/hash.h"
 
-#include <ext/hash_map>
-
 namespace CVC4 {
 
 class Type;
@@ -122,8 +122,8 @@ public:
 
   /** Push a scope level. */
   void pushScope() throw ();
-};
+};/* class DeclarationScope */
 
-} // namespace CVC4
+}/* namespace CVC4 */
 
-#endif /* DECLARATION_SCOPE_H_ */
+#endif /* DECLARATION_SCOPE_H */
diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h
index b0b704de4..4fc3f02d4 100644
--- a/src/expr/expr_manager_scope.h
+++ b/src/expr/expr_manager_scope.h
@@ -22,6 +22,7 @@
 
 #include "expr/expr.h"
 #include "expr/node_manager.h"
+#include "expr/expr_manager.h"
 
 namespace CVC4 {
 
@@ -56,9 +57,8 @@ public:
   inline ExprManagerScope(const ExprManager& exprManager) :
     d_nms(exprManager.getNodeManager()) {
   }
-};
-
-}
+};/* class ExprManagerScope */
 
+}/* CVC4 namespace */
 
 #endif /* __CVC4__EXPR_MANAGER_SCOPE_H */
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 3fd3cce28..da209c581 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -16,11 +16,6 @@
  ** Public-facing expression manager interface, implementation.
  **/
 
-#include "expr/node.h"
-#include "expr/expr.h"
-#include "expr/kind.h"
-#include "expr/metakind.h"
-#include "expr/type.h"
 #include "expr/node_manager.h"
 #include "expr/expr_manager.h"
 #include "context/context.h"
@@ -31,7 +26,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 35 "${template}"
+#line 30 "${template}"
 
 using namespace std;
 using namespace CVC4::context;
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 8e02c8ca4..70f4f8453 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -25,7 +25,6 @@
 
 #include "expr/kind.h"
 #include "expr/type.h"
-#include "expr/expr.h"
 
 ${includes}
 
@@ -33,11 +32,12 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 37 "${template}"
+#line 36 "${template}"
 
 namespace CVC4 {
 
 class Expr;
+class TypeCheckingException;
 class SmtEngine;
 class NodeManager;
 
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 48acd2588..54e20667f 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -17,12 +17,9 @@
  **/
 
 #include "expr/expr.h"
-#include "expr/expr_manager.h"
 #include "expr/node.h"
-#include "util/Assert.h"
-
-#include "util/output.h"
 #include "expr/expr_manager_scope.h"
+#include "util/Assert.h"
 
 ${includes}
 
@@ -36,6 +33,8 @@ using namespace CVC4::kind;
 
 namespace CVC4 {
 
+class ExprManager;
+
 namespace expr {
 
 const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc();
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 15938b160..349795156 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -21,18 +21,19 @@
 #ifndef __CVC4__EXPR_H
 #define __CVC4__EXPR_H
 
-#include "expr/type.h"
 #include <string>
 #include <iostream>
 #include <stdint.h>
 
+#include "util/exception.h"
+
 ${includes}
 
 // This is a hack, but an important one: if there's an error, the
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 36 "${template}"
+#line 37 "${template}"
 
 namespace CVC4 {
 
@@ -41,6 +42,8 @@ template <bool ref_count>
 class NodeTemplate;
 
 class Expr;
+class ExprManager;
+class Type;
 
 namespace expr {
   class CVC4_PUBLIC ExprSetDepth;
@@ -553,13 +556,13 @@ public:
   static inline void setPrintTypes(std::ostream& out, bool printTypes) {
     out.iword(s_iosIndex) = printTypes;
   }
-};
+};/* class ExprPrintTypes */
 
 }/* CVC4::expr namespace */
 
 ${getConst_instantiations}
 
-#line 388 "${template}"
+#line 566 "${template}"
 
 namespace expr {
 
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index b111e5604..43325d6cc 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -16,13 +16,12 @@
  ** Implementation of expression types 
  **/
 
+#include <string>
+
 #include "expr/node_manager.h"
-#include "expr/expr_manager.h"
 #include "expr/type.h"
 #include "expr/type_node.h"
-#include "expr/type_constant.h"
 #include "util/Assert.h"
-#include <string>
 
 namespace CVC4 {
 
@@ -31,15 +30,13 @@ std::ostream& operator<<(std::ostream& out, const Type& e) {
   return out;
 }
 
-Type Type::makeType(const TypeNode& typeNode) const
-{
+Type Type::makeType(const TypeNode& typeNode) const {
   return Type(d_nodeManager, new TypeNode(typeNode));
 }
 
 Type::Type(NodeManager* nm, TypeNode* node)
 : d_typeNode(node),
-  d_nodeManager(nm)
-{
+  d_nodeManager(nm) {
 }
 
 Type::~Type() {
diff --git a/src/expr/type.h b/src/expr/type.h
index 9ade5e6f5..3e3fbd368 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -21,19 +21,19 @@
 #ifndef __CVC4__TYPE_H
 #define __CVC4__TYPE_H
 
-#include "util/output.h"
-#include "util/Assert.h"
-
 #include <string>
 #include <vector>
 #include <limits.h>
 #include <stdint.h>
 
+#include "util/Assert.h"
+
 namespace CVC4 {
 
 class NodeManager;
 class ExprManager;
 class TypeNode;
+
 template <bool ref_count>
 class NodeTemplate;
 
diff --git a/src/expr/type_constant.h b/src/expr/type_constant.h
index 3d5ca229a..3001d4513 100644
--- a/src/expr/type_constant.h
+++ b/src/expr/type_constant.h
@@ -16,8 +16,12 @@
  ** Interface for expression types
  **/
 
-#ifndef __CVC4__TYPE_CONSTANT_H_
-#define __CVC4__TYPE_CONSTANT_H_
+#include "cvc4_public.h"
+
+#ifndef __CVC4__TYPE_CONSTANT_H
+#define __CVC4__TYPE_CONSTANT_H
+
+#include <iostream>
 
 namespace CVC4 {
 
@@ -33,7 +37,7 @@ enum TypeConstant {
   REAL_TYPE,
   /** The kind type (type of types) */
   KIND_TYPE
-};
+};/* enum TypeConstant */
 
 /**
  * We hash the constants with their values.
@@ -45,7 +49,6 @@ struct TypeConstantHashStrategy {
 };/* struct BoolHashStrategy */
 
 inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
-
   switch(typeConstant) {
   case BOOLEAN_TYPE:
     out << "BOOLEAN";
@@ -66,6 +69,6 @@ inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
   return out;
 }
 
-}
+}/* CVC4 namespace */
 
-#endif /* __CVC4__TYPE_CONSTANT_H_ */
+#endif /* __CVC4__TYPE_CONSTANT_H */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 491734b35..94213d941 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -115,5 +115,4 @@ unsigned TypeNode::getBitVectorSize() const {
   return getConst<BitVectorSize>();
 }
 
-
 }/* CVC4 namespace */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 811eab54f..30359495f 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -32,7 +32,6 @@
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "util/Assert.h"
-#include "util/output.h"
 
 namespace CVC4 {