summaryrefslogtreecommitdiff
path: root/src/theory/sets
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/sets')
-rw-r--r--src/theory/sets/cardinality_extension.h4
-rw-r--r--src/theory/sets/inference_manager.h6
-rw-r--r--src/theory/sets/normal_form.h4
-rw-r--r--src/theory/sets/singleton_op.h6
-rw-r--r--src/theory/sets/skolem_cache.h6
-rw-r--r--src/theory/sets/solver_state.h6
-rw-r--r--src/theory/sets/term_registry.h6
-rw-r--r--src/theory/sets/theory_sets.h6
-rw-r--r--src/theory/sets/theory_sets_private.h6
-rw-r--r--src/theory/sets/theory_sets_rewriter.h6
-rw-r--r--src/theory/sets/theory_sets_type_enumerator.h6
-rw-r--r--src/theory/sets/theory_sets_type_rules.h6
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback