6 files changed, 57 insertions, 54 deletions
diff --git a/include/klee/ArrayExprOptimizer.h b/include/klee/ArrayExprOptimizer.h
index 4836241d..aafe1d27 100644
--- a/include/klee/ArrayExprOptimizer.h
+++ b/include/klee/ArrayExprOptimizer.h
@@ -10,28 +10,15 @@
 #ifndef KLEE_EXPROPTIMIZER_H
 #define KLEE_EXPROPTIMIZER_H
 
-#include <cassert>
-#include <iterator>
+#include <cstdint>
 #include <map>
-#include <string>
+#include <unordered_map>
+#include <unordered_set>
 #include <utility>
 #include <vector>
 
 #include "Expr.h"
-#include "ExprBuilder.h"
-#include "Constraints.h"
-#include "Internal/Support/ErrorHandling.h"
-#include "util/ArrayExprVisitor.h"
-#include "util/Assignment.h"
 #include "util/Ref.h"
-#include "klee/AssignmentGenerator.h"
-#include "klee/ExecutionState.h"
-#include "klee/Config/Version.h"
-
-#include "llvm/Support/CommandLine.h"
-
-#include <unordered_map>
-#include <unordered_set>
 
 namespace klee {
 
@@ -42,10 +29,7 @@ enum ArrayOptimizationType {
   VALUE
 };
 
-class Expr;
-template <class T> class ref;
 typedef std::map<const Array *, std::vector<ref<Expr>>> array2idx_ty;
-typedef std::vector<const Array *> v_arr_ty;
 typedef std::map<ref<Expr>, std::vector<ref<Expr>>> mapIndexOptimizedExpr_ty;
 
 class ExprOptimizer {
@@ -62,9 +46,8 @@ public:
   ref<Expr> optimizeExpr(const ref<Expr> &e, bool valueOnly);
 
 private:
-  bool
-  computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
-                 std::map<ref<Expr>, std::vector<ref<Expr>>> &idx_valIdx) const;
+  bool computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
+                      mapIndexOptimizedExpr_ty &idx_valIdx) const;
 
   ref<Expr> getSelectOptExpr(
       const ref<Expr> &e, std::vector<const ReadExpr *> &reads,
diff --git a/include/klee/ArrayExprRewriter.h b/include/klee/ArrayExprRewriter.h
index 3828262a..2b6c78b4 100644
--- a/include/klee/ArrayExprRewriter.h
+++ b/include/klee/ArrayExprRewriter.h
@@ -10,31 +10,26 @@
 #ifndef LIB_EXPRREWRITER_H_
 #define LIB_EXPRREWRITER_H_
 
-#include "klee/Expr.h"
-#include "klee/CommandLine.h"
-#include "klee/Constraints.h"
-#include "klee/Internal/Support/ErrorHandling.h"
-#include "klee/util/ArrayExprVisitor.h"
-#include "klee/util/Assignment.h"
-#include "klee/util/Ref.h"
-#include "klee/AssignmentGenerator.h"
+#include <iterator>
+#include <map>
+#include <vector>
+
+#include "Expr.h"
+#include "util/Ref.h"
 
 namespace klee {
 
-typedef std::vector<const Array *> v_arr_ty;
 typedef std::map<const Array *, std::vector<ref<Expr>>> array2idx_ty;
 typedef std::map<ref<Expr>, std::vector<ref<Expr>>> mapIndexOptimizedExpr_ty;
 
 class ExprRewriter {
 public:
-  static ref<Expr>
-  createOptExpr(const ref<Expr> &e, const array2idx_ty &arrays,
-                const std::map<ref<Expr>, std::vector<ref<Expr>>> &idx_valIdx);
+  static ref<Expr> createOptExpr(const ref<Expr> &e, const array2idx_ty &arrays,
+                                 const mapIndexOptimizedExpr_ty &idx_valIdx);
 
 private:
-  static ref<Expr>
-  rewrite(const ref<Expr> &e, const array2idx_ty &arrays,
-          const std::map<ref<Expr>, std::vector<ref<Expr>>> &idx_valIdx);
+  static ref<Expr> rewrite(const ref<Expr> &e, const array2idx_ty &arrays,
+                           const mapIndexOptimizedExpr_ty &idx_valIdx);
 
   static ref<Expr>
   concatenateOrExpr(const std::vector<ref<Expr>>::const_iterator begin,
diff --git a/include/klee/AssignmentGenerator.h b/include/klee/AssignmentGenerator.h
index 96209498..404c8632 100644
--- a/include/klee/AssignmentGenerator.h
+++ b/include/klee/AssignmentGenerator.h
@@ -10,20 +10,14 @@
 #ifndef KLEE_ASSIGNMENTGENERATOR_H
 #define KLEE_ASSIGNMENTGENERATOR_H
 
-#include <cassert>
-#include <iterator>
-#include <map>
-#include <string>
-#include <utility>
 #include <vector>
 
 #include "Expr.h"
-#include "Constraints.h"
-#include "Internal/Support/ErrorHandling.h"
-#include "util/ArrayExprVisitor.h"
-#include "util/Assignment.h"
 #include "util/Ref.h"
 
+namespace klee {
+class Assignment;
+} /* namespace klee */
 
 namespace klee {
 
diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp
index 0929efb5..dc0b2002 100644
--- a/lib/Expr/ArrayExprOptimizer.cpp
+++ b/lib/Expr/ArrayExprOptimizer.cpp
@@ -9,11 +9,23 @@
 
 #include "klee/ArrayExprOptimizer.h"
 
+#include <algorithm>
+#include <cassert>
+#include <llvm/ADT/APInt.h>
+#include <llvm/Support/Casting.h>
+#include <llvm/Support/CommandLine.h>
+#include <set>
+#include <stddef.h>
+
 #include "klee/ArrayExprRewriter.h"
+#include "klee/AssignmentGenerator.h"
+#include "klee/Config/Version.h"
+#include "klee/ExprBuilder.h"
+#include "klee/Internal/Support/ErrorHandling.h"
+#include "klee/util/ArrayExprVisitor.h"
+#include "klee/util/Assignment.h"
 #include "klee/util/BitArray.h"
 
-#include <iostream>
-
 using namespace klee;
 
 namespace klee {
@@ -163,7 +175,7 @@ bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e,
     // For each concrete value 'i' stored in the array
     for (size_t aIdx = 0; aIdx < arr->constantValues.size(); aIdx += width) {
       Assignment *a = new Assignment();
-      v_arr_ty objects;
+      std::vector<const Array *> objects;
       std::vector<std::vector<unsigned char>> values;
 
       // For each symbolic index Expr(k) found
diff --git a/lib/Expr/ArrayExprRewriter.cpp b/lib/Expr/ArrayExprRewriter.cpp
index 5e5dac0d..26aef1ff 100644
--- a/lib/Expr/ArrayExprRewriter.cpp
+++ b/lib/Expr/ArrayExprRewriter.cpp
@@ -9,9 +9,15 @@
 
 #include "klee/ArrayExprRewriter.h"
 
-#include "klee/util/BitArray.h"
+#include <cassert>
+#include <cstdint>
+#include <llvm/ADT/APInt.h>
+#include <llvm/Support/Casting.h>
+#include <set>
+#include <utility>
 
-#include "llvm/Support/CommandLine.h"
+#include "klee/util/ArrayExprVisitor.h"
+#include "klee/util/BitArray.h"
 
 using namespace klee;
 
diff --git a/lib/Expr/AssignmentGenerator.cpp b/lib/Expr/AssignmentGenerator.cpp
index 4a1d68d8..a906f796 100644
--- a/lib/Expr/AssignmentGenerator.cpp
+++ b/lib/Expr/AssignmentGenerator.cpp
@@ -7,9 +7,22 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/AssignmentGenerator.h"
-
-#include "llvm/Support/raw_ostream.h"
+#include "../../include/klee/AssignmentGenerator.h"
+
+#include <cassert>
+#include <cstdint>
+#include <llvm/ADT/APInt.h>
+#include <llvm/Support/Casting.h>
+#include <llvm/Support/raw_ostream.h>
+#include <map>
+#include <set>
+#include <stddef.h>
+#include <string>
+#include <utility>
+
+#include "klee/Internal/Support/ErrorHandling.h"
+#include "klee/klee.h"
+#include "klee/util/Assignment.h"
 
 using namespace klee;