From 6bd5d045f2cb19331feb34d7ea74f748c5568a91 Mon Sep 17 00:00:00 2001
From: Martin Nowack <m.nowack@imperial.ac.uk>
Date: Thu, 18 Oct 2018 12:41:07 +0100
Subject: Clean-up headers

Remove unneeded headers from include files
---
 include/klee/ArrayExprOptimizer.h  | 27 +++++----------------------
 include/klee/ArrayExprRewriter.h   | 25 ++++++++++---------------
 include/klee/AssignmentGenerator.h | 12 +++---------
 3 files changed, 18 insertions(+), 46 deletions(-)

(limited to 'include')

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 {
 
-- 
cgit 1.4.1