diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-09 16:14:21 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-09 23:14:21 +0000 |
commit | 550c49a7dd2b13ea29743458336f0c0a0fb6099a (patch) | |
tree | b06962055a5de77d39c95fc577e54c0d7d69dcfd /src/theory/sets | |
parent | ca7e206c239d8de0f25fb23544e4923641b85d11 (diff) |
Rename CVC4__ header guards to CVC5__. (#6326)
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/cardinality_extension.h | 4 | ||||
-rw-r--r-- | src/theory/sets/inference_manager.h | 6 | ||||
-rw-r--r-- | src/theory/sets/normal_form.h | 4 | ||||
-rw-r--r-- | src/theory/sets/singleton_op.h | 6 | ||||
-rw-r--r-- | src/theory/sets/skolem_cache.h | 6 | ||||
-rw-r--r-- | src/theory/sets/solver_state.h | 6 | ||||
-rw-r--r-- | src/theory/sets/term_registry.h | 6 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.h | 6 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.h | 6 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rewriter.h | 6 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_enumerator.h | 6 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 6 |
12 files changed, 34 insertions, 34 deletions
diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h index c354f3f3a..7f426d003 100644 --- a/src/theory/sets/cardinality_extension.h +++ b/src/theory/sets/cardinality_extension.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__SETS__CARDINALITY_EXTENSION_H -#define CVC4__THEORY__SETS__CARDINALITY_EXTENSION_H +#ifndef CVC5__THEORY__SETS__CARDINALITY_EXTENSION_H +#define CVC5__THEORY__SETS__CARDINALITY_EXTENSION_H #include "context/cdhashset.h" #include "context/context.h" diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h index 90d2ce12a..0d7d437be 100644 --- a/src/theory/sets/inference_manager.h +++ b/src/theory/sets/inference_manager.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__SETS__INFERENCE_MANAGER_H -#define CVC4__THEORY__SETS__INFERENCE_MANAGER_H +#ifndef CVC5__THEORY__SETS__INFERENCE_MANAGER_H +#define CVC5__THEORY__SETS__INFERENCE_MANAGER_H #include "theory/inference_manager_buffered.h" #include "theory/sets/solver_state.h" @@ -102,4 +102,4 @@ class InferenceManager : public InferenceManagerBuffered } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__SETS__INFERENCE_MANAGER_H */ +#endif /* CVC5__THEORY__SETS__INFERENCE_MANAGER_H */ diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h index c0f02da7d..ae967cc39 100644 --- a/src/theory/sets/normal_form.h +++ b/src/theory/sets/normal_form.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__SETS__NORMAL_FORM_H -#define CVC4__THEORY__SETS__NORMAL_FORM_H +#ifndef CVC5__THEORY__SETS__NORMAL_FORM_H +#define CVC5__THEORY__SETS__NORMAL_FORM_H namespace cvc5 { namespace theory { diff --git a/src/theory/sets/singleton_op.h b/src/theory/sets/singleton_op.h index 7e338e518..591b9f0ee 100644 --- a/src/theory/sets/singleton_op.h +++ b/src/theory/sets/singleton_op.h @@ -14,8 +14,8 @@ #include "cvc4_public.h" -#ifndef CVC4__SINGLETON_OP_H -#define CVC4__SINGLETON_OP_H +#ifndef CVC5__SINGLETON_OP_H +#define CVC5__SINGLETON_OP_H #include <memory> @@ -60,4 +60,4 @@ struct SingletonOpHashFunction } // namespace cvc5 -#endif /* CVC4__SINGLETON_OP_H */ +#endif /* CVC5__SINGLETON_OP_H */ diff --git a/src/theory/sets/skolem_cache.h b/src/theory/sets/skolem_cache.h index 17e4bda71..f3e86cc96 100644 --- a/src/theory/sets/skolem_cache.h +++ b/src/theory/sets/skolem_cache.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__SETS__SKOLEM_CACHE_H -#define CVC4__THEORY__SETS__SKOLEM_CACHE_H +#ifndef CVC5__THEORY__SETS__SKOLEM_CACHE_H +#define CVC5__THEORY__SETS__SKOLEM_CACHE_H #include <map> #include <unordered_set> @@ -80,4 +80,4 @@ class SkolemCache } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__STRINGS__SKOLEM_CACHE_H */ +#endif /* CVC5__THEORY__STRINGS__SKOLEM_CACHE_H */ diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h index cbbb53d88..e6c742c86 100644 --- a/src/theory/sets/solver_state.h +++ b/src/theory/sets/solver_state.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H -#define CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H +#ifndef CVC5__THEORY__SETS__THEORY_SOLVER_STATE_H +#define CVC5__THEORY__SETS__THEORY_SOLVER_STATE_H #include <map> #include <vector> @@ -270,4 +270,4 @@ class SolverState : public TheoryState } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__SETS__THEORY_SOLVER_STATE_H */ +#endif /* CVC5__THEORY__SETS__THEORY_SOLVER_STATE_H */ diff --git a/src/theory/sets/term_registry.h b/src/theory/sets/term_registry.h index 3d1035c75..2cff01b86 100644 --- a/src/theory/sets/term_registry.h +++ b/src/theory/sets/term_registry.h @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__SETS__TERM_REGISTRY_H -#define CVC4__THEORY__SETS__TERM_REGISTRY_H +#ifndef CVC5__THEORY__SETS__TERM_REGISTRY_H +#define CVC5__THEORY__SETS__TERM_REGISTRY_H #include <map> #include <vector> @@ -91,4 +91,4 @@ class TermRegistry } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__SETS__TERM_REGISTRY_H */ +#endif /* CVC5__THEORY__SETS__TERM_REGISTRY_H */ diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 14f4b5699..5aa145a15 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__SETS__THEORY_SETS_H -#define CVC4__THEORY__SETS__THEORY_SETS_H +#ifndef CVC5__THEORY__SETS__THEORY_SETS_H +#define CVC5__THEORY__SETS__THEORY_SETS_H #include <memory> @@ -124,4 +124,4 @@ class TheorySets : public Theory } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__SETS__THEORY_SETS_H */ +#endif /* CVC5__THEORY__SETS__THEORY_SETS_H */ diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 3c3469b07..94baa3c0e 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H -#define CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H +#ifndef CVC5__THEORY__SETS__THEORY_SETS_PRIVATE_H +#define CVC5__THEORY__SETS__THEORY_SETS_PRIVATE_H #include "context/cdhashset.h" #include "context/cdqueue.h" @@ -240,4 +240,4 @@ class TheorySetsPrivate { } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H */ +#endif /* CVC5__THEORY__SETS__THEORY_SETS_PRIVATE_H */ diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h index 501a58430..9c81c1e67 100644 --- a/src/theory/sets/theory_sets_rewriter.h +++ b/src/theory/sets/theory_sets_rewriter.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H -#define CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H +#ifndef CVC5__THEORY__SETS__THEORY_SETS_REWRITER_H +#define CVC5__THEORY__SETS__THEORY_SETS_REWRITER_H #include "theory/rewriter.h" @@ -81,4 +81,4 @@ private: } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H */ +#endif /* CVC5__THEORY__SETS__THEORY_SETS_REWRITER_H */ diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h index 006afc964..457aede12 100644 --- a/src/theory/sets/theory_sets_type_enumerator.h +++ b/src/theory/sets/theory_sets_type_enumerator.h @@ -17,8 +17,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__SETS__TYPE_ENUMERATOR_H -#define CVC4__THEORY__SETS__TYPE_ENUMERATOR_H +#ifndef CVC5__THEORY__SETS__TYPE_ENUMERATOR_H +#define CVC5__THEORY__SETS__TYPE_ENUMERATOR_H #include "expr/kind.h" #include "expr/type_node.h" @@ -70,4 +70,4 @@ class SetEnumerator : public TypeEnumeratorBase<SetEnumerator> } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__SETS__TYPE_ENUMERATOR_H */ +#endif /* CVC5__THEORY__SETS__TYPE_ENUMERATOR_H */ diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index ab82ba710..7b8aa9778 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H -#define CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H +#ifndef CVC5__THEORY__SETS__THEORY_SETS_TYPE_RULES_H +#define CVC5__THEORY__SETS__THEORY_SETS_TYPE_RULES_H #include <climits> @@ -446,4 +446,4 @@ struct SetsProperties { } // namespace theory } // namespace cvc5 -#endif /* CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H */ +#endif /* CVC5__THEORY__SETS__THEORY_SETS_TYPE_RULES_H */ |