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

20 files changed, 36 insertions, 51 deletions

diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
index cdfdb0284..84f970e87 100644
--- 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 87db28d44..dbbdfe9b7 100644
--- 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 274421249..c00cfdaa3 100644
--- 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 7c837083c..8ea95e1c9 100644
--- 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 5c05bd6a7..edf4e987d 100644
--- 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 69c22c964..e59eacf4d 100644
--- 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 82e658498..9ce902b2a 100644
--- 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 2b7cddcf0..88c17a193 100644
--- 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 1ef2440c9..210391555 100644
--- 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 73c793951..2ce2d2941 100644
--- 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 828fb26f3..a62aaa2e6 100644
--- 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 ecda616f4..44f460559 100644
--- 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 36ab77dd0..10db4f723 100644
--- 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 b9768e6f5..c675ab6c9 100644
--- 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 62f4d4376..d81ad86ab 100644
--- 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 0db1d2fff..aad1f8b2d 100644
--- 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 e4bba78c2..976544e7f 100644
--- 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 e76e5605b..ccc36973d 100644
--- 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 607075658..d3681f471 100644
--- 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 8ce82ee7f..5be9525a9 100644
--- 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() */