klee
Public Member Functions | Public Attributes | Private Member Functions | Private Attributes | List of all members
klee::Z3Builder Class Reference

#include <Z3Builder.h>

Collaboration diagram for klee::Z3Builder:
Collaboration graph
[legend]

Public Member Functions

 Z3Builder (bool autoClearConstructCache, const char *z3LogInteractionFile)
 
 ~Z3Builder ()
 
Z3ASTHandle getTrue ()
 
Z3ASTHandle getFalse ()
 
Z3ASTHandle getInitialRead (const Array *os, unsigned index)
 
Z3ASTHandle construct (ref< Expr > e)
 
void clearConstructCache ()
 

Public Attributes

Z3_context ctx
 
std::unordered_map< const Array *, std::vector< Z3ASTHandle > > constant_array_assertions
 

Private Member Functions

Z3ASTHandle bvOne (unsigned width)
 
Z3ASTHandle bvZero (unsigned width)
 
Z3ASTHandle bvMinusOne (unsigned width)
 
Z3ASTHandle bvConst32 (unsigned width, uint32_t value)
 
Z3ASTHandle bvConst64 (unsigned width, uint64_t value)
 
Z3ASTHandle bvZExtConst (unsigned width, uint64_t value)
 
Z3ASTHandle bvSExtConst (unsigned width, uint64_t value)
 
Z3ASTHandle bvBoolExtract (Z3ASTHandle expr, int bit)
 
Z3ASTHandle bvExtract (Z3ASTHandle expr, unsigned top, unsigned bottom)
 
Z3ASTHandle eqExpr (Z3ASTHandle a, Z3ASTHandle b)
 
Z3ASTHandle bvLeftShift (Z3ASTHandle expr, unsigned shift)
 
Z3ASTHandle bvRightShift (Z3ASTHandle expr, unsigned shift)
 
Z3ASTHandle bvVarLeftShift (Z3ASTHandle expr, Z3ASTHandle shift)
 
Z3ASTHandle bvVarRightShift (Z3ASTHandle expr, Z3ASTHandle shift)
 
Z3ASTHandle bvVarArithRightShift (Z3ASTHandle expr, Z3ASTHandle shift)
 
Z3ASTHandle notExpr (Z3ASTHandle expr)
 
Z3ASTHandle bvNotExpr (Z3ASTHandle expr)
 
Z3ASTHandle andExpr (Z3ASTHandle lhs, Z3ASTHandle rhs)
 
Z3ASTHandle bvAndExpr (Z3ASTHandle lhs, Z3ASTHandle rhs)
 
Z3ASTHandle orExpr (Z3ASTHandle lhs, Z3ASTHandle rhs)
 
Z3ASTHandle bvOrExpr (Z3ASTHandle lhs, Z3ASTHandle rhs)
 
Z3ASTHandle iffExpr (Z3ASTHandle lhs, Z3ASTHandle rhs)
 
Z3ASTHandle bvXorExpr (Z3ASTHandle lhs, Z3ASTHandle rhs)
 
Z3ASTHandle bvSignExtend (Z3ASTHandle src, unsigned width)
 
Z3ASTHandle writeExpr (Z3ASTHandle array, Z3ASTHandle index, Z3ASTHandle value)
 
Z3ASTHandle readExpr (Z3ASTHandle array, Z3ASTHandle index)
 
Z3ASTHandle iteExpr (Z3ASTHandle condition, Z3ASTHandle whenTrue, Z3ASTHandle whenFalse)
 
unsigned getBVLength (Z3ASTHandle expr)
 
Z3ASTHandle bvLtExpr (Z3ASTHandle lhs, Z3ASTHandle rhs)
 
Z3ASTHandle bvLeExpr (Z3ASTHandle lhs, Z3ASTHandle rhs)
 
Z3ASTHandle sbvLtExpr (Z3ASTHandle lhs, Z3ASTHandle rhs)
 
Z3ASTHandle sbvLeExpr (Z3ASTHandle lhs, Z3ASTHandle rhs)
 
Z3ASTHandle constructAShrByConstant (Z3ASTHandle expr, unsigned shift, Z3ASTHandle isSigned)
 
Z3ASTHandle getInitialArray (const Array *os)
 
Z3ASTHandle getArrayForUpdate (const Array *root, const UpdateNode *un)
 
Z3ASTHandle constructActual (ref< Expr > e, int *width_out)
 
Z3ASTHandle construct (ref< Expr > e, int *width_out)
 
Z3ASTHandle buildArray (const char *name, unsigned indexWidth, unsigned valueWidth)
 
Z3SortHandle getBvSort (unsigned width)
 
Z3SortHandle getArraySort (Z3SortHandle domainSort, Z3SortHandle rangeSort)
 

Private Attributes

ExprHashMap< std::pair< Z3ASTHandle, unsigned > > constructed
 
Z3ArrayExprHash _arr_hash
 
bool autoClearConstructCache
 
std::string z3LogInteractionFile
 

Detailed Description

Definition at line 104 of file Z3Builder.h.

Constructor & Destructor Documentation

◆ Z3Builder()

klee::Z3Builder::Z3Builder ( bool  autoClearConstructCache,
const char *  z3LogInteractionFile 
)

◆ ~Z3Builder()

klee::Z3Builder::~Z3Builder ( )

Member Function Documentation

◆ andExpr()

Z3ASTHandle klee::Z3Builder::andExpr ( Z3ASTHandle  lhs,
Z3ASTHandle  rhs 
)
private

◆ buildArray()

Z3ASTHandle klee::Z3Builder::buildArray ( const char *  name,
unsigned  indexWidth,
unsigned  valueWidth 
)
private

◆ bvAndExpr()

Z3ASTHandle klee::Z3Builder::bvAndExpr ( Z3ASTHandle  lhs,
Z3ASTHandle  rhs 
)
private

◆ bvBoolExtract()

Z3ASTHandle klee::Z3Builder::bvBoolExtract ( Z3ASTHandle  expr,
int  bit 
)
private

◆ bvConst32()

Z3ASTHandle klee::Z3Builder::bvConst32 ( unsigned  width,
uint32_t  value 
)
private

◆ bvConst64()

Z3ASTHandle klee::Z3Builder::bvConst64 ( unsigned  width,
uint64_t  value 
)
private

◆ bvExtract()

Z3ASTHandle klee::Z3Builder::bvExtract ( Z3ASTHandle  expr,
unsigned  top,
unsigned  bottom 
)
private

◆ bvLeExpr()

Z3ASTHandle klee::Z3Builder::bvLeExpr ( Z3ASTHandle  lhs,
Z3ASTHandle  rhs 
)
private

◆ bvLeftShift()

Z3ASTHandle klee::Z3Builder::bvLeftShift ( Z3ASTHandle  expr,
unsigned  shift 
)
private

◆ bvLtExpr()

Z3ASTHandle klee::Z3Builder::bvLtExpr ( Z3ASTHandle  lhs,
Z3ASTHandle  rhs 
)
private

◆ bvMinusOne()

Z3ASTHandle klee::Z3Builder::bvMinusOne ( unsigned  width)
private

◆ bvNotExpr()

Z3ASTHandle klee::Z3Builder::bvNotExpr ( Z3ASTHandle  expr)
private

◆ bvOne()

Z3ASTHandle klee::Z3Builder::bvOne ( unsigned  width)
private

◆ bvOrExpr()

Z3ASTHandle klee::Z3Builder::bvOrExpr ( Z3ASTHandle  lhs,
Z3ASTHandle  rhs 
)
private

◆ bvRightShift()

Z3ASTHandle klee::Z3Builder::bvRightShift ( Z3ASTHandle  expr,
unsigned  shift 
)
private

◆ bvSExtConst()

Z3ASTHandle klee::Z3Builder::bvSExtConst ( unsigned  width,
uint64_t  value 
)
private

◆ bvSignExtend()

Z3ASTHandle klee::Z3Builder::bvSignExtend ( Z3ASTHandle  src,
unsigned  width 
)
private

◆ bvVarArithRightShift()

Z3ASTHandle klee::Z3Builder::bvVarArithRightShift ( Z3ASTHandle  expr,
Z3ASTHandle  shift 
)
private

◆ bvVarLeftShift()

Z3ASTHandle klee::Z3Builder::bvVarLeftShift ( Z3ASTHandle  expr,
Z3ASTHandle  shift 
)
private

◆ bvVarRightShift()

Z3ASTHandle klee::Z3Builder::bvVarRightShift ( Z3ASTHandle  expr,
Z3ASTHandle  shift 
)
private

◆ bvXorExpr()

Z3ASTHandle klee::Z3Builder::bvXorExpr ( Z3ASTHandle  lhs,
Z3ASTHandle  rhs 
)
private

◆ bvZero()

Z3ASTHandle klee::Z3Builder::bvZero ( unsigned  width)
private

◆ bvZExtConst()

Z3ASTHandle klee::Z3Builder::bvZExtConst ( unsigned  width,
uint64_t  value 
)
private

◆ clearConstructCache()

void klee::Z3Builder::clearConstructCache ( )
inline

Definition at line 190 of file Z3Builder.h.

References constructed.

Referenced by construct().

Here is the caller graph for this function:

◆ construct() [1/2]

Z3ASTHandle klee::Z3Builder::construct ( ref< Expr >  e)
inline

Definition at line 183 of file Z3Builder.h.

References autoClearConstructCache, clearConstructCache(), and construct().

Here is the call graph for this function:

◆ construct() [2/2]

Z3ASTHandle klee::Z3Builder::construct ( ref< Expr >  e,
int *  width_out 
)
private

Referenced by construct().

Here is the caller graph for this function:

◆ constructActual()

Z3ASTHandle klee::Z3Builder::constructActual ( ref< Expr >  e,
int *  width_out 
)
private

◆ constructAShrByConstant()

Z3ASTHandle klee::Z3Builder::constructAShrByConstant ( Z3ASTHandle  expr,
unsigned  shift,
Z3ASTHandle  isSigned 
)
private

◆ eqExpr()

Z3ASTHandle klee::Z3Builder::eqExpr ( Z3ASTHandle  a,
Z3ASTHandle  b 
)
private

◆ getArrayForUpdate()

Z3ASTHandle klee::Z3Builder::getArrayForUpdate ( const Array *  root,
const UpdateNode *  un 
)
private

◆ getArraySort()

Z3SortHandle klee::Z3Builder::getArraySort ( Z3SortHandle  domainSort,
Z3SortHandle  rangeSort 
)
private

◆ getBVLength()

unsigned klee::Z3Builder::getBVLength ( Z3ASTHandle  expr)
private

◆ getBvSort()

Z3SortHandle klee::Z3Builder::getBvSort ( unsigned  width)
private

◆ getFalse()

Z3ASTHandle klee::Z3Builder::getFalse ( )

◆ getInitialArray()

Z3ASTHandle klee::Z3Builder::getInitialArray ( const Array *  os)
private

◆ getInitialRead()

Z3ASTHandle klee::Z3Builder::getInitialRead ( const Array *  os,
unsigned  index 
)

◆ getTrue()

Z3ASTHandle klee::Z3Builder::getTrue ( )

◆ iffExpr()

Z3ASTHandle klee::Z3Builder::iffExpr ( Z3ASTHandle  lhs,
Z3ASTHandle  rhs 
)
private

◆ iteExpr()

Z3ASTHandle klee::Z3Builder::iteExpr ( Z3ASTHandle  condition,
Z3ASTHandle  whenTrue,
Z3ASTHandle  whenFalse 
)
private

◆ notExpr()

Z3ASTHandle klee::Z3Builder::notExpr ( Z3ASTHandle  expr)
private

◆ orExpr()

Z3ASTHandle klee::Z3Builder::orExpr ( Z3ASTHandle  lhs,
Z3ASTHandle  rhs 
)
private

◆ readExpr()

Z3ASTHandle klee::Z3Builder::readExpr ( Z3ASTHandle  array,
Z3ASTHandle  index 
)
private

◆ sbvLeExpr()

Z3ASTHandle klee::Z3Builder::sbvLeExpr ( Z3ASTHandle  lhs,
Z3ASTHandle  rhs 
)
private

◆ sbvLtExpr()

Z3ASTHandle klee::Z3Builder::sbvLtExpr ( Z3ASTHandle  lhs,
Z3ASTHandle  rhs 
)
private

◆ writeExpr()

Z3ASTHandle klee::Z3Builder::writeExpr ( Z3ASTHandle  array,
Z3ASTHandle  index,
Z3ASTHandle  value 
)
private

Member Data Documentation

◆ _arr_hash

Z3ArrayExprHash klee::Z3Builder::_arr_hash
private

Definition at line 106 of file Z3Builder.h.

◆ autoClearConstructCache

bool klee::Z3Builder::autoClearConstructCache
private

Definition at line 169 of file Z3Builder.h.

Referenced by construct().

◆ constant_array_assertions

std::unordered_map<const Array *, std::vector<Z3ASTHandle> > klee::Z3Builder::constant_array_assertions

Definition at line 175 of file Z3Builder.h.

◆ constructed

ExprHashMap<std::pair<Z3ASTHandle, unsigned> > klee::Z3Builder::constructed
private

Definition at line 105 of file Z3Builder.h.

Referenced by clearConstructCache().

◆ ctx

Z3_context klee::Z3Builder::ctx

Definition at line 173 of file Z3Builder.h.

◆ z3LogInteractionFile

std::string klee::Z3Builder::z3LogInteractionFile
private

Definition at line 170 of file Z3Builder.h.

The documentation for this class was generated from the following file: