#include <abstraction.hpp>

Public Member Functions
	AbstractionWrapper (const std::string &name)

	AbstractionWrapper (Abstraction *parent, const std::string &name)

	AbstractionWrapper (const abstraction_ptr_t &a)

	~AbstractionWrapper ()

NodeRef *	addInp (const std::string &name, int width)

NodeRef *	addBit (const std::string &name)

NodeRef *	addReg (const std::string &name, int width)

NodeRef *	addMem (const std::string &name, int addrW, int dataW)

NodeRef *	addFun (const std::string &name, int retW, const py::list &l)

NodeRef *	getInp (const std::string &name)

NodeRef *	getBit (const std::string &name)

NodeRef *	getReg (const std::string &name)

NodeRef *	getMem (const std::string &name)

NodeRef *	getFun (const std::string &name)

void	setInit (const std::string &name, NodeRef *n)

NodeRef *	getInit (const std::string &name) const

void	setIpred (const std::string &name, NodeRef *n)

NodeRef *	getIpred (const std::string &name) const

void	setNext (const std::string &name, NodeRef *n)

NodeRef *	getNext (const std::string &name) const

NodeRef *	getNextI (const std::string &name, int i) const

AbstractionWrapper *	addUAbs (const std::string &name, NodeRef *valid)

AbstractionWrapper *	getUAbs (const std::string &name)

void	connectUInst (const std::string &name, const AbstractionWrapper *uabs)

NodeRef *	bvConstLong (py::long_ l, int width)

NodeRef *	bvConstInt (unsigned int l, int width)

NodeRef *	boolConstB (bool b)

NodeRef *	boolConstI (int b)

NodeRef *	boolConstL (py::long_ b)

NodeRef *	memConst (const MemValues &mv)

NodeRef *	getFetchExpr () const

void	setFetchExpr (NodeRef *expr)

NodeRef *	getFetchValid () const

void	setFetchValid (NodeRef *expr)

void	setDecodeExpressions (const py::list &l)

py::list	getDecodeExpressions () const

void	addAssumption (NodeRef *expr)

py::list	getAllAssumptions () const

void	synthesizeAll (PyObject *fun)

void	synthesizeReg (const std::string &name, PyObject *fun)

NodeRef *	synthesizeElement (const std::string &name, NodeRef expr, PyObject fun)

void	exportOneToFile (NodeRef *node, const std::string &fileName) const

void	exportListToFile (const py::list &l, const std::string &fileName) const

void	exportAllToFile (const std::string &fileName) const

void	generateVerilogToFile (const std::string &fileName) const

void	generateVerilogModule (const std::string &fileName, const std::string &modName) const

NodeRef *	importOneFromFile (const std::string &fileName)

py::list	importListFromFile (const std::string &fileName)

void	importAllFromFile (const std::string &fileName)

void	generateSimToFile (const std::string &fileName) const

void	generateSimToDir (const std::string &dirName) const

void	generateCbmcCtoFile (const std::string &fileName) const

void	generateCbmcCtoDir (const std::string &dirName) const

bool	areEqual (NodeRef left, NodeRef right) const

bool	areEqualAssump (NodeRef assump, NodeRef left, NodeRef *right)

bool	areEqualUnrolled (unsigned n, NodeRef reg, NodeRef exp)

bool	bmcInit (NodeRef *assertion, unsigned n, bool init)

bool	bmcCond (NodeRef assertion, unsigned n, NodeRef assumpt)

MicroUnroller *	newUnroller (AbstractionWrapper *uILA, bool initCondition)

void	toBoogie (const std::string &name)

void	hornifyAll (const std::string &name)

void	hornifyNode (NodeRef *node, const std::string &rule)

void	generateHornMapping (const std::string &type)

void	exportHornToFile (const std::string &fileName)

void	hornifyIteAsNode (bool iteAsNode)

void	hornifyBvAsInt (bool bvAsInt)

void	addHornInstr (const std::string &i, NodeRef *d)

void	addHornNext (const std::string &i, const std::string &s, NodeRef *n)

void	addHornChild (const std::string &c, const std::string &i, NodeRef *d)

int	getEnParamSyn () const

void	setEnParamSyn (int en)

void	setVlgExpConfig (bool extMem, bool fAsM)

int	getReduceWhenImport () const

void	setReduceWhenImport (int en)

std::string	getName () const

const nmap_t &	getMems () const

const nmap_t &	getInps () const

const nmap_t &	getRegs () const

const nmap_t &	getBits () const

const nmap_t &	getFuns () const

Static Public Member Functions
static NodeRef *	bvConstLongStatic (py::long_ l, int width)

static NodeRef *	bvConstIntStatic (unsigned int l, int width)

static NodeRef *	boolConstBStatic (bool b)

static NodeRef *	boolConstIStatic (int b)

static NodeRef *	boolConstLStatic (py::long_ b)

static NodeRef *	memConstStatic (const MemValues &mv)

static bool	bmc (unsigned n1, AbstractionWrapper a1, NodeRef r1, unsigned n2, AbstractionWrapper a2, NodeRef r2)

static bool	EQcheckSimple (AbstractionWrapper a1, AbstractionWrapper a2)

static bool	EQcheck (MicroUnroller m1, MicroUnroller m2, const std::string &n1, const std::string &n2)

static void	EQcheckExport (const std::string &fn, MicroUnroller m1, MicroUnroller m2, const std::string &n1, const std::string &n2)

static bool	EQcheckWithAssump (MicroUnroller m1, MicroUnroller m2, const std::string &n1, const std::string &n2, py::list &assumps)

static void	EQcheckWithAssumpExport (const std::string &fn, MicroUnroller m1, MicroUnroller m2, const std::string &n1, const std::string &n2, py::list &assumps)

Public Attributes
abstraction_ptr_t	abs

Constructor & Destructor Documentation

◆ AbstractionWrapper() [1/3]

ilasynth::AbstractionWrapper::AbstractionWrapper ( const std::string & name )

inline

◆ AbstractionWrapper() [2/3]

ilasynth::AbstractionWrapper::AbstractionWrapper	(	Abstraction *	parent,
		const std::string &	name
	)

inline

◆ AbstractionWrapper() [3/3]

ilasynth::AbstractionWrapper::AbstractionWrapper ( const abstraction_ptr_t & a )

inline

◆ ~AbstractionWrapper()

ilasynth::AbstractionWrapper::~AbstractionWrapper ( )

inline

Member Function Documentation

◆ addAssumption()

void ilasynth::AbstractionWrapper::addAssumption ( NodeRef * expr )

inline

◆ addBit()

NodeRef* ilasynth::AbstractionWrapper::addBit ( const std::string & name )

inline

◆ addFun()

NodeRef* ilasynth::AbstractionWrapper::addFun	(	const std::string &	name,
		int	retW,
		const py::list &	l
	)

inline

◆ addHornChild()

void ilasynth::AbstractionWrapper::addHornChild	(	const std::string &	c,
		const std::string &	i,
		NodeRef *	d
	)

inline

◆ addHornInstr()

void ilasynth::AbstractionWrapper::addHornInstr	(	const std::string &	i,
		NodeRef *	d
	)

inline

◆ addHornNext()

void ilasynth::AbstractionWrapper::addHornNext	(	const std::string &	i,
		const std::string &	s,
		NodeRef *	n
	)

inline

◆ addInp()

NodeRef* ilasynth::AbstractionWrapper::addInp	(	const std::string &	name,
		int	width
	)

inline

◆ addMem()

NodeRef* ilasynth::AbstractionWrapper::addMem	(	const std::string &	name,
		int	addrW,
		int	dataW
	)

inline

◆ addReg()

NodeRef* ilasynth::AbstractionWrapper::addReg	(	const std::string &	name,
		int	width
	)

inline

◆ addUAbs()

AbstractionWrapper* ilasynth::AbstractionWrapper::addUAbs	(	const std::string &	name,
		NodeRef *	valid
	)

inline

◆ areEqual()

bool ilasynth::AbstractionWrapper::areEqual	(	NodeRef *	left,
		NodeRef *	right
	)		const

inline

◆ areEqualAssump()

bool ilasynth::AbstractionWrapper::areEqualAssump	(	NodeRef *	assump,
		NodeRef *	left,
		NodeRef *	right
	)

inline

◆ areEqualUnrolled()

bool ilasynth::AbstractionWrapper::areEqualUnrolled	(	unsigned	n,
		NodeRef *	reg,
		NodeRef *	exp
	)

inline

◆ bmc()

static bool ilasynth::AbstractionWrapper::bmc	(	unsigned	n1,
		AbstractionWrapper *	a1,
		NodeRef *	r1,
		unsigned	n2,
		AbstractionWrapper *	a2,
		NodeRef *	r2
	)

inlinestatic

◆ bmcCond()

bool ilasynth::AbstractionWrapper::bmcCond	(	NodeRef *	assertion,
		unsigned	n,
		NodeRef *	assumpt
	)

inline

◆ bmcInit()

bool ilasynth::AbstractionWrapper::bmcInit	(	NodeRef *	assertion,
		unsigned	n,
		bool	init
	)

inline

◆ boolConstB()

NodeRef* ilasynth::AbstractionWrapper::boolConstB ( bool b )

inline

◆ boolConstBStatic()

static NodeRef* ilasynth::AbstractionWrapper::boolConstBStatic ( bool b )

inlinestatic

◆ boolConstI()

NodeRef* ilasynth::AbstractionWrapper::boolConstI ( int b )

inline

◆ boolConstIStatic()

static NodeRef* ilasynth::AbstractionWrapper::boolConstIStatic ( int b )

inlinestatic

◆ boolConstL()

NodeRef* ilasynth::AbstractionWrapper::boolConstL ( py::long_ b )

inline

◆ boolConstLStatic()

static NodeRef* ilasynth::AbstractionWrapper::boolConstLStatic ( py::long_ b )

inlinestatic

◆ bvConstInt()

NodeRef* ilasynth::AbstractionWrapper::bvConstInt	(	unsigned int	l,
		int	width
	)

inline

◆ bvConstIntStatic()

static NodeRef* ilasynth::AbstractionWrapper::bvConstIntStatic	(	unsigned int	l,
		int	width
	)

inlinestatic

◆ bvConstLong()

NodeRef* ilasynth::AbstractionWrapper::bvConstLong	(	py::long_	l,
		int	width
	)

inline

◆ bvConstLongStatic()

static NodeRef* ilasynth::AbstractionWrapper::bvConstLongStatic	(	py::long_	l,
		int	width
	)

inlinestatic

◆ connectUInst()

void ilasynth::AbstractionWrapper::connectUInst	(	const std::string &	name,
		const AbstractionWrapper *	uabs
	)

inline

◆ EQcheck()

static bool ilasynth::AbstractionWrapper::EQcheck	(	MicroUnroller *	m1,
		MicroUnroller *	m2,
		const std::string &	n1,
		const std::string &	n2
	)

inlinestatic

◆ EQcheckExport()

static void ilasynth::AbstractionWrapper::EQcheckExport	(	const std::string &	fn,
		MicroUnroller *	m1,
		MicroUnroller *	m2,
		const std::string &	n1,
		const std::string &	n2
	)

inlinestatic

◆ EQcheckSimple()

static bool ilasynth::AbstractionWrapper::EQcheckSimple	(	AbstractionWrapper *	a1,
		AbstractionWrapper *	a2
	)

inlinestatic

◆ EQcheckWithAssump()

static bool ilasynth::AbstractionWrapper::EQcheckWithAssump	(	MicroUnroller *	m1,
		MicroUnroller *	m2,
		const std::string &	n1,
		const std::string &	n2,
		py::list &	assumps
	)

inlinestatic

◆ EQcheckWithAssumpExport()

static void ilasynth::AbstractionWrapper::EQcheckWithAssumpExport	(	const std::string &	fn,
		MicroUnroller *	m1,
		MicroUnroller *	m2,
		const std::string &	n1,
		const std::string &	n2,
		py::list &	assumps
	)

inlinestatic

◆ exportAllToFile()

void ilasynth::AbstractionWrapper::exportAllToFile ( const std::string & fileName ) const

inline

◆ exportHornToFile()

void ilasynth::AbstractionWrapper::exportHornToFile ( const std::string & fileName )

inline

◆ exportListToFile()

void ilasynth::AbstractionWrapper::exportListToFile	(	const py::list &	l,
		const std::string &	fileName
	)		const

inline

◆ exportOneToFile()

void ilasynth::AbstractionWrapper::exportOneToFile	(	NodeRef *	node,
		const std::string &	fileName
	)		const

inline

◆ generateCbmcCtoDir()

void ilasynth::AbstractionWrapper::generateCbmcCtoDir ( const std::string & dirName ) const

inline

◆ generateCbmcCtoFile()

void ilasynth::AbstractionWrapper::generateCbmcCtoFile ( const std::string & fileName ) const

inline

◆ generateHornMapping()

void ilasynth::AbstractionWrapper::generateHornMapping ( const std::string & type )

inline

◆ generateSimToDir()

void ilasynth::AbstractionWrapper::generateSimToDir ( const std::string & dirName ) const

inline

◆ generateSimToFile()

void ilasynth::AbstractionWrapper::generateSimToFile ( const std::string & fileName ) const

inline

◆ generateVerilogModule()

void ilasynth::AbstractionWrapper::generateVerilogModule	(	const std::string &	fileName,
		const std::string &	modName
	)		const

inline

◆ generateVerilogToFile()

void ilasynth::AbstractionWrapper::generateVerilogToFile ( const std::string & fileName ) const

inline

◆ getAllAssumptions()

py::list ilasynth::AbstractionWrapper::getAllAssumptions ( ) const

inline

◆ getBit()

NodeRef* ilasynth::AbstractionWrapper::getBit ( const std::string & name )

inline

◆ getBits()

const nmap_t& ilasynth::AbstractionWrapper::getBits ( ) const

inline

◆ getDecodeExpressions()

py::list ilasynth::AbstractionWrapper::getDecodeExpressions ( ) const

inline

◆ getEnParamSyn()

int ilasynth::AbstractionWrapper::getEnParamSyn ( ) const

inline

◆ getFetchExpr()

NodeRef* ilasynth::AbstractionWrapper::getFetchExpr ( ) const

inline

◆ getFetchValid()

NodeRef* ilasynth::AbstractionWrapper::getFetchValid ( ) const

inline

◆ getFun()

NodeRef* ilasynth::AbstractionWrapper::getFun ( const std::string & name )

inline

◆ getFuns()

const nmap_t& ilasynth::AbstractionWrapper::getFuns ( ) const

inline

◆ getInit()

NodeRef* ilasynth::AbstractionWrapper::getInit ( const std::string & name ) const

inline

◆ getInp()

NodeRef* ilasynth::AbstractionWrapper::getInp ( const std::string & name )

inline

◆ getInps()

const nmap_t& ilasynth::AbstractionWrapper::getInps ( ) const

inline

◆ getIpred()

NodeRef* ilasynth::AbstractionWrapper::getIpred ( const std::string & name ) const

inline

◆ getMem()

NodeRef* ilasynth::AbstractionWrapper::getMem ( const std::string & name )

inline

◆ getMems()

const nmap_t& ilasynth::AbstractionWrapper::getMems ( ) const

inline

◆ getName()

std::string ilasynth::AbstractionWrapper::getName ( ) const

inline

◆ getNext()

NodeRef* ilasynth::AbstractionWrapper::getNext ( const std::string & name ) const

inline

◆ getNextI()

NodeRef* ilasynth::AbstractionWrapper::getNextI	(	const std::string &	name,
		int	i
	)		const

inline

◆ getReduceWhenImport()

int ilasynth::AbstractionWrapper::getReduceWhenImport ( ) const

inline

◆ getReg()

NodeRef* ilasynth::AbstractionWrapper::getReg ( const std::string & name )

inline

◆ getRegs()

const nmap_t& ilasynth::AbstractionWrapper::getRegs ( ) const

inline

◆ getUAbs()

AbstractionWrapper* ilasynth::AbstractionWrapper::getUAbs ( const std::string & name )

inline

◆ hornifyAll()

void ilasynth::AbstractionWrapper::hornifyAll ( const std::string & name )

inline

◆ hornifyBvAsInt()

void ilasynth::AbstractionWrapper::hornifyBvAsInt ( bool bvAsInt )

inline

◆ hornifyIteAsNode()

void ilasynth::AbstractionWrapper::hornifyIteAsNode ( bool iteAsNode )

inline

◆ hornifyNode()

void ilasynth::AbstractionWrapper::hornifyNode	(	NodeRef *	node,
		const std::string &	rule
	)

inline

◆ importAllFromFile()

void ilasynth::AbstractionWrapper::importAllFromFile ( const std::string & fileName )

inline

◆ importListFromFile()

py::list ilasynth::AbstractionWrapper::importListFromFile ( const std::string & fileName )

inline

◆ importOneFromFile()

NodeRef* ilasynth::AbstractionWrapper::importOneFromFile ( const std::string & fileName )

inline

◆ memConst()

NodeRef* ilasynth::AbstractionWrapper::memConst ( const MemValues & mv )

inline

◆ memConstStatic()

static NodeRef* ilasynth::AbstractionWrapper::memConstStatic ( const MemValues & mv )

inlinestatic

◆ newUnroller()

MicroUnroller* ilasynth::AbstractionWrapper::newUnroller	(	AbstractionWrapper *	uILA,
		bool	initCondition
	)

inline

◆ setDecodeExpressions()

void ilasynth::AbstractionWrapper::setDecodeExpressions ( const py::list & l )

inline

◆ setEnParamSyn()

void ilasynth::AbstractionWrapper::setEnParamSyn ( int en )

inline

◆ setFetchExpr()

void ilasynth::AbstractionWrapper::setFetchExpr ( NodeRef * expr )

inline

◆ setFetchValid()

void ilasynth::AbstractionWrapper::setFetchValid ( NodeRef * expr )

inline

◆ setInit()

void ilasynth::AbstractionWrapper::setInit	(	const std::string &	name,
		NodeRef *	n
	)

inline

◆ setIpred()

void ilasynth::AbstractionWrapper::setIpred	(	const std::string &	name,
		NodeRef *	n
	)

inline

◆ setNext()

void ilasynth::AbstractionWrapper::setNext	(	const std::string &	name,
		NodeRef *	n
	)

inline

◆ setReduceWhenImport()

void ilasynth::AbstractionWrapper::setReduceWhenImport ( int en )

inline

◆ setVlgExpConfig()

void ilasynth::AbstractionWrapper::setVlgExpConfig	(	bool	extMem,
		bool	fAsM
	)

inline

◆ synthesizeAll()

void ilasynth::AbstractionWrapper::synthesizeAll ( PyObject * fun )

inline

◆ synthesizeElement()

NodeRef* ilasynth::AbstractionWrapper::synthesizeElement	(	const std::string &	name,
		NodeRef *	expr,
		PyObject *	fun
	)

inline

◆ synthesizeReg()

void ilasynth::AbstractionWrapper::synthesizeReg	(	const std::string &	name,
		PyObject *	fun
	)

inline

◆ toBoogie()

void ilasynth::AbstractionWrapper::toBoogie ( const std::string & name )

inline

Member Data Documentation

◆ abs

abstraction_ptr_t ilasynth::AbstractionWrapper::abs

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

abstraction.hpp

Public Member Functions

Static Public Member Functions

Public Attributes

Constructor & Destructor Documentation

◆ AbstractionWrapper() [1/3]

◆ AbstractionWrapper() [2/3]

◆ AbstractionWrapper() [3/3]

◆ ~AbstractionWrapper()

Member Function Documentation

◆ addAssumption()

◆ addBit()

◆ addFun()

◆ addHornChild()

◆ addHornInstr()

◆ addHornNext()

◆ addInp()

◆ addMem()

◆ addReg()

◆ addUAbs()

◆ areEqual()

◆ areEqualAssump()

◆ areEqualUnrolled()

◆ bmc()

◆ bmcCond()

◆ bmcInit()

◆ boolConstB()

◆ boolConstBStatic()

◆ boolConstI()

◆ boolConstIStatic()

◆ boolConstL()

◆ boolConstLStatic()

◆ bvConstInt()

◆ bvConstIntStatic()

◆ bvConstLong()

◆ bvConstLongStatic()

◆ connectUInst()

◆ EQcheck()

◆ EQcheckExport()

◆ EQcheckSimple()

◆ EQcheckWithAssump()

◆ EQcheckWithAssumpExport()

◆ exportAllToFile()

◆ exportHornToFile()

◆ exportListToFile()

◆ exportOneToFile()

◆ generateCbmcCtoDir()

◆ generateCbmcCtoFile()

◆ generateHornMapping()

◆ generateSimToDir()

◆ generateSimToFile()

◆ generateVerilogModule()

◆ generateVerilogToFile()

◆ getAllAssumptions()

◆ getBit()

◆ getBits()

◆ getDecodeExpressions()

◆ getEnParamSyn()

◆ getFetchExpr()

◆ getFetchValid()

◆ getFun()

◆ getFuns()

◆ getInit()

◆ getInp()

◆ getInps()

◆ getIpred()

◆ getMem()

◆ getMems()

◆ getName()

◆ getNext()

◆ getNextI()

◆ getReduceWhenImport()

◆ getReg()

◆ getRegs()

◆ getUAbs()

◆ hornifyAll()

◆ hornifyBvAsInt()

◆ hornifyIteAsNode()

◆ hornifyNode()

◆ importAllFromFile()

◆ importListFromFile()