[PPL-devel] [GIT] ppl/ppl(master): New test program.

[Roberto Bagnara]

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

Author: Roberto Bagnara <bagnara at 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 at 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