assumptions.h File Reference

Symbol assumptions for reasoning about bounds, constness, and evolution. More...

#include <cstddef>
#include <initializer_list>
#include <iterator>
#include <memory>
#include <stdexcept>
#include <unordered_map>
#include <utility>
#include "sdfg/symbolic/symbolic.h"
#include "sdfg/types/type.h"

Go to the source code of this file.

Classes
class	sdfg::symbolic::Assumption
	Represents assumptions about a symbol's properties and behavior. More...
class	sdfg::symbolic::Assumptions
	Map from symbols to their assumptions. More...
class	sdfg::symbolic::Assumptions::const_iterator
	Visits the own entries, then the base's entries the own ones do not shadow. More...

Namespaces
namespace	sdfg
namespace	sdfg::symbolic

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

Detailed Description

Symbol assumptions for reasoning about bounds, constness, and evolution.

Assumptions are a critical component of the symbolic system that enable reasoning about ranges of symbols, how they evolve, and whether they are constant. Examples:

• Ranges of memory accesses
• Ranges and evolution of loop iteration variables

Assumption System

Each symbol can have associated assumptions that describe its properties:

• Bounds: Lower and upper bounds that constrain the symbol's possible values
• Tight bounds: Exact minimum and maximum values the symbol can take
• Constness: Whether the symbol's value remains constant
• Map: How the symbol evolves (e.g., in loop iterations)

Example Usage

// Create a symbol with type-based assumptions
auto i = symbolic::symbol("i");
auto int32_type = types::Scalar::create(types::PrimitiveType::Int32);
auto assumption = Assumption::create(i, int32_type);
 
// Add loop bounds (e.g., 0 <= i < 10)
assumption.add_lower_bound(symbolic::zero());
assumption.add_upper_bound(symbolic::integer(10));
 
// Mark as non-constant (evolves in loop)
assumption.constant(false);
 
// Set evolution map (e.g., i' = i + 1)
assumption.map(symbolic::add(i, symbolic::one()));

See also

extreme_values.h for computing bounds of expressions using assumptions

sets.h for integer set operations using assumptions