Symbolic system for integer-based symbol analysis. More...

#include <symengine/add.h>
#include <symengine/basic.h>
#include <symengine/dict.h>
#include <symengine/integer.h>
#include <symengine/logic.h>
#include <symengine/mul.h>
#include <symengine/nan.h>
#include <symengine/real_double.h>
#include <symengine/simplify.h>
#include <symengine/symbol.h>
#include <unordered_map>
#include "symengine/functions.h"
#include "symengine/subs.h"

Classes
class	sdfg::symbolic::IModFunction
	Function class for integer modulo operation. More...
class	sdfg::symbolic::ZExtI64Function
	Function class for zero-extension to 64-bit integer. More...
class	sdfg::symbolic::TruncI32Function
	Function class for truncation to 32-bit integer. More...
class	sdfg::symbolic::SizeOfTypeFunction
	Function class representing sizeof for a type. More...
class	sdfg::symbolic::DynamicSizeOfFunction
	Function class for dynamic sizeof operation. More...
class	sdfg::symbolic::MallocUsableSizeFunction
	Function class for malloc_usable_size operation. More...

Namespaces
namespace	sdfg
namespace	sdfg::types
namespace	sdfg::symbolic

Typedefs
typedef SymEngine::RCP< const SymEngine::Symbol >	sdfg::symbolic::Symbol
	Reference-counted pointer to a SymEngine Symbol.
typedef SymEngine::RCP< const SymEngine::Number >	sdfg::symbolic::Number
	Reference-counted pointer to a SymEngine Number.
typedef SymEngine::RCP< const SymEngine::Integer >	sdfg::symbolic::Integer
	Reference-counted pointer to a SymEngine Integer constant.
typedef SymEngine::RCP< const SymEngine::Infty >	sdfg::symbolic::Infty
	Reference-counted pointer to a SymEngine Infinity value.
typedef SymEngine::RCP< const SymEngine::Basic >	sdfg::symbolic::Expression
	Reference-counted pointer to a symbolic expression (SymEngine Basic).
typedef SymEngine::RCP< const SymEngine::Boolean >	sdfg::symbolic::Condition
	Reference-counted pointer to a boolean condition expression.
typedef std::vector< Expression >	sdfg::symbolic::MultiExpression
	Vector of symbolic expressions for multi-dimensional operations.
typedef std::vector< Symbol >	sdfg::symbolic::SymbolVec
	Vector of symbols.
typedef std::set< Symbol, SymEngine::RCPBasicKeyLess >	sdfg::symbolic::SymbolSet
	Ordered set of symbols.
typedef std::unordered_map< Symbol, Expression, SymEngine::RCPBasicHash, SymEngine::RCPBasicKeyEq >	sdfg::symbolic::SymbolMap
	Map from symbols to expressions.
typedef std::vector< Symbol >	sdfg::symbolic::ExpressionVec
	Vector of expressions.
typedef std::set< Expression, SymEngine::RCPBasicKeyLess >	sdfg::symbolic::ExpressionSet
	Ordered set of expressions.
typedef std::unordered_map< Expression, Expression, SymEngine::RCPBasicHash, SymEngine::RCPBasicKeyEq >	sdfg::symbolic::ExpressionMap
	Map from expressions to expressions.
typedef SymEngine::map_basic_basic	sdfg::symbolic::ExpressionMapping

Functions
Symbol	sdfg::symbolic::symbol (const std::string &name)
	Creates a symbolic variable with the given name.
Integer	sdfg::symbolic::integer (int64_t value)
	Creates an integer constant.
Integer	sdfg::symbolic::zero ()
	Creates the integer constant 0.
Integer	sdfg::symbolic::one ()
	Creates the integer constant 1.
Condition	sdfg::symbolic::__false__ ()
	Creates a boolean false condition.
Condition	sdfg::symbolic::__true__ ()
	Creates a boolean true condition.
Symbol	sdfg::symbolic::__nullptr__ ()
	Creates a special null pointer symbol.
bool	sdfg::symbolic::is_nullptr (const Symbol symbol)
	Checks if a symbol is the null pointer.
bool	sdfg::symbolic::is_nullptr (const std::string &name)
	Same as is_nullptr(symbol(name)) without constructing a symbol.
bool	sdfg::symbolic::is_pointer (const Symbol symbol)
	Checks if a symbol represents a pointer.
bool	sdfg::symbolic::is_nv (const Symbol symbol)
	Checks if a symbol is an NVIDIA GPU built-in variable.
Condition	sdfg::symbolic::And (const Condition lhs, const Condition rhs)
	Logical AND of two conditions.
Condition	sdfg::symbolic::Or (const Condition lhs, const Condition rhs)
	Logical OR of two conditions.
Condition	sdfg::symbolic::Not (const Condition expr)
	Logical NOT (negation) of a condition.
bool	sdfg::symbolic::is_true (const Expression expr)
	Tests if an expression evaluates to true.
bool	sdfg::symbolic::is_false (const Expression expr)
	Tests if an expression evaluates to false.
Expression	sdfg::symbolic::add (const Expression lhs, const Expression rhs)
	Addition of two expressions.
Expression	sdfg::symbolic::sub (const Expression lhs, const Expression rhs)
	Subtraction of two expressions.
Expression	sdfg::symbolic::mul (const Expression lhs, const Expression rhs)
	Multiplication of two expressions.
Expression	sdfg::symbolic::div (const Expression lhs, const Expression rhs)
	Integer division idiv(lhs, rhs) with the semantics of signed C/C++ lhs / rhs on int64.
Expression	sdfg::symbolic::floor_div (const Expression lhs, const Expression divisor)
	Exact floor division floor(lhs / divisor) in terms of idiv.
Expression	sdfg::symbolic::ceil_div (const Expression dividend, const Expression divisor)
	Exact ceiling division ceil(dividend / divisor) in terms of idiv.
Expression	sdfg::symbolic::ceil_count (const Expression extent, const Expression chunk)
	Number of chunks of size chunk (positive) covering extent: max(0, ceil(extent / chunk)).
Expression	sdfg::symbolic::min (const Expression lhs, const Expression rhs)
	Minimum of two expressions.
Expression	sdfg::symbolic::max (const Expression lhs, const Expression rhs)
	Maximum of two expressions.
Expression	sdfg::symbolic::abs (const Expression expr)
	Absolute value of an expression.
Expression	sdfg::symbolic::mod (const Expression lhs, const Expression rhs)
	Integer remainder imod(lhs, rhs) with the semantics of signed C/C++ lhs % rhs on int64.
Expression	sdfg::symbolic::bit_xor (const Expression lhs, const Expression rhs)
	Bitwise XOR operation (integer).
Expression	sdfg::symbolic::pow (const Expression base, const Expression exp)
	Power/exponentiation operation.
Expression	sdfg::symbolic::zext_i64 (const Expression expr)
	Zero-extend to 64-bit integer.
Expression	sdfg::symbolic::trunc_i32 (const Expression expr)
	Truncate to 32-bit integer.
Expression	sdfg::symbolic::size_of_type (const types::IType &type)
	Computes the size of a type.
Expression	sdfg::symbolic::dynamic_sizeof (const Symbol symbol)
	Computes the dynamic size of a memory region.
Expression	sdfg::symbolic::malloc_usable_size (const Symbol symbol)
	Computes the usable size of a malloc allocation.
Condition	sdfg::symbolic::Eq (const Expression lhs, const Expression rhs)
	Equality comparison.
Condition	sdfg::symbolic::Ne (const Expression lhs, const Expression rhs)
	Inequality comparison.
Condition	sdfg::symbolic::Lt (const Expression lhs, const Expression rhs)
	Less-than comparison.
Condition	sdfg::symbolic::Gt (const Expression lhs, const Expression rhs)
	Greater-than comparison.
Condition	sdfg::symbolic::Le (const Expression lhs, const Expression rhs)
	Less-than-or-equal comparison.
Condition	sdfg::symbolic::Ge (const Expression lhs, const Expression rhs)
	Greater-than-or-equal comparison.
Expression	sdfg::symbolic::expand (const Expression expr)
	Expands an expression algebraically.
Expression	sdfg::symbolic::factor (const Expression expr)
	Factors an expression into a product of simpler terms.
Expression	sdfg::symbolic::simplify (const Expression expr)
	Simplifies an expression.
Expression	sdfg::symbolic::overapproximate (const Expression expr)
	Overapproximates an expression by resolving min/max to upper bounds.
bool	sdfg::symbolic::eq (const Expression lhs, const Expression rhs)
	Tests structural equality of two expressions.
bool	sdfg::symbolic::null_safe_eq (const Expression lhs, const Expression rhs)
	Tests equality of expressions with null-safety.
bool	sdfg::symbolic::uses (const Expression expr, const Symbol sym)
	Tests if an expression uses a specific symbol.
bool	sdfg::symbolic::uses (const Expression expr, const std::string &name)
	Tests if an expression uses a symbol with a specific name.
SymbolSet	sdfg::symbolic::atoms (const Expression expr)
	Extracts all symbols (atoms) from an expression.
template<typename T>
bool	sdfg::symbolic::has (const Expression expr)
	Checks if an expression contains a specific SymEngine type.
template<typename T>
ExpressionSet	sdfg::symbolic::find (const Expression expr)
	Finds all instances of a specific SymEngine type in an expression.
bool	sdfg::symbolic::has_dynamic_sizeof (const Expression expr)
	Checks if an expression contains a dynamic_sizeof operation.
ExpressionSet	sdfg::symbolic::muls (const Expression expr)
	Extracts all multiplication operations from an expression.
Expression	sdfg::symbolic::subs (const Expression expr, const Expression old_expr, const Expression new_expr)
	Substitutes a sub-expression with another expression.
Expression	sdfg::symbolic::subs (const Expression expr, const symbolic::ExpressionMapping &replacements)
	Bulk replacement.
Condition	sdfg::symbolic::subs (const Condition expr, const Expression old_expr, const Expression new_expr)
	Substitutes a sub-expression in a condition.
Condition	sdfg::symbolic::subs (const Condition expr, const symbolic::ExpressionMapping &replacements)
	Bulk replacement.
bool	sdfg::symbolic::substitute (ExpressionSet &set, const symbolic::ExpressionMapping &replacements)
MultiExpression	sdfg::symbolic::substitute (const MultiExpression &vec, const symbolic::ExpressionMapping &replacements)
Expression	sdfg::symbolic::inverse (const Expression expr, const Symbol symbol)
	Computes the inverse of an expression with respect to a symbol.
Symbol	sdfg::symbolic::threadIdx_x ()
	Thread index in X dimension.
Symbol	sdfg::symbolic::threadIdx_y ()
	Thread index in Y dimension.
Symbol	sdfg::symbolic::threadIdx_z ()
	Thread index in Z dimension.
Symbol	sdfg::symbolic::blockDim_x ()
	Block dimension (threads per block) in X.
Symbol	sdfg::symbolic::blockDim_y ()
	Block dimension (threads per block) in Y.
Symbol	sdfg::symbolic::blockDim_z ()
	Block dimension (threads per block) in Z.
Symbol	sdfg::symbolic::blockIdx_x ()
	Block index in X dimension.
Symbol	sdfg::symbolic::blockIdx_y ()
	Block index in Y dimension.
Symbol	sdfg::symbolic::blockIdx_z ()
	Block index in Z dimension.
Symbol	sdfg::symbolic::gridDim_x ()
	Grid dimension (blocks per grid) in X.
Symbol	sdfg::symbolic::gridDim_y ()
	Grid dimension (blocks per grid) in Y.
Symbol	sdfg::symbolic::gridDim_z ()
	Grid dimension (blocks per grid) in Z.
Expression	sdfg::symbolic::parse (const std::string &expr_str)
	Parses a string into a symbolic expression.

Detailed Description

Symbolic system for integer-based symbol analysis.

This file defines the symbolic system used throughout sdfglib. Symbolic expressions form the basis of the IR and are used to represent:

Address calculations in memlets
Loop iteration variables and bounds (indvar, bounds)
Conditional expressions in if-else statements (conditions)

Symbolic System

Symbolic expressions are functions of symbols, constants, and other symbolic expressions. The system is thereby constrained to the representation of integer-like symbols:

Every constant integer is a symbolic expression.
Every container declared as an integer is a symbol.
Every pointer declared in the SDFG system is a symbol.
Arithmetic operations (+, -, *, /, %, min, max, abs, pow) on symbolic expressions yield new symbolic expressions.

Examples

Creating symbols and expressions:

auto x = symbolic::symbol("x");
auto y = symbolic::symbol("y");
auto expr = symbolic::add(symbolic::mul(x, symbolic::integer(2)), y);  // 2*x + y

Building conditions:

auto cond = symbolic::And(symbolic::Ge(x, symbolic::zero()), symbolic::Lt(x, symbolic::integer(10)));

See also: assumptions.h for information on reasoning about symbol bounds and evolution; sets.h for integer set operations and disjointness checking

Classes

Namespaces

Typedefs

Functions

Detailed Description

Symbolic System

Examples