Module: ppl/ppl Branch: floating_point Commit: 219f235033052dd7e24399eb9d1e494911ed0401 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=219f235033052... Author: Fabio Bossi <bossi@cs.unipr.it> Date: Mon Sep 13 14:08:29 2010 +0200 Do not fail automatically when linearizing approximable references having more than one associated dimension. --- src/Float.defs.hh | 16 ++++++--- src/linearize.hh | 44 +++++++++++++++++++++----- tests/Concrete_Expression/C_Expr.defs.hh | 12 +++--- tests/Concrete_Expression/C_Expr.inlines.hh | 5 ++- tests/Concrete_Expression/linearize.cc | 45 ++++++++++++++++++++++++-- 5 files changed, 96 insertions(+), 26 deletions(-) diff --git a/src/Float.defs.hh b/src/Float.defs.hh index 059d3e4..ad67317 100644 --- a/src/Float.defs.hh +++ b/src/Float.defs.hh @@ -433,14 +433,18 @@ public: FP_Interval_Type& result) const = 0; /*! \brief - Asks the external analyzer for the space dimension associated to - the approximable reference \p expr. + Asks the external analyzer for the possible space dimensions that + are associated to the approximable reference \p expr. + Result is stored into \p result. + + \return <CODE>true</CODE> if the analyzer was able to return + the (possibly empty!) set, <CODE>false</CODE> otherwise. - \return the associated space dimension if succesful, - <CODE>not_a_dimension()<CODE> otherwise. + The resulting set MUST NOT contain <CODE>not_a_dimension()</CODE>. */ - virtual dimension_type get_associated_dimension( - const Approximable_Reference<Target>& expr) const = 0; + virtual bool get_associated_dimensions( + const Approximable_Reference<Target>& expr, + std::set<dimension_type>& result) const = 0; }; diff --git a/src/linearize.hh b/src/linearize.hh index 0aaa464..8767f80 100644 --- a/src/linearize.hh +++ b/src/linearize.hh @@ -738,15 +738,22 @@ linearize(const Concrete_Expression<Target>& expr, { const Approximable_Reference<Target>* ref_expr = expr.template as<Approximable_Reference>(); - /* Variable references are the only that we are currently - able to analyze */ - dimension_type variable_index = oracle.get_associated_dimension(*ref_expr); - if (variable_index == not_a_dimension()) + std::set<dimension_type> associated_dimensions; + if (!oracle.get_associated_dimensions(*ref_expr, associated_dimensions) + || associated_dimensions.empty()) + /* + We were unable to find any associated space dimension: + linearization fails. + */ return false; - else { - /* If a linear form associated to the referenced variable - exists in lf_store, return that form. Otherwise, return - the simplest linear form. */ + + if (associated_dimensions.size() == 1) { + /* If a linear form associated to the only referenced + space dimension exists in lf_store, return that form. + Otherwise, return the simplest linear form. */ + dimension_type variable_index = *associated_dimensions.begin(); + PPL_ASSERT(variable_index != not_a_dimension()); + typename FP_Linear_Form_Abstract_Store::const_iterator variable_value = lf_store.find(variable_index); if (variable_value == lf_store.end()) { @@ -759,6 +766,27 @@ linearize(const Concrete_Expression<Target>& expr, that an unbounded linear form was saved into lf_store? */ return !result.overflows(); } + + /* + Here associated_dimensions.size() > 1. Try to return the LUB + of all intervals associated to each space dimension. + */ + std::set<dimension_type>::const_iterator i = associated_dimensions.begin(); + std::set<dimension_type>::const_iterator i_end = + associated_dimensions.end(); + FP_Interval_Type lub(EMPTY); + for (; i != i_end; ++i) { + FP_Interval_Type curr_int; + PPL_ASSERT(*i != not_a_dimension()); + if (!oracle.get_interval(*i, curr_int)) + return false; + + lub.join_assign(curr_int); + } + + result = FP_Linear_Form(lub); + return !result.overflows(); + break; } case Cast_Operator<Target>::KIND: diff --git a/tests/Concrete_Expression/C_Expr.defs.hh b/tests/Concrete_Expression/C_Expr.defs.hh index 40de1c0..32104eb 100644 --- a/tests/Concrete_Expression/C_Expr.defs.hh +++ b/tests/Concrete_Expression/C_Expr.defs.hh @@ -227,10 +227,10 @@ class Approximable_Reference<C_Expr> : public Concrete_Expression<C_Expr>, public Approximable_Reference_Common<C_Expr> { public: - //! Builds a reference to the variable having the given index. + //! Builds a reference to the entity having the given index. Approximable_Reference<C_Expr>(Concrete_Expression_Type type, - const Integer_Interval_Type& val, - dimension_type var_index); + const Integer_Interval_Type& val, + dimension_type index); //! Do-nothing destructor. ~Approximable_Reference<C_Expr>(); @@ -241,11 +241,11 @@ public: //! Constant identifying approximable reference nodes. enum { KIND = APPROX_REF }; - //! An interval in which the variable's value falls. + //! An interval in which the referenced entity's value falls. Integer_Interval_Type value; - //! The index of the referenced variable. - dimension_type var_dimension; + //! The set of possible indexes for the referenced entity. + std::set<dimension_type> dimensions; }; } // namespace Parma_Polyhedra_Library diff --git a/tests/Concrete_Expression/C_Expr.inlines.hh b/tests/Concrete_Expression/C_Expr.inlines.hh index accb5d0..d12ccd5 100644 --- a/tests/Concrete_Expression/C_Expr.inlines.hh +++ b/tests/Concrete_Expression/C_Expr.inlines.hh @@ -165,10 +165,11 @@ inline Approximable_Reference<C_Expr>:: Approximable_Reference(Concrete_Expression_Type type, const Integer_Interval_Type& val, - dimension_type var_index) + dimension_type index) : Concrete_Expression<C_Expr>(type, APPROX_REF), value(val), - var_dimension(var_index) { + dimensions() { + dimensions.insert(index); } inline diff --git a/tests/Concrete_Expression/linearize.cc b/tests/Concrete_Expression/linearize.cc index 1cf9ae9..26dcf0e 100644 --- a/tests/Concrete_Expression/linearize.cc +++ b/tests/Concrete_Expression/linearize.cc @@ -58,9 +58,11 @@ public: return true; } - dimension_type get_associated_dimension( - const Approximable_Reference<C_Expr>& expr) const { - return expr.var_dimension; + bool get_associated_dimensions( + const Approximable_Reference<C_Expr>& expr, + std::set<dimension_type>& result) const { + result = expr.dimensions; + return true; } FP_Interval_Abstract_Store int_store; @@ -99,10 +101,13 @@ test02() { Binary_Operator<C_Expr> dif(FP_Type, Binary_Operator<C_Expr>::SUB, &var1, &con); Binary_Operator<C_Expr> mul(FP_Type, Binary_Operator<C_Expr>::MUL, &dif, &var0); FP_Linear_Form result; - linearize(mul, oracle, FP_Linear_Form_Abstract_Store(), result); + if (!linearize(mul, oracle, FP_Linear_Form_Abstract_Store(), result)) + return false; FP_Linear_Form known_result(compute_absolute_error<FP_Interval>(ANALYZED_FP_FORMAT)); + nout << "*** result ***" << endl + << result << endl; nout << "*** known_result ***" << endl << known_result << endl; bool ok = (result == known_result); @@ -274,6 +279,37 @@ test08() { return ok1 && ok2; } +/* + Tests linearization of an approximable reference having more than + one associated index. +*/ +bool +test09() { + Test_Oracle oracle(FP_Interval_Abstract_Store(4)); + oracle.int_store.set_interval(Variable(0), FP_Interval(0)); + oracle.int_store.set_interval(Variable(1), FP_Interval(10)); + oracle.int_store.set_interval(Variable(2), FP_Interval(20)); + oracle.int_store.set_interval(Variable(3), FP_Interval(5)); + Approximable_Reference<C_Expr> ref(FP_Type, Int_Interval(mpz_class(0)), 0); + ref.dimensions.insert(1); + ref.dimensions.insert(3); + FP_Linear_Form result; + if (!linearize(ref, oracle, FP_Linear_Form_Abstract_Store(), result)) + return false; + + FP_Interval known_int(FP_Interval(0)); + known_int.join_assign(FP_Interval(10)); + FP_Linear_Form known_result(known_int); + + nout << "*** result ***" << endl + << result << endl; + nout << "*** known_result ***" << endl + << known_result << endl; + bool ok = (result == known_result); + + return ok; +} + } // namespace BEGIN_MAIN @@ -285,4 +321,5 @@ BEGIN_MAIN DO_TEST(test06); DO_TEST(test07); DO_TEST(test08); + DO_TEST(test09); END_MAIN