18 #include "llvm/ADT/STLExtras.h"
19 #include "llvm/ADT/SmallBitVector.h"
20 #include "llvm/ADT/SmallVector.h"
21 #include "llvm/Support/raw_ostream.h"
29 using namespace presburger;
32 : space(disjunct.getSpaceWithoutLocals()) {
40 disjunct.setSpaceExceptLocals(
space);
46 cs.insertVar(kind, pos, num);
54 "srcKind/dstKind cannot be local");
55 assert(srcKind != dstKind &&
"cannot convert variables to the same kind");
57 "invalid range for source variables");
59 "invalid position for destination variables");
64 disjunct.convertVarKind(srcKind, srcPos, srcPos + num, dstKind, dstPos);
76 assert(index <
disjuncts.size() &&
"index out of bounds!");
175 "Range of `this` must be compatible with range of `set`");
185 "Domain of `this` must be compatible with range of `set`");
216 assert(
getSpace().getRangeSpace().isCompatible(
218 "Range of `this` should be compatible with domain of `rel`");
235 assert(
getSpace().getDomainSpace().isCompatible(
237 "Domain of `this` should be compatible with domain of `rel`");
256 s = cs.findSymbolicIntegerLexMin();
259 s = cs.findSymbolicIntegerLexMax();
292 "idx out of bounds!");
300 return llvm::to_vector<8>(eqCoeffs);
311 result.
unionInPlace(disjunct.computeReprWithOnlyDivLocals());
370 unsigned simplexSnapshot;
380 std::optional<unsigned> lastIneqProcessed;
391 level = frames.size();
395 if (level > frames.size()) {
433 "Subtraction is not supported when a representation of the local "
434 "variables of the subtrahend cannot be found!");
437 unsigned lb = repr[i].repr.inequalityPair.lowerBoundIdx;
438 unsigned ub = repr[i].repr.inequalityPair.upperBoundIdx;
444 "Upper and lower bounds must be different inequalities!");
445 canIgnoreIneq[lb] =
true;
446 canIgnoreIneq[ub] =
true;
449 "ReprKind isn't inequality so should be equality");
476 unsigned numLocalsAdded =
480 unsigned snapshotBeforeIntersect = simplex.
getSnapshot();
494 frames.push_back(Frame{initialSnapshot, initBCounts, sI,
502 unsigned totalNewSimplexInequalities =
518 for (
unsigned j = 0;
j < totalNewSimplexInequalities;
j++)
520 simplex.
rollback(snapshotBeforeIntersect);
523 ineqsToProcess.reserve(totalNewSimplexInequalities);
524 for (
unsigned i = 0; i < totalNewSimplexInequalities; ++i)
525 if (!canIgnoreIneq[i])
526 ineqsToProcess.push_back(i);
528 if (ineqsToProcess.empty()) {
530 level = frames.size();
536 frames.push_back(Frame{simplexSnapshot, bCounts, sI, ineqsToProcess,
545 if (level == frames.size()) {
546 Frame &frame = frames.back();
547 if (frame.lastIneqProcessed) {
555 simplex.
rollback(frame.simplexSnapshot);
563 if (frame.ineqsToProcess.empty()) {
566 level = frames.size();
574 unsigned idx = frame.ineqsToProcess.back();
580 frame.ineqsToProcess.pop_back();
581 frame.lastIneqProcessed = idx;
651 if (disjunct.getNumConstraints() == 0)
677 disjunct.findIntegerSample()) {
678 sample = std::move(*opt);
691 std::optional<MPInt> volume = disjunct.computeVolume();
744 void addCoalescedDisjunct(
unsigned i,
unsigned j,
773 void eraseDisjunct(
unsigned i);
791 for (
unsigned i = 0; i < disjuncts.size();) {
792 disjuncts[i].removeRedundantConstraints();
795 disjuncts[i] = disjuncts[disjuncts.size() - 1];
796 disjuncts.pop_back();
800 simplices.push_back(simp);
810 for (
unsigned i = 0; i < disjuncts.size();) {
815 for (
unsigned j = 0, e = disjuncts.size();
j < e; ++
j) {
817 redundantIneqsA.clear();
818 redundantIneqsB.clear();
819 cuttingIneqsA.clear();
820 cuttingIneqsB.clear();
854 void SetCoalescer::addCoalescedDisjunct(
unsigned i,
unsigned j,
856 assert(i !=
j &&
"The indices must refer to different disjuncts");
857 unsigned n = disjuncts.size();
862 disjuncts[i] = disjuncts[n - 2];
863 disjuncts.pop_back();
864 disjuncts[n - 2] = disjunct;
865 disjuncts[n - 2].removeRedundantConstraints();
867 simplices[i] = simplices[n - 2];
868 simplices.pop_back();
869 simplices[n - 2] =
Simplex(disjuncts[n - 2]);
877 disjuncts[i] = disjuncts[n - 1];
878 disjuncts[
j] = disjuncts[n - 2];
879 disjuncts.pop_back();
880 disjuncts[n - 2] = disjunct;
881 disjuncts[n - 2].removeRedundantConstraints();
883 simplices[i] = simplices[n - 1];
884 simplices[
j] = simplices[n - 2];
885 simplices.pop_back();
886 simplices[n - 2] =
Simplex(disjuncts[n - 2]);
906 LogicalResult SetCoalescer::coalescePairCutCase(
unsigned i,
unsigned j) {
912 return !isFacetContained(curr, simp);
918 newSet.addInequality(curr);
921 newSet.addInequality(curr);
923 addCoalescedDisjunct(i,
j, newSet);
930 if (type == Simplex::IneqType::Redundant)
931 redundantIneqsB.push_back(ineq);
932 else if (type == Simplex::IneqType::Cut)
933 cuttingIneqsB.push_back(ineq);
940 if (typeInequality(eq, simp).
failed())
944 if (typeInequality(inv, simp).
failed())
949 void SetCoalescer::eraseDisjunct(
unsigned i) {
950 assert(simplices.size() == disjuncts.size() &&
951 "simplices and disjuncts must be equally as long");
952 disjuncts[i] = disjuncts.back();
953 disjuncts.pop_back();
954 simplices[i] = simplices.back();
955 simplices.pop_back();
958 LogicalResult SetCoalescer::coalescePair(
unsigned i,
unsigned j) {
983 std::swap(redundantIneqsA, redundantIneqsB);
984 std::swap(cuttingIneqsA, cuttingIneqsB);
996 if (cuttingIneqsA.empty()) {
1006 std::swap(redundantIneqsA, redundantIneqsB);
1007 std::swap(cuttingIneqsA, cuttingIneqsB);
1011 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 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.
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 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.
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.
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.
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.
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.
Include the generated interface declarations.
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.