xref: /llvm-project/llvm/unittests/Analysis/ConstraintSystemTest.cpp (revision 355dab0b5a9e464765b752e7f0ac53c24992cb4c)
1cd4edf94SFlorian Hahn //===--- ConstraintSystemTests.cpp ----------------------------------------===//
2cd4edf94SFlorian Hahn //
3cd4edf94SFlorian Hahn // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4cd4edf94SFlorian Hahn // See https://llvm.org/LICENSE.txt for license information.
5cd4edf94SFlorian Hahn // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6cd4edf94SFlorian Hahn //
7cd4edf94SFlorian Hahn //===----------------------------------------------------------------------===//
8cd4edf94SFlorian Hahn 
9cd4edf94SFlorian Hahn #include "llvm/Analysis/ConstraintSystem.h"
10cd4edf94SFlorian Hahn #include "gtest/gtest.h"
11cd4edf94SFlorian Hahn 
12cd4edf94SFlorian Hahn using namespace llvm;
13cd4edf94SFlorian Hahn 
14cd4edf94SFlorian Hahn namespace {
15cd4edf94SFlorian Hahn 
TEST(ConstraintSolverTest,TestSolutionChecks)16db22e70dSFlorian Hahn TEST(ConstraintSolverTest, TestSolutionChecks) {
17cd4edf94SFlorian Hahn   {
18cd4edf94SFlorian Hahn     ConstraintSystem CS;
19cd4edf94SFlorian Hahn     // x + y <= 10, x >= 5, y >= 6, x <= 10, y <= 10
20cd4edf94SFlorian Hahn     CS.addVariableRow({10, 1, 1});
21cd4edf94SFlorian Hahn     CS.addVariableRow({-5, -1, 0});
22cd4edf94SFlorian Hahn     CS.addVariableRow({-6, 0, -1});
23cd4edf94SFlorian Hahn     CS.addVariableRow({10, 1, 0});
24cd4edf94SFlorian Hahn     CS.addVariableRow({10, 0, 1});
25cd4edf94SFlorian Hahn 
26cd4edf94SFlorian Hahn     EXPECT_FALSE(CS.mayHaveSolution());
27cd4edf94SFlorian Hahn   }
28cd4edf94SFlorian Hahn 
29cd4edf94SFlorian Hahn   {
30cd4edf94SFlorian Hahn     ConstraintSystem CS;
31cd4edf94SFlorian Hahn     // x + y <= 10, x >= 2, y >= 3, x <= 10, y <= 10
32cd4edf94SFlorian Hahn     CS.addVariableRow({10, 1, 1});
33cd4edf94SFlorian Hahn     CS.addVariableRow({-2, -1, 0});
34cd4edf94SFlorian Hahn     CS.addVariableRow({-3, 0, -1});
35cd4edf94SFlorian Hahn     CS.addVariableRow({10, 1, 0});
36cd4edf94SFlorian Hahn     CS.addVariableRow({10, 0, 1});
37cd4edf94SFlorian Hahn 
38cd4edf94SFlorian Hahn     EXPECT_TRUE(CS.mayHaveSolution());
39cd4edf94SFlorian Hahn   }
40cd4edf94SFlorian Hahn 
41cd4edf94SFlorian Hahn   {
42cd4edf94SFlorian Hahn     ConstraintSystem CS;
43*355dab0bSAntonio Frighetto     // x + y <= 10, x >= 10, y >= 10; does not have a solution.
44cd4edf94SFlorian Hahn     CS.addVariableRow({10, 1, 1});
45cd4edf94SFlorian Hahn     CS.addVariableRow({-10, -1, 0});
46cd4edf94SFlorian Hahn     CS.addVariableRow({-10, 0, -1});
47cd4edf94SFlorian Hahn 
48cd4edf94SFlorian Hahn     EXPECT_FALSE(CS.mayHaveSolution());
49cd4edf94SFlorian Hahn   }
50cd4edf94SFlorian Hahn 
51cd4edf94SFlorian Hahn   {
52cd4edf94SFlorian Hahn     ConstraintSystem CS;
53cd4edf94SFlorian Hahn     // x + y >= 20, 10 >= x, 10 >= y; does HAVE a solution.
54cd4edf94SFlorian Hahn     CS.addVariableRow({-20, -1, -1});
55cd4edf94SFlorian Hahn     CS.addVariableRow({-10, -1, 0});
56cd4edf94SFlorian Hahn     CS.addVariableRow({-10, 0, -1});
57cd4edf94SFlorian Hahn 
58cd4edf94SFlorian Hahn     EXPECT_TRUE(CS.mayHaveSolution());
59cd4edf94SFlorian Hahn   }
60cd4edf94SFlorian Hahn 
61cd4edf94SFlorian Hahn   {
62cd4edf94SFlorian Hahn     ConstraintSystem CS;
63cd4edf94SFlorian Hahn 
64cd4edf94SFlorian Hahn     // 2x + y + 3z <= 10,  2x + y >= 10, y >= 1
65cd4edf94SFlorian Hahn     CS.addVariableRow({10, 2, 1, 3});
66cd4edf94SFlorian Hahn     CS.addVariableRow({-10, -2, -1, 0});
67cd4edf94SFlorian Hahn     CS.addVariableRow({-1, 0, 0, -1});
68cd4edf94SFlorian Hahn 
69cd4edf94SFlorian Hahn     EXPECT_FALSE(CS.mayHaveSolution());
70cd4edf94SFlorian Hahn   }
71cd4edf94SFlorian Hahn 
72cd4edf94SFlorian Hahn   {
73cd4edf94SFlorian Hahn     ConstraintSystem CS;
74cd4edf94SFlorian Hahn 
75cd4edf94SFlorian Hahn     // 2x + y + 3z <= 10,  2x + y >= 10
76cd4edf94SFlorian Hahn     CS.addVariableRow({10, 2, 1, 3});
77cd4edf94SFlorian Hahn     CS.addVariableRow({-10, -2, -1, 0});
78cd4edf94SFlorian Hahn 
79cd4edf94SFlorian Hahn     EXPECT_TRUE(CS.mayHaveSolution());
80cd4edf94SFlorian Hahn   }
81cd4edf94SFlorian Hahn }
82db22e70dSFlorian Hahn 
TEST(ConstraintSolverTest,IsConditionImplied)83db22e70dSFlorian Hahn TEST(ConstraintSolverTest, IsConditionImplied) {
84db22e70dSFlorian Hahn   {
85db22e70dSFlorian Hahn     // For the test below, we assume we know
86db22e70dSFlorian Hahn     // x <= 5 && y <= 3
87db22e70dSFlorian Hahn     ConstraintSystem CS;
88db22e70dSFlorian Hahn     CS.addVariableRow({5, 1, 0});
89db22e70dSFlorian Hahn     CS.addVariableRow({3, 0, 1});
90db22e70dSFlorian Hahn 
91db22e70dSFlorian Hahn     // x + y <= 6 does not hold.
92db22e70dSFlorian Hahn     EXPECT_FALSE(CS.isConditionImplied({6, 1, 1}));
93db22e70dSFlorian Hahn     // x + y <= 7 does not hold.
94db22e70dSFlorian Hahn     EXPECT_FALSE(CS.isConditionImplied({7, 1, 1}));
95db22e70dSFlorian Hahn     // x + y <= 8 does hold.
96db22e70dSFlorian Hahn     EXPECT_TRUE(CS.isConditionImplied({8, 1, 1}));
97db22e70dSFlorian Hahn 
98db22e70dSFlorian Hahn     // 2 * x + y <= 12 does hold.
99db22e70dSFlorian Hahn     EXPECT_FALSE(CS.isConditionImplied({12, 2, 1}));
100db22e70dSFlorian Hahn     // 2 * x + y <= 13 does hold.
101db22e70dSFlorian Hahn     EXPECT_TRUE(CS.isConditionImplied({13, 2, 1}));
102db22e70dSFlorian Hahn 
103db22e70dSFlorian Hahn     //  x + y <= 12 does hold.
104db22e70dSFlorian Hahn     EXPECT_FALSE(CS.isConditionImplied({12, 2, 1}));
105db22e70dSFlorian Hahn     // 2 * x + y <= 13 does hold.
106db22e70dSFlorian Hahn     EXPECT_TRUE(CS.isConditionImplied({13, 2, 1}));
107db22e70dSFlorian Hahn 
108db22e70dSFlorian Hahn     // x <= y == x - y <= 0 does not hold.
109db22e70dSFlorian Hahn     EXPECT_FALSE(CS.isConditionImplied({0, 1, -1}));
110db22e70dSFlorian Hahn     // y <= x == -x + y <= 0 does not hold.
111db22e70dSFlorian Hahn     EXPECT_FALSE(CS.isConditionImplied({0, -1, 1}));
112db22e70dSFlorian Hahn   }
113db22e70dSFlorian Hahn 
114db22e70dSFlorian Hahn   {
115db22e70dSFlorian Hahn     // For the test below, we assume we know
116db22e70dSFlorian Hahn     // x + 1 <= y + 1 == x - y <= 0
117db22e70dSFlorian Hahn     ConstraintSystem CS;
118db22e70dSFlorian Hahn     CS.addVariableRow({0, 1, -1});
119db22e70dSFlorian Hahn 
120db22e70dSFlorian Hahn     // x <= y == x - y <= 0 does hold.
121db22e70dSFlorian Hahn     EXPECT_TRUE(CS.isConditionImplied({0, 1, -1}));
122db22e70dSFlorian Hahn     // y <= x == -x + y <= 0 does not hold.
123db22e70dSFlorian Hahn     EXPECT_FALSE(CS.isConditionImplied({0, -1, 1}));
124db22e70dSFlorian Hahn 
125db22e70dSFlorian Hahn     // x <= y + 10 == x - y <= 10 does hold.
126db22e70dSFlorian Hahn     EXPECT_TRUE(CS.isConditionImplied({10, 1, -1}));
127db22e70dSFlorian Hahn     // x + 10 <= y == x - y <= -10 does NOT hold.
128db22e70dSFlorian Hahn     EXPECT_FALSE(CS.isConditionImplied({-10, 1, -1}));
129db22e70dSFlorian Hahn   }
130db22e70dSFlorian Hahn 
131db22e70dSFlorian Hahn   {
132db22e70dSFlorian Hahn     // For the test below, we assume we know
133db22e70dSFlorian Hahn     // x <= y == x - y <= 0
134db22e70dSFlorian Hahn     // y <= z == y - x <= 0
135db22e70dSFlorian Hahn     ConstraintSystem CS;
136db22e70dSFlorian Hahn     CS.addVariableRow({0, 1, -1, 0});
137db22e70dSFlorian Hahn     CS.addVariableRow({0, 0, 1, -1});
138db22e70dSFlorian Hahn 
139db22e70dSFlorian Hahn     // z <= y == -y + z <= 0 does not hold.
140db22e70dSFlorian Hahn     EXPECT_FALSE(CS.isConditionImplied({0, 0, -1, 1}));
141db22e70dSFlorian Hahn     // x <= z == x - z <= 0 does hold.
142db22e70dSFlorian Hahn     EXPECT_TRUE(CS.isConditionImplied({0, 1, 0, -1}));
143db22e70dSFlorian Hahn   }
144db22e70dSFlorian Hahn }
145db22e70dSFlorian Hahn 
TEST(ConstraintSolverTest,IsConditionImpliedOverflow)146db22e70dSFlorian Hahn TEST(ConstraintSolverTest, IsConditionImpliedOverflow) {
147db22e70dSFlorian Hahn   ConstraintSystem CS;
148db22e70dSFlorian Hahn   // Make sure isConditionImplied returns false when there is an overflow.
149db22e70dSFlorian Hahn   int64_t Limit = std::numeric_limits<int64_t>::max();
150db22e70dSFlorian Hahn   CS.addVariableRow({Limit - 1, Limit - 2, Limit - 3});
151db22e70dSFlorian Hahn   EXPECT_FALSE(CS.isConditionImplied({Limit - 1, Limit - 2, Limit - 3}));
152db22e70dSFlorian Hahn }
153cd4edf94SFlorian Hahn } // namespace
154