From 0d949be444e52f42de4f920d71512c95ff96666d Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 19 Nov 2020 11:30:52 -0800 Subject: [PATCH] Include stddef.h (needed for size_t) in cvc4_public.h (#5476) This further removes obsolete explicit includes of stdint.h. --- src/context/cdhashmap.h | 1 - src/expr/attribute.h | 1 - src/expr/attribute_internals.h | 1 - src/expr/attribute_unique_id.h | 2 -- src/expr/expr_template.h | 1 - src/expr/kind_map.h | 1 - src/expr/node.h | 2 -- src/expr/node_builder.h | 1 - src/expr/node_traversal.h | 1 - src/expr/node_value.h | 2 -- src/expr/type.h | 1 - src/expr/type_node.h | 2 -- src/include/cvc4_public.h | 1 + src/options/options_template.cpp | 1 - src/parser/antlr_input.cpp | 1 - src/parser/cvc/Cvc.g | 1 - src/parser/memory_mapped_input_buffer.cpp | 1 - src/parser/parser.cpp | 2 -- src/parser/smt2/Smt2.g | 2 -- src/parser/tptp/Tptp.g | 1 - src/proof/sat_proof.h | 2 -- src/prop/sat_solver.h | 2 -- src/theory/arith/bound_counts.h | 2 -- src/theory/arith/fc_simplex.h | 2 -- src/theory/arith/nl/nonlinear_extension.h | 2 -- src/theory/arith/soi_simplex.h | 2 -- src/theory/arith/tableau_sizes.h | 1 - src/theory/arith/theory_arith_private.cpp | 2 -- src/theory/arith/theory_arith_private.h | 2 -- src/theory/strings/theory_strings_preprocess.cpp | 2 -- src/util/bitvector.h | 1 - src/util/gmp_util.h | 7 ------- src/util/hash.h | 1 - src/util/iand.h | 1 - src/util/index.cpp | 1 - src/util/index.h | 2 -- src/util/rational_gmp_imp.h | 6 ------ src/util/regexp.h | 1 - src/util/resource_manager.h | 1 - src/util/safe_print.h | 7 ------- src/util/statistics_registry.h | 2 -- src/util/string.h | 1 - 42 files changed, 1 insertion(+), 75 deletions(-) diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index afcfb00a9..07e928161 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -82,7 +82,6 @@ #ifndef CVC4__CONTEXT__CDHASHMAP_H #define CVC4__CONTEXT__CDHASHMAP_H -#include #include #include #include diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 2aa5c2fbc..1b5b6974d 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -25,7 +25,6 @@ #define CVC4__EXPR__ATTRIBUTE_H #include -#include #include "expr/attribute_unique_id.h" // include supporting templates diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index 37846cf45..e93656708 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -23,7 +23,6 @@ #ifndef CVC4__EXPR__ATTRIBUTE_INTERNALS_H #define CVC4__EXPR__ATTRIBUTE_INTERNALS_H -#include #include namespace CVC4 { diff --git a/src/expr/attribute_unique_id.h b/src/expr/attribute_unique_id.h index 2862e0d44..bf7c8926b 100644 --- a/src/expr/attribute_unique_id.h +++ b/src/expr/attribute_unique_id.h @@ -19,8 +19,6 @@ #pragma once -#include - // ATTRIBUTE IDs ============================================================ namespace CVC4 { diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 4c863184e..e62dee7f6 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -26,7 +26,6 @@ ${includes} #ifndef CVC4__EXPR_H #define CVC4__EXPR_H -#include #include #include #include diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h index e440fbc3d..996a32268 100644 --- a/src/expr/kind_map.h +++ b/src/expr/kind_map.h @@ -20,7 +20,6 @@ #ifndef CVC4__KIND_MAP_H #define CVC4__KIND_MAP_H -#include #include #include "base/check.h" diff --git a/src/expr/node.h b/src/expr/node.h index f18f27c81..75d4d2022 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -22,8 +22,6 @@ #ifndef CVC4__NODE_H #define CVC4__NODE_H -#include - #include #include #include diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index d8e15a60a..eaa9a46d5 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -158,7 +158,6 @@ #include #include #include -#include #include namespace CVC4 { diff --git a/src/expr/node_traversal.h b/src/expr/node_traversal.h index 1bc907019..e7e49db45 100644 --- a/src/expr/node_traversal.h +++ b/src/expr/node_traversal.h @@ -17,7 +17,6 @@ #ifndef CVC4__EXPR__NODE_TRAVERSAL_H #define CVC4__EXPR__NODE_TRAVERSAL_H -#include #include #include #include diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 66a7952c7..0635e983b 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -26,8 +26,6 @@ #ifndef CVC4__EXPR__NODE_VALUE_H #define CVC4__EXPR__NODE_VALUE_H -#include - #include #include diff --git a/src/expr/type.h b/src/expr/type.h index 6867673f8..69a8363dc 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -20,7 +20,6 @@ #define CVC4__TYPE_H #include -#include #include #include diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 895e05093..01e096c72 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -22,8 +22,6 @@ #ifndef CVC4__TYPE_NODE_H #define CVC4__TYPE_NODE_H -#include - #include #include #include diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h index 85a41dfd3..0e43335db 100644 --- a/src/include/cvc4_public.h +++ b/src/include/cvc4_public.h @@ -19,6 +19,7 @@ #ifndef CVC4_PUBLIC_H #define CVC4_PUBLIC_H +#include #include #if defined _WIN32 || defined __CYGWIN__ diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 8208da58b..af74fd31e 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -36,7 +36,6 @@ extern int optreset; #include #include -#include #include #include diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index e6d5c3f56..ef85dd1a9 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -18,7 +18,6 @@ #include #include -#include #include "base/output.h" #include "expr/type.h" diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index b62fb0bbb..fe14ce5fc 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -546,7 +546,6 @@ api::Term addNots(api::Solver* s, size_t n, api::Term e) { #include #include -#include #include "options/set_language.h" #include "parser/antlr_tracing.h" diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp index f73938db3..9cc1e7dd3 100644 --- a/src/parser/memory_mapped_input_buffer.cpp +++ b/src/parser/memory_mapped_input_buffer.cpp @@ -16,7 +16,6 @@ #include #include -#include #include diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index c5746020c..1fc995fd6 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -16,8 +16,6 @@ #include "parser/parser.h" -#include - #include #include #include diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index f81bfc163..88035dba4 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -63,8 +63,6 @@ options { }/* @lexer::includes */ @lexer::postinclude { -#include - #include "parser/smt2/smt2.h" #include "parser/antlr_input.h" diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 71c1de2fa..447a867c8 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -61,7 +61,6 @@ options { }/* @lexer::includes */ @lexer::postinclude { -#include #include "parser/tptp/tptp.h" #include "parser/antlr_input.h" diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index ebacbddb1..27c98d62a 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -19,8 +19,6 @@ #ifndef CVC4__SAT__PROOF_H #define CVC4__SAT__PROOF_H -#include - #include #include #include diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 583376a74..a842647bd 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -19,8 +19,6 @@ #ifndef CVC4__PROP__SAT_SOLVER_H #define CVC4__PROP__SAT_SOLVER_H -#include - #include #include "context/cdlist.h" diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h index 217af5641..d1044f36b 100644 --- a/src/theory/arith/bound_counts.h +++ b/src/theory/arith/bound_counts.h @@ -18,8 +18,6 @@ #include "cvc4_private.h" #pragma once -#include - #include "base/check.h" #include "theory/arith/arithvar.h" #include "util/dense_map.h" diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h index df2e05e5a..1bd4416e0 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -52,8 +52,6 @@ #pragma once -#include - #include "theory/arith/simplex.h" #include "util/dense_map.h" #include "util/statistics_registry.h" diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index bd3042231..21b978a55 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -18,8 +18,6 @@ #ifndef CVC4__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H #define CVC4__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H -#include - #include #include diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h index d8c73c400..b6df9b488 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -52,8 +52,6 @@ #pragma once -#include - #include "theory/arith/simplex.h" #include "util/dense_map.h" #include "util/statistics_registry.h" diff --git a/src/theory/arith/tableau_sizes.h b/src/theory/arith/tableau_sizes.h index 4dc25d80c..76914e04a 100644 --- a/src/theory/arith/tableau_sizes.h +++ b/src/theory/arith/tableau_sizes.h @@ -20,7 +20,6 @@ #pragma once -#include #include "theory/arith/arithvar.h" namespace CVC4 { diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 2f758e621..a684e1895 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -17,8 +17,6 @@ #include "theory/arith/theory_arith_private.h" -#include - #include #include #include diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 3abf17c3d..31435221f 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -17,8 +17,6 @@ #pragma once -#include - #include #include #include diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 936f60ed2..81ec79327 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -16,8 +16,6 @@ #include "theory/strings/theory_strings_preprocess.h" -#include - #include "expr/kind.h" #include "options/smt_options.h" #include "options/strings_options.h" diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 3ca410f72..997293639 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -19,7 +19,6 @@ #ifndef CVC4__BITVECTOR_H #define CVC4__BITVECTOR_H -#include #include #include "base/exception.h" diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h index c50bac71f..995579c3b 100644 --- a/src/util/gmp_util.h +++ b/src/util/gmp_util.h @@ -20,13 +20,6 @@ #ifndef CVC4__GMP_UTIL_H #define CVC4__GMP_UTIL_H -/* - * Older versions of GMP in combination with newer versions of GCC and C++11 - * cause errors: https://gcc.gnu.org/gcc-4.9/porting_to.html - * Including is a workaround for this issue. - */ -#include - #include namespace CVC4 { diff --git a/src/util/hash.h b/src/util/hash.h index dc1d19b5e..6f6af2bd7 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -20,7 +20,6 @@ #ifndef CVC4__HASH_H #define CVC4__HASH_H -#include #include #include diff --git a/src/util/iand.h b/src/util/iand.h index 5b0cbb628..68380824f 100644 --- a/src/util/iand.h +++ b/src/util/iand.h @@ -17,7 +17,6 @@ #ifndef CVC4__IAND_H #define CVC4__IAND_H -#include #include #include "base/exception.h" diff --git a/src/util/index.cpp b/src/util/index.cpp index 37b5f60a9..73fc54907 100644 --- a/src/util/index.cpp +++ b/src/util/index.cpp @@ -17,7 +17,6 @@ #include "util/index.h" -#include #include namespace CVC4 { diff --git a/src/util/index.h b/src/util/index.h index 1954e4365..d37ddb43e 100644 --- a/src/util/index.h +++ b/src/util/index.h @@ -19,8 +19,6 @@ #ifndef CVC4__INDEX_H #define CVC4__INDEX_H -#include - namespace CVC4 { /** Index is a standardized unsigned integer used for efficient indexing. */ diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index 12a696857..f166d9cdc 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -20,14 +20,8 @@ #ifndef CVC4__RATIONAL_H #define CVC4__RATIONAL_H -/* - * Older versions of GMP in combination with newer versions of GCC and C++11 - * cause errors: https://gcc.gnu.org/gcc-4.9/porting_to.html - * Including is a workaround for this issue. - */ #include -#include #include #include "base/exception.h" diff --git a/src/util/regexp.h b/src/util/regexp.h index abd76fff7..42c1b39d5 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -17,7 +17,6 @@ #ifndef CVC4__UTIL__REGEXP_H #define CVC4__UTIL__REGEXP_H -#include #include namespace CVC4 { diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index f6cff2e7f..3be99021b 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -24,7 +24,6 @@ #include #include -#include #include #include "base/exception.h" diff --git a/src/util/safe_print.h b/src/util/safe_print.h index b16441260..6f72569bb 100644 --- a/src/util/safe_print.h +++ b/src/util/safe_print.h @@ -37,13 +37,6 @@ #ifndef CVC4__SAFE_PRINT_H #define CVC4__SAFE_PRINT_H -#if __cplusplus >= 201103L -// For c++11 and newer -#include -#else -#include -#endif - #include #include diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 186b09307..f706f3321 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -36,8 +36,6 @@ #ifndef CVC4__STATISTICS_REGISTRY_H #define CVC4__STATISTICS_REGISTRY_H -#include - #include #include #include diff --git a/src/util/string.h b/src/util/string.h index 3fce6ea2e..7102ec1f2 100644 --- a/src/util/string.h +++ b/src/util/string.h @@ -17,7 +17,6 @@ #ifndef CVC4__UTIL__STRING_H #define CVC4__UTIL__STRING_H -#include #include #include #include -- 2.30.2