MimIR
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
constraints.cpp
Go to the documentation of this file.
2
4
5namespace {
6
7bool statically_le(const Def* lhs, const Def* rhs) {
8 if (lhs == rhs) return true;
9 auto l = Lit::isa<u64>(lhs);
10 auto r = Lit::isa<u64>(rhs);
11 return l && r && *l <= *r;
12}
13
14bool statically_violates(const Def* lhs, const Def* rhs) {
15 auto l = Lit::isa<u64>(lhs);
16 auto r = Lit::isa<u64>(rhs);
17 return l && r && *l > *r;
18}
19
20} // namespace
21
23 const Def* dim,
24 const Def* source_shape,
25 const Def* index_shape) {
26 auto rank_l = Lit::isa<u64>(rank);
27 auto dim_l = Lit::isa<u64>(dim);
28 if (!rank_l || !dim_l) return false;
29
30 bool proven = true;
31 for (u64 d = 0; d < *rank_l; ++d)
32 if (d != *dim_l) {
33 auto lhs = index_shape->proj(*rank_l, d);
34 auto rhs = source_shape->proj(*rank_l, d);
35 if (statically_violates(lhs, rhs))
36 fe::throwf("gather index shape exceeds input shape at axis {}", d);
37 proven &= statically_le(lhs, rhs);
38 }
39 return proven;
40}
41
43 const Def* dim,
44 const Def* source_shape,
45 const Def* index_shape,
46 const Def* updates_shape) {
47 auto rank_l = Lit::isa<u64>(rank);
48 auto dim_l = Lit::isa<u64>(dim);
49 if (!rank_l || !dim_l) return false;
50
51 bool proven = true;
52 for (u64 d = 0; d < *rank_l; ++d) {
53 auto idx = index_shape->proj(*rank_l, d);
54 auto upd = updates_shape->proj(*rank_l, d);
55 if (d != *dim_l) {
56 auto src = source_shape->proj(*rank_l, d);
57 if (statically_violates(idx, src))
58 fe::throwf("scatter index shape exceeds input shape at axis {}", d);
59 proven &= statically_le(idx, src);
60 }
61 if (statically_violates(idx, upd))
62 fe::throwf("scatter index shape exceeds updates shape at axis {}", d);
63 proven &= statically_le(idx, upd);
64 }
65 return proven;
66}
67
68} // namespace mim::plug::tensor::phase
Base class for all Defs.
Definition def.h:273
const Def * proj(nat_t a, nat_t i) const
Similar to World::extract while assuming an arity of a, but also works on Sigmas and Arrays.
Definition def.cpp:623
static std::optional< T > isa(const Def *def)
Definition def.h:937
bool check_scatter_shape_constraints(const Def *rank, const Def *dim, const Def *source_shape, const Def *index_shape, const Def *updates_shape)
Checks statically decidable scatter constraints. Returns false for unresolved relations.
bool check_gather_shape_constraints(const Def *rank, const Def *dim, const Def *source_shape, const Def *index_shape)
Checks statically decidable gather constraints. Returns false for unresolved relations.
uint64_t u64
Definition types.h:27