about summary refs log tree commit diff homepage
path: root/lib/Expr/ArrayExprOptimizer.h
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Expr/ArrayExprOptimizer.h')
-rw-r--r--lib/Expr/ArrayExprOptimizer.h65
1 files changed, 0 insertions, 65 deletions
diff --git a/lib/Expr/ArrayExprOptimizer.h b/lib/Expr/ArrayExprOptimizer.h
deleted file mode 100644
index 8fc040e5..00000000
--- a/lib/Expr/ArrayExprOptimizer.h
+++ /dev/null
@@ -1,65 +0,0 @@
-//===-- ArrayExprOptimizer.h ----------------------------------------------===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef KLEE_ARRAYEXPROPTIMIZER_H
-#define KLEE_ARRAYEXPROPTIMIZER_H
-
-#include <cstdint>
-#include <map>
-#include <unordered_map>
-#include <unordered_set>
-#include <utility>
-#include <vector>
-
-#include "klee/Expr/Expr.h"
-#include "klee/Expr/ExprHashMap.h"
-#include "klee/util/Ref.h"
-
-namespace klee {
-
-enum ArrayOptimizationType { NONE, ALL, INDEX, VALUE };
-
-using array2idx_ty = std::map<const Array *, std::vector<ref<Expr>>>;
-using mapIndexOptimizedExpr_ty = std::map<ref<Expr>, std::vector<ref<Expr>>>;
-
-class ExprOptimizer {
-private:
-  ExprHashMap<ref<Expr>> cacheExprOptimized;
-  ExprHashSet cacheExprUnapplicable;
-  ExprHashMap<ref<Expr>> cacheReadExprOptimized;
-
-public:
-  /// Returns the optimised version of e.
-  /// @param e expression to optimise
-  /// @param valueOnly XXX document
-  /// @return optimised expression
-  ref<Expr> optimizeExpr(const ref<Expr> &e, bool valueOnly);
-
-private:
-  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,
-      std::map<const ReadExpr *, std::pair<ref<Expr>, Expr::Width>> &readInfo,
-      bool isSymbolic);
-
-  ref<Expr> buildConstantSelectExpr(const ref<Expr> &index,
-                                    std::vector<uint64_t> &arrayValues,
-                                    Expr::Width width,
-                                    unsigned elementsInArray) const;
-
-  ref<Expr>
-  buildMixedSelectExpr(const ReadExpr *re,
-                       std::vector<std::pair<uint64_t, bool>> &arrayValues,
-                       Expr::Width width, unsigned elementsInArray) const;
-};
-} // namespace klee
-
-#endif /* KLEE_ARRAYEXPROPTIMIZER_H */