[PPL-devel] [GIT] ppl/ppl(master): The given problem is not satisfiable ( independently verified with other solvers).

Roberto Bagnara bagnara at cs.unipr.it
Fri Apr 6 09:04:13 CEST 2012


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

Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date:   Fri Apr  6 09:03:08 2012 +0200

The given problem is not satisfiable (independently verified with other solvers).

---

 tests/PIP_Problem/bug1.cc |   14 +++-----------
 1 files changed, 3 insertions(+), 11 deletions(-)

diff --git a/tests/PIP_Problem/bug1.cc b/tests/PIP_Problem/bug1.cc
index cc79299..76c7f68 100644
--- a/tests/PIP_Problem/bug1.cc
+++ b/tests/PIP_Problem/bug1.cc
@@ -25,7 +25,6 @@ site: http://bugseng.com/products/ppl/ . */
 
 #include "files.hh"
 #include <fstream>
-#include <iostream>
 
 using namespace IO_Operators;
 
@@ -110,19 +109,12 @@ test01() {
   cs.insert(O >= 0);
   cs.insert(H >= 0);
 
-#if 0
-  MIP_Problem mip(cs.space_dimension(), cs.begin(), cs.end());
-  std::cout << mip.is_satisfiable() << endl;
-  Variables_Set integer_space_dimensions(A, F1);
-  mip.add_to_integer_space_dimensions(integer_space_dimensions);
-  std::cout << mip.is_satisfiable() << endl;
-#endif
-
   PIP_Problem pip(cs.space_dimension(), cs.begin(), cs.end(), params);
 
-  bool ok = pip.is_satisfiable();
+  if (pip.is_satisfiable())
+    return false;
 
-  return ok;
+  return true;
 }
 
 } // namespace




More information about the PPL-devel mailing list