[PPL-devel] [GIT] ppl/ppl(bounded_arithmetic): Added functions operator^= and operator^ into Linear_Form.templates.hh,
Alberto Gioia
alberto.gioi1 at studenti.unipr.it
Wed May 4 13:03:15 CEST 2011
Module: ppl/ppl
Branch: bounded_arithmetic
Commit: 962819f083329ddc94a037cf6b8379704df4c916
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=962819f083329ddc94a037cf6b8379704df4c916
Author: Alberto Gioia <alberto.gioi1 at 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;
+ }
}
}
}
More information about the PPL-devel
mailing list