diff options
Diffstat (limited to 'src/expr')
33 files changed, 120 insertions, 120 deletions
diff --git a/src/expr/array.h b/src/expr/array.h index b313a694b..a53ac3cd2 100644 --- a/src/expr/array.h +++ b/src/expr/array.h @@ -16,11 +16,11 @@ #include "cvc4_public.h" -#ifndef __CVC4__ARRAY_H -#define __CVC4__ARRAY_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/expr/array_store_all.h b/src/expr/array_store_all.h index 3b1112e4f..0adcfde36 100644 --- a/src/expr/array_store_all.h +++ b/src/expr/array_store_all.h @@ -18,8 +18,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__ARRAY_STORE_ALL_H -#define __CVC4__ARRAY_STORE_ALL_H +#ifndef CVC4__ARRAY_STORE_ALL_H +#define CVC4__ARRAY_STORE_ALL_H #include <iosfwd> #include <memory> @@ -72,4 +72,4 @@ struct CVC4_PUBLIC ArrayStoreAllHashFunction { } // namespace CVC4 -#endif /* __CVC4__ARRAY_STORE_ALL_H */ +#endif /* CVC4__ARRAY_STORE_ALL_H */ diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h index 8089a2c85..94258896a 100644 --- a/src/expr/ascription_type.h +++ b/src/expr/ascription_type.h @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__ASCRIPTION_TYPE_H -#define __CVC4__ASCRIPTION_TYPE_H +#ifndef CVC4__ASCRIPTION_TYPE_H +#define CVC4__ASCRIPTION_TYPE_H #include "expr/type.h" @@ -63,4 +63,4 @@ inline std::ostream& operator<<(std::ostream& out, AscriptionType at) { }/* CVC4 namespace */ -#endif /* __CVC4__ASCRIPTION_TYPE_H */ +#endif /* CVC4__ASCRIPTION_TYPE_H */ diff --git a/src/expr/attribute.h b/src/expr/attribute.h index bccea5dda..46302fc9f 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -21,8 +21,8 @@ #include "expr/node.h" #include "expr/type_node.h" -#ifndef __CVC4__EXPR__ATTRIBUTE_H -#define __CVC4__EXPR__ATTRIBUTE_H +#ifndef CVC4__EXPR__ATTRIBUTE_H +#define CVC4__EXPR__ATTRIBUTE_H #include <string> #include <stdint.h> @@ -578,4 +578,4 @@ NodeManager::setAttribute(TypeNode n, const AttrKind&, }/* CVC4 namespace */ -#endif /* __CVC4__EXPR__ATTRIBUTE_H */ +#endif /* CVC4__EXPR__ATTRIBUTE_H */ diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index 83056896f..e47dce434 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -20,8 +20,8 @@ # error expr/attribute_internals.h should only be included by expr/attribute.h #endif /* CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H */ -#ifndef __CVC4__EXPR__ATTRIBUTE_INTERNALS_H -#define __CVC4__EXPR__ATTRIBUTE_INTERNALS_H +#ifndef CVC4__EXPR__ATTRIBUTE_INTERNALS_H +#define CVC4__EXPR__ATTRIBUTE_INTERNALS_H #include <cstdint> #include <unordered_map> @@ -486,4 +486,4 @@ const uint64_t Attribute<T, bool, context_dep>::s_id = }/* CVC4::expr namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__EXPR__ATTRIBUTE_INTERNALS_H */ +#endif /* CVC4__EXPR__ATTRIBUTE_INTERNALS_H */ diff --git a/src/expr/chain.h b/src/expr/chain.h index 99df9ee7b..9df819b4d 100644 --- a/src/expr/chain.h +++ b/src/expr/chain.h @@ -17,8 +17,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__CHAIN_H -#define __CVC4__CHAIN_H +#ifndef CVC4__CHAIN_H +#define CVC4__CHAIN_H #include "expr/kind.h" #include <iostream> @@ -48,4 +48,4 @@ struct CVC4_PUBLIC ChainHashFunction { }/* CVC4 namespace */ -#endif /* __CVC4__CHAIN_H */ +#endif /* CVC4__CHAIN_H */ diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 3cc02d3c5..0e8ace709 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -17,8 +17,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__DATATYPE_H -#define __CVC4__DATATYPE_H +#ifndef CVC4__DATATYPE_H +#define CVC4__DATATYPE_H #include <functional> #include <iostream> @@ -1288,4 +1288,4 @@ inline DatatypeConstructor::const_iterator DatatypeConstructor::end() const }/* CVC4 namespace */ -#endif /* __CVC4__DATATYPE_H */ +#endif /* CVC4__DATATYPE_H */ diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h index 7203063b7..9a582f8c8 100644 --- a/src/expr/expr_iomanip.h +++ b/src/expr/expr_iomanip.h @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__EXPR__EXPR_IOMANIP_H -#define __CVC4__EXPR__EXPR_IOMANIP_H +#ifndef CVC4__EXPR__EXPR_IOMANIP_H +#define CVC4__EXPR__EXPR_IOMANIP_H #include <iosfwd> @@ -236,4 +236,4 @@ std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) CVC4_PUBLIC; }/* CVC4 namespace */ -#endif /* __CVC4__EXPR__EXPR_IOMANIP_H */ +#endif /* CVC4__EXPR__EXPR_IOMANIP_H */ diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h index cad5195dd..b494796a1 100644 --- a/src/expr/expr_manager_scope.h +++ b/src/expr/expr_manager_scope.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__EXPR_MANAGER_SCOPE_H -#define __CVC4__EXPR_MANAGER_SCOPE_H +#ifndef CVC4__EXPR_MANAGER_SCOPE_H +#define CVC4__EXPR_MANAGER_SCOPE_H #include "expr/expr.h" #include "expr/node_manager.h" @@ -66,4 +66,4 @@ public: }/* CVC4 namespace */ -#endif /* __CVC4__EXPR_MANAGER_SCOPE_H */ +#endif /* CVC4__EXPR_MANAGER_SCOPE_H */ diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 2e6832840..17affaef0 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__EXPR_MANAGER_H -#define __CVC4__EXPR_MANAGER_H +#ifndef CVC4__EXPR_MANAGER_H +#define CVC4__EXPR_MANAGER_H #include <vector> @@ -586,4 +586,4 @@ ${mkConst_instantiations} }/* CVC4 namespace */ -#endif /* __CVC4__EXPR_MANAGER_H */ +#endif /* CVC4__EXPR_MANAGER_H */ diff --git a/src/expr/expr_stream.h b/src/expr/expr_stream.h index e4fdeb598..d31e8e4fc 100644 --- a/src/expr/expr_stream.h +++ b/src/expr/expr_stream.h @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__EXPR_STREAM_H -#define __CVC4__EXPR_STREAM_H +#ifndef CVC4__EXPR_STREAM_H +#define CVC4__EXPR_STREAM_H #include "expr/expr.h" @@ -41,5 +41,5 @@ public: }/* CVC4 namespace */ -#endif /* __CVC4__EXPR_STREAM_H */ +#endif /* CVC4__EXPR_STREAM_H */ diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 71f09825e..a32590050 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -23,8 +23,8 @@ // "expr.h" safely, then go on to completely declare their own stuff. ${includes} -#ifndef __CVC4__EXPR_H -#define __CVC4__EXPR_H +#ifndef CVC4__EXPR_H +#define CVC4__EXPR_H #include <stdint.h> #include <iosfwd> @@ -620,4 +620,4 @@ inline size_t ExprHashFunction::operator()(CVC4::Expr e) const { }/* CVC4 namespace */ -#endif /* __CVC4__EXPR_H */ +#endif /* CVC4__EXPR_H */ diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h index 45e128c37..a5ae73802 100644 --- a/src/expr/kind_map.h +++ b/src/expr/kind_map.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__KIND_MAP_H -#define __CVC4__KIND_MAP_H +#ifndef CVC4__KIND_MAP_H +#define CVC4__KIND_MAP_H #include <stdint.h> #include <iterator> @@ -271,4 +271,4 @@ inline KindMap operator^(Kind k1, KindMap m2) { }/* CVC4 namespace */ -#endif /* __CVC4__KIND_MAP_H */ +#endif /* CVC4__KIND_MAP_H */ diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 820fa6b7d..93c37f6cc 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__KIND_H -#define __CVC4__KIND_H +#ifndef CVC4__KIND_H +#define CVC4__KIND_H #include <iosfwd> @@ -104,4 +104,4 @@ std::string getStatsPrefix(TheoryId theoryId) CVC4_PUBLIC; }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__KIND_H */ +#endif /* CVC4__KIND_H */ diff --git a/src/expr/matcher.h b/src/expr/matcher.h index a08d17715..95ece7d23 100644 --- a/src/expr/matcher.h +++ b/src/expr/matcher.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__MATCHER_H -#define __CVC4__MATCHER_H +#ifndef CVC4__MATCHER_H +#define CVC4__MATCHER_H #include <iosfwd> #include <string> @@ -116,4 +116,4 @@ public: }/* CVC4 namespace */ -#endif /* __CVC4__MATCHER_H */ +#endif /* CVC4__MATCHER_H */ diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 1da66202b..3550acf05 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__KIND__METAKIND_H -#define __CVC4__KIND__METAKIND_H +#ifndef CVC4__KIND__METAKIND_H +#define CVC4__KIND__METAKIND_H #include <iosfwd> @@ -118,13 +118,13 @@ namespace kind { namespace metakind { /* these are #defines so their sum can be #if-checked in node_value.h */ -#define __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT 20 -#define __CVC4__EXPR__NODE_VALUE__NBITS__KIND 10 -#define __CVC4__EXPR__NODE_VALUE__NBITS__ID 40 -#define __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN 26 +#define CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT 20 +#define CVC4__EXPR__NODE_VALUE__NBITS__KIND 10 +#define CVC4__EXPR__NODE_VALUE__NBITS__ID 40 +#define CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN 26 static const unsigned MAX_CHILDREN = - (1u << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1; + (1u << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1; }/* CVC4::kind::metakind namespace */ }/* CVC4::kind namespace */ @@ -143,11 +143,11 @@ struct NodeValuePoolEq { #include "expr/node_value.h" -#endif /* __CVC4__KIND__METAKIND_H */ +#endif /* CVC4__KIND__METAKIND_H */ ${metakind_includes} -#ifdef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP +#ifdef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP namespace CVC4 { @@ -234,4 +234,4 @@ ${theory_alternate_doc}"; }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */ +#endif /* CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */ diff --git a/src/expr/node.h b/src/expr/node.h index cd7a1f839..935cde308 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -19,8 +19,8 @@ // circular dependency #include "expr/node_value.h" -#ifndef __CVC4__NODE_H -#define __CVC4__NODE_H +#ifndef CVC4__NODE_H +#define CVC4__NODE_H #include <stdint.h> @@ -1570,4 +1570,4 @@ static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>& }/* CVC4 namespace */ -#endif /* __CVC4__NODE_H */ +#endif /* CVC4__NODE_H */ diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index 0ed6e159b..656f162ae 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__EXPR__NODE_ALGORITHM_H -#define __CVC4__EXPR__NODE_ALGORITHM_H +#ifndef CVC4__EXPR__NODE_ALGORITHM_H +#define CVC4__EXPR__NODE_ALGORITHM_H #include <unordered_map> #include <vector> diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 299960c1d..9128bc190 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -152,8 +152,8 @@ #include "expr/node.h" #include "expr/type_node.h" -#ifndef __CVC4__NODE_BUILDER_H -#define __CVC4__NODE_BUILDER_H +#ifndef CVC4__NODE_BUILDER_H +#define CVC4__NODE_BUILDER_H #include <cstdlib> #include <iostream> @@ -274,7 +274,7 @@ class NodeBuilder { */ inline void realloc() { size_t newSize = 2 * size_t(d_nvMaxChildren); - size_t hardLimit = (1lu << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1; + size_t hardLimit = (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1; realloc(__builtin_expect( ( newSize > hardLimit ), false ) ? hardLimit : newSize); } @@ -774,9 +774,9 @@ template <unsigned nchild_thresh> void NodeBuilder<nchild_thresh>::realloc(size_t toSize) { Assert( toSize > d_nvMaxChildren, "attempt to realloc() a NodeBuilder to a smaller/equal size!" ); - Assert( toSize < (1lu << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN), + Assert( toSize < (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN), "attempt to realloc() a NodeBuilder to size %u (beyond hard limit of %u)", - toSize, (1lu << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1 ); + toSize, (1lu << CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1 ); if(__builtin_expect( ( nvIsAllocated() ), false )) { // Ensure d_nv is not modified on allocation failure @@ -1342,4 +1342,4 @@ std::ostream& operator<<(std::ostream& out, const NodeBuilder<nchild_thresh>& nb }/* CVC4 namespace */ -#endif /* __CVC4__NODE_BUILDER_H */ +#endif /* CVC4__NODE_BUILDER_H */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 30512c41e..510e6d585 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -25,8 +25,8 @@ #include "expr/expr.h" #include "expr/expr_manager.h" -#ifndef __CVC4__NODE_MANAGER_H -#define __CVC4__NODE_MANAGER_H +#ifndef CVC4__NODE_MANAGER_H +#define CVC4__NODE_MANAGER_H #include <vector> #include <string> @@ -1215,9 +1215,9 @@ inline TypeNode NodeManager::fromType(Type t) { }/* CVC4 namespace */ -#define __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP +#define CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP #include "expr/metakind.h" -#undef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP +#undef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP #include "expr/node_builder.h" @@ -1559,4 +1559,4 @@ NodeClass NodeManager::mkConstInternal(const T& val) { }/* CVC4 namespace */ -#endif /* __CVC4__NODE_MANAGER_H */ +#endif /* CVC4__NODE_MANAGER_H */ diff --git a/src/expr/node_manager_listeners.h b/src/expr/node_manager_listeners.h index 019a785d4..501c6129f 100644 --- a/src/expr/node_manager_listeners.h +++ b/src/expr/node_manager_listeners.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__EXPR__NODE_MANAGER_LISTENERS_H -#define __CVC4__EXPR__NODE_MANAGER_LISTENERS_H +#ifndef CVC4__EXPR__NODE_MANAGER_LISTENERS_H +#define CVC4__EXPR__NODE_MANAGER_LISTENERS_H #include "base/listener.h" #include "util/resource_manager.h" @@ -64,4 +64,4 @@ class RlimitPerListener : public Listener { }/* CVC4::expr namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__EXPR__NODE_MANAGER_LISTENERS_H */ +#endif /* CVC4__EXPR__NODE_MANAGER_LISTENERS_H */ diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h index e81d4c524..7e0478acc 100644 --- a/src/expr/node_self_iterator.h +++ b/src/expr/node_self_iterator.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__EXPR__NODE_SELF_ITERATOR_H -#define __CVC4__EXPR__NODE_SELF_ITERATOR_H +#ifndef CVC4__EXPR__NODE_SELF_ITERATOR_H +#define CVC4__EXPR__NODE_SELF_ITERATOR_H #include <iterator> @@ -125,4 +125,4 @@ inline bool NodeSelfIterator::operator!=(NodeSelfIterator i) const { }/* CVC4::expr namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__EXPR__NODE_SELF_ITERATOR_H */ +#endif /* CVC4__EXPR__NODE_SELF_ITERATOR_H */ diff --git a/src/expr/node_trie.h b/src/expr/node_trie.h index bc2e17ed0..7aa740a42 100644 --- a/src/expr/node_trie.h +++ b/src/expr/node_trie.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__EXPR__NODE_TRIE_H -#define __CVC4__EXPR__NODE_TRIE_H +#ifndef CVC4__EXPR__NODE_TRIE_H +#define CVC4__EXPR__NODE_TRIE_H #include <map> #include "expr/node.h" @@ -109,4 +109,4 @@ typedef NodeTemplateTrie<false> TNodeTrie; } // namespace theory } // namespace CVC4 -#endif /* __CVC4__EXPR__NODE_TRIE_H */ +#endif /* CVC4__EXPR__NODE_TRIE_H */ diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 4881033cb..024a13941 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -23,8 +23,8 @@ // circular dependency #include "expr/metakind.h" -#ifndef __CVC4__EXPR__NODE_VALUE_H -#define __CVC4__EXPR__NODE_VALUE_H +#ifndef CVC4__EXPR__NODE_VALUE_H +#define CVC4__EXPR__NODE_VALUE_H #include <stdint.h> @@ -59,10 +59,10 @@ namespace kind { namespace expr { -#if __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT + \ - __CVC4__EXPR__NODE_VALUE__NBITS__KIND + \ - __CVC4__EXPR__NODE_VALUE__NBITS__ID + \ - __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN != 96 +#if CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT + \ + CVC4__EXPR__NODE_VALUE__NBITS__KIND + \ + CVC4__EXPR__NODE_VALUE__NBITS__ID + \ + CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN != 96 # error NodeValue header bit assignment does not sum to 96 ! #endif /* sum != 96 */ @@ -71,10 +71,10 @@ namespace expr { */ class NodeValue { - static const unsigned NBITS_REFCOUNT = __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT; - static const unsigned NBITS_KIND = __CVC4__EXPR__NODE_VALUE__NBITS__KIND; - static const unsigned NBITS_ID = __CVC4__EXPR__NODE_VALUE__NBITS__ID; - static const unsigned NBITS_NCHILDREN = __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN; + static const unsigned NBITS_REFCOUNT = CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT; + static const unsigned NBITS_KIND = CVC4__EXPR__NODE_VALUE__NBITS__KIND; + static const unsigned NBITS_ID = CVC4__EXPR__NODE_VALUE__NBITS__ID; + static const unsigned NBITS_NCHILDREN = CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN; /** Maximum reference count possible. Used for sticky * reference-counting. Should be (1 << num_bits(d_rc)) - 1 */ @@ -549,4 +549,4 @@ static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue* }/* CVC4 namespace */ -#endif /* __CVC4__EXPR__NODE_VALUE_H */ +#endif /* CVC4__EXPR__NODE_VALUE_H */ diff --git a/src/expr/pickle_data.h b/src/expr/pickle_data.h index af91fbbea..316b6285c 100644 --- a/src/expr/pickle_data.h +++ b/src/expr/pickle_data.h @@ -20,8 +20,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PICKLE_DATA_H -#define __CVC4__PICKLE_DATA_H +#ifndef CVC4__PICKLE_DATA_H +#define CVC4__PICKLE_DATA_H #include <sstream> #include <deque> @@ -44,8 +44,8 @@ namespace expr { namespace pickle { const unsigned NBITS_BLOCK = 64; -const unsigned NBITS_KIND = __CVC4__EXPR__NODE_VALUE__NBITS__KIND; -const unsigned NBITS_NCHILDREN = __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN; +const unsigned NBITS_KIND = CVC4__EXPR__NODE_VALUE__NBITS__KIND; +const unsigned NBITS_NCHILDREN = CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN; const unsigned NBITS_CONSTBLOCKS = 32; struct BlockHeader { @@ -117,4 +117,4 @@ public: }/* CVC4::expr namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__PICKLE_DATA_H */ +#endif /* CVC4__PICKLE_DATA_H */ diff --git a/src/expr/pickler.h b/src/expr/pickler.h index f0d219eeb..02abdf18d 100644 --- a/src/expr/pickler.h +++ b/src/expr/pickler.h @@ -18,8 +18,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__PICKLER_H -#define __CVC4__PICKLER_H +#ifndef CVC4__PICKLER_H +#define CVC4__PICKLER_H #include "expr/variable_type_map.h" #include "expr/expr.h" @@ -126,4 +126,4 @@ protected: }/* CVC4::expr namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__PICKLER_H */ +#endif /* CVC4__PICKLER_H */ diff --git a/src/expr/record.h b/src/expr/record.h index 98fb5c106..bfa5d9395 100644 --- a/src/expr/record.h +++ b/src/expr/record.h @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__RECORD_H -#define __CVC4__RECORD_H +#ifndef CVC4__RECORD_H +#define CVC4__RECORD_H #include <functional> #include <iostream> @@ -90,4 +90,4 @@ std::ostream& operator<<(std::ostream& os, const Record& r) CVC4_PUBLIC; }/* CVC4 namespace */ -#endif /* __CVC4__RECORD_H */ +#endif /* CVC4__RECORD_H */ diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index ec89dd8b3..07f557059 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__SYMBOL_TABLE_H -#define __CVC4__SYMBOL_TABLE_H +#ifndef CVC4__SYMBOL_TABLE_H +#define CVC4__SYMBOL_TABLE_H #include <memory> #include <string> @@ -246,4 +246,4 @@ class CVC4_PUBLIC SymbolTable { } // namespace CVC4 -#endif /* __CVC4__SYMBOL_TABLE_H */ +#endif /* CVC4__SYMBOL_TABLE_H */ diff --git a/src/expr/type.h b/src/expr/type.h index 943af2344..2c68c9e73 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -16,8 +16,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__TYPE_H -#define __CVC4__TYPE_H +#ifndef CVC4__TYPE_H +#define CVC4__TYPE_H #include <climits> #include <cstdint> @@ -665,4 +665,4 @@ class CVC4_PUBLIC TesterType : public Type { }/* CVC4 namespace */ -#endif /* __CVC4__TYPE_H */ +#endif /* CVC4__TYPE_H */ diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h index b88f6eb5c..8c03cea98 100644 --- a/src/expr/type_checker.h +++ b/src/expr/type_checker.h @@ -19,8 +19,8 @@ // ordering dependence #include "expr/node.h" -#ifndef __CVC4__EXPR__TYPE_CHECKER_H -#define __CVC4__EXPR__TYPE_CHECKER_H +#ifndef CVC4__EXPR__TYPE_CHECKER_H +#define CVC4__EXPR__TYPE_CHECKER_H namespace CVC4 { namespace expr { @@ -40,4 +40,4 @@ public: }/* CVC4::expr namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__EXPR__TYPE_CHECKER_H */ +#endif /* CVC4__EXPR__TYPE_CHECKER_H */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 6babc104d..8ed26596b 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -19,8 +19,8 @@ // circular dependency #include "expr/node_value.h" -#ifndef __CVC4__TYPE_NODE_H -#define __CVC4__TYPE_NODE_H +#ifndef CVC4__TYPE_NODE_H +#define CVC4__TYPE_NODE_H #include <stdint.h> @@ -1072,4 +1072,4 @@ static void __attribute__((used)) debugPrintRawTypeNode(const TypeNode& n) { }/* CVC4 namespace */ -#endif /* __CVC4__NODE_H */ +#endif /* CVC4__NODE_H */ diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index 8d596ddaa..88447a125 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__TYPE_PROPERTIES_H -#define __CVC4__TYPE_PROPERTIES_H +#ifndef CVC4__TYPE_PROPERTIES_H +#define CVC4__TYPE_PROPERTIES_H #line 23 "${template}" @@ -138,4 +138,4 @@ ${type_groundterms} }/* CVC4::kind namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__TYPE_PROPERTIES_H */ +#endif /* CVC4__TYPE_PROPERTIES_H */ diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h index fe0521991..ba1c60549 100644 --- a/src/expr/variable_type_map.h +++ b/src/expr/variable_type_map.h @@ -17,8 +17,8 @@ #include "cvc4_public.h" -#ifndef __CVC4__VARIABLE_TYPE_MAP_H -#define __CVC4__VARIABLE_TYPE_MAP_H +#ifndef CVC4__VARIABLE_TYPE_MAP_H +#define CVC4__VARIABLE_TYPE_MAP_H #include <unordered_map> @@ -60,4 +60,4 @@ struct CVC4_PUBLIC ExprManagerMapCollection { }/* CVC4 namespace */ -#endif /* __CVC4__VARIABLE_MAP_H */ +#endif /* CVC4__VARIABLE_MAP_H */ |