September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Implemented tests (from test04 to test08).
by Roberto Amadini 16 Sep '09

16 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 3bdc87446af3286556472b791dea891c02cbc124 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=3bdc87446af3… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Wed Sep 16 17:09:43 2009 +0200 Implemented tests (from test04 to test08). --- tests/Floating_Point_Expression/affineimage3.cc | 71 +++++++++++------------ 1 files changed, 35 insertions(+), 36 deletions(-) diff --git a/tests/Floating_Point_Expression/affineimage3.cc b/tests/Floating_Point_Expression/affineimage3.cc index 8be7386..8438ea3 100644 --- a/tests/Floating_Point_Expression/affineimage3.cc +++ b/tests/Floating_Point_Expression/affineimage3.cc @@ -115,7 +115,7 @@ bool test03() { } -// tests affine_image(B, [1, 1]*B + [-1, 3]) +// tests affine_image(B, [1, 1]*B + [-1.5, 3.5]) bool test04() { Variable A(0); Variable B(1); @@ -124,24 +124,23 @@ bool test04() { oc1.add_constraint(A <= 2); oc1.add_constraint(A - B <= 3); oc1.add_constraint(B <= 2); - fl_r_oc free_term(-1); - free_term.join_assign(3); + fl_r_oc free_term(-1.5); + free_term.join_assign(3.5); Linear_Form<fl_r_oc> l(B); l += free_term; oc1.affine_image(B, l); - print_constraints(oc1, "*** oc1.affine_image(B, B + [-1, 3]) ***"); - oc1.ascii_dump(); + print_constraints(oc1, "*** oc1.affine_image(B, B + [-1.5, 3.5]) ***"); + Octagonal_Shape<float> known_result(3); - /* known_result.add_constraint(A >= -2); - known_result.add_constraint(B <= 2); - known_result.add_constraint(B - A <= 4); + known_result.add_constraint(A <= 2); + known_result.add_constraint(2*B <= 11); + known_result.add_constraint(2*B + 2*A <= 15); + known_result.add_constraint(-2*B + 2*A <= 9); print_constraints(known_result, "*** known_result ***"); bool ok = (oc1 == known_result); return ok; - */ - return true; } // tests affine_image(A, [1, 1]*B + [-2, 0.5]) @@ -159,18 +158,18 @@ bool test05() { l += free_term; oc1.affine_image(A, l); print_constraints(oc1, "*** oc1.affine_image(A, B + [-2, 0.5]) ***"); - oc1.ascii_dump(); + Octagonal_Shape<double> known_result(3); - /* known_result.add_constraint(A >= -2); + known_result.add_constraint(2*A <= 5); known_result.add_constraint(B <= 2); - known_result.add_constraint(B - A <= 4); + known_result.add_constraint(B - A <= 2); + known_result.add_constraint(2*A - 2*B <= 1); + known_result.add_constraint(2*A + 2*B <= 9); print_constraints(known_result, "*** known_result ***"); bool ok = (oc1 == known_result); return ok; - */ - return true; } // tests affine_image(B, [1, 1]*A + [-3, 1]) @@ -188,18 +187,18 @@ bool test06() { l += free_term; oc1.affine_image(B, l); print_constraints(oc1, "*** oc1.affine_image(B, A + [-3, 1]) ***"); - oc1.ascii_dump(); + Octagonal_Shape<double> known_result(3); - /* known_result.add_constraint(A >= -2); - known_result.add_constraint(B <= 2); - known_result.add_constraint(B - A <= 4); + known_result.add_constraint(A <= 2); + known_result.add_constraint(B <= 3); + known_result.add_constraint(B - A <= 1); + known_result.add_constraint(A - B <= 3); + known_result.add_constraint(A + B <= 5); print_constraints(known_result, "*** known_result ***"); bool ok = (oc1 == known_result); return ok; - */ - return true; } // tests affine_image(B, [-1, -1]*A + [0, 4]) @@ -217,18 +216,18 @@ bool test07() { l += free_term; oc1.affine_image(B, l); print_constraints(oc1, "*** oc1.affine_image(B, -A + [0, 4]) ***"); - oc1.ascii_dump(); + Octagonal_Shape<float> known_result(3); - /* known_result.add_constraint(A >= -2); - known_result.add_constraint(B <= 2); - known_result.add_constraint(B - A <= 4); + known_result.add_constraint(A <= 2); + known_result.add_constraint(-B <= 2); + known_result.add_constraint(-B - A <= 0); + known_result.add_constraint(A - B <= 4); + known_result.add_constraint(A + B <= 4); print_constraints(known_result, "*** known_result ***"); bool ok = (oc1 == known_result); return ok; - */ - return true; } // tests affine_image(A, [-1, -1]*B + [0, 2]) @@ -246,23 +245,23 @@ bool test08() { l += free_term; oc1.affine_image(A, l); print_constraints(oc1, "*** oc1.affine_image(A, -B + [0, 2]) ***"); - oc1.ascii_dump(); + Octagonal_Shape<float> known_result(3); - /* known_result.add_constraint(A >= -2); + known_result.add_constraint(-A <= 2); known_result.add_constraint(B <= 2); - known_result.add_constraint(B - A <= 4); + known_result.add_constraint(-B - A <= 0); + known_result.add_constraint(-A + B <= 4); + known_result.add_constraint(A + B <= 2); print_constraints(known_result, "*** known_result ***"); bool ok = (oc1 == known_result); return ok; - */ - return true; } // tests affine_image(A, i1*A + i2*B + i3) bool test09() { - + Variable A(0); Variable B(1); @@ -281,7 +280,7 @@ bool test09() { i2.join_assign(2); db_r_oc i1(1); i1.join_assign(1); - + Linear_Form<db_r_oc> l(i3); l += i1*Linear_Form<db_r_oc>(A); @@ -309,11 +308,11 @@ bool test09() { BEGIN_MAIN DO_TEST(test01); DO_TEST(test02); - DO_TEST(test03); /* FIXME: Not yet tested + DO_TEST(test03); DO_TEST(test04); DO_TEST(test05); DO_TEST(test06); DO_TEST(test07); - DO_TEST(test08); */ + DO_TEST(test08); DO_TEST(test09); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Fixed a couple of syntax errors.
by Fabio Bossi 16 Sep '09

16 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 47985bffa0b586928ab59cc6bf3aa789e44822c1 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=47985bffa0b5… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 16 16:21:33 2009 +0200 Fixed a couple of syntax errors. --- src/Octagonal_Shape.templates.hh | 6 +++--- 1 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 011754c..da27f9d 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -5453,7 +5453,7 @@ refine_fp_interval_abstract_store( dimension_type curr_var = ite->first; PPL_ASSERT(curr_var < space_dim); dimension_type n_curr_var = curr_var * 2; - FP_Interval_Type& curr_int = &(ite->second); + FP_Interval_Type& curr_int = ite->second; T& lb = curr_int.lower(); T& ub = curr_int.upper(); // FIXME: are we sure that ROUND_IGNORE is good? @@ -5462,7 +5462,7 @@ refine_fp_interval_abstract_store( div_2exp_assign_r(upper_bound, upper_bound, 1, ROUND_IGNORE); if (upper_bound < ub) - ub = upper_bound; + ub = upper_bound.raw_value(); // Now get the lower bound for curr_var in the octagon. neg_assign_r(upper_bound, matrix[n_curr_var][n_curr_var+1], @@ -5470,7 +5470,7 @@ refine_fp_interval_abstract_store( div_2exp_assign_r(upper_bound, upper_bound, 1, ROUND_IGNORE); if (upper_bound > lb) - lb = upper_bound; + lb = upper_bound.raw_value(); } }

1 0

[GIT] ppl/ppl(floating_point): Many corrections.
by Fabio Bossi 16 Sep '09

16 Sep '09

Module: ppl/ppl Branch: floating_point Commit: c6036d8d0b690c9c3151c6e2beded820db397ccf URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c6036d8d0b69… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 16 15:48:13 2009 +0200 Many corrections. --- src/Octagonal_Shape.templates.hh | 83 ++++++++++++++++++++++++-------------- 1 files changed, 53 insertions(+), 30 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index fc3700e..011754c 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -485,7 +485,9 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( const Linear_Form< Interval<T, Interval_Info> >& right) { // Check that T is a floating point type. - PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact); + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact, + "Octagonal_Shape<T>::refine_with_linear_form_inequality:" + " T not a floating point type."); // FIXME: what to do when empty? @@ -560,8 +562,8 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( const FP_Interval_Type& right_b = right.inhomogeneous_term(); sub_assign_r(b_plus_minus_a_minus, right_b.upper(), left_a.lower(), ROUND_UP); - mul_2exp_assign(b_plus_minus_a_minus, b_plus_minus_a_minus, 1, - ROUND_IGNORE); + mul_2exp_assign_r(b_plus_minus_a_minus, b_plus_minus_a_minus, 1, + ROUND_IGNORE); add_octagonal_constraint(n_right, n_right+1, b_plus_minus_a_minus); return; } @@ -573,8 +575,8 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( const FP_Interval_Type& right_b = right.inhomogeneous_term(); sub_assign_r(b_plus_minus_a_minus, right_b.upper(), left_a.lower(), ROUND_UP); - mul_2exp_assign(b_plus_minus_a_minus, b_plus_minus_a_minus, 1, - ROUND_IGNORE); + mul_2exp_assign_r(b_plus_minus_a_minus, b_plus_minus_a_minus, 1, + ROUND_IGNORE); add_octagonal_constraint(n_right+1, n_right, b_plus_minus_a_minus); return; } @@ -593,8 +595,8 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( const FP_Interval_Type& right_a = right.inhomogeneous_term(); sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(), ROUND_UP); - mul_2exp_assign(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, - ROUND_IGNORE); + mul_2exp_assign_r(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, + ROUND_IGNORE); add_octagonal_constraint(n_left+1, n_left, a_plus_minus_b_minus); return; } @@ -606,8 +608,8 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( const FP_Interval_Type& right_a = right.inhomogeneous_term(); sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(), ROUND_UP); - mul_2exp_assign(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, - ROUND_IGNORE); + mul_2exp_assign_r(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, + ROUND_IGNORE); add_octagonal_constraint(n_left, n_left+1, a_plus_minus_b_minus); return; } @@ -665,8 +667,8 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( const FP_Interval_Type& right_c = right.inhomogeneous_term(); sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(), ROUND_UP); - mul_2exp_assign(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, - ROUND_IGNORE); + mul_2exp_assign_r(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, + ROUND_IGNORE); if (left_w_id < right_w_id) add_octagonal_constraint(n_right, n_left, c_plus_minus_a_minus); else @@ -681,8 +683,8 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( const FP_Interval_Type& right_c = right.inhomogeneous_term(); sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(), ROUND_UP); - mul_2exp_assign(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, - ROUND_IGNORE); + mul_2exp_assign_r(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, + ROUND_IGNORE); if (left_w_id < right_w_id) add_octagonal_constraint(n_right+1, n_left, c_plus_minus_a_minus); else @@ -697,8 +699,8 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( const FP_Interval_Type& right_c = right.inhomogeneous_term(); sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(), ROUND_UP); - mul_2exp_assign(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, - ROUND_IGNORE); + mul_2exp_assign_r(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, + ROUND_IGNORE); if (left_w_id < right_w_id) add_octagonal_constraint(n_right, n_left+1, c_plus_minus_a_minus); else @@ -713,8 +715,8 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( const FP_Interval_Type& right_c = right.inhomogeneous_term(); sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(), ROUND_UP); - mul_2exp_assign(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, - ROUND_IGNORE); + mul_2exp_assign_r(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, + ROUND_IGNORE); if (left_w_id < right_w_id) add_octagonal_constraint(n_right+1, n_left+1, c_plus_minus_a_minus); else @@ -722,7 +724,6 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( return; } } - } // General case. @@ -5047,7 +5048,9 @@ Octagonal_Shape<T>::affine_image(Variable var, const Linear_Form< Interval<T, Interval_Info> >& lf) { // Check that T is a floating point type. - PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact); + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact, + "Octagonal_Shape<T>::affine_image(Variable, Linear_Form):" + " T not a floating point type."); // Dimension-compatibility checks. // The dimension of `lf' should not be greater than the dimension @@ -5302,7 +5305,9 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, N& result) const { // Check that T is a floating point type. - PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact); + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact, + "Octagonal_Shape<T>::linear_form_upper_bound:" + " T not a floating point type."); const dimension_type lf_space_dimension = lf.space_dimension(); PPL_ASSERT(lf_space_dimension <= space_dim); @@ -5351,14 +5356,28 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, assign_r(second_comparison_term, 0, ROUND_NOT_NEEDED); assign_r(third_comparison_term, 0, ROUND_NOT_NEEDED); assign_r(fourth_comparison_term, 0, ROUND_NOT_NEEDED); - add_mul_assign_r(first_comparison_term, curr_var_ub, curr_ub, - ROUND_UP); - add_mul_assign_r(second_comparison_term, curr_minus_var_ub, curr_ub, - ROUND_UP); - add_mul_assign_r(third_comparison_term, curr_var_ub, curr_lb, - ROUND_UP); - add_mul_assign_r(fourth_comparison_term, curr_minus_var_ub, curr_lb, - ROUND_UP); + if (is_plus_infinity(curr_var_ub)) { + assign_r(first_comparison_term, PLUS_INFINITY, ROUND_NOT_NEEDED); + assign_r(third_comparison_term, PLUS_INFINITY, ROUND_NOT_NEEDED); + } + else { + add_mul_assign_r(first_comparison_term, curr_var_ub, curr_ub, + ROUND_UP); + add_mul_assign_r(third_comparison_term, curr_var_ub, curr_lb, + ROUND_UP); + } + + if (is_minus_infinity(curr_minus_var_ub)) { + assign_r(second_comparison_term, PLUS_INFINITY, ROUND_NOT_NEEDED); + assign_r(fourth_comparison_term, PLUS_INFINITY, ROUND_NOT_NEEDED); + } + else { + add_mul_assign_r(second_comparison_term, curr_minus_var_ub, curr_ub, + ROUND_UP); + add_mul_assign_r(fourth_comparison_term, curr_minus_var_ub, curr_lb, + ROUND_UP); + } + assign_r(first_comparison_term, std::max(first_comparison_term, second_comparison_term), ROUND_NOT_NEEDED); @@ -5385,7 +5404,9 @@ interval_coefficient_upper_bound(const N& var_ub, const N& minus_var_ub, N& result) { // Check that T is a floating point type. - PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact); + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact, + "Octagonal_Shape<T>::interval_coefficient_upper_bound:" + " T not a floating point type."); // NOTE: we store the first comparison term directly into result. PPL_DIRTY_TEMP(N, second_comparison_term); @@ -5416,7 +5437,9 @@ refine_fp_interval_abstract_store( std::map< dimension_type, Interval<T, Interval_Info> >& store) { // Check that T is a floating point type. - PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact); + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact, + "Octagonal_Shape<T>::refine_fp_interval_abstract_store:" + " T not a floating point type."); strong_closure_assign();

1 0

[GIT] ppl/ppl(pip): Implemented additional steps of the simplex algorithm.
by François Galea 16 Sep '09

16 Sep '09

Module: ppl/ppl Branch: pip Commit: 5927b13d1aae63bca73f31b377ee437b28ce8618 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5927b13d1aae… Author: François Galea <francois.galea(a)uvsq.fr> Date: Wed Sep 16 15:24:24 2009 +0200 Implemented additional steps of the simplex algorithm. - handling of simplex rows with mixed parameter sign; - handling of tautology expressions; - handling of splitting a solution according to a test parametric expression. --- src/PIP_Tree.cc | 112 ++++++++++++++++++++++++++++++++++++++++++++++++- src/PIP_Tree.defs.hh | 3 + 2 files changed, 112 insertions(+), 3 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index edc073f..d528d37 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -74,7 +74,8 @@ PIP_Tree_Node::PIP_Tree_Node(const PIP_Tree_Node &x) PIP_Decision_Node::~PIP_Decision_Node() { delete true_child; - delete false_child; + if (false_child) + delete false_child; } PIP_Solution_Node::~PIP_Solution_Node() { @@ -196,6 +197,14 @@ PIP_Tree_Node::OK() const { return true; } +void +PIP_Tree_Node::add_constraint(const Row &row) { + Linear_Expression e; + for (dimension_type j=row.size(); j-- > 1; ) + e += row[j] * Variable(j-1); + constraints_.insert(e + row[0] >= 0); +} + bool PIP_Solution_Node::OK() const { /* FIXME: finish me! */ @@ -526,7 +535,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, // Main loop of the simplex algorithm for(;;) { - dimension_type i; + dimension_type i, j; dimension_type i_ = n_a_d; dimension_type i__ = n_a_d; dimension_type num_rows = tableau.t.num_rows(); @@ -590,7 +599,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, std::cout << "Found row with negative parameters: " << i_ << std::endl; #endif - dimension_type j, k; + dimension_type k; Coefficient z(0); Coefficient sij, cij, cij_; Coefficient c; @@ -738,6 +747,103 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, c /= sij; } } + + /* Otherwise, we have found a row i__ with mixed parameter sign. */ + else if (i__ != n_a_d) { + dimension_type neg = n_a_d; + Coefficient ns, score; + + /* Look for a constraint with mixed parameter sign with no positive + * variable coefficients */ + for (i=i__; i<num_rows; ++i) { + if (sign[i] != MIXED) + continue; + for (j=0; j<num_vars; ++j) { + if (tableau.s[i][j] > 0) + break; + } + /* Choose row with lowest score, potentially eliminating + * implicated tautologies if some exist */ + if (j == num_vars) { + score = 0; + for (j=0; j<num_params; ++j) + score += tableau.t[i][j]; + if (neg == n_a_d || score < ns) { + neg = i; + ns = score; + } + } + } + if (neg != n_a_d) { + i = neg; +#ifdef NOISY_PIP + std::cout << "Found row with unknown parameter sign and negative " + "variable coefficients: " << i + << std::endl; +#endif + Row &r = tableau.t[i]; + context.add_row(r); + add_constraint(r); +#ifdef NOISY_PIP + Linear_Expression e; + for (j=1; j<num_params; ++j) + e += r[j] * Variable(j-1); + Constraint c(e + r[0] >= 0); + std::cout << "Adding tautology: " << c + << std::endl; +#endif + } else { +#ifdef NOISY_PIP + std::cout << "Found row with mixed parameter sign: " << i__ + << std::endl + << "Solution depends on the sign of parameter" + << std::endl; +#endif + Row test(tableau.t[i__]); + + /* Create a solution Node to become "true" version of current Node */ + PIP_Tree_Node *tru = new PIP_Solution_Node(*this, true); + context.add_row(test); + PIP_Problem_Status status_t = tru->solve(tru, context); + + /* Modify *this to become "false" version */ + Constraint_System cs; + cs.swap(constraints_); + PIP_Tree_Node *fals = this; + Row &testf = context[context.num_rows()-1]; + negate_assign(testf, test); + PIP_Problem_Status status_f = solve(fals, context); + + if (status_t == UNFEASIBLE_PIP_PROBLEM + && status_f == UNFEASIBLE_PIP_PROBLEM) { + parent_ref = 0; + return UNFEASIBLE_PIP_PROBLEM; + } else if (status_t == UNFEASIBLE_PIP_PROBLEM) { + cs.swap(constraints_); + add_constraint(testf); + return OPTIMIZED_PIP_PROBLEM; + } else if (status_f == UNFEASIBLE_PIP_PROBLEM) { + cs.swap(tru->constraints_); + tru->add_constraint(test); + parent_ref = tru; + return OPTIMIZED_PIP_PROBLEM; + } + + /* Create a decision Node to become parent of current Node */ + PIP_Decision_Node *parent = new PIP_Decision_Node(fals, tru); + parent->add_constraint(test); + + if (!cs.empty()) { + /* If node to be solved had tautologies, store them in a new + decision node */ + parent = new PIP_Decision_Node(0, parent); + cs.swap(parent->constraints_); + } + + parent_ref = parent; + return OPTIMIZED_PIP_PROBLEM; + } + } //FIXME: to be finished } // Main loop of the simplex algorithm diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index cb41f49..f23bf31 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -129,6 +129,9 @@ protected: */ virtual PIP_Problem_Status solve(PIP_Tree_Node*& parent_ref, const Matrix& context) = 0; + + //! Inserts a new parametric constraint in internal Row format + void add_constraint(const Row &x); }; //! A tree node representing part of the space of solutions.

1 0

[GIT] ppl/ppl(pip): Modified prototype for solve method in PIP_Tree_Node and derivates.
by François Galea 16 Sep '09

16 Sep '09

Module: ppl/ppl Branch: pip Commit: 64bd2613cda2788010f510107f7ba3fa24ad40ce URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=64bd2613cda2… Author: François Galea <francois.galea(a)uvsq.fr> Date: Wed Sep 16 15:21:06 2009 +0200 Modified prototype for solve method in PIP_Tree_Node and derivates. --- src/PIP_Problem.cc | 2 +- src/PIP_Tree.cc | 12 ++++++------ src/PIP_Tree.defs.hh | 6 +++--- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/PIP_Problem.cc b/src/PIP_Problem.cc index 34affcd..ec42436 100644 --- a/src/PIP_Problem.cc +++ b/src/PIP_Problem.cc @@ -86,7 +86,7 @@ PPL::PIP_Problem::solve() const { parameters); Matrix initial_context(0, parameters.size()+1); - return_value = x.current_solution->solve(&x.current_solution, + return_value = x.current_solution->solve(x.current_solution, initial_context); switch (return_value) { diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 30e4080..edc073f 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -261,13 +261,13 @@ PIP_Decision_Node::update_tableau(PIP_Tree_Node ** /* parent_ref */, } PIP_Problem_Status -PIP_Decision_Node::solve(PIP_Tree_Node **parent_ref, const Matrix& context) { +PIP_Decision_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& context) { PIP_Problem_Status return_status; PIP_Problem_Status stt; PIP_Problem_Status stf = UNFEASIBLE_PIP_PROBLEM; Matrix context_true(context); merge_assign(context_true, constraints_); - stt = true_child->solve(&true_child, context_true); + stt = true_child->solve(true_child, context_true); if (false_child) { // Decision nodes with false child must have exactly one constraint PPL_ASSERT(1 == std::distance(constraints_.begin(), constraints_.end())); @@ -275,12 +275,12 @@ PIP_Decision_Node::solve(PIP_Tree_Node **parent_ref, const Matrix& context) { merge_assign(context_false, constraints_); Row &last = context_false[context_false.num_rows()-1]; negate_assign(last, last); - stf = false_child->solve(&false_child, context_false); + stf = false_child->solve(false_child, context_false); } if (stt == UNFEASIBLE_PIP_PROBLEM && stf == UNFEASIBLE_PIP_PROBLEM) { return_status = UNFEASIBLE_PIP_PROBLEM; - *parent_ref = 0; + parent_ref = 0; delete this; } else return_status = OPTIMIZED_PIP_PROBLEM; @@ -517,7 +517,7 @@ PIP_Solution_Node::update_tableau(PIP_Tree_Node ** /* parent_ref */, } PIP_Problem_Status -PIP_Solution_Node::solve(PIP_Tree_Node** parent_ref, +PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, const Matrix& ctx) { Matrix context(ctx); merge_assign(context, constraints_); @@ -632,7 +632,7 @@ PIP_Solution_Node::solve(PIP_Tree_Node** parent_ref, std::cout << "No positive pivot found: Solution = _|_" << std::endl; #endif - *parent_ref = 0; + parent_ref = 0; delete this; return UNFEASIBLE_PIP_PROBLEM; } diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index 72c6fc6..cb41f49 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -127,7 +127,7 @@ protected: An PIP_Problem_Status flag indicating the outcome of the optimization attempt (unfeasible or optimized problem). */ - virtual PIP_Problem_Status solve(PIP_Tree_Node **parent_ref, + virtual PIP_Problem_Status solve(PIP_Tree_Node*& parent_ref, const Matrix& context) = 0; }; @@ -326,7 +326,7 @@ protected: An PIP_Problem_Status flag indicating the outcome of the optimization attempt (unfeasible or optimized problem). */ - virtual PIP_Problem_Status solve(PIP_Tree_Node **parent_ref, + virtual PIP_Problem_Status solve(PIP_Tree_Node*& parent_ref, const Matrix& context); // FIXME: constructors to be decided. }; @@ -418,7 +418,7 @@ protected: An PIP_Problem_Status flag indicating the outcome of the optimization attempt (unfeasible or optimized problem). */ - virtual PIP_Problem_Status solve(PIP_Tree_Node **parent_ref, + virtual PIP_Problem_Status solve(PIP_Tree_Node*& parent_ref, const Matrix& context); };

1 0

[GIT] ppl/ppl(pip): Redefined and implemented the tree node constructors.
by François Galea 16 Sep '09

16 Sep '09

Module: ppl/ppl Branch: pip Commit: c93acf108e683d72dc4aef9f6e93d7d7b29b206a URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c93acf108e68… Author: François Galea <francois.galea(a)uvsq.fr> Date: Wed Sep 16 15:15:28 2009 +0200 Redefined and implemented the tree node constructors. --- src/PIP_Tree.cc | 40 +++++++++++++++++++++++++++++++++++++ src/PIP_Tree.defs.hh | 53 +++++++++++++++++++++++++------------------------ 2 files changed, 67 insertions(+), 26 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index c9f576a..30e4080 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -64,6 +64,13 @@ negate_assign(Row& x, const Row& y) { } // namespace +PIP_Tree_Node::PIP_Tree_Node() + : constraints_() { +} + +PIP_Tree_Node::PIP_Tree_Node(const PIP_Tree_Node &x) + : constraints_(x.constraints_) { +} PIP_Decision_Node::~PIP_Decision_Node() { delete true_child; @@ -73,6 +80,39 @@ PIP_Decision_Node::~PIP_Decision_Node() { PIP_Solution_Node::~PIP_Solution_Node() { } +PIP_Solution_Node::PIP_Solution_Node() + : PIP_Tree_Node(), + tableau(), + basis(), + mapping(), + sign() { +} + +PIP_Solution_Node::PIP_Solution_Node(const PIP_Solution_Node &x) + : PIP_Tree_Node(x), + tableau(x.tableau), + basis(x.basis), + mapping(x.mapping), + sign(x.sign) { +} + +PIP_Solution_Node::PIP_Solution_Node(const PIP_Solution_Node &x, + bool empty_constraints) + : PIP_Tree_Node(), + tableau(x.tableau), + basis(x.basis), + mapping(x.mapping), + sign(x.sign) { + if (!empty_constraints) + constraints_ = x.constraints_; +} + +PIP_Decision_Node::PIP_Decision_Node(PIP_Tree_Node* fcp, PIP_Tree_Node* tcp) + : PIP_Tree_Node(), + true_child(tcp), + false_child(fcp) { +} + const PIP_Solution_Node* PIP_Tree_Node::as_solution() const { return 0; diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index e88aa0f..72c6fc6 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -71,6 +71,12 @@ public: const Constraint_System& constraints() const; protected: + //! Default constructor. + PIP_Tree_Node(); + + //! Copy constructor. + PIP_Tree_Node(const PIP_Tree_Node &x); + //! A type alias for a sequence of constraints. typedef std::vector<Constraint> Constraint_Sequence; @@ -78,6 +84,7 @@ protected: // constructor and methods. friend class PIP_Problem; friend class PIP_Decision_Node; + friend class PIP_Solution_Node; //! The local system of parameter constraints. Constraint_System constraints_; @@ -127,6 +134,9 @@ protected: //! A tree node representing part of the space of solutions. class PIP_Solution_Node : public PIP_Tree_Node { public: + //! Default constructor. + PIP_Solution_Node(); + //! Destructor. ~PIP_Solution_Node(); @@ -272,6 +282,12 @@ private: static bool compatibility_check(const Matrix &ctx, const Row &cnst); protected: + //! Copy constructor. + PIP_Solution_Node(const PIP_Solution_Node &x); + + //! Copy constructor, allowing not to copy the constraint system. + PIP_Solution_Node(const PIP_Solution_Node &x, bool empty_constraints); + /*! \brief Populates the parametric simplex tableau using external data, if necessary @@ -336,6 +352,9 @@ public: bool OK() const; private: + // only PIP_Solution_Node is allowed to use the constructor and methods. + friend class PIP_Solution_Node; + //! Pointer to the "true" child of \p *this. PIP_Tree_Node* true_child; @@ -343,40 +362,22 @@ private: PIP_Tree_Node* false_child; /*! \brief - Constructs if \p cs then \p tcp \p else \p fcp. - - Constructs a decision node controlled by \p cs (which is copied), - with "true" child \p tcp and "false" child \p fcp. - - \param cs - The system of constraints controlling the node. - - \exception std::invalid_argument - Thrown if \p cs contains strict inequalities. - */ - PIP_Decision_Node(const Constraint_System& cs, - PIP_Tree_Node* fcp, PIP_Tree_Node* tcp); - - /*! \brief - Constructs if \p cs then \p tcp \p else \p fcp. + Constructs "if constraints then \p tcp else \p fcp". Initial constraint + set is empty. - Constructs a decision node controlled by \p cs (which is recycled), + Constructs a decision node, with "true" child \p tcp and "false" child \p fcp. - \param cs - The system of constraints controlling the node. It is not - declared <CODE>const</CODE> because its data-structures may be - recycled to build the polyhedron. + \param fcp + Pointer to "false" child - \param dummy - A dummy tag to syntactically differentiate this one - from the other constructors. + \param tcp + Pointer to "true" child \exception std::invalid_argument Thrown if \p cs contains strict inequalities. */ - PIP_Decision_Node(Constraint_System& cs, Recycle_Input dummy, - PIP_Tree_Node* fcp, PIP_Tree_Node* tcp); + PIP_Decision_Node(PIP_Tree_Node* fcp, PIP_Tree_Node* tcp); protected: /*! \brief

1 0

[GIT] ppl/ppl(floating_point): Use PPL_COMPILE_TIME_CHECK insteas of PPL_ASSERT whenever possible.
by Fabio Bossi 16 Sep '09

16 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 16204cc0b8e28f99b68099f0aa46702f0686a306 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=16204cc0b8e2… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 16 14:08:31 2009 +0200 Use PPL_COMPILE_TIME_CHECK insteas of PPL_ASSERT whenever possible. --- src/Octagonal_Shape.templates.hh | 10 +++++----- 1 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index c0aba85..fc3700e 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -485,7 +485,7 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( const Linear_Form< Interval<T, Interval_Info> >& right) { // Check that T is a floating point type. - PPL_ASSERT(!std::numeric_limits<T>::is_exact); + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact); // FIXME: what to do when empty? @@ -5047,7 +5047,7 @@ Octagonal_Shape<T>::affine_image(Variable var, const Linear_Form< Interval<T, Interval_Info> >& lf) { // Check that T is a floating point type. - PPL_ASSERT(!std::numeric_limits<T>::is_exact); + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact); // Dimension-compatibility checks. // The dimension of `lf' should not be greater than the dimension @@ -5302,7 +5302,7 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, N& result) const { // Check that T is a floating point type. - PPL_ASSERT(!std::numeric_limits<T>::is_exact); + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact); const dimension_type lf_space_dimension = lf.space_dimension(); PPL_ASSERT(lf_space_dimension <= space_dim); @@ -5385,7 +5385,7 @@ interval_coefficient_upper_bound(const N& var_ub, const N& minus_var_ub, N& result) { // Check that T is a floating point type. - PPL_ASSERT(!std::numeric_limits<T>::is_exact); + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact); // NOTE: we store the first comparison term directly into result. PPL_DIRTY_TEMP(N, second_comparison_term); @@ -5416,7 +5416,7 @@ refine_fp_interval_abstract_store( std::map< dimension_type, Interval<T, Interval_Info> >& store) { // Check that T is a floating point type. - PPL_ASSERT(!std::numeric_limits<T>::is_exact); + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<T>::is_exact); strong_closure_assign();

1 0

[GIT] ppl/ppl(floating_point): Fixed one typo.
by Fabio Bossi 16 Sep '09

16 Sep '09

Module: ppl/ppl Branch: floating_point Commit: ed84cf0c1472b75574bf6d1256944f3d48597dad URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ed84cf0c1472… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 16 12:24:01 2009 +0200 Fixed one typo. --- src/Octagonal_Shape.templates.hh | 2 +- 1 files changed, 1 insertions(+), 1 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 08feb94..c0aba85 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -628,7 +628,7 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( bool is_right_coeff_minus_one = (right_w_coeff == -1); if (left_w_id == right_w_id) { if (is_left_coeff_one && is_right_coeff_one || - is_left_coeff_minus_one && is_right_constraint_minus_one) { + is_left_coeff_minus_one && is_right_coeff_minus_one) { // Here we have an identity or a constants-only constraint. return; }

1 0

[GIT] ppl/ppl(floating_point): Added more cases for refine_linear_form_inequality.
by Fabio Bossi 16 Sep '09

16 Sep '09

Module: ppl/ppl Branch: floating_point Commit: e492c9a5c5291b95b3abffee549174744a9c8fe3 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e492c9a5c529… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Wed Sep 16 12:21:30 2009 +0200 Added more cases for refine_linear_form_inequality. --- src/Octagonal_Shape.templates.hh | 188 +++++++++++++++++++++++++++++++++++++- 1 files changed, 183 insertions(+), 5 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 9d4e70c..08feb94 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -506,10 +506,6 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( if (marked_empty()) return; - /* - FIXME: these are not really necessary right now. They will come in - handy when we optimize the most common cases. - */ // Number of non-zero coefficients in `left': will be set to // 0, 1, or 2, the latter value meaning any value greater than 1. dimension_type left_t = 0; @@ -545,7 +541,189 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( typedef typename OR_Matrix<N>::const_row_reference_type Row_reference; typedef Interval<T, Interval_Info> FP_Interval_Type; - // TODO: optimize the most common cases. + if (left_t == 0) { + if (right_t == 0) { + // The constraint involves constants only. Ignore it: it is up to + // the analyzer to handle it. + return; + } + + if (right_t == 1) { + // The constraint has the form [a-;a+] <= [b-;b+] + [c-;c+] * x. + // Reduce it to the constraint +/-x <= b+ - a- if [c-;c+] = +/-[1;1]. + const FP_Interval_Type& right_w_coeff = + right.coefficient(Variable(right_w_id)); + if (right_w_coeff == 1) { + const dimension_type n_right = right_w_id * 2; + PPL_DIRTY_TEMP(N, b_plus_minus_a_minus); + const FP_Interval_Type& left_a = left.inhomogeneous_term(); + const FP_Interval_Type& right_b = right.inhomogeneous_term(); + sub_assign_r(b_plus_minus_a_minus, right_b.upper(), left_a.lower(), + ROUND_UP); + mul_2exp_assign(b_plus_minus_a_minus, b_plus_minus_a_minus, 1, + ROUND_IGNORE); + add_octagonal_constraint(n_right, n_right+1, b_plus_minus_a_minus); + return; + } + + if (right_w_coeff == -1) { + const dimension_type n_right = right_w_id * 2; + PPL_DIRTY_TEMP(N, b_plus_minus_a_minus); + const FP_Interval_Type& left_a = left.inhomogeneous_term(); + const FP_Interval_Type& right_b = right.inhomogeneous_term(); + sub_assign_r(b_plus_minus_a_minus, right_b.upper(), left_a.lower(), + ROUND_UP); + mul_2exp_assign(b_plus_minus_a_minus, b_plus_minus_a_minus, 1, + ROUND_IGNORE); + add_octagonal_constraint(n_right+1, n_right, b_plus_minus_a_minus); + return; + } + } + } + else if (left_t == 1) { + if (right_t == 0) { + // The constraint has the form [b-;b+] + [c-;c+] * x <= [a-;a+] + // Reduce it to the constraint +/-x <= a+ - b- if [c-;c+] = +/-[1;1]. + const FP_Interval_Type& left_w_coeff = + left.coefficient(Variable(left_w_id)); + if (left_w_coeff == 1) { + const dimension_type n_left = left_w_id * 2; + PPL_DIRTY_TEMP(N, a_plus_minus_b_minus); + const FP_Interval_Type& left_b = left.inhomogeneous_term(); + const FP_Interval_Type& right_a = right.inhomogeneous_term(); + sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(), + ROUND_UP); + mul_2exp_assign(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, + ROUND_IGNORE); + add_octagonal_constraint(n_left+1, n_left, a_plus_minus_b_minus); + return; + } + + if (left_w_coeff == -1) { + const dimension_type n_left = left_w_id * 2; + PPL_DIRTY_TEMP(N, a_plus_minus_b_minus); + const FP_Interval_Type& left_b = left.inhomogeneous_term(); + const FP_Interval_Type& right_a = right.inhomogeneous_term(); + sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(), + ROUND_UP); + mul_2exp_assign(a_plus_minus_b_minus, a_plus_minus_b_minus, 1, + ROUND_IGNORE); + add_octagonal_constraint(n_left, n_left+1, a_plus_minus_b_minus); + return; + } + } + + if (right_t == 1) { + // The constraint has the form: + // [a-;a+] + [b-;b+] * x <= [c-;c+] + [d-;d+] * y. + // Reduce it to the constraint +/-x +/-y <= c+ - a- + // if [b-;b+] = +/-[1;1] and [d-;d+] = +/-[1;1]. + const FP_Interval_Type& left_w_coeff = + left.coefficient(Variable(left_w_id)); + const FP_Interval_Type& right_w_coeff = + right.coefficient(Variable(right_w_id)); + bool is_left_coeff_one = (left_w_coeff == 1); + bool is_left_coeff_minus_one = (left_w_coeff == -1); + bool is_right_coeff_one = (right_w_coeff == 1); + bool is_right_coeff_minus_one = (right_w_coeff == -1); + if (left_w_id == right_w_id) { + if (is_left_coeff_one && is_right_coeff_one || + is_left_coeff_minus_one && is_right_constraint_minus_one) { + // Here we have an identity or a constants-only constraint. + return; + } + if (is_left_coeff_one && is_right_coeff_minus_one) { + // We fall back to a previous case + // (but we do not need to multiply the result by two). + const dimension_type n_left = left_w_id * 2; + PPL_DIRTY_TEMP(N, a_plus_minus_b_minus); + const FP_Interval_Type& left_b = left.inhomogeneous_term(); + const FP_Interval_Type& right_a = right.inhomogeneous_term(); + sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(), + ROUND_UP); + add_octagonal_constraint(n_left+1, n_left, a_plus_minus_b_minus); + return; + } + if (is_left_coeff_minus_one && is_right_coeff_one) { + // We fall back to a previous case + // (but we do not need to multiply the result by two). + const dimension_type n_left = left_w_id * 2; + PPL_DIRTY_TEMP(N, a_plus_minus_b_minus); + const FP_Interval_Type& left_b = left.inhomogeneous_term(); + const FP_Interval_Type& right_a = right.inhomogeneous_term(); + sub_assign_r(a_plus_minus_b_minus, right_a.upper(), left_b.lower(), + ROUND_UP); + add_octagonal_constraint(n_left, n_left+1, a_plus_minus_b_minus); + return; + } + } + else if (is_left_coeff_one && is_right_coeff_one) { + const dimension_type n_left = left_w_id * 2; + const dimension_type n_right = right_w_id * 2; + PPL_DIRTY_TEMP(N, c_plus_minus_a_minus); + const FP_Interval_Type& left_a = left.inhomogeneous_term(); + const FP_Interval_Type& right_c = right.inhomogeneous_term(); + sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(), + ROUND_UP); + mul_2exp_assign(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, + ROUND_IGNORE); + if (left_w_id < right_w_id) + add_octagonal_constraint(n_right, n_left, c_plus_minus_a_minus); + else + add_octagonal_constraint(n_left+1, n_right+1, c_plus_minus_a_minus); + return; + } + if (is_left_coeff_one && is_right_coeff_minus_one) { + const dimension_type n_left = left_w_id * 2; + const dimension_type n_right = right_w_id * 2; + PPL_DIRTY_TEMP(N, c_plus_minus_a_minus); + const FP_Interval_Type& left_a = left.inhomogeneous_term(); + const FP_Interval_Type& right_c = right.inhomogeneous_term(); + sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(), + ROUND_UP); + mul_2exp_assign(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, + ROUND_IGNORE); + if (left_w_id < right_w_id) + add_octagonal_constraint(n_right+1, n_left, c_plus_minus_a_minus); + else + add_octagonal_constraint(n_left+1, n_right, c_plus_minus_a_minus); + return; + } + if (is_left_coeff_minus_one && is_right_coeff_one) { + const dimension_type n_left = left_w_id * 2; + const dimension_type n_right = right_w_id * 2; + PPL_DIRTY_TEMP(N, c_plus_minus_a_minus); + const FP_Interval_Type& left_a = left.inhomogeneous_term(); + const FP_Interval_Type& right_c = right.inhomogeneous_term(); + sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(), + ROUND_UP); + mul_2exp_assign(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, + ROUND_IGNORE); + if (left_w_id < right_w_id) + add_octagonal_constraint(n_right, n_left+1, c_plus_minus_a_minus); + else + add_octagonal_constraint(n_left, n_right+1, c_plus_minus_a_minus); + return; + } + if (is_left_coeff_minus_one && is_right_coeff_minus_one) { + const dimension_type n_left = left_w_id * 2; + const dimension_type n_right = right_w_id * 2; + PPL_DIRTY_TEMP(N, c_plus_minus_a_minus); + const FP_Interval_Type& left_a = left.inhomogeneous_term(); + const FP_Interval_Type& right_c = right.inhomogeneous_term(); + sub_assign_r(c_plus_minus_a_minus, right_c.upper(), left_a.lower(), + ROUND_UP); + mul_2exp_assign(c_plus_minus_a_minus, c_plus_minus_a_minus, 1, + ROUND_IGNORE); + if (left_w_id < right_w_id) + add_octagonal_constraint(n_right+1, n_left+1, c_plus_minus_a_minus); + else + add_octagonal_constraint(n_left, n_right, c_plus_minus_a_minus); + return; + } + } + + } // General case.

1 0

[GIT] ppl/ppl(floating_point): Fixed a bug in Linear_Form::operator<<()
by Fabio Biselli 16 Sep '09

16 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 56bd6524e6e38b943e424cdd83365c053edffad5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=56bd6524e6e3… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Wed Sep 16 14:10:28 2009 +0200 Fixed a bug in Linear_Form::operator<<() Fixed a bug in Octagonal_Shape::linear_form_upper_bound() Added a test --- src/Linear_Form.templates.hh | 2 +- src/Octagonal_Shape.templates.hh | 2 +- tests/Floating_Point_Expression/affineimage3.cc | 49 ++++++++++++++++++++-- 3 files changed, 46 insertions(+), 7 deletions(-) diff --git a/src/Linear_Form.templates.hh b/src/Linear_Form.templates.hh index fc7e81e..46aaf8c 100644 --- a/src/Linear_Form.templates.hh +++ b/src/Linear_Form.templates.hh @@ -385,7 +385,7 @@ IO_Operators::operator<<(std::ostream& s, const Linear_Form<C>& f) { const C& fv = f[v+1]; if (fv != 0) { if (first) { - if (fv == 1.0) + if (fv == -1.0) s << "-"; else if (fv != 1.0) s << fv << "*"; diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 9251559..9d4e70c 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -5151,7 +5151,7 @@ linear_form_upper_bound(const Linear_Form< Interval<T, Interval_Info> >& lf, curr_coefficient = &(lf.coefficient(Variable(curr_var))); assign_r(curr_lb, curr_coefficient->lower(), ROUND_NOT_NEEDED); assign_r(curr_ub, curr_coefficient->upper(), ROUND_NOT_NEEDED); - if (curr_lb != 0 && curr_ub != 0) { + if (curr_lb != 0 || curr_ub != 0) { // FIXME: ensure that ROUND_IGNORE works fine with divisions by 2. assign_r(curr_var_ub, matrix[n_var+1][n_var], ROUND_NOT_NEEDED); div_2exp_assign_r(curr_var_ub, curr_var_ub, 1, ROUND_IGNORE); diff --git a/tests/Floating_Point_Expression/affineimage3.cc b/tests/Floating_Point_Expression/affineimage3.cc index a2bdc0f..8be7386 100644 --- a/tests/Floating_Point_Expression/affineimage3.cc +++ b/tests/Floating_Point_Expression/affineimage3.cc @@ -260,9 +260,48 @@ bool test08() { return true; } -// tests affine_image(A, i + i1 * A + i2 * B) +// tests affine_image(A, i1*A + i2*B + i3) bool test09() { - return true; + + Variable A(0); + Variable B(1); + + Octagonal_Shape<double> oc1(2); + oc1.add_constraint(A >= 0); + oc1.add_constraint(A <= 2); + oc1.add_constraint(B >= 0); + oc1.add_constraint(B <= 2); + oc1.add_constraint(A - B >= 0); + + print_constraints(oc1, "*** oc1 ***"); + + db_r_oc i3(0); + i3.join_assign(2); + db_r_oc i2(1); + i2.join_assign(2); + db_r_oc i1(1); + i1.join_assign(1); + + Linear_Form<db_r_oc> l(i3); + + l += i1*Linear_Form<db_r_oc>(A); + l += i2*Linear_Form<db_r_oc>(B);; + print_constraints(oc1, "*** oc1.affine_image(A,i1*A+i2*B+i3) ***"); + oc1.affine_image(A,l); + + Octagonal_Shape<double> know_result(2); + know_result.add_constraint(A >= 0); + know_result.add_constraint(A <= 8); + know_result.add_constraint(B >= 0); + know_result.add_constraint(B <= 2); + know_result.add_constraint(A - B <= 6); + know_result.add_constraint(A + B <= 10); + know_result.add_constraint(-A + B <= 0); + know_result.add_constraint(-A - B <= 0); + + bool ok = (oc1 == know_result); + + return ok; } } //namespace @@ -270,11 +309,11 @@ bool test09() { BEGIN_MAIN DO_TEST(test01); DO_TEST(test02); - DO_TEST(test03); /* FIXME: Not yet tested! + DO_TEST(test03); /* FIXME: Not yet tested DO_TEST(test04); DO_TEST(test05); DO_TEST(test06); DO_TEST(test07); - DO_TEST(test08); - DO_TEST(test09); */ + DO_TEST(test08); */ + DO_TEST(test09); END_MAIN

1 0