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

Author: Roberto Bagnara bagnara@cs.unipr.it Date: Sat Apr 7 18:41:48 2012 +0200

New test program.

---

tests/PIP_Problem/Makefile.am | 5 +- tests/PIP_Problem/{bug1.cc => weightwatch1.cc} | 71 ++++++++++++++++++++++- 2 files changed, 71 insertions(+), 5 deletions(-)

diff --git a/tests/PIP_Problem/Makefile.am b/tests/PIP_Problem/Makefile.am index 1d7bc47..8bab0f7 100644 --- a/tests/PIP_Problem/Makefile.am +++ b/tests/PIP_Problem/Makefile.am @@ -54,7 +54,8 @@ $(top_builddir)/src/libppl.la \ TESTS = \ ascii_dump_load1 \ exceptions1 \ -pipproblem1 pipproblem2 pipproblem3 +pipproblem1 pipproblem2 pipproblem3 \ +weightwatch1

XFAIL_TESTS =

@@ -72,6 +73,8 @@ pipproblem1_SOURCES = pipproblem1.cc pipproblem2_SOURCES = pipproblem2.cc pipproblem3_SOURCES = pipproblem3.cc

+weightwatch1_SOURCES = weightwatch1.cc + check_PROGRAMS = \ $(TESTS) \ $(BUGS) diff --git a/tests/PIP_Problem/bug1.cc b/tests/PIP_Problem/weightwatch1.cc similarity index 63% rename from tests/PIP_Problem/bug1.cc rename to tests/PIP_Problem/weightwatch1.cc index 76c7f68..653d129 100644 --- a/tests/PIP_Problem/bug1.cc +++ b/tests/PIP_Problem/weightwatch1.cc @@ -1,4 +1,4 @@ -/* Reproduce Mantis issue [PPL 0000353]. +/* Test PIP_Problem (and MIP_Problem) with respect to deterministic timeouts. Copyright (C) 2001-2010 Roberto Bagnara bagnara@cs.unipr.it Copyright (C) 2010-2012 BUGSENG srl (http://bugseng.com)

@@ -33,6 +33,33 @@ using std::ios_base;

namespace {

+typedef +Parma_Polyhedra_Library::Threshold_Watcher<Weightwatch_Traits> Weightwatch; + +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); @@ -109,12 +136,48 @@ test01() { cs.insert(O >= 0); cs.insert(H >= 0);

- PIP_Problem pip(cs.space_dimension(), cs.begin(), cs.end(), params); + try { + PIP_Problem pip(cs.space_dimension(), cs.begin(), cs.end(), params); + + Weightwatch ww(200000000, too_fat);

- if (pip.is_satisfiable()) + (void) pip.is_satisfiable(); + + // Should not get there. + return false; + } + // Note: other exceptions are just propagated. + catch (const Deterministic_Timeout& e) { + // Expected timeout exception. + nout << endl << e.what() << endl; + + try { + MIP_Problem mip(cs.space_dimension(), cs.begin(), cs.end(), params); + // Set all variable to be constrained to have an integer value. + mip.add_to_integer_space_dimensions(Variables_Set(A, F1)); + + Weightwatch ww(4000000, too_fat); + + if (mip.is_satisfiable()) { + nout << "mip is satisfiable?!" << endl; + return false; + } + + return true; + } + // Note: other exceptions are just propagated. + catch (const Deterministic_Timeout& e) { + // Unexpected timeout exception. + nout << endl << e.what() << endl; + return false; + } + + // Should never get here. return false; + }

- return true; + // Should never get here. + return false; }

} // namespace