148 lines · cpp
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-exception6//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-formed11// IntegerSets. The tests with well-formed input compare the returned FACs to12// 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, and24/// 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(dims, syms, 0));31 for (const auto &div : divs)32 fac.addLocalFloorDiv(div.first, div.second);33 for (const auto &eq : eqs)34 fac.addEquality(eq);35 for (const auto &ineq : ineqs)36 fac.addInequality(ineq);37 return fac;38}39 40/// Parses and compares the `str` to the `ex`. The equality check is performed41/// by using PresburgerSet::isEqual42static bool parseAndCompare(StringRef str, const IntegerPolyhedron &ex) {43 IntegerPolyhedron poly = parseIntegerPolyhedron(str);44 return PresburgerSet(poly).isEqual(PresburgerSet(ex));45}46 47TEST(ParseFACTest, ParseAndCompareTest) {48 // constant-fold addition49 EXPECT_TRUE(parseAndCompare("() : (4 + 3 >= 0)",50 makeFACFromConstraints(0, 0, {}, {})));51 52 // constant-fold addition + multiplication53 EXPECT_TRUE(parseAndCompare("()[a] : (4 * 3 == 10 + 2)",54 makeFACFromConstraints(0, 1, {}, {})));55 56 // constant-fold ceildiv + floordiv57 EXPECT_TRUE(parseAndCompare("(x) : (11 ceildiv 3 == 13 floordiv 3)",58 makeFACFromConstraints(1, 0, {}, {})));59 60 // simple ineq61 EXPECT_TRUE(parseAndCompare("(x)[] : (x >= 0)",62 makeFACFromConstraints(1, 0, {{1, 0}})));63 64 // simple eq65 EXPECT_TRUE(parseAndCompare("(x)[] : (x == 0)",66 makeFACFromConstraints(1, 0, {}, {{1, 0}})));67 68 // multiple constraints69 EXPECT_TRUE(parseAndCompare("(x)[] : (7 * x >= 0, -7 * x + 5 >= 0)",70 makeFACFromConstraints(1, 0, {{7, 0}, {-7, 5}})));71 72 // multiplication distribution73 EXPECT_TRUE(74 parseAndCompare("(x) : (2 * x >= 2, (-7 + x * 9) * 5 >= 0)",75 makeFACFromConstraints(1, 0, {{2, -2}, {45, -35}})));76 77 // multiple dimensions78 EXPECT_TRUE(parseAndCompare("(x,y,z)[] : (x + y - z >= 0)",79 makeFACFromConstraints(3, 0, {{1, 1, -1, 0}})));80 81 // dimensions and symbols82 EXPECT_TRUE(83 parseAndCompare("(x,y,z)[a,b] : (x + y - z + 2 * a - 15 * b >= 0)",84 makeFACFromConstraints(3, 2, {{1, 1, -1, 2, -15, 0}})));85 86 // only symbols87 EXPECT_TRUE(parseAndCompare("()[a] : (2 * a - 4 == 0)",88 makeFACFromConstraints(0, 1, {}, {{2, -4}})));89 90 // no linear terms91 EXPECT_TRUE(parseAndCompare(92 "(x, y) : (26 * (x floordiv 6) == y floordiv 3)",93 makeFACFromConstraints(2, 0, {}, {{0, 0, 26, -1, 0}},94 {{{1, 0, 0}, 6}, {{0, 1, 0, 0}, 3}})));95 96 // simple floordiv97 EXPECT_TRUE(parseAndCompare(98 "(x, y) : (y - 3 * ((x + y - 13) floordiv 3) - 42 == 0)",99 makeFACFromConstraints(2, 0, {}, {{0, 1, -3, -42}}, {{{1, 1, -13}, 3}})));100 101 // simple ceildiv102 EXPECT_TRUE(parseAndCompare(103 "(x, y) : (y - 3 * ((x + y - 13) ceildiv 3) - 42 == 0)",104 makeFACFromConstraints(2, 0, {}, {{0, 1, -3, -42}}, {{{1, 1, -11}, 3}})));105 106 // simple mod107 EXPECT_TRUE(parseAndCompare(108 "(x, y) : (y - 3 * ((x + y - 13) mod 3) - 42 == 0)",109 makeFACFromConstraints(2, 0, {}, {{-3, -2, 9, -3}}, {{{1, 1, -13}, 3}})));110 111 // multiple floordiv112 EXPECT_TRUE(parseAndCompare(113 "(x, y) : (y - x floordiv 3 - y floordiv 2 == 0)",114 makeFACFromConstraints(2, 0, {}, {{0, 1, -1, -1, 0}},115 {{{1, 0, 0}, 3}, {{0, 1, 0, 0}, 2}})));116 117 // multiple ceildiv118 EXPECT_TRUE(parseAndCompare(119 "(x, y) : (y - x ceildiv 3 - y ceildiv 2 == 0)",120 makeFACFromConstraints(2, 0, {}, {{0, 1, -1, -1, 0}},121 {{{1, 0, 2}, 3}, {{0, 1, 0, 1}, 2}})));122 123 // multiple mod124 EXPECT_TRUE(parseAndCompare(125 "(x, y) : (y - x mod 3 - y mod 2 == 0)",126 makeFACFromConstraints(2, 0, {}, {{-1, 0, 3, 2, 0}},127 {{{1, 0, 0}, 3}, {{0, 1, 0, 0}, 2}})));128 129 // nested floordiv130 EXPECT_TRUE(parseAndCompare(131 "(x, y) : (y - (x + y floordiv 2) floordiv 3 == 0)",132 makeFACFromConstraints(2, 0, {}, {{0, 1, 0, -1, 0}},133 {{{0, 1, 0}, 2}, {{1, 0, 1, 0}, 3}})));134 135 // nested mod136 EXPECT_TRUE(parseAndCompare(137 "(x, y) : (y - (x + y mod 2) mod 3 == 0)",138 makeFACFromConstraints(2, 0, {}, {{-1, 0, 2, 3, 0}},139 {{{0, 1, 0}, 2}, {{1, 1, -2, 0}, 3}})));140 141 // nested floordiv + ceildiv + mod142 EXPECT_TRUE(parseAndCompare(143 "(x, y) : ((2 * x + 3 * (y floordiv 2) + x mod 7 + 1) ceildiv 3 == 42)",144 makeFACFromConstraints(145 2, 0, {}, {{0, 0, 0, 0, 1, -42}},146 {{{0, 1, 0}, 2}, {{1, 0, 0, 0}, 7}, {{3, 0, 3, -7, 3}, 3}})));147}148