7 files changed, 24 insertions, 54 deletions
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index f3c6385e5..d9f77d50f 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -18,17 +18,18 @@
 #ifndef __CVC4__THEORY__ARRAYS__ARRAY_INFO_H
 #define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H
 
-#include "util/backtrackable.h"
-#include "context/cdlist.h"
-#include "context/cdhashmap.h"
-#include "expr/node.h"
-#include "util/statistics_registry.h"
-#include "util/ntuple.h"
 #include <ext/hash_set>
 #include <ext/hash_map>
 #include <iostream>
 #include <map>
 
+#include "context/backtrackable.h"
+#include "context/cdlist.h"
+#include "context/cdhashmap.h"
+#include "expr/node.h"
+#include "expr/statistics_registry.h"
+#include "util/ntuple.h"
+
 namespace CVC4 {
 namespace theory {
 namespace arrays {
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index c18492a58..d5f313ca1 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -35,7 +35,7 @@ operator STORE 3 "array store; first parameter is an array term, second is the s
 constant STORE_ALL \
     ::CVC4::ArrayStoreAll \
     ::CVC4::ArrayStoreAllHashFunction \
-    "util/array_store_all.h" \
+    "expr/array_store_all.h" \
     "array store-all; payload is an instance of the CVC4::ArrayStoreAll class (this is not supported by arrays decision procedure yet, but it is used for returned array models)"
 
 # used internally by array theory
diff --git a/src/theory/arrays/options b/src/theory/arrays/options
deleted file mode 100644
index 8ed80c1f1..000000000
--- a/src/theory/arrays/options
+++ /dev/null
@@ -1,32 +0,0 @@
-#
-# Option specification file for CVC4
-# See src/options/base_options for a description of this file format
-#
-
-module ARRAYS "theory/arrays/options.h" Arrays theory
-
-option arraysOptimizeLinear --arrays-optimize-linear bool :default true :read-write
- turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper)
-
-option arraysLazyRIntro1 --arrays-lazy-rintro1 bool :default true :read-write
- turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination)
-
-option arraysModelBased --arrays-model-based bool :default false :read-write
- turn on model-based array solver
-
-option arraysEagerIndexSplitting --arrays-eager-index bool :default true :read-write
- turn on eager index splitting for generated array lemmas
-
-option arraysEagerLemmas --arrays-eager-lemmas bool :default false :read-write
- turn on eager lemma generation for arrays
-
-option arraysConfig --arrays-config int :default 0 :read-write
- set different array option configurations - for developers only
-
-option arraysReduceSharing --arrays-reduce-sharing bool :default false :read-write
- use model information to reduce size of care graph for arrays
-
-option arraysPropagate --arrays-prop int :default 2 :read-write
- propagation effort for arrays: 0 is none, 1 is some, 2 is full
-
-endmodule
diff --git a/src/theory/arrays/static_fact_manager.cpp b/src/theory/arrays/static_fact_manager.cpp
index 1743e3b30..0d04ce097 100644
--- a/src/theory/arrays/static_fact_manager.cpp
+++ b/src/theory/arrays/static_fact_manager.cpp
@@ -18,9 +18,9 @@
 
 #include <iostream>
 
-#include "theory/arrays/static_fact_manager.h"
-#include "util/cvc4_assert.h"
+#include "base/cvc4_assert.h"
 #include "expr/node.h"
+#include "theory/arrays/static_fact_manager.h"
 
 using namespace std;
 
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index d872ab42c..5af7f02db 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -14,17 +14,18 @@
  ** Implementation of the theory of arrays.
  **/
 
-
 #include "theory/arrays/theory_arrays.h"
-#include "theory/valuation.h"
-#include "expr/kind.h"
+
 #include <map>
+
+#include "expr/kind.h"
+#include "options/arrays_options.h"
+#include "options/smt_options.h"
+#include "smt/logic_exception.h"
+#include "smt_util/command.h"
 #include "theory/rewriter.h"
-#include "expr/command.h"
 #include "theory/theory_model.h"
-#include "theory/arrays/options.h"
-#include "smt/options.h"
-#include "smt/logic_exception.h"
+#include "theory/valuation.h"
 
 
 using namespace std;
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index b2e039912..717c654d2 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -19,13 +19,13 @@
 #ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
 #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H
 
-#include "theory/theory.h"
-#include "theory/arrays/array_info.h"
-#include "util/statistics_registry.h"
-#include "theory/uf/equality_engine.h"
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/cdqueue.h"
+#include "expr/statistics_registry.h"
+#include "theory/arrays/array_info.h"
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arrays/union_find.cpp b/src/theory/arrays/union_find.cpp
index 9e6978c92..3f71b350e 100644
--- a/src/theory/arrays/union_find.cpp
+++ b/src/theory/arrays/union_find.cpp
@@ -18,9 +18,9 @@
 
 #include <iostream>
 
-#include "theory/arrays/union_find.h"
-#include "util/cvc4_assert.h"
+#include "base/cvc4_assert.h"
 #include "expr/node.h"
+#include "theory/arrays/union_find.h"
 
 using namespace std;