diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-04 04:20:19 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-04 04:20:19 +0000 |
commit | 7719416c6698cdc49b7a0d2d62b4472ef815a487 (patch) | |
tree | 472f1fd2f399224062753b5bc588b567423efa4a /src/util | |
parent | 738114852c81e7203fda105d5386dc26187fcb87 (diff) |
remove/shuffle some #include dependencies; fix some documentation; apply coding standards
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Assert.cpp | 2 | ||||
-rw-r--r-- | src/util/Assert.h | 5 | ||||
-rw-r--r-- | src/util/array.h | 9 | ||||
-rw-r--r-- | src/util/bitvector.cpp | 2 | ||||
-rw-r--r-- | src/util/bitvector.h | 8 | ||||
-rw-r--r-- | src/util/configuration_private.h | 2 | ||||
-rw-r--r-- | src/util/congruence_closure.cpp | 8 | ||||
-rw-r--r-- | src/util/congruence_closure.h | 5 | ||||
-rw-r--r-- | src/util/decision_engine.cpp | 1 | ||||
-rw-r--r-- | src/util/hash.h | 10 | ||||
-rw-r--r-- | src/util/integer_cln_imp.h | 4 | ||||
-rw-r--r-- | src/util/integer_gmp_imp.h | 1 | ||||
-rw-r--r-- | src/util/output.cpp | 1 | ||||
-rw-r--r-- | src/util/rational_cln_imp.cpp | 1 | ||||
-rw-r--r-- | src/util/rational_cln_imp.h | 1 | ||||
-rw-r--r-- | src/util/rational_gmp_imp.cpp | 1 | ||||
-rw-r--r-- | src/util/rational_gmp_imp.h | 1 | ||||
-rw-r--r-- | src/util/result.h | 2 | ||||
-rw-r--r-- | src/util/sexpr.h | 12 | ||||
-rw-r--r-- | src/util/stats.cpp | 11 |
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() */ |