[PPL-devel] [GIT] ppl/ppl(bounded_arithmetic): Corrected documentation.
Alberto Gioia
alberto.gioia1 at studenti.unipr.it
Thu Jul 14 18:22:48 CEST 2011
Module: ppl/ppl
Branch: bounded_arithmetic
Commit: 126e67ad12f38972e01d0dbe529e970a70c059a6
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=126e67ad12f38972e01d0dbe529e970a70c059a6
Author: Alberto Gioia <alberto.gioia1 at studenti.unipr.it>
Date: Thu Jul 14 18:21:36 2011 +0200
Corrected documentation.
---
doc/definitions.dox | 34 +++++++++++++++++-----------------
src/linearize_integer.hh | 40 ++++++++++++++++++++--------------------
2 files changed, 37 insertions(+), 37 deletions(-)
diff --git a/doc/definitions.dox b/doc/definitions.dox
index 250f50e..f6381b7 100644
--- a/doc/definitions.dox
+++ b/doc/definitions.dox
@@ -2823,11 +2823,11 @@ The interval bitwise operators are defined as follow:
\mbox{if }a \geq 0\mbox{ and } a' \geq 0
\\
\left[0, \max\left(b, b'\right)\right] &
- \mbox{if }a \geq 0\mbox{ and } b' \le 0
- \mbox{, or }b \le 0\mbox{ and } a' \geq 0
+ \mbox{if }a \geq 0\mbox{ and } b' < 0
+ \mbox{, or }b < 0\mbox{ and } a' \geq 0
\\
\left[a + a' , \min\left(b,b'\right)\right] &
- \mbox{if }b \le 0\mbox{ and } b' \le 0 \\
+ \mbox{if }b < 0\mbox{ and } b' < 0 \\
\end{cases}
\f]
@@ -2838,11 +2838,11 @@ The interval bitwise operators are defined as follow:
\mbox{if }a \geq 0\mbox{ and } a' \geq 0
\\
\left[\min\left(a,a'\right),-1\right] &
- \mbox{if }a \geq 0\mbox{ and } b' \le 0
- \mbox{, or }b \le 0\mbox{ and } a' \geq 0
+ \mbox{if }a \geq 0\mbox{ and } b' < 0
+ \mbox{, or }b < 0\mbox{ and } a' \geq 0
\\
\left[\max\left(a,a'\right),-1\right] &
- \mbox{if }b \le 0\mbox{ and } b' \le 0 \\
+ \mbox{if }b < 0\mbox{ and } b' < 0 \\
\end{cases}
\f]
@@ -2851,11 +2851,11 @@ The interval bitwise operators are defined as follow:
\begin{cases}
\left[0,\left|b + b' \right|\right] &
\mbox{if }a \geq 0\mbox{ and } a' \geq 0
- \mbox{, or }b \le 0\mbox{ and }b' \le 0
+ \mbox{, or }b < 0\mbox{ and }b' < 0
\\
\left[-\left(\left|a\right| + \left|b\right|\right),-1\right] &
- \mbox{if }a \geq 0\mbox{ and }b' \le 0
- \mbox{, or }b \le 0\mbox{ and } a' \geq 0 \\
+ \mbox{if }a \geq 0\mbox{ and }b' < 0
+ \mbox{, or }b < 0\mbox{ and } a' \geq 0 \\
\end{cases}
\f]
@@ -2866,13 +2866,13 @@ The interval bitwise operators are defined as follow:
\mbox{if }a \geq 0\mbox{ and } a' \geq 0
\\
\left[0, \left(b / 2^{\left|b'\right|}\right)\right] &
- \mbox{if }a \geq 0\mbox{ and } b' \le 0
+ \mbox{if }a \geq 0\mbox{ and } b' < 0
\\
\left[\left(a \times 2^{a'}\right), 0\right] &
- \mbox{if }b \le 0\mbox{ and } a' \geq 0
+ \mbox{if }b < 0\mbox{ and } a' \geq 0
\\
\left[\left(a / 2^{\left|a'\right|}\right), 0\right] &
- \mbox{if }b \le 0\mbox{ and } b' \le 0 \\
+ \mbox{if }b < 0\mbox{ and } b' < 0 \\
\end{cases}
\f]
@@ -2883,13 +2883,13 @@ The interval bitwise operators are defined as follow:
\mbox{if }a \geq 0\mbox{ and } a' \geq 0
\\
\left[0, \left(b \times 2^{\left|b'\right|}\right)\right] &
- \mbox{if }a \geq 0\mbox{ and } b' \le 0
+ \mbox{if }a \geq 0\mbox{ and } b' < 0
\\
\left[\left(a / 2^{a'}\right), 0\right] &
- \mbox{if }b \le 0\mbox{ and } a' \geq 0
+ \mbox{if }b < 0\mbox{ and } a' \geq 0
\\
\left[\left(a \times 2^{\left|a'\right|}\right), 0\right] &
- \mbox{if }b \le 0\mbox{ and } b' \le 0 \\
+ \mbox{if }b < 0\mbox{ and } b' < 0 \\
\end{cases}
\f]
@@ -3200,8 +3200,8 @@ composed by two parts:
associating each variable with its current approximating linear form.
An interval abstract store is represented by a
-\link Parma_Polyhedra_Library::Box \c Box \endlink with integer boundaries,
-while a linear form abstract store is a map of the Standard Template Library.
+\link Parma_Polyhedra_Library::Box \c Box \endlink with integer boundaries,
+while a linear form abstract store is a map of the Standard Template Library.
The <CODE>linearize</CODE> method requires both stores as its arguments.
\section use_of_library Using the Library
diff --git a/src/linearize_integer.hh b/src/linearize_integer.hh
index 55ee129..9b45508 100644
--- a/src/linearize_integer.hh
+++ b/src/linearize_integer.hh
@@ -1386,7 +1386,7 @@ xor_linearize_int
\leq
\left(i + \sum_{v \in \cV}i_{v}v \right)
\adivlf
- 2^{\left(i' + \sum_{v \in \cV}i'_{v}v \right)}
+ 2^{\left(\left|i'\right| + \sum_{v \in \cV}\left|i'_{v}\right|v \right)}
\f]
and we can define the elments of the linear form
@@ -1397,7 +1397,7 @@ xor_linearize_int
\leq
k
\leq
- \left(i \adivifp 2^{i'} \right)
+ \left(i \adivifp 2^\left|{i'}\right| \right)
\f]
\f[
@@ -1405,7 +1405,7 @@ xor_linearize_int
\leq
k_{v}
\leq
- \left(i_{v} \adivifp 2^{i'_{v}} \right)
+ \left(i_{v} \adivifp 2^\left|{i'_{v}}\right| \right)
\f]
then
@@ -1415,7 +1415,7 @@ xor_linearize_int
\approx
0
\bowtie
- \left(i \adivifp 2^{i'} \right)
+ \left(i \adivifp 2^\left|{i'}\right| \right)
\f]
\f[
@@ -1423,7 +1423,7 @@ xor_linearize_int
\approx
0
\bowtie
- \left(i_{v} \adivifp 2^{i'_{v}} \right)
+ \left(i_{v} \adivifp 2^\left|{i'_{v}}\right| \right)
\f]
If instead, let \f$x\f$ and \f$y\f$ be two integer constants with \f$x\f$
@@ -1529,7 +1529,7 @@ xor_linearize_int
\f[
\left(i + \sum_{v \in \cV}i_{v}v \right)
\adivlf
- 2^{\left(i' + \sum_{v \in \cV}i'_{v}v \right)}
+ 2^{\left(\left|i'\right| + \sum_{v \in \cV}\left|i'_{v}\right|v \right)}
\leq
\left(k + \sum_{v \in \cV}k_{v}v \right)
\leq
@@ -1540,7 +1540,7 @@ xor_linearize_int
\f$k + \sum_{v \in \cV}k_{v}v\f$, as follows, \f$\forall v \in \cV\f$:
\f[
- \left(i \adivifp 2^{i'} \right)
+ \left(i \adivifp 2^\left|{i'}\right| \right)
\leq
k
\leq
@@ -1548,7 +1548,7 @@ xor_linearize_int
\f]
\f[
- \left(i_{v} \adivifp 2^{i'_{v}} \right)
+ \left(i_{v} \adivifp 2^\left|{i'_{v}}\right| \right)
\leq
k_{v}
\leq
@@ -1560,7 +1560,7 @@ xor_linearize_int
\f[
k
\approx
- \left(i \adivifp 2^{i'} \right)
+ \left(i \adivifp 2^\left|{i'}\right| \right)
\bowtie
0
\f]
@@ -1568,7 +1568,7 @@ xor_linearize_int
\f[
k_{v}
\approx
- \left(i_{v} \adivifp 2^{i'_{v}} \right)
+ \left(i_{v} \adivifp 2^\left|{i'_{v}}\right| \right)
\bowtie
0
\f]
@@ -1744,7 +1744,7 @@ lshift_linearize_int
\leq
\left(i + \sum_{v \in \cV}i_{v}v \right)
\amlf
- 2^{\left(i' + \sum_{v \in \cV}i'_{v}v \right)}
+ 2^{\left(\left|i'\right| + \sum_{v \in \cV}\left|i'_{v}\right|v \right)}
\f]
and we can define the elments of the linear form
@@ -1755,7 +1755,7 @@ lshift_linearize_int
\leq
k
\leq
- \left(i \amifp 2^{i'} \right)
+ \left(i \amifp 2^\left|{i'}\right| \right)
\f]
\f[
@@ -1763,7 +1763,7 @@ lshift_linearize_int
\leq
k_{v}
\leq
- \left(i_{v} \amifp 2^{i'_{v}} \right)
+ \left(i_{v} \amifp 2^\left|{i'_{v}}\right| \right)
\f]
then
@@ -1773,7 +1773,7 @@ lshift_linearize_int
\approx
0
\bowtie
- \left(i \amifp 2^{i'} \right)
+ \left(i \amifp 2^\left|{i'}\right| \right)
\f]
\f[
@@ -1781,7 +1781,7 @@ lshift_linearize_int
\approx
0
\bowtie
- \left(i_{v} \amifp 2^{i'_{v}} \right)
+ \left(i_{v} \amifp 2^\left|{i'_{v}}\right| \right)
\f]
If instead, let \f$x\f$ and \f$y\f$ be two integer constants with \f$x\f$
@@ -1887,7 +1887,7 @@ lshift_linearize_int
\f[
\left(i + \sum_{v \in \cV}i_{v}v \right)
\amlf
- 2^{\left(i' + \sum_{v \in \cV}i'_{v}v \right)}
+ 2^{\left(\left|i'\right| + \sum_{v \in \cV}\left|i'_{v}\right|v \right)}
\leq
\left(k + \sum_{v \in \cV}k_{v}v \right)
\leq
@@ -1898,7 +1898,7 @@ lshift_linearize_int
\f$k + \sum_{v \in \cV}k_{v}v\f$, as follows, \f$\forall v \in \cV\f$:
\f[
- \left(i \amifp 2^{i'} \right)
+ \left(i \amifp 2^\left|{i'}\right| \right)
\leq
k
\leq
@@ -1906,7 +1906,7 @@ lshift_linearize_int
\f]
\f[
- \left(i_{v} \amifp 2^{i'_{v}} \right)
+ \left(i_{v} \amifp 2^\left|{i'_{v}}\right| \right)
\leq
k_{v}
\leq
@@ -1918,7 +1918,7 @@ lshift_linearize_int
\f[
k
\approx
- \left(i \amifp 2^{i'} \right)
+ \left(i \amifp 2^\left|{i'}\right| \right)
\bowtie
0
\f]
@@ -1926,7 +1926,7 @@ lshift_linearize_int
\f[
k_{v}
\approx
- \left(i_{v} \amifp 2^{i'_{v}} \right)
+ \left(i_{v} \amifp 2^\left|{i'_{v}}\right| \right)
\bowtie
0
\f]
More information about the PPL-devel
mailing list