/// Checks if two constraint systems are in the same space, i.e., if they are
/// associated with the same set of identifiers, appearing in the same order.
-static bool areIdsAligned(const FlatAffineConstraints &A,
- const FlatAffineConstraints &B) {
- return A.getNumDimIds() == B.getNumDimIds() &&
- A.getNumSymbolIds() == B.getNumSymbolIds() &&
- A.getNumIds() == B.getNumIds() && A.getIds().equals(B.getIds());
+static bool areIdsAligned(const FlatAffineConstraints &a,
+ const FlatAffineConstraints &b) {
+ return a.getNumDimIds() == b.getNumDimIds() &&
+ a.getNumSymbolIds() == b.getNumSymbolIds() &&
+ a.getNumIds() == b.getNumIds() && a.getIds().equals(b.getIds());
}
/// Calls areIdsAligned to check if two constraint systems have the same set
// Eg: Input: A has ((%i %j) [%M %N]) and B has (%k, %j) [%P, %N, %M])
// Output: both A, B have (%i, %j, %k) [%M, %N, %P]
//
-static void mergeAndAlignIds(unsigned offset, FlatAffineConstraints *A,
- FlatAffineConstraints *B) {
- assert(offset <= A->getNumDimIds() && offset <= B->getNumDimIds());
+static void mergeAndAlignIds(unsigned offset, FlatAffineConstraints *a,
+ FlatAffineConstraints *b) {
+ assert(offset <= a->getNumDimIds() && offset <= b->getNumDimIds());
// A merge/align isn't meaningful if a cst's ids aren't distinct.
- assert(areIdsUnique(*A) && "A's id values aren't unique");
- assert(areIdsUnique(*B) && "B's id values aren't unique");
+ assert(areIdsUnique(*a) && "A's id values aren't unique");
+ assert(areIdsUnique(*b) && "B's id values aren't unique");
- assert(std::all_of(A->getIds().begin() + offset,
- A->getIds().begin() + A->getNumDimAndSymbolIds(),
+ assert(std::all_of(a->getIds().begin() + offset,
+ a->getIds().begin() + a->getNumDimAndSymbolIds(),
[](Optional<Value> id) { return id.hasValue(); }));
- assert(std::all_of(B->getIds().begin() + offset,
- B->getIds().begin() + B->getNumDimAndSymbolIds(),
+ assert(std::all_of(b->getIds().begin() + offset,
+ b->getIds().begin() + b->getNumDimAndSymbolIds(),
[](Optional<Value> id) { return id.hasValue(); }));
// Place local id's of A after local id's of B.
- for (unsigned l = 0, e = A->getNumLocalIds(); l < e; l++) {
- B->addLocalId(0);
+ for (unsigned l = 0, e = a->getNumLocalIds(); l < e; l++) {
+ b->addLocalId(0);
}
- for (unsigned t = 0, e = B->getNumLocalIds() - A->getNumLocalIds(); t < e;
+ for (unsigned t = 0, e = b->getNumLocalIds() - a->getNumLocalIds(); t < e;
t++) {
- A->addLocalId(A->getNumLocalIds());
+ a->addLocalId(a->getNumLocalIds());
}
SmallVector<Value, 4> aDimValues, aSymValues;
- A->getIdValues(offset, A->getNumDimIds(), &aDimValues);
- A->getIdValues(A->getNumDimIds(), A->getNumDimAndSymbolIds(), &aSymValues);
+ a->getIdValues(offset, a->getNumDimIds(), &aDimValues);
+ a->getIdValues(a->getNumDimIds(), a->getNumDimAndSymbolIds(), &aSymValues);
{
// Merge dims from A into B.
unsigned d = offset;
for (auto aDimValue : aDimValues) {
unsigned loc;
- if (B->findId(aDimValue, &loc)) {
+ if (b->findId(aDimValue, &loc)) {
assert(loc >= offset && "A's dim appears in B's aligned range");
- assert(loc < B->getNumDimIds() &&
+ assert(loc < b->getNumDimIds() &&
"A's dim appears in B's non-dim position");
- B->swapId(d, loc);
+ b->swapId(d, loc);
} else {
- B->addDimId(d);
- B->setIdValue(d, aDimValue);
+ b->addDimId(d);
+ b->setIdValue(d, aDimValue);
}
d++;
}
// Dimensions that are in B, but not in A, are added at the end.
- for (unsigned t = A->getNumDimIds(), e = B->getNumDimIds(); t < e; t++) {
- A->addDimId(A->getNumDimIds());
- A->setIdValue(A->getNumDimIds() - 1, B->getIdValue(t));
+ for (unsigned t = a->getNumDimIds(), e = b->getNumDimIds(); t < e; t++) {
+ a->addDimId(a->getNumDimIds());
+ a->setIdValue(a->getNumDimIds() - 1, b->getIdValue(t));
}
}
{
// Merge symbols: merge A's symbols into B first.
- unsigned s = B->getNumDimIds();
+ unsigned s = b->getNumDimIds();
for (auto aSymValue : aSymValues) {
unsigned loc;
- if (B->findId(aSymValue, &loc)) {
- assert(loc >= B->getNumDimIds() && loc < B->getNumDimAndSymbolIds() &&
+ if (b->findId(aSymValue, &loc)) {
+ assert(loc >= b->getNumDimIds() && loc < b->getNumDimAndSymbolIds() &&
"A's symbol appears in B's non-symbol position");
- B->swapId(s, loc);
+ b->swapId(s, loc);
} else {
- B->addSymbolId(s - B->getNumDimIds());
- B->setIdValue(s, aSymValue);
+ b->addSymbolId(s - b->getNumDimIds());
+ b->setIdValue(s, aSymValue);
}
s++;
}
// Symbols that are in B, but not in A, are added at the end.
- for (unsigned t = A->getNumDimAndSymbolIds(),
- e = B->getNumDimAndSymbolIds();
+ for (unsigned t = a->getNumDimAndSymbolIds(),
+ e = b->getNumDimAndSymbolIds();
t < e; t++) {
- A->addSymbolId(A->getNumSymbolIds());
- A->setIdValue(A->getNumDimAndSymbolIds() - 1, B->getIdValue(t));
+ a->addSymbolId(a->getNumSymbolIds());
+ a->setIdValue(a->getNumDimAndSymbolIds() - 1, b->getIdValue(t));
}
}
- assert(areIdsAligned(*A, *B) && "IDs expected to be aligned");
+ assert(areIdsAligned(*a, *b) && "IDs expected to be aligned");
}
// Call 'mergeAndAlignIds' to align constraint systems of 'this' and 'other'.
// Eliminate the remaining using FM.
for (unsigned i = 0, e = tmpCst.getNumIds(); i < e; i++) {
- tmpCst.FourierMotzkinEliminate(
+ tmpCst.fourierMotzkinEliminate(
getBestIdToEliminate(tmpCst, 0, tmpCst.getNumIds()));
// Check for a constraint explosion. This rarely happens in practice, but
// this check exists as a safeguard against improperly constructed
// Example on how this affects practical cases: consider the scenario:
// 64*i >= 100, j = 64*i; without a tightening, elimination of i would yield
// j >= 100 instead of the tighter (exact) j >= 128.
-void FlatAffineConstraints::GCDTightenInequalities() {
+void FlatAffineConstraints::gcdTightenInequalities() {
unsigned numCols = getNumCols();
for (unsigned i = 0, e = getNumInequalities(); i < e; ++i) {
uint64_t gcd = std::abs(atIneq(i, 0));
if (posStart >= posLimit)
return 0;
- GCDTightenInequalities();
+ gcdTightenInequalities();
unsigned pivotCol = 0;
for (pivotCol = posStart; pivotCol < posLimit; ++pivotCol) {
normalizeConstraintByGCD</*isEq=*/false>(this, i);
}
removeEquality(pivotRow);
- GCDTightenInequalities();
+ gcdTightenInequalities();
}
// Update position limit based on number eliminated.
posLimit = pivotCol;
// A more complex check to eliminate redundant inequalities and equalities. Uses
// Simplex to check if a constraint is redundant.
void FlatAffineConstraints::removeRedundantConstraints() {
- // First, we run GCDTightenInequalities. This allows us to catch some
+ // First, we run gcdTightenInequalities. This allows us to catch some
// constraints which are not redundant when considering rational solutions
// but are redundant in terms of integer solutions.
- GCDTightenInequalities();
+ gcdTightenInequalities();
Simplex simplex(*this);
simplex.detectRedundant();
// Uses a DenseSet to hash and detect duplicates followed by a linear scan to
// remove duplicates in place.
void FlatAffineConstraints::removeTrivialRedundancy() {
- GCDTightenInequalities();
+ gcdTightenInequalities();
normalizeConstraintsByGCD();
// A map used to detect redundancy stemming from constraints that only differ
/// darkShadow = false, isResultIntegerExact = nullptr are default values.
// TODO: a slight modification to yield dark shadow version of FM (tightened),
// which can prove the existence of a solution if there is one.
-void FlatAffineConstraints::FourierMotzkinEliminate(
+void FlatAffineConstraints::fourierMotzkinEliminate(
unsigned pos, bool darkShadow, bool *isResultIntegerExact) {
LLVM_DEBUG(llvm::dbgs() << "FM input (eliminate pos " << pos << "):\n");
LLVM_DEBUG(dump());
}
// A fast linear time tightening.
- GCDTightenInequalities();
+ gcdTightenInequalities();
// Check if the identifier appears at all in any of the inequalities.
unsigned r, e;
// GCD tightening and normalization allows detection of more trivially
// redundant constraints.
- newFac.GCDTightenInequalities();
+ newFac.gcdTightenInequalities();
newFac.normalizeConstraintsByGCD();
newFac.removeTrivialRedundancy();
clearAndCopyFrom(newFac);
// Eliminate the remaining using Fourier-Motzkin.
for (unsigned i = 0; i < num - numGaussianEliminated; i++) {
unsigned numToEliminate = num - numGaussianEliminated - i;
- FourierMotzkinEliminate(
+ fourierMotzkinEliminate(
getBestIdToEliminate(*this, pos, pos + numToEliminate));
}
// Fast/trivial simplifications.
- GCDTightenInequalities();
+ gcdTightenInequalities();
// Normalize constraints after tightening since the latter impacts this, but
// not the other way round.
normalizeConstraintsByGCD();
bool ret = findId(id, &pos);
assert(ret);
(void)ret;
- FourierMotzkinEliminate(pos);
+ fourierMotzkinEliminate(pos);
}
void FlatAffineConstraints::clearConstraints() {
} // namespace
// Returns constraints that are common to both A & B.
-static void getCommonConstraints(const FlatAffineConstraints &A,
- const FlatAffineConstraints &B,
- FlatAffineConstraints &C) {
- C.reset(A.getNumDimIds(), A.getNumSymbolIds(), A.getNumLocalIds());
- // A naive O(n^2) check should be enough here given the input sizes.
- for (unsigned r = 0, e = A.getNumInequalities(); r < e; ++r) {
- for (unsigned s = 0, f = B.getNumInequalities(); s < f; ++s) {
- if (A.getInequality(r) == B.getInequality(s)) {
- C.addInequality(A.getInequality(r));
+static void getCommonConstraints(const FlatAffineConstraints &a,
+ const FlatAffineConstraints &b,
+ FlatAffineConstraints &c) {
+ c.reset(a.getNumDimIds(), a.getNumSymbolIds(), a.getNumLocalIds());
+ // a naive O(n^2) check should be enough here given the input sizes.
+ for (unsigned r = 0, e = a.getNumInequalities(); r < e; ++r) {
+ for (unsigned s = 0, f = b.getNumInequalities(); s < f; ++s) {
+ if (a.getInequality(r) == b.getInequality(s)) {
+ c.addInequality(a.getInequality(r));
break;
}
}
}
- for (unsigned r = 0, e = A.getNumEqualities(); r < e; ++r) {
- for (unsigned s = 0, f = B.getNumEqualities(); s < f; ++s) {
- if (A.getEquality(r) == B.getEquality(s)) {
- C.addEquality(A.getEquality(r));
+ for (unsigned r = 0, e = a.getNumEqualities(); r < e; ++r) {
+ for (unsigned s = 0, f = b.getNumEqualities(); s < f; ++s) {
+ if (a.getEquality(r) == b.getEquality(s)) {
+ c.addEquality(a.getEquality(r));
break;
}
}