15 #include "llvm/ADT/STLExtras.h"
16 #include "llvm/ADT/ScopeExit.h"
17 #include "llvm/ADT/SmallBitVector.h"
21 using namespace presburger;
24 : space(disjunct.getSpaceWithoutLocals()) {
32 disjunct.setSpaceExceptLocals(
space);
38 cs.insertVar(kind, pos, num);
46 "srcKind/dstKind cannot be local");
47 assert(srcKind != dstKind &&
"cannot convert variables to the same kind");
49 "invalid range for source variables");
51 "invalid position for destination variables");
56 disjunct.convertVarKind(srcKind, srcPos, srcPos + num, dstKind, dstPos);
68 assert(index <
disjuncts.size() &&
"index out of bounds!");
167 "Range of `this` must be compatible with range of `set`");
177 "Domain of `this` must be compatible with range of `set`");
208 assert(
getSpace().getRangeSpace().isCompatible(
210 "Range of `this` should be compatible with domain of `rel`");
227 assert(
getSpace().getDomainSpace().isCompatible(
229 "Domain of `this` should be compatible with domain of `rel`");
248 s = cs.findSymbolicIntegerLexMin();
251 s = cs.findSymbolicIntegerLexMax();
284 "idx out of bounds!");
292 return llvm::to_vector<8>(eqCoeffs);
303 result.
unionInPlace(disjunct.computeReprWithOnlyDivLocals());
362 unsigned simplexSnapshot;
372 std::optional<unsigned> lastIneqProcessed;
383 level = frames.size();
387 if (level > frames.size()) {
425 "Subtraction is not supported when a representation of the local "
426 "variables of the subtrahend cannot be found!");
429 unsigned lb = repr[i].repr.inequalityPair.lowerBoundIdx;
430 unsigned ub = repr[i].repr.inequalityPair.upperBoundIdx;
436 "Upper and lower bounds must be different inequalities!");
437 canIgnoreIneq[lb] =
true;
438 canIgnoreIneq[ub] =
true;
441 "ReprKind isn't inequality so should be equality");
468 unsigned numLocalsAdded =
472 unsigned snapshotBeforeIntersect = simplex.
getSnapshot();
486 frames.push_back(Frame{initialSnapshot, initBCounts, sI,
494 unsigned totalNewSimplexInequalities =
510 for (
unsigned j = 0;
j < totalNewSimplexInequalities;
j++)
512 simplex.
rollback(snapshotBeforeIntersect);
515 ineqsToProcess.reserve(totalNewSimplexInequalities);
516 for (
unsigned i = 0; i < totalNewSimplexInequalities; ++i)
517 if (!canIgnoreIneq[i])
518 ineqsToProcess.push_back(i);
520 if (ineqsToProcess.empty()) {
522 level = frames.size();
528 frames.push_back(Frame{simplexSnapshot, bCounts, sI, ineqsToProcess,
537 if (level == frames.size()) {
538 Frame &frame = frames.back();
539 if (frame.lastIneqProcessed) {
547 simplex.
rollback(frame.simplexSnapshot);
555 if (frame.ineqsToProcess.empty()) {
558 level = frames.size();
566 unsigned idx = frame.ineqsToProcess.back();
572 frame.ineqsToProcess.pop_back();
573 frame.lastIneqProcessed = idx;
640 if (disjunct.getNumConstraints() == 0)
666 disjunct.findIntegerSample()) {
667 sample = std::move(*opt);
680 std::optional<MPInt> volume = disjunct.computeVolume();
733 void addCoalescedDisjunct(
unsigned i,
unsigned j,
762 void eraseDisjunct(
unsigned i);
780 for (
unsigned i = 0; i < disjuncts.size();) {
781 disjuncts[i].removeRedundantConstraints();
784 disjuncts[i] = disjuncts[disjuncts.size() - 1];
785 disjuncts.pop_back();
789 simplices.push_back(simp);
799 for (
unsigned i = 0; i < disjuncts.size();) {
804 for (
unsigned j = 0, e = disjuncts.size();
j < e; ++
j) {
806 redundantIneqsA.clear();
807 redundantIneqsB.clear();
808 cuttingIneqsA.clear();
809 cuttingIneqsB.clear();
826 for (
unsigned i = 0, e = disjuncts.size(); i < e; ++i)
843 void SetCoalescer::addCoalescedDisjunct(
unsigned i,
unsigned j,
845 assert(i !=
j &&
"The indices must refer to different disjuncts");
846 unsigned n = disjuncts.size();
851 disjuncts[i] = disjuncts[n - 2];
852 disjuncts.pop_back();
853 disjuncts[n - 2] = disjunct;
854 disjuncts[n - 2].removeRedundantConstraints();
856 simplices[i] = simplices[n - 2];
857 simplices.pop_back();
858 simplices[n - 2] =
Simplex(disjuncts[n - 2]);
866 disjuncts[i] = disjuncts[n - 1];
867 disjuncts[
j] = disjuncts[n - 2];
868 disjuncts.pop_back();
869 disjuncts[n - 2] = disjunct;
870 disjuncts[n - 2].removeRedundantConstraints();
872 simplices[i] = simplices[n - 1];
873 simplices[
j] = simplices[n - 2];
874 simplices.pop_back();
875 simplices[n - 2] =
Simplex(disjuncts[n - 2]);
895 LogicalResult SetCoalescer::coalescePairCutCase(
unsigned i,
unsigned j) {
901 return !isFacetContained(curr, simp);
907 newSet.addInequality(curr);
910 newSet.addInequality(curr);
912 addCoalescedDisjunct(i,
j, newSet);
919 if (type == Simplex::IneqType::Redundant)
920 redundantIneqsB.push_back(ineq);
921 else if (type == Simplex::IneqType::Cut)
922 cuttingIneqsB.push_back(ineq);
929 if (typeInequality(eq, simp).
failed())
933 if (typeInequality(inv, simp).
failed())
938 void SetCoalescer::eraseDisjunct(
unsigned i) {
939 assert(simplices.size() == disjuncts.size() &&
940 "simplices and disjuncts must be equally as long");
941 disjuncts[i] = disjuncts.back();
942 disjuncts.pop_back();
943 simplices[i] = simplices.back();
944 simplices.pop_back();
947 LogicalResult SetCoalescer::coalescePair(
unsigned i,
unsigned j) {
972 std::swap(redundantIneqsA, redundantIneqsB);
973 std::swap(cuttingIneqsA, cuttingIneqsB);
985 if (cuttingIneqsA.empty()) {
995 std::swap(redundantIneqsA, redundantIneqsB);
996 std::swap(cuttingIneqsA, cuttingIneqsB);
1000 if (cuttingIneqsA.empty()) {
static SymbolicLexOpt findSymbolicIntegerLexOpt(const PresburgerRelation &rel, bool isMin)
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
void compose(const IntegerRelation &rel)
Let the relation this be R1, and the relation rel be R2.
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.
This class represents a piece-wise MultiAffineFunction.
PWMAFunction unionLexMax(const PWMAFunction &func)
PWMAFunction unionLexMin(const PWMAFunction &func)
Return a function defined on the union of the domains of this and func, such that when only one of th...
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.
unsigned getNumLocalVars() const
void setSpace(const PresburgerSpace &oSpace)
Set the space to oSpace.
unsigned getNumRangeVars() const
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)
PresburgerSet getRangeSet() const
Return a set corresponding to the range of the relation.
bool isConvexNoLocals() const
Return true if the set is consist of a single disjunct, without any local variables,...
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.
unsigned getNumDomainVars() const
bool isIntegerEmpty() const
Return true if all the sets in the union are known to be integer empty false otherwise.
PresburgerRelation intersectRange(const PresburgerSet &set) const
Return the range intersection of the given set with this relation.
void unionInPlace(const IntegerRelation &disjunct)
Mutate this set, turning it into the union of this set and the given disjunct.
void convertVarKind(VarKind srcKind, unsigned srcPos, unsigned num, VarKind dstKind, unsigned dstPos)
Converts variables of the specified kind in the column range [srcPos, srcPos + num) to variables of t...
PresburgerRelation intersectDomain(const PresburgerSet &set) const
Return the domain intersection of the given set with this relation.
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.
void applyDomain(const PresburgerRelation &rel)
Apply the domain of given relation rel to this relation.
unsigned getNumDisjuncts() const
Return the number of disjuncts in the union.
void applyRange(const PresburgerRelation &rel)
Same as compose, provided for uniformity with applyDomain.
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.
bool isPlainEqual(const PresburgerRelation &set) const
Perform a quick equality check on this and other.
void compose(const PresburgerRelation &rel)
Compose this relation with the given relation rel in-place.
const PresburgerSpace & getSpace() const
void print(raw_ostream &os) const
Print the set's internal state.
void inverse()
Invert the relation, i.e.
bool isPlainUniverse() const
Return true if the set is known to have one unconstrained disjunct, false otherwise.
PresburgerSet getDomainSet() const
Return a set corresponding to the domain of the relation.
SymbolicLexOpt findSymbolicIntegerLexMax() const
Compute the symbolic integer lexmax of the relation, i.e.
bool isPlainEmpty() const
Return true if there is no disjunct, false otherwise.
void insertVarInPlace(VarKind kind, unsigned pos, unsigned num=1)
PresburgerRelation unionSet(const PresburgerRelation &set) const
Return the union of this set and the given set.
SymbolicLexOpt findSymbolicIntegerLexMin() const
Compute the symbolic integer lexmin of the relation, i.e.
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.
PresburgerSpace getRangeSpace() const
unsigned getNumVarKind(VarKind kind) const
Get the number of vars of the specified kind.
PresburgerSpace getDomainSpace() const
Get the domain/range space of this space.
void convertVarKind(VarKind srcKind, unsigned srcPos, unsigned num, VarKind dstKind, unsigned dstPos)
Converts variables of the specified kind in the column range [srcPos, srcPos + num) to variables of t...
unsigned getNumLocalVars() const
bool isCompatible(const PresburgerSpace &other) const
Returns true if both the spaces are compatible i.e.
static PresburgerSpace getRelationSpace(unsigned numDomain=0, unsigned numRange=0, unsigned numSymbols=0, unsigned numLocals=0)
unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1)
Insert num variables of the specified kind at position pos.
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 assist 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
Represents the result of a symbolic lexicographic optimization computation.
PWMAFunction lexopt
This maps assignments of symbols to the corresponding lexopt.
PresburgerSet unboundedDomain
Contains all assignments to the symbols that made the lexopt unbounded.
Eliminates variable at the specified position using Fourier-Motzkin variable elimination.