ArrayExprRewriter.h

Go to the documentation of this file.

//===-- 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/ADT/Ref.h"
#include "klee/Expr/Expr.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 */