Module: ppl/ppl Branch: bounded_arithmetic Commit: 962819f083329ddc94a037cf6b8379704df4c916 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=962819f083329...

Author: Alberto Gioia alberto.gioi1@studenti.unipr.it Date: Wed May 4 13:01:45 2011 +0200

Added functions operator^= and operator^ into Linear_Form.templates.hh, and into Interval.defs.hh and Interval.inlines.hh added functions operator^= and xor_assign. This functions are necessary for the linearization of the bitwise operator XOR.

---

src/Interval.defs.hh | 12 +++ src/Interval.inlines.hh | 95 ++++++++++++++++++++++++ src/Linear_Form.templates.hh | 47 ++++++++++++ tests/Concrete_Expression/linearize_integer.hh | 39 ++++++++-- 4 files changed, 187 insertions(+), 6 deletions(-)

diff --git a/src/Interval.defs.hh b/src/Interval.defs.hh index 2314b42..02dee90 100644 --- a/src/Interval.defs.hh +++ b/src/Interval.defs.hh @@ -174,6 +174,13 @@ public: return *this; }

+ template <typename T> + typename Enable_If<Is_Singleton<T>::value || Is_Interval<T>::value, Interval&>::type + operator^=(const T& x) { + xor_assign(*this, x); + return *this; + } +

template <typename T> typename Enable_If<Is_Singleton<T>::value || Is_Interval<T>::value, Interval&>::type @@ -843,6 +850,11 @@ public:

template <typename From1, typename From2> typename Enable_If<((Is_Singleton<From1>::value || Is_Interval<From1>::value) + && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), I_Result>::type + xor_assign(const From1& x, const From2& y); + + template <typename From1, typename From2> + typename Enable_If<((Is_Singleton<From1>::value || Is_Interval<From1>::value) && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), I_Result>::type sub_assign(const From1& x, const From2& y);

diff --git a/src/Interval.inlines.hh b/src/Interval.inlines.hh index d07daa3..ca4256e 100644 --- a/src/Interval.inlines.hh +++ b/src/Interval.inlines.hh @@ -882,6 +882,101 @@ template <typename To_Boundary, typename To_Info> template <typename From1, typename From2> inline typename Enable_If<((Is_Singleton<From1>::value || Is_Interval<From1>::value) + && (Is_Singleton<From2>::value + || Is_Interval<From2>::value)), I_Result>::type +Interval<To_Boundary, To_Info>::xor_assign(const From1& x, const From2& y) { + PPL_ASSERT(f_OK(x)); + PPL_ASSERT(f_OK(y)); + + PPL_DIRTY_TEMP(To_Info, to_info); + to_info.clear(); + Result rl,ru; + int xls = sgn_b(LOWER, f_lower(x), f_info(x)); + int yls = sgn_b(LOWER, f_lower(y), f_info(y)); + /* + Same sign. + 1<= XOR(x,y) <= |x+y| + */ + if ( ((xls>=0) && (yls >=0) ) || ((xls<0) && (yls<0)) ){ + if (f_upper(x)+f_upper(y) > INT_MAX || + f_upper(x)+f_upper(y) < -INT_MAX) + return assign(EMPTY); + + rl = Boundary_NS::assign(LOWER, lower(),to_info, + LOWER, f_lower(Constant<1>::value),f_info(Constant<1>::value)); + + PPL_DIRTY_TEMP(To_Info, tmp_info); + tmp_info.clear(); + + ru = Boundary_NS::add_assign(UPPER, upper(), to_info, + UPPER, f_upper(x), f_info(x), + UPPER, f_upper(y), f_info(y)); + if(upper()<0) + ru = Boundary_NS::neg_assign(UPPER, upper(), to_info, + UPPER, upper(), to_info); + } + /* + Signs of discord + -(|x|+|y|) <= XOR(x,y) <= 0 + */ + else { + if (f_lower(x) < -INT_MAX || f_lower(y) < -INT_MAX) + return assign(EMPTY); + if (xls < 0) { + if(-f_lower(x) + f_lower(y) > INT_MAX) + return assign(EMPTY); + } + if (yls < 0) { + if(f_lower(x) - f_lower(y) > INT_MAX) + return assign(EMPTY); + } + + PPL_DIRTY_TEMP(To_Boundary, tmp_lowerx); + PPL_DIRTY_TEMP(To_Boundary, tmp_lowery); + PPL_DIRTY_TEMP(To_Boundary, tmp_lower); + + + PPL_DIRTY_TEMP(To_Info, tmp_infox); + PPL_DIRTY_TEMP(To_Info, tmp_infoy); + PPL_DIRTY_TEMP(To_Info, tmp_info); + + tmp_infox.clear(); + tmp_infoy.clear(); + tmp_info.clear(); + + Boundary_NS::assign(LOWER, tmp_lowerx, tmp_infox, + LOWER, f_lower(x), f_info(x)); + + if (xls < 0) + Boundary_NS::neg_assign(LOWER, tmp_lowerx, tmp_infox, + LOWER, tmp_lowerx, tmp_infox); + + Boundary_NS::assign(LOWER, tmp_lowery, tmp_infoy, + LOWER, f_lower(y), f_info(y)); + + if (yls < 0) + Boundary_NS::neg_assign(LOWER, tmp_lowery, tmp_infoy, + LOWER, tmp_lowery, tmp_infoy); + + Boundary_NS::add_assign(LOWER, tmp_lower, tmp_info, + LOWER, tmp_lowerx, tmp_infox, + LOWER, tmp_lowery, tmp_infoy); + rl = Boundary_NS::neg_assign(LOWER, lower(), to_info, + LOWER, tmp_lower, tmp_info); + + ru = Boundary_NS::assign(UPPER, upper(), to_info, + UPPER, f_upper(Constant<0>::value), f_info(Constant<0>::value)); + + } + assign_or_swap(info(), to_info); + PPL_ASSERT(OK()); + return combine(rl, ru); +} + +template <typename To_Boundary, typename To_Info> +template <typename From1, typename From2> +inline typename Enable_If<((Is_Singleton<From1>::value + || Is_Interval<From1>::value) && (Is_Singleton<From2>::value || Is_Interval<From2>::value)), I_Result>::type Interval<To_Boundary, To_Info>::sub_assign(const From1& x, const From2& y) { diff --git a/src/Linear_Form.templates.hh b/src/Linear_Form.templates.hh index 5706422..1233097 100644 --- a/src/Linear_Form.templates.hh +++ b/src/Linear_Form.templates.hh @@ -316,6 +316,40 @@ operator&(const Linear_Form<C>& f1, const Linear_Form<C>& f2) {

/*! \relates Parma_Polyhedra_Library::Linear_Form */ template <typename C> +Linear_Form<C> +operator^(const Linear_Form<C>& f1, const Linear_Form<C>& f2) { + dimension_type f1_size = f1.size(); + dimension_type f2_size = f2.size(); + dimension_type min_size; + dimension_type max_size; + const Linear_Form<C>* p_e_max; + if (f1_size > f2_size) { + min_size = f2_size; + max_size = f1_size; + p_e_max = &f1; + } + else { + min_size = f1_size; + max_size = f2_size; + p_e_max = &f2; + } + + Linear_Form<C> r(max_size, false); + dimension_type i = max_size; + while (i > min_size) { + --i; + r[i] = p_e_max->vec[i]; + } + while (i > 0) { + --i; + r[i] = f1[i]; + r[i] ^= f2[i]; + } + return r; +} + +/*! \relates Parma_Polyhedra_Library::Linear_Form */ +template <typename C> Linear_Form<C>& operator+=(Linear_Form<C>& f1, const Linear_Form<C>& f2) { dimension_type f1_size = f1.size(); @@ -418,6 +452,19 @@ operator&=(Linear_Form<C>& f1, const Linear_Form<C>& f2) { return f1; }

+/*! \relates Parma_Polyhedra_Library::Linear_Form */ +template <typename C> +Linear_Form<C>& +operator^=(Linear_Form<C>& f1, const Linear_Form<C>& f2) { + dimension_type f1_size = f1.size(); + dimension_type f2_size = f2.size(); + if (f1_size < f2_size) + f1.extend(f2_size); + for (dimension_type i = f2_size; i-- > 0; ) + f1[i] ^= f2[i]; + return f1; +} + /*! \relates Linear_Row */ template <typename C> inline bool diff --git a/tests/Concrete_Expression/linearize_integer.hh b/tests/Concrete_Expression/linearize_integer.hh index 306ed81..8bb755f 100644 --- a/tests/Concrete_Expression/linearize_integer.hh +++ b/tests/Concrete_Expression/linearize_integer.hh @@ -4,6 +4,31 @@ #include "Linear_Form.defs.hh" namespace Parma_Polyhedra_Library {

+template <typename Target, typename Integer_Interval> +static bool +or_linearize_int(const Binary_Operator<Target>& bop_expr, + + const Oracle<Target,Integer_Interval>& oracle, + const std::map<dimension_type, Linear_Form<Integer_Interval> >& lf_store, + Linear_Form<Integer_Interval>& result) { + PPL_ASSERT(bop_expr.binary_operator() == Binary_Operator<Target>::ADD); + + typedef Linear_Form<Integer_Interval> Integer_Linear_Form; + typedef Box<Integer_Interval> Integer_Interval_Abstract_Store; + typedef std::map<dimension_type, Integer_Linear_Form> Integer_Linear_Form_Abstract_Store; + + if (!linearize_int(*(bop_expr.left_hand_side()), oracle, lf_store, result)) + return false; + + Integer_Linear_Form linearized_second_operand; + + if (!linearize_int(*(bop_expr.right_hand_side()), oracle, lf_store, + linearized_second_operand)) + return false; + + result |= linearized_second_operand; + return true; +}

template <typename Target, typename Integer_Interval> static bool @@ -33,7 +58,7 @@ and_linearize_int(const Binary_Operator<Target>& bop_expr,

template <typename Target, typename Integer_Interval> static bool -or_linearize_int(const Binary_Operator<Target>& bop_expr, +xor_linearize_int(const Binary_Operator<Target>& bop_expr,

const Oracle<Target,Integer_Interval>& oracle, const std::map<dimension_type, Linear_Form<Integer_Interval> >& lf_store, @@ -43,17 +68,17 @@ or_linearize_int(const Binary_Operator<Target>& bop_expr, typedef Linear_Form<Integer_Interval> Integer_Linear_Form; typedef Box<Integer_Interval> Integer_Interval_Abstract_Store; typedef std::map<dimension_type, Integer_Linear_Form> Integer_Linear_Form_Abstract_Store; - + if (!linearize_int(*(bop_expr.left_hand_side()), oracle, lf_store, result)) return false;

Integer_Linear_Form linearized_second_operand; - + if (!linearize_int(*(bop_expr.right_hand_side()), oracle, lf_store, linearized_second_operand)) return false;

- result |= linearized_second_operand; + result ^= linearized_second_operand; return true; }

@@ -91,8 +116,10 @@ linearize_int(const Concrete_Expression<Target>& expr, case Binary_Operator<Target>::BAND: return and_linearize_int(*bop_expr, oracle, lf_store, result); break; - - } + case Binary_Operator<Target>::BXOR: + return xor_linearize_int(*bop_expr, oracle, lf_store, result); + break; + } } } }