Utils.cpp File Reference

#include "mlir/Analysis/Presburger/Utils.h"
#include "mlir/Analysis/Presburger/IntegerRelation.h"
#include "mlir/Analysis/Presburger/PresburgerSpace.h"
#include "llvm/ADT/STLFunctionalExtras.h"
#include "llvm/ADT/SmallBitVector.h"
#include "llvm/Support/LogicalResult.h"
#include "llvm/Support/raw_ostream.h"
#include <cassert>
#include <cstdint>
#include <numeric>
#include <optional>

Go to the source code of this file.

Functions
static void	normalizeDivisionByGCD (MutableArrayRef< DynamicAPInt > dividend, DynamicAPInt &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< DynamicAPInt > expr, DynamicAPInt &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< DynamicAPInt > expr, DynamicAPInt &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< DynamicAPInt > dividend, unsigned pos)

Function Documentation

checkExplicitRepresentation()

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

static

Definition at line 197 of file Utils.cpp.

References mlir::presburger::IntegerRelation::getNumVars().

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

getDivRepr() [1/2]

static LogicalResult getDivRepr ( const IntegerRelation &  cst, unsigned  pos, unsigned  eqInd, MutableArrayRef< DynamicAPInt >  expr, DynamicAPInt &  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 165 of file Utils.cpp.

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

getDivRepr() [2/2]

static LogicalResult getDivRepr ( const IntegerRelation &  cst, unsigned  pos, unsigned  ubIneq, unsigned  lbIneq, MutableArrayRef< DynamicAPInt >  expr, DynamicAPInt &  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 99 of file Utils.cpp.

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

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

normalizeDivisionByGCD()

static void normalizeDivisionByGCD ( MutableArrayRef< DynamicAPInt >  dividend, DynamicAPInt &  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 33 of file Utils.cpp.

References mlir::presburger::abs().

Referenced by getDivRepr().