September 2009 - PPL-devel - BUGSENG Mailman

[GIT] ppl/ppl(floating_point): Improved test05
by Roberto Amadini 28 Sep '09

28 Sep '09

Module: ppl/ppl Branch: floating_point Commit: e4f52c87f28fc156fa7f5407f4680f46d43e7403 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e4f52c87f28f… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Mon Sep 28 16:04:33 2009 +0200 Improved test05 --- tests/Floating_Point_Expression/polyhedron2.cc | 24 +++++++++++++++--------- 1 files changed, 15 insertions(+), 9 deletions(-) diff --git a/tests/Floating_Point_Expression/polyhedron2.cc b/tests/Floating_Point_Expression/polyhedron2.cc index b6298ea..94d7c24 100644 --- a/tests/Floating_Point_Expression/polyhedron2.cc +++ b/tests/Floating_Point_Expression/polyhedron2.cc @@ -163,7 +163,7 @@ test04() { } // tests (2/3)*B + [-0.5, 0.5] >= (1/3)*A -// FIXME: Not pass at the moment. +// where A = B = [-1, 1] bool test05() { Variable A(0); @@ -185,16 +185,11 @@ test05() { lb += tmp; NNC_Polyhedron ph(2); + FP_Linear_Form l(tmp0); + ph.affine_image(A, l, store); + ph.affine_image(B, l, store); ph.generalized_refine_with_linear_form_inequality( lb, la, GREATER_OR_EQUAL, store); - ph.generalized_refine_with_linear_form_inequality( - FP_Linear_Form(A), FP_Linear_Form(FP_Interval(-1)), GREATER_OR_EQUAL, store); - ph.generalized_refine_with_linear_form_inequality( - FP_Linear_Form(A), FP_Linear_Form(FP_Interval(1)), LESS_OR_EQUAL, store); - ph.generalized_refine_with_linear_form_inequality( - FP_Linear_Form(B), FP_Linear_Form(FP_Interval(-1)), GREATER_OR_EQUAL, store); - ph.generalized_refine_with_linear_form_inequality( - FP_Linear_Form(B), FP_Linear_Form(FP_Interval(1)), LESS_OR_EQUAL, store); print_constraints(ph, "*** ph ***"); NNC_Polyhedron known_result1(2); @@ -207,6 +202,17 @@ test05() { bool ok1 = ph.contains(known_result1); + ph.refine_fp_interval_abstract_store(store); + nout << "*** FP_Interval_Abstract_Store ***" << endl; + + nout << "A = " << store.get_interval(A) << endl; + bool ok2 = tmp0.contains(store.get_interval(A)); + + nout << "B = " << store.get_interval(B) << endl; + bool ok3 = tmp0.contains(store.get_interval(B)); + + return ok1 && ok2 && ok3; + return ok1; }

1 0

[GIT] ppl/ppl(floating_point): Fixed test05.
by Fabio Bossi 28 Sep '09

28 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 2fcd493ce5e2f9be78ed60654b6d2d39096805d0 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=2fcd493ce5e2… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Mon Sep 28 15:24:11 2009 +0200 Fixed test05. --- tests/Floating_Point_Expression/polyhedron2.cc | 25 ++++++++++++----------- 1 files changed, 13 insertions(+), 12 deletions(-) diff --git a/tests/Floating_Point_Expression/polyhedron2.cc b/tests/Floating_Point_Expression/polyhedron2.cc index 2a285a2..b6298ea 100644 --- a/tests/Floating_Point_Expression/polyhedron2.cc +++ b/tests/Floating_Point_Expression/polyhedron2.cc @@ -187,28 +187,29 @@ test05() { NNC_Polyhedron ph(2); ph.generalized_refine_with_linear_form_inequality( lb, la, GREATER_OR_EQUAL, store); + ph.generalized_refine_with_linear_form_inequality( + FP_Linear_Form(A), FP_Linear_Form(FP_Interval(-1)), GREATER_OR_EQUAL, store); + ph.generalized_refine_with_linear_form_inequality( + FP_Linear_Form(A), FP_Linear_Form(FP_Interval(1)), LESS_OR_EQUAL, store); + ph.generalized_refine_with_linear_form_inequality( + FP_Linear_Form(B), FP_Linear_Form(FP_Interval(-1)), GREATER_OR_EQUAL, store); + ph.generalized_refine_with_linear_form_inequality( + FP_Linear_Form(B), FP_Linear_Form(FP_Interval(1)), LESS_OR_EQUAL, store); print_constraints(ph, "*** ph ***"); NNC_Polyhedron known_result1(2); known_result1.add_constraint(2*A <= 4*B + 3); + known_result1.add_constraint(A >= -1); + known_result1.add_constraint(A <= 1); + known_result1.add_constraint(B >= -1); + known_result1.add_constraint(B <= 1); print_constraints(known_result1, "*** known_result1 ***"); bool ok1 = ph.contains(known_result1); - ph.refine_fp_interval_abstract_store(store); - nout << "*** FP_Interval_Abstract_Store ***" << endl; - - nout << "A = " << store.get_interval(A) << endl; - bool ok2 = tmp0.contains(store.get_interval(A)); - - nout << "B = " << store.get_interval(B) << endl; - bool ok3 = tmp0.contains(store.get_interval(B)); - - return ok1 && ok2 && ok3; + return ok1; } - - } // namespace BEGIN_MAIN

1 0

[GIT] ppl/ppl(floating_point): Modified test04 and test05.
by Roberto Amadini 28 Sep '09

28 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 1ddf04b0c29576fb94b513083211d152200dfcc8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1ddf04b0c295… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Mon Sep 28 15:07:52 2009 +0200 Modified test04 and test05. --- tests/Floating_Point_Expression/polyhedron2.cc | 13 +++++-------- 1 files changed, 5 insertions(+), 8 deletions(-) diff --git a/tests/Floating_Point_Expression/polyhedron2.cc b/tests/Floating_Point_Expression/polyhedron2.cc index fa75dad..2a285a2 100644 --- a/tests/Floating_Point_Expression/polyhedron2.cc +++ b/tests/Floating_Point_Expression/polyhedron2.cc @@ -133,11 +133,9 @@ test04() { ph.generalized_refine_with_linear_form_inequality( lk, -la, GREATER_OR_EQUAL, store); ph.generalized_refine_with_linear_form_inequality( - lk, lb, LESS_OR_EQUAL, store); - tmp = 3; - lk *= tmp; - tmp = 1; - lk += tmp; + lb, -lk, LESS_OR_EQUAL, store); + tmp = 0; + lk = FP_Linear_Form(tmp); ph.generalized_refine_with_linear_form_inequality( -lb, lk, LESS_THAN, store); print_constraints(ph, "*** ph ***"); @@ -157,7 +155,6 @@ test04() { nout << "A = " << store.get_interval(A) << endl; bool ok2 = tmp0.contains(store.get_interval(A)); - //FIXME: Sound, but not much precise. nout << "B = " << store.get_interval(B) << endl; bool ok3 = tmp0.contains(store.get_interval(B)); @@ -189,11 +186,11 @@ test05() { NNC_Polyhedron ph(2); ph.generalized_refine_with_linear_form_inequality( - lb, la, GREATER_THAN, store); + lb, la, GREATER_OR_EQUAL, store); print_constraints(ph, "*** ph ***"); NNC_Polyhedron known_result1(2); - known_result1.add_constraint(2*A <= 4*B + 1); + known_result1.add_constraint(2*A <= 4*B + 3); print_constraints(known_result1, "*** known_result1 ***"); bool ok1 = ph.contains(known_result1);

1 0

[GIT] ppl/ppl(floating_point): Modified poyhedron2. cc in order to test NNC_Polyhedron and
by Roberto Amadini 26 Sep '09

26 Sep '09

Module: ppl/ppl Branch: floating_point Commit: f5e8676cd64d4a14908d5ba845c9f50f79f2d33f URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=f5e8676cd64d… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Sat Sep 26 19:09:56 2009 +0200 Modified poyhedron2.cc in order to test NNC_Polyhedron and Polyhedron::generalized_refine_with_linear_form_inequality. --- tests/Floating_Point_Expression/polyhedron2.cc | 48 ++++++++++++++++-------- 1 files changed, 32 insertions(+), 16 deletions(-) diff --git a/tests/Floating_Point_Expression/polyhedron2.cc b/tests/Floating_Point_Expression/polyhedron2.cc index 06e88ae..fa75dad 100644 --- a/tests/Floating_Point_Expression/polyhedron2.cc +++ b/tests/Floating_Point_Expression/polyhedron2.cc @@ -1,5 +1,6 @@ -/* Test Polyhedron::refine_fp_interval_abstract_store and - Polyhedron::refine_with_linear_form_inequality. +/* Test Polyhedron::refine_fp_interval_abstract_store, + Polyhedron::refine_with_linear_form_inequality and + Polyhedron::generalized_refine_with_linear_form_inequality. Copyright (C) 2001-2009 Roberto Bagnara <bagnara(a)cs.unipr.it> This file is part of the Parma Polyhedra Library (PPL). @@ -69,16 +70,19 @@ test02() { return ph == known_result; } -// tests -A <= 0 && A <= 2 && -A <= 1 && -B <= -1 +// tests -A <= 0 && A <= 2 && -A <= 1 && -B <= -1 && C = 0 bool test03() { Variable A(0); Variable B(1); - FP_Interval_Abstract_Store store(2); - store.set_interval(A, FP_Interval(1)); - store.set_interval(B, FP_Interval(2)); - - C_Polyhedron ph(2); + Variable C(2); + FP_Interval_Abstract_Store store(3); + FP_Interval tmp(0); + store.set_interval(A, tmp); + store.set_interval(B, tmp); + store.set_interval(C, tmp); + + C_Polyhedron ph(3); ph.refine_with_linear_form_inequality(-FP_Linear_Form(A), FP_Linear_Form(FP_Interval(0)), store); ph.refine_with_linear_form_inequality(FP_Linear_Form(A), @@ -87,12 +91,17 @@ test03() { FP_Linear_Form(FP_Interval(1)), store); ph.refine_with_linear_form_inequality(-FP_Linear_Form(B), FP_Linear_Form(FP_Interval(-1)), store); + ph.generalized_refine_with_linear_form_inequality( + FP_Linear_Form(C), FP_Linear_Form(tmp), EQUAL, store); + ph.generalized_refine_with_linear_form_inequality( + FP_Linear_Form(C), FP_Linear_Form(tmp), NOT_EQUAL, store); print_constraints(ph, "*** ph ***"); - C_Polyhedron known_result(2); + C_Polyhedron known_result(3); known_result.add_constraint(A >= 0); known_result.add_constraint(A <= 2); known_result.add_constraint(B >= 1); + known_result.add_constraint(C == 0); print_constraints(known_result, "*** known_result ***"); return ph == known_result; @@ -117,16 +126,20 @@ test04() { FP_Linear_Form lk(tmp); C_Polyhedron ph(2); - ph.refine_with_linear_form_inequality(la, lk, store); + ph.generalized_refine_with_linear_form_inequality( + lk, la, GREATER_THAN, store); tmp = 1; lk -= tmp; - ph.refine_with_linear_form_inequality(-la, lk, store); - ph.refine_with_linear_form_inequality(lk, lb, store); + ph.generalized_refine_with_linear_form_inequality( + lk, -la, GREATER_OR_EQUAL, store); + ph.generalized_refine_with_linear_form_inequality( + lk, lb, LESS_OR_EQUAL, store); tmp = 3; lk *= tmp; tmp = 1; lk += tmp; - ph.refine_with_linear_form_inequality(-lb, lk, store); + ph.generalized_refine_with_linear_form_inequality( + -lb, lk, LESS_THAN, store); print_constraints(ph, "*** ph ***"); C_Polyhedron known_result1(2); @@ -174,11 +187,12 @@ test05() { tmp.upper() = 0.5; lb += tmp; - C_Polyhedron ph(2); - ph.refine_with_linear_form_inequality(la, lb, store); + NNC_Polyhedron ph(2); + ph.generalized_refine_with_linear_form_inequality( + lb, la, GREATER_THAN, store); print_constraints(ph, "*** ph ***"); - C_Polyhedron known_result1(2); + NNC_Polyhedron known_result1(2); known_result1.add_constraint(2*A <= 4*B + 1); print_constraints(known_result1, "*** known_result1 ***"); @@ -196,6 +210,8 @@ test05() { return ok1 && ok2 && ok3; } + + } // namespace BEGIN_MAIN

1 0

[GIT] ppl/ppl(floating_point): Temporarily edited tests/ Floating_Point_Expression/Makefile.am
by Roberto Amadini 26 Sep '09

26 Sep '09

Module: ppl/ppl Branch: floating_point Commit: e88b2238c1d7ebf462efe7c3e19dad77919ad14e URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=e88b2238c1d7… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Sat Sep 26 17:48:51 2009 +0200 Temporarily edited tests/Floating_Point_Expression/Makefile.am --- tests/Floating_Point_Expression/Makefile.am | 19 +++++++++++-------- 1 files changed, 11 insertions(+), 8 deletions(-) diff --git a/tests/Floating_Point_Expression/Makefile.am b/tests/Floating_Point_Expression/Makefile.am index b165040..823f722 100644 --- a/tests/Floating_Point_Expression/Makefile.am +++ b/tests/Floating_Point_Expression/Makefile.am @@ -50,13 +50,14 @@ $(top_builddir)/tests/libppl_tests.a \ $(top_builddir)/src/libppl.la \ @extra_libraries@ -ORIGINAL_TESTS = \ -bdshape1 \ -floatingpointexpr1 \ -linearform1 \ -octagonalshape1 \ -octagonalshape2 \ -polyhedron1 \ +ORIGINAL_TESTS = polyhedron2 + +#bdshape1 \ +#floatingpointexpr1 \ +#linearform1 \ +#octagonalshape1 \ +#octagonalshape2 \ +#polyhedron1 \ polyhedron2 DERIVED_TESTS = @@ -127,7 +128,9 @@ print_INSTANCES: # Sources for the tests # -polyhedron1_SOURCES = polyhedron1.cc +polyhedron2_SOURCES = polyhedron2.cc + +#polyhedron1_SOURCES = polyhedron1.cc #bdshape1_SOURCES = bdshape1.cc

1 0

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

26 Sep '09

Module: ppl/ppl Branch: floating_point Commit: d002a27f5e250e877bcf5e353cedd1f7b3682883 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d002a27f5e25… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Sat Sep 26 17:48:18 2009 +0200 Added another test. --- tests/Floating_Point_Expression/polyhedron2.cc | 43 +++++++++++++++++++++-- 1 files changed, 39 insertions(+), 4 deletions(-) diff --git a/tests/Floating_Point_Expression/polyhedron2.cc b/tests/Floating_Point_Expression/polyhedron2.cc index 8dedc6f..06e88ae 100644 --- a/tests/Floating_Point_Expression/polyhedron2.cc +++ b/tests/Floating_Point_Expression/polyhedron2.cc @@ -111,8 +111,6 @@ test04() { store.set_interval(B, tmp0); FP_Interval tmp(tmp0); tmp = 2; - //tmp.lower() = 2; - //tmp.upper() = 2; tmp /= FP_Interval(3); FP_Linear_Form la(A); FP_Linear_Form lb(B); @@ -154,11 +152,48 @@ test04() { } -// tests (2/3)*B - 0.5 >= (1/3)*A +// tests (2/3)*B + [-0.5, 0.5] >= (1/3)*A +// FIXME: Not pass at the moment. bool test05() { + Variable A(0); + Variable B(1); + FP_Interval tmp0(-1); + tmp0.join_assign(1); + FP_Interval_Abstract_Store store(2); + store.set_interval(A, tmp0); + store.set_interval(B, tmp0); + FP_Interval tmp(1); + tmp /= FP_Interval(3); + FP_Linear_Form la(A); + la *= tmp; + FP_Linear_Form lb(B); + tmp += tmp; + lb *= tmp; + tmp.lower() = -0.5; + tmp.upper() = 0.5; + lb += tmp; + + C_Polyhedron ph(2); + ph.refine_with_linear_form_inequality(la, lb, store); + print_constraints(ph, "*** ph ***"); + + C_Polyhedron known_result1(2); + known_result1.add_constraint(2*A <= 4*B + 1); + print_constraints(known_result1, "*** known_result1 ***"); + + bool ok1 = ph.contains(known_result1); - return true; + ph.refine_fp_interval_abstract_store(store); + nout << "*** FP_Interval_Abstract_Store ***" << endl; + + nout << "A = " << store.get_interval(A) << endl; + bool ok2 = tmp0.contains(store.get_interval(A)); + + nout << "B = " << store.get_interval(B) << endl; + bool ok3 = tmp0.contains(store.get_interval(B)); + + return ok1 && ok2 && ok3; } } // namespace

1 0

[GIT] ppl/ppl(floating_point): Added a test in polyhedron2.cc
by Roberto Amadini 26 Sep '09

26 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 66f38555e1528bf95da38877f0254a421eacd13c URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=66f38555e152… Author: Roberto Amadini <r.amadini(a)virgilio.it> Date: Sat Sep 26 17:09:48 2009 +0200 Added a test in polyhedron2.cc --- tests/Floating_Point_Expression/polyhedron2.cc | 96 ++++++++++++++++++++--- 1 files changed, 83 insertions(+), 13 deletions(-) diff --git a/tests/Floating_Point_Expression/polyhedron2.cc b/tests/Floating_Point_Expression/polyhedron2.cc index 3b57c57..8dedc6f 100644 --- a/tests/Floating_Point_Expression/polyhedron2.cc +++ b/tests/Floating_Point_Expression/polyhedron2.cc @@ -25,6 +25,7 @@ site: http://www.cs.unipr.it/ppl/ . */ namespace { +// tests incompatible dimensions. bool test01() { C_Polyhedron pol(1); @@ -42,6 +43,7 @@ test01() { pol.refine_with_linear_form_inequality(l1, l2, store); } catch (std::invalid_argument) { + nout << "incompatible dimensions." << endl; return true; } } @@ -49,22 +51,25 @@ test01() { return false; } +// tests A <= [57, 57] bool test02() { - C_Polyhedron result(1); + C_Polyhedron ph(1); FP_Interval_Abstract_Store store(1); store.set_interval(Variable(0), FP_Interval(1.5)); FP_Interval interval(57); FP_Linear_Form lf1(Variable(0)); FP_Linear_Form lf2(interval); - result.refine_with_linear_form_inequality(lf1, lf2, store); - print_constraints(result, "RESULT"); + ph.refine_with_linear_form_inequality(lf1, lf2, store); + print_constraints(ph, "*** A <= [57, 57] ***"); C_Polyhedron known_result(1); known_result.refine_with_constraint(Variable(0) <= 57); - print_constraints(known_result, "KNOWN RESULT"); - return result == known_result; + print_constraints(known_result, "*** known_result ***"); + + return ph == known_result; } +// tests -A <= 0 && A <= 2 && -A <= 1 && -B <= -1 bool test03() { Variable A(0); @@ -73,24 +78,87 @@ test03() { store.set_interval(A, FP_Interval(1)); store.set_interval(B, FP_Interval(2)); - C_Polyhedron result(2); - result.refine_with_linear_form_inequality(-FP_Linear_Form(A), + C_Polyhedron ph(2); + ph.refine_with_linear_form_inequality(-FP_Linear_Form(A), FP_Linear_Form(FP_Interval(0)), store); - result.refine_with_linear_form_inequality(FP_Linear_Form(A), + ph.refine_with_linear_form_inequality(FP_Linear_Form(A), FP_Linear_Form(FP_Interval(2)), store); - result.refine_with_linear_form_inequality(-FP_Linear_Form(A), + ph.refine_with_linear_form_inequality(-FP_Linear_Form(A), FP_Linear_Form(FP_Interval(1)), store); - result.refine_with_linear_form_inequality(-FP_Linear_Form(B), + ph.refine_with_linear_form_inequality(-FP_Linear_Form(B), FP_Linear_Form(FP_Interval(-1)), store); - print_constraints(result, "RESULT"); + print_constraints(ph, "*** ph ***"); C_Polyhedron known_result(2); known_result.add_constraint(A >= 0); known_result.add_constraint(A <= 2); known_result.add_constraint(B >= 1); - print_constraints(known_result, "KNOWN RESULT"); + print_constraints(known_result, "*** known_result ***"); + + return ph == known_result; +} + +// tests -A <= -1/3 && A <= 2/3 && -B <= 0 && B <= 1/3 +// and refine_fp_interval_abstract_store +bool +test04() { + Variable A(0); + Variable B(1); + FP_Interval tmp0(0); + tmp0.join_assign(10); + FP_Interval_Abstract_Store store(2); + store.set_interval(A, tmp0); + store.set_interval(B, tmp0); + FP_Interval tmp(tmp0); + tmp = 2; + //tmp.lower() = 2; + //tmp.upper() = 2; + tmp /= FP_Interval(3); + FP_Linear_Form la(A); + FP_Linear_Form lb(B); + FP_Linear_Form lk(tmp); + + C_Polyhedron ph(2); + ph.refine_with_linear_form_inequality(la, lk, store); + tmp = 1; + lk -= tmp; + ph.refine_with_linear_form_inequality(-la, lk, store); + ph.refine_with_linear_form_inequality(lk, lb, store); + tmp = 3; + lk *= tmp; + tmp = 1; + lk += tmp; + ph.refine_with_linear_form_inequality(-lb, lk, store); + print_constraints(ph, "*** ph ***"); + + C_Polyhedron known_result1(2); + known_result1.add_constraint(3*A >= 1); + known_result1.add_constraint(3*A <= 2); + known_result1.add_constraint(B >= 0); + known_result1.add_constraint(3*B <= 1); + print_constraints(known_result1, "*** known_result1 ***"); + + bool ok1 = ph.contains(known_result1); + + ph.refine_fp_interval_abstract_store(store); + nout << "*** FP_Interval_Abstract_Store ***" << endl; + + nout << "A = " << store.get_interval(A) << endl; + bool ok2 = tmp0.contains(store.get_interval(A)); + + //FIXME: Sound, but not much precise. + nout << "B = " << store.get_interval(B) << endl; + bool ok3 = tmp0.contains(store.get_interval(B)); + + return ok1 && ok2 && ok3; + +} + +// tests (2/3)*B - 0.5 >= (1/3)*A +bool +test05() { - return result == known_result; + return true; } } // namespace @@ -99,4 +167,6 @@ BEGIN_MAIN DO_TEST(test01); DO_TEST(test02); DO_TEST(test03); + DO_TEST(test04); + DO_TEST(test05); END_MAIN

1 0

[GIT] ppl/ppl(floating_point): Added missing const qualifiers.
by Fabio Bossi 26 Sep '09

26 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 0eb634591ec2041438c8f8d27e001540e4528742 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=0eb634591ec2… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Sat Sep 26 10:19:13 2009 +0200 Added missing const qualifiers. --- src/Octagonal_Shape.inlines.hh | 2 +- src/Polyhedron.inlines.hh | 2 +- src/Polyhedron.templates.hh | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Octagonal_Shape.inlines.hh b/src/Octagonal_Shape.inlines.hh index 73e4124..0776a7e 100644 --- a/src/Octagonal_Shape.inlines.hh +++ b/src/Octagonal_Shape.inlines.hh @@ -618,7 +618,7 @@ inline void Octagonal_Shape<T>::generalized_refine_with_linear_form_inequality( const Linear_Form< Interval<T, Interval_Info> >& left, const Linear_Form< Interval<T, Interval_Info> >& right, - Relation_Symbol relsym) { + const Relation_Symbol relsym) { switch (relsym) { case EQUAL: refine_with_linear_form_inequality(left, right); diff --git a/src/Polyhedron.inlines.hh b/src/Polyhedron.inlines.hh index affc433..8005c95 100644 --- a/src/Polyhedron.inlines.hh +++ b/src/Polyhedron.inlines.hh @@ -377,7 +377,7 @@ inline void Polyhedron::generalized_refine_with_linear_form_inequality( const Linear_Form< Interval<FP_Format, Interval_Info> >& left, const Linear_Form< Interval<FP_Format, Interval_Info> >& right, - Relation_Symbol relsym, + const Relation_Symbol relsym, const Box< Interval<FP_Format, Interval_Info> >& store) { switch (relsym) { case EQUAL: diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index e12b6fd..d35090b 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -301,7 +301,7 @@ Polyhedron::refine_with_linear_form_inequality( const Linear_Form< Interval<FP_Format, Interval_Info> >& left, const Linear_Form< Interval<FP_Format, Interval_Info> >& right, const Box< Interval<FP_Format, Interval_Info> >& store, - bool is_strict) { + const bool is_strict) { // Check that FP_Format is indeed a floating point type. PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact,

1 0

[GIT] ppl/ppl(floating_point): Implemented generalized_refine_with_linear_form_inequality.
by Fabio Bossi 25 Sep '09

25 Sep '09

Module: ppl/ppl Branch: floating_point Commit: c8904fdf2c5ef79dec43db7bb3104b9c2a861fe8 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=c8904fdf2c5e… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Sep 25 14:31:28 2009 +0200 Implemented generalized_refine_with_linear_form_inequality. Adapted refine_with_linear_form_inequality to accept strict inequalities on not necessarily closed polyhedra. --- src/Polyhedron.defs.hh | 51 ++++++++++++++++++++++++++++++++++++++++-- src/Polyhedron.inlines.hh | 31 ++++++++++++++++++++++++++ src/Polyhedron.templates.hh | 8 +++++- 3 files changed, 85 insertions(+), 5 deletions(-) diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh index 74eeb78..c3a33cb 100644 --- a/src/Polyhedron.defs.hh +++ b/src/Polyhedron.defs.hh @@ -978,9 +978,10 @@ public: */ void refine_with_congruences(const Congruence_System& cgs); - /*! - Refines \p *this with the constraint expressed by \p left \f$\leq\f$ - \p right. + /*! \brief + Refines \p *this with the constraint expressed by \p left \f$<\f$ + \p right if \p is_strict is set, with the constraint \p left \f$\leq\f$ + \p right otherwise. \param left The linear form on intervals with floating point boundaries that @@ -997,6 +998,9 @@ public: performed. All variables that occur in \p left or \p right MUST have an associated interval in it, and all of these intervals MUST be bounded. + \param is_strict + True if the comparison is strict. + \exception std::invalid_argument Thrown if \p left (or \p right) is dimension-incompatible with \p *this. @@ -1008,6 +1012,47 @@ public: void refine_with_linear_form_inequality( const Linear_Form< Interval<FP_Format, Interval_Info> >& left, const Linear_Form< Interval<FP_Format, Interval_Info> >& right, + const Box< Interval<FP_Format, Interval_Info> >& store, + bool is_strict = false); + + /*! \brief + Refines \p *this with the constraint expressed by \p left \f$\relsym\f$ + \p right, where \f$\relsym\f$ is the relation symbol specified by + \p relsym.. + + \param left + The linear form on intervals with floating point boundaries that + is on the left of the comparison operator. All of its coefficients + MUST be bounded. + + \param right + The linear form on intervals with floating point boundaries that + is on the right of the comparison operator. All of its coefficients + MUST be bounded. + + \param relsym + The relation symbol. + + \param store + The interval abstract store in which the test defining the filter is + performed. All variables that occur in \p left or \p right MUST have + an associated interval in it, and all of these intervals MUST be bounded. + + \exception std::invalid_argument + Thrown if \p left (or \p right) is dimension-incompatible with \p *this. + + \exception std::runtime_error + Thrown if \p relsym is not a valid relation symbol. + + This function is used in abstract interpretation to model a filter + that is generated by a comparison of two expressions that are correctly + approximated by \p left and \p right respectively. + */ + template <typename FP_Format, typename Interval_Info> + void generalized_refine_with_linear_form_inequality( + const Linear_Form< Interval<FP_Format, Interval_Info> >& left, + const Linear_Form< Interval<FP_Format, Interval_Info> >& right, + Relation_Symbol relsym, const Box< Interval<FP_Format, Interval_Info> >& store); //! Refines \p store with the constraints defining \p *this. diff --git a/src/Polyhedron.inlines.hh b/src/Polyhedron.inlines.hh index 5de0af8..affc433 100644 --- a/src/Polyhedron.inlines.hh +++ b/src/Polyhedron.inlines.hh @@ -374,6 +374,37 @@ Polyhedron::add_recycled_congruences(Congruence_System& cgs) { template <typename FP_Format, typename Interval_Info> inline void +Polyhedron::generalized_refine_with_linear_form_inequality( + const Linear_Form< Interval<FP_Format, Interval_Info> >& left, + const Linear_Form< Interval<FP_Format, Interval_Info> >& right, + Relation_Symbol relsym, + const Box< Interval<FP_Format, Interval_Info> >& store) { + switch (relsym) { + case EQUAL: + refine_with_linear_form_inequality(left, right, store, false); + refine_with_linear_form_inequality(right, left, store, false); + break; + case LESS_THAN: + refine_with_linear_form_inequality(left, right, store, true); + break; + case LESS_OR_EQUAL: + refine_with_linear_form_inequality(left, right, store, false); + break; + case GREATER_THAN: + refine_with_linear_form_inequality(right, left, store, true); + break; + case GREATER_OR_EQUAL: + refine_with_linear_form_inequality(right, left, store, false); + break; + case NOT_EQUAL: + break; + default: + throw std::runtime_error("PPL internal error"); + } +} + +template <typename FP_Format, typename Interval_Info> +inline void Polyhedron:: refine_fp_interval_abstract_store( Box< Interval<FP_Format, Interval_Info> >& store) const { diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh index 074e717..e12b6fd 100644 --- a/src/Polyhedron.templates.hh +++ b/src/Polyhedron.templates.hh @@ -300,7 +300,8 @@ void Polyhedron::refine_with_linear_form_inequality( const Linear_Form< Interval<FP_Format, Interval_Info> >& left, const Linear_Form< Interval<FP_Format, Interval_Info> >& right, - const Box< Interval<FP_Format, Interval_Info> >& store) { + const Box< Interval<FP_Format, Interval_Info> >& store, + bool is_strict) { // Check that FP_Format is indeed a floating point type. PPL_COMPILE_TIME_CHECK(!std::numeric_limits<FP_Format>::is_exact, @@ -340,7 +341,10 @@ Polyhedron::refine_with_linear_form_inequality( convert_to_integer_expression(lf_approx, lf_space_dim, lf_approx_le); // Finally, do the refinement. - refine_with_constraint(lf_approx_le <= 0); + if (!is_strict || is_necessarily_closed()) + refine_with_constraint(lf_approx_le <= 0); + else + refine_with_constraint(lf_approx_le < 0); } template <typename FP_Format, typename Interval_Info>

1 0

[GIT] ppl/ppl(floating_point): Added a trivial implementation of
by Fabio Bossi 25 Sep '09

25 Sep '09

Module: ppl/ppl Branch: floating_point Commit: 1ce1a9746e940039f68b71e9da8248b3d6145104 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=1ce1a9746e94… Author: Fabio Bossi <bossi(a)cs.unipr.it> Date: Fri Sep 25 11:40:55 2009 +0200 Added a trivial implementation of generalized_refine_with_linear_form_inequality. --- src/Octagonal_Shape.defs.hh | 34 ++++++++++++++++++++++++++++++++++ src/Octagonal_Shape.inlines.hh | 27 +++++++++++++++++++++++++++ 2 files changed, 61 insertions(+), 0 deletions(-) diff --git a/src/Octagonal_Shape.defs.hh b/src/Octagonal_Shape.defs.hh index 42166af..0accc69 100644 --- a/src/Octagonal_Shape.defs.hh +++ b/src/Octagonal_Shape.defs.hh @@ -1014,6 +1014,40 @@ public: const Linear_Form< Interval<T, Interval_Info> >& right); /*! \brief + Refines the system of octagonal constraints defining \p *this using + the constraint expressed by \p left \f$\relsym\f$ \p right, where + \f$\relsym\f$ is the relation symbol specified by \p relsym. + + \param left + The linear form on intervals with floating point boundaries that + is at the left of the comparison operator. All of its coefficients + MUST be bounded. + + \param right + The linear form on intervals with floating point boundaries that + is at the right of the comparison operator. All of its coefficients + MUST be bounded. + + \param relsym + The relation symbol. + + \exception std::invalid_argument + Thrown if \p left (or \p right) is dimension-incompatible with \p *this. + + \exception std::runtime_error + Thrown if \p relsym is not a valid relation symbol. + + This function is used in abstract interpretation to model a filter + that is generated by a comparison of two expressions that are correctly + approximated by \p left and \p right respectively. + */ + template <typename Interval_Info> + void generalized_refine_with_linear_form_inequality( + const Linear_Form< Interval<T, Interval_Info> >& left, + const Linear_Form< Interval<T, Interval_Info> >& right, + Relation_Symbol relsym); + + /*! \brief Computes the \ref Cylindrification "cylindrification" of \p *this with respect to space dimension \p var, assigning the result to \p *this. diff --git a/src/Octagonal_Shape.inlines.hh b/src/Octagonal_Shape.inlines.hh index cee791c..73e4124 100644 --- a/src/Octagonal_Shape.inlines.hh +++ b/src/Octagonal_Shape.inlines.hh @@ -615,6 +615,33 @@ Octagonal_Shape<T>::strictly_contains(const Octagonal_Shape& y) const { template <typename T> template <typename Interval_Info> inline void +Octagonal_Shape<T>::generalized_refine_with_linear_form_inequality( + const Linear_Form< Interval<T, Interval_Info> >& left, + const Linear_Form< Interval<T, Interval_Info> >& right, + Relation_Symbol relsym) { + switch (relsym) { + case EQUAL: + refine_with_linear_form_inequality(left, right); + refine_with_linear_form_inequality(right, left); + break; + case LESS_THAN: + case LESS_OR_EQUAL: + refine_with_linear_form_inequality(left, right); + break; + case GREATER_THAN: + case GREATER_OR_EQUAL: + refine_with_linear_form_inequality(right, left); + break; + case NOT_EQUAL: + break; + default: + throw std::runtime_error("PPL internal error"); + } +} + +template <typename T> +template <typename Interval_Info> +inline void Octagonal_Shape<T>:: refine_fp_interval_abstract_store( Box< Interval<T, Interval_Info> >& store) const {

1 0