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/expr | |
parent | 738114852c81e7203fda105d5386dc26187fcb87 (diff) |
remove/shuffle some #include dependencies; fix some documentation; apply coding standards
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/attribute.h | 8 | ||||
-rw-r--r-- | src/expr/attribute_internals.h | 4 | ||||
-rw-r--r-- | src/expr/declaration_scope.h | 14 | ||||
-rw-r--r-- | src/expr/expr_manager_scope.h | 6 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 7 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 4 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 7 | ||||
-rw-r--r-- | src/expr/expr_template.h | 11 | ||||
-rw-r--r-- | src/expr/type.cpp | 11 | ||||
-rw-r--r-- | src/expr/type.h | 6 | ||||
-rw-r--r-- | src/expr/type_constant.h | 15 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 1 | ||||
-rw-r--r-- | src/expr/type_node.h | 1 |
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 { |