ilang::UnrollerSmt< Generator > Class Template Reference

Base class for unrolling ILA execution in different settings. More...

#include <u_unroller_smt.h>

Inheritance diagram for ilang::UnrollerSmt< Generator >:

Public Member Functions
	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 Types
typedef std::vector< ExprPtr >	IlaExprVec
typedef std::vector< SmtExpr >	SmtExprVec

Protected Member Functions
virtual void	SetDecidingVars ()=0
	Setup the deciding variabels.
virtual void	MakeOneTransition (const size_t &idx)=0
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.

Protected Attributes
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::UnrollerSmt< Generator >

Base class for unrolling ILA execution in different settings.

Member Function Documentation

template<class Generator >

virtual void ilang::UnrollerSmt< Generator >::MakeOneTransition ( const size_t &  idx )

protectedpure virtual

Make one transition (step) and setup the update_holder_ and assert_holder_ accordingly

Implemented in ilang::PathUnroller< Generator >.

---

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

• u_unroller_smt.h