MLIR  16.0.0git
PresburgerRelation.cpp File Reference
#include "mlir/Analysis/Presburger/PresburgerRelation.h"
#include "mlir/Analysis/Presburger/Simplex.h"
#include "mlir/Analysis/Presburger/Utils.h"
#include "llvm/ADT/STLExtras.h"
#include "llvm/ADT/ScopeExit.h"
#include "llvm/ADT/SmallBitVector.h"
Include dependency graph for PresburgerRelation.cpp:

Go to the source code of this file.

## Classes

class  mlir::presburger::SetCoalescer
The SetCoalescer class contains all functionality concerning the coalesce heuristic. More...

## Functions

static SmallVector< MPInt, 8 > getIneqCoeffsFromIdx (const IntegerRelation &rel, unsigned idx)
Return the coefficients of the ineq in rel specified by idx. More...

static PresburgerRelation getSetDifference (IntegerRelation b, const PresburgerRelation &s)
Return the set difference b \ s. More...

## ◆ getIneqCoeffsFromIdx()

 static SmallVector getIneqCoeffsFromIdx ( const IntegerRelation & rel, unsigned idx )
static

Return the coefficients of the ineq in rel specified by idx.

idx can refer not only to an actual inequality of rel, but also to either of the inequalities that make up an equality in rel.

When 0 <= idx < rel.getNumInequalities(), this returns the coeffs of the idx-th inequality of rel.

Otherwise, it is then considered to index into the ineqs corresponding to eqs of rel, and it must hold that

0 <= idx - rel.getNumInequalities() < 2*getNumEqualities().

For every eq coeffs == 0 there are two possible ineqs to index into. The first is coeffs >= 0 and the second is coeffs <= 0.

Definition at line 124 of file PresburgerRelation.cpp.

## ◆ getSetDifference()

 static PresburgerRelation getSetDifference ( IntegerRelation b, const PresburgerRelation & s )
static

Return the set difference b \ s.

In the following, U denotes union, /\ denotes intersection, \ denotes set difference and ~ denotes complement.

Let s = (U_i s_i). We want b \ (U_i s_i).

Let s_i = /_j s_ij, where each s_ij is a single inequality. To compute b \ s_i = b /\ ~s_i, we partition s_i based on the first violated inequality: ~s_i = (~s_i1) U (s_i1 /\ ~s_i2) U (s_i1 /\ s_i2 /\ ~s_i3) U ... And the required result is (b /\ ~s_i1) U (b /\ s_i1 /\ ~s_i2) U ... We recurse by subtracting U_{j > i} S_j from each of these parts and returning the union of the results. Each equality is handled as a conjunction of two inequalities.

Note that the same approach works even if an inequality involves a floor division. For example, the complement of x <= 7*floor(x/7) is still x > 7*floor(x/7). Since b \ s_i contains the inequalities of both b and s_i (or the complements of those inequalities), b \ s_i may contain the divisions present in both b and s_i. Therefore, we need to add the local division variables of both b and s_i to each part in the result. This means adding the local variables of both b and s_i, as well as the corresponding division inequalities to each part. Since the division inequalities are added to each part, we can skip the parts where the complement of any division inequality is added, as these parts will become empty anyway.

As a heuristic, we try adding all the constraints and check if simplex says that the intersection is empty. If it is, then subtracting this disjuncts is a no-op and we just skip it. Also, in the process we find out that some constraints are redundant. These redundant constraints are ignored.

Definition at line 182 of file PresburgerRelation.cpp.