24
24
namespace mlir {
25
25
namespace presburger {
26
26
27
- // / An IntegerRelation is a PresburgerSpace subject to affine constraints.
28
- // / Affine constraints can be inequalities or equalities in the form:
27
+ // / An IntegerRelation represents the set of points from a PresburgerSpace that
28
+ // / satisfy a list of affine constraints. Affine constraints can be inequalities
29
+ // / or equalities in the form:
29
30
// /
30
31
// / Inequality: c_0*x_0 + c_1*x_1 + .... + c_{n-1}*x_{n-1} + c_n >= 0
31
32
// / Equality : c_0*x_0 + c_1*x_1 + .... + c_{n-1}*x_{n-1} + c_n == 0
@@ -42,7 +43,7 @@ namespace presburger {
42
43
// /
43
44
// / Since IntegerRelation makes a distinction between dimensions, IdKind::Range
44
45
// / and IdKind::Domain should be used to refer to dimension identifiers.
45
- class IntegerRelation : public PresburgerSpace {
46
+ class IntegerRelation {
46
47
public:
47
48
// / All derived classes of IntegerRelation.
48
49
enum class Kind {
@@ -58,11 +59,11 @@ class IntegerRelation : public PresburgerSpace {
58
59
IntegerRelation (unsigned numReservedInequalities,
59
60
unsigned numReservedEqualities, unsigned numReservedCols,
60
61
const PresburgerSpace &space)
61
- : PresburgerSpace (space),
62
- equalities ( 0 , getNumIds() + 1, numReservedEqualities, numReservedCols),
63
- inequalities(0 , getNumIds() + 1, numReservedInequalities,
62
+ : space (space), equalities( 0 , space.getNumIds() + 1 ,
63
+ numReservedEqualities, numReservedCols),
64
+ inequalities (0 , space. getNumIds() + 1, numReservedInequalities,
64
65
numReservedCols) {
65
- assert (numReservedCols >= getNumIds () + 1 );
66
+ assert (numReservedCols >= space. getNumIds () + 1 );
66
67
}
67
68
68
69
// / Constructs a relation with the specified number of dimensions and symbols.
@@ -71,6 +72,8 @@ class IntegerRelation : public PresburgerSpace {
71
72
/* numReservedEqualities=*/ 0 ,
72
73
/* numReservedCols=*/ space.getNumIds() + 1, space) {}
73
74
75
+ virtual ~IntegerRelation () = default ;
76
+
74
77
// / Return a system with no constraints, i.e., one which is satisfied by all
75
78
// / points.
76
79
static IntegerRelation getUniverse (const PresburgerSpace &space) {
@@ -85,6 +88,16 @@ class IntegerRelation : public PresburgerSpace {
85
88
// Clones this object.
86
89
std::unique_ptr<IntegerRelation> clone () const ;
87
90
91
+ // / Returns a reference to the underlying space.
92
+ const PresburgerSpace &getSpace () const { return space; }
93
+
94
+ // / Returns a copy of the space without locals.
95
+ PresburgerSpace getSpaceWithoutLocals () const {
96
+ return PresburgerSpace::getRelationSpace (space.getNumDomainIds (),
97
+ space.getNumRangeIds (),
98
+ space.getNumSymbolIds ());
99
+ }
100
+
88
101
// / Appends constraints from `other` into `this`. This is equivalent to an
89
102
// / intersection with no simplification of any sort attempted.
90
103
void append (const IntegerRelation &other);
@@ -117,8 +130,19 @@ class IntegerRelation : public PresburgerSpace {
117
130
return getNumInequalities () + getNumEqualities ();
118
131
}
119
132
133
+ unsigned getNumDomainIds () const { return space.getNumDomainIds (); }
134
+ unsigned getNumRangeIds () const { return space.getNumRangeIds (); }
135
+ unsigned getNumSymbolIds () const { return space.getNumSymbolIds (); }
136
+ unsigned getNumLocalIds () const { return space.getNumLocalIds (); }
137
+
138
+ unsigned getNumDimIds () const { return space.getNumDimIds (); }
139
+ unsigned getNumDimAndSymbolIds () const {
140
+ return space.getNumDimAndSymbolIds ();
141
+ }
142
+ unsigned getNumIds () const { return space.getNumIds (); }
143
+
120
144
// / Returns the number of columns in the constraint system.
121
- inline unsigned getNumCols () const { return getNumIds () + 1 ; }
145
+ inline unsigned getNumCols () const { return space. getNumIds () + 1 ; }
122
146
123
147
inline unsigned getNumEqualities () const { return equalities.getNumRows (); }
124
148
@@ -142,6 +166,27 @@ class IntegerRelation : public PresburgerSpace {
142
166
return inequalities.getRow (idx);
143
167
}
144
168
169
+ // / Get the number of ids of the specified kind.
170
+ unsigned getNumIdKind (IdKind kind) const { return space.getNumIdKind (kind); };
171
+
172
+ // / Return the index at which the specified kind of id starts.
173
+ unsigned getIdKindOffset (IdKind kind) const {
174
+ return space.getIdKindOffset (kind);
175
+ };
176
+
177
+ // / Return the index at Which the specified kind of id ends.
178
+ unsigned getIdKindEnd (IdKind kind) const { return space.getIdKindEnd (kind); };
179
+
180
+ // / Get the number of elements of the specified kind in the range
181
+ // / [idStart, idLimit).
182
+ unsigned getIdKindOverlap (IdKind kind, unsigned idStart,
183
+ unsigned idLimit) const {
184
+ return space.getIdKindOverlap (kind, idStart, idLimit);
185
+ };
186
+
187
+ // / Return the IdKind of the id at the specified position.
188
+ IdKind getIdKindAt (unsigned pos) const { return space.getIdKindAt (pos); };
189
+
145
190
// / The struct CountsSnapshot stores the count of each IdKind, and also of
146
191
// / each constraint type. getCounts() returns a CountsSnapshot object
147
192
// / describing the current state of the IntegerRelation. truncate() truncates
@@ -171,7 +216,7 @@ class IntegerRelation : public PresburgerSpace {
171
216
// / corresponding to the added identifiers are initialized to zero. Return the
172
217
// / absolute column position (i.e., not relative to the kind of identifier)
173
218
// / of the first added identifier.
174
- unsigned insertId (IdKind kind, unsigned pos, unsigned num = 1 ) override ;
219
+ virtual unsigned insertId (IdKind kind, unsigned pos, unsigned num = 1 );
175
220
176
221
// / Append `num` identifiers of the specified kind after the last identifier.
177
222
// / of that kind. Return the position of the first appended column relative to
@@ -193,7 +238,7 @@ class IntegerRelation : public PresburgerSpace {
193
238
// / within the specified range) from the system. The specified location is
194
239
// / relative to the first identifier of the specified kind.
195
240
void removeId (IdKind kind, unsigned pos);
196
- void removeIdRange (IdKind kind, unsigned idStart, unsigned idLimit) override ;
241
+ virtual void removeIdRange (IdKind kind, unsigned idStart, unsigned idLimit);
197
242
198
243
// / Removes the specified identifier from the system.
199
244
void removeId (unsigned pos);
@@ -432,6 +477,14 @@ class IntegerRelation : public PresburgerSpace {
432
477
// / match.
433
478
void mergeLocalIds (IntegerRelation &other);
434
479
480
+ // / Changes the partition between dimensions and symbols. Depending on the new
481
+ // / symbol count, either a chunk of dimensional identifiers immediately before
482
+ // / the split become symbols, or some of the symbols immediately after the
483
+ // / split become dimensions.
484
+ void setDimSymbolSeparation (unsigned newSymbolCount) {
485
+ space.setDimSymbolSeparation (newSymbolCount);
486
+ }
487
+
435
488
void print (raw_ostream &os) const ;
436
489
void dump () const ;
437
490
@@ -512,7 +565,10 @@ class IntegerRelation : public PresburgerSpace {
512
565
// / arrays as needed.
513
566
void removeIdRange (unsigned idStart, unsigned idLimit);
514
567
515
- using PresburgerSpace::truncateIdKind;
568
+ // / Truncate the ids of the specified kind to the specified number by dropping
569
+ // / some ids at the end. `num` must be less than the current number.
570
+ void truncateIdKind (IdKind kind, unsigned num);
571
+
516
572
// / Truncate the ids to the number in the space of the specified
517
573
// / CountsSnapshot.
518
574
void truncateIdKind (IdKind kind, const CountsSnapshot &counts);
@@ -529,6 +585,8 @@ class IntegerRelation : public PresburgerSpace {
529
585
// constraints. This is conservatively set low and can be raised if needed.
530
586
constexpr static unsigned kExplosionFactor = 32 ;
531
587
588
+ PresburgerSpace space;
589
+
532
590
// / Coefficients of affine equalities (in == 0 form).
533
591
Matrix equalities;
534
592
@@ -537,9 +595,10 @@ class IntegerRelation : public PresburgerSpace {
537
595
};
538
596
539
597
struct SymbolicLexMin ;
540
- // / An IntegerPolyhedron is a PresburgerSpace subject to affine
541
- // / constraints. Affine constraints can be inequalities or equalities in the
542
- // / form:
598
+
599
+ // / An IntegerPolyhedron represents the set of points from a PresburgerSpace
600
+ // / that satisfy a list of affine constraints. Affine constraints can be
601
+ // / inequalities or equalities in the form:
543
602
// /
544
603
// / Inequality: c_0*x_0 + c_1*x_1 + .... + c_{n-1}*x_{n-1} + c_n >= 0
545
604
// / Equality : c_0*x_0 + c_1*x_1 + .... + c_{n-1}*x_{n-1} + c_n == 0
0 commit comments