ilasynth::SynRewriter Class Reference

#include <synrewriter.hpp>

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

Public Member Functions
	SynRewriter (z3::model &m, Z3ExprAdapter &a)
	~SynRewriter ()
void	operator() (const Node *n)
nptr_t	rewrite (const Node *n)

Protected Member Functions
void	getNewArgs (const Node *n, nptr_vec_t &args)

Protected Attributes
expr_map_t	exprmap
z3::model &	m
Z3ExprAdapter &	adapter

Private Member Functions
template<typename T >
void	_synChoiceExpr (const ChoiceExpr< T > *op)

Member Typedef Documentation

expr_map_t

typedef std::unordered_map<const Node*, nptr_t, decltype(&nodeHash), decltype(&nodeEqual)> ilasynth::SynRewriter::expr_map_t

Constructor & Destructor Documentation

SynRewriter()

ilasynth::SynRewriter::SynRewriter	(	z3::model &	m,
		Z3ExprAdapter &	a
	)

~SynRewriter()

ilasynth::SynRewriter::~SynRewriter

(

)

Member Function Documentation

_synChoiceExpr()

template<typename T >

void ilasynth::SynRewriter::_synChoiceExpr ( const ChoiceExpr< T > *  op )

inlineprivate

getNewArgs()

void ilasynth::SynRewriter::getNewArgs ( const Node *  n, nptr_vec_t &  args  )

protected

operator()()

void ilasynth::SynRewriter::operator()

(

const Node *

n

)

rewrite()

nptr_t ilasynth::SynRewriter::rewrite

(

const Node *

n

)

Member Data Documentation

adapter

Z3ExprAdapter& ilasynth::SynRewriter::adapter

protected

exprmap

expr_map_t ilasynth::SynRewriter::exprmap

protected

m

z3::model& ilasynth::SynRewriter::m

protected

---

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

• synrewriter.hpp