12 #include "llvm/ADT/STLExtras.h"
13 #include "llvm/ADT/ScopeExit.h"
14 #include "llvm/ADT/SmallBitVector.h"
18 using namespace presburger;
21 : space(disjunct.getSpaceWithoutLocals()) {
29 disjunct.setSpaceExceptLocals(
space);
41 assert(index <
disjuncts.size() &&
"index out of bounds!");
128 "idx out of bounds!");
136 return llvm::to_vector<8>(eqCoeffs);
147 result.
unionInPlace(disjunct.computeReprWithOnlyDivLocals());
206 unsigned simplexSnapshot;
216 std::optional<unsigned> lastIneqProcessed;
227 level = frames.size();
231 if (level > frames.size()) {
269 "Subtraction is not supported when a representation of the local "
270 "variables of the subtrahend cannot be found!");
273 unsigned lb = repr[i].repr.inequalityPair.lowerBoundIdx;
274 unsigned ub = repr[i].repr.inequalityPair.upperBoundIdx;
280 "Upper and lower bounds must be different inequalities!");
281 canIgnoreIneq[lb] =
true;
282 canIgnoreIneq[ub] =
true;
285 "ReprKind isn't inequality so should be equality");
312 unsigned numLocalsAdded =
316 unsigned snapshotBeforeIntersect = simplex.
getSnapshot();
330 frames.push_back(Frame{initialSnapshot, initBCounts, sI,
338 unsigned totalNewSimplexInequalities =
354 for (
unsigned j = 0;
j < totalNewSimplexInequalities;
j++)
356 simplex.
rollback(snapshotBeforeIntersect);
359 ineqsToProcess.reserve(totalNewSimplexInequalities);
360 for (
unsigned i = 0; i < totalNewSimplexInequalities; ++i)
361 if (!canIgnoreIneq[i])
362 ineqsToProcess.push_back(i);
364 if (ineqsToProcess.empty()) {
366 level = frames.size();
372 frames.push_back(Frame{simplexSnapshot, bCounts, sI, ineqsToProcess,
381 if (level == frames.size()) {
382 Frame &frame = frames.back();
383 if (frame.lastIneqProcessed) {
391 simplex.
rollback(frame.simplexSnapshot);
399 if (frame.ineqsToProcess.empty()) {
402 level = frames.size();
410 unsigned idx = frame.ineqsToProcess.back();
416 frame.ineqsToProcess.pop_back();
417 frame.lastIneqProcessed = idx;
467 disjunct.findIntegerSample()) {
468 sample = std::move(*opt);
481 std::optional<MPInt> volume = disjunct.computeVolume();
534 void addCoalescedDisjunct(
unsigned i,
unsigned j,
563 void eraseDisjunct(
unsigned i);
581 for (
unsigned i = 0; i < disjuncts.size();) {
582 disjuncts[i].removeRedundantConstraints();
585 disjuncts[i] = disjuncts[disjuncts.size() - 1];
586 disjuncts.pop_back();
590 simplices.push_back(simp);
600 for (
unsigned i = 0; i < disjuncts.size();) {
605 for (
unsigned j = 0, e = disjuncts.size();
j < e; ++
j) {
607 redundantIneqsA.clear();
608 redundantIneqsB.clear();
609 cuttingIneqsA.clear();
610 cuttingIneqsB.clear();
627 for (
unsigned i = 0, e = disjuncts.size(); i < e; ++i)
644 void SetCoalescer::addCoalescedDisjunct(
unsigned i,
unsigned j,
646 assert(i !=
j &&
"The indices must refer to different disjuncts");
647 unsigned n = disjuncts.size();
652 disjuncts[i] = disjuncts[n - 2];
653 disjuncts.pop_back();
654 disjuncts[n - 2] = disjunct;
655 disjuncts[n - 2].removeRedundantConstraints();
657 simplices[i] = simplices[n - 2];
658 simplices.pop_back();
659 simplices[n - 2] =
Simplex(disjuncts[n - 2]);
667 disjuncts[i] = disjuncts[n - 1];
668 disjuncts[
j] = disjuncts[n - 2];
669 disjuncts.pop_back();
670 disjuncts[n - 2] = disjunct;
671 disjuncts[n - 2].removeRedundantConstraints();
673 simplices[i] = simplices[n - 1];
674 simplices[
j] = simplices[n - 2];
675 simplices.pop_back();
676 simplices[n - 2] =
Simplex(disjuncts[n - 2]);
696 LogicalResult SetCoalescer::coalescePairCutCase(
unsigned i,
unsigned j) {
702 return !isFacetContained(curr, simp);
708 newSet.addInequality(curr);
711 newSet.addInequality(curr);
713 addCoalescedDisjunct(i,
j, newSet);
720 if (type == Simplex::IneqType::Redundant)
721 redundantIneqsB.push_back(ineq);
722 else if (type == Simplex::IneqType::Cut)
723 cuttingIneqsB.push_back(ineq);
730 if (typeInequality(eq, simp).
failed())
734 if (typeInequality(inv, simp).
failed())
739 void SetCoalescer::eraseDisjunct(
unsigned i) {
740 assert(simplices.size() == disjuncts.size() &&
741 "simplices and disjuncts must be equally as long");
742 disjuncts[i] = disjuncts.back();
743 disjuncts.pop_back();
744 simplices[i] = simplices.back();
745 simplices.pop_back();
748 LogicalResult SetCoalescer::coalescePair(
unsigned i,
unsigned j) {
773 std::swap(redundantIneqsA, redundantIneqsB);
774 std::swap(cuttingIneqsA, cuttingIneqsB);
786 if (cuttingIneqsA.empty()) {
796 std::swap(redundantIneqsA, redundantIneqsB);
797 std::swap(cuttingIneqsA, cuttingIneqsB);
801 if (cuttingIneqsA.empty()) {
static SmallVector< MPInt, 8 > getIneqCoeffsFromIdx(const IntegerRelation &rel, unsigned idx)
Return the coefficients of the ineq in rel specified by idx.
static PresburgerRelation getSetDifference(IntegerRelation b, const PresburgerRelation &s)
Return the set difference b \ s.
Class storing division representation of local variables of a constraint system.
MPInt & getDenom(unsigned i)
MutableArrayRef< MPInt > getDividend(unsigned i)
An IntegerPolyhedron represents the set of points from a PresburgerSpace that satisfy a list of affin...
static IntegerPolyhedron getUniverse(const PresburgerSpace &space)
Return a system with no constraints, i.e., one which is satisfied by all points.
An IntegerRelation represents the set of points from a PresburgerSpace that satisfy a list of affine ...
ArrayRef< MPInt > getEquality(unsigned idx) const
PresburgerSpace getSpaceWithoutLocals() const
Returns a copy of the space without locals.
void addInequality(ArrayRef< MPInt > inEq)
Adds an inequality (>= 0) from the coefficients specified in inEq.
void truncate(const CountsSnapshot &counts)
CountsSnapshot getCounts() const
bool isEmptyByGCDTest() const
Runs the GCD test on all equality constraints.
void removeDuplicateDivs()
void print(raw_ostream &os) const
bool isIntegerEmpty() const
Returns true if the set of constraints is found to have no solution, false if a solution exists.
IntegerRelation intersect(IntegerRelation other) const
Return the intersection of the two relations.
ArrayRef< MPInt > getInequality(unsigned idx) const
std::optional< SmallVector< MPInt, 8 > > containsPointNoLocal(ArrayRef< MPInt > point) const
Given the values of non-local vars, return a satisfying assignment to the local if one exists,...
static IntegerRelation getUniverse(const PresburgerSpace &space)
Return a system with no constraints, i.e., one which is satisfied by all points.
unsigned getNumLocalVars() const
bool isEmpty() const
Checks for emptiness by performing variable elimination on all variables, running the GCD test on eac...
DivisionRepr getLocalReprs(std::vector< MaybeLocalRepr > *repr=nullptr) const
Returns a DivisonRepr representing the division representation of local variables in the constraint s...
bool hasOnlyDivLocals() const
Check whether all local ids have a division representation.
unsigned mergeLocalVars(IntegerRelation &other)
Adds additional local vars to the sets such that they both have the union of the local vars in each s...
unsigned getNumInequalities() const
const PresburgerSpace & getSpace() const
Returns a reference to the underlying space.
unsigned getNumEqualities() const
unsigned getVarKindOffset(VarKind kind) const
Return the index at which the specified kind of vars starts.
This class provides support for multi-precision arithmetic.
A PresburgerRelation represents a union of IntegerRelations that live in the same PresburgerSpace wit...
unsigned getNumSymbolVars() const
bool containsPoint(ArrayRef< MPInt > point) const
Return true if the set contains the given point, and false otherwise.
void setSpace(const PresburgerSpace &oSpace)
Set the space to oSpace.
PresburgerRelation intersect(const PresburgerRelation &set) const
Return the intersection of this set and the given set.
bool hasOnlyDivLocals() const
Check whether all local ids in all disjuncts have a div representation.
PresburgerRelation subtract(const PresburgerRelation &set) const
Return the set difference of this set and the given set, i.e., return this \ set.
friend class SetCoalescer
PresburgerRelation(const IntegerRelation &disjunct)
PresburgerRelation computeReprWithOnlyDivLocals() const
Compute an equivalent representation of the same relation, such that all local ids in all disjuncts h...
bool isSubsetOf(const PresburgerRelation &set) const
Return true if this set is a subset of the given set, and false otherwise.
bool isIntegerEmpty() const
Return true if all the sets in the union are known to be integer empty false otherwise.
void unionInPlace(const IntegerRelation &disjunct)
Mutate this set, turning it into the union of this set and the given disjunct.
std::optional< MPInt > computeVolume() const
Compute an overapproximation of the number of integer points in the disjunct.
bool isEqual(const PresburgerRelation &set) const
Return true if this set is equal to the given set, and false otherwise.
static PresburgerRelation getEmpty(const PresburgerSpace &space)
Return an empty set of the specified type that contains no points.
unsigned getNumDisjuncts() const
Return the number of disjuncts in the union.
PresburgerRelation coalesce() const
Simplifies the representation of a PresburgerRelation.
static PresburgerRelation getUniverse(const PresburgerSpace &space)
Return a universe set of the specified type that contains all points.
const IntegerRelation & getDisjunct(unsigned index) const
Return the disjunct at the specified index.
ArrayRef< IntegerRelation > getAllDisjuncts() const
Return a reference to the list of disjuncts.
SmallVector< IntegerRelation, 2 > disjuncts
The list of disjuncts that this set is the union of.
const PresburgerSpace & getSpace() const
void print(raw_ostream &os) const
Print the set's internal state.
PresburgerRelation unionSet(const PresburgerRelation &set) const
Return the union of this set and the given set.
bool findIntegerSample(SmallVectorImpl< MPInt > &sample)
Find an integer sample from the given set.
PresburgerRelation complement() const
Return the complement of this set.
PresburgerSet intersect(const PresburgerRelation &set) const
PresburgerSet(const IntegerPolyhedron &disjunct)
Create a set from a relation.
PresburgerSet unionSet(const PresburgerRelation &set) const
These operations are the same as the ones in PresburgeRelation, they just forward the arguement and r...
PresburgerSet subtract(const PresburgerRelation &set) const
static PresburgerSet getEmpty(const PresburgerSpace &space)
Return an empty set of the specified type that contains no points.
static PresburgerSet getUniverse(const PresburgerSpace &space)
Return a universe set of the specified type that contains all points.
PresburgerSet coalesce() const
PresburgerSet complement() const
PresburgerSpace is the space of all possible values of a tuple of integer valued variables/variables.
unsigned getNumLocalVars() const
bool isCompatible(const PresburgerSpace &other) const
Returns true if both the spaces are compatible i.e.
bool isEmpty() const
Returns true if the tableau is empty (has conflicting constraints), false otherwise.
void appendVariable(unsigned count=1)
Add new variables to the end of the list of variables.
void intersectIntegerRelation(const IntegerRelation &rel)
Add all the constraints from the given IntegerRelation.
unsigned getSnapshot() const
Get a snapshot of the current state.
void addEquality(ArrayRef< MPInt > coeffs)
Add an equality to the tableau.
void rollback(unsigned snapshot)
Rollback to a snapshot. This invalidates all later snapshots.
unsigned getNumConstraints() const
Returns the number of constraints in the tableau.
Takes a snapshot of the simplex state on construction and rolls back to the snapshot on destruction.
The Simplex class uses the Normal pivot rule and supports integer emptiness checks as well as detecti...
bool isMarkedRedundant(unsigned constraintIndex) const
Returns whether the specified constraint has been marked as redundant.
void addInequality(ArrayRef< MPInt > coeffs) final
Add an inequality to the tableau.
bool isRedundantInequality(ArrayRef< MPInt > coeffs)
Check if the specified inequality already holds in the polytope.
void detectRedundant(unsigned offset, unsigned count)
Finds a subset of constraints that is redundant, i.e., such that the set of solutions does not change...
IneqType findIneqType(ArrayRef< MPInt > coeffs)
Returns the type of the inequality with coefficients coeffs.
The SetCoalescer class contains all functionality concerning the coalesce heuristic.
SetCoalescer(const PresburgerRelation &s)
Construct a SetCoalescer from a PresburgerSet.
PresburgerRelation coalesce()
Simplifies the representation of a PresburgerSet.
SmallVector< MPInt, 8 > getDivLowerBound(ArrayRef< MPInt > dividend, const MPInt &divisor, unsigned localVarIdx)
SmallVector< MPInt, 8 > getDivUpperBound(ArrayRef< MPInt > dividend, const MPInt &divisor, unsigned localVarIdx)
If q is defined to be equal to expr floordiv d, this equivalent to saying that q is an integer and q ...
SmallVector< MPInt, 8 > getNegatedCoeffs(ArrayRef< MPInt > coeffs)
Return coeffs with all the elements negated.
SmallVector< MPInt, 8 > getComplementIneq(ArrayRef< MPInt > ineq)
Return the complement of the given inequality.
This header declares functions that assit transformations in the MemRef dialect.
LogicalResult failure(bool isFailure=true)
Utility function to generate a LogicalResult.
bool succeeded(LogicalResult result)
Utility function that returns true if the provided LogicalResult corresponds to a success value.
LogicalResult success(bool isSuccess=true)
Utility function to generate a LogicalResult.
bool failed(LogicalResult result)
Utility function that returns true if the provided LogicalResult corresponds to a failure value.
This class represents an efficient way to signal success or failure.
bool failed() const
Returns true if the provided LogicalResult corresponds to a failure value.
The struct CountsSnapshot stores the count of each VarKind, and also of each constraint type.
const PresburgerSpace & getSpace() const
Eliminates variable at the specified position using Fourier-Motzkin variable elimination.