summaryrefslogtreecommitdiff
path: root/src/theory/bags
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bags')
-rw-r--r--src/theory/bags/bag_solver.h6
-rw-r--r--src/theory/bags/bags_rewriter.h6
-rw-r--r--src/theory/bags/bags_statistics.h6
-rw-r--r--src/theory/bags/infer_info.h6
-rw-r--r--src/theory/bags/inference_generator.h6
-rw-r--r--src/theory/bags/inference_manager.h6
-rw-r--r--src/theory/bags/make_bag_op.h6
-rw-r--r--src/theory/bags/normal_form.h6
-rw-r--r--src/theory/bags/rewrites.h6
-rw-r--r--src/theory/bags/solver_state.h6
-rw-r--r--src/theory/bags/term_registry.h6
-rw-r--r--src/theory/bags/theory_bags.h6
-rw-r--r--src/theory/bags/theory_bags_type_enumerator.h6
-rw-r--r--src/theory/bags/theory_bags_type_rules.h6
14 files changed, 42 insertions, 42 deletions
diff --git a/src/theory/bags/bag_solver.h b/src/theory/bags/bag_solver.h
index 5cd7ed338..191fd481c 100644
--- a/src/theory/bags/bag_solver.h
+++ b/src/theory/bags/bag_solver.h
@@ -14,8 +14,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAG__SOLVER_H
-#define CVC4__THEORY__BAG__SOLVER_H
+#ifndef CVC5__THEORY__BAG__SOLVER_H
+#define CVC5__THEORY__BAG__SOLVER_H
#include "theory/bags/inference_generator.h"
@@ -92,4 +92,4 @@ class BagSolver
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAG__SOLVER_H */
+#endif /* CVC5__THEORY__BAG__SOLVER_H */
diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h
index bc66d7efa..26686bcc0 100644
--- a/src/theory/bags/bags_rewriter.h
+++ b/src/theory/bags/bags_rewriter.h
@@ -14,8 +14,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H
-#define CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H
+#ifndef CVC5__THEORY__BAGS__THEORY_BAGS_REWRITER_H
+#define CVC5__THEORY__BAGS__THEORY_BAGS_REWRITER_H
#include "theory/bags/rewrites.h"
#include "theory/theory_rewriter.h"
@@ -225,4 +225,4 @@ class BagsRewriter : public TheoryRewriter
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H */
+#endif /* CVC5__THEORY__BAGS__THEORY_BAGS_REWRITER_H */
diff --git a/src/theory/bags/bags_statistics.h b/src/theory/bags/bags_statistics.h
index ac60fbc3e..58765a996 100644
--- a/src/theory/bags/bags_statistics.h
+++ b/src/theory/bags/bags_statistics.h
@@ -14,8 +14,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS_STATISTICS_H
-#define CVC4__THEORY__BAGS_STATISTICS_H
+#ifndef CVC5__THEORY__BAGS_STATISTICS_H
+#define CVC5__THEORY__BAGS_STATISTICS_H
#include "theory/bags/rewrites.h"
#include "util/statistics_registry.h"
@@ -42,4 +42,4 @@ class BagsStatistics
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS_STATISTICS_H */
+#endif /* CVC5__THEORY__BAGS_STATISTICS_H */
diff --git a/src/theory/bags/infer_info.h b/src/theory/bags/infer_info.h
index 508c49fe5..633c3a828 100644
--- a/src/theory/bags/infer_info.h
+++ b/src/theory/bags/infer_info.h
@@ -14,8 +14,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__INFER_INFO_H
-#define CVC4__THEORY__BAGS__INFER_INFO_H
+#ifndef CVC5__THEORY__BAGS__INFER_INFO_H
+#define CVC5__THEORY__BAGS__INFER_INFO_H
#include <map>
#include <vector>
@@ -87,4 +87,4 @@ std::ostream& operator<<(std::ostream& out, const InferInfo& ii);
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__INFER_INFO_H */
+#endif /* CVC5__THEORY__BAGS__INFER_INFO_H */
diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h
index baa391f38..639fd3215 100644
--- a/src/theory/bags/inference_generator.h
+++ b/src/theory/bags/inference_generator.h
@@ -14,8 +14,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H
-#define CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H
+#ifndef CVC5__THEORY__BAGS__INFERENCE_GENERATOR_H
+#define CVC5__THEORY__BAGS__INFERENCE_GENERATOR_H
#include "expr/node.h"
#include "infer_info.h"
@@ -190,4 +190,4 @@ class InferenceGenerator
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H */
+#endif /* CVC5__THEORY__BAGS__INFERENCE_GENERATOR_H */
diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h
index 68d923889..f17a6828b 100644
--- a/src/theory/bags/inference_manager.h
+++ b/src/theory/bags/inference_manager.h
@@ -14,8 +14,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__INFERENCE_MANAGER_H
-#define CVC4__THEORY__BAGS__INFERENCE_MANAGER_H
+#ifndef CVC5__THEORY__BAGS__INFERENCE_MANAGER_H
+#define CVC5__THEORY__BAGS__INFERENCE_MANAGER_H
#include "theory/inference_manager_buffered.h"
@@ -65,4 +65,4 @@ class InferenceManager : public InferenceManagerBuffered
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__INFERENCE_MANAGER_H */
+#endif /* CVC5__THEORY__BAGS__INFERENCE_MANAGER_H */
diff --git a/src/theory/bags/make_bag_op.h b/src/theory/bags/make_bag_op.h
index 44b105225..33de51ed7 100644
--- a/src/theory/bags/make_bag_op.h
+++ b/src/theory/bags/make_bag_op.h
@@ -14,8 +14,8 @@
#include "cvc4_public.h"
-#ifndef CVC4__MAKE_BAG_OP_H
-#define CVC4__MAKE_BAG_OP_H
+#ifndef CVC5__MAKE_BAG_OP_H
+#define CVC5__MAKE_BAG_OP_H
#include <memory>
@@ -59,4 +59,4 @@ struct MakeBagOpHashFunction
} // namespace cvc5
-#endif /* CVC4__MAKE_BAG_OP_H */
+#endif /* CVC5__MAKE_BAG_OP_H */
diff --git a/src/theory/bags/normal_form.h b/src/theory/bags/normal_form.h
index 5b5591133..9eb2d8137 100644
--- a/src/theory/bags/normal_form.h
+++ b/src/theory/bags/normal_form.h
@@ -16,8 +16,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__NORMAL_FORM_H
-#define CVC4__THEORY__BAGS__NORMAL_FORM_H
+#ifndef CVC5__THEORY__BAGS__NORMAL_FORM_H
+#define CVC5__THEORY__BAGS__NORMAL_FORM_H
namespace cvc5 {
namespace theory {
@@ -194,4 +194,4 @@ class NormalForm
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__NORMAL_FORM_H */
+#endif /* CVC5__THEORY__BAGS__NORMAL_FORM_H */
diff --git a/src/theory/bags/rewrites.h b/src/theory/bags/rewrites.h
index aa49c71fb..54bf72c2f 100644
--- a/src/theory/bags/rewrites.h
+++ b/src/theory/bags/rewrites.h
@@ -14,8 +14,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__REWRITES_H
-#define CVC4__THEORY__BAGS__REWRITES_H
+#ifndef CVC5__THEORY__BAGS__REWRITES_H
+#define CVC5__THEORY__BAGS__REWRITES_H
#include <iosfwd>
@@ -94,4 +94,4 @@ std::ostream& operator<<(std::ostream& out, Rewrite r);
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__REWRITES_H */
+#endif /* CVC5__THEORY__BAGS__REWRITES_H */
diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h
index e7c09db8f..9309a704f 100644
--- a/src/theory/bags/solver_state.h
+++ b/src/theory/bags/solver_state.h
@@ -14,8 +14,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H
-#define CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H
+#ifndef CVC5__THEORY__BAGS__THEORY_SOLVER_STATE_H
+#define CVC5__THEORY__BAGS__THEORY_SOLVER_STATE_H
#include <map>
@@ -92,4 +92,4 @@ class SolverState : public TheoryState
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H */
+#endif /* CVC5__THEORY__BAGS__THEORY_SOLVER_STATE_H */
diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h
index ab519b100..a9a03abe6 100644
--- a/src/theory/bags/term_registry.h
+++ b/src/theory/bags/term_registry.h
@@ -14,8 +14,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__TERM_REGISTRY_H
-#define CVC4__THEORY__BAGS__TERM_REGISTRY_H
+#ifndef CVC5__THEORY__BAGS__TERM_REGISTRY_H
+#define CVC5__THEORY__BAGS__TERM_REGISTRY_H
#include <map>
@@ -61,4 +61,4 @@ class TermRegistry
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__TERM_REGISTRY_H */
+#endif /* CVC5__THEORY__BAGS__TERM_REGISTRY_H */
diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h
index 7505f43bf..f1122ed6b 100644
--- a/src/theory/bags/theory_bags.h
+++ b/src/theory/bags/theory_bags.h
@@ -14,8 +14,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_H
-#define CVC4__THEORY__BAGS__THEORY_BAGS_H
+#ifndef CVC5__THEORY__BAGS__THEORY_BAGS_H
+#define CVC5__THEORY__BAGS__THEORY_BAGS_H
#include "theory/bags/bag_solver.h"
#include "theory/bags/bags_rewriter.h"
@@ -118,4 +118,4 @@ class TheoryBags : public Theory
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__THEORY_BAGS_H */
+#endif /* CVC5__THEORY__BAGS__THEORY_BAGS_H */
diff --git a/src/theory/bags/theory_bags_type_enumerator.h b/src/theory/bags/theory_bags_type_enumerator.h
index bdf57213d..74325e2c5 100644
--- a/src/theory/bags/theory_bags_type_enumerator.h
+++ b/src/theory/bags/theory_bags_type_enumerator.h
@@ -14,8 +14,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__TYPE_ENUMERATOR_H
-#define CVC4__THEORY__BAGS__TYPE_ENUMERATOR_H
+#ifndef CVC5__THEORY__BAGS__TYPE_ENUMERATOR_H
+#define CVC5__THEORY__BAGS__TYPE_ENUMERATOR_H
#include "expr/type_node.h"
#include "theory/type_enumerator.h"
@@ -88,4 +88,4 @@ class BagEnumerator : public TypeEnumeratorBase<BagEnumerator>
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__TYPE_ENUMERATOR_H */ \ No newline at end of file
+#endif /* CVC5__THEORY__BAGS__TYPE_ENUMERATOR_H */ \ No newline at end of file
diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h
index 909f607a9..599b3879a 100644
--- a/src/theory/bags/theory_bags_type_rules.h
+++ b/src/theory/bags/theory_bags_type_rules.h
@@ -14,8 +14,8 @@
#include "cvc4_private.h"
-#ifndef CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
-#define CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
+#ifndef CVC5__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
+#define CVC5__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H
#include "expr/node.h"
#include "expr/type_node.h"
@@ -142,4 +142,4 @@ struct BagsProperties
} // namespace theory
} // namespace cvc5
-#endif /* CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H */
+#endif /* CVC5__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback