Rename CVC4__ header guards to CVC5__. (#6326)

13 files changed, 35 insertions, 35 deletions

diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index 66f0d8d1d..c7a6e596f 100644
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY_UF_STRONG_SOLVER_H
-#define CVC4__THEORY_UF_STRONG_SOLVER_H
+#ifndef CVC5__THEORY_UF_STRONG_SOLVER_H
+#define CVC5__THEORY_UF_STRONG_SOLVER_H
 
 #include "context/cdhashmap.h"
 #include "context/context.h"
@@ -465,4 +465,4 @@ class CardinalityExtension
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY_UF_STRONG_SOLVER_H */
+#endif /* CVC5__THEORY_UF_STRONG_SOLVER_H */
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 464e1d07a..a0375a77d 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__UF__EQUALITY_ENGINE_H
-#define CVC4__THEORY__UF__EQUALITY_ENGINE_H
+#ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_H
+#define CVC5__THEORY__UF__EQUALITY_ENGINE_H
 
 #include <deque>
 #include <queue>
diff --git a/src/theory/uf/equality_engine_iterator.h b/src/theory/uf/equality_engine_iterator.h
index 12dfea34a..8cd8bb686 100644
--- a/src/theory/uf/equality_engine_iterator.h
+++ b/src/theory/uf/equality_engine_iterator.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__UF__EQUALITY_ENGINE_ITERATOR_H
-#define CVC4__THEORY__UF__EQUALITY_ENGINE_ITERATOR_H
+#ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_ITERATOR_H
+#define CVC5__THEORY__UF__EQUALITY_ENGINE_ITERATOR_H
 
 #include "expr/node.h"
 #include "theory/uf/equality_engine_types.h"
diff --git a/src/theory/uf/equality_engine_notify.h b/src/theory/uf/equality_engine_notify.h
index 4187c067f..fff01402f 100644
--- a/src/theory/uf/equality_engine_notify.h
+++ b/src/theory/uf/equality_engine_notify.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
-#define CVC4__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
+#ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
+#define CVC5__THEORY__UF__EQUALITY_ENGINE_NOTIFY_H
 
 #include "expr/node.h"
 
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index 030c3b998..e2a271ceb 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H
-#define CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H
+#ifndef CVC5__THEORY__UF__EQUALITY_ENGINE_TYPES_H
+#define CVC5__THEORY__UF__EQUALITY_ENGINE_TYPES_H
 
 #include <string>
 #include <iostream>
@@ -361,4 +361,4 @@ struct TriggerInfo {
 } // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__UF__EQUALITY_ENGINE_TYPES_H */
+#endif /* CVC5__THEORY__UF__EQUALITY_ENGINE_TYPES_H */
diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h
index d703feb88..184be6522 100644
--- a/src/theory/uf/ho_extension.h
+++ b/src/theory/uf/ho_extension.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__UF__HO_EXTENSION_H
-#define __CVC4__THEORY__UF__HO_EXTENSION_H
+#ifndef __CVC5__THEORY__UF__HO_EXTENSION_H
+#define __CVC5__THEORY__UF__HO_EXTENSION_H
 
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
@@ -200,4 +200,4 @@ class HoExtension
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* __CVC4__THEORY__UF__HO_EXTENSION_H */
+#endif /* __CVC5__THEORY__UF__HO_EXTENSION_H */
diff --git a/src/theory/uf/proof_checker.h b/src/theory/uf/proof_checker.h
index 011b2868d..f3e20aea5 100644
--- a/src/theory/uf/proof_checker.h
+++ b/src/theory/uf/proof_checker.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__UF__PROOF_CHECKER_H
-#define CVC4__THEORY__UF__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__UF__PROOF_CHECKER_H
+#define CVC5__THEORY__UF__PROOF_CHECKER_H
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
@@ -46,4 +46,4 @@ class UfProofRuleChecker : public ProofRuleChecker
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__UF__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__UF__PROOF_CHECKER_H */
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index ca0b58b5d..a1545be8f 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
-#define CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
+#ifndef CVC5__THEORY__UF__PROOF_EQUALITY_ENGINE_H
+#define CVC5__THEORY__UF__PROOF_EQUALITY_ENGINE_H
 
 #include <vector>
 
@@ -298,4 +298,4 @@ class ProofEqEngine : public EagerProofGenerator
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__STRINGS__PROOF_MANAGER_H */
+#endif /* CVC5__THEORY__STRINGS__PROOF_MANAGER_H */
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index e38a1f67b..169794f3d 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -41,8 +41,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__UF__SYMMETRY_BREAKER_H
-#define CVC4__THEORY__UF__SYMMETRY_BREAKER_H
+#ifndef CVC5__THEORY__UF__SYMMETRY_BREAKER_H
+#define CVC5__THEORY__UF__SYMMETRY_BREAKER_H
 
 #include <iostream>
 #include <list>
@@ -179,4 +179,4 @@ std::ostream& operator<<(
 
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__UF__SYMMETRY_BREAKER_H */
+#endif /* CVC5__THEORY__UF__SYMMETRY_BREAKER_H */
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index cc53094b7..314ffa63c 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__UF__THEORY_UF_H
-#define CVC4__THEORY__UF__THEORY_UF_H
+#ifndef CVC5__THEORY__UF__THEORY_UF_H
+#define CVC5__THEORY__UF__THEORY_UF_H
 
 #include "expr/node.h"
 #include "expr/node_trie.h"
@@ -186,4 +186,4 @@ private:
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__UF__THEORY_UF_H */
+#endif /* CVC5__THEORY__UF__THEORY_UF_H */
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 949586976..74ce90650 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY_UF_MODEL_H
-#define CVC4__THEORY_UF_MODEL_H
+#ifndef CVC5__THEORY_UF_MODEL_H
+#define CVC5__THEORY_UF_MODEL_H
 
 #include <vector>
 
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index 60a394126..0681c3ece 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__UF__THEORY_UF_REWRITER_H
-#define CVC4__THEORY__UF__THEORY_UF_REWRITER_H
+#ifndef CVC5__THEORY__UF__THEORY_UF_REWRITER_H
+#define CVC5__THEORY__UF__THEORY_UF_REWRITER_H
 
 #include "expr/node_algorithm.h"
 #include "options/uf_options.h"
@@ -212,4 +212,4 @@ public: //conversion between HO_APPLY AND APPLY_UF
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__UF__THEORY_UF_REWRITER_H */
+#endif /* CVC5__THEORY__UF__THEORY_UF_REWRITER_H */
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 8493c8a38..dc8f3b462 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H
-#define CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H
+#ifndef CVC5__THEORY__UF__THEORY_UF_TYPE_RULES_H
+#define CVC5__THEORY__UF__THEORY_UF_TYPE_RULES_H
 
 #include <climits>
 
@@ -180,4 +180,4 @@ class HoApplyTypeRule {
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__UF__THEORY_UF_TYPE_RULES_H */
+#endif /* CVC5__THEORY__UF__THEORY_UF_TYPE_RULES_H */