Merge branch 'master' into indexof_reindexof_re

5 files changed, 12 insertions, 4 deletions

diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index e39f30c6e..67abc149d 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -36,7 +36,8 @@ operator EQ_RANGE 4 "equality of two arrays over an index range lower/upper"
 
 # storeall t e  is  \all i in indexType(t) <= e
 constant STORE_ALL \
-    ::cvc5::ArrayStoreAll \
+    class \
+    ArrayStoreAll \
     ::cvc5::ArrayStoreAllHashFunction \
     "expr/array_store_all.h" \
     "array store-all; payload is an instance of the cvc5::ArrayStoreAll class (this is not supported by arrays decision procedure yet, but it is used for returned array models)"
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 0bdccfd17..ea18b3180 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -18,6 +18,7 @@
 #include <map>
 #include <memory>
 
+#include "expr/array_store_all.h"
 #include "expr/kind.h"
 #include "expr/node_algorithm.h"
 #include "options/arrays_options.h"
diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp
index 8ad7a5f95..1072ffaf4 100644
--- a/src/theory/arrays/theory_arrays_rewriter.cpp
+++ b/src/theory/arrays/theory_arrays_rewriter.cpp
@@ -16,9 +16,12 @@
  * \todo document this file
  */
 
-#include "expr/attribute.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
 
+#include "expr/array_store_all.h"
+#include "expr/attribute.h"
+#include "util/cardinality.h"
+
 namespace cvc5 {
 namespace theory {
 namespace arrays {
diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp
index 04a2f1a74..6d16e4020 100644
--- a/src/theory/arrays/theory_arrays_type_rules.cpp
+++ b/src/theory/arrays/theory_arrays_type_rules.cpp
@@ -16,8 +16,10 @@
 #include "theory/arrays/theory_arrays_type_rules.h"
 
 // for array-constant attributes
+#include "expr/array_store_all.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/type_enumerator.h"
+#include "util/cardinality.h"
 
 namespace cvc5 {
 namespace theory {
diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
index 181a42da4..6fc026b19 100644
--- a/src/theory/arrays/type_enumerator.h
+++ b/src/theory/arrays/type_enumerator.h
@@ -18,10 +18,11 @@
 #ifndef CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H
 #define CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H
 
-#include "theory/type_enumerator.h"
-#include "expr/type_node.h"
+#include "expr/array_store_all.h"
 #include "expr/kind.h"
+#include "expr/type_node.h"
 #include "theory/rewriter.h"
+#include "theory/type_enumerator.h"
 
 namespace cvc5 {
 namespace theory {