MLIR  19.0.0git
Functions
Utils.cpp File Reference
#include "mlir/Analysis/Presburger/Utils.h"
#include "mlir/Analysis/Presburger/IntegerRelation.h"
#include "mlir/Analysis/Presburger/MPInt.h"
#include "mlir/Analysis/Presburger/PresburgerSpace.h"
#include "mlir/Support/LLVM.h"
#include "mlir/Support/LogicalResult.h"
#include "llvm/ADT/STLFunctionalExtras.h"
#include "llvm/ADT/SmallBitVector.h"
#include "llvm/Support/raw_ostream.h"
#include <algorithm>
#include <cassert>
#include <cstddef>
#include <cstdint>
#include <functional>
#include <numeric>
#include <optional>

Go to the source code of this file.

Functions

static void normalizeDivisionByGCD (MutableArrayRef< MPInt > dividend, MPInt &divisor)
 Normalize a division's dividend and the divisor by their GCD. More...
 
static LogicalResult getDivRepr (const IntegerRelation &cst, unsigned pos, unsigned ubIneq, unsigned lbIneq, MutableArrayRef< MPInt > expr, MPInt &divisor)
 Check if the pos^th variable can be represented as a division using upper bound inequality at position ubIneq and lower bound inequality at position lbIneq. More...
 
static LogicalResult getDivRepr (const IntegerRelation &cst, unsigned pos, unsigned eqInd, MutableArrayRef< MPInt > expr, MPInt &divisor)
 Check if the pos^th variable can be represented as a division using equality at position eqInd. More...
 
static bool checkExplicitRepresentation (const IntegerRelation &cst, ArrayRef< bool > foundRepr, ArrayRef< MPInt > dividend, unsigned pos)
 

Function Documentation

◆ checkExplicitRepresentation()

static bool checkExplicitRepresentation ( const IntegerRelation cst,
ArrayRef< bool >  foundRepr,
ArrayRef< MPInt dividend,
unsigned  pos 
)
static

◆ getDivRepr() [1/2]

static LogicalResult getDivRepr ( const IntegerRelation cst,
unsigned  pos,
unsigned  eqInd,
MutableArrayRef< MPInt expr,
MPInt divisor 
)
static

Check if the pos^th variable can be represented as a division using equality at position eqInd.

For example: 32*k == 16*i + j - 31 <– eqInd for 'k' expr = 16*i + j - 31, divisor = 32 k = (16*i + j - 31) floordiv 32

If successful, expr is set to dividend of the division and divisor is set to the denominator of the division. The final division expression is normalized by GCD.

Definition at line 170 of file Utils.cpp.

References mlir::presburger::IntegerRelation::atEq(), mlir::failure(), mlir::presburger::IntegerRelation::getNumCols(), mlir::presburger::IntegerRelation::getNumEqualities(), mlir::presburger::IntegerRelation::getNumVars(), normalizeDivisionByGCD(), and mlir::success().

◆ getDivRepr() [2/2]

static LogicalResult getDivRepr ( const IntegerRelation cst,
unsigned  pos,
unsigned  ubIneq,
unsigned  lbIneq,
MutableArrayRef< MPInt expr,
MPInt divisor 
)
static

Check if the pos^th variable can be represented as a division using upper bound inequality at position ubIneq and lower bound inequality at position lbIneq.

Let var be the pos^th variable, then var is equivalent to expr floordiv divisor if there are constraints of the form: 0 <= expr - divisor * var <= divisor - 1 Rearranging, we have: divisor * var - expr + (divisor - 1) >= 0 <– Lower bound for 'var' -divisor * var + expr >= 0 <– Upper bound for 'var'

For example: 32*k >= 16*i + j - 31 <– Lower bound for 'k' 32*k <= 16*i + j <– Upper bound for 'k' expr = 16*i + j, divisor = 32 k = ( 16*i + j ) floordiv 32

4q >= i + j - 2 <– Lower bound for 'q' 4q <= i + j + 1 <– Upper bound for 'q' expr = i + j + 1, divisor = 4 q = (i + j + 1) floordiv 4 This function also supports detecting divisions from bounds that are strictly tighter than the division bounds described above, since tighter bounds imply the division bounds. For example: 4q - i - j + 2 >= 0 <– Lower bound for 'q' -4q + i + j >= 0 <– Tight upper bound for 'q'

To extract floor divisions with tighter bounds, we assume that the constraints are of the form: c <= expr - divisior * var <= divisor - 1, where 0 <= c <= divisor - 1 Rearranging, we have: divisor * var - expr + (divisor - 1) >= 0 <– Lower bound for 'var' -divisor * var + expr - c >= 0 <– Upper bound for 'var'

If successful, expr is set to dividend of the division and divisor is set to the denominator of the division, which will be positive. The final division expression is normalized by GCD.

Definition at line 105 of file Utils.cpp.

References mlir::presburger::IntegerRelation::atIneq(), mlir::failure(), mlir::presburger::IntegerRelation::getNumCols(), mlir::presburger::IntegerRelation::getNumInequalities(), mlir::presburger::IntegerRelation::getNumVars(), normalizeDivisionByGCD(), and mlir::success().

Referenced by mlir::presburger::computeSingleVarRepr().

◆ normalizeDivisionByGCD()

static void normalizeDivisionByGCD ( MutableArrayRef< MPInt dividend,
MPInt divisor 
)
static

Normalize a division's dividend and the divisor by their GCD.

For example: if the dividend and divisor are [2,0,4] and 4 respectively, they get normalized to [1,0,2] and 2. The divisor must be non-negative; it is allowed for the divisor to be zero, but nothing is done in this case.

Definition at line 39 of file Utils.cpp.

References mlir::presburger::abs(), and mlir::presburger::gcd().

Referenced by getDivRepr().