diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-04-24 15:39:24 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-04-24 15:39:24 -0700 |
commit | 2ab48defab1f0c8918cd7612c1943be7503e4d30 (patch) | |
tree | ab8fafc614f5fceef133a3a32f27a0fddcd3c717 /src/theory/bv | |
parent | 5f716f5aac730f976eac538cfbf47dcc651e54f7 (diff) |
Do not use __ prefix for header guards. (#2974)
Fixes 2887.
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/abstraction.h | 4 | ||||
-rw-r--r-- | src/theory/bv/bitblast/aig_bitblaster.h | 6 | ||||
-rw-r--r-- | src/theory/bv/bitblast/bitblast_strategies_template.h | 4 | ||||
-rw-r--r-- | src/theory/bv/bitblast/bitblast_utils.h | 6 | ||||
-rw-r--r-- | src/theory/bv/bitblast/bitblaster.h | 6 | ||||
-rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.h | 6 | ||||
-rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.h | 6 | ||||
-rw-r--r-- | src/theory/bv/bv_eager_solver.h | 6 | ||||
-rw-r--r-- | src/theory/bv/bv_inequality_graph.h | 6 | ||||
-rw-r--r-- | src/theory/bv/bv_quick_check.h | 6 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory.h | 6 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.h | 6 | ||||
-rw-r--r-- | src/theory/bv/slicer.h | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.h | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_type_rules.h | 6 | ||||
-rw-r--r-- | src/theory/bv/type_enumerator.h | 6 |
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 */ |