diff options
40 files changed, 105 insertions, 125 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 { diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index b63f39d78..2e0af677e 100644 --- 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 1bb8f0679..da352c226 100644 --- 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 23879fda8..e704d027d 100644 --- 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 25083688a..9f24e9873 100644 --- 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 20dd56fa7..70b53a930 100644 --- 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 5d1137d27..2ff92e788 100644 --- 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 b0f899f9b..748ac3f9d 100644 --- 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 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() */ |