sdfg::symbolic Namespace Reference

Namespaces
namespace	maps
namespace	polyhedral

Classes
class	Assumption
	Represents assumptions about a symbol's properties and behavior. More...
class	Assumptions
	Map from symbols to their assumptions. More...
class	CNFException
	Exception thrown when CNF conversion fails. More...
struct	DelinearizeResult
struct	Interval
	Result of bounding an expression: an interval [lower, upper]. More...
class	BoundAnalysis
	Computes bounds of symbolic expressions using assumptions. More...
class	AssumptionsBounds
	Bundles Assumptions with both the loose and tight BoundAnalysis derived from them. More...
struct	AffineDecomposition
	Result of affine decomposition of an expression w.r.t. More...
class	IModFunction
	Function class for integer modulo operation. More...
class	ZExtI64Function
	Function class for zero-extension to 64-bit integer. More...
class	TruncI32Function
	Function class for truncation to 32-bit integer. More...
class	SizeOfTypeFunction
	Function class representing sizeof for a type. More...
class	DynamicSizeOfFunction
	Function class for dynamic sizeof operation. More...
class	MallocUsableSizeFunction
	Function class for malloc_usable_size operation. More...

Typedefs
typedef std::vector< std::vector< Condition > >	CNF
	Conjunctive Normal Form representation.
typedef SymEngine::RCP< const SymEngine::MExprPoly >	Polynomial
	Type representing a SymEngine polynomial expression.
typedef std::unordered_map< Symbol, Expression, SymEngine::RCPBasicHash, SymEngine::RCPBasicKeyEq >	AffineCoeffs
	Map from symbols to their coefficients in an affine expression.
typedef SymEngine::RCP< const SymEngine::Symbol >	Symbol
	Reference-counted pointer to a SymEngine Symbol.
typedef SymEngine::RCP< const SymEngine::Number >	Number
	Reference-counted pointer to a SymEngine Number.
typedef SymEngine::RCP< const SymEngine::Integer >	Integer
	Reference-counted pointer to a SymEngine Integer constant.
typedef SymEngine::RCP< const SymEngine::Infty >	Infty
	Reference-counted pointer to a SymEngine Infinity value.
typedef SymEngine::RCP< const SymEngine::Basic >	Expression
	Reference-counted pointer to a symbolic expression (SymEngine Basic).
typedef SymEngine::RCP< const SymEngine::Boolean >	Condition
	Reference-counted pointer to a boolean condition expression.
typedef std::vector< Expression >	MultiExpression
	Vector of symbolic expressions for multi-dimensional operations.
typedef std::vector< Symbol >	SymbolVec
	Vector of symbols.
typedef std::set< Symbol, SymEngine::RCPBasicKeyLess >	SymbolSet
	Ordered set of symbols.
typedef std::unordered_map< Symbol, Expression, SymEngine::RCPBasicHash, SymEngine::RCPBasicKeyEq >	SymbolMap
	Map from symbols to expressions.
typedef std::vector< Symbol >	ExpressionVec
	Vector of expressions.
typedef std::set< Expression, SymEngine::RCPBasicKeyLess >	ExpressionSet
	Ordered set of expressions.
typedef std::unordered_map< Expression, Expression, SymEngine::RCPBasicHash, SymEngine::RCPBasicKeyEq >	ExpressionMap
	Map from expressions to expressions.
typedef SymEngine::map_basic_basic	ExpressionMapping

Functions
bool	substitute (Assumptions &assumptions, const symbolic::ExpressionMapping &replacements)
CNF	conjunctive_normal_form (const Condition cond)
	Convert a condition to conjunctive normal form.
bool	is_tautology (const std::vector< symbolic::Condition > &clause)
	Check if a disjunctive clause is a tautology.
DelinearizeResult	delinearize (const Expression &expr, const Assumptions &assums)
	Delinearizes a linearized expression into indices and dimensions based on parameter assumptions.
DelinearizeResult	delinearize (const Expression &expr, AssumptionsBounds &bounds)
	Same as delinearize, but reuses a caller-supplied AssumptionsBounds.
Expression	minimum (const Expression expr, const SymbolSet &parameters, const Assumptions &assumptions, bool tight)
	Compute the minimum of an expression.
Expression	maximum (const Expression expr, const SymbolSet &parameters, const Assumptions &assumptions, bool tight)
	Compute the maximum of an expression.
bool	is_nonneg (const Expression &expr, const SymbolSet &parameters, const Assumptions &assumptions, bool tight=false)
	Prove expr >= 0.
bool	is_positive (const Expression &expr, const SymbolSet &parameters, const Assumptions &assumptions, bool tight=false)
	Prove expr > 0.
bool	is_nonpos (const Expression &expr, const SymbolSet &parameters, const Assumptions &assumptions, bool tight=false)
	Prove expr <= 0.
bool	is_negative (const Expression &expr, const SymbolSet &parameters, const Assumptions &assumptions, bool tight=false)
	Prove expr < 0.
bool	is_ge (const Expression &a, const Expression &b, const SymbolSet &parameters, const Assumptions &assumptions, bool tight=false)
	Prove a >= b.
bool	is_gt (const Expression &a, const Expression &b, const SymbolSet &parameters, const Assumptions &assumptions, bool tight=false)
	Prove a > b.
bool	is_le (const Expression &a, const Expression &b, const SymbolSet &parameters, const Assumptions &assumptions, bool tight=false)
	Prove a <= b.
bool	is_lt (const Expression &a, const Expression &b, const SymbolSet &parameters, const Assumptions &assumptions, bool tight=false)
	Prove a < b.
bool	is_eq (const Expression &a, const Expression &b, const SymbolSet &parameters, const Assumptions &assumptions, bool tight=false)
	Prove a == b (both a >= b and a <= b).
bool	is_nonneg (const Expression &expr, BoundAnalysis &ba)
	Prove expr >= 0 using a pre-built BoundAnalysis.
bool	is_positive (const Expression &expr, BoundAnalysis &ba)
	Prove expr > 0 using a pre-built BoundAnalysis.
bool	is_nonpos (const Expression &expr, BoundAnalysis &ba)
	Prove expr <= 0 using a pre-built BoundAnalysis.
bool	is_negative (const Expression &expr, BoundAnalysis &ba)
	Prove expr < 0 using a pre-built BoundAnalysis.
bool	is_ge (const Expression &a, const Expression &b, BoundAnalysis &ba)
	Prove a >= b using a pre-built BoundAnalysis.
bool	is_gt (const Expression &a, const Expression &b, BoundAnalysis &ba)
	Prove a > b using a pre-built BoundAnalysis.
bool	is_le (const Expression &a, const Expression &b, BoundAnalysis &ba)
	Prove a <= b using a pre-built BoundAnalysis.
bool	is_lt (const Expression &a, const Expression &b, BoundAnalysis &ba)
	Prove a < b using a pre-built BoundAnalysis.
bool	is_eq (const Expression &a, const Expression &b, BoundAnalysis &ba)
	Prove a == b using a pre-built BoundAnalysis.
Polynomial	polynomial (const Expression expr, SymbolVec &symbols)
	Converts an Expression to a Polynomial.
AffineCoeffs	affine_coefficients (Polynomial poly)
	Converts a Polynomial of degree 1 to coefficient map.
bool	is_integer_affine (const Expression &expr)
	Whether expr is affine in all of its symbols with integer coefficients, e.g.
Expression	affine_inverse (AffineCoeffs coeffs, Symbol symbol)
	Computes the inverse function for an affine expression.
AffineDecomposition	affine_decomposition (const Expression &expr, const Symbol &symbol)
	Decomposes an expression into affine form w.r.t.
Expression	solve_affine_bound (const Expression &expr, const Symbol &symbol, const Expression &bound_value, bool is_lower_bound)
	Solves for a symbol's bound given an inequality constraint.
std::pair< Expression, Expression >	polynomial_div (const Expression &dividend, const Expression &divisor)
	Performs polynomial division.
bool	is_subset (const MultiExpression &expr1, const MultiExpression &expr2, const Assumptions &assums1, const Assumptions &assums2)
	Interprets the expressions as integer sets and checks if expr1 is a subset of expr2.
bool	is_subset (const MultiExpression &expr1, const MultiExpression &expr2, AssumptionsBounds &bounds1, AssumptionsBounds &bounds2)
	Same as is_subset, but reuses caller-supplied AssumptionsBounds.
bool	is_disjoint (const MultiExpression &expr1, const MultiExpression &expr2, const Assumptions &assums1, const Assumptions &assums2)
	Interprets the expressions as integer sets and checks if expr1 is disjoint from expr2.
bool	is_disjoint (const MultiExpression &expr1, const MultiExpression &expr2, AssumptionsBounds &bounds1, AssumptionsBounds &bounds2)
	Same as is_disjoint, but reuses caller-supplied AssumptionsBounds.
Symbol	symbol (const std::string &name)
	Creates a symbolic variable with the given name.
Integer	integer (int64_t value)
	Creates an integer constant.
Integer	zero ()
	Creates the integer constant 0.
Integer	one ()
	Creates the integer constant 1.
Condition	__false__ ()
	Creates a boolean false condition.
Condition	__true__ ()
	Creates a boolean true condition.
Symbol	__nullptr__ ()
	Creates a special null pointer symbol.
bool	is_nullptr (const Symbol symbol)
	Checks if a symbol is the null pointer.
bool	is_nullptr (const std::string &name)
	Same as is_nullptr(symbol(name)) without constructing a symbol.
bool	is_pointer (const Symbol symbol)
	Checks if a symbol represents a pointer.
bool	is_nv (const Symbol symbol)
	Checks if a symbol is an NVIDIA GPU built-in variable.
Condition	And (const Condition lhs, const Condition rhs)
	Logical AND of two conditions.
Condition	Or (const Condition lhs, const Condition rhs)
	Logical OR of two conditions.
Condition	Not (const Condition expr)
	Logical NOT (negation) of a condition.
bool	is_true (const Expression expr)
	Tests if an expression evaluates to true.
bool	is_false (const Expression expr)
	Tests if an expression evaluates to false.
Expression	add (const Expression lhs, const Expression rhs)
	Addition of two expressions.
Expression	sub (const Expression lhs, const Expression rhs)
	Subtraction of two expressions.
Expression	mul (const Expression lhs, const Expression rhs)
	Multiplication of two expressions.
Expression	div (const Expression lhs, const Expression rhs)
	Integer division idiv(lhs, rhs) with the semantics of signed C/C++ lhs / rhs on int64.
Expression	floor_div (const Expression lhs, const Expression divisor)
	Exact floor division floor(lhs / divisor) in terms of idiv.
Expression	ceil_div (const Expression dividend, const Expression divisor)
	Exact ceiling division ceil(dividend / divisor) in terms of idiv.
Expression	ceil_count (const Expression extent, const Expression chunk)
	Number of chunks of size chunk (positive) covering extent: max(0, ceil(extent / chunk)).
Expression	min (const Expression lhs, const Expression rhs)
	Minimum of two expressions.
Expression	max (const Expression lhs, const Expression rhs)
	Maximum of two expressions.
Expression	abs (const Expression expr)
	Absolute value of an expression.
Expression	mod (const Expression lhs, const Expression rhs)
	Integer remainder imod(lhs, rhs) with the semantics of signed C/C++ lhs % rhs on int64.
Expression	bit_xor (const Expression lhs, const Expression rhs)
	Bitwise XOR operation (integer).
Expression	pow (const Expression base, const Expression exp)
	Power/exponentiation operation.
Expression	zext_i64 (const Expression expr)
	Zero-extend to 64-bit integer.
Expression	trunc_i32 (const Expression expr)
	Truncate to 32-bit integer.
Expression	size_of_type (const types::IType &type)
	Computes the size of a type.
Expression	dynamic_sizeof (const Symbol symbol)
	Computes the dynamic size of a memory region.
Expression	malloc_usable_size (const Symbol symbol)
	Computes the usable size of a malloc allocation.
Condition	Eq (const Expression lhs, const Expression rhs)
	Equality comparison.
Condition	Ne (const Expression lhs, const Expression rhs)
	Inequality comparison.
Condition	Lt (const Expression lhs, const Expression rhs)
	Less-than comparison.
Condition	Gt (const Expression lhs, const Expression rhs)
	Greater-than comparison.
Condition	Le (const Expression lhs, const Expression rhs)
	Less-than-or-equal comparison.
Condition	Ge (const Expression lhs, const Expression rhs)
	Greater-than-or-equal comparison.
Expression	expand (const Expression expr)
	Expands an expression algebraically.
Expression	factor (const Expression expr)
	Factors an expression into a product of simpler terms.
Expression	simplify (const Expression expr)
	Simplifies an expression.
Expression	overapproximate (const Expression expr)
	Overapproximates an expression by resolving min/max to upper bounds.
bool	eq (const Expression lhs, const Expression rhs)
	Tests structural equality of two expressions.
bool	null_safe_eq (const Expression lhs, const Expression rhs)
	Tests equality of expressions with null-safety.
bool	uses (const Expression expr, const Symbol sym)
	Tests if an expression uses a specific symbol.
bool	uses (const Expression expr, const std::string &name)
	Tests if an expression uses a symbol with a specific name.
SymbolSet	atoms (const Expression expr)
	Extracts all symbols (atoms) from an expression.
template<typename T>
bool	has (const Expression expr)
	Checks if an expression contains a specific SymEngine type.
template<typename T>
ExpressionSet	find (const Expression expr)
	Finds all instances of a specific SymEngine type in an expression.
bool	has_dynamic_sizeof (const Expression expr)
	Checks if an expression contains a dynamic_sizeof operation.
ExpressionSet	muls (const Expression expr)
	Extracts all multiplication operations from an expression.
Expression	subs (const Expression expr, const Expression old_expr, const Expression new_expr)
	Substitutes a sub-expression with another expression.
Expression	subs (const Expression expr, const symbolic::ExpressionMapping &replacements)
	Bulk replacement.
Condition	subs (const Condition expr, const Expression old_expr, const Expression new_expr)
	Substitutes a sub-expression in a condition.
Condition	subs (const Condition expr, const symbolic::ExpressionMapping &replacements)
	Bulk replacement.
bool	substitute (ExpressionSet &set, const symbolic::ExpressionMapping &replacements)
MultiExpression	substitute (const MultiExpression &vec, const symbolic::ExpressionMapping &replacements)
Expression	inverse (const Expression expr, const Symbol symbol)
	Computes the inverse of an expression with respect to a symbol.
Symbol	threadIdx_x ()
	Thread index in X dimension.
Symbol	threadIdx_y ()
	Thread index in Y dimension.
Symbol	threadIdx_z ()
	Thread index in Z dimension.
Symbol	blockDim_x ()
	Block dimension (threads per block) in X.
Symbol	blockDim_y ()
	Block dimension (threads per block) in Y.
Symbol	blockDim_z ()
	Block dimension (threads per block) in Z.
Symbol	blockIdx_x ()
	Block index in X dimension.
Symbol	blockIdx_y ()
	Block index in Y dimension.
Symbol	blockIdx_z ()
	Block index in Z dimension.
Symbol	gridDim_x ()
	Grid dimension (blocks per grid) in X.
Symbol	gridDim_y ()
	Grid dimension (blocks per grid) in Y.
Symbol	gridDim_z ()
	Grid dimension (blocks per grid) in Z.
Expression	parse (const std::string &expr_str)
	Parses a string into a symbolic expression.
std::string	expression_to_map_str (const MultiExpression &expr, const Assumptions &assums)
	Converts a multi-dimensional expression to an ISL map string.
std::tuple< std::string, std::string, std::string >	expressions_to_intersection_map_str (const MultiExpression &expr1, const MultiExpression &expr2, const Symbol indvar, const Assumptions &assums1, const Assumptions &assums2)
	Converts two expressions to ISL format for intersection analysis.
bool	expressions_to_intersection_maps (isl_ctx *ctx, const MultiExpression &expr1, const MultiExpression &expr2, const Symbol indvar, const Assumptions &assums1, const Assumptions &assums2, isl_map **map_1, isl_map **map_2, isl_map **map_3)
	Builds the three maps of expressions_to_intersection_map_str directly in ctx, without parsing.
isl_map *	expression_to_may_map (isl_ctx *ctx, const MultiExpression &expr, const Assumptions &assums)
	Builds the map of expression_to_map_str directly in ctx, possibly over-approximating its domain like expressions_to_intersection_maps (may-queries only).
std::optional< bool >	decide_nonneg (const Expression &expr, const Assumptions &assums, bool strict)
	Decides expr >= 0 (> 0 if strict) under the bounds and constraints of assums with isl.
ExpressionSet	generate_constraints (SymbolSet &syms, const Assumptions &assums, SymbolSet &seen)
	Generates constraint expressions from assumptions.
std::string	constraint_to_isl_str (const Expression con)
	Converts a constraint expression to ISL string format.
std::string	expression_to_isl_str (const Expression expr)
	Converts an index or bound expression to ISL syntax.
void	canonicalize_map_dims (isl_map *map, const std::string &in_prefix, const std::string &out_prefix)
	Canonicalizes dimension names in an ISL map.
bool	vectors_of_expressions_match (const std::vector< Expression > &a, const std::vector< Expression > &b)
bool	vectors_of_expressions_match (const std::vector< Expression > &a, const std::vector< Expression > &b, const ExpressionMapping &replacements)
	Applies replacement mappings to a before checking.

Variables
constexpr int64_t	DEFAULT_BOUND_BUDGET = 50000
constexpr int64_t	DELINEARIZATION_PROOF_BUDGET = 5000
constexpr OptionKey< int64_t >	BOUND_BUDGET {"symbolic.bound_budget"}

Typedef Documentation

AffineCoeffs

typedef std::unordered_map<Symbol, Expression, SymEngine::RCPBasicHash, SymEngine::RCPBasicKeyEq> sdfg::symbolic::AffineCoeffs

Map from symbols to their coefficients in an affine expression.

CNF

typedef std::vector<std::vector<Condition> > sdfg::symbolic::CNF

Conjunctive Normal Form representation.

A CNF is represented as a vector of clauses, where each clause is a vector of conditions (literals). The overall expression is the AND of all clauses, and each clause is the OR of its literals.

Example: [[A, B], [C, D], [E]] represents (A OR B) AND (C OR D) AND E

Polynomial

typedef SymEngine::RCP<const SymEngine::MExprPoly> sdfg::symbolic::Polynomial

Type representing a SymEngine polynomial expression.

Function Documentation

affine_coefficients()

AffineCoeffs sdfg::symbolic::affine_coefficients

(

Polynomial

poly

)

Converts a Polynomial of degree 1 to coefficient map.

Parameters

poly	The Polynomial to convert (must be degree 1)

Returns

A AffineCoeffs map where keys are the polynomial's variables and values are their coefficients, plus a __daisy_constant__ entry for the constant term.

Extracts the coefficients from a degree-1 (affine) polynomial. For an expression like 2*i + 3*j + 5, this returns a map with entries {i: 2, j: 3, __daisy_constant__: 5}. The variable -> exponent-index mapping is recovered from the polynomial itself, so the result is independent of the order in which variables were originally passed to polynomial().

SymbolVec symbols = {i, j};
auto poly = polynomial(expr, symbols);
auto coeffs = affine_coefficients(poly);
// Access individual coefficients: coeffs[i] gives 2

affine_decomposition()

AffineDecomposition sdfg::symbolic::affine_decomposition	(	const Expression &	expr,
		const Symbol &	symbol )

Decomposes an expression into affine form w.r.t.

a single symbol

Parameters

expr	The expression to decompose
symbol	The symbol to decompose with respect to

Returns

AffineDecomposition containing coefficient and offset, or failure

Given an expression, checks if it is affine (degree <= 1) in the given symbol. If so, returns the coefficient and offset such that expr = coeff * symbol + offset.

auto result = affine_decomposition(parse("-2 + _s0"), symbol("_s0"));
// result.success = true, result.coeff = 1, result.offset = -2
 
auto result2 = affine_decomposition(parse("_s0 * _s0"), symbol("_s0"));
// result2.success = false (quadratic, not affine)

affine_inverse()

Expression sdfg::symbolic::affine_inverse	(	AffineCoeffs	coeffs,
		Symbol	symbol )

Computes the inverse function for an affine expression.

Parameters

coeffs	Coefficient map from affine_coefficients()
symbol	The symbol to solve for

Returns

Expression representing the inverse function

Given an affine expression y = a*x + b (represented as coefficients), computes the inverse x = (y - b) / a.

// If we have y = 2*i + 5, compute i in terms of y
auto inv = affine_inverse(coeffs, i);  // Returns (y - 5) / 2

canonicalize_map_dims()

void sdfg::symbolic::canonicalize_map_dims	(	isl_map *	map,
		const std::string &	in_prefix,
		const std::string &	out_prefix )

Canonicalizes dimension names in an ISL map.

Parameters

map	ISL map to modify
in_prefix	Prefix for input dimensions (e.g., "i")
out_prefix	Prefix for output dimensions (e.g., "o")

Renames the dimensions of an ISL map to use canonical names with specified prefixes. This ensures consistent naming across different maps for easier composition and comparison.

conjunctive_normal_form()

CNF sdfg::symbolic::conjunctive_normal_form

(

const Condition

cond

)

Convert a condition to conjunctive normal form.

Parameters

cond	The condition to convert

Returns

The conjunctive normal form of the condition

Exceptions

CNFException

if the condition cannot be converted to CNF

Converts a boolean condition into CNF by applying logical equivalences and distribution laws. The result is a standardized form that can be used for further analysis or optimization.

// Convert (A AND B) OR C to CNF
auto cnf = conjunctive_normal_form(condition);
// Result: (A OR C) AND (B OR C)

constraint_to_isl_str()

std::string sdfg::symbolic::constraint_to_isl_str

(

const Expression

con

)

Converts a constraint expression to ISL string format.

Parameters

con	Constraint expression (typically a comparison)

Returns

ISL-formatted string for the constraint

Converts individual constraint expressions (like "i >= 0" or "i < N") to ISL's string representation.

decide_nonneg()

std::optional< bool > sdfg::symbolic::decide_nonneg	(	const Expression &	expr,
		const Assumptions &	assums,
		bool	strict )

Decides expr >= 0 (> 0 if strict) under the bounds and constraints of assums with isl.

Returns nullopt if expr is not quasi-affine or a violation may stem from an over-approximation.

delinearize() [1/2]

DelinearizeResult sdfg::symbolic::delinearize	(	const Expression &	expr,
		AssumptionsBounds &	bounds )

Same as delinearize, but reuses a caller-supplied AssumptionsBounds.

Construct one AssumptionsBounds per scope (per Assumptions reference) and pass it through repeated delinearize calls so the internal BoundAnalysis memoization amortizes across all of them.

delinearize() [2/2]

DelinearizeResult sdfg::symbolic::delinearize	(	const Expression &	expr,
		const Assumptions &	assums )

Delinearizes a linearized expression into indices and dimensions based on parameter assumptions.

Parameters

expr	Linearized expression potentially containing linearized indices
assums	Assumptions about parameters

Returns

Delinearized result containing indices, dimensions, and success flag

Attempts to recover multi-dimensional structure from a linearized expression. For example, if an expression represents a linearized 2D array access A[i*N + j], this function tries to recover the 2D indices [i, j].

The delinearization technique is based on the algorithm described in: "Optimistic Delinearization of Parametrically Sized Arrays" https://dl.acm.org/doi/10.1145/2751205.2751248

expression_to_isl_str()

std::string sdfg::symbolic::expression_to_isl_str

(

const Expression

expr

)

Converts an index or bound expression to ISL syntax.

Integer divisions and remainders by literals (idiv, imod), min and max become quasi-affine ISL expressions; anything ISL cannot represent prints as-is and fails to parse.

expression_to_map_str()

std::string sdfg::symbolic::expression_to_map_str	(	const MultiExpression &	expr,
		const Assumptions &	assums )

Converts a multi-dimensional expression to an ISL map string.

Parameters

expr	Multi-dimensional expression representing iteration or access space
assums	Assumptions about symbol bounds

Returns

ISL-formatted string representing the expression as a map

Converts symbolic expressions to ISL's string format for use with ISL library functions. The resulting string includes constraints from assumptions.

expression_to_may_map()

isl_map * sdfg::symbolic::expression_to_may_map	(	isl_ctx *	ctx,
		const MultiExpression &	expr,
		const Assumptions &	assums )

Builds the map of expression_to_map_str directly in ctx, possibly over-approximating its domain like expressions_to_intersection_maps (may-queries only).

Returns null if unsupported.

expressions_to_intersection_map_str()

std::tuple< std::string, std::string, std::string > sdfg::symbolic::expressions_to_intersection_map_str	(	const MultiExpression &	expr1,
		const MultiExpression &	expr2,
		const Symbol	indvar,
		const Assumptions &	assums1,
		const Assumptions &	assums2 )

Converts two expressions to ISL format for intersection analysis.

Parameters

expr1	First multi-dimensional expression
expr2	Second multi-dimensional expression
indvar	Induction variable for the iteration space
assums1	Assumptions for first expression
assums2	Assumptions for second expression

Returns

Tuple of (map1_str, map2_str, combined_constraints_str) in ISL format

Prepares two expressions and their assumptions for intersection checking using ISL. Returns formatted strings that can be parsed by ISL to construct maps and perform set operations.

expressions_to_intersection_maps()

bool sdfg::symbolic::expressions_to_intersection_maps	(	isl_ctx *	ctx,
		const MultiExpression &	expr1,
		const MultiExpression &	expr2,
		const Symbol	indvar,
		const Assumptions &	assums1,
		const Assumptions &	assums2,
		isl_map **	map_1,
		isl_map **	map_2,
		isl_map **	map_3 )

Builds the three maps of expressions_to_intersection_map_str directly in ctx, without parsing.

The domains may over-approximate the parsed ones: inequalities that stay piecewise (e.g. C division by a numerator of unknown sign) are dropped, so the maps are only valid for may-queries (dependences, disjointness). Returns false (with null maps) for inputs the direct construction does not support (non-affine terms, unknown functions, name clashes); map_3 may be null.

generate_constraints()

ExpressionSet sdfg::symbolic::generate_constraints	(	SymbolSet &	syms,
		const Assumptions &	assums,
		SymbolSet &	seen )

Generates constraint expressions from assumptions.

Parameters

syms	Set of symbols to generate constraints for
assums	Assumptions containing bounds information
seen	Set of symbols already processed (to avoid duplicates)

Returns

Set of constraint expressions derived from assumptions

Extracts bound constraints from assumptions and converts them to constraint expressions suitable for ISL. This includes lower bounds (sym >= lb) and upper bounds (sym <= ub) for all symbols.

is_disjoint() [1/2]

bool sdfg::symbolic::is_disjoint	(	const MultiExpression &	expr1,
		const MultiExpression &	expr2,
		AssumptionsBounds &	bounds1,
		AssumptionsBounds &	bounds2 )

Same as is_disjoint, but reuses caller-supplied AssumptionsBounds.

is_disjoint() [2/2]

bool sdfg::symbolic::is_disjoint	(	const MultiExpression &	expr1,
		const MultiExpression &	expr2,
		const Assumptions &	assums1,
		const Assumptions &	assums2 )

Interprets the expressions as integer sets and checks if expr1 is disjoint from expr2.

Parameters

expr1	The first expression to check.
expr2	The second expression to check.
assums1	The assumptions for the first expression.
assums2	The assumptions for the second expression.

Returns

true if expr1 is disjoint from expr2, false otherwise.

is_eq() [1/2]

bool sdfg::symbolic::is_eq	(	const Expression &	a,
		const Expression &	b,
		BoundAnalysis &	ba )

Prove a == b using a pre-built BoundAnalysis.

is_eq() [2/2]

bool sdfg::symbolic::is_eq	(	const Expression &	a,
		const Expression &	b,
		const SymbolSet &	parameters,
		const Assumptions &	assumptions,
		bool	tight = false )

Prove a == b (both a >= b and a <= b).

is_ge() [1/2]

bool sdfg::symbolic::is_ge	(	const Expression &	a,
		const Expression &	b,
		BoundAnalysis &	ba )

Prove a >= b using a pre-built BoundAnalysis.

is_ge() [2/2]

bool sdfg::symbolic::is_ge	(	const Expression &	a,
		const Expression &	b,
		const SymbolSet &	parameters,
		const Assumptions &	assumptions,
		bool	tight = false )

Prove a >= b.

is_gt() [1/2]

bool sdfg::symbolic::is_gt	(	const Expression &	a,
		const Expression &	b,
		BoundAnalysis &	ba )

Prove a > b using a pre-built BoundAnalysis.

is_gt() [2/2]

bool sdfg::symbolic::is_gt	(	const Expression &	a,
		const Expression &	b,
		const SymbolSet &	parameters,
		const Assumptions &	assumptions,
		bool	tight = false )

Prove a > b.

is_integer_affine()

bool sdfg::symbolic::is_integer_affine

(

const Expression &

expr

)

Whether expr is affine in all of its symbols with integer coefficients, e.g.

2*i - j + 3 (but not N*i, idiv(i, 2) or i/2).

is_le() [1/2]

bool sdfg::symbolic::is_le	(	const Expression &	a,
		const Expression &	b,
		BoundAnalysis &	ba )

Prove a <= b using a pre-built BoundAnalysis.

is_le() [2/2]

bool sdfg::symbolic::is_le	(	const Expression &	a,
		const Expression &	b,
		const SymbolSet &	parameters,
		const Assumptions &	assumptions,
		bool	tight = false )

Prove a <= b.

is_lt() [1/2]

bool sdfg::symbolic::is_lt	(	const Expression &	a,
		const Expression &	b,
		BoundAnalysis &	ba )

Prove a < b using a pre-built BoundAnalysis.

is_lt() [2/2]

bool sdfg::symbolic::is_lt	(	const Expression &	a,
		const Expression &	b,
		const SymbolSet &	parameters,
		const Assumptions &	assumptions,
		bool	tight = false )

Prove a < b.

is_negative() [1/2]

bool sdfg::symbolic::is_negative	(	const Expression &	expr,
		BoundAnalysis &	ba )

Prove expr < 0 using a pre-built BoundAnalysis.

is_negative() [2/2]

bool sdfg::symbolic::is_negative	(	const Expression &	expr,
		const SymbolSet &	parameters,
		const Assumptions &	assumptions,
		bool	tight = false )

Prove expr < 0.

is_nonneg() [1/2]

bool sdfg::symbolic::is_nonneg	(	const Expression &	expr,
		BoundAnalysis &	ba )

Prove expr >= 0 using a pre-built BoundAnalysis.

is_nonneg() [2/2]

bool sdfg::symbolic::is_nonneg	(	const Expression &	expr,
		const SymbolSet &	parameters,
		const Assumptions &	assumptions,
		bool	tight = false )

Prove expr >= 0.

is_nonpos() [1/2]

bool sdfg::symbolic::is_nonpos	(	const Expression &	expr,
		BoundAnalysis &	ba )

Prove expr <= 0 using a pre-built BoundAnalysis.

is_nonpos() [2/2]

bool sdfg::symbolic::is_nonpos	(	const Expression &	expr,
		const SymbolSet &	parameters,
		const Assumptions &	assumptions,
		bool	tight = false )

Prove expr <= 0.

is_positive() [1/2]

bool sdfg::symbolic::is_positive	(	const Expression &	expr,
		BoundAnalysis &	ba )

Prove expr > 0 using a pre-built BoundAnalysis.

is_positive() [2/2]

bool sdfg::symbolic::is_positive	(	const Expression &	expr,
		const SymbolSet &	parameters,
		const Assumptions &	assumptions,
		bool	tight = false )

Prove expr > 0.

is_subset() [1/2]

bool sdfg::symbolic::is_subset	(	const MultiExpression &	expr1,
		const MultiExpression &	expr2,
		AssumptionsBounds &	bounds1,
		AssumptionsBounds &	bounds2 )

Same as is_subset, but reuses caller-supplied AssumptionsBounds.

Constructing one AssumptionsBounds per scope and threading it through many subset queries amortizes the internal delinearize bound-analysis cache across all of them.

is_subset() [2/2]

bool sdfg::symbolic::is_subset	(	const MultiExpression &	expr1,
		const MultiExpression &	expr2,
		const Assumptions &	assums1,
		const Assumptions &	assums2 )

Interprets the expressions as integer sets and checks if expr1 is a subset of expr2.

Parameters

expr1	The first expression to check.
expr2	The second expression to check.
assums1	The assumptions for the first expression.
assums2	The assumptions for the second expression.

Returns

true if expr1 is a subset of expr2, false otherwise.

is_tautology()

bool sdfg::symbolic::is_tautology

(

const std::vector< symbolic::Condition > &

clause

)

Check if a disjunctive clause is a tautology.

Parameters

clause

The clause to check, represented as a vector of conditions (literals)

Returns

true if the clause is a tautology, false otherwise

maximum()

Expression sdfg::symbolic::maximum	(	const Expression	expr,
		const SymbolSet &	parameters,
		const Assumptions &	assumptions,
		bool	tight )

Compute the maximum of an expression.

Parameters

expr	The expression to compute the maximum of
parameters	Symbols treated as free parameters in the result
assumptions	Bounds information for symbols
tight	If true, use tight (exact) bounds; if false, use loose (conservative) bounds

Returns

The maximum of the expression, or null if unbounded

minimum()

Expression sdfg::symbolic::minimum	(	const Expression	expr,
		const SymbolSet &	parameters,
		const Assumptions &	assumptions,
		bool	tight )

Compute the minimum of an expression.

Parameters

expr	The expression to compute the minimum of
parameters	Symbols treated as free parameters in the result
assumptions	Bounds information for symbols
tight	If true, use tight (exact) bounds; if false, use loose (conservative) bounds

Returns

The minimum of the expression, or null if unbounded

polynomial()

Polynomial sdfg::symbolic::polynomial	(	const Expression	expr,
		SymbolVec &	symbols )

Converts an Expression to a Polynomial.

Parameters

expr	The Expression to convert
symbols	A vector of symbols that will be used in the polynomial

Returns

A Polynomial representation of the Expression

Converts a symbolic expression into SymEngine's polynomial representation, which allows for efficient polynomial operations and coefficient extraction. The symbols vector specifies which symbols should be treated as polynomial variables.

polynomial_div()

std::pair< Expression, Expression > sdfg::symbolic::polynomial_div	(	const Expression &	dividend,
		const Expression &	divisor )

Performs polynomial division.

Parameters

dividend	The polynomial to divide
divisor	The polynomial to divide by

Returns

Pair of (quotient, remainder) expressions

Performs polynomial division and returns both the quotient and remainder. For polynomials p(x) and q(x), computes p(x) = q(x)*quotient + remainder.

auto dividend = parse("x*x + 3*x + 2");  // x^2 + 3x + 2
auto divisor = parse("x + 1");            // x + 1
auto [quot, rem] = polynomial_div(dividend, divisor);
// quot = x + 2, rem = 0

solve_affine_bound()

Expression sdfg::symbolic::solve_affine_bound	(	const Expression &	expr,
		const Symbol &	symbol,
		const Expression &	bound_value,
		bool	is_lower_bound )

Solves for a symbol's bound given an inequality constraint.

Parameters

expr	Expression containing the symbol
symbol	The symbol to solve for
bound_value	The value that expr must be >= (for lower) or <= (for upper)
is_lower_bound	True if solving expr >= bound_value, false for expr <= bound_value

Returns

The bound on the symbol, or null if cannot be solved

Given an affine expression expr = coeff * symbol + offset and a constraint:

• For lower bound (expr >= bound_value): symbol >= (bound_value - offset) / coeff (if coeff > 0)
• For upper bound (expr <= bound_value): symbol <= (bound_value - offset) / coeff (if coeff > 0)

Only works when coeff is a positive integer.

// For loop bound: -2 + _s0 >= 1 (loop must execute at least once)
auto bound = solve_affine_bound(parse("-2 + _s0"), symbol("_s0"), integer(1), true);
// Returns 3 (_s0 >= 3)

substitute()

bool sdfg::symbolic::substitute	(	Assumptions &	assumptions,
		const symbolic::ExpressionMapping &	replacements )

vectors_of_expressions_match() [1/2]

bool sdfg::symbolic::vectors_of_expressions_match	(	const std::vector< Expression > &	a,
		const std::vector< Expression > &	b )

vectors_of_expressions_match() [2/2]

bool sdfg::symbolic::vectors_of_expressions_match	(	const std::vector< Expression > &	a,
		const std::vector< Expression > &	b,
		const ExpressionMapping &	replacements )

Applies replacement mappings to a before checking.

Parameters

replacements

mapping from symbols inside a to the symbols used by b

Returns

Variable Documentation

BOUND_BUDGET

OptionKey<int64_t> sdfg::symbolic::BOUND_BUDGET {"symbolic.bound_budget"}

inlineconstexpr

DEFAULT_BOUND_BUDGET

int64_t sdfg::symbolic::DEFAULT_BOUND_BUDGET = 50000

inlineconstexpr

DELINEARIZATION_PROOF_BUDGET

int64_t sdfg::symbolic::DELINEARIZATION_PROOF_BUDGET = 5000

inlineconstexpr