@@ -36,25 +36,20 @@ using namespace presburger;
36
36
namespace {
37
37
38
38
// See comments for SimpleAffineExprFlattener.
39
- // An AffineExprFlattener extends a SimpleAffineExprFlattener by recording
40
- // constraint information associated with mod's, floordiv's, and ceildiv's
41
- // in FlatLinearConstraints 'localVarCst'.
42
- struct AffineExprFlattener : public SimpleAffineExprFlattener {
43
- public:
39
+ // An AffineExprFlattenerWithLocalVars extends a SimpleAffineExprFlattener by
40
+ // recording constraint information associated with mod's, floordiv's, and
41
+ // ceildiv's in FlatLinearConstraints 'localVarCst'.
42
+ struct AffineExprFlattenerWithLocalVars : public SimpleAffineExprFlattener {
43
+ using SimpleAffineExprFlattener::SimpleAffineExprFlattener;
44
+
44
45
// Constraints connecting newly introduced local variables (for mod's and
45
46
// div's) to existing (dimensional and symbolic) ones. These are always
46
47
// inequalities.
47
48
IntegerPolyhedron localVarCst;
48
49
49
- AffineExprFlattener (unsigned nDims, unsigned nSymbols,
50
- bool addConservativeSemiAffineBounds = false )
50
+ AffineExprFlattenerWithLocalVars (unsigned nDims, unsigned nSymbols)
51
51
: SimpleAffineExprFlattener(nDims, nSymbols),
52
- localVarCst (PresburgerSpace::getSetSpace(nDims, nSymbols)),
53
- addConservativeSemiAffineBounds(addConservativeSemiAffineBounds) {}
54
-
55
- bool hasUnhandledSemiAffineExpressions () const {
56
- return unhandledSemiAffineExpressions;
57
- }
52
+ localVarCst (PresburgerSpace::getSetSpace(nDims, nSymbols)) {};
58
53
59
54
private:
60
55
// Add a local variable (needed to flatten a mod, floordiv, ceildiv expr).
@@ -70,30 +65,71 @@ struct AffineExprFlattener : public SimpleAffineExprFlattener {
70
65
localVarCst.addLocalFloorDiv (dividend, divisor);
71
66
}
72
67
73
- // Add a local identifier (needed to flatten a mod, floordiv, ceildiv, mul
74
- // expr) when the rhs is a symbolic expression. The local identifier added
75
- // may be a floordiv, ceildiv, mul or mod of a pure affine/semi-affine
76
- // function of other identifiers, coefficients of which are specified in the
77
- // lhs of the mod, floordiv, ceildiv or mul expression and with respect to a
78
- // symbolic rhs expression. `localExpr` is the simplified tree expression
79
- // (AffineExpr) corresponding to the quantifier.
80
- void addLocalIdSemiAffine (AffineExpr localExpr, ArrayRef<int64_t > lhs,
81
- ArrayRef<int64_t > rhs) override {
82
- SimpleAffineExprFlattener::addLocalIdSemiAffine (localExpr, lhs, rhs);
83
- if (!addConservativeSemiAffineBounds) {
84
- unhandledSemiAffineExpressions = true ;
85
- return ;
86
- }
68
+ // Semi-affine expressions are not supported by all flatteners.
69
+ LogicalResult addLocalIdSemiAffine (ArrayRef<int64_t > lhs,
70
+ ArrayRef<int64_t > rhs,
71
+ AffineExpr localExpr) override = 0;
72
+ };
73
+
74
+ // An AffineExprFlattener is an AffineExprFlattenerWithLocalVars that explicitly
75
+ // disallows semi-affine expressions. Flattening will fail if a semi-affine
76
+ // expression is encountered.
77
+ struct AffineExprFlattener : public AffineExprFlattenerWithLocalVars {
78
+ using AffineExprFlattenerWithLocalVars::AffineExprFlattenerWithLocalVars;
79
+
80
+ LogicalResult addLocalIdSemiAffine (ArrayRef<int64_t > lhs,
81
+ ArrayRef<int64_t > rhs,
82
+ AffineExpr localExpr) override {
83
+ // AffineExprFlattener does not support semi-affine expressions.
84
+ return failure ();
85
+ }
86
+ };
87
+
88
+ // A SemiAffineExprFlattener is an AffineExprFlattenerWithLocalVars that adds
89
+ // conservative bounds for semi-affine expressions (given assumptions hold). If
90
+ // the assumptions required to add the semi-affine bounds are found not to hold
91
+ // the final constraints set will be empty/inconsistent. If the assumptions are
92
+ // never contradicted the final bounds still only will be correct if the
93
+ // assumptions hold.
94
+ struct SemiAffineExprFlattener : public AffineExprFlattenerWithLocalVars {
95
+ using AffineExprFlattenerWithLocalVars::AffineExprFlattenerWithLocalVars;
96
+
97
+ LogicalResult addLocalIdSemiAffine (ArrayRef<int64_t > lhs,
98
+ ArrayRef<int64_t > rhs,
99
+ AffineExpr localExpr) override {
100
+ auto result =
101
+ SimpleAffineExprFlattener::addLocalIdSemiAffine (lhs, rhs, localExpr);
102
+ assert (succeeded (result) &&
103
+ " unexpected failure in SimpleAffineExprFlattener" );
104
+ (void )result;
105
+
87
106
if (localExpr.getKind () == AffineExprKind::Mod) {
88
- localVarCst.addLocalModConservativeBounds (lhs, rhs);
89
- return ;
107
+ localVarCst.appendVar (VarKind::Local);
108
+ // Add a conservative bound for `mod` assuming the rhs is > 0.
109
+
110
+ // Note: If the rhs is later found to be < 0 the following two constraints
111
+ // will contradict each other (and lead to the final constraints set
112
+ // becoming empty). If the sign of the rhs is never specified the bound
113
+ // will assume it is positive.
114
+
115
+ // Upper bound: rhs - (lhs % rhs) - 1 >= 0 i.e. lhs % rhs < rhs
116
+ // This only holds if the rhs is > 0.
117
+ SmallVector<int64_t , 8 > resultUpperBound (rhs);
118
+ resultUpperBound.insert (resultUpperBound.end () - 1 , -1 );
119
+ --resultUpperBound.back ();
120
+ localVarCst.addInequality (resultUpperBound);
121
+
122
+ // Lower bound: lhs % rhs >= 0 (always holds)
123
+ SmallVector<int64_t , 8 > resultLowerBound (rhs.size ());
124
+ resultLowerBound.insert (resultLowerBound.end () - 1 , 1 );
125
+ localVarCst.addInequality (resultLowerBound);
126
+
127
+ return success ();
90
128
}
129
+
91
130
// TODO: Support other semi-affine expressions.
92
- unhandledSemiAffineExpressions = true ;
131
+ return failure () ;
93
132
}
94
-
95
- bool addConservativeSemiAffineBounds = false ;
96
- bool unhandledSemiAffineExpressions = false ;
97
133
};
98
134
99
135
} // namespace
@@ -114,27 +150,34 @@ getFlattenedAffineExprs(ArrayRef<AffineExpr> exprs, unsigned numDims,
114
150
return success ();
115
151
}
116
152
117
- AffineExprFlattener flattener (numDims, numSymbols,
118
- addConservativeSemiAffineBounds);
119
- // Use the same flattener to simplify each expression successively. This way
120
- // local variables / expressions are shared.
121
- for (auto expr : exprs) {
122
- auto flattenResult = flattener.walkPostOrder (expr);
123
- if (failed (flattenResult))
124
- return failure ();
125
- if (flattener.hasUnhandledSemiAffineExpressions ())
126
- return failure ();
127
- }
153
+ auto flattenExprs =
154
+ [&](AffineExprFlattenerWithLocalVars &flattener) -> LogicalResult {
155
+ // Use the same flattener to simplify each expression successively. This way
156
+ // local variables / expressions are shared.
157
+ for (auto expr : exprs) {
158
+ auto flattenResult = flattener.walkPostOrder (expr);
159
+ if (failed (flattenResult))
160
+ return failure ();
161
+ }
162
+
163
+ assert (flattener.operandExprStack .size () == exprs.size ());
164
+ flattenedExprs->clear ();
165
+ flattenedExprs->assign (flattener.operandExprStack .begin (),
166
+ flattener.operandExprStack .end ());
128
167
129
- assert (flattener.operandExprStack .size () == exprs.size ());
130
- flattenedExprs->clear ();
131
- flattenedExprs->assign (flattener.operandExprStack .begin (),
132
- flattener.operandExprStack .end ());
168
+ if (localVarCst)
169
+ localVarCst->clearAndCopyFrom (flattener.localVarCst );
170
+
171
+ return success ();
172
+ };
133
173
134
- if (localVarCst)
135
- localVarCst->clearAndCopyFrom (flattener.localVarCst );
174
+ if (addConservativeSemiAffineBounds) {
175
+ SemiAffineExprFlattener flattener (numDims, numSymbols);
176
+ return flattenExprs (flattener);
177
+ }
136
178
137
- return success ();
179
+ AffineExprFlattener flattener (numDims, numSymbols);
180
+ return flattenExprs (flattener);
138
181
}
139
182
140
183
// Flattens 'expr' into 'flattenedExpr'. Returns failure if 'expr' was unable to
0 commit comments