Include stddef.h (needed for size_t) in cvc4_public.h (#5476)

This further removes obsolete explicit includes of stdint.h.

42 files changed, 1 insertions, 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 <cstddef>
 #include <functional>
 #include <iterator>
 #include <unordered_map>
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 <string>
-#include <stdint.h>
 #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 <cstdint>
 #include <unordered_map>
 
 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 <stdint.h>
-
 // 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 <stdint.h>
 #include <iosfwd>
 #include <iterator>
 #include <string>
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 <stdint.h>
 #include <iterator>
 
 #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 <stdint.h>
-
 #include <algorithm>
 #include <functional>
 #include <iostream>
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 <cstdlib>
 #include <iostream>
 #include <memory>
-#include <stdint.h>
 #include <vector>
 
 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 <cstddef>
 #include <functional>
 #include <iterator>
 #include <unordered_map>
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 <stdint.h>
-
 #include <iterator>
 #include <string>
 
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 <climits>
-#include <cstdint>
 #include <string>
 #include <vector>
 
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 <stdint.h>
-
 #include <iostream>
 #include <string>
 #include <unordered_map>
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 <stddef.h>
 #include <stdint.h>
 
 #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 <unistd.h>
 #include <string.h>
-#include <stdint.h>
 #include <time.h>
 
 #include <cstdio>
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 <antlr3.h>
 #include <limits.h>
-#include <stdint.h>
 
 #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 <cassert>
 #include <memory>
-#include <stdint.h>
 
 #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 <fcntl.h>
 #include <stdio.h>
-#include <stdint.h>
 
 #include <antlr3input.h>
 
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 <stdint.h>
-
 #include <cassert>
 #include <fstream>
 #include <iostream>
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 <stdint.h>
-
 #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 <stdint.h>
 
 #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 <stdint.h>
-
 #include <iosfwd>
 #include <set>
 #include <sstream>
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 <stdint.h>
-
 #include <string>
 
 #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 <stdint.h>
-
 #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 <stdint.h>
-
 #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 <stdint.h>
-
 #include <map>
 #include <vector>
 
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 <stdint.h>
-
 #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 <stdint.h>
 #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 <stdint.h>
-
 #include <map>
 #include <queue>
 #include <vector>
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 <stdint.h>
-
 #include <map>
 #include <queue>
 #include <vector>
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 <stdint.h>
-
 #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 <cstdint>
 #include <iosfwd>
 
 #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 <cstddef> is a workaround for this issue.
- */
-#include <cstddef>
-
 #include <gmpxx.h>
 
 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 <cstdint>
 #include <functional>
 #include <string>
 
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 <cstdint>
 #include <iosfwd>
 
 #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 <cstddef>
 #include <limits>
 
 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 <cstdint>
-
 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 <cstddef> is a workaround for this issue.
- */
 #include <gmp.h>
 
-#include <cstddef>
 #include <string>
 
 #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 <cstdint>
 #include <iosfwd>
 
 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 <sys/time.h>
 
 #include <chrono>
-#include <cstddef>
 #include <memory>
 
 #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 <cstdint>
-#else
-#include <stdint.h>
-#endif
-
 #include <unistd.h>
 
 #include <cstring>
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 <stdint.h>
-
 #include <ctime>
 #include <iomanip>
 #include <map>
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 <cstddef>
 #include <functional>
 #include <ostream>
 #include <string>