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/array_proof_reconstruction.h6
-rw-r--r--src/theory/arrays/static_fact_manager.h6
-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
8 files changed, 24 insertions, 24 deletions
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index c221569bb..7e18f9ed2 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 CVC4__THEORY__ARRAYS__ARRAY_INFO_H
+#define CVC4__THEORY__ARRAYS__ARRAY_INFO_H
#include <iostream>
#include <map>
@@ -211,4 +211,4 @@ public:
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARRAYS__ARRAY_INFO_H */
+#endif /* CVC4__THEORY__ARRAYS__ARRAY_INFO_H */
diff --git a/src/theory/arrays/array_proof_reconstruction.h b/src/theory/arrays/array_proof_reconstruction.h
index 3c656de1a..37b014d35 100644
--- a/src/theory/arrays/array_proof_reconstruction.h
+++ b/src/theory/arrays/array_proof_reconstruction.h
@@ -15,8 +15,8 @@
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H
-#define __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H
+#ifndef CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H
+#define CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H
#include "theory/uf/equality_engine.h"
@@ -56,4 +56,4 @@ private:
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H */
+#endif /* CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H */
diff --git a/src/theory/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h
index 135e46790..6b68edf26 100644
--- a/src/theory/arrays/static_fact_manager.h
+++ b/src/theory/arrays/static_fact_manager.h
@@ -18,8 +18,8 @@
#include "cvc4_private.h"
-#ifndef __CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H
-#define __CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H
+#ifndef CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H
+#define CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H
#include <utility>
#include <vector>
@@ -113,4 +113,4 @@ inline void StaticFactManager::setCanon(TNode n, TNode newParent) {
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /*__CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H */
+#endif /*CVC4__THEORY__ARRAYS__STATIC_FACT_MANAGER_H */
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 51e95844f..be80a081d 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 CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
+#define CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
#include <tuple>
#include <unordered_map>
@@ -491,4 +491,4 @@ class TheoryArrays : public Theory {
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H */
+#endif /* CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H */
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 21cc56dbc..5f3fcf48d 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 CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
+#define CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
#include <unordered_map>
#include <unordered_set>
@@ -509,4 +509,4 @@ public:
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H */
+#endif /* CVC4__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 e789b8445..78756176d 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 CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
+#define CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
#include "theory/arrays/theory_arrays_rewriter.h" // for array-constant attributes
#include "theory/type_enumerator.h"
@@ -227,4 +227,4 @@ struct ArrayPartialSelectTypeRule {
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H */
+#endif /* CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H */
diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
index 2e09763e4..5ca156b2e 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 CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H
+#define CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H
#include "theory/type_enumerator.h"
#include "expr/type_node.h"
@@ -158,4 +158,4 @@ class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H */
+#endif /* CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H */
diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h
index 5b552c7f8..1f38f1280 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 CVC4__THEORY__ARRAYS__UNION_FIND_H
+#define CVC4__THEORY__ARRAYS__UNION_FIND_H
#include <utility>
#include <vector>
@@ -139,4 +139,4 @@ inline void UnionFind<NodeType, NodeHash>::setCanon(TNode n, TNode newParent) {
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /*__CVC4__THEORY__ARRAYS__UNION_FIND_H */
+#endif /*CVC4__THEORY__ARRAYS__UNION_FIND_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback