ilang::CommDiag Class Reference

Generator for commutating diagram-based equivalence checking. More...

#include <v_eq_check_refinement.h>

Public Types
typedef MonoUnroll	Unroll

Public Member Functions
	CommDiag (z3::context &ctx, const CrrPtr crr)
	Default constructor.
	~CommDiag ()
	Default destructor.
bool	EqCheck (const int &max=10)
	Check equivalence between two models based on the refinement relation up to the given unrolling bound. More...
bool	IncEqCheck (const int &min=0, const int &max=10, const int &step=1)
	Incrementally checking equivalence between two models based on the refinement relation up to the given unrolling bound. More...
bool	IncCheck (const int &min=0, const int &max=10, const int &step=1)

Detailed Description

Generator for commutating diagram-based equivalence checking.

Member Function Documentation

bool ilang::CommDiag::EqCheck

(

const int &

max = 10

)

Check equivalence between two models based on the refinement relation up to the given unrolling bound.

Parameters

[in]

max

unrolling bound.

bool ilang::CommDiag::IncEqCheck	(	const int &	min = 0,
		const int &	max = 10,
		const int &	step = 1
	)

Incrementally checking equivalence between two models based on the refinement relation up to the given unrolling bound.

Parameters

[in]	min	#step of unrolling.
[in]	max	#step of unrolling.

---

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

• v_eq_check_refinement.h