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

diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 0668c5f8f7742c1146f74770c76ede587aedb12d..98aea9707144e01b55c36f7d75c6f236a1849ff1 100644 (file)
--- 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 b5ccb6f79387e69a159d3c745bdf8809714d028d..a77d09c4df96c26a4f1c336a0dc97878ca64498d 100644 (file)
--- 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 83462c355a651b51b26a1f33532cc9da94bb4db8..74869bae753882f5c6f5160ad2b97c4202318841 100644 (file)
--- 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 b0b704de46cf65c03dd1264005f4aa475ffc7904..4fc3f02d475b0bc33cd8ed5c344b06e92316ff90 100644 (file)
--- 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 3fd3cce28bc8b886da62028f2db5fd9095f4f97c..da209c58150c3ad5f4dc39a79305d44a44dc147c 100644 (file)
--- 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 8e02c8ca426f23044f0bcec1de04f7c290444675..70f4f8453bc62377211114c50e15ed795a2440fc 100644 (file)
--- 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 48acd25889ccf0d42d5b32a843c7a42bb96c994e..54e20667f45c7dea6f01bd1623f1ffe2f40d6ab5 100644 (file)
--- 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 15938b16087da919a07df97c7b9e92e7399cdc82..349795156194b5bebe1f7d70fc1eaa8b6cb3959d 100644 (file)
--- 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 b111e5604ca4905fc37ca280194f9da2bf232de8..43325d6cc4131fb0700429a879b83ac29a0185db 100644 (file)
--- 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 9ade5e6f5f76bdce12220b09ed1d6b19ba76b835..3e3fbd368711da0396aa4ae61a71a51c9d26c6cf 100644 (file)
--- 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 3d5ca229a7205542eed0ee0e4313a8c3024dde91..3001d4513248ef3f313a0a1e337e2306421f5938 100644 (file)
--- 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 491734b35398a4784b263eb38f4139f642b0cdff..94213d941b054f9e45cd05d3dc5b759293d1a67d 100644 (file)
--- 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 811eab54f03a213e62b9ca9ceabbd273f452e131..30359495f63effecca9eee9c9fc4084e32f85351 100644 (file)
--- 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 {
 

diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index b63f39d789ed1cec77063be780f8345c9cbd9389..2e0af677effccc006deeed5e51bc5f2d006e2afe 100644 (file)
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -18,8 +18,8 @@
 
 #include "cvc4parser_public.h"
 
-#ifndef __CVC4__PARSER__PARSER_BUILDER_H_
-#define __CVC4__PARSER__PARSER_BUILDER_H_
+#ifndef __CVC4__PARSER__PARSER_BUILDER_H
+#define __CVC4__PARSER__PARSER_BUILDER_H
 
 #include <string>
 
@@ -31,8 +31,8 @@ namespace CVC4 {
 class ExprManager;
 
 namespace parser {
-/*
 
+/*
 class InputBuilder {
 protected:
   InputLanguage d_lang;
@@ -126,9 +126,9 @@ public:
 
   /** Set the parser to use the given string for its input. */
   ParserBuilder& withStringInput(const std::string& input);
-};
+};/* class ParserBuilder */
 
-} /* namespace parser */
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
 
-} /* namespace CVC4 */
-#endif /* __CVC4__PARSER__PARSER_BUILDER_H_ */
+#endif /* __CVC4__PARSER__PARSER_BUILDER_H */

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index 1bb8f0679cc2b1d25490c96ff9c699c3b44f6612..da352c226d09e1c791ba4556605ec9e87d31bd04 100644 (file)
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -16,9 +16,10 @@
 
 #include <ext/hash_map>
 namespace std {
-using namespace __gnu_cxx;
+  using namespace __gnu_cxx;
 }
 
+#include "expr/type.h"
 #include "parser/parser.h"
 #include "parser/smt/smt.h"
 

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 23879fda883217f7d7fc9ce0e5a73b0af4f4cfbe..e704d027d58847ebd32dbfb0ee359d587914bd43 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -16,6 +16,7 @@
  ** Definitions of SMT2 constants.
  **/
 
+#include "expr/type.h"
 #include "parser/parser.h"
 #include "parser/smt/smt.h"
 #include "parser/smt2/smt2.h"

diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index 25083688ab2f574acc7919302f75bf3a8b13b18f..9f24e9873c9df22be546cc3251d801eab1e53cce 100644 (file)
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H_
-#define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H_
+#ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
+#define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
 
 namespace CVC4 {
 namespace theory {
@@ -63,4 +63,4 @@ struct ArrayStoreTypeRule {
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H_ */
+#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H */

diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index 20dd56fa780b73b57ce5b87a7c90c33262f75a67..70b53a930728ff327c7389b92966499c50a54d83 100644 (file)
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY_BOOL_TYPE_RULES_H_
-#define __CVC4__THEORY_BOOL_TYPE_RULES_H_
+#ifndef __CVC4__THEORY_BOOL_TYPE_RULES_H
+#define __CVC4__THEORY_BOOL_TYPE_RULES_H
 
 namespace CVC4 {
 namespace theory {
@@ -61,8 +61,8 @@ class IteTypeRule {
   }
 };
 
-} // boolean namespace
-} // theory namespace
-} // CVC4 namespace
+}/* namespace CVC4::theory::boolean */
+}/* namespace CVC4::theory */
+}/* namespace CVC4 */
 
-#endif /* __CVC4__THEORY_BOOL_TYPE_RULES_H_ */
+#endif /* __CVC4__THEORY_BOOL_TYPE_RULES_H */

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 5d1137d27c71ae5c297c0e1276214465eadff651..2ff92e7888d60f9aa4c2db40848035f31f83eb68 100644 (file)
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H_
-#define __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H_
+#ifndef __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H
+#define __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H
 
 #include "expr/node.h"
 #include "expr/type_node.h"
@@ -93,4 +93,4 @@ public:
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H_ */
+#endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H */

diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index b0f899f9b2718ea17a47b9d7031eaa43bf1796ec..748ac3f9d0542bc52a280a6d97f37a793ac936e5 100644 (file)
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H_
-#define __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H_
+#ifndef __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H
+#define __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H
 
 namespace CVC4 {
 namespace theory {
@@ -55,4 +55,4 @@ public:
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H_ */
+#endif /* __CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H */

diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
index cdfdb0284a10a7842f91e1302a2119af071970ef..84f970e87aa7806491bdbcf65f16d416071bc96f 100644 (file)
--- a/src/util/Assert.cpp
+++ b/src/util/Assert.cpp
@@ -21,8 +21,6 @@
 #include <cstdio>
 
 #include "util/Assert.h"
-#include "util/exception.h"
-#include "util/tls.h"
 
 using namespace std;
 

diff --git a/src/util/Assert.h b/src/util/Assert.h
index 87db28d44b20b4083799350308e71a4f56f05d4b..dbbdfe9b7f79b21c5c9db2fab60a7e38267a3592 100644 (file)
--- a/src/util/Assert.h
+++ b/src/util/Assert.h
@@ -28,9 +28,12 @@
 #include <cstdarg>
 
 #include "util/exception.h"
-#include "util/output.h"
 #include "util/tls.h"
 
+// output.h not strictly needed for this header, but it _is_ needed to
+// actually _use_ anything in this header, so let's include it.
+#include "util/output.h"
+
 namespace CVC4 {
 
 class CVC4_PUBLIC AssertionException : public Exception {

diff --git a/src/util/array.h b/src/util/array.h
index 2744212497e4e970df92e60a770c81e114e678ca..c00cfdaa36b0d868e1c27884b16752c948d0d6ed 100644 (file)
--- a/src/util/array.h
+++ b/src/util/array.h
@@ -18,14 +18,11 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__ARRAY_H_
-#define __CVC4__ARRAY_H_
-
-#include <iostream>
-#include "util/Assert.h"
+#ifndef __CVC4__ARRAY_H
+#define __CVC4__ARRAY_H
 
 // we get ArrayType right now by #including type.h.
 // array.h is still useful for the auto-generated kinds #includes.
 #include "expr/type.h"
 
-#endif /* __CVC4__ARRAY_H_ */
+#endif /* __CVC4__ARRAY_H */

diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
index 7c837083c9c44d61370f8a79ffaf4e119e95f053..8ea95e1c9a53a081c1387a8a986e6292c5f5315d 100644 (file)
--- a/src/util/bitvector.cpp
+++ b/src/util/bitvector.cpp
@@ -29,4 +29,4 @@ std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
   return os << "[" << bv.high << ":" << bv.low << "]";
 }
 
-}
+}/* CVC4 namespace */

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 5c05bd6a76f6ec5645b75c31d7b4dea07a1e1c3c..edf4e987d82437a303b998dfab14d0c5d4d60212 100644 (file)
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -19,8 +19,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__BITVECTOR_H_
-#define __CVC4__BITVECTOR_H_
+#ifndef __CVC4__BITVECTOR_H
+#define __CVC4__BITVECTOR_H
 
 #include <iostream>
 #include "util/Assert.h"
@@ -247,7 +247,7 @@ struct UnsignedHashStrategy {
 
 std::ostream& operator <<(std::ostream& os, const BitVector& bv);
 std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv);
-}
 
+}/* CVC4 namespace */
 
-#endif /* __CVC4__BITVECTOR_H_ */
+#endif /* __CVC4__BITVECTOR_H */

diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index 69c22c964f86a912972b98c4234a4555618af45a..e59eacf4d6242fcf30c1bd4ff2b4f29e45d91cd8 100644 (file)
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -20,8 +20,6 @@
 #ifndef __CVC4__CONFIGURATION_PRIVATE_H
 #define __CVC4__CONFIGURATION_PRIVATE_H
 
-#include "cvc4autoconfig.h"
-
 using namespace std;
 
 namespace CVC4 {

diff --git a/src/util/congruence_closure.cpp b/src/util/congruence_closure.cpp
index 82e65849886df7680af77e55e4838937aeeec105..9ce902b2a83b4249f88c3e4941c9ca8df6b398d8 100644 (file)
--- a/src/util/congruence_closure.cpp
+++ b/src/util/congruence_closure.cpp
@@ -17,17 +17,9 @@
  **/
 
 #include "util/congruence_closure.h"
-#include "util/Assert.h"
-
-#include <string>
-#include <list>
-#include <algorithm>
-#include <utility>
-#include <ext/hash_map>
 
 using namespace std;
 
 namespace CVC4 {
 
-
 }/* CVC4 namespace */

diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h
index 2b7cddcf097c69fca2d791f456872f46a737b33f..88c17a19349a8fb9817f21459019b4563303bb41 100644 (file)
--- a/src/util/congruence_closure.h
+++ b/src/util/congruence_closure.h
@@ -21,14 +21,13 @@
 #ifndef __CVC4__UTIL__CONGRUENCE_CLOSURE_H
 #define __CVC4__UTIL__CONGRUENCE_CLOSURE_H
 
+#include <sstream>
 #include <list>
+
 #include <ext/hash_map>
-#include <ext/hash_set>
-#include <sstream>
 
 #include "expr/node_manager.h"
 #include "expr/node.h"
-#include "context/context.h"
 #include "context/cdmap.h"
 #include "context/cdset.h"
 #include "context/cdlist.h"

diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp
index 1ef2440c995d4947a8194217f75738a2ec55b305..2103915554d8f99871bbaa67ed0d585253b619cf 100644 (file)
--- a/src/util/decision_engine.cpp
+++ b/src/util/decision_engine.cpp
@@ -17,7 +17,6 @@
 
 #include "util/decision_engine.h"
 #include "util/Assert.h"
-#include "expr/node.h"
 
 namespace CVC4 {
 

diff --git a/src/util/hash.h b/src/util/hash.h
index 73c7939512e6e889eae4e2005f466a3a3e152a15..2ce2d294170aeadd75aa1099047d27047618fe6a 100644 (file)
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -17,8 +17,8 @@
  ** \todo document this file
  **/
 
-#ifndef __CVC4__HASH_H_
-#define __CVC4__HASH_H_
+#ifndef __CVC4__HASH_H
+#define __CVC4__HASH_H
 
 #include <ext/hash_map>
 namespace std { using namespace __gnu_cxx; }
@@ -29,8 +29,8 @@ struct StringHashFunction {
   size_t operator()(const std::string& str) const {
     return std::hash<const char*>()(str.c_str());
   }
-};
+};/* struct StringHashFunction */
 
-}
+}/* CVC4 namespace */
 
-#endif /* __CVC4__HASH_H_ */
+#endif /* __CVC4__HASH_H */

diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 828fb26f37911e8be703b388593f19bfa19048ac..a62aaa2e6f5351d309170f02f8c7d3e7bca0ea33 100644 (file)
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -23,12 +23,12 @@
 #define __CVC4__INTEGER_H
 
 #include <string>
+#include <sstream>
 #include <iostream>
+
 #include <cln/integer.h>
-#include <sstream>
 #include <cln/input.h>
 #include <cln/integer_io.h>
-#include "util/Assert.h"
 
 namespace CVC4 {
 

diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index ecda616f4908de4f92c12f677e6656c92206449a..44f4605597a5cf719e0f5f7544b30d685c998b20 100644 (file)
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -24,6 +24,7 @@
 
 #include <string>
 #include <iostream>
+
 #include "util/gmp_util.h"
 
 namespace CVC4 {

diff --git a/src/util/output.cpp b/src/util/output.cpp
index 36ab77dd009ba5ae2ab90f407ed076b0a770e46d..10db4f723a3da28dbfb2e07122eb8dd94dbb0f90 100644 (file)
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -17,6 +17,7 @@
  **/
 
 #include <iostream>
+
 #include "util/output.h"
 
 using namespace std;

diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index b9768e6f5e789fd0ba730f9b153082d56137788f..c675ab6c98edff541bbf2d7a2d8d3b60b381423e 100644 (file)
--- a/src/util/rational_cln_imp.cpp
+++ b/src/util/rational_cln_imp.cpp
@@ -18,7 +18,6 @@
 
 #include "cvc4autoconfig.h"
 #include "util/rational.h"
-#include "util/integer.h"
 #include <string>
 
 #ifndef CVC4_CLN_IMP

diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 62f4d4376effaefeafeb177941d0d8b9a492646d..d81ad86ababa96f0d1aa5a059c652b56cf40b685 100644 (file)
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -29,6 +29,7 @@
 #include <cln/input.h>
 #include <cln/rational_io.h>
 #include <cln/number_io.h>
+
 #include "util/Assert.h"
 #include "util/integer.h"
 

diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp
index 0db1d2ffff9d9b4a0479fcb2eb71a9d6ff0f6ddf..aad1f8b2d91b3a7c1004c3adce7241ea50b872a4 100644 (file)
--- a/src/util/rational_gmp_imp.cpp
+++ b/src/util/rational_gmp_imp.cpp
@@ -18,7 +18,6 @@
 
 #include "cvc4autoconfig.h"
 #include "util/rational.h"
-#include "util/integer.h"
 #include <string>
 
 #ifndef CVC4_GMP_IMP

diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index e4bba78c2954be06e98528d16ea07adaf736ef54..976544e7f96fd79d1a41e8b9bbb6dcff7ec7065b 100644 (file)
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -24,6 +24,7 @@
 
 #include <gmp.h>
 #include <string>
+
 #include "util/integer.h"
 
 namespace CVC4 {

diff --git a/src/util/result.h b/src/util/result.h
index e76e5605b22ea7dcdaea6c4f18d420364413d26e..ccc36973d4b68b512a5d0bef2d9b93d6b1b2485b 100644 (file)
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -21,8 +21,6 @@
 #ifndef __CVC4__RESULT_H
 #define __CVC4__RESULT_H
 
-#include "util/Assert.h"
-
 namespace CVC4 {
 
 // TODO: perhaps best to templatize Result on its Kind (SAT/Validity),

diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 607075658ae06cdab85490e8b2d05fc366c282eb..d3681f4713be1d731fbbed0b8c0cc3462e9495b3 100644 (file)
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -18,14 +18,14 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__SEXPR_H_
-#define __CVC4__SEXPR_H_
-
-#include "util/Assert.h"
+#ifndef __CVC4__SEXPR_H
+#define __CVC4__SEXPR_H
 
 #include <vector>
 #include <string>
 
+#include "util/Assert.h"
+
 namespace CVC4 {
 
 /**
@@ -106,6 +106,6 @@ inline std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) {
   return out;
 }
 
-}
+}/* CVC4 namespace */
 
-#endif /* __CVC4__SEXPR_H_ */
+#endif /* __CVC4__SEXPR_H */

diff --git a/src/util/stats.cpp b/src/util/stats.cpp
index 8ce82ee7fbf97a68e47aca800332da284229cdf3..5be9525a935170573dc1fa70c2580feca28a207c 100644 (file)
--- a/src/util/stats.cpp
+++ b/src/util/stats.cpp
@@ -25,15 +25,14 @@ StatisticsRegistry::StatSet StatisticsRegistry::d_registeredStats;
 
 std::string Stat::s_delim(",");
 
-
-
-
-void StatisticsRegistry::flushStatistics(std::ostream& out){
+void StatisticsRegistry::flushStatistics(std::ostream& out) {
 #ifdef CVC4_STATISTICS_ON
-  for(StatSet::iterator i=d_registeredStats.begin();i != d_registeredStats.end();++i){
+  for(StatSet::iterator i = d_registeredStats.begin();
+      i != d_registeredStats.end();
+      ++i) {
     Stat* s = *i;
     s->flushStat(out);
     out << std::endl;
   }
 #endif
-}
+}/* StatisticsRegistry::flushStatistics() */