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

#include <analyzer.h>

Inheritance diagram for tvm::arith::AnalyzerObj:

Collaboration diagram for tvm::arith::AnalyzerObj:

Public Member Functions
	AnalyzerObj ()
	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 ffi::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...

Analyzer	Clone () const
	Deep-copy this analyzer into a new, independent Analyzer. More...

	TVM_FFI_DECLARE_OBJECT_INFO_FINAL ("arith.Analyzer", AnalyzerObj, ffi::Object)

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...

Z3Prover	z3_prover
	sub-analyzer using Z3 More...

Static Public Attributes
static constexpr bool	_type_mutable = true
	Analyzer methods update facts, constraints, caches, and stats. 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

◆ AnalyzerObj()

tvm::arith::AnalyzerObj::AnalyzerObj ( )

constructor

Member Function Documentation

◆ Bind() [1/3]

void tvm::arith::AnalyzerObj::Bind	(	const ffi::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::AnalyzerObj::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::AnalyzerObj::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::AnalyzerObj::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::AnalyzerObj::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::AnalyzerObj::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::AnalyzerObj::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::AnalyzerObj::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.

◆ Clone()

Analyzer tvm::arith::AnalyzerObj::Clone ( ) const

Deep-copy this analyzer into a new, independent Analyzer.

The returned analyzer carries the same accumulated facts (variable bounds, modular sets, rewrite/canonical bindings, integer-set domains, literal constraints and transitive comparisons) as this one, but owns its own state: binding or simplifying on either analyzer afterwards does not affect the other. This is the deep copy that handle-copying an Analyzer does not provide.

Note: Do not call this while a With<ConstraintContext> scope is active on this analyzer. The clone would inherit the scoped constraints but not the recovery functions that pop them on scope exit, so the constraints would leak as if they were global facts. Clone at a point where no constraint scope is in effect.

Returns: A new Analyzer holding an independent copy of the facts.

◆ MarkGlobalNonNegValue()

void tvm::arith::AnalyzerObj::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

A canonical use of MarkGlobalNonNegValue is to record a non-negativity fact at a Var's definition site. Because each Var identity is defined exactly once in canonical IR, the fact is globally valid for that identity.

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.

◆ Simplify()

PrimExpr tvm::arith::AnalyzerObj::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.

◆ TVM_FFI_DECLARE_OBJECT_INFO_FINAL()

tvm::arith::AnalyzerObj::TVM_FFI_DECLARE_OBJECT_INFO_FINAL	(	"arith.Analyzer"	,
		AnalyzerObj	,
		ffi::Object
	)

Member Data Documentation

◆ _type_mutable

constexpr bool tvm::arith::AnalyzerObj::_type_mutable = true

staticconstexpr

Analyzer methods update facts, constraints, caches, and stats.

Marking the object mutable makes the Analyzer ObjectRef expose a non-const operator->, so APIs can take const Analyzer& while still allowing calls such as analyzer->Bind(...). const Analyzer& keeps the handle itself from being rebound; it does not make the underlying AnalyzerObj immutable.

◆ canonical_simplify

CanonicalSimplifier tvm::arith::AnalyzerObj::canonical_simplify

sub-analyzer canonical simplify

◆ const_int_bound

ConstIntBoundAnalyzer tvm::arith::AnalyzerObj::const_int_bound

sub-analyzer: const integer bound

◆ int_set

IntSetAnalyzer tvm::arith::AnalyzerObj::int_set

sub-analyzer: int set

◆ modular_set

ModularSetAnalyzer tvm::arith::AnalyzerObj::modular_set

sub-analyzer: modular set

◆ rewrite_simplify

RewriteSimplifier tvm::arith::AnalyzerObj::rewrite_simplify

sub-analyzer rewrite simplify

◆ transitive_comparisons

TransitiveComparisonAnalyzer tvm::arith::AnalyzerObj::transitive_comparisons

sub-analyzer transitive comparisons

◆ z3_prover

Z3Prover tvm::arith::AnalyzerObj::z3_prover

sub-analyzer using Z3

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

include/tvm/arith/analyzer.h

Public Member Functions

Public Attributes

Static Public Attributes

Detailed Description

Constructor & Destructor Documentation

◆ AnalyzerObj()

Member Function Documentation

◆ Bind() [1/3]

◆ Bind() [2/3]

◆ Bind() [3/3]

◆ CanProve()

◆ CanProveEqual()

◆ CanProveGreaterEqual()

◆ CanProveLess()

◆ CanProveLessEqualThanSymbolicShapeValue()

◆ Clone()

◆ MarkGlobalNonNegValue()

◆ Simplify()

◆ TVM_FFI_DECLARE_OBJECT_INFO_FINAL()

Member Data Documentation

◆ _type_mutable

◆ canonical_simplify

◆ const_int_bound

◆ int_set

◆ modular_set

◆ rewrite_simplify

◆ transitive_comparisons

◆ z3_prover