15 #include "llvm/ADT/STLExtras.h"
16 #include "llvm/ADT/SmallBitVector.h"
17 #include "llvm/ADT/SmallVector.h"
18 #include "llvm/Support/raw_ostream.h"
26 using namespace presburger;
29 : space(disjunct.getSpaceWithoutLocals()) {
37 disjunct.setSpaceExceptLocals(
space);
43 cs.insertVar(
kind, pos, num);
51 "srcKind/dstKind cannot be local");
52 assert(srcKind != dstKind &&
"cannot convert variables to the same kind");
54 "invalid range for source variables");
56 "invalid position for destination variables");
61 disjunct.convertVarKind(srcKind, srcPos, srcPos + num, dstKind, dstPos);
73 assert(index <
disjuncts.size() &&
"index out of bounds!");
172 "Range of `this` must be compatible with range of `set`");
182 "Domain of `this` must be compatible with range of `set`");
213 assert(
getSpace().getRangeSpace().isCompatible(
215 "Range of `this` should be compatible with domain of `rel`");
232 assert(
getSpace().getDomainSpace().isCompatible(
234 "Domain of `this` should be compatible with domain of `rel`");
253 s = cs.findSymbolicIntegerLexMin();
256 s = cs.findSymbolicIntegerLexMax();
289 "idx out of bounds!");
297 return llvm::to_vector<8>(eqCoeffs);
308 result.
unionInPlace(disjunct.computeReprWithOnlyDivLocals());
367 unsigned simplexSnapshot;
377 std::optional<unsigned> lastIneqProcessed;
380 Frame(
unsigned simplexSnapshot,
383 std::optional<unsigned> lastIneqProcessed = std::nullopt)
384 : simplexSnapshot(simplexSnapshot), bCounts(bCounts), sI(sI),
385 ineqsToProcess(ineqsToProcess), lastIneqProcessed(lastIneqProcessed) {
397 level = frames.size();
401 if (level > frames.size()) {
439 "Subtraction is not supported when a representation of the local "
440 "variables of the subtrahend cannot be found!");
443 unsigned lb = repr[i].repr.inequalityPair.lowerBoundIdx;
444 unsigned ub = repr[i].repr.inequalityPair.upperBoundIdx;
450 "Upper and lower bounds must be different inequalities!");
451 canIgnoreIneq[lb] =
true;
452 canIgnoreIneq[ub] =
true;
455 "ReprKind isn't inequality so should be equality");
482 unsigned numLocalsAdded =
486 unsigned snapshotBeforeIntersect = simplex.
getSnapshot();
500 frames.emplace_back(Frame{initialSnapshot, initBCounts, sI});
506 unsigned totalNewSimplexInequalities =
522 for (
unsigned j = 0;
j < totalNewSimplexInequalities;
j++)
524 simplex.
rollback(snapshotBeforeIntersect);
527 ineqsToProcess.reserve(totalNewSimplexInequalities);
528 for (
unsigned i = 0; i < totalNewSimplexInequalities; ++i)
529 if (!canIgnoreIneq[i])
530 ineqsToProcess.emplace_back(i);
532 if (ineqsToProcess.empty()) {
534 level = frames.size();
540 frames.emplace_back(Frame{simplexSnapshot, bCounts, sI, ineqsToProcess});
548 if (level == frames.size()) {
549 Frame &frame = frames.back();
550 if (frame.lastIneqProcessed) {
558 simplex.
rollback(frame.simplexSnapshot);
566 if (frame.ineqsToProcess.empty()) {
569 level = frames.size();
577 unsigned idx = frame.ineqsToProcess.back();
583 frame.ineqsToProcess.pop_back();
584 frame.lastIneqProcessed = idx;
654 if (disjunct.getNumConstraints() == 0)
681 disjunct.findIntegerSample()) {
682 sample = std::move(*opt);
693 DynamicAPInt result(0);
695 std::optional<DynamicAPInt> volume = disjunct.computeVolume();
748 void addCoalescedDisjunct(
unsigned i,
unsigned j,
762 LogicalResult coalescePairCutCase(
unsigned i,
unsigned j);
777 void eraseDisjunct(
unsigned i);
784 LogicalResult coalescePair(
unsigned i,
unsigned j);
795 for (
unsigned i = 0; i < disjuncts.size();) {
796 disjuncts[i].removeRedundantConstraints();
799 disjuncts[i] = disjuncts[disjuncts.size() - 1];
800 disjuncts.pop_back();
804 simplices.emplace_back(simp);
814 for (
unsigned i = 0; i < disjuncts.size();) {
819 for (
unsigned j = 0, e = disjuncts.size();
j < e; ++
j) {
821 redundantIneqsA.clear();
822 redundantIneqsB.clear();
823 cuttingIneqsA.clear();
824 cuttingIneqsB.clear();
827 if (coalescePair(i,
j).succeeded()) {
859 void SetCoalescer::addCoalescedDisjunct(
unsigned i,
unsigned j,
861 assert(i !=
j &&
"The indices must refer to different disjuncts");
862 unsigned n = disjuncts.size();
867 disjuncts[i] = disjuncts[n - 2];
868 disjuncts.pop_back();
869 disjuncts[n - 2] = disjunct;
870 disjuncts[n - 2].removeRedundantConstraints();
872 simplices[i] = simplices[n - 2];
873 simplices.pop_back();
874 simplices[n - 2] =
Simplex(disjuncts[n - 2]);
882 disjuncts[i] = disjuncts[n - 1];
883 disjuncts[
j] = disjuncts[n - 2];
884 disjuncts.pop_back();
885 disjuncts[n - 2] = disjunct;
886 disjuncts[n - 2].removeRedundantConstraints();
888 simplices[i] = simplices[n - 1];
889 simplices[
j] = simplices[n - 2];
890 simplices.pop_back();
891 simplices[n - 2] =
Simplex(disjuncts[n - 2]);
911 LogicalResult SetCoalescer::coalescePairCutCase(
unsigned i,
unsigned j) {
917 return !isFacetContained(curr, simp);
923 newSet.addInequality(curr);
926 newSet.addInequality(curr);
928 addCoalescedDisjunct(i,
j, newSet);
935 if (type == Simplex::IneqType::Redundant)
936 redundantIneqsB.emplace_back(ineq);
937 else if (type == Simplex::IneqType::Cut)
938 cuttingIneqsB.emplace_back(ineq);
946 if (typeInequality(eq, simp).
failed())
950 return typeInequality(inv, simp);
953 void SetCoalescer::eraseDisjunct(
unsigned i) {
954 assert(simplices.size() == disjuncts.size() &&
955 "simplices and disjuncts must be equally as long");
956 disjuncts[i] = disjuncts.back();
957 disjuncts.pop_back();
958 simplices[i] = simplices.back();
959 simplices.pop_back();
962 LogicalResult SetCoalescer::coalescePair(
unsigned i,
unsigned j) {
984 if (typeEquality(a.
getEquality(k), simpB).failed())
987 std::swap(redundantIneqsA, redundantIneqsB);
988 std::swap(cuttingIneqsA, cuttingIneqsB);
995 if (typeEquality(b.
getEquality(k), simpA).failed())
1000 if (cuttingIneqsA.empty()) {
1006 if (coalescePairCutCase(i,
j).succeeded())
1010 std::swap(redundantIneqsA, redundantIneqsB);
1011 std::swap(cuttingIneqsA, cuttingIneqsB);
1015 if (cuttingIneqsA.empty()) {
1021 return coalescePairCutCase(
j, i);
union mlir::linalg::@1244::ArityGroupAndKind::Kind kind
static SymbolicLexOpt findSymbolicIntegerLexOpt(const PresburgerRelation &rel, bool isMin)
static SmallVector< DynamicAPInt, 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.
DynamicAPInt & getDenom(unsigned i)
MutableArrayRef< DynamicAPInt > 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 ...
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 truncate(const CountsSnapshot &counts)
CountsSnapshot getCounts() const
std::optional< SmallVector< DynamicAPInt, 8 > > containsPointNoLocal(ArrayRef< DynamicAPInt > point) const
Given the values of non-local vars, return a satisfying assignment to the local if one exists,...
ArrayRef< DynamicAPInt > getInequality(unsigned idx) const
bool isEmptyByGCDTest() const
Runs the GCD test on all equality constraints.
void simplify()
Simplify the constraint system by removing canonicalizing constraints and removing redundant constrai...
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.
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 isObviouslyEmpty() const
Performs GCD checks and invalid constraint checks.
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.
void addInequality(ArrayRef< DynamicAPInt > inEq)
Adds an inequality (>= 0) from the coefficients specified in inEq.
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...
ArrayRef< DynamicAPInt > getEquality(unsigned idx) const
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 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
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.
bool containsPoint(ArrayRef< DynamicAPInt > point) const
Return true if the set contains the given point, and false otherwise.
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.
std::optional< DynamicAPInt > computeVolume() const
Compute an overapproximation of the number of integer points in the 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.
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.
bool findIntegerSample(SmallVectorImpl< DynamicAPInt > &sample)
Find an integer sample from the given set.
bool isObviouslyEmpty() const
Return true if there is no disjunct, false otherwise.
bool isObviouslyUniverse() const
Return true if the set is known to have one unconstrained disjunct, false otherwise.
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.
PresburgerRelation simplify() const
Simplify each disjunct, canonicalizing each disjunct and removing redundencies.
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.
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.
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.
bool isObviouslyEqual(const PresburgerRelation &set) const
Perform a quick equality check on this and other.
SymbolicLexOpt findSymbolicIntegerLexMin() const
Compute the symbolic integer lexmin of the relation, i.e.
bool isFullDim() const
Return whether the given PresburgerRelation is full-dimensional.
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< DynamicAPInt > 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.
IneqType findIneqType(ArrayRef< DynamicAPInt > coeffs)
Returns the type of the inequality with coefficients coeffs.
bool isRedundantInequality(ArrayRef< DynamicAPInt > coeffs)
Check if the specified inequality already holds in the polytope.
void addInequality(ArrayRef< DynamicAPInt > coeffs) final
Add an inequality to the tableau.
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...
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< DynamicAPInt, 8 > getNegatedCoeffs(ArrayRef< DynamicAPInt > coeffs)
Return coeffs with all the elements negated.
SmallVector< DynamicAPInt, 8 > getDivUpperBound(ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &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< DynamicAPInt, 8 > getDivLowerBound(ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &divisor, unsigned localVarIdx)
SmallVector< DynamicAPInt, 8 > getComplementIneq(ArrayRef< DynamicAPInt > ineq)
Return the complement of the given inequality.
Include the generated interface declarations.
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.