Do not use __ prefix for header guards. (#2974)

Fixes 2887.

24 files changed, 70 insertions, 70 deletions

diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index a93bf4c57..a1df24fac 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__ARITH__PROOF_H
-#define __CVC4__ARITH__PROOF_H
+#ifndef CVC4__ARITH__PROOF_H
+#define CVC4__ARITH__PROOF_H
 
 #include <memory>
 #include <unordered_set>
@@ -172,4 +172,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__ARITH__PROOF_H */
+#endif /* CVC4__ARITH__PROOF_H */
diff --git a/src/proof/arith_proof_recorder.h b/src/proof/arith_proof_recorder.h
index fe7bffbd0..3fff6968d 100644
--- a/src/proof/arith_proof_recorder.h
+++ b/src/proof/arith_proof_recorder.h
@@ -42,8 +42,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__ARITH_PROOF_RECORDER_H
-#define __CVC4__PROOF__ARITH_PROOF_RECORDER_H
+#ifndef CVC4__PROOF__ARITH_PROOF_RECORDER_H
+#define CVC4__PROOF__ARITH_PROOF_RECORDER_H
 
 #include <map>
 #include <set>
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index 7e3340af0..372ad1f67 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__ARRAY__PROOF_H
-#define __CVC4__ARRAY__PROOF_H
+#ifndef CVC4__ARRAY__PROOF_H
+#define CVC4__ARRAY__PROOF_H
 
 #include <memory>
 #include <unordered_set>
@@ -117,4 +117,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__ARRAY__PROOF_H */
+#endif /* CVC4__ARRAY__PROOF_H */
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 91c07fcb5..f0a0717fa 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__BITVECTOR_PROOF_H
-#define __CVC4__BITVECTOR_PROOF_H
+#ifndef CVC4__BITVECTOR_PROOF_H
+#define CVC4__BITVECTOR_PROOF_H
 
 #include <set>
 #include <unordered_map>
@@ -276,4 +276,4 @@ class BitVectorProof : public TheoryProof
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__BITVECTOR__PROOF_H */
+#endif /* CVC4__BITVECTOR__PROOF_H */
diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h
index b53bcd5e2..b10b1ad1c 100644
--- a/src/proof/clausal_bitvector_proof.h
+++ b/src/proof/clausal_bitvector_proof.h
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
-#define __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
+#ifndef CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
+#define CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
 
 #include <iostream>
 #include <sstream>
@@ -135,4 +135,4 @@ class LfscErBitVectorProof : public LfscClausalBitVectorProof
 
 }  // namespace CVC4
 
-#endif /* __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H */
+#endif /* CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H */
diff --git a/src/proof/clause_id.h b/src/proof/clause_id.h
index e8b9841c8..4a9ebc74a 100644
--- a/src/proof/clause_id.h
+++ b/src/proof/clause_id.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__CLAUSE_ID_H
-#define __CVC4__PROOF__CLAUSE_ID_H
+#ifndef CVC4__PROOF__CLAUSE_ID_H
+#define CVC4__PROOF__CLAUSE_ID_H
 
 namespace CVC4 {
 
@@ -30,4 +30,4 @@ typedef unsigned ClauseId;
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__PROOF__CLAUSE_ID_H */
+#endif /* CVC4__PROOF__CLAUSE_ID_H */
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index a17777c66..e589950bc 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__CNF_PROOF_H
-#define __CVC4__CNF_PROOF_H
+#ifndef CVC4__CNF_PROOF_H
+#define CVC4__CNF_PROOF_H
 
 #include <iosfwd>
 #include <unordered_map>
@@ -212,4 +212,4 @@ public:
 
 } /* CVC4 namespace */
 
-#endif /* __CVC4__CNF_PROOF_H */
+#endif /* CVC4__CNF_PROOF_H */
diff --git a/src/proof/dimacs_printer.h b/src/proof/dimacs_printer.h
index f46cb51ec..2ae4abefa 100644
--- a/src/proof/dimacs_printer.h
+++ b/src/proof/dimacs_printer.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__DIMACS_PRINTER_H
-#define __CVC4__PROOF__DIMACS_PRINTER_H
+#ifndef CVC4__PROOF__DIMACS_PRINTER_H
+#define CVC4__PROOF__DIMACS_PRINTER_H
 
 #include <iosfwd>
 #include <memory>
@@ -63,4 +63,4 @@ void printDimacs(
 }  // namespace proof
 }  // namespace CVC4
 
-#endif  // __CVC4__PROOF__DIMACS_PRINTER_H
+#endif  // CVC4__PROOF__DIMACS_PRINTER_H
diff --git a/src/proof/drat/drat_proof.h b/src/proof/drat/drat_proof.h
index c4b7c2e02..082107d0a 100644
--- a/src/proof/drat/drat_proof.h
+++ b/src/proof/drat/drat_proof.h
@@ -19,8 +19,8 @@
  **
  **/
 
-#ifndef __CVC4__PROOF__DRAT__DRAT_PROOF_H
-#define __CVC4__PROOF__DRAT__DRAT_PROOF_H
+#ifndef CVC4__PROOF__DRAT__DRAT_PROOF_H
+#define CVC4__PROOF__DRAT__DRAT_PROOF_H
 
 #include "cvc4_private.h"
 #include "prop/sat_solver.h"
@@ -137,4 +137,4 @@ class DratProof
 }  // namespace proof
 }  // namespace CVC4
 
-#endif  // __CVC4__PROOF__DRAT__DRAT_PROOF_H
+#endif  // CVC4__PROOF__DRAT__DRAT_PROOF_H
diff --git a/src/proof/er/er_proof.h b/src/proof/er/er_proof.h
index 0a0038738..f5af0783b 100644
--- a/src/proof/er/er_proof.h
+++ b/src/proof/er/er_proof.h
@@ -23,8 +23,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__ER__ER_PROOF_H
-#define __CVC4__PROOF__ER__ER_PROOF_H
+#ifndef CVC4__PROOF__ER__ER_PROOF_H
+#define CVC4__PROOF__ER__ER_PROOF_H
 
 #include <memory>
 #include <vector>
@@ -205,4 +205,4 @@ class ErProof
 }  // namespace proof
 }  // namespace CVC4
 
-#endif  // __CVC4__PROOF__ER__ER_PROOF_H
+#endif  // CVC4__PROOF__ER__ER_PROOF_H
diff --git a/src/proof/lemma_proof.h b/src/proof/lemma_proof.h
index b4b40ef1b..7dfce57cf 100644
--- a/src/proof/lemma_proof.h
+++ b/src/proof/lemma_proof.h
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__LEMMA_PROOF_H
-#define __CVC4__LEMMA_PROOF_H
+#ifndef CVC4__LEMMA_PROOF_H
+#define CVC4__LEMMA_PROOF_H
 
 #include "expr/expr.h"
 #include "proof/clause_id.h"
@@ -112,4 +112,4 @@ std::ostream& operator<<(std::ostream & out, const LemmaProofRecipe & recipe);
 
 } /* CVC4 namespace */
 
-#endif /* __CVC4__LEMMA_PROOF_H */
+#endif /* CVC4__LEMMA_PROOF_H */
diff --git a/src/proof/lfsc_proof_printer.h b/src/proof/lfsc_proof_printer.h
index beef4823e..f2f55aa94 100644
--- a/src/proof/lfsc_proof_printer.h
+++ b/src/proof/lfsc_proof_printer.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__LFSC_PROOF_PRINTER_H
-#define __CVC4__PROOF__LFSC_PROOF_PRINTER_H
+#ifndef CVC4__PROOF__LFSC_PROOF_PRINTER_H
+#define CVC4__PROOF__LFSC_PROOF_PRINTER_H
 
 #include <iosfwd>
 #include <string>
@@ -151,4 +151,4 @@ class LFSCProofPrinter
 }  // namespace proof
 }  // namespace CVC4
 
-#endif /* __CVC4__PROOF__LFSC_PROOF_PRINTER_H */
+#endif /* CVC4__PROOF__LFSC_PROOF_PRINTER_H */
diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h
index f231e5a6b..33b2fad3f 100644
--- a/src/proof/lrat/lrat_proof.h
+++ b/src/proof/lrat/lrat_proof.h
@@ -23,8 +23,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__LRAT__LRAT_PROOF_H
-#define __CVC4__PROOF__LRAT__LRAT_PROOF_H
+#ifndef CVC4__PROOF__LRAT__LRAT_PROOF_H
+#define CVC4__PROOF__LRAT__LRAT_PROOF_H
 
 #include <iosfwd>
 #include <string>
diff --git a/src/proof/proof.h b/src/proof/proof.h
index b39d73134..9e7e20a22 100644
--- a/src/proof/proof.h
+++ b/src/proof/proof.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__PROOF_H
-#define __CVC4__PROOF__PROOF_H
+#ifndef CVC4__PROOF__PROOF_H
+#define CVC4__PROOF__PROOF_H
 
 #include "options/smt_options.h"
 
@@ -67,4 +67,4 @@
 # define PSTATS(x)
 #endif /* CVC4_PROOF_STATS */
 
-#endif /* __CVC4__PROOF__PROOF_H */
+#endif /* CVC4__PROOF__PROOF_H */
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 0d3250b12..eb5942bea 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF_MANAGER_H
-#define __CVC4__PROOF_MANAGER_H
+#ifndef CVC4__PROOF_MANAGER_H
+#define CVC4__PROOF_MANAGER_H
 
 #include <iosfwd>
 #include <memory>
@@ -351,4 +351,4 @@ std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k);
 
 
 
-#endif /* __CVC4__PROOF_MANAGER_H */
+#endif /* CVC4__PROOF_MANAGER_H */
diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h
index 9bf1e0e5c..ff84a3743 100644
--- a/src/proof/proof_output_channel.h
+++ b/src/proof/proof_output_channel.h
@@ -13,8 +13,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H
-#define __CVC4__PROOF_OUTPUT_CHANNEL_H
+#ifndef CVC4__PROOF_OUTPUT_CHANNEL_H
+#define CVC4__PROOF_OUTPUT_CHANNEL_H
 
 #include <memory>
 #include <set>
@@ -74,4 +74,4 @@ public:
 
 } /* CVC4 namespace */
 
-#endif /* __CVC4__PROOF_OUTPUT_CHANNEL_H */
+#endif /* CVC4__PROOF_OUTPUT_CHANNEL_H */
diff --git a/src/proof/resolution_bitvector_proof.h b/src/proof/resolution_bitvector_proof.h
index 24d1bc76f..5fd11092f 100644
--- a/src/proof/resolution_bitvector_proof.h
+++ b/src/proof/resolution_bitvector_proof.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
-#define __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
+#ifndef CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
+#define CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
 
 #include <iosfwd>
 
@@ -110,4 +110,4 @@ class LfscResolutionBitVectorProof : public ResolutionBitVectorProof
 
 }  // namespace CVC4
 
-#endif /* __CVC4__PROOF__RESOLUTIONBITVECTORPROOF_H */
+#endif /* CVC4__PROOF__RESOLUTIONBITVECTORPROOF_H */
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 82bd93947..ec0928c07 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__SAT__PROOF_H
-#define __CVC4__SAT__PROOF_H
+#ifndef CVC4__SAT__PROOF_H
+#define CVC4__SAT__PROOF_H
 
 #include <stdint.h>
 
@@ -373,4 +373,4 @@ void toSatClause(const typename Solver::TClause& minisat_cl,
 
 } /* CVC4 namespace */
 
-#endif /* __CVC4__SAT__PROOF_H */
+#endif /* CVC4__SAT__PROOF_H */
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index bc32b7959..d9c959ae4 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__SAT__PROOF_IMPLEMENTATION_H
-#define __CVC4__SAT__PROOF_IMPLEMENTATION_H
+#ifndef CVC4__SAT__PROOF_IMPLEMENTATION_H
+#define CVC4__SAT__PROOF_IMPLEMENTATION_H
 
 #include "proof/clause_id.h"
 #include "proof/cnf_proof.h"
@@ -1081,4 +1081,4 @@ inline std::ostream& operator<<(std::ostream& out, CVC4::ClauseKind k) {
 
 } /* CVC4 namespace */
 
-#endif /* __CVC4__SAT__PROOF_IMPLEMENTATION_H */
+#endif /* CVC4__SAT__PROOF_IMPLEMENTATION_H */
diff --git a/src/proof/simplify_boolean_node.h b/src/proof/simplify_boolean_node.h
index 0b1cf4990..fe8b7174b 100644
--- a/src/proof/simplify_boolean_node.h
+++ b/src/proof/simplify_boolean_node.h
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__SIMPLIFY_BOOLEAN_NODE_H
-#define __CVC4__SIMPLIFY_BOOLEAN_NODE_H
+#ifndef CVC4__SIMPLIFY_BOOLEAN_NODE_H
+#define CVC4__SIMPLIFY_BOOLEAN_NODE_H
 
 namespace CVC4 {
 
@@ -24,4 +24,4 @@ Node simplifyBooleanNode(const Node &n);
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__SIMPLIFY_BOOLEAN_NODE_H */
+#endif /* CVC4__SIMPLIFY_BOOLEAN_NODE_H */
diff --git a/src/proof/skolemization_manager.h b/src/proof/skolemization_manager.h
index 54b30e6f0..cb23268f3 100644
--- a/src/proof/skolemization_manager.h
+++ b/src/proof/skolemization_manager.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__SKOLEMIZATION_MANAGER_H
-#define __CVC4__SKOLEMIZATION_MANAGER_H
+#ifndef CVC4__SKOLEMIZATION_MANAGER_H
+#define CVC4__SKOLEMIZATION_MANAGER_H
 
 #include <iostream>
 #include <unordered_map>
@@ -52,4 +52,4 @@ private:
 
 
 
-#endif /* __CVC4__SKOLEMIZATION_MANAGER_H */
+#endif /* CVC4__SKOLEMIZATION_MANAGER_H */
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 94765d95a..b487b62a8 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY_PROOF_H
-#define __CVC4__THEORY_PROOF_H
+#ifndef CVC4__THEORY_PROOF_H
+#define CVC4__THEORY_PROOF_H
 
 #include <iosfwd>
 #include <unordered_map>
@@ -401,4 +401,4 @@ public:
 
 } /* CVC4 namespace */
 
-#endif /* __CVC4__THEORY_PROOF_H */
+#endif /* CVC4__THEORY_PROOF_H */
diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index e5fd396c5..ca8b3f90e 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__UF__PROOF_H
-#define __CVC4__UF__PROOF_H
+#ifndef CVC4__UF__PROOF_H
+#define CVC4__UF__PROOF_H
 
 #include <memory>
 #include <unordered_set>
@@ -102,4 +102,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__UF__PROOF_H */
+#endif /* CVC4__UF__PROOF_H */
diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h
index 6e0c84840..0217b6326 100644
--- a/src/proof/unsat_core.h
+++ b/src/proof/unsat_core.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__UNSAT_CORE_H
-#define __CVC4__UNSAT_CORE_H
+#ifndef CVC4__UNSAT_CORE_H
+#define CVC4__UNSAT_CORE_H
 
 #include <iosfwd>
 #include <vector>
@@ -71,4 +71,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__UNSAT_CORE_H */
+#endif /* CVC4__UNSAT_CORE_H */