sdfg::symbolic::Assumption Class Reference

Represents assumptions about a symbol's properties and behavior. More...

#include <sdfg/symbolic/assumptions.h>

Public Types
enum class	ReplaceResult { IdSame = 0 , IdChanged }

Public Member Functions
	Assumption ()
	Default constructor creating an empty assumption.
	Assumption (const Symbol symbol)
	Constructs an assumption for a specific symbol.
	Assumption (const Assumption &a)
	Copy constructor.
Assumption &	operator= (const Assumption &a)
	Assignment operator.
const Symbol	symbol () const
	Gets the symbol this assumption is for.
const ExpressionSet &	lower_bounds () const
	Gets all lower bound constraints.
void	add_lower_bound (const Expression lb)
	Adds a lower bound constraint.
bool	contains_lower_bound (const Expression lb)
	Checks if a specific lower bound exists.
bool	remove_lower_bound (const Expression lb)
	Removes a lower bound constraint.
const ExpressionSet &	upper_bounds () const
	Gets all upper bound constraints.
void	add_upper_bound (const Expression ub)
	Adds an upper bound constraint.
bool	contains_upper_bound (const Expression ub)
	Checks if a specific upper bound exists.
bool	remove_upper_bound (const Expression ub)
	Removes an upper bound constraint.
const Expression	tight_lower_bound () const
	Gets the tight lower bound.
void	tight_lower_bound (const Expression tight_lb)
	Sets the tight lower bound.
const Expression	tight_upper_bound () const
	Gets the tight upper bound.
void	tight_upper_bound (const Expression tight_ub)
	Sets the tight upper bound.
const ExpressionSet &	constraints () const
	Gets the constraints registered on this symbol.
void	add_constraint (const Expression c)
	Adds a constraint involving this symbol.
bool	contains_constraint (const Expression c)
	Checks if a specific constraint is present.
bool	remove_constraint (const Expression c)
	Removes a constraint.
bool	constant () const
	Checks if the symbol is constant.
void	constant (bool constant)
	Sets whether the symbol is constant.
const Expression	map () const
	Gets the evolution map for this symbol.
void	map (const Expression map)
	Sets the evolution map for this symbol.
ReplaceResult	replace (const symbolic::ExpressionMapping &replacements)

Static Public Member Functions
static Assumption	create (const Symbol symbol, const types::IType &type)
	Creates an assumption with bounds derived from a type.

Detailed Description

Represents assumptions about a symbol's properties and behavior.

Member Enumeration Documentation

ReplaceResult

enum class sdfg::symbolic::Assumption::ReplaceResult

strong

Enumerator
IdSame
IdChanged

Constructor & Destructor Documentation

Assumption() [1/3]

sdfg::symbolic::Assumption::Assumption

(

)

Default constructor creating an empty assumption.

Assumption() [2/3]

sdfg::symbolic::Assumption::Assumption

(

const Symbol

symbol

)

Constructs an assumption for a specific symbol.

Parameters

symbol

The symbol this assumption is for

Assumption() [3/3]

sdfg::symbolic::Assumption::Assumption

(

const Assumption &

a

)

Copy constructor.

Parameters

a	Assumption to copy

Member Function Documentation

add_constraint()

void sdfg::symbolic::Assumption::add_constraint

(

const Expression

c

)

Adds a constraint involving this symbol.

Parameters

c	Expression with implicit <= 0 semantics

The expression must mention this symbol (otherwise it does not constrain it) and should be affine in every non-constant symbol it mentions, so that downstream consumers can project it onto a single variable when needed.

add_lower_bound()

void sdfg::symbolic::Assumption::add_lower_bound

(

const Expression

lb

)

Adds a lower bound constraint.

Parameters

lb	The lower bound expression to add

The symbol is constrained to be greater than or equal to this expression. Multiple lower bounds can be added; the effective bound is their maximum.

add_upper_bound()

void sdfg::symbolic::Assumption::add_upper_bound

(

const Expression

ub

)

Adds an upper bound constraint.

Parameters

ub	The upper bound expression to add

The symbol is constrained to be less than or equal to this expression. Multiple upper bounds can be added; the effective bound is their minimum.

constant() [1/2]

bool sdfg::symbolic::Assumption::constant

(

)

const

Checks if the symbol is constant.

Returns

true if the symbol's value does not change

A constant symbol has the same value throughout its scope. Non-constant symbols may evolve (e.g., loop iteration variables).

constant() [2/2]

void sdfg::symbolic::Assumption::constant

(

bool

constant

)

Sets whether the symbol is constant.

Parameters

constant

true if the symbol is constant, false if it evolves

constraints()

const ExpressionSet & sdfg::symbolic::Assumption::constraints

(

)

const

Gets the constraints registered on this symbol.

Returns

Set of constraint expressions, each with implicit <= 0 semantics

A constraint is an affine expression involving this symbol together with other symbols (e.g. i + j - 15 to express i + j <= 15). The same constraint expression is registered under each non-constant symbol it mentions, so consumers holding any one of those symbols can find the coupling fact via constraints().

Equality a = b is represented as two constraints: a - b and b - a.

contains_constraint()

bool sdfg::symbolic::Assumption::contains_constraint

(

const Expression

c

)

Checks if a specific constraint is present.

contains_lower_bound()

bool sdfg::symbolic::Assumption::contains_lower_bound

(

const Expression

lb

)

Checks if a specific lower bound exists.

Parameters

lb	The lower bound expression to check

Returns

true if this lower bound is present

contains_upper_bound()

bool sdfg::symbolic::Assumption::contains_upper_bound

(

const Expression

ub

)

Checks if a specific upper bound exists.

Parameters

ub	The upper bound expression to check

Returns

true if this upper bound is present

create()

Assumption sdfg::symbolic::Assumption::create ( const Symbol symbol, const types::IType & type )

static

Creates an assumption with bounds derived from a type.

Parameters

symbol	The symbol to create assumption for
type	The type to derive bounds from

Returns

Assumption with bounds matching the type's range

Creates an assumption initialized with bounds appropriate for the given type. For example, an Int32 type would set bounds to [-2^31, 2^31-1].

auto i = symbolic::symbol("i");
auto int32_type = types::Scalar::create(types::PrimitiveType::Int32);
auto assumption = Assumption::create(i, int32_type);

lower_bounds()

const ExpressionSet & sdfg::symbolic::Assumption::lower_bounds

(

)

const

Gets all lower bound constraints.

Returns

Set of all lower bound expressions

A symbol may have multiple lower bound constraints (e.g., from different analysis passes). The effective lower bound is the maximum of these.

map() [1/2]

const Expression sdfg::symbolic::Assumption::map

(

)

const

Gets the evolution map for this symbol.

Returns

Expression describing how the symbol evolves, or null if none

The map describes how the symbol's value changes, typically in loop iterations. For example, a loop counter might have map(i) = i + 1, indicating it increments by 1 each iteration.

map() [2/2]

void sdfg::symbolic::Assumption::map

(

const Expression

map

)

Sets the evolution map for this symbol.

Parameters

map	Expression describing how the symbol evolves

Sets how the symbol evolves over time or iterations. This is used to track induction variables in loops and analyze their behavior.

operator=()

Assumption & sdfg::symbolic::Assumption::operator=

(

const Assumption &

a

)

Assignment operator.

Parameters

a	Assumption to assign from

Returns

Reference to this assumption

remove_constraint()

bool sdfg::symbolic::Assumption::remove_constraint

(

const Expression

c

)

Removes a constraint.

Returns

true if the constraint was found and removed

remove_lower_bound()

bool sdfg::symbolic::Assumption::remove_lower_bound

(

const Expression

lb

)

Removes a lower bound constraint.

Parameters

lb	The lower bound expression to remove

Returns

true if the bound was found and removed

remove_upper_bound()

bool sdfg::symbolic::Assumption::remove_upper_bound

(

const Expression

ub

)

Removes an upper bound constraint.

Parameters

ub	The upper bound expression to remove

Returns

true if the bound was found and removed

replace()

ReplaceResult sdfg::symbolic::Assumption::replace

(

const symbolic::ExpressionMapping &

replacements

)

symbol()

const Symbol sdfg::symbolic::Assumption::symbol

(

)

const

Gets the symbol this assumption is for.

Returns

The symbol

tight_lower_bound() [1/2]

const Expression sdfg::symbolic::Assumption::tight_lower_bound

(

)

const

Gets the tight lower bound.

Returns

The exact minimum value the symbol can take, or null if unknown

Unlike lower_bounds which are constraints, the tight lower bound represents the exact minimum value the symbol will take during execution.

tight_lower_bound() [2/2]

void sdfg::symbolic::Assumption::tight_lower_bound

(

const Expression

tight_lb

)

Sets the tight lower bound.

Parameters

tight_lb

The exact minimum value

Sets the exact minimum value the symbol will take. This is more precise than lower bound constraints.

tight_upper_bound() [1/2]

const Expression sdfg::symbolic::Assumption::tight_upper_bound

(

)

const

Gets the tight upper bound.

Returns

The exact maximum value the symbol can take, or null if unknown

Unlike upper_bounds which are constraints, the tight upper bound represents the exact maximum value the symbol will take during execution.

tight_upper_bound() [2/2]

void sdfg::symbolic::Assumption::tight_upper_bound

(

const Expression

tight_ub

)

Sets the tight upper bound.

Parameters

tight_ub

The exact maximum value

Sets the exact maximum value the symbol will take. This is more precise than upper bound constraints.

upper_bounds()

const ExpressionSet & sdfg::symbolic::Assumption::upper_bounds

(

)

const

Gets all upper bound constraints.

Returns

Set of all upper bound expressions

A symbol may have multiple upper bound constraints (e.g., from different analysis passes). The effective upper bound is the minimum of these.

---

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

• sdfg/include/sdfg/symbolic/assumptions.h