14#include "llvm/ADT/STLExtras.h"
15#include "llvm/ADT/STLFunctionalExtras.h"
16#include "llvm/ADT/SmallVector.h"
17#include "llvm/Support/raw_ostream.h"
25void MultiAffineFunction::assertIsConsistent()
const {
26 assert(space.getNumVars() - space.getNumRangeVars() + 1 ==
27 output.getNumColumns() &&
28 "Inconsistent number of output columns");
29 assert(space.getNumDomainVars() + space.getNumSymbolVars() ==
30 divs.getNumNonDivs() &&
31 "Inconsistent number of non-division variables in divs");
32 assert(space.getNumRangeVars() == output.getNumRows() &&
33 "Inconsistent number of output rows");
34 assert(space.getNumLocalVars() == divs.getNumDivs() &&
35 "Inconsistent number of divisions.");
36 assert(divs.hasAllReprs() &&
"All divisions should have a representation");
44 assert(vecA.size() == vecB.size() &&
45 "Cannot subtract vectors of differing lengths!");
47 result.reserve(vecA.size());
48 for (
unsigned i = 0, e = vecA.size(); i < e; ++i)
49 result.emplace_back(vecA[i] - vecB[i]);
55 for (
const Piece &piece : pieces)
62 os <<
"Division Representation:\n";
73 "Point has incorrect dimensionality!");
78 divs.divValuesAt(point);
81 pointHomogenous.reserve(pointHomogenous.size() + divValues.size());
82 for (
const std::optional<DynamicAPInt> &divVal : divValues)
83 pointHomogenous.emplace_back(*divVal);
89 pointHomogenous.emplace_back(1);
91 output.postMultiplyWithColumn(pointHomogenous);
97 assert(space.isCompatible(other.space) &&
98 "Spaces should be compatible for equality check.");
104 assert(space.isCompatible(other.space) &&
105 "Spaces should be compatible for equality check.");
112 return restrictedThis.
isEqual(restrictedOther);
117 assert(space.isCompatible(other.space) &&
118 "Spaces should be compatible for equality check.");
121 return isEqual(other, IntegerPolyhedron(disjunct));
132 output.removeRows(start, end - start);
136 assert(space.isCompatible(other.space) &&
"Functions should be compatible");
139 unsigned divOffset = divs.getDivOffset();
144 for (
unsigned i = 0; i < nDivs; ++i) {
148 std::copy(divs.getDividend(i).begin(), divs.getDividend(i).end() - 1,
151 div.back() = divs.getDividend(i).back();
152 other.divs.
setDiv(i,
div, divs.getDenom(i));
158 auto merge = [&](
unsigned i,
unsigned j) {
170 other.output.
addToColumn(divOffset + i, divOffset +
j, 1);
177 unsigned newDivs = other.divs.
getNumDivs() - nDivs;
180 output.insertColumns(divOffset + nDivs, newDivs);
184 assertIsConsistent();
185 other.assertIsConsistent();
192 "Output space of funcs should be compatible");
226 for (
unsigned i = 0, e = funcA.
getNumDivs(); i < e; ++i) {
235 for (
unsigned level = 0; level < funcA.
getNumOutputs(); ++level) {
260 assert(
false &&
"Not implemented case");
264 result.unionInPlace(levelSet);
278 if (!space.isCompatible(other.space))
288 return llvm::all_of(this->pieces, [&other](
const Piece &pieceA) {
289 return llvm::all_of(other.pieces, [&pieceA](
const Piece &pieceB) {
290 PresburgerSet commonDomain = pieceA.domain.intersect(pieceB.domain);
291 return pieceA.output.isEqual(pieceB.output, commonDomain);
297 assert(piece.
isConsistent() &&
"Piece should be consistent");
299 "Piece should be disjoint from the function");
300 pieces.emplace_back(piece);
306 for (
const Piece &piece : pieces) {
307 os <<
"Domain of piece:\n";
308 piece.domain.print(os);
309 os <<
"Output of piece\n";
310 piece.output.print(os);
320 "Ranges of functions should be same.");
322 "Space is not compatible.");
336 for (
const Piece &pieceA : pieces) {
338 for (
const Piece &pieceB :
func.pieces) {
346 result.addPiece({better, pieceB.output});
347 dom = dom.subtract(better);
359 result.addPiece({dom, pieceA.output});
364 for (
const Piece &pieceB : func.pieces)
365 result.addPiece({pieceB.domain.subtract(dom), pieceB.output});
373template <OrderingKind comp>
391 assert(space.isCompatible(other.space) &&
392 "Spaces should be compatible for subtraction.");
397 output.addToRow(i, copyOther.
getOutputExpr(i), DynamicAPInt(-1));
400 assertIsConsistent();
409 "All divisions in divs should have a representation");
411 "Relation and divs should have the same number of vars");
413 "Relation and divs should have the same number of local vars");
415 for (
unsigned i = 0, e = divs.
getNumDivs(); i < e; ++i) {
427 space.getNumDomainVars(), 0, space.getNumSymbolVars(),
428 space.getNumLocalVars()));
466 for (
Piece &piece : pieces)
467 piece.output.removeOutputs(start, end);
470std::optional<SmallVector<DynamicAPInt, 8>>
474 for (
const Piece &piece : pieces)
475 if (piece.domain.containsPoint(point))
476 return piece.output.valueAt(point);
static PresburgerSet tiebreakLex(const PWMAFunction::Piece &pieceA, const PWMAFunction::Piece &pieceB)
A tiebreak function which breaks ties by comparing the outputs lexicographically based on the given c...
static SmallVector< DynamicAPInt, 8 > subtractExprs(ArrayRef< DynamicAPInt > vecA, ArrayRef< DynamicAPInt > vecB)
static void addDivisionConstraints(IntegerRelation &rel, const DivisionRepr &divs)
Adds division constraints corresponding to local variables, given a relation and division representat...
Class storing division representation of local variables of a constraint system.
void removeDuplicateDivs(llvm::function_ref< bool(unsigned i, unsigned j)> merge)
Removes duplicate divisions.
unsigned getNumVars() const
unsigned getDivOffset() const
unsigned getNumDivs() const
DynamicAPInt & getDenom(unsigned i)
void insertDiv(unsigned pos, ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &divisor)
void setDiv(unsigned i, ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &divisor)
MutableArrayRef< DynamicAPInt > getDividend(unsigned i)
An IntegerPolyhedron represents the set of points from a PresburgerSpace that satisfy a list of affin...
An IntegerRelation represents the set of points from a PresburgerSpace that satisfy a list of affine ...
void addBound(BoundType type, unsigned pos, const DynamicAPInt &value)
Adds a constant bound for the specified variable.
unsigned getNumVars() const
void intersectDomain(const IntegerPolyhedron &poly)
Intersect the given poly with the domain in-place.
bool isEqual(const IntegerRelation &other) const
Return whether this and other are equal.
void addEquality(ArrayRef< DynamicAPInt > eq)
Adds an equality from the coefficients specified in eq.
unsigned getNumLocalVars() const
void removeInequality(unsigned pos)
void addInequality(ArrayRef< DynamicAPInt > inEq)
Adds an inequality (>= 0) from the coefficients specified in inEq.
unsigned getNumInequalities() const
void removeColumn(unsigned pos)
void addToColumn(unsigned sourceColumn, unsigned targetColumn, const T &scale)
Add scale multiples of the source column to the target column.
void insertColumns(unsigned pos, unsigned count)
Insert columns having positions pos, pos + 1, ... pos + count - 1.
void subtract(const MultiAffineFunction &other)
void removeOutputs(unsigned start, unsigned end)
Remove the specified range of outputs.
const PresburgerSpace & getSpace() const
Get the space of this function.
void print(raw_ostream &os) const
unsigned getNumDivs() const
MultiAffineFunction(const PresburgerSpace &space, const IntMatrix &output)
PresburgerSpace getDomainSpace() const
Get the domain/output space of the function.
PresburgerSet getLexSet(OrderingKind comp, const MultiAffineFunction &other) const
Return the set of domain points where the output of this and other are ordered lexicographically acco...
unsigned getNumOutputs() const
SmallVector< DynamicAPInt, 8 > valueAt(ArrayRef< DynamicAPInt > point) const
unsigned getNumDomainVars() const
void mergeDivs(MultiAffineFunction &other)
Given a MAF other, merges division variables such that both functions have the union of the division ...
unsigned getNumSymbolVars() const
ArrayRef< DynamicAPInt > getOutputExpr(unsigned i) const
Get the i^th output expression.
IntegerRelation getAsRelation() const
Get this function as a relation.
bool isEqual(const MultiAffineFunction &other) const
Return whether the this and other are equal when the domain is restricted to domain.
This class represents a piece-wise MultiAffineFunction.
void addPiece(const Piece &piece)
unsigned getNumDomainVars() const
void print(raw_ostream &os) const
PWMAFunction unionLexMax(const PWMAFunction &func)
unsigned getNumPieces() const
void removeOutputs(unsigned start, unsigned end)
Remove the specified range of outputs.
unsigned getNumOutputs() const
const PresburgerSpace & getSpace() const
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...
PWMAFunction(const PresburgerSpace &space)
std::optional< SmallVector< DynamicAPInt, 8 > > valueAt(ArrayRef< DynamicAPInt > point) const
Return the output of the function at the given point.
PresburgerSet getDomain() const
Return the domain of this piece-wise MultiAffineFunction.
PresburgerSpace getDomainSpace() const
Get the domain/output space of the function.
unsigned getNumSymbolVars() const
bool isEqual(const PWMAFunction &other) const
Return whether this and other are equal as PWMAFunctions, i.e.
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.
ArrayRef< IntegerRelation > getAllDisjuncts() const
Return a reference to the list of disjuncts.
PresburgerSet intersect(const PresburgerRelation &set) const
static PresburgerSet getEmpty(const PresburgerSpace &space)
Return an empty set of the specified type that contains no points.
PresburgerSpace is the space of all possible values of a tuple of integer valued variables/variables.
void removeVarRange(VarKind kind, unsigned varStart, unsigned varLimit)
Removes variables of the specified kind in the column range [varStart, varLimit).
unsigned getNumVars() const
unsigned getNumLocalVars() const
PresburgerSpace getSpaceWithoutLocals() const
Get the space without local variables.
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.
OrderingKind
Enum representing a binary comparison operator: equal, not equal, less than, less than or equal,...
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)
Include the generated interface declarations.
MultiAffineFunction output
bool isConsistent() const
Eliminates variable at the specified position using Fourier-Motzkin variable elimination.