#include <horn.hpp>

Classes
struct	Instr_t

Public Member Functions
	HornTranslator (Abstraction *abs, const std::string &name)

virtual	~HornTranslator ()

void	hornifyAll (const std::string &fileName)

hvptr_t	hornifyNode (NodeRef *node, const std::string &ruleName)

void	generateMapping (const std::string &type)

void	exportHorn (const std::string &fileName)

void	setIteAsNode (bool iteAsNode)

void	setBvAsInt (bool bvAsInt)

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

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

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

void	depthFirstTraverse (nptr_t n)

void	operator() (nptr_t n)

std::string	addSuffix (const std::string &name, const int &idx) const

hvptr_t	copyVar (hvptr_t v, const int &idx)

Private Member Functions
hvptr_t	getVar (nptr_t n)

hvptr_t	getVar (const std::string &s)

hcptr_t	addClause (hvptr_t v=NULL)

void	initVar (hvptr_t v, nptr_t n)

void	initVarBv (hvptr_t v, nptr_t n)

void	initVarInt (hvptr_t v, nptr_t n)

void	initVar (hvptr_t v, const std::string &s)

hvptr_t	getEqVar (hvptr_t a, hvptr_t b)

hvptr_t	getConVar (hvptr_t c)

bool	isITE (nptr_t n) const

void	initBoolOp (const BoolOp *n, hvptr_t v)

void	initBoolVar (const BoolVar *n, hvptr_t v)

void	initBoolConst (const BoolConst *n, hvptr_t v)

void	initBvOp (const BitvectorOp *n, hvptr_t v)

void	initBvVar (const BitvectorVar *n, hvptr_t v)

void	initBvConst (const BitvectorConst *n, hvptr_t v)

void	initMemOp (const MemOp *n, hvptr_t v)

void	initMemVar (const MemVar *n, hvptr_t v)

void	initMemConst (const MemConst *n, hvptr_t v)

void	initFuncVar (const FuncVar *n, hvptr_t v)

void	initBoolOpInt (const BoolOp *n, hvptr_t v)

void	initBoolVarInt (const BoolVar *n, hvptr_t v)

void	initBoolConstInt (const BoolConst *n, hvptr_t v)

void	initBvOpInt (const BitvectorOp *n, hvptr_t v)

void	initBvVarInt (const BitvectorVar *n, hvptr_t v)

void	initBvConstInt (const BitvectorConst *n, hvptr_t v)

void	initMemOpInt (const MemOp *n, hvptr_t v)

void	initMemVarInt (const MemVar *n, hvptr_t v)

void	initMemConstInt (const MemConst *n, hvptr_t v)

void	initFuncVarInt (const FuncVar *n, hvptr_t v)

void	addBoolOp (const BoolOp *n, hvptr_t v)

void	addBoolVar (const BoolVar *n, hvptr_t v)

void	addBoolConst (const BoolConst *n, hvptr_t v)

void	addBvOp (const BitvectorOp *n, hvptr_t v)

void	addBvVar (const BitvectorVar *n, hvptr_t v)

void	addBvConst (const BitvectorConst *n, hvptr_t v)

void	addMemOp (const MemOp *n, hvptr_t v)

void	addMemVar (const MemVar *n, hvptr_t v)

void	addMemConst (const MemConst *n, hvptr_t v)

void	addFuncVar (const FuncVar *n, hvptr_t v)

std::string	genReadMemBlkExecLit (const std::string &mem, const std::string &addr, int addrWidth, int idx) const

std::string	genReadMemBlkExecBig (const std::string &mem, const std::string &addr, int addrWidth, int idx, int num) const

std::string	genStoreMemBlkExecLit (const std::string &mem, const std::string &addr, const std::string &data, int chunkSize, int chunkNum, int addrWidth, int idx) const

std::string	genStoreMemBlkExecBig (const std::string &mem, const std::string &addr, const std::string &data, int chunkSize, int chunkNum, int addrWidth, int idx) const

std::string	bvToString (mp_int_t val, int width) const

std::string	bvToString (int val, int width) const

void	genMemConstRules (const MemConst *n, hvptr_t v)

bool	isLongBv (const int &w) const

void	generateInterleaveMapping ()

void	generateBlockingMapping ()

HornRewriter *	generateLoopPredicate ()

void	allInterleaveMapping ()

Private Attributes
std::string	_name

Abstraction *	_abs

HornDB *	_db

bool	_iteAsNode

bool	_bvAsInt

int	_bvMaxSize

unsigned	_varCnt

std::map< nptr_t, hvptr_t >	_nVarMap

std::map< std::string, hvptr_t >	_sVarMap

hcptr_t	_curHc

std::set< std::string >	_states

std::map< std::string, struct Instr_t * >	_instrs

std::map< std::string, struct Instr_t * >	_childs

Constructor & Destructor Documentation

◆ HornTranslator()

ilasynth::HornTranslator::HornTranslator	(	Abstraction *	abs,
		const std::string &	name
	)

◆ ~HornTranslator()

virtual ilasynth::HornTranslator::~HornTranslator ( )

virtual

Member Function Documentation

◆ addBoolConst()

void ilasynth::HornTranslator::addBoolConst	(	const BoolConst *	n,
		hvptr_t	v
	)

private

◆ addBoolOp()

void ilasynth::HornTranslator::addBoolOp	(	const BoolOp *	n,
		hvptr_t	v
	)

private

◆ addBoolVar()

void ilasynth::HornTranslator::addBoolVar	(	const BoolVar *	n,
		hvptr_t	v
	)

private

◆ addBvConst()

void ilasynth::HornTranslator::addBvConst	(	const BitvectorConst *	n,
		hvptr_t	v
	)

private

◆ addBvOp()

void ilasynth::HornTranslator::addBvOp	(	const BitvectorOp *	n,
		hvptr_t	v
	)

private

◆ addBvVar()

void ilasynth::HornTranslator::addBvVar	(	const BitvectorVar *	n,
		hvptr_t	v
	)

private

◆ addChildInstr()

void ilasynth::HornTranslator::addChildInstr	(	const std::string &	c,
		const std::string &	i,
		NodeRef *	d
	)

◆ addClause()

hcptr_t ilasynth::HornTranslator::addClause ( hvptr_t v = NULL )

private

◆ addFuncVar()

void ilasynth::HornTranslator::addFuncVar	(	const FuncVar *	n,
		hvptr_t	v
	)

private

◆ addInstr()

void ilasynth::HornTranslator::addInstr	(	const std::string &	i,
		NodeRef *	d
	)

◆ addMemConst()

void ilasynth::HornTranslator::addMemConst	(	const MemConst *	n,
		hvptr_t	v
	)

private

◆ addMemOp()

void ilasynth::HornTranslator::addMemOp	(	const MemOp *	n,
		hvptr_t	v
	)

private

◆ addMemVar()

void ilasynth::HornTranslator::addMemVar	(	const MemVar *	n,
		hvptr_t	v
	)

private

◆ addNext()

void ilasynth::HornTranslator::addNext	(	const std::string &	i,
		const std::string &	s,
		NodeRef *	n
	)

◆ addSuffix()

std::string ilasynth::HornTranslator::addSuffix	(	const std::string &	name,
		const int &	idx
	)		const

◆ allInterleaveMapping()

void ilasynth::HornTranslator::allInterleaveMapping ( )

private

◆ bvToString() [1/2]

std::string ilasynth::HornTranslator::bvToString	(	mp_int_t	val,
		int	width
	)		const

private

◆ bvToString() [2/2]

std::string ilasynth::HornTranslator::bvToString	(	int	val,
		int	width
	)		const

private

◆ copyVar()

hvptr_t ilasynth::HornTranslator::copyVar	(	hvptr_t	v,
		const int &	idx
	)

◆ depthFirstTraverse()

void ilasynth::HornTranslator::depthFirstTraverse ( nptr_t n )

◆ exportHorn()

void ilasynth::HornTranslator::exportHorn ( const std::string & fileName )

◆ generateBlockingMapping()

void ilasynth::HornTranslator::generateBlockingMapping ( )

private

◆ generateInterleaveMapping()

void ilasynth::HornTranslator::generateInterleaveMapping ( )

private

◆ generateLoopPredicate()

HornRewriter* ilasynth::HornTranslator::generateLoopPredicate ( )

private

◆ generateMapping()

void ilasynth::HornTranslator::generateMapping ( const std::string & type )

◆ genMemConstRules()

void ilasynth::HornTranslator::genMemConstRules	(	const MemConst *	n,
		hvptr_t	v
	)

private

◆ genReadMemBlkExecBig()

std::string ilasynth::HornTranslator::genReadMemBlkExecBig	(	const std::string &	mem,
		const std::string &	addr,
		int	addrWidth,
		int	idx,
		int	num
	)		const

private

◆ genReadMemBlkExecLit()

std::string ilasynth::HornTranslator::genReadMemBlkExecLit	(	const std::string &	mem,
		const std::string &	addr,
		int	addrWidth,
		int	idx
	)		const

private

◆ genStoreMemBlkExecBig()

std::string ilasynth::HornTranslator::genStoreMemBlkExecBig	(	const std::string &	mem,
		const std::string &	addr,
		const std::string &	data,
		int	chunkSize,
		int	chunkNum,
		int	addrWidth,
		int	idx
	)		const

private

◆ genStoreMemBlkExecLit()

std::string ilasynth::HornTranslator::genStoreMemBlkExecLit	(	const std::string &	mem,
		const std::string &	addr,
		const std::string &	data,
		int	chunkSize,
		int	chunkNum,
		int	addrWidth,
		int	idx
	)		const

private

◆ getConVar()

hvptr_t ilasynth::HornTranslator::getConVar ( hvptr_t c )

private

◆ getEqVar()

hvptr_t ilasynth::HornTranslator::getEqVar	(	hvptr_t	a,
		hvptr_t	b
	)

private

◆ getVar() [1/2]

hvptr_t ilasynth::HornTranslator::getVar ( nptr_t n )

private

◆ getVar() [2/2]

hvptr_t ilasynth::HornTranslator::getVar ( const std::string & s )

private

◆ hornifyAll()

void ilasynth::HornTranslator::hornifyAll ( const std::string & fileName )

◆ hornifyNode()

hvptr_t ilasynth::HornTranslator::hornifyNode	(	NodeRef *	node,
		const std::string &	ruleName
	)

◆ initBoolConst()

void ilasynth::HornTranslator::initBoolConst	(	const BoolConst *	n,
		hvptr_t	v
	)

private

◆ initBoolConstInt()

void ilasynth::HornTranslator::initBoolConstInt	(	const BoolConst *	n,
		hvptr_t	v
	)

private

◆ initBoolOp()

void ilasynth::HornTranslator::initBoolOp	(	const BoolOp *	n,
		hvptr_t	v
	)

private

◆ initBoolOpInt()

void ilasynth::HornTranslator::initBoolOpInt	(	const BoolOp *	n,
		hvptr_t	v
	)

private

◆ initBoolVar()

void ilasynth::HornTranslator::initBoolVar	(	const BoolVar *	n,
		hvptr_t	v
	)

private

◆ initBoolVarInt()

void ilasynth::HornTranslator::initBoolVarInt	(	const BoolVar *	n,
		hvptr_t	v
	)

private

◆ initBvConst()

void ilasynth::HornTranslator::initBvConst	(	const BitvectorConst *	n,
		hvptr_t	v
	)

private

◆ initBvConstInt()

void ilasynth::HornTranslator::initBvConstInt	(	const BitvectorConst *	n,
		hvptr_t	v
	)

private

◆ initBvOp()

void ilasynth::HornTranslator::initBvOp	(	const BitvectorOp *	n,
		hvptr_t	v
	)

private

◆ initBvOpInt()

void ilasynth::HornTranslator::initBvOpInt	(	const BitvectorOp *	n,
		hvptr_t	v
	)

private

◆ initBvVar()

void ilasynth::HornTranslator::initBvVar	(	const BitvectorVar *	n,
		hvptr_t	v
	)

private

◆ initBvVarInt()

void ilasynth::HornTranslator::initBvVarInt	(	const BitvectorVar *	n,
		hvptr_t	v
	)

private

◆ initFuncVar()

void ilasynth::HornTranslator::initFuncVar	(	const FuncVar *	n,
		hvptr_t	v
	)

private

◆ initFuncVarInt()

void ilasynth::HornTranslator::initFuncVarInt	(	const FuncVar *	n,
		hvptr_t	v
	)

private

◆ initMemConst()

void ilasynth::HornTranslator::initMemConst	(	const MemConst *	n,
		hvptr_t	v
	)

private

◆ initMemConstInt()

void ilasynth::HornTranslator::initMemConstInt	(	const MemConst *	n,
		hvptr_t	v
	)

private

◆ initMemOp()

void ilasynth::HornTranslator::initMemOp	(	const MemOp *	n,
		hvptr_t	v
	)

private

◆ initMemOpInt()

void ilasynth::HornTranslator::initMemOpInt	(	const MemOp *	n,
		hvptr_t	v
	)

private

◆ initMemVar()

void ilasynth::HornTranslator::initMemVar	(	const MemVar *	n,
		hvptr_t	v
	)

private

◆ initMemVarInt()

void ilasynth::HornTranslator::initMemVarInt	(	const MemVar *	n,
		hvptr_t	v
	)

private

◆ initVar() [1/2]

void ilasynth::HornTranslator::initVar	(	hvptr_t	v,
		nptr_t	n
	)

private

◆ initVar() [2/2]

void ilasynth::HornTranslator::initVar	(	hvptr_t	v,
		const std::string &	s
	)

private

◆ initVarBv()

void ilasynth::HornTranslator::initVarBv	(	hvptr_t	v,
		nptr_t	n
	)

private

◆ initVarInt()

void ilasynth::HornTranslator::initVarInt	(	hvptr_t	v,
		nptr_t	n
	)

private

◆ isITE()

bool ilasynth::HornTranslator::isITE ( nptr_t n ) const

private

◆ isLongBv()

bool ilasynth::HornTranslator::isLongBv ( const int & w ) const

private

◆ operator()()

void ilasynth::HornTranslator::operator() ( nptr_t n )

◆ setBvAsInt()

void ilasynth::HornTranslator::setBvAsInt ( bool bvAsInt )

◆ setIteAsNode()

void ilasynth::HornTranslator::setIteAsNode ( bool iteAsNode )

Member Data Documentation

◆ _abs

Abstraction* ilasynth::HornTranslator::_abs

private

◆ _bvAsInt

bool ilasynth::HornTranslator::_bvAsInt

private

◆ _bvMaxSize

int ilasynth::HornTranslator::_bvMaxSize

private

◆ _childs

std::map<std::string, struct Instr_t*> ilasynth::HornTranslator::_childs

private

◆ _curHc

hcptr_t ilasynth::HornTranslator::_curHc

private

◆ _db

HornDB* ilasynth::HornTranslator::_db

private

◆ _instrs

std::map<std::string, struct Instr_t*> ilasynth::HornTranslator::_instrs

private

◆ _iteAsNode

bool ilasynth::HornTranslator::_iteAsNode

private

◆ _name

std::string ilasynth::HornTranslator::_name

private

◆ _nVarMap

std::map<nptr_t, hvptr_t> ilasynth::HornTranslator::_nVarMap

private

◆ _states

std::set<std::string> ilasynth::HornTranslator::_states

private

◆ _sVarMap

std::map<std::string, hvptr_t> ilasynth::HornTranslator::_sVarMap

private

◆ _varCnt

unsigned ilasynth::HornTranslator::_varCnt

private

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

horn.hpp

Classes

Public Member Functions

Private Member Functions

Private Attributes

Constructor & Destructor Documentation

◆ HornTranslator()

◆ ~HornTranslator()

Member Function Documentation

◆ addBoolConst()

◆ addBoolOp()

◆ addBoolVar()

◆ addBvConst()

◆ addBvOp()

◆ addBvVar()

◆ addChildInstr()

◆ addClause()

◆ addFuncVar()

◆ addInstr()

◆ addMemConst()

◆ addMemOp()

◆ addMemVar()

◆ addNext()

◆ addSuffix()

◆ allInterleaveMapping()

◆ bvToString() [1/2]

◆ bvToString() [2/2]

◆ copyVar()

◆ depthFirstTraverse()

◆ exportHorn()

◆ generateBlockingMapping()

◆ generateInterleaveMapping()

◆ generateLoopPredicate()

◆ generateMapping()

◆ genMemConstRules()

◆ genReadMemBlkExecBig()

◆ genReadMemBlkExecLit()

◆ genStoreMemBlkExecBig()

◆ genStoreMemBlkExecLit()

◆ getConVar()

◆ getEqVar()

◆ getVar() [1/2]

◆ getVar() [2/2]

◆ hornifyAll()

◆ hornifyNode()

◆ initBoolConst()

◆ initBoolConstInt()

◆ initBoolOp()

◆ initBoolOpInt()

◆ initBoolVar()

◆ initBoolVarInt()

◆ initBvConst()

◆ initBvConstInt()

◆ initBvOp()

◆ initBvOpInt()

◆ initBvVar()

◆ initBvVarInt()

◆ initFuncVar()

◆ initFuncVarInt()

◆ initMemConst()

◆ initMemConstInt()

◆ initMemOp()

◆ initMemOpInt()

◆ initMemVar()

◆ initMemVarInt()

◆ initVar() [1/2]

◆ initVar() [2/2]

◆ initVarBv()

◆ initVarInt()

◆ isITE()

◆ isLongBv()

◆ operator()()

◆ setBvAsInt()

◆ setIteAsNode()

Member Data Documentation

◆ _abs

◆ _bvAsInt

◆ _bvMaxSize

◆ _childs

◆ _curHc

◆ _db