extreme_values.h File Reference

Computing bounds of symbolic expressions using assumptions. More...

#include "sdfg/options.h"
#include "sdfg/symbolic/assumptions.h"
#include "sdfg/symbolic/polynomials.h"
#include "sdfg/symbolic/symbolic.h"
#include <memory>
#include <string>
#include <unordered_map>

Go to the source code of this file.

Classes
struct	sdfg::symbolic::Interval
	Result of bounding an expression: an interval [lower, upper]. More...
class	sdfg::symbolic::BoundAnalysis
	Computes bounds of symbolic expressions using assumptions. More...
class	sdfg::symbolic::AssumptionsBounds
	Bundles Assumptions with both the loose and tight BoundAnalysis derived from them. More...

Namespaces
namespace	sdfg
namespace	sdfg::symbolic

Functions
Expression	sdfg::symbolic::minimum (const Expression expr, const SymbolSet &parameters, const Assumptions &assumptions, bool tight)
	Compute the minimum of an expression.
Expression	sdfg::symbolic::maximum (const Expression expr, const SymbolSet &parameters, const Assumptions &assumptions, bool tight)
	Compute the maximum of an expression.
bool	sdfg::symbolic::is_nonneg (const Expression &expr, const SymbolSet &parameters, const Assumptions &assumptions, bool tight=false)
	Prove expr >= 0.
bool	sdfg::symbolic::is_positive (const Expression &expr, const SymbolSet &parameters, const Assumptions &assumptions, bool tight=false)
	Prove expr > 0.
bool	sdfg::symbolic::is_nonpos (const Expression &expr, const SymbolSet &parameters, const Assumptions &assumptions, bool tight=false)
	Prove expr <= 0.
bool	sdfg::symbolic::is_negative (const Expression &expr, const SymbolSet &parameters, const Assumptions &assumptions, bool tight=false)
	Prove expr < 0.
bool	sdfg::symbolic::is_ge (const Expression &a, const Expression &b, const SymbolSet &parameters, const Assumptions &assumptions, bool tight=false)
	Prove a >= b.
bool	sdfg::symbolic::is_gt (const Expression &a, const Expression &b, const SymbolSet &parameters, const Assumptions &assumptions, bool tight=false)
	Prove a > b.
bool	sdfg::symbolic::is_le (const Expression &a, const Expression &b, const SymbolSet &parameters, const Assumptions &assumptions, bool tight=false)
	Prove a <= b.
bool	sdfg::symbolic::is_lt (const Expression &a, const Expression &b, const SymbolSet &parameters, const Assumptions &assumptions, bool tight=false)
	Prove a < b.
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).
bool	sdfg::symbolic::is_nonneg (const Expression &expr, BoundAnalysis &ba)
	Prove expr >= 0 using a pre-built BoundAnalysis.
bool	sdfg::symbolic::is_positive (const Expression &expr, BoundAnalysis &ba)
	Prove expr > 0 using a pre-built BoundAnalysis.
bool	sdfg::symbolic::is_nonpos (const Expression &expr, BoundAnalysis &ba)
	Prove expr <= 0 using a pre-built BoundAnalysis.
bool	sdfg::symbolic::is_negative (const Expression &expr, BoundAnalysis &ba)
	Prove expr < 0 using a pre-built BoundAnalysis.
bool	sdfg::symbolic::is_ge (const Expression &a, const Expression &b, BoundAnalysis &ba)
	Prove a >= b using a pre-built BoundAnalysis.
bool	sdfg::symbolic::is_gt (const Expression &a, const Expression &b, BoundAnalysis &ba)
	Prove a > b using a pre-built BoundAnalysis.
bool	sdfg::symbolic::is_le (const Expression &a, const Expression &b, BoundAnalysis &ba)
	Prove a <= b using a pre-built BoundAnalysis.
bool	sdfg::symbolic::is_lt (const Expression &a, const Expression &b, BoundAnalysis &ba)
	Prove a < b using a pre-built BoundAnalysis.
bool	sdfg::symbolic::is_eq (const Expression &a, const Expression &b, BoundAnalysis &ba)
	Prove a == b using a pre-built BoundAnalysis.

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

Detailed Description

Computing bounds of symbolic expressions using assumptions.

This file provides the BoundAnalysis class and convenience functions for computing the minimum and maximum values that symbolic expressions can take, given a set of assumptions about symbol bounds.

Bound Computation

The bound computation uses assumptions about symbols (from assumptions.h) to determine the extreme values (minimum and maximum) that an expression can reach. The computation considers:

• Symbol bounds from assumptions
• Parameter symbols (treated as unknowns preserved in the result)
• Tight vs. loose bounds (exact vs. conservative estimates)

Mathematical Foundation

For an expression e(x, p) where x_i in [l_i, u_i] and p are free parameters:

• Polynomial normalization groups correlated addends (e.g. -2x + Tx -> (T-2)x)
• Sign-aware affine analysis uses monotonicity: if coeff > 0, min(c*x) = c*min(x)
• For multilinear products, extrema occur at vertices of the bounding box
• min(max(a,b)) = max(min(a), min(b)); max(min(a,b)) = min(max(a), max(b))

See also

assumptions.h for information about symbol assumptions

symbolic.h for building symbolic expressions