ilang::PathUnroller< Generator > Class Template Reference

Application class for unrolling a sequence of instructions. More...

#include <u_unroller_smt.h>

Inheritance diagram for ilang::PathUnroller< Generator >:

Public Member Functions
	PathUnroller (SmtShim< Generator > &smt_shim, const std::string &suffix="")
	Constructor.
auto	Unroll (const InstrVec &seq, const size_t &begin=0)
	Unroll the sequence.
auto	UnrollWithStepsUnconnected (const InstrVec &seq, const size_t &begin)
	Unroll the sequence without connecting the steps.
Public Member Functions inherited from ilang::UnrollerSmt< Generator >
	UnrollerSmt (SmtShim< Generator > &smt_shim, const std::string &suffix)
	Constructor.
void	AssertGlobal (const ExprPtr &p)
	Add the predicate p to be asserted globally.
void	AssertInitial (const ExprPtr &p)
	Add the predicate p to be asserted at the first step (initial condition).
void	AssertStep (const ExprPtr &p, const int &k)
	Add the predicate p to be asserted at the k-th step.
void	ClearGlobalAssertion ()
	Clear all the global assertions.
void	ClearInitialAssertion ()
	Clear all the initial assertions.
void	ClearStepAssertion ()
	Clear all the step-specific assertions.
auto	GetSmtCurrent (const ExprPtr &expr, const size_t &k) const
	Return the SMT formula of expr at the beginning k-th step.
auto	GetSmtNext (const ExprPtr &expr, const size_t &k) const
	Return the SMT formula of expr at the end of k-th step.
auto	GetSmtFuncDecl (const FuncPtr &func) const
	Return the SMT function declaration of uninterpreted function func.

Protected Member Functions
void	SetDecidingVars ()
	Setup the deciding variables.
void	MakeOneTransition (const size_t &idx)
	Make one transition and setup holders accordingly.
Protected Member Functions inherited from ilang::UnrollerSmt< Generator >
SmtExpr	Unroll_ (const size_t &len, const size_t &begin)
	Unroll the whole sequence.
SmtExpr	UnrollWithStepsUnconnected_ (const size_t &len, const size_t &begin)
	Unroll the whole sequence without connecting the steps.

Additional Inherited Members
Protected Types inherited from ilang::UnrollerSmt< Generator >
typedef std::vector< ExprPtr >	IlaExprVec
typedef std::vector< SmtExpr >	SmtExprVec
Protected Attributes inherited from ilang::UnrollerSmt< Generator >
decltype(smt_gen_.GetShimExpr(nullptr,"")) typedef	SmtExpr
decltype(smt_gen_.GetShimFunc(nullptr)) typedef	SmtFunc
IlaExprVec	deciding_vars_
	Variables on which the instruction sequence depends.
IlaExprVec	update_holder_
	State update functions of the deciding variables.
IlaExprVec	assert_holder_
	Non-execution semantics (state update) properties.

Detailed Description

template<class Generator>
class ilang::PathUnroller< Generator >

Application class for unrolling a sequence of instructions.

---

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

• u_unroller_smt.h