ilasynth::Unroller Class Reference

#include <Unroller.hpp>

Public Member Functions
	Unroller (const char *suffix, Abstraction &abs, z3::context &c, z3::solver &s)
	~Unroller ()
void	Fr0Init (bool init)
void	setAssertion (z3::expr &a)
z3::expr &	getAssertion ()
void	pushAssertion ()
void	reset (z3::solver *solver)
void	addAssump (z3::expr &a)
	register literal as an assumption More...
std::vector< z3::expr > &	getAssumps ()
	return all assumptions More...
void	_initVar (Z3ExprAdapter &z3expr, const npair_t &p, int &cnt)
unsigned	frame ()
void	newFrame ()
unsigned	frames ()
void	addPrimaryInput (z3::expr in)
z3::expr &	getPrimaryInput (unsigned nFrame, int nNum)
std::vector< z3::expr > &	getPrimaryInputs (unsigned nFrame)
void	addOutput (z3::expr out)
z3::expr &	getOutput (unsigned nFrame, Node *var)
z3::expr &	getOutput (unsigned nFrame, int nNum)
std::vector< z3::expr > &	getOutputs (unsigned nFrame)
std::vector< std::vector< z3::expr > > &	getAllOutputs ()
void	addTr ()
z3::expr	subsFormula (Node *n)

Static Public Member Functions
static void	EvalEachFrame (z3::model &m, Unroller *u, std::ostream &cexf)

Private Member Functions
void	addTr0 ()
void	addTrN ()
bool	checkAbsNextExpNotNull ()

Private Attributes
std::string	m_sName
Abstraction *	m_pAbstraction
z3::context *	m_pContext
z3::solver *	m_pSolver
unsigned	m_nFrames
std::unordered_map< Node *, int, decltype(&nodeHash), decltype(&nodeEqual)>	m_mInputIndices
	Map between primary input pointers and indices into m_vPrimaryInputs. More...
std::vector< std::vector< z3::expr > >	m_vPrimaryInputs
	Primary Inputs, by frame. More...
std::unordered_map< Node *, int, decltype(&nodeHash), decltype(&nodeEqual)>	m_mStateIndices
	Map between state pointers and indices into m_vOutputs. More...
std::vector< std::vector< z3::expr > >	m_vOutputs
	Outputs, by frame. More...
std::vector< z3::expr >	m_Assumps
	All assumptions. More...
z3::expr *	m_pAssertion
	Expr for assertion to be checked. More...
bool	setInit

Constructor & Destructor Documentation

Unroller()

ilasynth::Unroller::Unroller ( const char *  suffix, Abstraction &  abs, z3::context &  c, z3::solver &  s  )

inline

~Unroller()

ilasynth::Unroller::~Unroller ( )

inline

Member Function Documentation

_initVar()

void ilasynth::Unroller::_initVar	(	Z3ExprAdapter &	z3expr,
		const npair_t &	p,
		int &	cnt
	)

addAssump()

void ilasynth::Unroller::addAssump ( z3::expr &  a )

inline

register literal as an assumption

addOutput()

void ilasynth::Unroller::addOutput ( z3::expr  out )

inline

addPrimaryInput()

void ilasynth::Unroller::addPrimaryInput ( z3::expr  in )

inline

addTr()

void ilasynth::Unroller::addTr ( )

inline

addTr0()

void ilasynth::Unroller::addTr0 ( )

private

addTrN()

void ilasynth::Unroller::addTrN ( )

private

checkAbsNextExpNotNull()

bool ilasynth::Unroller::checkAbsNextExpNotNull ( )

private

EvalEachFrame()

static void ilasynth::Unroller::EvalEachFrame ( z3::model &  m, Unroller *  u, std::ostream &  cexf  )

static

Fr0Init()

void ilasynth::Unroller::Fr0Init ( bool  init )

inline

frame()

unsigned ilasynth::Unroller::frame ( )

inline

frames()

unsigned ilasynth::Unroller::frames ( )

inline

getAllOutputs()

std::vector<std::vector<z3::expr> >& ilasynth::Unroller::getAllOutputs ( )

inline

getAssertion()

z3::expr& ilasynth::Unroller::getAssertion ( )

inline

getAssumps()

std::vector<z3::expr>& ilasynth::Unroller::getAssumps ( )

inline

return all assumptions

getOutput() [1/2]

z3::expr& ilasynth::Unroller::getOutput ( unsigned  nFrame, Node *  var  )

inline

getOutput() [2/2]

z3::expr& ilasynth::Unroller::getOutput ( unsigned  nFrame, int  nNum  )

inline

getOutputs()

std::vector<z3::expr>& ilasynth::Unroller::getOutputs ( unsigned  nFrame )

inline

getPrimaryInput()

z3::expr& ilasynth::Unroller::getPrimaryInput ( unsigned  nFrame, int  nNum  )

inline

getPrimaryInputs()

std::vector<z3::expr>& ilasynth::Unroller::getPrimaryInputs ( unsigned  nFrame )

inline

newFrame()

void ilasynth::Unroller::newFrame ( )

inline

pushAssertion()

void ilasynth::Unroller::pushAssertion ( )

inline

reset()

void ilasynth::Unroller::reset ( z3::solver *  solver )

inline

Reset everything

setAssertion()

void ilasynth::Unroller::setAssertion ( z3::expr &  a )

inline

subsFormula()

z3::expr ilasynth::Unroller::subsFormula

(

Node *

n

)

Member Data Documentation

m_Assumps

std::vector<z3::expr> ilasynth::Unroller::m_Assumps

private

All assumptions.

m_mInputIndices

std::unordered_map<Node*, int, decltype(&nodeHash), decltype(&nodeEqual)> ilasynth::Unroller::m_mInputIndices

private

Map between primary input pointers and indices into m_vPrimaryInputs.

m_mStateIndices

std::unordered_map<Node*, int, decltype(&nodeHash), decltype(&nodeEqual)> ilasynth::Unroller::m_mStateIndices

private

Map between state pointers and indices into m_vOutputs.

m_nFrames

unsigned ilasynth::Unroller::m_nFrames

private

m_pAbstraction

Abstraction* ilasynth::Unroller::m_pAbstraction

private

m_pAssertion

z3::expr* ilasynth::Unroller::m_pAssertion

private

Expr for assertion to be checked.

m_pContext

z3::context* ilasynth::Unroller::m_pContext

private

m_pSolver

z3::solver* ilasynth::Unroller::m_pSolver

private

m_sName

std::string ilasynth::Unroller::m_sName

private

m_vOutputs

std::vector<std::vector<z3::expr> > ilasynth::Unroller::m_vOutputs

private

Outputs, by frame.

m_vPrimaryInputs

std::vector<std::vector<z3::expr> > ilasynth::Unroller::m_vPrimaryInputs

private

Primary Inputs, by frame.

setInit

bool ilasynth::Unroller::setInit

private

---

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

• Unroller.hpp