September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Added test for Octagonal_Shape<T>:: refine_fp_interval_abstract_store.
by Roberto Amadini 18 Sep '09

18 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 4a811294d3accd1cf5fbcc0470e8e70905c076dd URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=4a811294d3ac… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Fri Sep 18 12:32:47 2009 +0200 Added test for Octagonal_Shape<T>::refine_fp_interval_abstract_store. --- .../floatingpointexpr1.cc | 8 ++-- tests/Floating_Point_Expression/refinelf1.cc | 47 ++++++++++++++++++++ 2 files changed, 51 insertions(+), 4 deletions(-) diff --git a/tests/Floating_Point_Expression/floatingpointexpr1.cc b/tests/Floating_Point_Expression/floatingpointexpr1.cc index 1553458..624f00f 100644 --- a/tests/Floating_Point_Expression/floatingpointexpr1.cc +++ b/tests/Floating_Point_Expression/floatingpointexpr1.cc @@ -60,16 +60,16 @@ typedef Opposite_Floating_Point_Expression<db_r_oc, IEEE754_Single> opp_fpeds; typedef Opposite_Floating_Point_Expression<db_r_oc, IEEE754_Double> opp_fpedd; typedef Floating_Point_Expression<fl_r_oc, IEEE754_Single>::FP_Interval_Abstract_Store sstr; -typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Single>::FP_Interval_Abstract_Store dstr; +typedef Floating_Point_Expression<db_r_oc, IEEE754_Single>::FP_Interval_Abstract_Store dstr; typedef Floating_Point_Expression<fl_r_oc, IEEE754_Single>::FP_Linear_Form_Abstract_Store lsstr; -typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Single>::FP_Linear_Form_Abstract_Store ldstr; +typedef Floating_Point_Expression<db_r_oc, IEEE754_Single>::FP_Linear_Form_Abstract_Store ldstr; typedef Floating_Point_Expression<fl_r_oc, IEEE754_Double>::FP_Interval_Abstract_Store sdtr; -typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Double>::FP_Interval_Abstract_Store ddtr; +typedef Floating_Point_Expression<db_r_oc, IEEE754_Double>::FP_Interval_Abstract_Store ddtr; typedef Floating_Point_Expression<fl_r_oc, IEEE754_Double>::FP_Linear_Form_Abstract_Store lsdtr; -typedef Constant_Floating_Point_Expression<db_r_oc, IEEE754_Double>::FP_Linear_Form_Abstract_Store lddtr; +typedef Floating_Point_Expression<db_r_oc, IEEE754_Double>::FP_Linear_Form_Abstract_Store lddtr; namespace { diff --git a/tests/Floating_Point_Expression/refinelf1.cc b/tests/Floating_Point_Expression/refinelf1.cc index 8f25961..5d15285 100644 --- a/tests/Floating_Point_Expression/refinelf1.cc +++ b/tests/Floating_Point_Expression/refinelf1.cc @@ -23,6 +23,8 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "ppl_test.hh" +typedef Floating_Point_Expression<db_r_oc, IEEE754_Double>::FP_Interval_Abstract_Store ddtr; + namespace { // tests trivial cases @@ -403,6 +405,50 @@ test10() { return ok; } +// tests Octagonal_Shape<T>::refine_fp_interval_abstract_store +// FIXME: this test should be parametric according to the floating point +// format of analyzer and analyzed. +bool +test11() { + Variable A(0); + Variable B(1); + ddtr store; + db_r_oc tmp(-2.5); + tmp.join_assign(3.5); + store[0] = tmp; + tmp.lower() = -4; + tmp.upper() = 4; + store[1] = tmp; + Octagonal_Shape<double> oc1(2); + oc1.add_constraint(A <= 2); + oc1.add_constraint(B <= 2); + oc1.add_constraint(A >= -3); + oc1.add_constraint(2*B >= -3); + oc1.refine_fp_interval_abstract_store(store); + + nout << "*** store[0] ***" << endl + << store[0] << endl; + + db_r_oc known_result1(-2.5); + known_result1.join_assign(2); + nout << "*** known_result1 ***" << endl + << known_result1 << endl; + + bool ok1 = (store[0] == known_result1); + + nout << "*** store[1] ***" << endl + << store[1] << endl; + + db_r_oc known_result2(-1.5); + known_result2.join_assign(2); + nout << "*** known_result2 ***" << endl + << known_result2 << endl; + + bool ok2 = (store[1] == known_result2); + + return ok1 && ok2; +} + } //namespace BEGIN_MAIN @@ -416,4 +462,5 @@ BEGIN_MAIN DO_TEST(test08); DO_TEST(test09); DO_TEST(test10); + DO_TEST(test11); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Added function BD_Shape::affine_image( const Variable& var,
by Fabio Biselli 18 Sep '09

18 Sep '09

Module: ppl/ppl Branch: floating_point Commit: a6766fae53279618b5f623bdce9f5c84948474df URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a6766fae5327… Author: Fabio Biselli <fabio.biselli(a)studenti.unipr.it> Date: Fri Sep 18 14:27:30 2009 +0200 Added function BD_Shape::affine_image(const Variable& var, const Linear_Form< Interval<T, Interval_Info> >& lf); Added interfaces for auxiliary functions: BD_Shape::inhomogeneous_affine_image(...); BD_Shape::one_variable_affine_image(...); BD_Shape::two_variable_affine_image(...); Added a preliminary test. --- src/BD_Shape.defs.hh | 60 +++++++++++++ src/BD_Shape.templates.hh | 126 +++++++++++++++++++++++++++ tests/Floating_Point_Expression/Makefile.am | 4 +- tests/Floating_Point_Expression/bdshape1.cc | 58 ++++++++++++ 4 files changed, 247 insertions(+), 1 deletions(-) Diff: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commitdiff;h=a6766fae…

1 0

[GIT] ppl/ppl(floating_point): Added a first implementation of overapproximate_linear_form.
by Fabio Bossi 18 Sep '09

18 Sep '09

Module: ppl/ppl Branch: floating_point Commit: c6258052096010a54056670b55879e5f0c4f0856 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c62580520960… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Sep 18 12:05:02 2009 +0200 Added a first implementation of overapproximate_linear_form. --- src/Polyhedron.defs.hh | 1 + src/Polyhedron.templates.hh | 33 +++++++++++++++++++++++++++++++++ 2 files changed, 34 insertions(+), 0 deletions(-) diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 62673bb..3ea0e58 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -2569,6 +2569,7 @@ protected: template <typename FP_Format, typename Interval_Info> static void overapproximate_linear_form( const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, + const dimension_type lf_dimension, const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store, Linear_Form<Interval <FP_Format, Interval_Info> >& result); diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 4c49c85..51c98c4 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -306,8 +306,41 @@ template <typename FP_Format, typename Interval_Info> void Polyhedron::overapproximate_linear_form( const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, + const dimension_type lf_dimension, const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store, Linear_Form<Interval <FP_Format, Interval_Info> >& result) { + + // Check that FP_Format is indeed a floating point type. + PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact, + "Polyhedron::overapproximate_linear_form:" + " FP_Format not a floating point type."); + + typedef Interval<FP_Format, Interval_Info> FP_Interval_Type; + typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; + typedef std::map<dimension_type, FP_Interval_Type> Interval_Abstract_Store; + + result = FP_Linear_Form(lf.inhomogeneous_term()); + const FP_Interval_Type aux_divisor1(static_cast<FP_Format>(0.5)); + FP_Interval_Type aux_divisor2(aux_divisor1); + aux_divisor2.lower() = static_cast<FP_Format>(-0.5); + + for (dimension_type i = 0; i < lf_dimension; ++i) { + Variable curr_var(i); + const FP_Interval_Type& curr_coeff = lf.coefficient(curr_var); + FP_Format curr_lb = curr_coeff.lower(); + FP_Format curr_ub = curr_coeff.upper(); + if (curr_lb != 0 || curr_ub != 0) { + FP_Interval_Type curr_addend(curr_ub - curr_lb); + curr_addend *= aux_divisor2; + curr_addend *= store[i]; + result += curr_addend; + curr_addend = FP_Interval_Type(curr_lb + curr_ub); + curr_addend *= aux_divisor1; + curr_addend *= curr_var; + result += curr_addend; + } + } + } } // namespace Parma_Polyhedra_Library

1 0

[GIT] ppl/ppl(pip): Fixed ASCII dump/load methods, solving compilation issues.
by Francois GALEA 18 Sep '09

18 Sep '09

Module: ppl/ppl Branch: pip Commit: 1271e1583604aec39697a3998ad8de90b3df5bf5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1271e1583604… Author: Francois GALEA <fgalea(a)verlaine.prism.uvsq.fr> Date: Fri Sep 18 11:32:12 2009 +0200 Fixed ASCII dump/load methods, solving compilation issues. --- src/PIP_Tree.cc | 25 +++++++++++++++++++++++-- src/PIP_Tree.defs.hh | 3 +++ 2 files changed, 26 insertions(+), 2 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index abdb0d5..8ed994e 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -340,6 +340,23 @@ PIP_Solution_Node::Rational_Matrix::scale(const Coefficient &ratio) { } void +PIP_Tree_Node::ascii_dump(std::ostream& s) const { + s << "\nconstraints_\n"; + constraints_.ascii_dump(s); +} + +bool +PIP_Tree_Node::ascii_load(std::istream& s) { + std::string str; + if (!(s >> str) || str != "constraints_") + return false; + constraints_.ascii_load(s); + + PPL_ASSERT(OK()); + return true; +} + +void PIP_Solution_Node::Rational_Matrix::ascii_dump(std::ostream& s) const { s << "denominator " << denominator << "\n"; Matrix::ascii_dump(s); @@ -360,6 +377,8 @@ PIP_Solution_Node::Rational_Matrix::ascii_load(std::istream& s) { void PIP_Solution_Node::ascii_dump(std::ostream& s) const { + PIP_Tree_Node::ascii_dump(s); + s << "\nvariable_tableau\n"; tableau.s.ascii_dump(s); @@ -367,11 +386,13 @@ PIP_Solution_Node::ascii_dump(std::ostream& s) const { tableau.t.ascii_dump(s); } - bool PIP_Solution_Node::ascii_load(std::istream& s) { + if (!PIP_Tree_Node::ascii_load(s)) + return false; + std::string str; - if (!(s >> str) || str != "simplex_tableau") + if (!(s >> str) || str != "variable_tableau") return false; if (!tableau.s.ascii_load(s)) return false; diff --git a/src/PIP_Tree.defs.hh b/src/PIP_Tree.defs.hh index f23bf31..7ac9ec2 100644 --- a/src/PIP_Tree.defs.hh +++ b/src/PIP_Tree.defs.hh @@ -70,6 +70,9 @@ public: */ const Constraint_System& constraints() const; + void ascii_dump(std::ostream& s) const; + bool ascii_load(std::istream& s); + protected: //! Default constructor. PIP_Tree_Node();

1 0

[GIT] ppl/ppl(pip): Finished parametric simplex algorithm. No cut generation yet.
by François Galea 18 Sep '09

18 Sep '09

Module: ppl/ppl Branch: pip Commit: 80b7e08459297f6dc193ad8988e49baa21e27df4 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=80b7e0845929… Author: François Galea <francois.galea(a)uvsq.fr> Date: Fri Sep 18 09:21:54 2009 +0200 Finished parametric simplex algorithm. No cut generation yet. --- src/PIP_Tree.cc | 30 +++++++++++++++++++++++++++++- 1 files changed, 29 insertions(+), 1 deletions(-) diff --git a/src/PIP_Tree.cc b/src/PIP_Tree.cc index 604683c..abdb0d5 100644 --- a/src/PIP_Tree.cc +++ b/src/PIP_Tree.cc @@ -871,8 +871,36 @@ PIP_Solution_Node::solve(PIP_Tree_Node*& parent_ref, return OPTIMIZED_PIP_PROBLEM; } } - //FIXME: to be finished + /* Otherwise, all parameters are positive: we have found a continuous + * solution. If the solution happens to be integer, then it is a + * solution of the integer problem. Otherwise, we may need to generate + * a new cut to try and get back into the integer case. */ + else { +#ifdef NOISY_PIP + std::cout << "All parameters are positive." + << std::endl; +#endif + tableau.s.normalize(); + tableau.t.normalize(); + + if (tableau.s.is_integer() && tableau.t.is_integer()) { + /* The solution is integer */ +#ifdef NOISY_PIP + std::cout << "Solution found for in current node." + << std::endl; +#endif + return OPTIMIZED_PIP_PROBLEM; + } + else { + /* The solution is non-integer. We have to generate a cut. */ + //FIXME: to be finished +#ifdef NOISY_PIP + std::cout << "Cut generation required." + << std::endl; +#endif + } + } } // Main loop of the simplex algorithm return OPTIMIZED_PIP_PROBLEM;

1 0

[GIT] ppl/ppl(floating_point): Coverage of 100% reached for refine_with_linear_form_inequality.
by Roberto Amadini 18 Sep '09

18 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 876484912959e603f7e8406a16453b63a39004e9 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=876484912959… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Fri Sep 18 10:41:44 2009 +0200 Coverage of 100% reached for refine_with_linear_form_inequality. --- tests/Floating_Point_Expression/refinelf1.cc | 5 ++--- 1 files changed, 2 insertions(+), 3 deletions(-) diff --git a/tests/Floating_Point_Expression/refinelf1.cc b/tests/Floating_Point_Expression/refinelf1.cc index 235a4d6..8f25961 100644 --- a/tests/Floating_Point_Expression/refinelf1.cc +++ b/tests/Floating_Point_Expression/refinelf1.cc @@ -323,6 +323,7 @@ test08() { } // tests [0.25, 0.5] * A + [-2, -1] * B <= [-7, -2] +// and [-7, -2] <= [0.25, 0.5] * A + [-2, -1] * B bool test09() { Variable A(0); @@ -352,7 +353,7 @@ test09() { known_result.add_constraint(2*A <= 7); print_constraints(known_result, "*** known_result ***"); - bool ok = (oc1 == known_result); + bool ok1 = (oc1 == known_result); oc1.refine_with_linear_form_inequality(l2, l1); print_constraints(oc1, "*** [-7, -2] <= [0.25, 0.5]*A + [-2, -1]*B ***"); @@ -362,8 +363,6 @@ test09() { bool ok2 = (oc1 == known_result); return ok1 && ok2; - - return ok; } // tests [-5, -1] * A <= [2, 3] * B + [0.5, 1]

1 0

[GIT] ppl/ppl(floating_point): Added a test.
by Roberto Amadini 18 Sep '09

18 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 9015398c7a2e8c38e8cb99afb34c53b40b03f6cd URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=9015398c7a2e… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Fri Sep 18 10:36:24 2009 +0200 Added a test. --- tests/Floating_Point_Expression/refinelf1.cc | 9 +++++++++ 1 files changed, 9 insertions(+), 0 deletions(-) diff --git a/tests/Floating_Point_Expression/refinelf1.cc b/tests/Floating_Point_Expression/refinelf1.cc index 485348d..235a4d6 100644 --- a/tests/Floating_Point_Expression/refinelf1.cc +++ b/tests/Floating_Point_Expression/refinelf1.cc @@ -354,6 +354,15 @@ test09() { bool ok = (oc1 == known_result); + oc1.refine_with_linear_form_inequality(l2, l1); + print_constraints(oc1, "*** [-7, -2] <= [0.25, 0.5]*A + [-2, -1]*B ***"); + + print_constraints(known_result, "*** known_result2 ***"); + + bool ok2 = (oc1 == known_result); + + return ok1 && ok2; + return ok; }

1 0

[GIT] ppl/ppl(floating_point): Added missing multiplications by 2.
by Fabio Bossi 18 Sep '09

18 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 0cbe08ccba51a6dbc6a22aa2c50af0d7729dace5 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0cbe08ccba51… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Sep 18 10:31:58 2009 +0200 Added missing multiplications by 2. All tests now pass. --- src/Octagonal_Shape.templates.hh | 6 ++++-- tests/Floating_Point_Expression/refinelf1.cc | 4 ++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/Octagonal_Shape.templates.hh b/src/Octagonal_Shape.templates.hh index 6734c48..b21bc3d 100644 --- a/src/Octagonal_Shape.templates.hh +++ b/src/Octagonal_Shape.templates.hh @@ -828,9 +828,11 @@ Octagonal_Shape<T>::refine_with_linear_form_inequality( in the main diagonal of the matrix. They will be moved later. */ linear_form_upper_bound(right_minus_left + var, upper_bound); - assign_r(matrix[n_var+1][n_var+1], upper_bound, ROUND_NOT_NEEDED); + mul_2exp_assign_r(matrix[n_var+1][n_var+1], upper_bound, 1, + ROUND_UP); linear_form_upper_bound(right_minus_left - var, upper_bound); - assign_r(matrix[n_var][n_var], upper_bound, ROUND_NOT_NEEDED); + mul_2exp_assign_r(matrix[n_var][n_var], upper_bound, 1, + ROUND_UP); } } diff --git a/tests/Floating_Point_Expression/refinelf1.cc b/tests/Floating_Point_Expression/refinelf1.cc index 7998d21..485348d 100644 --- a/tests/Floating_Point_Expression/refinelf1.cc +++ b/tests/Floating_Point_Expression/refinelf1.cc @@ -406,6 +406,6 @@ BEGIN_MAIN DO_TEST(test06); DO_TEST(test07); DO_TEST(test08); - DO_TEST(test09); //FIXME: A <= 1.75 (cut&paste error???) - DO_TEST(test10); //FIXME: A >= -7.5 (cut&paste error???) + DO_TEST(test09); + DO_TEST(test10); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Added interfaces (and empty body) of two new methods.
by Fabio Bossi 18 Sep '09

18 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 81a3ebf8481602636a20697a3ab1870d04fbba5d URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=81a3ebf84816… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Sep 18 10:11:16 2009 +0200 Added interfaces (and empty body) of two new methods. --- src/Polyhedron.defs.hh | 14 +++++++++++++- src/Polyhedron.templates.hh | 17 +++++++++++++++++ 2 files changed, 30 insertions(+), 1 deletions(-) diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 50d27a5..62673bb 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -47,7 +47,10 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Box.types.hh" #include "BD_Shape.types.hh" #include "Octagonal_Shape.types.hh" +#include "Interval.types.hh" +#include "Linear_Form.types.hh" #include <vector> +#include <map> #include <iosfwd> namespace Parma_Polyhedra_Library { @@ -1142,6 +1145,10 @@ public: Coefficient_traits::const_reference denominator = Coefficient_one()); + template <typename FP_Format, typename Interval_Info> + void affine_image(const Variable& var, + const Linear_Form<Interval <FP_Format, Interval_Info> >& lf); + /*! \brief Assigns to \p *this the \ref Single_Update_Affine_Functions "affine preimage" @@ -2559,8 +2566,13 @@ protected: //@} // Exception Throwers #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) -}; + template <typename FP_Format, typename Interval_Info> + static void overapproximate_linear_form( + const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, + const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store, + Linear_Form<Interval <FP_Format, Interval_Info> >& result); +}; namespace std { diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 86e8619..4c49c85 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -25,7 +25,10 @@ site: http://www.cs.unipr.it/ppl/ . */ #include "Generator.defs.hh" #include "MIP_Problem.defs.hh" +#include "Interval.defs.hh" +#include "Linear_Form.defs.hh" #include <algorithm> +#include <map> #include <deque> namespace Parma_Polyhedra_Library { @@ -293,6 +296,20 @@ Polyhedron::map_space_dimensions(const Partial_Function& pfunc) { PPL_ASSERT_HEAVY(OK(true)); } +template <typename FP_Format, typename Interval_Info> +void +Polyhedron::affine_image(const Variable& var, + const Linear_Form<Interval <FP_Format, Interval_Info> >& lf) { +} + +template <typename FP_Format, typename Interval_Info> +void +Polyhedron::overapproximate_linear_form( + const Linear_Form<Interval <FP_Format, Interval_Info> >& lf, + const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store, + Linear_Form<Interval <FP_Format, Interval_Info> >& result) { +} + } // namespace Parma_Polyhedra_Library #endif // !defined(PPL_Polyhedron_templates_hh)

1 0

[GIT] ppl/ppl(floating_point): Added two more tests in refinelf1.cc
by Roberto Amadini 18 Sep '09

18 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 5decdfb92cce7eaa4aac059286afb163bac93016 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=5decdfb92cce… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Fri Sep 18 09:48:03 2009 +0200 Added two more tests in refinelf1.cc Improved a test in affineimage3.cc --- tests/Floating_Point_Expression/affineimage3.cc | 19 +++--- tests/Floating_Point_Expression/refinelf1.cc | 75 +++++++++++++++++++++++ 2 files changed, 85 insertions(+), 9 deletions(-) diff --git a/tests/Floating_Point_Expression/affineimage3.cc b/tests/Floating_Point_Expression/affineimage3.cc index 5736f8d..6633d3e 100644 --- a/tests/Floating_Point_Expression/affineimage3.cc +++ b/tests/Floating_Point_Expression/affineimage3.cc @@ -299,15 +299,16 @@ bool test10() { oc1.add_constraint(B >= 0); oc1.add_constraint(B <= 2); oc1.add_constraint(A - B >= 0); - 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);; + db_r_oc tmp(1); + tmp.join_assign(1); + Linear_Form<db_r_oc> l(A); + l *= tmp; + tmp.lower() = 0; + tmp.upper() = 2; + l += tmp; + tmp.lower() = 1; + tmp.upper() = 2; + l += tmp * Linear_Form<db_r_oc>(B); oc1.affine_image(A,l); print_constraints(oc1, "*** oc1.affine_image(A, i + i0*A + i1*B) ***"); diff --git a/tests/Floating_Point_Expression/refinelf1.cc b/tests/Floating_Point_Expression/refinelf1.cc index 4515350..7998d21 100644 --- a/tests/Floating_Point_Expression/refinelf1.cc +++ b/tests/Floating_Point_Expression/refinelf1.cc @@ -322,6 +322,79 @@ test08() { return ok; } +// tests [0.25, 0.5] * A + [-2, -1] * B <= [-7, -2] +bool +test09() { + Variable A(0); + Variable B(1); + + Octagonal_Shape<double> oc1(3); + oc1.add_constraint(A <= 2); + oc1.add_constraint(A - B <= 3); + oc1.add_constraint(B <= 2); + Octagonal_Shape<double> known_result(oc1); + + db_r_oc tmp(-7); + tmp.join_assign(-2); + Linear_Form<db_r_oc> l2(tmp); + Linear_Form<db_r_oc> l1(A); + tmp.lower() = 0.25; + tmp.upper() = 0.5; + l1 *= tmp; + tmp.lower() = -2; + tmp.upper() = -1; + l1 += tmp * Linear_Form<db_r_oc>(B); + oc1.refine_with_linear_form_inequality(l1, l2); + print_constraints(oc1, "*** [0.25, 0.5]*A + [-2, -1]*B <= [-7, -2] ***"); + + known_result.add_constraint(2*B + 2*A <= 11); + known_result.add_constraint(-2*B + 2*A <= 3); + known_result.add_constraint(2*A <= 7); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (oc1 == known_result); + + return ok; +} + +// tests [-5, -1] * A <= [2, 3] * B + [0.5, 1] +bool +test10() { + Variable A(0); + Variable B(1); + + Octagonal_Shape<float> oc1(3); + oc1.add_constraint(A <= 2); + oc1.add_constraint(A - B <= 3); + oc1.add_constraint(B <= 2); + Octagonal_Shape<float> known_result(oc1); + fl_r_oc tmp(2); + tmp.join_assign(3); + Linear_Form<fl_r_oc> l2(B); + l2 *= tmp; + tmp.lower() = 0.5; + tmp.upper() = 1; + l2 += tmp; + Linear_Form<fl_r_oc> l1(A); + tmp.lower() = -5; + tmp.upper() = -1; + l1 *= tmp; + oc1.refine_with_linear_form_inequality(l1, l2); + print_constraints(oc1, "*** [-5, -1] * A <= [2, 3] * B + [0.5, 1] ***"); + + known_result.add_constraint(B - A <= 17); + known_result.add_constraint(B + A <= 21); + known_result.add_constraint(-B - A <= 13); + known_result.add_constraint(-B + A <= 17); + known_result.add_constraint(A <= 19); + known_result.add_constraint(-A <= 15); + print_constraints(known_result, "*** known_result ***"); + + bool ok = (oc1 == known_result); + + return ok; +} + } //namespace BEGIN_MAIN @@ -333,4 +406,6 @@ BEGIN_MAIN DO_TEST(test06); DO_TEST(test07); DO_TEST(test08); + DO_TEST(test09); //FIXME: A <= 1.75 (cut&paste error???) + DO_TEST(test10); //FIXME: A >= -7.5 (cut&paste error???) END_MAIN

1 0