September 2009 - PPL-devel - BUGSENG Mailman

Problems with test suite on alpha
by Michael Tautschnig 09 Sep '10

09 Sep '10

Hi PPL developers, I've reported problems with some test cases because of suspected gcc bugs on alpha earlier already. Now it seems that even more test cases are broken, most probably because of the very same bug (I suspect it to be http://gcc.gnu.org/bugzilla/show_bug.cgi?id=8966). My question now is: How to proceed? Shall I specifically disable the failing test cases by surrounding them with an #ifndef __alpha__ or disable the entire test suite on alpha? Thanks, Michael

2 6

Parametric integer linear programming solver
by Sebastian Pop 22 Nov '09

22 Nov '09

Hello, I would like to know whether there exists a parametric integer linear programming solver that can be called from the PPL interface, or how we could use from PPL an existing solver, like http://piplib.org We would need such a tool to improve the precision of the data dependence analysis of Graphite by computing the reaching definitions of array accesses. Thank you, Sebastian Pop -- AMD - GNU Tools

4 10

[GIT] ppl/ppl(pip): Implemented handling of artificial parameters, preparing cut generation.
by François Galea 30 Sep '09

30 Sep '09

Module: ppl/ppl Branch: pip Commit: 4cd20a07c080b717e54ea5dd371bcbc144cdf5af URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4cd20a07c080… Author: François Galea <francois.galea(a)uvsq.fr> Date: Wed Sep 30 18:28:04 2009 +0200 Implemented handling of artificial parameters, preparing cut generation. --- src/PIP_Problem.cc | 3 +- src/PIP_Tree.cc | 119 +++++++++++++++++++++++++++++++++++++++++++++----- src/PIP_Tree.defs.hh | 70 +++++++++++++++++++++++++++-- 3 files changed, 175 insertions(+), 17 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=4cd20a07…

1 0

[GIT] ppl/ppl(floating_point): Removed ad useless parameter in linear_form_upperbound();
by Fabio Biselli 30 Sep '09

30 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 86c9d02d4adb6416d4ab77c3d3461fc1df739a14 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=86c9d02d4adb… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Wed Sep 30 17:02:15 2009 +0200 Removed ad useless parameter in linear_form_upperbound(); --- src/BD_Shape.defs.hh | 3 +-- src/BD_Shape.templates.hh | 28 +++++++++++++--------------- 2 files changed, 14 insertions(+), 17 deletions(-) diff --git a/src/BD_Shape.defs.hh b/src/BD_Shape.defs.hh index e474a00..631bec8 100644 --- a/src/BD_Shape.defs.hh +++ b/src/BD_Shape.defs.hh @@ -2168,8 +2168,7 @@ private: template <typename Interval_Info> void linear_form_upper_bound( const Linear_Form< Interval<T, Interval_Info> >& lf, - N& result, - const dimension_type& space_dim) const; + N& result) const; //! An helper function for the computation of affine relations. /*! diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index aa6a981..a1f5694 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4251,24 +4251,24 @@ void BD_Shape<T> // Update binary constraints on var FIRST. for (dimension_type curr_var = 1; curr_var < var_id; ++curr_var) { Variable current(curr_var - 1); - linear_form_upper_bound(lf - current, upper_bound, space_dim); + linear_form_upper_bound(lf - current, upper_bound); assign_r(dbm[curr_var][var_id], upper_bound, ROUND_NOT_NEEDED); - linear_form_upper_bound(minus_lf + current, upper_bound, space_dim); + linear_form_upper_bound(minus_lf + current, upper_bound); assign_r(dbm[var_id][curr_var], upper_bound, ROUND_NOT_NEEDED); } for (dimension_type curr_var = var_id + 1; curr_var <= space_dim; ++curr_var) { Variable current(curr_var - 1); - linear_form_upper_bound(lf - current, upper_bound, space_dim); + linear_form_upper_bound(lf - current, upper_bound); assign_r(dbm[curr_var][var_id], upper_bound, ROUND_NOT_NEEDED); - linear_form_upper_bound(minus_lf + current, upper_bound, space_dim); + linear_form_upper_bound(minus_lf + current, upper_bound); assign_r(dbm[var_id][curr_var], upper_bound, ROUND_NOT_NEEDED); } // Finally, update unary constraints on var. PPL_DIRTY_TEMP(N, lf_ub); - linear_form_upper_bound(lf, lf_ub, space_dim); + linear_form_upper_bound(lf, lf_ub); PPL_DIRTY_TEMP(N, minus_lf_ub); - linear_form_upper_bound(minus_lf, minus_lf_ub, space_dim); + linear_form_upper_bound(minus_lf, minus_lf_ub); assign_r(dbm[0][var_id], lf_ub, ROUND_NOT_NEEDED); assign_r(dbm[var_id][0], minus_lf_ub, ROUND_NOT_NEEDED); } @@ -4552,8 +4552,7 @@ BD_Shape<T> PPL_DIRTY_TEMP(N, upper_bound); dimension_type max_w_id = std::max(left_w_id, right_w_id); - const dimension_type space_dim = space_dimension(); - + for (dimension_type first_v = 0; first_v < max_w_id; ++first_v) { for (dimension_type second_v = first_v+1; second_v <= max_w_id; ++second_v) { @@ -4605,10 +4604,10 @@ BD_Shape<T> dimension_type n_first_var = first_v +1 ; dimension_type n_second_var = second_v + 1; linear_form_upper_bound(right_minus_left - first + second, - upper_bound, space_dim); + upper_bound); add_dbm_constraint(n_first_var, n_second_var, upper_bound); linear_form_upper_bound(right_minus_left + first - second, - upper_bound, space_dim); + upper_bound); add_dbm_constraint(n_second_var, n_first_var, upper_bound); } } @@ -4637,9 +4636,9 @@ BD_Shape<T> if (do_update) { Variable var(v); dimension_type n_var = v + 1; - linear_form_upper_bound(right_minus_left + var, upper_bound, space_dim); + linear_form_upper_bound(right_minus_left + var, upper_bound); add_dbm_constraint(0, n_var, upper_bound); - linear_form_upper_bound(right_minus_left - var, upper_bound, space_dim); + linear_form_upper_bound(right_minus_left - var, upper_bound); add_dbm_constraint(n_var, 0, upper_bound); } } @@ -4651,8 +4650,7 @@ template <typename Interval_Info> void BD_Shape<T>:: linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, - N& result, - const dimension_type& space_dim) const { + N& result) const { // Check that T is a floating point type. PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact, @@ -4660,7 +4658,7 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, " T not a floating point type."); const dimension_type lf_space_dimension = lf.space_dimension(); - PPL_ASSERT(lf_space_dimension <= space_dim); + PPL_ASSERT(lf_space_dimension <= space_dimension()); typedef Interval<T, Interval_Info> FP_Interval_Type;

1 0

[GIT] ppl/ppl(floating_point): Few tests added;
by Fabio Biselli 30 Sep '09

30 Sep '09

Module: ppl/ppl Branch: floating_point Commit: f3324f27c92998f4d79e61f7daa6f9f3b5ce0ab2 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f3324f27c929… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Wed Sep 30 16:49:14 2009 +0200 Few tests added; Fixed refine_with_linear_form_inequality(); --- src/BD_Shape.templates.hh | 10 --- tests/Floating_Point_Expression/Makefile.am | 14 ++-- tests/Floating_Point_Expression/bdshape2.cc | 107 +++++++++++++++++++++++++++ 3 files changed, 114 insertions(+), 17 deletions(-) diff --git a/src/BD_Shape.templates.hh b/src/BD_Shape.templates.hh index a4c1726..aa6a981 100644 --- a/src/BD_Shape.templates.hh +++ b/src/BD_Shape.templates.hh @@ -4404,7 +4404,6 @@ BD_Shape<T>::left_inhomogeneous_refine(const dimension_type& right_t, return; } } - return; } // end of left_inhomogeneous_refine @@ -4521,14 +4520,6 @@ BD_Shape<T> add_dbm_constraint(right_w_id+1, left_w_id+1, c_plus_minus_a_minus); return; } - if (is_left_coeff_one && is_right_coeff_minus_one) { - // if right coefficent is negative the constraint x + y <= b - // is ignored; - - // FIXME: manage this case adding a costraint x <= k - // where k is an overaproximation of b - y - return; - } if (is_left_coeff_minus_one && is_right_coeff_minus_one) { PPL_DIRTY_TEMP(N, c_plus_minus_a_minus); const FP_Interval_Type& left_a = left.inhomogeneous_term(); @@ -4539,7 +4530,6 @@ BD_Shape<T> return; } } - return; } template <typename T> diff --git a/tests/Floating_Point_Expression/Makefile.am b/tests/Floating_Point_Expression/Makefile.am index 941c905..f91ef32 100644 --- a/tests/Floating_Point_Expression/Makefile.am +++ b/tests/Floating_Point_Expression/Makefile.am @@ -137,19 +137,19 @@ digitalfilters1_SOURCES = digitalfilters1.cc bdshape2_SOURCE = bdshape2.cc -#polyhedron2_SOURCES = polyhedron2.cc +polyhedron2_SOURCES = polyhedron2.cc -#polyhedron1_SOURCES = polyhedron1.cc +polyhedron1_SOURCES = polyhedron1.cc -#bdshape1_SOURCES = bdshape1.cc +bdshape1_SOURCES = bdshape1.cc -#floatingpointexpr1_SOURCES = floatingpointexpr1.cc +floatingpointexpr1_SOURCES = floatingpointexpr1.cc -#linearform1_SOURCES = linearform1.cc +linearform1_SOURCES = linearform1.cc -#octagonalshape1_SOURCES = octagonalshape1.cc +octagonalshape1_SOURCES = octagonalshape1.cc -#octagonalshape2_SOURCES = octagonalshape2.cc +octagonalshape2_SOURCES = octagonalshape2.cc # diff --git a/tests/Floating_Point_Expression/bdshape2.cc b/tests/Floating_Point_Expression/bdshape2.cc index 4b5277d..5a70ad3 100644 --- a/tests/Floating_Point_Expression/bdshape2.cc +++ b/tests/Floating_Point_Expression/bdshape2.cc @@ -442,6 +442,110 @@ test11() { return ok1 && ok2; } +// tests - A <= [-1, 0] and [0, 1] <= A +bool +test12() { + Variable A(0); + Variable B(1); + + FP_BD_Shape bd1(2); + bd1.add_constraint(A <= 2); + bd1.add_constraint(A - B <= 3); + bd1.add_constraint(B <= 2); + FP_BD_Shape known_result(bd1); + FP_Interval tmp(0); + tmp.join_assign(-1); + FP_Linear_Form l2(tmp); + FP_Linear_Form l1(-A); + + bd1.refine_with_linear_form_inequality(l1, l2); + print_constraints(bd1, "*** - A <= [-1, 0] ***"); + + known_result.add_constraint( - A <= 0); + print_constraints(known_result, "*** known_result ***"); + + bool ok1 = (bd1 == known_result); + + bd1.refine_with_linear_form_inequality(l2, l1); + print_constraints(bd1, "*** [0, 1] <= - A ***"); + known_result.add_constraint( A <= 1); + print_constraints(known_result, "*** known_result ***"); + + bool ok2 = (bd1 == known_result); + + return ok1 && ok2; +} + +// tests A <= - B + [-1, 0] and - B + [0, 1] <= A +bool +test13() { + Variable A(0); + Variable B(1); + + FP_BD_Shape bd1(2); + bd1.add_constraint(A <= 2); + bd1.add_constraint(A - B <= 3); + bd1.add_constraint(B <= 2); + FP_BD_Shape known_result(bd1); + FP_Interval tmp(0); + tmp.join_assign(-1); + FP_Linear_Form l2(-B); + FP_Linear_Form l1(A); + l2 += tmp; + + bd1.refine_with_linear_form_inequality(l1, l2); + print_constraints(bd1, "*** A <= - B + [-1, 0] ***"); + + print_constraints(known_result, "*** known_result ***"); + + bool ok1 = (bd1 == known_result); + + bd1.refine_with_linear_form_inequality(l2, l1); + print_constraints(bd1, "*** - B + [0, 1] <= A ***"); + + print_constraints(known_result, "*** known_result ***"); + + bool ok2 = (bd1 == known_result); + + return ok1 && ok2; +} + +// tests A <= - A + [-1, 0] and - A + [0, 1] <= A +bool +test14() { + Variable A(0); + Variable B(1); + + FP_BD_Shape bd1(2); + bd1.add_constraint(A <= 2); + bd1.add_constraint(A - B <= 3); + bd1.add_constraint(B <= 2); + FP_BD_Shape known_result(bd1); + FP_Interval tmp(0); + tmp.join_assign(-1); + FP_Linear_Form l2(-A); + FP_Linear_Form l1(A); + l2 += tmp; + + bd1.refine_with_linear_form_inequality(l1, l2); + print_constraints(bd1, "*** A <= - A + [-1, 0] ***"); + + known_result.add_constraint(2*A <= 0); + print_constraints(known_result, "*** known_result ***"); + + bool ok1 = (bd1 == known_result); + + bd1.refine_with_linear_form_inequality(l2, l1); + print_constraints(bd1, "*** - A + [0, 1] <= A ***"); + + known_result.add_constraint(2*(-A) <= 1); + print_constraints(known_result, "*** known_result ***"); + + bool ok2 = (bd1 == known_result); + + return ok1 && ok2; +} + } // namespace BEGIN_MAIN @@ -456,4 +560,7 @@ BEGIN_MAIN DO_TEST(test09); DO_TEST(test10); DO_TEST(test11); + DO_TEST(test12); + DO_TEST(test13); + DO_TEST(test14); END_MAIN

1 0

[GIT] ppl/w3ppl(master): Put under Git control.
by Roberto Bagnara 29 Sep '09

29 Sep '09

Module: ppl/w3ppl Branch: master Commit: 7a3f9b7c5a746bb3e53f0da87d9df3fdf6a629e4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=7a3f9b7c5a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Sep 29 20:48:17 2009 +0200 Put under Git control. --- htdocs/Documentation/BagnaraHZ09CGTA.pdf | Bin 0 -> 347557 bytes 1 files changed, 0 insertions(+), 0 deletions(-) diff --git a/htdocs/Documentation/BagnaraHZ09CGTA.pdf b/htdocs/Documentation/BagnaraHZ09CGTA.pdf new file mode 100644 index 0000000..a66d364 Binary files /dev/null and b/htdocs/Documentation/BagnaraHZ09CGTA.pdf differ

1 0

[GIT] ppl/w3ppl(master): Added BagnaraHZ09CGTA.
by Roberto Bagnara 29 Sep '09

29 Sep '09

Module: ppl/w3ppl Branch: master Commit: 2f467f99eb8834996cbe183be0ca3660387b1055 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=2f467f99eb… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Sep 29 20:24:01 2009 +0200 Added BagnaraHZ09CGTA. --- htdocs/Documentation/ppl.bib | 37 +++++++++++++++++++++++++++++++++++++ 1 files changed, 37 insertions(+), 0 deletions(-) diff --git a/htdocs/Documentation/ppl.bib b/htdocs/Documentation/ppl.bib index 2421342..80ff5e3 100644 --- a/htdocs/Documentation/ppl.bib +++ b/htdocs/Documentation/ppl.bib @@ -869,6 +869,43 @@ URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ08SCP.pdf" } +@Article{BagnaraHZ09CGTA, + Author = "R. Bagnara and P. M. Hill and E. Zaffanella", + Title = "Exact Join Detection for Convex Polyhedra + and Other Numerical Abstractions", + Journal = "Computational Geometry: Theory and Applications", + Publisher = "Elsevier", + Year = 2009, + Note = "To appear", + Abstract = "Deciding whether the union of two convex polyhedra is + itself a convex polyhedron is a basic problem in + polyhedral computations; having important applications + in the field of constrained control and in the + synthesis, analysis, verification and optimization of + hardware and software systems. In such application + fields though, general convex polyhedra are just one + among many, so-called, \emph{numerical abstractions}, + which range from restricted families of (not necessarily + closed) convex polyhedra to non-convex geometrical + objects. We thus tackle the problem from an abstract + point of view: for a wide range of numerical + abstractions that can be modeled as bounded + join-semilattices ---that is, partial orders where any + finite set of elements has a least upper bound---, we + show necessary and sufficient conditions for the + equivalence between the lattice-theoretic join and the + set-theoretic union. For the case of closed convex + polyhedra ---which, as far as we know, is the only one + already studied in the literature--- we improve upon the + state-of-the-art by providing a new algorithm with a + better worst-case complexity. The results and + algorithms presented for the other numerical + abstractions are new to this paper. All the algorithms + have been implemented, experimentally validated, and + made available in the Parma Polyhedra Library.", + URL = "http://www.cs.unipr.it/ppl/Documentation/BagnaraHZ09CGTA.pdf" +} + @Article{BagnaraHZ09TCS, Author = "R. Bagnara and P. M. Hill and E. Zaffanella", Title = "Applications of Polyhedral Computations to the Analysis

1 0

[GIT] ppl/w3ppl(master): BagnaraHZ09TCS completed.
by Roberto Bagnara 29 Sep '09

29 Sep '09

Module: ppl/w3ppl Branch: master Commit: 03cf70737a9b7918d93586e3ed2c80c285af2c6c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/w3ppl.git;a=commit;h=03cf70737a… Author: Roberto Bagnara <bagnara(a)cs.unipr.it> Date: Tue Sep 29 18:25:19 2009 +0200 BagnaraHZ09TCS completed. --- htdocs/Documentation/ppl.bib | 4 ++-- 1 files changed, 2 insertions(+), 2 deletions(-) diff --git a/htdocs/Documentation/ppl.bib b/htdocs/Documentation/ppl.bib index 27cec84..2421342 100644 --- a/htdocs/Documentation/ppl.bib +++ b/htdocs/Documentation/ppl.bib @@ -874,10 +874,10 @@ Title = "Applications of Polyhedral Computations to the Analysis and Verification of Hardware and Software Systems", Journal = "Theoretical Computer Science", + Volume = 410, + Number = 46, Publisher = "Elsevier", Year = 2009, - Note = "To appear in print. Available online at - \url{http://dx.doi.org/10.1016/j.tcs.2009.07.033}.", Abstract = "Convex polyhedra are the basis for several abstractions used in static analysis and computer-aided verification of complex and sometimes mission critical systems. For

1 0

[GIT] ppl/ppl(floating_point): Added few tests;
by Fabio Biselli 29 Sep '09

29 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 2134fb6959a58a8c572e1bb1d02033b84c4e5b70 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2134fb6959a5… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Tue Sep 29 20:09:54 2009 +0200 Added few tests; Fixed refine_with_linear_form_inequality() and auxiliary functions; Implemented inline void refine_fp_interval_abstract_store(); --- src/BD_Shape.defs.hh | 12 ++- src/BD_Shape.inlines.hh | 17 ++ src/BD_Shape.templates.hh | 89 +++++++---- tests/Floating_Point_Expression/bdshape2.cc | 242 ++++++++++++++++++++++++++- 4 files changed, 323 insertions(+), 37 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=2134fb69…

1 0

[GIT] ppl/ppl(pip): Added support for adding constraints in initial context .
by François Galea 29 Sep '09

29 Sep '09

Module: ppl/ppl Branch: pip Commit: 233be8bdca82973ae4f3ac475c9f672b861c7540 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=233be8bdca82… Author: François Galea <francois.galea(a)uvsq.fr> Date: Tue Sep 29 16:25:02 2009 +0200 Added support for adding constraints in initial context. --- src/PIP_Problem.cc | 50 +++++++++++++++++++++++++++++++++++-- src/PIP_Problem.defs.hh | 7 +++++ src/PIP_Problem.templates.hh | 3 +- src/PIP_Tree.cc | 11 ++++++-- tests/PIP_Problem/pipproblem1.cc | 2 + 5 files changed, 66 insertions(+), 7 deletions(-) diff --git a/src/PIP_Problem.cc b/src/PIP_Problem.cc index a772079..4186408 100644 --- a/src/PIP_Problem.cc +++ b/src/PIP_Problem.cc @@ -39,7 +39,8 @@ PPL::PIP_Problem::PIP_Problem(dimension_type dim) initialized(false), input_cs(), first_pending_constraint(0), - parameters() { + parameters(), + initial_context() { // Check for space dimension overflow. if (dim > max_space_dimension()) throw std::length_error("PPL::PIP_Problem:: PIP_Problem(dim):\n" @@ -56,7 +57,8 @@ PPL::PIP_Problem::PIP_Problem(const PIP_Problem &y) initialized(y.initialized), input_cs(y.input_cs), first_pending_constraint(y.first_pending_constraint), - parameters(y.parameters) { + parameters(y.parameters), + initial_context(y.initial_context) { PPL_ASSERT(OK()); } @@ -83,6 +85,40 @@ PPL::PIP_Problem::solve() const { return OPTIMIZED_PIP_PROBLEM; } + //look for constraints with only parameter coefficients + Constraint_Sequence::const_iterator c; + Constraint_Sequence::const_iterator c_end = input_cs.end(); + Variables_Set::iterator param_begin = parameters.begin(); + Variables_Set::iterator param_end = parameters.end(); + Variables_Set::iterator pi; + dimension_type i; + + // resize context matrix properly + dimension_type num_params = parameters.size()+1; + dimension_type num_cols = initial_context.num_columns(); + if (num_cols < num_params) + x.initial_context.add_zero_columns(num_params-num_cols); + + for (c = input_cs.begin()+first_pending_constraint; c != c_end; ++c) { + dimension_type width = c->space_dimension(); + if (external_space_dim < width) + x.external_space_dim = width; + for (i = 0; i < width; ++i) { + if (c->coefficient(Variable(i)) != 0 && parameters.count(i) == 0) + /* nonzero variable coefficient, constraint not to be inserted + in context */ + break; + } + if (i == width) { + // At this point, the constraint must be translated into context row + Row row(num_params, Row::Flags()); + for (pi = param_begin, i = 1; pi != param_end; ++pi, ++i) + row[i] = c->coefficient(Variable(*pi)); + row[0] = c->inhomogeneous_term(); + x.initial_context.add_row(row); + } + } + x.current_solution->update_tableau(external_space_dim, first_pending_constraint, input_cs, @@ -90,7 +126,6 @@ PPL::PIP_Problem::solve() const { x.internal_space_dim = external_space_dim; x.first_pending_constraint = input_cs.size(); - Matrix initial_context(0, parameters.size()+1); return_value = x.current_solution->solve(x.current_solution, initial_context); @@ -162,6 +197,9 @@ PPL::PIP_Problem::ascii_dump(std::ostream& s) const { s << "\nparameters"; parameters.ascii_dump(s); + + s << "\ninitial_context"; + initial_context.ascii_dump(s); } PPL_OUTPUT_DEFINITIONS(PIP_Problem) @@ -239,6 +277,12 @@ PPL::PIP_Problem::ascii_load(std::istream& s) { if (!parameters.ascii_load(s)) return false; + if (!(s >> str) || str != "initial_context") + return false; + + if (!initial_context.ascii_load(s)) + return false; + PPL_ASSERT(OK()); return true; } diff --git a/src/PIP_Problem.defs.hh b/src/PIP_Problem.defs.hh index 3accf0e..a8317bc 100644 --- a/src/PIP_Problem.defs.hh +++ b/src/PIP_Problem.defs.hh @@ -327,6 +327,13 @@ private: interpreted as problem parameters. */ Variables_Set parameters; + + /*! \brief + The initial context + + Contains problem constraints on parameters only + */ + Matrix initial_context; }; namespace std { diff --git a/src/PIP_Problem.templates.hh b/src/PIP_Problem.templates.hh index 8e8c22f..6594990 100644 --- a/src/PIP_Problem.templates.hh +++ b/src/PIP_Problem.templates.hh @@ -39,7 +39,8 @@ PIP_Problem::PIP_Problem(dimension_type dim, initialized(false), input_cs(), first_pending_constraint(0), - parameters(p_vars) { + parameters(p_vars), + initial_context() { // Check that integer Variables_Set does not exceed the space dimension // of the problem. if (p_vars.space_dimension() > external_space_dim) { diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index b16c902..66d05be 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -615,9 +615,14 @@ PIP_Solution_Node::update_tableau(dimension_type external_space_dim, } } // FIXME: must handle equality constraints - tableau.s.add_row(var); - tableau.t.add_row(param); - sign.push_back(row_sign(param)); + if (row_sign(var) != ZERO) { + /* parametric-only constraints have already been inserted in initial + context, so no need to insert them in the tableau + */ + tableau.s.add_row(var); + tableau.t.add_row(param); + sign.push_back(row_sign(param)); + } } } diff --git a/tests/PIP_Problem/pipproblem1.cc b/tests/PIP_Problem/pipproblem1.cc index 5d0f563..4895eb8 100644 --- a/tests/PIP_Problem/pipproblem1.cc +++ b/tests/PIP_Problem/pipproblem1.cc @@ -79,6 +79,8 @@ test01() { cs.insert(X1 + I0 - N >= 0); cs.insert(-X1 - I0 + N >= 0); cs.insert(X2 + J0 - N - 1 >= 0); + cs.insert(I0 >= 1); + cs.insert(N >= 1); PIP_Problem pip(cs.space_dimension(), cs.begin(), cs.end(), params);

1 0