PresburgerRelation.cpp | Explore in Territory

//===- PresburgerRelation.cpp - MLIR PresburgerRelation Class -------------===//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//

#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>

usingnamespacemlir;
usingnamespacepresburger;

PresburgerRelation::PresburgerRelation(const IntegerRelation &disjunct)
    : … { … }

void PresburgerRelation::setSpace(const PresburgerSpace &oSpace) { … }

void PresburgerRelation::insertVarInPlace(VarKind kind, unsigned pos,
                                          unsigned num) { … }

void PresburgerRelation::convertVarKind(VarKind srcKind, unsigned srcPos,
                                        unsigned num, VarKind dstKind,
                                        unsigned dstPos) { … }

unsigned PresburgerRelation::getNumDisjuncts() const { … }

ArrayRef<IntegerRelation> PresburgerRelation::getAllDisjuncts() const { … }

const IntegerRelation &PresburgerRelation::getDisjunct(unsigned index) const { … }

/// Mutate this set, turning it into the union of this set and the given
/// IntegerRelation.
void PresburgerRelation::unionInPlace(const IntegerRelation &disjunct) { … }

/// Mutate this set, turning it into the union of this set and the given set.
///
/// This is accomplished by simply adding all the disjuncts of the given set
/// to this set.
void PresburgerRelation::unionInPlace(const PresburgerRelation &set) { … }

/// Return the union of this set and the given set.
PresburgerRelation
PresburgerRelation::unionSet(const PresburgerRelation &set) const { … }

/// A point is contained in the union iff any of the parts contain the point.
bool PresburgerRelation::containsPoint(ArrayRef<DynamicAPInt> point) const { … }

PresburgerRelation
PresburgerRelation::getUniverse(const PresburgerSpace &space) { … }

PresburgerRelation PresburgerRelation::getEmpty(const PresburgerSpace &space) { … }

// Return the intersection of this set with the given set.
//
// We directly compute (S_1 or S_2 ...) and (T_1 or T_2 ...)
// as (S_1 and T_1) or (S_1 and T_2) or ...
//
// If S_i or T_j have local variables, then S_i and T_j contains the local
// variables of both.
PresburgerRelation
PresburgerRelation::intersect(const PresburgerRelation &set) const { … }

PresburgerRelation
PresburgerRelation::intersectRange(const PresburgerSet &set) const { … }

PresburgerRelation
PresburgerRelation::intersectDomain(const PresburgerSet &set) const { … }

PresburgerSet PresburgerRelation::getDomainSet() const { … }

PresburgerSet PresburgerRelation::getRangeSet() const { … }

void PresburgerRelation::inverse() { … }

void PresburgerRelation::compose(const PresburgerRelation &rel) { … }

void PresburgerRelation::applyDomain(const PresburgerRelation &rel) { … }

void PresburgerRelation::applyRange(const PresburgerRelation &rel) { … }

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

SymbolicLexOpt PresburgerRelation::findSymbolicIntegerLexMin() const { … }

SymbolicLexOpt PresburgerRelation::findSymbolicIntegerLexMax() const { … }

/// 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.
static SmallVector<DynamicAPInt, 8>
getIneqCoeffsFromIdx(const IntegerRelation &rel, unsigned idx) { … }

PresburgerRelation PresburgerRelation::computeReprWithOnlyDivLocals() const { … }

/// 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.
///
static PresburgerRelation getSetDifference(IntegerRelation b,
                                           const PresburgerRelation &s) { … }

/// Return the complement of this set.
PresburgerRelation PresburgerRelation::complement() const { … }

/// Return the result of subtract the given set from this set, i.e.,
/// return `this \ set`.
PresburgerRelation
PresburgerRelation::subtract(const PresburgerRelation &set) const { … }

/// T is a subset of S iff T \ S is empty, since if T \ S contains a
/// point then this is a point that is contained in T but not S, and
/// if T contains a point that is not in S, this also lies in T \ S.
bool PresburgerRelation::isSubsetOf(const PresburgerRelation &set) const { … }

/// Two sets are equal iff they are subsets of each other.
bool PresburgerRelation::isEqual(const PresburgerRelation &set) const { … }

bool PresburgerRelation::isObviouslyEqual(const PresburgerRelation &set) const { … }

/// Return true if the Presburger relation represents the universe set, false
/// otherwise. It is a simple check that only check if the relation has at least
/// one unconstrained disjunct, indicating the absence of constraints or
/// conditions.
bool PresburgerRelation::isObviouslyUniverse() const { … }

bool PresburgerRelation::isConvexNoLocals() const { … }

/// Return true if there is no disjunct, false otherwise.
bool PresburgerRelation::isObviouslyEmpty() const { … }

/// Return true if all the sets in the union are known to be integer empty,
/// false otherwise.
bool PresburgerRelation::isIntegerEmpty() const { … }

bool PresburgerRelation::findIntegerSample(
    SmallVectorImpl<DynamicAPInt> &sample) { … }

std::optional<DynamicAPInt> PresburgerRelation::computeVolume() const { … }

/// The SetCoalescer class contains all functionality concerning the coalesce
/// heuristic. It is built from a `PresburgerRelation` and has the `coalesce()`
/// function as its main API. The coalesce heuristic simplifies the
/// representation of a PresburgerRelation. In particular, it removes all
/// disjuncts which are subsets of other disjuncts in the union and it combines
/// sets that overlap and can be combined in a convex way.
class presburger::SetCoalescer { … };

/// Constructs a `SetCoalescer` from a `PresburgerRelation`. Only adds non-empty
/// `IntegerRelation`s to the `disjuncts` vector.
SetCoalescer::SetCoalescer(const PresburgerRelation &s) : … { … }

/// Simplifies the representation of a PresburgerSet.
PresburgerRelation SetCoalescer::coalesce() { … }

/// Given a Simplex `simp` and one of its inequalities `ineq`, check
/// that all inequalities of `cuttingIneqsB` are redundant for the facet of
/// `simp` where `ineq` holds as an equality is contained within `a`.
bool SetCoalescer::isFacetContained(ArrayRef<DynamicAPInt> ineq,
                                    Simplex &simp) { … }

void SetCoalescer::addCoalescedDisjunct(unsigned i, unsigned j,
                                        const IntegerRelation &disjunct) { … }

/// Given two polyhedra `a` and `b` at positions `i` and `j` in
/// `disjuncts` and `redundantIneqsA` being the inequalities of `a` that
/// are redundant for `b` (similarly for `cuttingIneqsA`, `redundantIneqsB`,
/// and `cuttingIneqsB`), Checks whether the facets of all cutting
/// inequalites of `a` are contained in `b`. If so, a new polyhedron
/// consisting of all redundant inequalites of `a` and `b` and all
/// equalities of both is created.
///
/// An example of this case:
///    ___________        ___________
///   /   /  |   /       /          /
///   \   \  |  /   ==>  \         /
///    \   \ | /          \       /
///     \___\|/            \_____/
///
///
LogicalResult SetCoalescer::coalescePairCutCase(unsigned i, unsigned j) { … }

LogicalResult SetCoalescer::typeInequality(ArrayRef<DynamicAPInt> ineq,
                                           Simplex &simp) { … }

LogicalResult SetCoalescer::typeEquality(ArrayRef<DynamicAPInt> eq,
                                         Simplex &simp) { … }

void SetCoalescer::eraseDisjunct(unsigned i) { … }

LogicalResult SetCoalescer::coalescePair(unsigned i, unsigned j) { … }

PresburgerRelation PresburgerRelation::coalesce() const { … }

bool PresburgerRelation::hasOnlyDivLocals() const { … }

PresburgerRelation PresburgerRelation::simplify() const { … }

bool PresburgerRelation::isFullDim() const { … }

void PresburgerRelation::print(raw_ostream &os) const { … }

void PresburgerRelation::dump() const { … }

PresburgerSet PresburgerSet::getUniverse(const PresburgerSpace &space) { … }

PresburgerSet PresburgerSet::getEmpty(const PresburgerSpace &space) { … }

PresburgerSet::PresburgerSet(const IntegerPolyhedron &disjunct)
    : … { … }

PresburgerSet::PresburgerSet(const PresburgerRelation &set)
    : … { … }

PresburgerSet PresburgerSet::unionSet(const PresburgerRelation &set) const { … }

PresburgerSet PresburgerSet::intersect(const PresburgerRelation &set) const { … }

PresburgerSet PresburgerSet::complement() const { … }

PresburgerSet PresburgerSet::subtract(const PresburgerRelation &set) const { … }

PresburgerSet PresburgerSet::coalesce() const { … }
llvm/mlir/lib/Analysis/Presburger/PresburgerRelation.cpp
