ilasynth::Z3ExprAdapter Class Reference

#include <smt.hpp>

Inheritance diagram for ilasynth::Z3ExprAdapter:

Public Types
typedef std::unordered_map< const Node *, z3::expr, decltype(&nodeHash), decltype(&nodeEqual)>	expr_map_t

Public Member Functions
	Z3ExprAdapter (z3::context &c, const std::string &suffix)
	Z3ExprAdapter (z3::context &c, const char *suffix)
virtual	~Z3ExprAdapter ()
virtual void	operator() (const Node *n)
z3::expr	getExpr (const Node *n)
z3::expr	getCnst (const Node *n)
z3::context &	ctx () const
void	clear ()
std::string	extractNumeralString (z3::model &m, const Node *r)
int	getNumeralInt (z3::model &m, const Node *r)
mp_int_t	getNumeralCppInt (z3::model &m, const Node *r)
bool	getBoolValue (z3::model &m, const Node *r)
template<typename T >
bool	getChoiceBool (z3::model &m, const ChoiceExpr< T > *op, int i)
void	setNameSuffix (const std::string &ns)
const std::string &	getNameSuffix () const

Public Attributes
bool	simplify

Protected Member Functions
z3::expr	_getArg (const expr_map_t &m, const Node *n, int i)
z3::expr	getArgExpr (const Node *n, int i)
z3::expr	getArgCnst (const Node *n, int i)
void	_populateExprMap (const Node *n)
void	_populateCnstMap (const Node *n)
virtual z3::expr	getBoolVarExpr (const BoolVar *bv)
virtual z3::expr	getBoolOpExpr (const BoolOp *op)
virtual z3::expr	getChoiceExpr (const BoolChoice *op)
virtual z3::expr	getBitvectorVarExpr (const BitvectorVar *bvv)
virtual z3::expr	getBvOpExpr (const BitvectorOp *op)
virtual z3::expr	getChoiceExpr (const BitvectorChoice *op)
virtual z3::expr	getBVInRangeExpr (const BVInRange *op)
virtual z3::expr	getBVInRangeCnst (const BVInRange *op)
virtual z3::expr	getMemVarExpr (const MemVar *mv)
virtual z3::expr	getMemOpExpr (const MemOp *mw)
virtual z3::expr	getChoiceExpr (const MemChoice *op)
virtual z3::expr	getFuncVarExpr (const FuncVar *fv)

Protected Attributes
expr_map_t	exprmap
expr_map_t	cnstmap
z3::context &	c
std::string	suffix
std::string	name_suffix
	Added to every name. More...

Private Member Functions
template<typename T >
z3::expr	_getChoiceExpr (const ChoiceExpr< T > *op)

Member Typedef Documentation

expr_map_t

typedef std::unordered_map<const Node*, z3::expr, decltype(&nodeHash), decltype(&nodeEqual)> ilasynth::Z3ExprAdapter::expr_map_t

Constructor & Destructor Documentation

Z3ExprAdapter() [1/2]

ilasynth::Z3ExprAdapter::Z3ExprAdapter	(	z3::context &	c,
		const std::string &	suffix
	)

Z3ExprAdapter() [2/2]

ilasynth::Z3ExprAdapter::Z3ExprAdapter	(	z3::context &	c,
		const char *	suffix
	)

~Z3ExprAdapter()

virtual ilasynth::Z3ExprAdapter::~Z3ExprAdapter ( )

virtual

Member Function Documentation

_getArg()

z3::expr ilasynth::Z3ExprAdapter::_getArg ( const expr_map_t &  m, const Node *  n, int  i  )

protected

_getChoiceExpr()

template<typename T >

z3::expr ilasynth::Z3ExprAdapter::_getChoiceExpr ( const ChoiceExpr< T > *  op )

inlineprivate

_populateCnstMap()

void ilasynth::Z3ExprAdapter::_populateCnstMap ( const Node *  n )

protected

_populateExprMap()

void ilasynth::Z3ExprAdapter::_populateExprMap ( const Node *  n )

protected

clear()

void ilasynth::Z3ExprAdapter::clear ( )

inline

ctx()

z3::context& ilasynth::Z3ExprAdapter::ctx ( ) const

inline

extractNumeralString()

std::string ilasynth::Z3ExprAdapter::extractNumeralString	(	z3::model &	m,
		const Node *	r
	)

getArgCnst()

z3::expr ilasynth::Z3ExprAdapter::getArgCnst ( const Node *  n, int  i  )

inlineprotected

getArgExpr()

z3::expr ilasynth::Z3ExprAdapter::getArgExpr ( const Node *  n, int  i  )

inlineprotected

getBitvectorVarExpr()

virtual z3::expr ilasynth::Z3ExprAdapter::getBitvectorVarExpr ( const BitvectorVar *  bvv )

protectedvirtual

Reimplemented in ilasynth::Z3ExprRewritingAdapter.

getBoolOpExpr()

virtual z3::expr ilasynth::Z3ExprAdapter::getBoolOpExpr ( const BoolOp *  op )

protectedvirtual

getBoolValue()

bool ilasynth::Z3ExprAdapter::getBoolValue	(	z3::model &	m,
		const Node *	r
	)

getBoolVarExpr()

virtual z3::expr ilasynth::Z3ExprAdapter::getBoolVarExpr ( const BoolVar *  bv )

protectedvirtual

Reimplemented in ilasynth::Z3ExprRewritingAdapter.

getBVInRangeCnst()

virtual z3::expr ilasynth::Z3ExprAdapter::getBVInRangeCnst ( const BVInRange *  op )

protectedvirtual

getBVInRangeExpr()

virtual z3::expr ilasynth::Z3ExprAdapter::getBVInRangeExpr ( const BVInRange *  op )

protectedvirtual

getBvOpExpr()

virtual z3::expr ilasynth::Z3ExprAdapter::getBvOpExpr ( const BitvectorOp *  op )

protectedvirtual

getChoiceBool()

template<typename T >

bool ilasynth::Z3ExprAdapter::getChoiceBool ( z3::model &  m, const ChoiceExpr< T > *  op, int  i  )

inline

getChoiceExpr() [1/3]

virtual z3::expr ilasynth::Z3ExprAdapter::getChoiceExpr ( const BoolChoice *  op )

protectedvirtual

getChoiceExpr() [2/3]

virtual z3::expr ilasynth::Z3ExprAdapter::getChoiceExpr ( const BitvectorChoice *  op )

protectedvirtual

getChoiceExpr() [3/3]

virtual z3::expr ilasynth::Z3ExprAdapter::getChoiceExpr ( const MemChoice *  op )

protectedvirtual

getCnst()

z3::expr ilasynth::Z3ExprAdapter::getCnst

(

const Node *

n

)

getExpr()

z3::expr ilasynth::Z3ExprAdapter::getExpr

(

const Node *

n

)

getFuncVarExpr()

virtual z3::expr ilasynth::Z3ExprAdapter::getFuncVarExpr ( const FuncVar *  fv )

protectedvirtual

getMemOpExpr()

virtual z3::expr ilasynth::Z3ExprAdapter::getMemOpExpr ( const MemOp *  mw )

protectedvirtual

getMemVarExpr()

virtual z3::expr ilasynth::Z3ExprAdapter::getMemVarExpr ( const MemVar *  mv )

protectedvirtual

Reimplemented in ilasynth::Z3ExprRewritingAdapter.

getNameSuffix()

const std::string& ilasynth::Z3ExprAdapter::getNameSuffix ( ) const

inline

getNumeralCppInt()

mp_int_t ilasynth::Z3ExprAdapter::getNumeralCppInt	(	z3::model &	m,
		const Node *	r
	)

getNumeralInt()

int ilasynth::Z3ExprAdapter::getNumeralInt	(	z3::model &	m,
		const Node *	r
	)

operator()()

virtual void ilasynth::Z3ExprAdapter::operator() ( const Node *  n )

virtual

setNameSuffix()

void ilasynth::Z3ExprAdapter::setNameSuffix ( const std::string &  ns )

inline

Member Data Documentation

c

z3::context& ilasynth::Z3ExprAdapter::c

protected

cnstmap

expr_map_t ilasynth::Z3ExprAdapter::cnstmap

protected

exprmap

expr_map_t ilasynth::Z3ExprAdapter::exprmap

protected

name_suffix

std::string ilasynth::Z3ExprAdapter::name_suffix

protected

Added to every name.

simplify

bool ilasynth::Z3ExprAdapter::simplify

suffix

std::string ilasynth::Z3ExprAdapter::suffix

protected

---

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

• smt.hpp