[PPL-devel] [GIT] ppl/ppl(floating_point): Finished writing a first version of our affine_image variant.
Fabio Bossi
bossi at cs.unipr.it
Mon Sep 21 11:34:46 CEST 2009
Module: ppl/ppl
Branch: floating_point
Commit: 04edf0b5d66a1dfe43f19050098b4d30969d1b46
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=04edf0b5d66a1dfe43f19050098b4d30969d1b46
Author: Fabio Bossi <bossi at cs.unipr.it>
Date: Mon Sep 21 10:11:18 2009 +0200
Finished writing a first version of our affine_image variant.
---
src/Polyhedron.templates.hh | 18 ++++++++++++++----
1 files changed, 14 insertions(+), 4 deletions(-)
diff --git a/src/Polyhedron.templates.hh b/src/Polyhedron.templates.hh
index ab61ee1..8ac2f9d 100644
--- a/src/Polyhedron.templates.hh
+++ b/src/Polyhedron.templates.hh
@@ -318,18 +318,28 @@ const std::map< dimension_type, Interval<FP_Format, Interval_Info> >& store) {
if (space_dim < var_id + 1)
throw_dimension_incompatible("affine_image(v, l, s)", var.id()+1);
+ // We suppose that the analyzer will not filter an unreachable test.
PPL_ASSERT(!marked_empty());
- minimize();
- unconstrain(var);
-
typedef Interval<FP_Format, Interval_Info> FP_Interval_Type;
typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;
+ // Overapproximate lf.
FP_Linear_Form lf_approx;
overapproximate_linear_form(lf, lf_space_dim, store, lf_approx);
-
+ // Normalize lf.
+ Linear_Expression lf_approx_le;
+ PPL_DIRTY_TEMP_COEFFICIENT(lo_coeff);
+ PPL_DIRTY_TEMP_COEFFICIENT(hi_coeff);
+ convert_to_integer_expressions(lf_approx, lf_space_dim, lo_coeff, hi_coeff);
+
+ // Finally, do the assignment.
+ PPL_DIRTY_TEMP_COEFFICIENT(one_coeff);
+ one_coeff = 1;
+ generalized_affine_image(var, GREATER_OR_EQUAL, lf_approx + lo_coeff,
+ one_coeff);
+ generalized_affine_image(var, LESS_OR_EQUAL, lf_approx + hi_coeff, one_coeff);
}
More information about the PPL-devel
mailing list