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

This further removes obsolete explicit includes of stdint.h.

diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index afcfb00a98e4d4b26f8c8dd70abd91c84897d44e..07e9281616809c40cdb96fa2efaa8120cc94d76a 100644 (file)
--- 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 2aa5c2fbc2775ec8d5e9d7a3046cd6be2c5639b0..1b5b6974d5e7051c2d20384f3d113a540b21d0cb 100644 (file)
--- 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 37846cf4550819cdcd9c35d51a18e71c331c6213..e93656708b9f9aef88ebd74b66f885332b753654 100644 (file)
--- 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 2862e0d44cdb3af1f3f9406fe1fbbf81f857be54..bf7c8926bf44d7e32dddfe034cd06a96cde41db1 100644 (file)
--- 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 4c863184ec4e7b314e8ea0e37851f8b13bb4a880..e62dee7f6bda39645ca949e94dcb07a9c8205ac6 100644 (file)
--- 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 e440fbc3df5826c9b53a54a609dd73514a14c9f8..996a3226883aa5320a3d4bfee0ceae2984ebe854 100644 (file)
--- 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 f18f27c81bb7a5d0488c706a5fb2c5f467b8235c..75d4d2022da18d2fe73326cd8028c563a898f6e3 100644 (file)
--- 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 d8e15a60a69c0189c3044fe59185bf4361deff1e..eaa9a46d59650fe73e7eef1d3f929af54da8a1ff 100644 (file)
--- 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 1bc90701907ee8c1e3dbcb793655795326dd15d6..e7e49db45556da276d75949d6cb47c7fef73664e 100644 (file)
--- 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 66a7952c7abff8fe4abea2042ff127ab7c91a8a2..0635e983b200e837a8e0fbd03f45cda7e1f01a0f 100644 (file)
--- 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 6867673f80e529e0f3cf0af23f3319cf49d8efaf..69a8363dc2d7d13d5a998bebbcb3bd2be3e9f80e 100644 (file)
--- 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 895e05093be3d243c434be2778e87657c04e7db4..01e096c720c7b0b836d486c26b3737afa56c9057 100644 (file)
--- 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 85a41dfd30904b6ee894e2b7463a368be19b3204..0e43335dba88e3a4293afe51b2f67caa76051419 100644 (file)
--- 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 8208da58b5132f1b3cb0a7e7c3d09da972e688ad..af74fd31e11d462b9708fe1d39684aa135754965 100644 (file)
--- 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 e6d5c3f56e6c525d1d8f9f1630d201b2627f446a..ef85dd1a9459ac607d5ed23d13daf2fd9eccb4f0 100644 (file)
--- 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 b62fb0bbb44c495d37a7f3a440a665995dd5de69..fe14ce5fca02bc96777f8d21280faebdea3d0f0a 100644 (file)
--- 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 f73938db3cd4fc2daa3a6384eb89f593288719ef..9cc1e7dd35b1046172669844f2b856455de6f3b8 100644 (file)
--- 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 c5746020c86679c242ee8c20b04492d53d898efb..1fc995fd64593f9b49429039824cea942d02b582 100644 (file)
--- 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 f81bfc163d213bf77a590557806d201180afe98b..88035dba4bf343b23853a72df8c8920a8133ce88 100644 (file)
--- 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 71c1de2faa9ea67dd163e88594ef10345da2df18..447a867c83ea4b4b1fb5238a28f327c007adad8f 100644 (file)
--- 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 ebacbddb19d24e73ffdb897f66f3a845e0819d2c..27c98d62a31e20b678c23d4a45d23807f487153d 100644 (file)
--- 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 583376a74407661397303f797119ac0f6610b413..a842647bd09280b5cb2cbc50e5c438a27b52b5c1 100644 (file)
--- 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 217af56415b5fbde000e36eb4bc5ef9991cc20dd..d1044f36b2108ba0e423b6992beae4c0b1ca44b2 100644 (file)
--- 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 df2e05e5a9cf2f65c30ec59543b8c77045e63738..1bd4416e03f22de965871d67fcd58b1247660295 100644 (file)
--- 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 bd30422313a5d89c75465160ccffb409ee3427e9..21b978a5549fde3ecc82283ae3291d8498debb9a 100644 (file)
--- 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 d8c73c40094e989c12f1d4b3a5ed1da24a1dd02c..b6df9b488cdd4d5e77aada2d9ba2414ca493cec7 100644 (file)
--- 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 4dc25d80cc07545e9591564417629107a36fd15d..76914e04a2465336ef6e1efdaec31973dd864a2e 100644 (file)
--- 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 2f758e62160f0dd5df13ea0d747549df358b44a0..a684e18953c35ccc81e13d2b117eb8fc76454dd5 100644 (file)
--- 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 3abf17c3dfcb3363d3e5de38a4f0138f71cb4e4a..31435221fb528a7c4dfeed01a23d0b6c01c8998a 100644 (file)
--- 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 936f60ed2a3efab0a7920024a229194b326ae881..81ec79327a3aa2e1751396439c7e94ba18610131 100644 (file)
--- 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 3ca410f72e11334bab8e76c44009cab70824fa53..997293639ce3fc223b652455637d4e2102d0175b 100644 (file)
--- 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 c50bac71fff74c9c80b82060c8475ee850823166..995579c3bbfb59361ca6a3ee5984869456df6069 100644 (file)
--- 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 dc1d19b5e1228545807412f51095565839364406..6f6af2bd775157b0443adc050c4aae2300426e26 100644 (file)
--- 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 5b0cbb6288bfe5b7f739b7530ad1d0906e18f8f3..68380824f18715cf0f67257e7be314ed51594fff 100644 (file)
--- 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 37b5f60a99b4f3567779f396cf573c4b2054f7c1..73fc54907bce05ca60653c43a69feb3205ca957b 100644 (file)
--- 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 1954e4365b44e59c981098b4ccab49d7485c7f29..d37ddb43eb2f8e1060744c4c467b3b7ea8de5d36 100644 (file)
--- 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 12a696857e6719b4a5950ac7570dd631cea85fd7..f166d9cdc3f00c45a57eea99202350ce53565b21 100644 (file)
--- 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 abd76fff7eb3462ef688046ef89849c4ac0198aa..42c1b39d53934de492ead5e017af16cdb0cca82c 100644 (file)
--- 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 f6cff2e7fd3f24374268efeebd57300986df56c6..3be99021b8fae6eb58d8bd98382e599da22d1225 100644 (file)
--- 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 b164412609401d13691a4e328b43f74e8f6532bb..6f72569bb90a15b5ec8d1219216a93c3a9b8966e 100644 (file)
--- 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 186b0930779e9f1eb53b3064408ab8ae3c66df70..f706f3321feb60fed9589908375fd3df46794489 100644 (file)
--- 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 3fce6ea2e240e58d12f7c4a9214e8a53b436c22b..7102ec1f2cf179f11653f48dd1f75ed2efd42ca4 100644 (file)
--- 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>