24 #ifndef TVM_ARITH_ANALYZER_H_
25 #define TVM_ARITH_ANALYZER_H_
28 #include <tvm/ffi/reflection/registry.h>
34 #include <unordered_map>
92 refl::ObjectDef<ConstIntBoundNode>()
132 using BoundMapType = std::unordered_map<PrimExpr, ConstIntBound, ObjectPtrHash, ObjectPtrEqual>;
184 std::function<void()> EnterConstraint(
const PrimExpr& constraint);
212 refl::ObjectDef<ModularSetNode>()
263 std::function<void()> EnterConstraint(
const PrimExpr& constraint);
463 return CompareResult(
static_cast<int>(lhs) &
static_cast<int>(rhs));
466 return CompareResult(
static_cast<int>(lhs) |
static_cast<int>(rhs));
495 bool propagate_inequalities =
true);
528 std::unique_ptr<Impl> impl_;
557 : analyzer_(analyzer), constraint_(constraint) {}
559 void EnterWithScope();
561 void ExitWithScope();
567 std::vector<std::function<void()>> recovery_functions_;
611 TVM_DLL
void Bind(
const Var&
var,
const Range& new_range,
bool allow_override =
false);
705 void Bind(
const ffi::Map<Var, Range>& variables,
bool allow_override =
false);
Reference to PrimExprNode.
Definition: expr.h:124
Range container
Definition: expr.h:689
RAII wrapper function to enter and exit a context object similar to python's with syntax.
Definition: with.h:58
Analyzer that contains bunch of sub-analyzers.
Definition: analyzer.h:634
void Bind(const ffi::Map< Var, Range > &variables, bool allow_override=false)
Bind all the vars in the Map.
IntSetAnalyzer int_set
sub-analyzer: int set
Definition: analyzer.h:650
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.
TransitiveComparisonAnalyzer transitive_comparisons
sub-analyzer transitive comparisons
Definition: analyzer.h:652
ConstIntBoundAnalyzer const_int_bound
sub-analyzer: const integer bound
Definition: analyzer.h:642
bool CanProveLessEqualThanSymbolicShapeValue(const PrimExpr &lhs, const PrimExpr &shape)
Whether we can prove lhs is smaller than possibly symbolic shape.
bool CanProveEqual(const PrimExpr &lhs, const PrimExpr &rhs)
Whether can we prove lhs == rhs.
bool CanProveGreaterEqual(const PrimExpr &expr, int64_t lower_bound)
Whether can we prove expr >= val.
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.
CanonicalSimplifier canonical_simplify
sub-analyzer canonical simplify
Definition: analyzer.h:648
bool CanProve(const PrimExpr &cond, ProofStrength strength=ProofStrength::kDefault)
Whether can we prove condition.
void MarkGlobalNonNegValue(const PrimExpr &value)
Mark the value as non-negative value globally in analyzer.
PrimExpr Simplify(const PrimExpr &expr, int steps=2)
Simplify expr.
Analyzer & operator=(const Analyzer &)=delete
ModularSetAnalyzer modular_set
sub-analyzer: modular set
Definition: analyzer.h:644
RewriteSimplifier rewrite_simplify
sub-analyzer rewrite simplify
Definition: analyzer.h:646
bool CanProveLess(const PrimExpr &expr, int64_t upper_bound)
Whether can we prove expr < val.
Analyzer(const Analyzer &)=delete
Canonical-form based simplifier.
Definition: analyzer.h:418
PrimExpr operator()(const PrimExpr &expr)
analyze the expr
void Update(const Var &var, const PrimExpr &new_expr, bool allow_override=false)
Update binding of var to a new expression.
Analyzer to get constant integer bound over expression.
Definition: analyzer.h:130
bool IsBound(const Var &var) const
Check if a variable is bound to a range.
std::unordered_map< PrimExpr, ConstIntBound, ObjectPtrHash, ObjectPtrEqual > BoundMapType
Definition: analyzer.h:132
void Update(const Var &var, const ConstIntBound &info, bool allow_override=false)
Update constant int bound information of var.
void Bind(const Var &var, const Range &range, bool allow_override=false)
Bind variable to a range.
ConstIntBound operator()(const PrimExpr &expr, BoundMapType *bound)
analyze the expr with the intermediate memorized to avoid redundant computation
ConstIntBound operator()(const PrimExpr &expr) const
analyze the expr
Constant integer up and lower bound(inclusive). Useful for value bound analysis.
Definition: analyzer.h:85
int64_t min_value
Definition: analyzer.h:87
TVM_FFI_DECLARE_OBJECT_INFO_FINAL("arith.ConstIntBound", ConstIntBoundNode, Object)
static constexpr const int64_t kNegInf
Number to represent -inf.
Definition: analyzer.h:103
int64_t max_value
Definition: analyzer.h:88
static constexpr TVMFFISEqHashKind _type_s_eq_hash_kind
Definition: analyzer.h:105
static constexpr const int64_t kPosInf
Number to represent +inf.
Definition: analyzer.h:98
static void RegisterReflection()
Definition: analyzer.h:90
reference class to ConstIntBoundNode
Definition: analyzer.h:113
TVM_FFI_DEFINE_OBJECT_REF_METHODS_NULLABLE(ConstIntBound, ObjectRef, ConstIntBoundNode)
static constexpr const int64_t kNegInf
Definition: analyzer.h:123
ConstIntBound(int64_t min_value, int64_t max_value)
constructor by fields.
static constexpr const int64_t kPosInf
Definition: analyzer.h:122
Constraint context.
Definition: analyzer.h:547
Integer set analyzer.
Definition: analyzer.h:573
std::function< void()> EnterConstraint(const PrimExpr &constraint)
void Update(const Var &var, const IntSet &new_interval_set, bool allow_override=false)
Update binding of var to a new expression.
void Bind(const Var &var, const Range &new_range, bool allow_override=false)
Update binding of var to a new expression.
IntSet operator()(const PrimExpr &expr, const ffi::Map< Var, IntSet > &dom_map)
Find a symbolic integer set that contains all possible values of expr given the domain of each variab...
IntSet operator()(const PrimExpr &expr)
Find a symbolic integer set that contains all possible values of expr given the domain of each variab...
Managed reference to IntSetNode.
Definition: int_set.h:66
Analyzer to get modular information over expression.
Definition: analyzer.h:235
void Update(const Var &var, const ModularSet &info, bool allow_override=false)
Update constant int bound information of var.
ModularSet operator()(const PrimExpr &expr)
analyze the expr
Range of a linear integer function. Use to do specify the possible index values.
Definition: analyzer.h:203
int64_t coeff
linear co-efficient
Definition: analyzer.h:206
static void RegisterReflection()
Definition: analyzer.h:210
static constexpr TVMFFISEqHashKind _type_s_eq_hash_kind
Definition: analyzer.h:217
TVM_FFI_DECLARE_OBJECT_INFO_FINAL("arith.ModularSet", ModularSetNode, Object)
int64_t base
The base.
Definition: analyzer.h:208
reference of ModularSetNode
Definition: analyzer.h:225
TVM_FFI_DEFINE_OBJECT_REF_METHODS_NULLABLE(ModularSet, ObjectRef, ModularSetNode)
ModularSet(int64_t coeff, int64_t base)
Rewrite-rule based simplifier.
Definition: analyzer.h:273
std::function< void()> EnterConstraint(const PrimExpr &constraint)
Update the internal state to enter constraint.
Extension GetEnabledExtensions() const
Return the currently enabled extensions.
void SetEnabledExtensions(Extension flags)
Enable an optional extension or extensions.
ObjectRef GetStatsCounters() const
Return the statistics counters.
void Update(const Var &var, const PrimExpr &new_expr, bool allow_override=false)
Update binding of var to a new expression.
Extension
Flags to enable more computationally-intensive simplifications.
Definition: analyzer.h:311
@ kNone
Definition: analyzer.h:313
@ kApplyConstraintsToBooleanBranches
Definition: analyzer.h:341
@ kTransitivelyProveInequalities
Definition: analyzer.h:320
@ kComparisonOfProductAndSum
Definition: analyzer.h:370
@ kConvertBooleanToAndOfOrs
Definition: analyzer.h:328
void SetMaximumRewriteSteps(int64_t maximum)
Set the maximum allowed number of rewrite steps.
void ResetStatsCounters()
Reset the statistics counters.
PrimExpr operator()(const PrimExpr &expr)
analyze the expr
Using previously specified knowns, compare the expressions provided.
Definition: analyzer.h:475
void Bind(const Var &var, const Range &range, bool allow_override=false)
Bind a variable as being within a specified range.
std::function< void()> EnterConstraint(const PrimExpr &constraint)
Update the internal state to enter constraint.
void Bind(const Var &var, const PrimExpr &expr, bool allow_override=false)
Bind a variable as being equal to a known expression.
CompareResult TryCompare(const PrimExpr &lhs, const PrimExpr &rhs, bool propagate_inequalities=true)
a named variable in TIR
Definition: var.h:77
ProofStrength
The strength used in top-level condition proves.
Definition: analyzer.h:70
@ kSymbolicBound
Prove using symbolic bound analysis.
@ kDefault
default strength, can be used in.
CompareResult
Structure for representing result of known.
Definition: analyzer.h:451
constexpr CompareResult operator|(CompareResult lhs, CompareResult rhs)
Definition: analyzer.h:465
DivMode
Definition: analyzer.h:56
@ kTruncDiv
Truncated division.
Definition: analyzer.h:58
@ kFloorDiv
Floor division.
Definition: analyzer.h:60
@ kUnknown
Definition: int_set.h:50
constexpr CompareResult operator&(CompareResult lhs, CompareResult rhs)
Definition: analyzer.h:462
Definition: repr_printer.h:91
Var var(std::string name_hint, DataType t=DataType::Int(32))
Construct a new Var expression.
Tensor shape(const Tensor &src, DataType dtype, const std::string name="T_shape", const std::string tag=kInjective)
Get the shape of input tensor.
Definition: transform.h:1960
tvm::PrimExpr maximum(const tvm::PrimExpr &a, const tvm::PrimExpr &b)
Definition: broadcast.h:359
Performance counters for profiling via the PAPI library.
Definition: analyzer.h:37
PrimExpr max(PrimExpr a, PrimExpr b, Span span=Span())
take maximum of two values
PrimExpr min_value(const DataType &dtype, Span span=Span())
PrimExpr max_value(const DataType &dtype, Span span=Span())
RAII wrapper function to enter and exit a context object similar to python's with syntax.