Make sure all headers do #pragma once. (#6188)

src/api/z3_logger.h

@@ -16,6 +16,8 @@ Module Name:
 Notes:
     
 --*/
+#pragma once
+
 #include "util/symbol.h"
 
 void R();

src/api/z3_macros.h

@@ -3,7 +3,7 @@
 Copyright (c) 2015 Microsoft Corporation
 
 --*/
-
+#pragma once
 
 #ifndef Z3_API
 # ifdef __GNUC__

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"

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"

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"

src/cmd_context/extra_cmds/subpaving_cmds.h

@@ -15,6 +15,7 @@ Module Name:
 Notes:
 
 --*/
+#pragma once
 
 class cmd_context;
 

src/math/dd/pdd_eval.h

@@ -17,6 +17,8 @@ Module Name:
 Revision History:
 
 --*/
+#pragma once
+
 #include "math/dd/dd_pdd.h"
 
 namespace dd {

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"
 

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 {

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"

src/math/lp/core_solver_pretty_printer_def.h

@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <limits>
 #include <string>
 #include <algorithm>

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"

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"

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"

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"

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"

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{
 

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>

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 {

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"

src/math/lp/lp_settings_def.h

@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <cmath>
 #include <string>
 #include "util/vector.h"

src/math/lp/lp_solver_def.h

@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <string>
 #include <algorithm>
 #include "util/vector.h"

src/math/lp/lu_def.h

@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include <string>
 #include <algorithm>
 #include <set>

src/math/lp/matrix_def.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+#pragma once
 
 #include <cmath>
 #include <string>

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 {

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"

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 {

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"

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 {

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"

src/math/lp/static_matrix_def.h

@@ -17,6 +17,8 @@ Revision History:
 
 
 --*/
+#pragma once
+
 #include "util/vector.h"
 #include <utility>
 #include <set>

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"

src/muz/base/dl_boogie_proof.h

@@ -3,6 +3,7 @@
 Copyright (c) 2015 Microsoft Corporation
 
 --*/
+#pragma once
 
 /**
 

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
 {

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) {

src/shell/options.h

@@ -3,6 +3,7 @@
 Copyright (c) 2015 Microsoft Corporation
 
 --*/
+#pragma once
 
 
 /**

src/smt/database.h

@@ -3,6 +3,7 @@
 Copyright (c) 2015 Microsoft Corporation
 
 --*/
+#pragma once
 
 static char const g_pattern_database[] =
 "(benchmark patterns \n"

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"

src/test/lp/argument_parser.h

@@ -17,6 +17,7 @@ Revision History:
 
 
 --*/
+#pragma once
 
 #include <unordered_map>
 #include <vector>

src/test/lp/gomory_test.h

@@ -1,3 +1,5 @@
+#pragma once
+
 namespace lp {
 #include "math/lp/lp_utils.h"
 struct gomory_test {

src/util/max_cliques.h

@@ -17,6 +17,7 @@ Module Name:
 
 
 --*/
+#pragma once
 
 #include "util/vector.h"
 #include "util/uint_set.h"