#include "mlir/Analysis/Presburger/PresburgerRelation.h"
#include "mlir/Analysis/Presburger/IntegerRelation.h"
#include "mlir/Analysis/Presburger/PWMAFunction.h"
#include "mlir/Analysis/Presburger/PresburgerSpace.h"
#include "mlir/Analysis/Presburger/Simplex.h"
#include "mlir/Analysis/Presburger/Utils.h"
#include "llvm/ADT/STLExtras.h"
#include "llvm/ADT/SmallBitVector.h"
#include "llvm/ADT/SmallVector.h"
#include "llvm/Support/LogicalResult.h"
#include "llvm/Support/raw_ostream.h"
#include <cassert>
#include <functional>
#include <optional>
#include <utility>
#include <vector>

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

Functions
static SymbolicLexOpt	findSymbolicIntegerLexOpt (const PresburgerRelation &rel, bool isMin)

static SmallVector< DynamicAPInt, 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...

Function Documentation

◆ findSymbolicIntegerLexOpt()

static SymbolicLexOpt findSymbolicIntegerLexOpt	(	const PresburgerRelation &	rel,
		bool	isMin
	)

static

Definition at line 246 of file PresburgerRelation.cpp.

References mlir::presburger::PresburgerRelation::getAllDisjuncts(), mlir::presburger::PresburgerRelation::getSpace(), mlir::presburger::PresburgerSet::intersect(), mlir::presburger::SymbolicLexOpt::lexopt, mlir::presburger::SymbolicLexOpt::unboundedDomain, mlir::presburger::PWMAFunction::unionLexMax(), and mlir::presburger::PWMAFunction::unionLexMin().

Referenced by mlir::presburger::PresburgerRelation::findSymbolicIntegerLexMax(), and mlir::presburger::PresburgerRelation::findSymbolicIntegerLexMin().

◆ getIneqCoeffsFromIdx()

static SmallVector<DynamicAPInt, 8> 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 288 of file PresburgerRelation.cpp.

References mlir::presburger::IntegerRelation::getEquality(), mlir::presburger::IntegerRelation::getInequality(), mlir::presburger::getNegatedCoeffs(), mlir::presburger::IntegerRelation::getNumEqualities(), and mlir::presburger::IntegerRelation::getNumInequalities().

Referenced by getSetDifference().

◆ 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 345 of file PresburgerRelation.cpp.

Referenced by mlir::presburger::PresburgerRelation::complement(), and mlir::presburger::PresburgerRelation::subtract().

Classes

Functions

Function Documentation

◆ findSymbolicIntegerLexOpt()

◆ getIneqCoeffsFromIdx()

◆ getSetDifference()