ilasynth::Synthesizer Class Reference

#include <synthesizer.hpp>

Classes
struct	init_assump_t

Public Member Functions
	Synthesizer (Abstraction &abs, const std::vector< nmap_t *> &maps)
	~Synthesizer ()
void	synthesizeAll (PyObject *pyfun)
void	synthesizeReg (nmap_t::iterator pos, PyObject *pyfun)

Protected Member Functions
void	_addExpr (const nptr_t &expr, Z3ExprAdapter &c1, Z3ExprAdapter &c2)
std::unique_ptr< DistInput >	_getDistInput (z3::expr y)
nptr_t	_synthesize (const std::string &name, const nptr_t &de_expr, const nptr_t &expr, const z3::expr &y, PyObject *pyfun)
nptr_t	_synthesizeEx (const std::string &name, const nptr_t &de_expr, const nptr_t &expr, const z3::expr &y, PyObject *pyfun)
z3::expr	_createSynMiter (const nptr_t &ex)
void	_initSynthesis ()
nptr_t	_synthesizeOp (const std::string &name, const nptr_t &var, nptr_vec_t &next_vec, const nptr_t &next, PyObject *pyfun)
nptr_t	_getCombinedExpr (const nptr_t &var, const nptr_vec_t &next_vec)
bool	_eq (const nptr_t &n1, const nptr_t &n2)
void	_addConstRegAssumps ()
void	_npair_check ()

Protected Attributes
Abstraction &	abs
const std::vector< nmap_t * >	maps
SupportVars	decodeSupport
int	MAX_SYN_ITER
z3::context	c
z3::solver	S
z3::solver	Sp
Z3ExprAdapter	c1
Z3ExprAdapter	c2
DITree	ditree

Static Protected Attributes
static const char *	suffix1
static const char *	suffix2

Friends
struct	init_assump_t
class	DITree

Constructor & Destructor Documentation

Synthesizer()

ilasynth::Synthesizer::Synthesizer	(	Abstraction &	abs,
		const std::vector< nmap_t *> &	maps
	)

~Synthesizer()

ilasynth::Synthesizer::~Synthesizer

(

)

Member Function Documentation

_addConstRegAssumps()

void ilasynth::Synthesizer::_addConstRegAssumps ( )

protected

_addExpr()

void ilasynth::Synthesizer::_addExpr ( const nptr_t &  expr, Z3ExprAdapter &  c1, Z3ExprAdapter &  c2  )

protected

_createSynMiter()

z3::expr ilasynth::Synthesizer::_createSynMiter ( const nptr_t &  ex )

protected

_eq()

bool ilasynth::Synthesizer::_eq ( const nptr_t &  n1, const nptr_t &  n2  )

protected

_getCombinedExpr()

nptr_t ilasynth::Synthesizer::_getCombinedExpr ( const nptr_t &  var, const nptr_vec_t &  next_vec  )

protected

_getDistInput()

std::unique_ptr<DistInput> ilasynth::Synthesizer::_getDistInput ( z3::expr  y )

protected

_initSynthesis()

void ilasynth::Synthesizer::_initSynthesis ( )

protected

_npair_check()

void ilasynth::Synthesizer::_npair_check ( )

protected

_synthesize()

nptr_t ilasynth::Synthesizer::_synthesize ( const std::string &  name, const nptr_t &  de_expr, const nptr_t &  expr, const z3::expr &  y, PyObject *  pyfun  )

protected

_synthesizeEx()

nptr_t ilasynth::Synthesizer::_synthesizeEx ( const std::string &  name, const nptr_t &  de_expr, const nptr_t &  expr, const z3::expr &  y, PyObject *  pyfun  )

protected

_synthesizeOp()

nptr_t ilasynth::Synthesizer::_synthesizeOp ( const std::string &  name, const nptr_t &  var, nptr_vec_t &  next_vec, const nptr_t &  next, PyObject *  pyfun  )

protected

synthesizeAll()

void ilasynth::Synthesizer::synthesizeAll

(

PyObject *

pyfun

)

synthesizeReg()

void ilasynth::Synthesizer::synthesizeReg	(	nmap_t::iterator	pos,
		PyObject *	pyfun
	)

Friends And Related Function Documentation

DITree

friend class DITree

friend

init_assump_t

friend struct init_assump_t

friend

Member Data Documentation

abs

Abstraction& ilasynth::Synthesizer::abs

protected

c

z3::context ilasynth::Synthesizer::c

protected

c1

Z3ExprAdapter ilasynth::Synthesizer::c1

protected

c2

Z3ExprAdapter ilasynth::Synthesizer::c2

protected

decodeSupport

SupportVars ilasynth::Synthesizer::decodeSupport

protected

ditree

DITree ilasynth::Synthesizer::ditree

protected

maps

const std::vector<nmap_t*> ilasynth::Synthesizer::maps

protected

MAX_SYN_ITER

int ilasynth::Synthesizer::MAX_SYN_ITER

protected

S

z3::solver ilasynth::Synthesizer::S

protected

Sp

z3::solver ilasynth::Synthesizer::Sp

protected

suffix1

const char* ilasynth::Synthesizer::suffix1

staticprotected

suffix2

const char* ilasynth::Synthesizer::suffix2

staticprotected

---

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

• synthesizer.hpp