Classes
class	IslCtx
	Move-only RAII owner of an isl_ctx. More...
class	IslHandle
	Move-only RAII owner of a reference-counted ISL object. More...

Typedefs
using	IslMap = IslHandle<isl_map, isl_map_free>
using	IslSet = IslHandle<isl_set, isl_set_free>
using	IslSpace = IslHandle<isl_space, isl_space_free>

Functions
bool	equal_on_domain (const MultiExpression &f, const MultiExpression &g, const Symbol indvar, const Assumptions &assums)
	Decides whether two access expressions denote the same cell at every point of the domain implied by `assums`.

Typedef Documentation

◆ IslMap

using sdfg::symbolic::polyhedral::IslMap = IslHandle<isl_map, isl_map_free>

◆ IslSet

using sdfg::symbolic::polyhedral::IslSet = IslHandle<isl_set, isl_set_free>

◆ IslSpace

using sdfg::symbolic::polyhedral::IslSpace = IslHandle<isl_space, isl_space_free>

Function Documentation

◆ equal_on_domain()

bool sdfg::symbolic::polyhedral::equal_on_domain	(	const MultiExpression &	f,
		const MultiExpression &	g,
		const Symbol	indvar,
		const Assumptions &	assums )

Decides whether two access expressions denote the same cell at every point of the domain implied by assums.

Semantically tests \(\forall x \in \mathrm{Dom}:\ f(x) = g(x)\) using ISL, i.e. affine/parametric equality rather than structural (SymEngine) equality. This proves equalities such as i*N + k ≡ k + N*i and rejects shifted accesses such as A[i] vs A[i-1] (a scan, not a reduction).

Parameters

f	First (e.g. write) access subset.
g	Second (e.g. read-back) access subset.
indvar	The loop induction variable (used to scope the domain).
assums	Assumptions/bounds shared by both accesses (same block/scope).

Returns: true iff f and g are provably equal across the whole domain.

Scalar accesses (empty subsets) are trivially equal. On any ISL parse/analysis failure the result is conservatively false.

Classes