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

Fixes 2887.

17 files changed, 49 insertions, 49 deletions

diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h
index 09e3ce10c..5472aa5a2 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__BV__ABSTRACTION_H
-#define __CVC4__THEORY__BV__ABSTRACTION_H
+#ifndef CVC4__THEORY__BV__ABSTRACTION_H
+#define CVC4__THEORY__BV__ABSTRACTION_H
 
 #include <unordered_map>
 #include <unordered_set>
diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
index cc821d333..8b63a9aa6 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
-#define __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
+#ifndef CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
+#define CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
 
 #include "theory/bv/bitblast/bitblaster.h"
 #include "prop/sat_solver.h"
@@ -111,4 +111,4 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*>
 }  // namespace bv
 }  // namespace theory
 }  // namespace CVC4
-#endif  //  __CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
+#endif  //  CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h
index 6b8cafb7b..9e668e258 100644
--- a/src/theory/bv/bitblast/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast/bitblast_strategies_template.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
-#define __CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
+#ifndef CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
+#define CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
 
 #include <cmath>
 #include <ostream>
diff --git a/src/theory/bv/bitblast/bitblast_utils.h b/src/theory/bv/bitblast/bitblast_utils.h
index a4c4261d2..f2bee22e5 100644
--- a/src/theory/bv/bitblast/bitblast_utils.h
+++ b/src/theory/bv/bitblast/bitblast_utils.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
-#define __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
+#ifndef CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
+#define CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
 
 
 #include <ostream>
@@ -269,4 +269,4 @@ T inline sLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqu
 }  // namespace theory
 }  // namespace CVC4
 
-#endif  // __CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
+#endif  // CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index f29882b0d..df7cc4f11 100644
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
-#define __CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
+#ifndef CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
+#define CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
 
 #include <unordered_map>
 #include <unordered_set>
@@ -286,4 +286,4 @@ Node TBitblaster<T>::getTermModel(TNode node, bool fullModel)
 }  // namespace theory
 }  // namespace CVC4
 
-#endif /* __CVC4__THEORY__BV__BITBLAST__BITBLASTER_H */
+#endif /* CVC4__THEORY__BV__BITBLAST__BITBLASTER_H */
diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index 296014b76..d407b8131 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
-#define __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+#ifndef CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+#define CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
 
 #include <unordered_set>
 
@@ -88,4 +88,4 @@ class BitblastingRegistrar : public prop::Registrar
 }  // namespace bv
 }  // namespace theory
 }  // namespace CVC4
-#endif  //  __CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+#endif  //  CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index 920b669a6..ac5cd5c7f 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
-#define __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+#ifndef CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+#define CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
 
 #include "proof/resolution_bitvector_proof.h"
 #include "theory/bv/bitblast/bitblaster.h"
@@ -176,4 +176,4 @@ class TLazyBitblaster : public TBitblaster<Node>
 }  // namespace bv
 }  // namespace theory
 }  // namespace CVC4
-#endif  //  __CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+#endif  //  CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 5322cca9a..8e42d5cab 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__BV__BV_EAGER_SOLVER_H
-#define __CVC4__THEORY__BV__BV_EAGER_SOLVER_H
+#ifndef CVC4__THEORY__BV__BV_EAGER_SOLVER_H
+#define CVC4__THEORY__BV__BV_EAGER_SOLVER_H
 
 #include <unordered_set>
 #include <vector>
@@ -68,4 +68,4 @@ class EagerBitblastSolver {
 }  // namespace theory
 }  // namespace CVC4
 
-#endif  // __CVC4__THEORY__BV__BV_EAGER_SOLVER_H
+#endif  // CVC4__THEORY__BV__BV_EAGER_SOLVER_H
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index a3a2f0445..07facf4af 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
-#define __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
+#ifndef CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
+#define CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
 
 #include <list>
 #include <queue>
@@ -282,4 +282,4 @@ public:
 }
 }
 
-#endif /* __CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H */
+#endif /* CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H */
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index c1ac95946..75f39b6e0 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__BV_QUICK_CHECK_H
-#define __CVC4__BV_QUICK_CHECK_H
+#ifndef CVC4__BV_QUICK_CHECK_H
+#define CVC4__BV_QUICK_CHECK_H
 
 #include <vector>
 #include <unordered_set>
@@ -172,4 +172,4 @@ public:
 } /* theory namespace */
 } /* CVC4 namespace */
 
-#endif /* __CVC4__BV_QUICK_CHECK_H */
+#endif /* CVC4__BV_QUICK_CHECK_H */
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 84a6f1b35..60660eda9 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -14,8 +14,8 @@
  ** Interface for bit-vectors sub-solvers.
  **/
 
-#ifndef __CVC4__THEORY__BV__BV_SUBTHEORY_H
-#define __CVC4__THEORY__BV__BV_SUBTHEORY_H
+#ifndef CVC4__THEORY__BV__BV_SUBTHEORY_H
+#define CVC4__THEORY__BV__BV_SUBTHEORY_H
 
 #include "cvc4_private.h"
 #include "context/context.h"
@@ -117,4 +117,4 @@ class SubtheorySolver {
 }  // namespace theory
 }  // namespace CVC4
 
-#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY_H */
+#endif /* CVC4__THEORY__BV__BV_SUBTHEORY_H */
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index b64b229f9..e18c886df 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
-#define __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
+#ifndef CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
+#define CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
 
 #include <unordered_set>
 
@@ -83,4 +83,4 @@ public:
 }
 }
 
-#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */
+#endif /* CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index ec715d2f5..3ddbcaf36 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -28,8 +28,8 @@
 #include "util/index.h"
 #include "util/statistics_registry.h"
 
-#ifndef __CVC4__THEORY__BV__SLICER_BV_H
-#define __CVC4__THEORY__BV__SLICER_BV_H
+#ifndef CVC4__THEORY__BV__SLICER_BV_H
+#define CVC4__THEORY__BV__SLICER_BV_H
 
 
 namespace CVC4 {
@@ -251,4 +251,4 @@ public:
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__BV__SLICER_BV_H */
+#endif /* CVC4__THEORY__BV__SLICER_BV_H */
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 55aad0ba7..7ca98f2ea 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__BV__THEORY_BV_H
-#define __CVC4__THEORY__BV__THEORY_BV_H
+#ifndef CVC4__THEORY__BV__THEORY_BV_H
+#define CVC4__THEORY__BV__THEORY_BV_H
 
 #include <unordered_map>
 #include <unordered_set>
@@ -273,4 +273,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__BV__THEORY_BV_H */
+#endif /* CVC4__THEORY__BV__THEORY_BV_H */
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 8009daf3c..bf707c268 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__BV__THEORY_BV_REWRITER_H
-#define __CVC4__THEORY__BV__THEORY_BV_REWRITER_H
+#ifndef CVC4__THEORY__BV__THEORY_BV_REWRITER_H
+#define CVC4__THEORY__BV__THEORY_BV_REWRITER_H
 
 #include "theory/rewriter.h"
 #include "util/statistics_registry.h"
@@ -109,4 +109,4 @@ public:
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__BV__THEORY_BV_REWRITER_H */
+#endif /* CVC4__THEORY__BV__THEORY_BV_REWRITER_H */
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 79c69b9f0..64d04a37e 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -18,8 +18,8 @@
 
 #include <algorithm>
 
-#ifndef __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
-#define __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
+#ifndef CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
+#define CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
 
 namespace CVC4 {
 namespace theory {
@@ -525,4 +525,4 @@ class BitVectorAckermanizationUremTypeRule
 }  // namespace theory
 }  // namespace CVC4
 
-#endif /* __CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */
+#endif /* CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */
diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
index 0bb67be42..90aae339b 100644
--- a/src/theory/bv/type_enumerator.h
+++ b/src/theory/bv/type_enumerator.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__BV__TYPE_ENUMERATOR_H
-#define __CVC4__THEORY__BV__TYPE_ENUMERATOR_H
+#ifndef CVC4__THEORY__BV__TYPE_ENUMERATOR_H
+#define CVC4__THEORY__BV__TYPE_ENUMERATOR_H
 
 #include "expr/kind.h"
 #include "expr/type_node.h"
@@ -63,4 +63,4 @@ public:
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__BV__TYPE_ENUMERATOR_H */
+#endif /* CVC4__THEORY__BV__TYPE_ENUMERATOR_H */