mlir/unittests/Analysis/Presburger/PresburgerRelationTest.cpp

   1 //===- PresburgerRelationTest.cpp - Tests for PresburgerRelation class ----===//
   2 //
   3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
   4 // See https://llvm.org/LICENSE.txt for license information.
   5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
   6 //
   7 //===----------------------------------------------------------------------===//
   8 #include "mlir/Analysis/Presburger/PresburgerRelation.h"
   9 #include "Parser.h"
  10 #include "mlir/Analysis/Presburger/IntegerRelation.h"
  11 #include "mlir/Analysis/Presburger/Simplex.h"
  12
  13 #include <gmock/gmock.h>
  14 #include <gtest/gtest.h>
  15 #include <iostream>
  16
  17 using namespace mlir;
  18 using namespace presburger;
  19
  20 TEST(PresburgerRelationTest, intersectDomainAndRange) {
  21   {
  22     PresburgerRelation rel = parsePresburgerRelationFromPresburgerSet(
  23         {// (x, y) -> (x + N, y - N)
  24          "(x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0)",
  25          // (x, y) -> (x + y, x - y)
  26          "(x, y, a, b)[N] : (a - x - y == 0, b - x + y == 0)",
  27          // (x, y) -> (x - y, y - x)}
  28          "(x, y, a, b)[N] : (a - x + y == 0, b - y + x == 0)"},
  29         2);
  30
  31     PresburgerSet set =
  32         parsePresburgerSet({// (2x, x)
  33                             "(a, b)[N] : (a - 2 * b == 0)",
  34                             // (x, -x)
  35                             "(a, b)[N] : (a + b == 0)",
  36                             // (N, N)
  37                             "(a, b)[N] : (a - N == 0, b - N == 0)"});
  38
  39     PresburgerRelation expectedRel = parsePresburgerRelationFromPresburgerSet(
  40         {"(x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0, x - 2 * y == 0)",
  41          "(x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0, x + y == 0)",
  42          "(x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0, x - N == 0, y - N "
  43          "== 0)",
  44          "(x, y, a, b)[N] : (a - x - y == 0, b - x + y == 0, x - 2 * y == 0)",
  45          "(x, y, a, b)[N] : (a - x - y == 0, b - x + y == 0, x + y == 0)",
  46          "(x, y, a, b)[N] : (a - x - y == 0, b - x + y == 0, x - N == 0, y - N "
  47          "== 0)",
  48          "(x, y, a, b)[N] : (a - x + y == 0, b - y + x == 0, x - 2 * y == 0)",
  49          "(x, y, a, b)[N] : (a - x + y == 0, b - y + x == 0, x + y == 0)",
  50          "(x, y, a, b)[N] : (a - x + y == 0, b - y + x == 0, x - N == 0, y - N "
  51          "== 0)"},
  52         2);
  53
  54     PresburgerRelation computedRel = rel.intersectDomain(set);
  55     EXPECT_TRUE(computedRel.isEqual(expectedRel));
  56   }
  57
  58   {
  59     PresburgerRelation rel = parsePresburgerRelationFromPresburgerSet(
  60         {// (x)[N] -> (x + N, x - N)
  61          "(x, a, b)[N] : (a - x - N == 0, b - x + N == 0)",
  62          // (x)[N] -> (x, -x)
  63          "(x, a, b)[N] : (a - x == 0, b + x == 0)",
  64          // (x)[N] -> (N - x, 2 * x)}
  65          "(x, a, b)[N] : (a - N + x == 0, b - 2 * x == 0)"},
  66         1);
  67
  68     PresburgerSet set =
  69         parsePresburgerSet({// (2x, x)
  70                             "(a, b)[N] : (a - 2 * b == 0)",
  71                             // (x, -x)
  72                             "(a, b)[N] : (a + b == 0)",
  73                             // (N, N)
  74                             "(a, b)[N] : (a - N == 0, b - N == 0)"});
  75
  76     PresburgerRelation expectedRel = parsePresburgerRelationFromPresburgerSet(
  77         {"(x, a, b)[N] : (a - x - N == 0, b - x + N == 0, a - 2 * b == 0)",
  78          "(x, a, b)[N] : (a - x - N == 0, b - x + N == 0, a + b == 0)",
  79          "(x, a, b)[N] : (a - x - N == 0, b - x + N == 0, a - N == 0, b - N "
  80          "== 0)",
  81          "(x, a, b)[N] : (a - x == 0, b + x == 0, a - 2 * b == 0)",
  82          "(x, a, b)[N] : (a - x == 0, b + x == 0, a + b == 0)",
  83          "(x, a, b)[N] : (a - x == 0, b + x == 0, a - N == 0, b - N "
  84          "== 0)",
  85          "(x, a, b)[N] : (a - N + x == 0, b - 2 * x == 0, a - 2 * b == 0)",
  86          "(x, a, b)[N] : (a - N + x == 0, b - 2 * x == 0, a + b == 0)",
  87          "(x, a, b)[N] : (a - N + x == 0, b - 2 * x == 0, a - N == 0, b - N "
  88          "== 0)"},
  89         1);
  90
  91     PresburgerRelation computedRel = rel.intersectRange(set);
  92     EXPECT_TRUE(computedRel.isEqual(expectedRel));
  93   }
  94 }
  95
  96 TEST(PresburgerRelationTest, applyDomainAndRange) {
  97   {
  98     PresburgerRelation map1 = parsePresburgerRelationFromPresburgerSet(
  99         {// (x, y) -> (y, x)
 100          "(x, y, a, b)[N] : (y - a == 0, x - b == 0)",
 101          // (x, y) -> (x + N, y - N)
 102          "(x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0)"},
 103         2);
 104     PresburgerRelation map2 = parsePresburgerRelationFromPresburgerSet(
 105         {// (x, y) -> (x - y)
 106          "(x, y, r)[N] : (x - y - r == 0)",
 107          // (x, y) -> N
 108          "(x, y, r)[N] : (N - r == 0)"},
 109         2);
 110
 111     map1.applyDomain(map2);
 112
 113     PresburgerRelation map3 = parsePresburgerRelationFromPresburgerSet(
 114         {// (y - x) -> (x, y)
 115          "(r, x, y)[N] : (y - x - r == 0)",
 116          // (x - y - 2N) -> (x, y)
 117          "(r, x, y)[N] : (x - y - 2 * N - r == 0)",
 118          // (x, y) -> N
 119          "(r, x, y)[N] : (N - r == 0)"},
 120         1);
 121
 122     EXPECT_TRUE(map1.isEqual(map3));
 123   }
 124 }
 125
 126 TEST(PresburgerRelationTest, inverse) {
 127   {
 128     PresburgerRelation rel = parsePresburgerRelationFromPresburgerSet(
 129         {// (x, y) -> (-y, -x)
 130          "(x, y, a, b)[N] : (y + a == 0, x + b == 0)",
 131          // (x, y) -> (x + N, y - N)
 132          "(x, y, a, b)[N] : (x - a + N == 0, y - b - N == 0)"},
 133         2);
 134
 135     rel.inverse();
 136
 137     PresburgerRelation inverseRel = parsePresburgerRelationFromPresburgerSet(
 138         {// (x, y) -> (-y, -x)
 139          "(x, y, a, b)[N] : (y + a == 0, x + b == 0)",
 140          // (x, y) -> (x - N, y + N)
 141          "(x, y, a, b)[N] : (x - N - a == 0, y + N - b == 0)"},
 142         2);
 143
 144     EXPECT_TRUE(rel.isEqual(inverseRel));
 145   }
 146 }
 147
 148 TEST(PresburgerRelationTest, symbolicLexOpt) {
 149   PresburgerRelation rel1 = parsePresburgerRelationFromPresburgerSet(
 150       {"(x, y)[N, M] : (x >= 0, y >= 0, N - 1 >= 0, M >= 0, M - 2 * N - 1>= 0, "
 151        "2 * N - x >= 0, 2 * N - y >= 0)",
 152        "(x, y)[N, M] : (x >= 0, y >= 0, N - 1 >= 0, M >= 0, M - 2 * N - 1>= 0, "
 153        "x - N >= 0, M - x >= 0, y - 2 * N >= 0, M - y >= 0)"},
 154       1);
 155
 156   SymbolicLexOpt lexmin1 = rel1.findSymbolicIntegerLexMin();
 157
 158   PWMAFunction expectedLexMin1 = parsePWMAF({
 159       {"(x)[N, M] : (x >= 0, N - 1 >= 0, M >= 0, M - 2 * N - 1 >= 0, "
 160        "2 * N - x >= 0)",
 161        "(x)[N, M] -> (0)"},
 162       {"(x)[N, M] : (x >= 0, N - 1 >= 0, M >= 0, M - 2 * N - 1 >= 0, "
 163        "x - 2 * N- 1 >= 0, M - x >= 0)",
 164        "(x)[N, M] -> (2 * N)"},
 165   });
 166
 167   SymbolicLexOpt lexmax1 = rel1.findSymbolicIntegerLexMax();
 168
 169   PWMAFunction expectedLexMax1 = parsePWMAF({
 170       {"(x)[N, M] : (x >= 0, N - 1 >= 0, M >= 0, M - 2 * N - 1 >= 0, "
 171        "N - 1 - x  >= 0)",
 172        "(x)[N, M] -> (2 * N)"},
 173       {"(x)[N, M] : (x >= 0, N - 1 >= 0, M >= 0, M - 2 * N - 1 >= 0, "
 174        "x - N >= 0, M - x >= 0)",
 175        "(x)[N, M] -> (M)"},
 176   });
 177
 178   EXPECT_TRUE(lexmin1.unboundedDomain.isIntegerEmpty());
 179   EXPECT_TRUE(lexmin1.lexopt.isEqual(expectedLexMin1));
 180   EXPECT_TRUE(lexmax1.unboundedDomain.isIntegerEmpty());
 181   EXPECT_TRUE(lexmax1.lexopt.isEqual(expectedLexMax1));
 182
 183   PresburgerRelation rel2 = parsePresburgerRelationFromPresburgerSet(
 184       // x or y or z
 185       // lexmin = (x, 0, 1 - x)
 186       // lexmax = (x, 1, 1)
 187       {"(x, y, z) : (x >= 0, y >= 0, z >= 0, 1 - x >= 0, 1 - y >= 0, "
 188        "1 - z >= 0, x + y + z - 1 >= 0)",
 189        // (x or y) and (y or z) and (z or x)
 190        // lexmin = (x, 1 - x, 1)
 191        // lexmax = (x, 1, 1)
 192        "(x, y, z) : (x >= 0, y >= 0, z >= 0, 1 - x >= 0, 1 - y >= 0, "
 193        "1 - z >= 0, x + y - 1 >= 0, y + z - 1 >= 0, z + x - 1 >= 0)",
 194        // x => (not y) or (not z)
 195        // lexmin = (x, 0, 0)
 196        // lexmax = (x, 1, 1 - x)
 197        "(x, y, z) : (x >= 0, y >= 0, z >= 0, 1 - x >= 0, 1 - y >= 0, "
 198        "1 - z >= 0, 2 - x - y - z >= 0)"},
 199       1);
 200
 201   SymbolicLexOpt lexmin2 = rel2.findSymbolicIntegerLexMin();
 202
 203   PWMAFunction expectedLexMin2 =
 204       parsePWMAF({{"(x) : (x >= 0, 1 - x >= 0)", "(x) -> (0, 0)"}});
 205
 206   SymbolicLexOpt lexmax2 = rel2.findSymbolicIntegerLexMax();
 207
 208   PWMAFunction expectedLexMax2 =
 209       parsePWMAF({{"(x) : (x >= 0, 1 - x >= 0)", "(x) -> (1, 1)"}});
 210
 211   EXPECT_TRUE(lexmin2.unboundedDomain.isIntegerEmpty());
 212   EXPECT_TRUE(lexmin2.lexopt.isEqual(expectedLexMin2));
 213   EXPECT_TRUE(lexmax2.unboundedDomain.isIntegerEmpty());
 214   EXPECT_TRUE(lexmax2.lexopt.isEqual(expectedLexMax2));
 215
 216   PresburgerRelation rel3 = parsePresburgerRelationFromPresburgerSet(
 217       // (x => u or v or w) and (x or v) and (x or (not w))
 218       // lexmin = (x, 0, 0, 1 - x)
 219       // lexmax = (x, 1, 1 - x, x)
 220       {"(x, u, v, w) : (x >= 0, u >= 0, v >= 0, w >= 0, 1 - x >= 0, "
 221        "1 - u >= 0, 1 - v >= 0, 1 - w >= 0, -x + u + v + w >= 0, "
 222        "x + v - 1 >= 0, x - w >= 0)",
 223        // x => (u => (v => w)) and (x or (not v)) and (x or (not w))
 224        // lexmin = (x, 0, 0, x)
 225        // lexmax = (x, 1, x, x)
 226        "(x, u, v, w) : (x >= 0, u >= 0, v >= 0, w >= 0, 1 - x >= 0, "
 227        "1 - u >= 0, 1 - v >= 0, 1 - w >= 0, -x - u - v + w + 2 >= 0, "
 228        "x - v >= 0, x - w >= 0)",
 229        // (x or (u or (not v))) and ((not x) or ((not u) or w))
 230        // and (x or (not v)) and (x or (not w))
 231        // lexmin = (x, 0, 0, x)
 232        // lexmax = (x, 1, x, x)
 233        "(x, u, v, w) : (x >= 0, u >= 0, v >= 0, w >= 0, 1 - x >= 0, "
 234        "1 - u >= 0, 1 - v >= 0, 1 - w >= 0, x + u - v >= 0, x - u + w >= 0, "
 235        "x - v >= 0, x - w >= 0)"},
 236       1);
 237
 238   SymbolicLexOpt lexmin3 = rel3.findSymbolicIntegerLexMin();
 239
 240   PWMAFunction expectedLexMin3 =
 241       parsePWMAF({{"(x) : (x >= 0, 1 - x >= 0)", "(x) -> (0, 0, 0)"}});
 242
 243   SymbolicLexOpt lexmax3 = rel3.findSymbolicIntegerLexMax();
 244
 245   PWMAFunction expectedLexMax3 =
 246       parsePWMAF({{"(x) : (x >= 0, 1 - x >= 0)", "(x) -> (1, 1, x)"}});
 247
 248   EXPECT_TRUE(lexmin3.unboundedDomain.isIntegerEmpty());
 249   EXPECT_TRUE(lexmin3.lexopt.isEqual(expectedLexMin3));
 250   EXPECT_TRUE(lexmax3.unboundedDomain.isIntegerEmpty());
 251   EXPECT_TRUE(lexmax3.lexopt.isEqual(expectedLexMax3));
 252 }
 253
 254 TEST(PresburgerRelationTest, getDomainAndRangeSet) {
 255   PresburgerRelation rel = parsePresburgerRelationFromPresburgerSet(
 256       {// (x, y) -> (x + N, y - N)
 257        "(x, y, a, b)[N] : (a >= 0, b >= 0, N - a >= 0, N - b >= 0, x - a + N "
 258        "== 0, y - b - N == 0)",
 259        // (x, y) -> (- y, - x)
 260        "(x, y, a, b)[N] : (a >= 0, b >= 0, 2 * N - a >= 0, 2 * N - b >= 0, a + "
 261        "y == 0, b + x == 0)"},
 262       2);
 263
 264   PresburgerSet domainSet = rel.getDomainSet();
 265
 266   PresburgerSet expectedDomainSet = parsePresburgerSet(
 267       {"(x, y)[N] : (x + N >= 0, -x >= 0, y - N >= 0, 2 * N - y >= 0)",
 268        "(x, y)[N] : (x + 2 * N >= 0, -x >= 0, y + 2 * N >= 0, -y >= 0)"});
 269
 270   EXPECT_TRUE(domainSet.isEqual(expectedDomainSet));
 271
 272   PresburgerSet rangeSet = rel.getRangeSet();
 273
 274   PresburgerSet expectedRangeSet = parsePresburgerSet(
 275       {"(x, y)[N] : (x >= 0, 2 * N - x >= 0, y >= 0, 2 * N - y >= 0)"});
 276
 277   EXPECT_TRUE(rangeSet.isEqual(expectedRangeSet));
 278 }
 279
 280 TEST(PresburgerRelationTest, convertVarKind) {
 281   PresburgerSpace space = PresburgerSpace::getRelationSpace(2, 1, 3, 0);
 282
 283   IntegerRelation disj1 = parseRelationFromSet(
 284                       "(x, y, a)[U, V, W] : (x - U == 0, y + a - W == 0,"
 285                       "U - V >= 0, y - a >= 0)",
 286                       2),
 287                   disj2 = parseRelationFromSet(
 288                       "(x, y, a)[U, V, W] : (x + y - U == 0, x - a + V == 0,"
 289                       "V - U >= 0, y + a >= 0)",
 290                       2);
 291
 292   PresburgerRelation rel(disj1);
 293   rel.unionInPlace(disj2);
 294
 295   // Make a few kind conversions.
 296   rel.convertVarKind(VarKind::Domain, 0, 1, VarKind::Range, 0);
 297   rel.convertVarKind(VarKind::Symbol, 1, 2, VarKind::Domain, 1);
 298   rel.convertVarKind(VarKind::Symbol, 0, 1, VarKind::Range, 1);
 299
 300   // Expected rel.
 301   disj1.convertVarKind(VarKind::Domain, 0, 1, VarKind::Range, 0);
 302   disj1.convertVarKind(VarKind::Symbol, 1, 3, VarKind::Domain, 1);
 303   disj1.convertVarKind(VarKind::Symbol, 0, 1, VarKind::Range, 1);
 304   disj2.convertVarKind(VarKind::Domain, 0, 1, VarKind::Range, 0);
 305   disj2.convertVarKind(VarKind::Symbol, 1, 3, VarKind::Domain, 1);
 306   disj2.convertVarKind(VarKind::Symbol, 0, 1, VarKind::Range, 1);
 307
 308   PresburgerRelation expectedRel(disj1);
 309   expectedRel.unionInPlace(disj2);
 310
 311   // Check if var counts are correct.
 312   EXPECT_EQ(rel.getNumDomainVars(), 3u);
 313   EXPECT_EQ(rel.getNumRangeVars(), 3u);
 314   EXPECT_EQ(rel.getNumSymbolVars(), 0u);
 315
 316   // Check if identifiers are transferred correctly.
 317   EXPECT_TRUE(expectedRel.isEqual(rel));
 318 }