April 2012 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(master): Added a comment to clarify definition of PPL_ASSERT.
by Enea Zaffanella 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: 81a68dd16a56d4c8d7072081fa10d51a3af78cf0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=81a68dd16a56… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Apr 6 16:48:59 2012 +0200 Added a comment to clarify definition of PPL_ASSERT. --- src/assert.hh | 4 ++++ 1 files changed, 4 insertions(+), 0 deletions(-) diff --git a/src/assert.hh b/src/assert.hh index 3039b77..5b0a65a 100644 --- a/src/assert.hh +++ b/src/assert.hh @@ -53,6 +53,7 @@ site: http://bugseng.com/products/ppl/ . */ // Non zero to detect use of PPL_ASSERT instead of PPL_ASSERT_HEAVY +// Note: flag does not affect code built with NDEBUG defined. #define PPL_DEBUG_PPL_ASSERT 1 // The PPL_ASSERT macro states that Boolean condition cond__ should hold. @@ -60,6 +61,9 @@ site: http://bugseng.com/products/ppl/ . */ #if defined(NDEBUG) || (!PPL_DEBUG_PPL_ASSERT) #define PPL_ASSERT(cond__) PPL_ASSERT_IMPL_(cond__) #else +// Note: here we have assertions enabled and PPL_DEBUG_PPL_ASSERT is 1. +// Check if the call to PPL_ASSERT should be replaced by PPL_ASSERT_HEAVY +// (i.e., if the former may interfere with computational weights). #define PPL_ASSERT(cond__) \ do { \ typedef Parma_Polyhedra_Library::Weightwatch_Traits W_Traits; \

1 0

[GIT] ppl/ppl(master): Improved error message reporting for assertion failures.
by Enea Zaffanella 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: 488490ab24f427266b6c305a0c48ecc42ddcf4d4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=488490ab24f4… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Apr 6 16:38:44 2012 +0200 Improved error message reporting for assertion failures. --- src/assert.cc | 8 ++++++++ src/assert.hh | 38 +++++++++++++++++++++++++------------- 2 files changed, 33 insertions(+), 13 deletions(-) diff --git a/src/assert.cc b/src/assert.cc index c9d756a..926539c 100644 --- a/src/assert.cc +++ b/src/assert.cc @@ -42,3 +42,11 @@ PPL::ppl_unreachable_msg(const char* msg, abort(); } +void +PPL::ppl_assertion_failed(const char* assertion_text, + const char* file, unsigned int line, + const char* function) { + std::cerr << file << ":" << line << ": " << function + << ": Assertion `" << assertion_text << "' failed\n"; + abort(); +} diff --git a/src/assert.hh b/src/assert.hh index 35c2ef1..3039b77 100644 --- a/src/assert.hh +++ b/src/assert.hh @@ -36,6 +36,11 @@ site: http://bugseng.com/products/ppl/ . */ // The PPL_UNREACHABLE macro flags a program point as unreachable. #define PPL_UNREACHABLE PPL_UNREACHABLE_MSG("unreachable") +// The PPL_ASSERTION_FAILED macro is used to output a message after +// an assertion failure and then cause program termination. +// (It is meant to be used only when assertions are turned on). +#define PPL_ASSERTION_FAILED(msg__) Parma_Polyhedra_Library:: \ + ppl_assertion_failed(msg__, __FILE__, __LINE__, __func__) // Helper macro PPL_ASSERT_IMPL_: do not use it directly. #if defined(NDEBUG) @@ -43,7 +48,7 @@ site: http://bugseng.com/products/ppl/ . */ #else #define PPL_STRING_(s) #s #define PPL_ASSERT_IMPL_(cond__) \ - ((cond__) ? (void) 0 : PPL_UNREACHABLE_MSG(PPL_STRING_(cond__))) + ((cond__) ? (void) 0 : PPL_ASSERTION_FAILED(PPL_STRING_(cond__))) #endif @@ -90,17 +95,18 @@ site: http://bugseng.com/products/ppl/ . */ namespace Parma_Polyhedra_Library { -#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS -//! Helper function causing program termination by calling \c abort. -#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) -void ppl_unreachable() #if PPL_CXX_SUPPORTS_ATTRIBUTE_WEAK - __attribute__((weak, noreturn)); +#define PPL_WEAK_NORETURN __attribute__((weak, noreturn)) #else - __attribute__((noreturn)); +#define PPL_WEAK_NORETURN __attribute__((noreturn)) #endif #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS +//! Helper function causing program termination by calling \c abort. +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) +void ppl_unreachable() PPL_WEAK_NORETURN; + +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS /*! \brief Helper function printing message on \c std::cerr and causing program termination by calling \c abort. @@ -108,12 +114,18 @@ void ppl_unreachable() #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) void ppl_unreachable_msg(const char* msg, const char* file, unsigned int line, - const char* function) -#if PPL_CXX_SUPPORTS_ATTRIBUTE_WEAK - __attribute__((weak, noreturn)); -#else - __attribute__((noreturn)); -#endif + const char* function) PPL_WEAK_NORETURN; + +#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS +/*! \brief + Helper function printing an assertion failure message on \c std::cerr + and causing program termination by calling \c abort. +*/ +#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) +void ppl_assertion_failed(const char* assertion_text, + const char* file, unsigned int line, + const char* function) PPL_WEAK_NORETURN; + #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS /*! \brief

1 0

[GIT] ppl/ppl(master): Reordered so as to allow compilability with -DPPL_PROFILE_ADD_WEIGHT=1.
by Roberto Bagnara 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: fb4ff186479c5cd0a16838439b7b9743c9c10292 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=fb4ff186479c… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Apr 6 12:13:14 2012 +0200 Reordered so as to allow compilability with -DPPL_PROFILE_ADD_WEIGHT=1. --- src/globals.defs.hh | 94 ++++++++++++++++++++++++++------------------------- 1 files changed, 48 insertions(+), 46 deletions(-) diff --git a/src/globals.defs.hh b/src/globals.defs.hh index c0b3733..53815ef 100644 --- a/src/globals.defs.hh +++ b/src/globals.defs.hh @@ -32,9 +32,6 @@ site: http://bugseng.com/products/ppl/ . */ #include <exception> #include <gmpxx.h> -#if defined(NDEBUG) && PPL_PROFILE_ADD_WEIGHT -#include "Weight_Profiler.defs.hh" -#endif namespace Parma_Polyhedra_Library { @@ -143,49 +140,6 @@ extern unsigned int in_assert; } // namespace Implementation #endif -#ifndef PPL_PROFILE_ADD_WEIGHT -#define PPL_PROFILE_ADD_WEIGHT 0 -#endif - -#if defined(NDEBUG) -#if PPL_PROFILE_ADD_WEIGHT -#define WEIGHT_BEGIN() Weight_Profiler::begin() -#define WEIGHT_ADD(delta) \ - do { \ - static Weight_Profiler wp__(__FILE__, __LINE__, delta); \ - wp__.end(); \ - } while (false) -#define WEIGHT_ADD_MUL(delta, factor) \ - do { \ - static Weight_Profiler wp__(__FILE__, __LINE__, delta); \ - wp__.end(factor); \ - } while (false) -#else -#define WEIGHT_BEGIN() \ - do { \ - } while (false) -#define WEIGHT_ADD(delta) \ - do { \ - Weightwatch_Traits::weight += (delta); \ - } while (false) -#define WEIGHT_ADD_MUL(delta, factor) \ - do { \ - Weightwatch_Traits::weight += (delta)*(factor); \ - } while (false) -#endif -#else -#define WEIGHT_BEGIN() -#define WEIGHT_ADD(delta) \ - do { \ - if (Implementation::in_assert == 0) \ - Weightwatch_Traits::weight += delta; \ - } while (false) -#define WEIGHT_ADD_MUL(delta, factor) \ - do { \ - if (Implementation::in_assert == 0) \ - Weightwatch_Traits::weight += delta * factor; \ - } while (false) -#endif //! User objects the PPL can throw. /*! \ingroup PPL_CXX_interface @@ -515,6 +469,54 @@ least_significant_one_mask(dimension_type i); #define PPL_USE_SPARSE_MATRIX 1 #endif +#ifndef PPL_PROFILE_ADD_WEIGHT +#define PPL_PROFILE_ADD_WEIGHT 0 +#endif + +#if defined(NDEBUG) && PPL_PROFILE_ADD_WEIGHT +#include "Weight_Profiler.defs.hh" +#endif + +#if defined(NDEBUG) +#if PPL_PROFILE_ADD_WEIGHT +#define WEIGHT_BEGIN() Weight_Profiler::begin() +#define WEIGHT_ADD(delta) \ + do { \ + static Weight_Profiler wp__(__FILE__, __LINE__, delta); \ + wp__.end(); \ + } while (false) +#define WEIGHT_ADD_MUL(delta, factor) \ + do { \ + static Weight_Profiler wp__(__FILE__, __LINE__, delta); \ + wp__.end(factor); \ + } while (false) +#else +#define WEIGHT_BEGIN() \ + do { \ + } while (false) +#define WEIGHT_ADD(delta) \ + do { \ + Weightwatch_Traits::weight += (delta); \ + } while (false) +#define WEIGHT_ADD_MUL(delta, factor) \ + do { \ + Weightwatch_Traits::weight += (delta)*(factor); \ + } while (false) +#endif +#else +#define WEIGHT_BEGIN() +#define WEIGHT_ADD(delta) \ + do { \ + if (Implementation::in_assert == 0) \ + Weightwatch_Traits::weight += delta; \ + } while (false) +#define WEIGHT_ADD_MUL(delta, factor) \ + do { \ + if (Implementation::in_assert == 0) \ + Weightwatch_Traits::weight += delta * factor; \ + } while (false) +#endif + #include "globals.inlines.hh" #endif // !defined(PPL_globals_defs_hh)

1 0

[GIT] ppl/ppl(master): Reference to no longer existing namespace removed.
by Roberto Bagnara 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: 04e4cfbf6a817a734047d14319aa91f64e2c2183 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=04e4cfbf6a81… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Apr 6 12:11:56 2012 +0200 Reference to no longer existing namespace removed. (Wonder why we did not have a Doxygen warning.) --- src/Threshold_Watcher.defs.hh | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Threshold_Watcher.defs.hh b/src/Threshold_Watcher.defs.hh index c68ae79..4896adc 100644 --- a/src/Threshold_Watcher.defs.hh +++ b/src/Threshold_Watcher.defs.hh @@ -34,7 +34,7 @@ site: http://bugseng.com/products/ppl/ . */ \tparam Traits A class to set data types and functions for the threshold handling. - See \c Parma_Polyhedra_Library::Watchdog::Weightwatch_Traits for an example. + See \c Parma_Polyhedra_Library::Weightwatch_Traits for an example. */ template <typename Traits> class Parma_Polyhedra_Library::Threshold_Watcher { @@ -80,7 +80,7 @@ private: //! Check threshold reaching. static void check(); -}; // class Parma_Polyhedra_Library::Watchdog::Threshold_Watcher +}; // class Parma_Polyhedra_Library::Threshold_Watcher // Templatic initialization of static data member.

1 0

[GIT] ppl/ppl(master): Variable name fixed.
by Roberto Bagnara 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: 34fa558e18b00b28060b8da6ae6004c891440050 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=34fa558e18b0… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Apr 6 12:12:45 2012 +0200 Variable name fixed. --- src/Weight_Profiler.cc | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Weight_Profiler.cc b/src/Weight_Profiler.cc index 064a6d3..75c2795 100644 --- a/src/Weight_Profiler.cc +++ b/src/Weight_Profiler.cc @@ -47,7 +47,7 @@ void Weight_Profiler::output_stats() { << " max( " << stat[VALID].max << ")" << " average(" << average << ")"; std::cout << " variance( " << variance << ")" - << " stddev( " << sqrt(var) << ")"; + << " stddev( " << sqrt(variance) << ")"; } if (stat[DISCARDED].samples > 0) { std::cout << " min_threshold( " << min_threshold << ")"

1 0

[GIT] ppl/ppl(master): Clarified reason of assertion failing by adding a message.
by Enea Zaffanella 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: 0e40494f8f379687c9b7d44fbbfb60493e23da1d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0e40494f8f37… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Apr 6 10:41:12 2012 +0200 Clarified reason of assertion failing by adding a message. --- src/Linear_Row.inlines.hh | 12 ++++++++---- 1 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/Linear_Row.inlines.hh b/src/Linear_Row.inlines.hh index 9b24a0b..f8d3439 100644 --- a/src/Linear_Row.inlines.hh +++ b/src/Linear_Row.inlines.hh @@ -60,7 +60,8 @@ Linear_Row::Flags::Flags(const Topology t, const Kind k) inline bool Linear_Row::Flags::is_ray_or_point_or_inequality() const { - PPL_ASSERT(test_bits(1U << rpi_validity_bit)); + PPL_ASSERT(test_bits(1U << rpi_validity_bit) + && ("rpi bit tested before being initialized" != 0)); return test_bits(static_cast<unsigned>(RAY_OR_POINT_OR_INEQUALITY) << rpi_bit); } @@ -75,7 +76,8 @@ Linear_Row::Flags::set_is_ray_or_point_or_inequality() { inline bool Linear_Row::Flags::is_line_or_equality() const { - PPL_ASSERT(test_bits(1U << rpi_validity_bit)); + PPL_ASSERT(test_bits(1U << rpi_validity_bit) + && ("rpi bit tested before being initialized" != 0)); return !is_ray_or_point_or_inequality(); } @@ -89,13 +91,15 @@ Linear_Row::Flags::set_is_line_or_equality() { inline bool Linear_Row::Flags::is_not_necessarily_closed() const { - PPL_ASSERT(test_bits(1U << nnc_validity_bit)); + PPL_ASSERT(test_bits(1U << nnc_validity_bit) + && ("nnc bit tested before being initialized" != 0)); return test_bits(static_cast<unsigned>(NOT_NECESSARILY_CLOSED) << nnc_bit); } inline bool Linear_Row::Flags::is_necessarily_closed() const { - PPL_ASSERT(test_bits(1U << nnc_validity_bit)); + PPL_ASSERT(test_bits(1U << nnc_validity_bit) + && ("nnc bit tested before being initialized" != 0)); return !is_not_necessarily_closed(); }

1 0

[GIT] ppl/ppl(master): When dumping Linear_Row:: Flags with assertions turned off,
by Enea Zaffanella 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: b406ba2b5a15f5b1b8fa011034d9de64af012536 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=b406ba2b5a15… Author: Enea Zaffanella <zaffanella(a)cs.unipr.it> Date: Fri Apr 6 10:19:18 2012 +0200 When dumping Linear_Row::Flags with assertions turned off, force the (unavailable) rpi/nnc validity bits as "set". --- src/Linear_Row.cc | 24 ++++++++++++++++++------ 1 files changed, 18 insertions(+), 6 deletions(-) diff --git a/src/Linear_Row.cc b/src/Linear_Row.cc index 5a5de51..a3646c4 100644 --- a/src/Linear_Row.cc +++ b/src/Linear_Row.cc @@ -152,14 +152,26 @@ const char* bit_names[] = {rpi_valid, is_rpi, nnc_valid, is_nnc}; void PPL::Linear_Row::Flags::ascii_dump(std::ostream& s) const { +#ifndef NDEBUG s << (test_bits(1U << Flags::rpi_validity_bit) ? '+' : '-') - << rpi_valid << ' ' - << (test_bits(1U << Flags::rpi_bit) ? '+' : '-') + << rpi_valid << ' '; +#else + // NOTE: dump the (unavailable) validity bit as set to avoid + // crashes when ascii_loading with assertions turned on. + s << '+' << rpi_valid << ' '; +#endif + s << (test_bits(1U << Flags::rpi_bit) ? '+' : '-') << is_rpi << ' ' - << ' ' - << (test_bits(1U << Flags::nnc_validity_bit) ? '+' : '-') - << nnc_valid << ' ' - << (test_bits(1U << Flags::nnc_bit) ? '+' : '-') + << ' '; +#ifndef NDEBUG + s << (test_bits(1U << Flags::nnc_validity_bit) ? '+' : '-') + << nnc_valid << ' '; +#else + // NOTE: dump the (unavailable) validity bit as set to avoid + // crashes when ascii_loading with assertions turned on. + s << '+' << nnc_valid << ' '; +#endif + s << (test_bits(1U << Flags::nnc_bit) ? '+' : '-') << is_nnc; }

1 0

[GIT] ppl/ppl(master): Do not use #define without a value.
by Roberto Bagnara 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: 946038b56de1a069614eebe80f1a308b74b8a93e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=946038b56de1… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Apr 6 09:03:47 2012 +0200 Do not use #define without a value. --- src/PIP_Tree.cc | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 8e4f09b..6c5a22c 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -28,9 +28,9 @@ site: http://bugseng.com/products/ppl/ . */ #include <memory> #include <map> -// #define NOISY_PIP_TREE_STRUCTURE -// #define NOISY_PIP -// #define VERY_NOISY_PIP +// #define NOISY_PIP_TREE_STRUCTURE 1 +// #define NOISY_PIP 1 +// #define VERY_NOISY_PIP 1 namespace Parma_Polyhedra_Library {

1 0

[GIT] ppl/ppl(master): The given problem is not satisfiable ( independently verified with other solvers).
by Roberto Bagnara 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: 3415eb20ae3bd9e1fb42c9208865211575dfe6ca URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3415eb20ae3b… Author: Roberto Bagnara <bagnara(a)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

1 0

[GIT] ppl/ppl(master): Make it easier to reproduce issue [PPL 0000353].
by Roberto Bagnara 06 Apr '12

06 Apr '12

Module: ppl/ppl Branch: master Commit: 36136d48b149f536afc224a99ce4965513f8fc18 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=36136d48b149… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Fri Apr 6 07:51:20 2012 +0200 Make it easier to reproduce issue [PPL 0000353]. --- tests/PIP_Problem/Makefile.am | 4 +- tests/PIP_Problem/bug1.cc | 93 +++++++++++++++++++++++++++++++++++--- tests/PIP_Problem/bug1.dat | 99 ----------------------------------------- 3 files changed, 88 insertions(+), 108 deletions(-) diff --git a/tests/PIP_Problem/Makefile.am b/tests/PIP_Problem/Makefile.am index 1d7bc47..0a5041c 100644 --- a/tests/PIP_Problem/Makefile.am +++ b/tests/PIP_Problem/Makefile.am @@ -58,7 +58,7 @@ pipproblem1 pipproblem2 pipproblem3 XFAIL_TESTS = -BUGS = +BUGS = bug1 bug2 # # Sources for the tests @@ -72,6 +72,8 @@ pipproblem1_SOURCES = pipproblem1.cc pipproblem2_SOURCES = pipproblem2.cc pipproblem3_SOURCES = pipproblem3.cc +bug1_SOURCES = bug1.cc + check_PROGRAMS = \ $(TESTS) \ $(BUGS) diff --git a/tests/PIP_Problem/bug1.cc b/tests/PIP_Problem/bug1.cc index fa99cb2..cc79299 100644 --- a/tests/PIP_Problem/bug1.cc +++ b/tests/PIP_Problem/bug1.cc @@ -24,10 +24,11 @@ site: http://bugseng.com/products/ppl/ . */ #include "ppl_test.hh" #include "files.hh" -#include <string> #include <fstream> +#include <iostream> + +using namespace IO_Operators; -using std::string; using std::fstream; using std::ios_base; @@ -35,13 +36,89 @@ namespace { bool test01() { - const char* my_file = "bug1.dat"; + 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); + Variable S(18); + Variable T(19); + Variable U(20); + Variable V(21); + Variable W(22); + Variable X(23); + Variable Y(24); + Variable Z(25); + Variable A1(26); + Variable B1(27); + Variable C1(28); + Variable D1(29); + Variable E1(30); + Variable F1(31); + Variables_Set params; + + Constraint_System cs; + cs.insert(162*B + D + 9*F + 1620*H - F1 == 0); + cs.insert(E1 == 0); + cs.insert(D1 == 1); + cs.insert(162*B + D + 9*F + 1620*H - C1 == 0); + cs.insert(B1 == 0); + cs.insert(A1 == 1); + cs.insert(162*B + D + 9*F + 1620*H - 162*O - Q - 9*S - 1620*Z == 0); + cs.insert(O - Y == 0); + cs.insert(S - X == 0); + cs.insert(Q - W == 0); + cs.insert(V == 0); + cs.insert(162*B + D + 9*F + 1620*H - 162*O - Q - 9*S - 1620*U == 0); + cs.insert(T == 0); + cs.insert(R == 0); + cs.insert(P == 0); + cs.insert(N == 0); + cs.insert(H - M == 0); + cs.insert(B - L == 0); + cs.insert(F - K == 0); + cs.insert(D - J == 0); + cs.insert(I == 0); + cs.insert(G == 0); + cs.insert(E == 0); + cs.insert(C == 0); + cs.insert(A == 0); + cs.insert(B - O >= 1); + cs.insert(D >= 0); + cs.insert(-162*B - D - 9*F - 1620*H + 162*O + Q + 9*S >= -6480); + cs.insert(-B >= -9); + cs.insert(-D >= -8); + cs.insert(-F >= -17); + cs.insert(F >= 0); + cs.insert(-Q >= -8); + cs.insert(-S >= -17); + cs.insert(S >= 0); + cs.insert(Q >= 0); + 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 - fstream f; - open(f, my_file, ios_base::in); - PIP_Problem pip; - pip.ascii_load(f); - close(f); + PIP_Problem pip(cs.space_dimension(), cs.begin(), cs.end(), params); bool ok = pip.is_satisfiable(); diff --git a/tests/PIP_Problem/bug1.dat b/tests/PIP_Problem/bug1.dat deleted file mode 100644 index 4bcd823..0000000 --- a/tests/PIP_Problem/bug1.dat +++ /dev/null @@ -1,99 +0,0 @@ -external_space_dim: 32 - -internal_space_dim: 0 - -input_cs( 38 ) -size 33 0 0 162 0 1 0 9 0 1620 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 -f +RPI_V -RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 0 162 0 1 0 9 0 1620 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 -f +RPI_V -RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 0 162 0 1 0 9 0 1620 0 0 0 0 0 0 -162 0 -1 0 -9 0 0 0 0 0 0 -1620 0 0 -0 0 0 0 f +RPI_V -RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 -1 0 0 0 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 0 162 0 1 0 9 0 1620 0 0 0 0 0 0 -162 0 -1 0 -9 0 -1620 0 0 0 0 0 0 0 -0 0 0 0 f +RPI_V -RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 0 0 1 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 0 1 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 1 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 0 0 0 1 0 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V -RPI +NNC_V -NNC -size 33 -1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V +RPI +NNC_V -NNC -size 33 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V +RPI +NNC_V -NNC -size 33 6480 0 -162 0 -1 0 -9 0 -1620 0 0 0 0 0 0 162 0 1 0 9 0 0 0 0 0 0 0 0 0 -0 0 0 0 f +RPI_V +RPI +NNC_V -NNC -size 33 9 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V +RPI +NNC_V -NNC -size 33 8 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V +RPI +NNC_V -NNC -size 33 17 0 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V +RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V +RPI +NNC_V -NNC -size 33 8 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V +RPI +NNC_V -NNC -size 33 17 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V +RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V +RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V +RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V +RPI +NNC_V -NNC -size 33 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 f -+RPI_V +RPI +NNC_V -NNC - -first_pending_constraint: 0 - -status: PARTIALLY_SATISFIABLE - -parameters -variables( 0 ) - -initial_context -0 x 0 - -control_parameters -CUTTING_STRATEGY_FIRST -PIVOT_ROW_STRATEGY_FIRST - -big_parameter_dimension: 18446744073709551615 - -current_solution: BOTTOM

1 0