1//===- PresbugerParserTest.cpp - Presburger parsing unit tests --*- C++ -*-===//
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//
9// This file contains tests for parsing IntegerSets to IntegerPolyhedron.
10// The tests with invalid input check that the parser only accepts well-formed
11// IntegerSets. The tests with well-formed input compare the returned FACs to
12// manually constructed FACs with a PresburgerSet equality check.
13//
14//===----------------------------------------------------------------------===//
15
16#include "Parser.h"
17
18#include <gtest/gtest.h>
19
20using namespace mlir;
21using namespace presburger;
22
23/// Construct a IntegerPolyhedron from a set of inequality, equality, and
24/// division constraints.
25static IntegerPolyhedron makeFACFromConstraints(
26 unsigned dims, unsigned syms, ArrayRef<SmallVector<int64_t, 4>> ineqs,
27 ArrayRef<SmallVector<int64_t, 4>> eqs = {},
28 ArrayRef<std::pair<SmallVector<int64_t, 4>, int64_t>> divs = {}) {
29 IntegerPolyhedron fac(ineqs.size(), eqs.size(), dims + syms + 1,
30 PresburgerSpace::getSetSpace(numDims: dims, numSymbols: syms, numLocals: 0));
31 for (const auto &div : divs)
32 fac.addLocalFloorDiv(dividend: div.first, divisor: div.second);
33 for (const auto &eq : eqs)
34 fac.addEquality(eq);
35 for (const auto &ineq : ineqs)
36 fac.addInequality(inEq: ineq);
37 return fac;
38}
39
40/// Parses and compares the `str` to the `ex`. The equality check is performed
41/// by using PresburgerSet::isEqual
42static bool parseAndCompare(StringRef str, const IntegerPolyhedron &ex) {
43 IntegerPolyhedron poly = parseIntegerPolyhedron(str);
44 return PresburgerSet(poly).isEqual(set: PresburgerSet(ex));
45}
46
47TEST(ParseFACTest, ParseAndCompareTest) {
48 // simple ineq
49 EXPECT_TRUE(parseAndCompare("(x)[] : (x >= 0)",
50 makeFACFromConstraints(1, 0, {{1, 0}})));
51
52 // simple eq
53 EXPECT_TRUE(parseAndCompare("(x)[] : (x == 0)",
54 makeFACFromConstraints(1, 0, {}, {{1, 0}})));
55
56 // multiple constraints
57 EXPECT_TRUE(parseAndCompare("(x)[] : (7 * x >= 0, -7 * x + 5 >= 0)",
58 makeFACFromConstraints(1, 0, {{7, 0}, {-7, 5}})));
59
60 // multiple dimensions
61 EXPECT_TRUE(parseAndCompare("(x,y,z)[] : (x + y - z >= 0)",
62 makeFACFromConstraints(3, 0, {{1, 1, -1, 0}})));
63
64 // dimensions and symbols
65 EXPECT_TRUE(
66 parseAndCompare("(x,y,z)[a,b] : (x + y - z + 2 * a - 15 * b >= 0)",
67 makeFACFromConstraints(3, 2, {{1, 1, -1, 2, -15, 0}})));
68
69 // only symbols
70 EXPECT_TRUE(parseAndCompare("()[a] : (2 * a - 4 == 0)",
71 makeFACFromConstraints(0, 1, {}, {{2, -4}})));
72
73 // simple floordiv
74 EXPECT_TRUE(parseAndCompare(
75 "(x, y) : (y - 3 * ((x + y - 13) floordiv 3) - 42 == 0)",
76 makeFACFromConstraints(2, 0, {}, {{0, 1, -3, -42}}, {{{1, 1, -13}, 3}})));
77
78 // multiple floordiv
79 EXPECT_TRUE(parseAndCompare(
80 "(x, y) : (y - x floordiv 3 - y floordiv 2 == 0)",
81 makeFACFromConstraints(2, 0, {}, {{0, 1, -1, -1, 0}},
82 {{{1, 0, 0}, 3}, {{0, 1, 0, 0}, 2}})));
83
84 // nested floordiv
85 EXPECT_TRUE(parseAndCompare(
86 "(x, y) : (y - (x + y floordiv 2) floordiv 3 == 0)",
87 makeFACFromConstraints(2, 0, {}, {{0, 1, 0, -1, 0}},
88 {{{0, 1, 0}, 2}, {{1, 0, 1, 0}, 3}})));
89}
90

source code of mlir/unittests/Analysis/Presburger/ParserTest.cpp