ilang::IlaZ3Unroller Class Reference

The wrapper of generating z3::expr for verification. More...

#include <ilang++.h>

Public Member Functions
	IlaZ3Unroller (z3::context &ctx, const std::string &suff="")
	Default constructor.
	~IlaZ3Unroller ()
	Default virtual destructor.
void	AddGlobPred (const ExprRef &p)
	Add a predicate that should be asserted globally when unrolled.
void	AddInitPred (const ExprRef &p)
	Add a predicate that should be asserted in the initial condition.
void	AddStepPred (const int &k, const ExprRef &p)
	Add a predicate that should be asserted at the k-th step.
void	ClearGlobPred ()
	Clear the global predicates.
void	ClearInitPred ()
	Clear the initial predicates.
void	ClearStepPred ()
	Clear the step-specific predicates.
z3::expr	UnrollMonoConn (const Ila &top, const int &k, const int &init=0)
	Unroll the ILA monolithically with each step connected. More...
z3::expr	UnrollMonoFree (const Ila &top, const int &k, const int &init=0)
	Unroll the ILA monolithically with each step freely defined. More...
z3::expr	UnrollPathConn (const std::vector< InstrRef > &path, const int &init=0)
	Unroll a path with each step connected. More...
z3::expr	UnrollPathSubs (const std::vector< InstrRef > &path, const int &init=0)
	Unroll a path with each step connected with rewriting. More...
z3::expr	UnrollPathFree (const std::vector< InstrRef > &path, const int &init=0)
	Unroll a path with each step freely defined. More...
z3::expr	CurrState (const ExprRef &v, const int &t)
	Return the z3::expr representing the current state at the time.
z3::expr	NextState (const ExprRef &v, const int &t)
	Return the z3::expr representing the next state at the time.
z3::expr	GetZ3Expr (const ExprRef &v, const int &t=0)
	Return the z3::expr representing the current-based Expr at the time.
z3::expr	Equal (const ExprRef &va, const int &ta, const ExprRef &vb, const int &tb)
	Return the z3::expr representing a and b are equal at their time.
z3::func_decl	GetZ3FuncDecl (const FuncRef &f) const
	Return the z3::func_decl representing f.

Detailed Description

The wrapper of generating z3::expr for verification.

Member Function Documentation

z3::expr ilang::IlaZ3Unroller::UnrollMonoConn	(	const Ila &	top,
		const int &	k,
		const int &	init = 0
	)

Unroll the ILA monolithically with each step connected.

Parameters

[in]	top	the top-level ILA of the hierarchy.
[in]	k	the number of steps to unroll.
[in]	init	the starting time frame.

z3::expr ilang::IlaZ3Unroller::UnrollMonoFree	(	const Ila &	top,
		const int &	k,
		const int &	init = 0
	)

Unroll the ILA monolithically with each step freely defined.

Parameters

[in]	top	the top-level ILA of the hierarchy.
[in]	k	the number of steps to unroll.
[in]	init	the starting time frame.

z3::expr ilang::IlaZ3Unroller::UnrollPathConn	(	const std::vector< InstrRef > &	path,
		const int &	init = 0
	)

Unroll a path with each step connected.

Parameters

[in]	path	the sequence of instructions.
[in]	init	the starting time frame.

z3::expr ilang::IlaZ3Unroller::UnrollPathFree	(	const std::vector< InstrRef > &	path,
		const int &	init = 0
	)

Unroll a path with each step freely defined.

Parameters

[in]	path	the sequence of instructions.
[in]	init	the starting time frame.

z3::expr ilang::IlaZ3Unroller::UnrollPathSubs	(	const std::vector< InstrRef > &	path,
		const int &	init = 0
	)

Unroll a path with each step connected with rewriting.

Parameters

[in]	path	the sequence of instructions.
[in]	init	the starting time frame.

---

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

• ilang++.h