diff options
Diffstat (limited to 'lib/Expr/ArrayExprRewriter.h')
-rw-r--r-- | lib/Expr/ArrayExprRewriter.h | 47 |
1 files changed, 0 insertions, 47 deletions
diff --git a/lib/Expr/ArrayExprRewriter.h b/lib/Expr/ArrayExprRewriter.h deleted file mode 100644 index 098cb0a6..00000000 --- a/lib/Expr/ArrayExprRewriter.h +++ /dev/null @@ -1,47 +0,0 @@ -//===-- ArrayExprRewriter.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_ARRAYEXPRREWRITER_H -#define KLEE_ARRAYEXPRREWRITER_H - -#include <iterator> -#include <map> -#include <vector> - -#include "klee/Expr/Expr.h" -#include "klee/util/Ref.h" - -namespace klee { - -using array2idx_ty = std::map<const Array *, std::vector<ref<Expr>>>; -using mapIndexOptimizedExpr_ty = std::map<ref<Expr>, std::vector<ref<Expr>>>; - -class ExprRewriter { -public: - 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 mapIndexOptimizedExpr_ty &idx_valIdx); - - static ref<Expr> - concatenateOrExpr(const std::vector<ref<Expr>>::const_iterator begin, - const std::vector<ref<Expr>>::const_iterator end); - - static ref<Expr> createEqExpr(const ref<Expr> &index, - const ref<Expr> &valIndex); - - static ref<Expr> createRangeExpr(const ref<Expr> &index, - const ref<Expr> &valStart, - const ref<Expr> &valEnd); -}; -} // namespace klee - -#endif /* KLEE_ARRAYEXPRREWRITER_H */ |