1 /* Test Pointset_Powerset<PH>::BGP99_extrapolation_assign().
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 <vector>
26
27 namespace {
28
29 const C_Polyhedron&
aux1_test01(unsigned n)30 aux1_test01(unsigned n) {
31 Variable x(0);
32 Variable y(1);
33
34 static std::vector<C_Polyhedron> p;
35 if (p.size() < 5) {
36 p.resize(5, C_Polyhedron(2));
37 p[2].add_constraint(0 <= x);
38 p[2].add_constraint(x <= 4);
39 p[2].add_constraint(0 <= y);
40 p[2].add_constraint(y <= 4);
41 p[1] = p[2];
42 p[1].add_constraint(x-y <= 3);
43 p[0] = p[1];
44 p[0].add_constraint(x+y >= 1);
45
46 p[3].add_constraint(0 <= x);
47 p[3].add_constraint(x <= 8);
48 p[3].add_constraint(0 <= y);
49 p[3].add_constraint(y <= 8);
50 p[3].add_constraint(x+y <= 14);
51 p[3].add_constraint(x-y >= -6);
52 p[4] = p[3];
53 p[3].add_constraint(5*x-y >= -2);
54 p[3].add_constraint(x+3*y >= 3);
55 p[4].add_constraint(4*x-y >= -3);
56 p[4].add_constraint(x+2*y >= 2);
57 }
58
59 if (n >= p.size()) {
60 unsigned new_size = p.size();
61 while (n >= new_size)
62 new_size *= 2;
63 p.resize(p.size()*2);
64 }
65
66 if (p[n].is_universe()) {
67 p[n] = aux1_test01(n-4);
68 p[n].affine_image(x, 2*x);
69 p[n].affine_image(y, 8 - 2*y);
70 }
71
72 return p[n];
73 }
74
75 Pointset_Powerset<C_Polyhedron>
aux2_test01(unsigned n)76 aux2_test01(unsigned n) {
77 Pointset_Powerset<C_Polyhedron> s(2, EMPTY);
78 if (n == 0) {
79
80 nout << "S0 = { P0 }" << endl;
81
82 s.add_disjunct(aux1_test01(0));
83 return s;
84 }
85
86 const int p_base = (n-1)/3*4;
87
88 switch (n % 3) {
89 case 1:
90
91 nout << "S" << n << " = { "
92 << "P" << p_base + 1 << ", "
93 << "P" << p_base + 3 << " }" << endl;
94
95 s.add_disjunct(aux1_test01(p_base + 1));
96 s.add_disjunct(aux1_test01(p_base + 3));
97 break;
98 case 2:
99
100 nout << "S" << n << " = { "
101 << "P" << p_base + 2 << ", "
102 << "P" << p_base + 3 << " }" << endl;
103
104 s.add_disjunct(aux1_test01(p_base + 2));
105 s.add_disjunct(aux1_test01(p_base + 3));
106 break;
107 case 0:
108
109 nout << "S" << n << " = { "
110 << "P" << p_base + 2 << ", "
111 << "P" << p_base + 4 << " }" << endl;
112
113 s.add_disjunct(aux1_test01(p_base + 2));
114 s.add_disjunct(aux1_test01(p_base + 4));
115 break;
116 }
117 return s;
118 }
119
120 void
aux3_test01(std::ostream & s,const Variable v)121 aux3_test01(std::ostream& s, const Variable v) {
122 s << char('x' + v.id());
123 }
124
125 bool
test01()126 test01() {
127 // Install the alternate output function.
128 Variable::set_output_function(aux3_test01);
129
130 Pointset_Powerset<C_Polyhedron> T = aux2_test01(0);
131
132 using namespace Parma_Polyhedra_Library::IO_Operators;
133
134 nout << "T0 = " << T << endl;
135
136 bool converged = false;
137 for (unsigned n = 1; !converged && n <= 20; ++n) {
138 Pointset_Powerset<C_Polyhedron> Sn = aux2_test01(n);
139
140 nout << "S" << n << " = " << Sn << endl;
141
142 Sn.BGP99_extrapolation_assign
143 (T, widen_fun_ref(&Polyhedron::H79_widening_assign), 2);
144
145 nout << "T" << n << " = " << Sn << endl;
146
147 if (Sn.definitely_entails(T))
148 converged = true;
149 else
150 swap(Sn, T);
151 }
152
153 return !converged;
154 }
155
156 } // namespace
157
158 BEGIN_MAIN
159 DO_TEST_F16(test01);
160 END_MAIN
161