summaryrefslogtreecommitdiff
path: root/src/theory/arrays
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays')
-rw-r--r--src/theory/arrays/array_info.h6
-rw-r--r--src/theory/arrays/inference_manager.h4
-rw-r--r--src/theory/arrays/proof_checker.h6
-rw-r--r--src/theory/arrays/skolem_cache.h4
-rw-r--r--src/theory/arrays/theory_arrays.h6
-rw-r--r--src/theory/arrays/theory_arrays_rewriter.h6
-rw-r--r--src/theory/arrays/theory_arrays_type_rules.h6
-rw-r--r--src/theory/arrays/type_enumerator.h6
-rw-r--r--src/theory/arrays/union_find.h6
9 files changed, 25 insertions, 25 deletions
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index 1a1cf441b..fc1754fdc 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -15,8 +15,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__ARRAY_INFO_H
-#define CVC4__THEORY__ARRAYS__ARRAY_INFO_H
+#ifndef CVC5__THEORY__ARRAYS__ARRAY_INFO_H
+#define CVC5__THEORY__ARRAYS__ARRAY_INFO_H
#include <tuple>
#include <unordered_map>
@@ -209,4 +209,4 @@ public:
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARRAYS__ARRAY_INFO_H */
+#endif /* CVC5__THEORY__ARRAYS__ARRAY_INFO_H */
diff --git a/src/theory/arrays/inference_manager.h b/src/theory/arrays/inference_manager.h
index 58b2b37bc..f70c986ed 100644
--- a/src/theory/arrays/inference_manager.h
+++ b/src/theory/arrays/inference_manager.h
@@ -14,8 +14,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__INFERENCE_MANAGER_H
-#define CVC4__THEORY__ARRAYS__INFERENCE_MANAGER_H
+#ifndef CVC5__THEORY__ARRAYS__INFERENCE_MANAGER_H
+#define CVC5__THEORY__ARRAYS__INFERENCE_MANAGER_H
#include "expr/node.h"
#include "expr/proof_rule.h"
diff --git a/src/theory/arrays/proof_checker.h b/src/theory/arrays/proof_checker.h
index b62f929a3..08c760493 100644
--- a/src/theory/arrays/proof_checker.h
+++ b/src/theory/arrays/proof_checker.h
@@ -14,8 +14,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__PROOF_CHECKER_H
-#define CVC4__THEORY__ARRAYS__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__ARRAYS__PROOF_CHECKER_H
+#define CVC5__THEORY__ARRAYS__PROOF_CHECKER_H
#include "expr/node.h"
#include "expr/proof_checker.h"
@@ -45,4 +45,4 @@ class ArraysProofRuleChecker : public ProofRuleChecker
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARRAYS__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__ARRAYS__PROOF_CHECKER_H */
diff --git a/src/theory/arrays/skolem_cache.h b/src/theory/arrays/skolem_cache.h
index fbd547079..81981fe66 100644
--- a/src/theory/arrays/skolem_cache.h
+++ b/src/theory/arrays/skolem_cache.h
@@ -14,8 +14,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__SKOLEM_CACHE_H
-#define CVC4__THEORY__ARRAYS__SKOLEM_CACHE_H
+#ifndef CVC5__THEORY__ARRAYS__SKOLEM_CACHE_H
+#define CVC5__THEORY__ARRAYS__SKOLEM_CACHE_H
#include "expr/node.h"
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 24772a5f0..cf1e216f2 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -16,8 +16,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
-#define CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
+#ifndef CVC5__THEORY__ARRAYS__THEORY_ARRAYS_H
+#define CVC5__THEORY__ARRAYS__THEORY_ARRAYS_H
#include <tuple>
#include <unordered_map>
@@ -494,4 +494,4 @@ class TheoryArrays : public Theory {
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H */
+#endif /* CVC5__THEORY__ARRAYS__THEORY_ARRAYS_H */
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 2d8da6929..a3e5c65c4 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -17,8 +17,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
-#define CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
+#ifndef CVC5__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
+#define CVC5__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
#include <unordered_map>
#include <unordered_set>
@@ -505,4 +505,4 @@ class TheoryArraysRewriter : public TheoryRewriter
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H */
+#endif /* CVC5__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H */
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index 5637639de..b2146a8cf 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -16,8 +16,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
-#define CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
+#ifndef CVC5__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
+#define CVC5__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
#include "theory/arrays/theory_arrays_rewriter.h" // for array-constant attributes
#include "theory/type_enumerator.h"
@@ -278,4 +278,4 @@ struct ArrayEqRangeTypeRule
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H */
+#endif /* CVC5__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H */
diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
index 715a3f7a5..0bb54b994 100644
--- a/src/theory/arrays/type_enumerator.h
+++ b/src/theory/arrays/type_enumerator.h
@@ -16,8 +16,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H
-#define CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H
+#ifndef CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H
+#define CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H
#include "theory/type_enumerator.h"
#include "expr/type_node.h"
@@ -159,4 +159,4 @@ class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H */
+#endif /* CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H */
diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h
index 6285e0e9b..938ddbea9 100644
--- a/src/theory/arrays/union_find.h
+++ b/src/theory/arrays/union_find.h
@@ -18,8 +18,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__ARRAYS__UNION_FIND_H
-#define CVC4__THEORY__ARRAYS__UNION_FIND_H
+#ifndef CVC5__THEORY__ARRAYS__UNION_FIND_H
+#define CVC5__THEORY__ARRAYS__UNION_FIND_H
#include <utility>
#include <vector>
@@ -139,4 +139,4 @@ inline void UnionFind<NodeType, NodeHash>::setCanon(TNode n, TNode newParent) {
} // namespace theory
} // namespace cvc5
-#endif /*CVC4__THEORY__ARRAYS__UNION_FIND_H */
+#endif /*CVC5__THEORY__ARRAYS__UNION_FIND_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback