Analyzer that contains bunch of sub-analyzers. More...

#include <analyzer.h>

Collaboration diagram for tvm::arith::Analyzer:

Public Member Functions
	Analyzer (const Analyzer &)=delete

Analyzer &	operator= (const Analyzer &)=delete

	Analyzer ()
	constructor More...

void	MarkGlobalNonNegValue (const PrimExpr &value)
	Mark the value as non-negative value globally in analyzer. More...

void	Bind (const Var &var, const PrimExpr &expr, bool allow_override=false)
	Notify all the sub-analyzers that var is created and binded to expr. More...

void	Bind (const Var &var, const Range &range, bool allow_override=false)
	Notify all the sub-analyzers that var is created and bound to a range. More...

void	Bind (const Map< Var, Range > &variables, bool allow_override=false)
	Bind all the vars in the Map. More...

bool	CanProveGreaterEqual (const PrimExpr &expr, int64_t lower_bound)
	Whether can we prove expr >= val. More...

bool	CanProveLess (const PrimExpr &expr, int64_t upper_bound)
	Whether can we prove expr < val. More...

bool	CanProveEqual (const PrimExpr &lhs, const PrimExpr &rhs)
	Whether can we prove lhs == rhs. More...

bool	CanProveLessEqualThanSymbolicShapeValue (const PrimExpr &lhs, const PrimExpr &shape)
	Whether we can prove lhs is smaller than possibly symbolic shape. More...

bool	CanProve (const PrimExpr &cond, ProofStrength strength=ProofStrength::kDefault)
	Whether can we prove condition. More...

PrimExpr	Simplify (const PrimExpr &expr, int steps=2)
	Simplify expr. More...

Public Attributes
ConstIntBoundAnalyzer	const_int_bound
	sub-analyzer: const integer bound More...

ModularSetAnalyzer	modular_set
	sub-analyzer: modular set More...

RewriteSimplifier	rewrite_simplify
	sub-analyzer rewrite simplify More...

CanonicalSimplifier	canonical_simplify
	sub-analyzer canonical simplify More...

IntSetAnalyzer	int_set
	sub-analyzer: int set More...

TransitiveComparisonAnalyzer	transitive_comparisons
	sub-analyzer transitive comparisons More...

Detailed Description

Analyzer that contains bunch of sub-analyzers.

Each sub-analyzer can make use of another sub-analyzer by weak reference of this.

NOTE for sub-analyzer developers: If the analyzer uses memoization, we need to clear the internal cache when information about a Var has been overridden.

Constructor & Destructor Documentation

◆ Analyzer() [1/2]

tvm::arith::Analyzer::Analyzer ( const Analyzer & )

delete

◆ Analyzer() [2/2]

tvm::arith::Analyzer::Analyzer ( )

constructor

Member Function Documentation

◆ Bind() [1/3]

void tvm::arith::Analyzer::Bind	(	const Map< Var, Range > &	variables,
		bool	allow_override = `false`
	)

Bind all the vars in the Map.

Parameters

variables	The {variable -> range} map.
allow_override	Whether we allow overriding an existing var's expression. This option should not be used if there is any dependency between variables.

◆ Bind() [2/3]

void tvm::arith::Analyzer::Bind	(	const Var &	var,
		const PrimExpr &	expr,
		bool	allow_override = `false`
	)

Notify all the sub-analyzers that var is created and binded to expr.

Each var can only be bound once.

Parameters

var	The variable.
expr	The expression we bind to.
allow_override	Whether we allow overriding an existing var's expression. This option should not be used if there is any dependency between variables.

◆ Bind() [3/3]

void tvm::arith::Analyzer::Bind	(	const Var &	var,
		const Range &	range,
		bool	allow_override = `false`
	)

Notify all the sub-analyzers that var is created and bound to a range.

Each var can only be bound once.

Parameters

var	The variable.
range	The range we bind to.
allow_override	Whether we allow overriding an existing var's expression. This option should not be used if there is any dependency between variables.

◆ CanProve()

bool tvm::arith::Analyzer::CanProve	(	const PrimExpr &	cond,
		ProofStrength	strength = `ProofStrength::kDefault`
	)

Whether can we prove condition.

Parameters

cond	The expression to be proved.
strength	the strength of the prove.

Returns: The result.

Note: Analyzer will call into sub-analyzers to get the result. Do not use strength beyond default in sub-analyzers and only use it in top-level predicate analysis.

◆ CanProveEqual()

bool tvm::arith::Analyzer::CanProveEqual	(	const PrimExpr &	lhs,
		const PrimExpr &	rhs
	)

Whether can we prove lhs == rhs.

Parameters

lhs	The input lhs.
rhs	The input rhs.

Returns: Whether we can prove lhs == rhs.

Note: Analyzer will call into sub-analyzers to get the result.

◆ CanProveGreaterEqual()

bool tvm::arith::Analyzer::CanProveGreaterEqual	(	const PrimExpr &	expr,
		int64_t	lower_bound
	)

Whether can we prove expr >= val.

Non-negative proof is very useful in integer analysis to lower divisions and mods given difference in trunc and ceil mode.

Parameters

expr	The expression.
lower_bound	The lower bound.

Returns: Whether we can prove it.

Note: Analyzer will call into sub-analyzers to get the result.

◆ CanProveLess()

bool tvm::arith::Analyzer::CanProveLess	(	const PrimExpr &	expr,
		int64_t	upper_bound
	)

Whether can we prove expr < val.

Non-negative proof is very useful in integer analysis to lower divisions and mods given difference in trunc and ceil mode.

Parameters

expr	The expression.
upper_bound	The upper bound.

Returns: Whether we can prove it.

Note: Analyzer will call into sub-analyzers to get the result.

◆ CanProveLessEqualThanSymbolicShapeValue()

bool tvm::arith::Analyzer::CanProveLessEqualThanSymbolicShapeValue	(	const PrimExpr &	lhs,
		const PrimExpr &	shape
	)

Whether we can prove lhs is smaller than possibly symbolic shape.

By calling this function, the caller gives an extra hint that shape > 0, because it appeared in buffer shape.

This is useful to prove condition such as 32 <= 32 * n where the 32 * n is known to be a shape. Use this routine to reduce the symbolic comparisons in buffer compaction.

The underlying analyzer will use the kSymbolicBound proof.

Parameters

lhs	The input lhs.
shape	The symbolic shape.

Returns: Whether we can prove lhs <= shape.

◆ MarkGlobalNonNegValue()

void tvm::arith::Analyzer::MarkGlobalNonNegValue ( const PrimExpr & value )

Mark the value as non-negative value globally in analyzer.

Only call this function if the non-neg condition is global and not context-dependent.

This function does best-effort propagations to the sub-analyzers

Note: We expose this function because non-negative global values, such as symbolic buffer shapes in function arguments are really important to ensure the best simplification, and usually they can be handled in a simpler way than the generic constraints.

This function may call into the Update function of the sub-analyzers.

◆ operator=()

Analyzer& tvm::arith::Analyzer::operator= ( const Analyzer & )

delete

◆ Simplify()

PrimExpr tvm::arith::Analyzer::Simplify	(	const PrimExpr &	expr,
		int	steps = `2`
	)

Simplify expr.

Parameters

expr	The expression to be simplified.
steps	The simplification runs in the order of rewrite_simplify (step 1) -> canonical_simplify (step 2) -> rewrite_simplify (step 3) -> canonical_simplify (step 4) -> ... param steps controls how many steps to run. Default is 2, i.e., rewrite_simplify + canonical_simplify.

Returns: The result.

Note: Analyzer will call into sub-analyzers to get the result.

Member Data Documentation

◆ canonical_simplify

CanonicalSimplifier tvm::arith::Analyzer::canonical_simplify

sub-analyzer canonical simplify

◆ const_int_bound

ConstIntBoundAnalyzer tvm::arith::Analyzer::const_int_bound

sub-analyzer: const integer bound

◆ int_set

IntSetAnalyzer tvm::arith::Analyzer::int_set

sub-analyzer: int set

◆ modular_set

ModularSetAnalyzer tvm::arith::Analyzer::modular_set

sub-analyzer: modular set

◆ rewrite_simplify

RewriteSimplifier tvm::arith::Analyzer::rewrite_simplify

sub-analyzer rewrite simplify

◆ transitive_comparisons

TransitiveComparisonAnalyzer tvm::arith::Analyzer::transitive_comparisons

sub-analyzer transitive comparisons

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

include/tvm/arith/analyzer.h

Public Member Functions

Public Attributes

Detailed Description

Constructor & Destructor Documentation

◆ Analyzer() [1/2]

◆ Analyzer() [2/2]

Member Function Documentation

◆ Bind() [1/3]

◆ Bind() [2/3]

◆ Bind() [3/3]

◆ CanProve()

◆ CanProveEqual()

◆ CanProveGreaterEqual()

◆ CanProveLess()

◆ CanProveLessEqualThanSymbolicShapeValue()

◆ MarkGlobalNonNegValue()

◆ operator=()

◆ Simplify()

Member Data Documentation

◆ canonical_simplify

◆ const_int_bound

◆ int_set

◆ modular_set

◆ rewrite_simplify

◆ transitive_comparisons