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