1 /* Test the weightwatch (i.e., deterministic timeout) facility of the library.
2 Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
3 Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com)
4
5 This file is part of the Parma Polyhedra Library (PPL).
6
7 The PPL is free software; you can redistribute it and/or modify it
8 under the terms of the GNU General Public License as published by the
9 Free Software Foundation; either version 3 of the License, or (at your
10 option) any later version.
11
12 The PPL is distributed in the hope that it will be useful, but WITHOUT
13 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
14 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
15 for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software Foundation,
19 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
20
21 For the most up-to-date information see the Parma Polyhedra Library
22 site: http://bugseng.com/products/ppl/ . */
23
24 #include "ppl_test.hh"
25 #include <stdexcept>
26
27 namespace {
28
29 typedef
30 Parma_Polyhedra_Library::Threshold_Watcher<Weightwatch_Traits> Weightwatch;
31
32 class Deterministic_Timeout
33 : virtual public std::exception,
34 public Parma_Polyhedra_Library::Throwable {
35 public:
what() const36 const char* what() const throw() {
37 return "deterministic timeout in weightwatch1.cc";
38 }
39
throw_me() const40 void throw_me() const {
41 throw *this;
42 }
43
priority() const44 int priority() const {
45 return 0;
46 }
47
~Deterministic_Timeout()48 ~Deterministic_Timeout() throw() {
49 }
50 };
51
too_fat()52 void too_fat() {
53 throw Deterministic_Timeout();
54 }
55
test01()56 bool test01() {
57 Variable A(0);
58 Variable B(1);
59 Variable C(2);
60 Variable D(3);
61 Variable E(4);
62 Variable F(5);
63 Variable G(6);
64 Variable H(7);
65 Variable I(8);
66 Variable J(9);
67 Variable K(10);
68 Variable L(11);
69 Variable M(12);
70 Variable N(13);
71 Variable O(14);
72 Variable P(15);
73 Variable Q(16);
74 Variable R(17);
75
76 Constraint_System cs;
77 cs.insert(B + 8192*D - R == 0);
78 cs.insert(Q == 1);
79 cs.insert(B + 8192*D - P == 0);
80 cs.insert(O == 1);
81 cs.insert(B + 8192*D - I - 8192*N == 0);
82 cs.insert(I - M == 0);
83 cs.insert(L == 0);
84 cs.insert(B + 8192*D - I - 8192*K == 0);
85 cs.insert(J == 0);
86 cs.insert(H == 0);
87 cs.insert(D - G == 0);
88 cs.insert(B - F == 0);
89 cs.insert(E == 0);
90 cs.insert(C == 0);
91 cs.insert(A == 0);
92 // Blind relaxation of strict constraint B - I > 0.
93 cs.insert(B - I >= 0);
94 cs.insert(-B - 8192*D + I >= -67100672);
95 cs.insert(-B >= -8191);
96 cs.insert(I >= 0);
97 cs.insert(D >= 0);
98
99 C_Polyhedron ph(cs);
100 print_constraints(ph, "*** ph ***");
101
102 try {
103 Weightwatch ww(5000000, too_fat);
104 // Thanks to the blind relaxation of the strict inequality constraint,
105 // polyhedron ph is easily seen to contain an integer point.
106 const bool contains = ph.contains_integer_point();
107 nout << endl << "ph "
108 << (contains ? "contains" : "does not contain")
109 << " an integer point" << endl;
110 return contains;
111 }
112 // Note: other exceptions are just propagated.
113 catch (const Deterministic_Timeout& e) {
114 // Unexpected timeout exception.
115 nout << endl << e.what() << endl;
116 return false;
117 }
118 // Should never get here.
119 return false;
120 }
121
test02()122 bool test02() {
123 Variable A(0);
124 Variable B(1);
125 Variable C(2);
126 Variable D(3);
127 Variable E(4);
128 Variable F(5);
129 Variable G(6);
130 Variable H(7);
131 Variable I(8);
132 Variable J(9);
133 Variable K(10);
134 Variable L(11);
135 Variable M(12);
136 Variable N(13);
137 Variable O(14);
138 Variable P(15);
139 Variable Q(16);
140 Variable R(17);
141
142 Constraint_System cs;
143 cs.insert(B + 8192*D - R == 0);
144 cs.insert(Q == 1);
145 cs.insert(B + 8192*D - P == 0);
146 cs.insert(O == 1);
147 cs.insert(B + 8192*D - I - 8192*N == 0);
148 cs.insert(I - M == 0);
149 cs.insert(L == 0);
150 cs.insert(B + 8192*D - I - 8192*K == 0);
151 cs.insert(J == 0);
152 cs.insert(H == 0);
153 cs.insert(D - G == 0);
154 cs.insert(B - F == 0);
155 cs.insert(E == 0);
156 cs.insert(C == 0);
157 cs.insert(A == 0);
158 // Rewriting the strict constraint B - I > 0.
159 cs.insert(B - I >= 1);
160 cs.insert(-B - 8192*D + I >= -67100672);
161 cs.insert(-B >= -8191);
162 cs.insert(I >= 0);
163 cs.insert(D >= 0);
164
165 C_Polyhedron ph(cs);
166 print_constraints(ph, "*** ph ***");
167
168 try {
169 Weightwatch ww(2500000, too_fat);
170 // The branch-and-bound heuristics of the MIP solver behaves badly
171 // on this particular example, causing timeout to expire.
172 const bool contains = ph.contains_integer_point();
173 nout << endl
174 << "ph " << (contains ? "contains" : "does not contain")
175 << " an integer point" << endl;
176 return false;
177 }
178 // Note: other exceptions are just propagated.
179 catch (const Deterministic_Timeout& e) {
180 // Expected exception.
181 nout << endl << e.what() << endl;
182 return true;
183 }
184 // Should never get here.
185 return false;
186 }
187
test03()188 bool test03() {
189 Variable A(0);
190 Variable B(1);
191 Variable C(2);
192 Variable D(3);
193
194 Constraint_System cs;
195 cs.insert(8192*A + B - 8192*C - D == 0);
196 cs.insert(D >= 0);
197 cs.insert(-B >= -8191);
198 cs.insert(B -D >= 1);
199 cs.insert(-B + 8192*C + D >= 0);
200 cs.insert(-C >= -8191);
201
202 C_Polyhedron ph(cs);
203 print_constraints(ph, "*** ph ***");
204
205 try {
206 Weightwatch ww(1000000000, too_fat);
207 // Polyhedron ph is the projection of the polyehdron of test01
208 // onto a lower dimensional space: the performance issue of previous
209 // test does not depend on high dimension vector space.
210 const bool contains = ph.contains_integer_point();
211 nout << endl
212 << "ph " << (contains ? "contains" : "does not contain")
213 << " an integer point" << endl;
214 return false;
215 }
216 // Note: other exceptions are just propagated.
217 catch (const Deterministic_Timeout& e) {
218 // Expected exception.
219 nout << endl << e.what() << endl;
220 return true;
221 }
222 // Should never get here.
223 return false;
224 }
225
226 } // namespace
227
228 BEGIN_MAIN
229 DO_TEST_F32(test01);
230 DO_TEST_F32(test02);
231 DO_TEST_F32(test03);
232 END_MAIN
233