ilasynth::ITESimplifier Class Reference

#include <simplify.hpp>

Public Member Functions
	ITESimplifier (const nptr_t &assump)
virtual	~ITESimplifier ()
void	addAssumptions (const nptr_vec_t &assumps)
void	addAssumption (const nptr_t &a)
void	createClone (const Node *n)
void	reset ()
nptr_t	simplify (Node *n)

Private Member Functions
void	_add (const nptr_t &a, bool negate=false)
boost::logic::tribool	_isConstant (const nptr_t &c)
void	getNewArgs (const Node *op, nptr_vec_t &args)
nptr_t	getRepl (const Node *n) const
nptr_t	rewriteITE (const Node *n)
void	dfs (const Node *n)

Private Attributes
z3::context	ctx
z3::solver	S
Z3ExprAdapter	adapter
rwmap_t	rwmap

Constructor & Destructor Documentation

ITESimplifier()

ilasynth::ITESimplifier::ITESimplifier

(

const nptr_t &

assump

)

~ITESimplifier()

virtual ilasynth::ITESimplifier::~ITESimplifier ( )

virtual

Member Function Documentation

_add()

void ilasynth::ITESimplifier::_add ( const nptr_t &  a, bool  negate = false  )

private

_isConstant()

boost::logic::tribool ilasynth::ITESimplifier::_isConstant ( const nptr_t &  c )

private

addAssumption()

void ilasynth::ITESimplifier::addAssumption

(

const nptr_t &

a

)

addAssumptions()

void ilasynth::ITESimplifier::addAssumptions

(

const nptr_vec_t &

assumps

)

createClone()

void ilasynth::ITESimplifier::createClone

(

const Node *

n

)

dfs()

void ilasynth::ITESimplifier::dfs ( const Node *  n )

private

getNewArgs()

void ilasynth::ITESimplifier::getNewArgs ( const Node *  op, nptr_vec_t &  args  )

private

getRepl()

nptr_t ilasynth::ITESimplifier::getRepl ( const Node *  n ) const

private

reset()

void ilasynth::ITESimplifier::reset ( )

inline

rewriteITE()

nptr_t ilasynth::ITESimplifier::rewriteITE ( const Node *  n )

private

simplify()

nptr_t ilasynth::ITESimplifier::simplify

(

Node *

n

)

Member Data Documentation

adapter

Z3ExprAdapter ilasynth::ITESimplifier::adapter

private

ctx

z3::context ilasynth::ITESimplifier::ctx

private

rwmap

rwmap_t ilasynth::ITESimplifier::rwmap

private

S

z3::solver ilasynth::ITESimplifier::S

private

---

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

• simplify.hpp