diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2018-10-18 12:41:07 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-10-23 18:53:46 +0300 |
commit | 6bd5d045f2cb19331feb34d7ea74f748c5568a91 (patch) | |
tree | eb1147b7b7e5dc02d36011992f7311840fef95f6 /include | |
parent | a72a2a9622aa05bd6eb1ffeb66e0db47b8cc4745 (diff) | |
download | klee-6bd5d045f2cb19331feb34d7ea74f748c5568a91.tar.gz |
Clean-up headers
Remove unneeded headers from include files
Diffstat (limited to 'include')
-rw-r--r-- | include/klee/ArrayExprOptimizer.h | 27 | ||||
-rw-r--r-- | include/klee/ArrayExprRewriter.h | 25 | ||||
-rw-r--r-- | include/klee/AssignmentGenerator.h | 12 |
3 files changed, 18 insertions, 46 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 { |