From 3e38bbb0094e97177d477156e356efbbfb2f7a5c Mon Sep 17 00:00:00 2001
From: Bruce Mitchener <bruce.mitchener@gmail.com>
Date: Sun, 24 Jul 2022 00:41:14 +0700
Subject: [PATCH] Make sure all headers do `#pragma once`. (#6188)

---
 src/api/z3_logger.h                                | 2 ++
 src/api/z3_macros.h                                | 2 +-
 src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h | 2 ++
 src/ast/rewriter/poly_rewriter_def.h               | 1 +
 src/ast/rewriter/rewriter_def.h                    | 2 ++
 src/cmd_context/extra_cmds/subpaving_cmds.h        | 1 +
 src/math/dd/pdd_eval.h                             | 2 ++
 src/math/dd/pdd_interval.h                         | 2 ++
 src/math/lp/binary_heap_priority_queue_def.h       | 2 ++
 src/math/lp/binary_heap_upair_queue_def.h          | 1 +
 src/math/lp/core_solver_pretty_printer_def.h       | 2 ++
 src/math/lp/dense_matrix_def.h                     | 2 ++
 src/math/lp/indexed_vector_def.h                   | 2 ++
 src/math/lp/lar_core_solver_def.h                  | 2 ++
 src/math/lp/lp_core_solver_base_def.h              | 2 ++
 src/math/lp/lp_dual_core_solver_def.h              | 2 ++
 src/math/lp/lp_dual_simplex_def.h                  | 2 ++
 src/math/lp/lp_primal_core_solver_def.h            | 2 ++
 src/math/lp/lp_primal_core_solver_tableau_def.h    | 2 ++
 src/math/lp/lp_primal_simplex_def.h                | 2 ++
 src/math/lp/lp_settings_def.h                      | 2 ++
 src/math/lp/lp_solver_def.h                        | 2 ++
 src/math/lp/lu_def.h                               | 2 ++
 src/math/lp/matrix_def.h                           | 1 +
 src/math/lp/permutation_matrix_def.h               | 2 ++
 src/math/lp/random_updater_def.h                   | 2 ++
 src/math/lp/row_eta_matrix_def.h                   | 2 ++
 src/math/lp/scaler_def.h                           | 2 ++
 src/math/lp/square_dense_submatrix_def.h           | 2 ++
 src/math/lp/square_sparse_matrix_def.h             | 1 +
 src/math/lp/static_matrix_def.h                    | 2 ++
 src/math/subpaving/subpaving_t_def.h               | 2 ++
 src/muz/base/dl_boogie_proof.h                     | 1 +
 src/muz/spacer/spacer_legacy_frames.h              | 1 +
 src/sat/sat_cutset_compute_shift.h                 | 1 +
 src/shell/options.h                                | 1 +
 src/smt/database.h                                 | 1 +
 src/smt/theory_pb.h                                | 1 +
 src/test/lp/argument_parser.h                      | 1 +
 src/test/lp/gomory_test.h                          | 2 ++
 src/util/max_cliques.h                             | 1 +
 41 files changed, 68 insertions(+), 1 deletion(-)

diff --git a/src/api/z3_logger.h b/src/api/z3_logger.h
index 6462095759b..2c95e18ca42 100644
--- a/src/api/z3_logger.h
+++ b/src/api/z3_logger.h
@@ -16,6 +16,8 @@ Module Name:
 Notes:
     
 --*/
+#pragma once
+
 #include "util/symbol.h"
 
 void R();
diff --git a/src/api/z3_macros.h b/src/api/z3_macros.h
index 08756cf152e..5f8659379e1 100644
--- a/src/api/z3_macros.h
+++ b/src/api/z3_macros.h
@@ -3,7 +3,7 @@
 Copyright (c) 2015 Microsoft Corporation
 
 --*/
-
+#pragma once
 
 #ifndef Z3_API
 # ifdef __GNUC__
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
index ae125a0adad..dc1df22a362 100644
--- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
+++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
@@ -16,6 +16,8 @@ Module Name:
 Revision History:
 
 --*/
+#pragma once
+
 #include "util/rational.h"
 #include "util/common_msgs.h"
 #include "ast/rewriter/bit_blaster/bit_blaster_tpl.h"
diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h
index eb72ddd67c9..0a17fc37537 100644
--- a/src/ast/rewriter/poly_rewriter_def.h
+++ b/src/ast/rewriter/poly_rewriter_def.h
@@ -16,6 +16,7 @@ Module Name:
 Notes:
 
 --*/
+#pragma once
 
 #include "util/container_util.h"
 #include "ast/rewriter/poly_rewriter.h"
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 4bf829be6b3..e9b9c316a95 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -16,6 +16,8 @@ Module Name:
 Notes:
 
 --*/
+#pragma once
+
 #include "ast/rewriter/rewriter.h"
 #include "ast/ast_smt2_pp.h"
 #include "ast/ast_ll_pp.h"
diff --git a/src/cmd_context/extra_cmds/subpaving_cmds.h b/src/cmd_context/extra_cmds/subpaving_cmds.h
index 33ed347b7f7..651d5b16194 100644
--- a/src/cmd_context/extra_cmds/subpaving_cmds.h
+++ b/src/cmd_context/extra_cmds/subpaving_cmds.h
@@ -15,6 +15,7 @@ Module Name:
 Notes:
 
 --*/
+#pragma once
 
 class cmd_context;
 
diff --git a/src/math/dd/pdd_eval.h b/src/math/dd/pdd_eval.h
index f7682927f85..9872935cf93 100644
--- a/src/math/dd/pdd_eval.h
+++ b/src/math/dd/pdd_eval.h
@@ -17,6 +17,8 @@ Module Name:
 Revision History:
 
 --*/
+#pragma once
+
 #include "math/dd/dd_pdd.h"
 
 namespace dd {
diff --git a/src/math/dd/pdd_interval.h b/src/math/dd/pdd_interval.h
index d8e2b8db150..c5b4c9e1c67 100644
--- a/src/math/dd/pdd_interval.h
+++ b/src/math/dd/pdd_interval.h
@@ -17,6 +17,8 @@ Module Name:
 Revision History:
 
 --*/
+#pragma once
+
 #include "math/dd/dd_pdd.h"
 #include "math/interval/dep_intervals.h"
 
diff --git a/src/math/lp/binary_heap_priority_queue_def.h b/src/math/lp/binary_heap_priority_queue_def.h
index c17d70fb273..0e640d949df 100644
--- a/src/math/lp/binary_heap_priority_queue_def.h
+++ b/src/math/lp/binary_heap_priority_queue_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "util/vector.h"
 #include "math/lp/binary_heap_priority_queue.h"
 namespace lp {
diff --git a/src/math/lp/binary_heap_upair_queue_def.h b/src/math/lp/binary_heap_upair_queue_def.h
index a74f9e46a3e..65485a6ebf8 100644
--- a/src/math/lp/binary_heap_upair_queue_def.h
+++ b/src/math/lp/binary_heap_upair_queue_def.h
@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+#pragma once
 
 #include <set>
 #include "math/lp/lp_utils.h"
diff --git a/src/math/lp/core_solver_pretty_printer_def.h b/src/math/lp/core_solver_pretty_printer_def.h
index 2f54b175a33..23417b691b6 100644
--- a/src/math/lp/core_solver_pretty_printer_def.h
+++ b/src/math/lp/core_solver_pretty_printer_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <limits>
 #include <string>
 #include <algorithm>
diff --git a/src/math/lp/dense_matrix_def.h b/src/math/lp/dense_matrix_def.h
index f781dbf8fa6..8eb9ad5dd50 100644
--- a/src/math/lp/dense_matrix_def.h
+++ b/src/math/lp/dense_matrix_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "math/lp/lp_settings.h"
 #ifdef Z3DEBUG
 #include "util/vector.h"
diff --git a/src/math/lp/indexed_vector_def.h b/src/math/lp/indexed_vector_def.h
index 443ca160e20..0e25ee27115 100644
--- a/src/math/lp/indexed_vector_def.h
+++ b/src/math/lp/indexed_vector_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "util/vector.h"
 #include "math/lp/indexed_vector.h"
 #include "math/lp/lp_settings.h"
diff --git a/src/math/lp/lar_core_solver_def.h b/src/math/lp/lar_core_solver_def.h
index f20aa7e6b0a..939a0511461 100644
--- a/src/math/lp/lar_core_solver_def.h
+++ b/src/math/lp/lar_core_solver_def.h
@@ -9,6 +9,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <string>
 #include "util/vector.h"
 #include "math/lp/lar_core_solver.h"
diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h
index 42c2ddcf709..c1b64492b62 100644
--- a/src/math/lp/lp_core_solver_base_def.h
+++ b/src/math/lp/lp_core_solver_base_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <set>
 #include <string>
 #include "util/vector.h"
diff --git a/src/math/lp/lp_dual_core_solver_def.h b/src/math/lp/lp_dual_core_solver_def.h
index 4a847fe8523..b42d644af34 100644
--- a/src/math/lp/lp_dual_core_solver_def.h
+++ b/src/math/lp/lp_dual_core_solver_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <algorithm>
 #include <string>
 #include "util/vector.h"
diff --git a/src/math/lp/lp_dual_simplex_def.h b/src/math/lp/lp_dual_simplex_def.h
index c21429c8807..8af9d87c104 100644
--- a/src/math/lp/lp_dual_simplex_def.h
+++ b/src/math/lp/lp_dual_simplex_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "math/lp/lp_dual_simplex.h"
 namespace lp{
 
diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h
index 75eff208a85..7b5dec945d6 100644
--- a/src/math/lp/lp_primal_core_solver_def.h
+++ b/src/math/lp/lp_primal_core_solver_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <list>
 #include "util/vector.h"
 #include <fstream>
diff --git a/src/math/lp/lp_primal_core_solver_tableau_def.h b/src/math/lp/lp_primal_core_solver_tableau_def.h
index 03f07115b7f..46297a63e14 100644
--- a/src/math/lp/lp_primal_core_solver_tableau_def.h
+++ b/src/math/lp/lp_primal_core_solver_tableau_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 // this is a part of lp_primal_core_solver that deals with the tableau
 #include "math/lp/lp_primal_core_solver.h"
 namespace lp {
diff --git a/src/math/lp/lp_primal_simplex_def.h b/src/math/lp/lp_primal_simplex_def.h
index e805ecc88db..7ffe819b207 100644
--- a/src/math/lp/lp_primal_simplex_def.h
+++ b/src/math/lp/lp_primal_simplex_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <string>
 #include "util/vector.h"
 #include "math/lp/lp_primal_simplex.h"
diff --git a/src/math/lp/lp_settings_def.h b/src/math/lp/lp_settings_def.h
index 4c783049cc4..2aba3594672 100644
--- a/src/math/lp/lp_settings_def.h
+++ b/src/math/lp/lp_settings_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <cmath>
 #include <string>
 #include "util/vector.h"
diff --git a/src/math/lp/lp_solver_def.h b/src/math/lp/lp_solver_def.h
index 4b5bc6db719..191832a2487 100644
--- a/src/math/lp/lp_solver_def.h
+++ b/src/math/lp/lp_solver_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <string>
 #include <algorithm>
 #include "util/vector.h"
diff --git a/src/math/lp/lu_def.h b/src/math/lp/lu_def.h
index df0f53730d8..80c9cdf0ed4 100644
--- a/src/math/lp/lu_def.h
+++ b/src/math/lp/lu_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <string>
 #include <algorithm>
 #include <set>
diff --git a/src/math/lp/matrix_def.h b/src/math/lp/matrix_def.h
index 8dba9d0b891..95810bd5a96 100644
--- a/src/math/lp/matrix_def.h
+++ b/src/math/lp/matrix_def.h
@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+#pragma once
 
 #include <cmath>
 #include <string>
diff --git a/src/math/lp/permutation_matrix_def.h b/src/math/lp/permutation_matrix_def.h
index c6ad20a396f..703830ffcf3 100644
--- a/src/math/lp/permutation_matrix_def.h
+++ b/src/math/lp/permutation_matrix_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "util/vector.h"
 #include "math/lp/permutation_matrix.h"
 namespace lp {
diff --git a/src/math/lp/random_updater_def.h b/src/math/lp/random_updater_def.h
index 25ef6f82f1f..7d167a4a03d 100644
--- a/src/math/lp/random_updater_def.h
+++ b/src/math/lp/random_updater_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "math/lp/random_updater.h"
 #include "math/lp/static_matrix.h"
 #include "math/lp/lar_solver.h"
diff --git a/src/math/lp/row_eta_matrix_def.h b/src/math/lp/row_eta_matrix_def.h
index 817d39481c0..faac5c6fe0b 100644
--- a/src/math/lp/row_eta_matrix_def.h
+++ b/src/math/lp/row_eta_matrix_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "util/vector.h"
 #include "math/lp/row_eta_matrix.h"
 namespace lp {
diff --git a/src/math/lp/scaler_def.h b/src/math/lp/scaler_def.h
index c05b25a167c..8604a67a131 100644
--- a/src/math/lp/scaler_def.h
+++ b/src/math/lp/scaler_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <algorithm>
 #include "math/lp/scaler.h"
 #include "math/lp/numeric_pair.h"
diff --git a/src/math/lp/square_dense_submatrix_def.h b/src/math/lp/square_dense_submatrix_def.h
index 8b565f92ec3..3a9006b4d9e 100644
--- a/src/math/lp/square_dense_submatrix_def.h
+++ b/src/math/lp/square_dense_submatrix_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "util/vector.h"
 #include "math/lp/square_dense_submatrix.h"
 namespace lp {
diff --git a/src/math/lp/square_sparse_matrix_def.h b/src/math/lp/square_sparse_matrix_def.h
index 0a2cffd61bd..3533ba066b5 100644
--- a/src/math/lp/square_sparse_matrix_def.h
+++ b/src/math/lp/square_sparse_matrix_def.h
@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+#pragma once
 
 #include "util/vector.h"
 #include "math/lp/square_sparse_matrix.h"
diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h
index 45d5d6d892b..af2eac36017 100644
--- a/src/math/lp/static_matrix_def.h
+++ b/src/math/lp/static_matrix_def.h
@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "util/vector.h"
 #include <utility>
 #include <set>
diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h
index c31e920abbb..89f6dad0fe1 100644
--- a/src/math/subpaving/subpaving_t_def.h
+++ b/src/math/subpaving/subpaving_t_def.h
@@ -16,6 +16,8 @@ Module Name:
 Revision History:
 
 --*/
+#pragma once
+
 #include "math/subpaving/subpaving_t.h"
 #include "math/interval/interval_def.h"
 #include "util/buffer.h"
diff --git a/src/muz/base/dl_boogie_proof.h b/src/muz/base/dl_boogie_proof.h
index ed2f5a801ce..5107d9529b7 100644
--- a/src/muz/base/dl_boogie_proof.h
+++ b/src/muz/base/dl_boogie_proof.h
@@ -3,6 +3,7 @@
 Copyright (c) 2015 Microsoft Corporation
 
 --*/
+#pragma once
 
 /**
 
diff --git a/src/muz/spacer/spacer_legacy_frames.h b/src/muz/spacer/spacer_legacy_frames.h
index 7ff4b6fad1a..cb78ec6a9cc 100644
--- a/src/muz/spacer/spacer_legacy_frames.h
+++ b/src/muz/spacer/spacer_legacy_frames.h
@@ -5,6 +5,7 @@
 
   Notes: this file is included from the middle of spacer_context.h
 */
+#pragma once
 
 class legacy_frames
 {
diff --git a/src/sat/sat_cutset_compute_shift.h b/src/sat/sat_cutset_compute_shift.h
index 7a9aff612ec..45d2e1de87a 100644
--- a/src/sat/sat_cutset_compute_shift.h
+++ b/src/sat/sat_cutset_compute_shift.h
@@ -18,6 +18,7 @@
     The truth table covers up to 6 inputs, which fits in 64 bits.
 
   --*/
+#pragma once
 
 static uint64_t compute_shift(uint64_t x, unsigned code) {
     switch (code) {
diff --git a/src/shell/options.h b/src/shell/options.h
index ee1de00fb99..39fe2fe8fb2 100644
--- a/src/shell/options.h
+++ b/src/shell/options.h
@@ -3,6 +3,7 @@
 Copyright (c) 2015 Microsoft Corporation
 
 --*/
+#pragma once
 
 
 /**
diff --git a/src/smt/database.h b/src/smt/database.h
index 3edb87f1f56..f1ce25f2612 100644
--- a/src/smt/database.h
+++ b/src/smt/database.h
@@ -3,6 +3,7 @@
 Copyright (c) 2015 Microsoft Corporation
 
 --*/
+#pragma once
 
 static char const g_pattern_database[] =
 "(benchmark patterns \n"
diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h
index 2d62bb7ac85..f713877b361 100644
--- a/src/smt/theory_pb.h
+++ b/src/smt/theory_pb.h
@@ -19,6 +19,7 @@ Module Name:
     It performs unit propagation and switches to creating
     sorting circuits if it keeps having to propagate (create new clauses).
 --*/
+#pragma once
 
 #include "smt/smt_theory.h"
 #include "ast/pb_decl_plugin.h"
diff --git a/src/test/lp/argument_parser.h b/src/test/lp/argument_parser.h
index f2a74f12233..12ab02831f3 100644
--- a/src/test/lp/argument_parser.h
+++ b/src/test/lp/argument_parser.h
@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+#pragma once
 
 #include <unordered_map>
 #include <vector>
diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h
index c7b0002cdce..890ff90e352 100644
--- a/src/test/lp/gomory_test.h
+++ b/src/test/lp/gomory_test.h
@@ -1,3 +1,5 @@
+#pragma once
+
 namespace lp {
 #include "math/lp/lp_utils.h"
 struct gomory_test {
diff --git a/src/util/max_cliques.h b/src/util/max_cliques.h
index 2841db60957..de68b6b108c 100644
--- a/src/util/max_cliques.h
+++ b/src/util/max_cliques.h
@@ -17,6 +17,7 @@ Module Name:
 
 
 --*/
+#pragma once
 
 #include "util/vector.h"
 #include "util/uint_set.h"