ilasynth::BoogieTranslator Class Reference

#include <boogie.hpp>

Public Types
typedef std::vector< z3::expr >	exprvec_t
typedef std::stack< exprvec_t >	stack_t

Public Member Functions
	BoogieTranslator (Abstraction *a)
virtual	~BoogieTranslator ()
void	translate ()

Private Member Functions
bool	isConstant (const npair_t *obj)

Private Attributes
Abstraction *	abs
nodeset_t	fetchVars
nodevec_t	inpFV
nodevec_t	varFV
nodevec_t	constFV
exprvec_t	constEx
stack_t	states
z3::context	c_
Z3ExprAdapter	c

Member Typedef Documentation

exprvec_t

typedef std::vector<z3::expr> ilasynth::BoogieTranslator::exprvec_t

stack_t

typedef std::stack<exprvec_t> ilasynth::BoogieTranslator::stack_t

Constructor & Destructor Documentation

BoogieTranslator()

ilasynth::BoogieTranslator::BoogieTranslator

(

Abstraction *

a

)

~BoogieTranslator()

virtual ilasynth::BoogieTranslator::~BoogieTranslator ( )

virtual

Member Function Documentation

isConstant()

bool ilasynth::BoogieTranslator::isConstant ( const npair_t *  obj )

private

translate()

void ilasynth::BoogieTranslator::translate

(

)

Member Data Documentation

abs

Abstraction* ilasynth::BoogieTranslator::abs

private

c

Z3ExprAdapter ilasynth::BoogieTranslator::c

private

c_

z3::context ilasynth::BoogieTranslator::c_

private

constEx

exprvec_t ilasynth::BoogieTranslator::constEx

private

constFV

nodevec_t ilasynth::BoogieTranslator::constFV

private

fetchVars

nodeset_t ilasynth::BoogieTranslator::fetchVars

private

inpFV

nodevec_t ilasynth::BoogieTranslator::inpFV

private

states

stack_t ilasynth::BoogieTranslator::states

private

varFV

nodevec_t ilasynth::BoogieTranslator::varFV

private

---

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

• boogie.hpp