|
207
|
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({10, 1, 1});
|
|
|
21 CS.addVariableRow({-5, -1, 0});
|
|
|
22 CS.addVariableRow({-6, 0, -1});
|
|
|
23 CS.addVariableRow({10, 1, 0});
|
|
|
24 CS.addVariableRow({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({10, 1, 1});
|
|
|
33 CS.addVariableRow({-2, -1, 0});
|
|
|
34 CS.addVariableRow({-3, 0, -1});
|
|
|
35 CS.addVariableRow({10, 1, 0});
|
|
|
36 CS.addVariableRow({10, 0, 1});
|
|
|
37
|
|
|
38 EXPECT_TRUE(CS.mayHaveSolution());
|
|
|
39 }
|
|
|
40
|
|
|
41 {
|
|
|
42 ConstraintSystem CS;
|
|
|
43 // x + y <= 10, 10 >= x, 10 >= y; does not have a solution.
|
|
|
44 CS.addVariableRow({10, 1, 1});
|
|
|
45 CS.addVariableRow({-10, -1, 0});
|
|
|
46 CS.addVariableRow({-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({-20, -1, -1});
|
|
|
55 CS.addVariableRow({-10, -1, 0});
|
|
|
56 CS.addVariableRow({-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({10, 2, 1, 3});
|
|
|
66 CS.addVariableRow({-10, -2, -1, 0});
|
|
|
67 CS.addVariableRow({-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({10, 2, 1, 3});
|
|
|
77 CS.addVariableRow({-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({5, 1, 0});
|
|
|
89 CS.addVariableRow({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({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({0, 1, -1, 0});
|
|
|
137 CS.addVariableRow({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({Limit - 1, Limit - 2, Limit - 3});
|
|
|
151 EXPECT_FALSE(CS.isConditionImplied({Limit - 1, Limit - 2, Limit - 3}));
|
|
|
152 }
|
|
|
153 } // namespace
|
