Module: ppl/ppl Branch: master Commit: 1fec820348a7ebe1ebedd8c3d860ac04ed508f42 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1fec820348a7e...

Author: Enea Zaffanella zaffanella@cs.unipr.it Date: Sun Jul 12 09:18:13 2009 +0200

Added a first test for the deterministic timeout.

---

tests/Polyhedron/Makefile.am | 23 +++- tests/Polyhedron/weightwatch1.cc | 242 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 260 insertions(+), 5 deletions(-)

diff --git a/tests/Polyhedron/Makefile.am b/tests/Polyhedron/Makefile.am index 9a2acb0..99b75fa 100644 --- a/tests/Polyhedron/Makefile.am +++ b/tests/Polyhedron/Makefile.am @@ -644,6 +644,8 @@ memory1_SRCS = memory1.cc

watchdog1_SRCS = watchdog1.cc

+weightwatch1_SRCS = weightwatch1.cc + if !VALGRIND_TESTS_ENABLED VALGRIND_BRITTLE_TESTS = memory1

@@ -653,14 +655,25 @@ endif !VALGRIND_TESTS_ENABLED

if BUILD_WATCHDOG_LIBRARY -WATCHDOG_TESTS = watchdog1

-watchdog1_SOURCES = $(watchdog1_SRCS) -watchdog1_CPPFLAGS = \ +WATCHDOG_TESTS = \ +watchdog1 \ +weightwatch1 + +WATCHDOG_LIBRARY_CPPFLAGS = \ $(AM_CPPFLAGS) \ -I$(top_builddir)/Watchdog \ -I$(top_builddir)/Watchdog/src -watchdog1_LDADD = $(LDADD) $(top_builddir)/Watchdog/src/libpwl.la + +WATCHDOG_LIBRARY_LDADD = $(LDADD) $(top_builddir)/Watchdog/src/libpwl.la + +watchdog1_SOURCES = $(watchdog1_SRCS) +watchdog1_CPPFLAGS = $(WATCHDOG_LIBRARY_CPPFLAGS) +watchdog1_LDADD = $(WATCHDOG_LIBRARY_LDADD) + +weightwatch1_SOURCES = $(weightwatch1_SRCS) +weightwatch1_CPPFLAGS = $(WATCHDOG_LIBRARY_CPPFLAGS) +weightwatch1_LDADD = $(WATCHDOG_LIBRARY_LDADD)

endif BUILD_WATCHDOG_LIBRARY

@@ -674,7 +687,7 @@ XFAIL_TESTS =

check_PROGRAMS = $(TESTS) $(BUGS)

-EXTRA_DIST = $(memory1_SRCS) $(watchdog1_SRCS) +EXTRA_DIST = $(memory1_SRCS) $(watchdog1_SRCS) $(weightwatch1_SRCS)

BUGS =

diff --git a/tests/Polyhedron/weightwatch1.cc b/tests/Polyhedron/weightwatch1.cc new file mode 100644 index 0000000..1386131 --- /dev/null +++ b/tests/Polyhedron/weightwatch1.cc @@ -0,0 +1,242 @@ +/* Test the weightwatch (i.e., deterministic timeout) facility of the library. + Copyright (C) 2001-2009 Roberto Bagnara bagnara@cs.unipr.it + +This file is part of the Parma Polyhedra Library (PPL). + +The PPL is free software; you can redistribute it and/or modify it +under the terms of the GNU General Public License as published by the +Free Software Foundation; either version 3 of the License, or (at your +option) any later version. + +The PPL is distributed in the hope that it will be useful, but WITHOUT +ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or +FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +for more details. + +You should have received a copy of the GNU General Public License +along with this program; if not, write to the Free Software Foundation, +Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. + +For the most up-to-date information see the Parma Polyhedra Library +site: http://www.cs.unipr.it/ppl/ . */ + +#include "ppl_test.hh" +#include "pwl.hh" +#include <stdexcept> + +namespace { + +typedef +Parma_Watchdog_Library::Threshold_Watcher<Weightwatch_Traits> Weightwatch; + +template <> +Weightwatch::Initialize Weightwatch::initialize(0); + + +class Deterministic_Timeout + : virtual public std::exception, + public Parma_Polyhedra_Library::Throwable { +public: + const char* what() const throw() { + return "Deterministic timeout in weightwatch1.cc"; + } + + void throw_me() const { + throw *this; + } + + int priority() const { + return 0; + } + + ~Deterministic_Timeout() throw() { + } +}; + +void too_fat() { + throw Deterministic_Timeout(); +} + +bool test01() { + Variable A(0); + Variable B(1); + Variable C(2); + Variable D(3); + Variable E(4); + Variable F(5); + Variable G(6); + Variable H(7); + Variable I(8); + Variable J(9); + Variable K(10); + Variable L(11); + Variable M(12); + Variable N(13); + Variable O(14); + Variable P(15); + Variable Q(16); + Variable R(17); + + Constraint_System cs; + cs.insert(B + 8192*D - R == 0); + cs.insert(Q == 1); + cs.insert(B + 8192*D - P == 0); + cs.insert(O == 1); + cs.insert(B + 8192*D - I - 8192*N == 0); + cs.insert(I - M == 0); + cs.insert(L == 0); + cs.insert(B + 8192*D - I - 8192*K == 0); + cs.insert(J == 0); + cs.insert(H == 0); + cs.insert(D - G == 0); + cs.insert(B - F == 0); + cs.insert(E == 0); + cs.insert(C == 0); + cs.insert(A == 0); + // Blind relaxation of strict constraint B - I > 0. + cs.insert(B - I >= 0); + cs.insert(-B - 8192*D + I >= -67100672); + cs.insert(-B >= -8191); + cs.insert(I >= 0); + cs.insert(D >= 0); + + C_Polyhedron ph(cs); + print_constraints(ph, "*** ph ***"); + + try { + Weightwatch ww(400, too_fat); + // Thanks to the blind relaxation of the strict inequality constraint, + // polyhedron ph is easily seen to contain an integer point. + const bool contains = ph.contains_integer_point(); + nout << "\nph " << (contains ? "contains" : "does not contain") + << " an integer point" << endl; + return contains; + } + catch (const Deterministic_Timeout& e) { + // Unexpected timeout exception. + nout << e.what() << endl; + return false; + } + catch (...) { + // Unexpected exception. + return false; + } + // Should never get here. + return false; +} + +bool test02() { + Variable A(0); + Variable B(1); + Variable C(2); + Variable D(3); + Variable E(4); + Variable F(5); + Variable G(6); + Variable H(7); + Variable I(8); + Variable J(9); + Variable K(10); + Variable L(11); + Variable M(12); + Variable N(13); + Variable O(14); + Variable P(15); + Variable Q(16); + Variable R(17); + + Constraint_System cs; + cs.insert(B + 8192*D - R == 0); + cs.insert(Q == 1); + cs.insert(B + 8192*D - P == 0); + cs.insert(O == 1); + cs.insert(B + 8192*D - I - 8192*N == 0); + cs.insert(I - M == 0); + cs.insert(L == 0); + cs.insert(B + 8192*D - I - 8192*K == 0); + cs.insert(J == 0); + cs.insert(H == 0); + cs.insert(D - G == 0); + cs.insert(B - F == 0); + cs.insert(E == 0); + cs.insert(C == 0); + cs.insert(A == 0); + // Rewriting the strict constraint B - I > 0. + cs.insert(B - I >= 1); + cs.insert(-B - 8192*D + I >= -67100672); + cs.insert(-B >= -8191); + cs.insert(I >= 0); + cs.insert(D >= 0); + + C_Polyhedron ph(cs); + print_constraints(ph, "*** ph ***"); + + try { + Weightwatch ww(400, too_fat); + // The branch-and-bound heuristics of the MIP solver behaves badly + // on this particular example, causing timeout to expire. + const bool contains = ph.contains_integer_point(); + nout << "ph " << (contains ? "contains" : "does not contain") + << " an integer point" << endl; + return false; + } + catch (const Deterministic_Timeout& e) { + // Expected exception. + nout << e.what() << endl; + return true; + } + catch (...) { + // Unexpected exception. + return false; + } + // Should never get here. + return false; +} + +bool test03() { + Variable A(0); + Variable B(1); + Variable C(2); + Variable D(3); + + Constraint_System cs; + cs.insert(8192*A + B - 8192*C - D == 0); + cs.insert(D >= 0); + cs.insert(-B >= -8191); + cs.insert(B -D >= 1); + cs.insert(-B + 8192*C + D >= 0); + cs.insert(-C >= -8191); + + C_Polyhedron ph(cs); + print_constraints(ph, "*** ph ***"); + + try { + Weightwatch ww(400, too_fat); + // Polyhedron ph is the projection of the polyehdron of test01 + // onto a lower dimensional space: the performance issue of previous + // test does not depend on high dimension vector space. + const bool contains = ph.contains_integer_point(); + nout << "ph " << (contains ? "contains" : "does not contain") + << " an integer point" << endl; + return false; + } + catch (const Deterministic_Timeout& e) { + // Expected exception. + nout << e.what() << endl; + return true; + } + catch (...) { + // Unexpected exception. + return false; + } + // Should never get here. + return false; +} + +} // namespace + +BEGIN_MAIN + DO_TEST(test01); + DO_TEST(test02); + DO_TEST(test03); +END_MAIN