diff options
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/array_info.h | 6 | ||||
-rw-r--r-- | src/theory/arrays/inference_manager.h | 4 | ||||
-rw-r--r-- | src/theory/arrays/proof_checker.h | 6 | ||||
-rw-r--r-- | src/theory/arrays/skolem_cache.h | 4 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 6 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 6 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.h | 6 | ||||
-rw-r--r-- | src/theory/arrays/type_enumerator.h | 6 | ||||
-rw-r--r-- | src/theory/arrays/union_find.h | 6 |
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 */ |