1 /* Test Pointset_Powerset<PH>::definitely_entails().
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
26 namespace {
27
28 // Powerset of polyhedra: definitely_entails().
29 bool
test01()30 test01() {
31 Variable x(0);
32 Pointset_Powerset<C_Polyhedron> c_ps(1, EMPTY);
33 Constraint_System cs;
34 cs.insert(x >= 0);
35 c_ps.add_disjunct(C_Polyhedron(cs));
36
37 Pointset_Powerset<C_Polyhedron> c_ps1(1, EMPTY);
38 Constraint_System cs1;
39 cs1.insert(x >= 0);
40 cs1.insert(x <= 2);
41 c_ps1.add_disjunct(C_Polyhedron(cs1));
42
43 bool ok = c_ps1.definitely_entails(c_ps);
44
45 return ok;
46 }
47
48 // Powerset of boxes: definitely_entails().
49 bool
test02()50 test02() {
51 Variable x(0);
52 Pointset_Powerset<TBox> pps_box(1, EMPTY);
53 Constraint_System cs;
54 cs.insert(x >= 0);
55 pps_box.add_disjunct(TBox(cs));
56
57 Pointset_Powerset<TBox> pps_box1(1, EMPTY);
58 Constraint_System cs1;
59 cs1.insert(x >= 0);
60 cs1.insert(x <= 2);
61 pps_box1.add_disjunct(TBox(cs1));
62
63 bool ok = pps_box1.definitely_entails(pps_box);
64
65 return ok;
66 }
67
68 } // namespace
69
70 BEGIN_MAIN
71 DO_TEST(test01);
72 DO_TEST(test02);
73 END_MAIN
74