klee
Static Public Member Functions | Static Private Member Functions | List of all members
klee::ExprRewriter Class Reference

#include <ArrayExprRewriter.h>

Static Public Member Functions

static ref< Expr > createOptExpr (const ref< Expr > &e, const array2idx_ty &arrays, const mapIndexOptimizedExpr_ty &idx_valIdx)
 

Static Private Member Functions

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)
 

Detailed Description

Definition at line 25 of file ArrayExprRewriter.h.

Member Function Documentation

◆ concatenateOrExpr()

ref< Expr > ExprRewriter::concatenateOrExpr ( const std::vector< ref< Expr > >::const_iterator  begin,
const std::vector< ref< Expr > >::const_iterator  end 
)
staticprivate

Definition at line 144 of file ArrayExprRewriter.cpp.

References concatenateOrExpr(), and klee::Expr::Int32.

Referenced by concatenateOrExpr(), and rewrite().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createEqExpr()

ref< Expr > ExprRewriter::createEqExpr ( const ref< Expr > &  index,
const ref< Expr > &  valIndex 
)
staticprivate

Definition at line 156 of file ArrayExprRewriter.cpp.

Referenced by rewrite().

Here is the caller graph for this function:

◆ createOptExpr()

ref< Expr > ExprRewriter::createOptExpr ( const ref< Expr > &  e,
const array2idx_ty &  arrays,
const mapIndexOptimizedExpr_ty &  idx_valIdx 
)
static

Definition at line 26 of file ArrayExprRewriter.cpp.

References rewrite().

Referenced by klee::ExprOptimizer::optimizeExpr().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ createRangeExpr()

ref< Expr > ExprRewriter::createRangeExpr ( const ref< Expr > &  index,
const ref< Expr > &  valStart,
const ref< Expr > &  valEnd 
)
staticprivate

Definition at line 161 of file ArrayExprRewriter.cpp.

Referenced by rewrite().

Here is the caller graph for this function:

◆ rewrite()

ref< Expr > ExprRewriter::rewrite ( const ref< Expr > &  e,
const array2idx_ty &  arrays,
const mapIndexOptimizedExpr_ty &  idx_valIdx 
)
staticprivate

Definition at line 31 of file ArrayExprRewriter.cpp.

References klee::ConstantExpr::alloc(), klee::NotExpr::alloc(), concatenateOrExpr(), klee::ConstantExpr::create(), createEqExpr(), createRangeExpr(), klee::BitArray::get(), klee::IndexTransformationExprVisitor::getMul(), klee::IndexTransformationExprVisitor::getWidth(), klee::BitArray::set(), klee::Array::size, and klee::ExprVisitor::visit().

Referenced by createOptExpr().

Here is the call graph for this function:
Here is the caller graph for this function:
The documentation for this class was generated from the following files: