[PPL-devel] [GIT] ppl/ppl(bounded_arithmetic): Corrected documentation.
Alberto Gioia
alberto.gioia1 at studenti.unipr.it
Thu Jul 7 17:42:38 CEST 2011
Module: ppl/ppl
Branch: bounded_arithmetic
Commit: d3a4393da2940e2ab9fe2af718aecb7de6dda2f7
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=d3a4393da2940e2ab9fe2af718aecb7de6dda2f7
Author: Alberto Gioia <alberto.gioia1 at studenti.unipr.it>
Date: Thu Jul 7 17:41:12 2011 +0200
Corrected documentation.
---
doc/definitions.dox | 28 +++++++++++++-------------
src/linearize_integer.hh | 48 +++++++++++++++++++++++-----------------------
2 files changed, 38 insertions(+), 38 deletions(-)
diff --git a/doc/definitions.dox b/doc/definitions.dox
index 9b997ed..8735398 100644
--- a/doc/definitions.dox
+++ b/doc/definitions.dox
@@ -2858,9 +2858,9 @@ The interval bitwise operators are defined as follow:
\left[a,b\right] \olessthan ^{\#} \left[a',b'\right] \approx
\begin{cases}
\left[0, \left(b \amifp 2^{b'}\right)\right] & \mbox{if }a \geq 0\mbox{ and } a' \geq 0 \\
- \left[0, \left(b \adivifp 2^{b'}\right)\right] & \mbox{if }a \geq 0\mbox{ and } b' \le 0 \\
- \left[\left(a \amifp 2^{a'}\right), -1\right] & \mbox{if }b \le 0\mbox{ and } a' \geq 0 \\
- \left[\left(a \adivifp 2^{a'}\right), -1\right] & \mbox{if }b \le 0\mbox{ and } b' \le 0 \\
+ \left[0, \left(b \adivifp 2^{\left|b'\right|}\right)\right] & \mbox{if }a \geq 0\mbox{ and } b' \le 0 \\
+ \left[\left(a \amifp 2^{a'}\right), 0\right] & \mbox{if }b \le 0\mbox{ and } a' \geq 0 \\
+ \left[\left(a \adivifp 2^{\left|a'\right|}\right), 0\right] & \mbox{if }b \le 0\mbox{ and } b' \le 0 \\
\end{cases}
@@ -2872,9 +2872,9 @@ The interval bitwise operators are defined as follow:
\left[a,b\right] \ogreaterthan ^{\#} \left[a',b'\right] \approx
\begin{cases}
\left[0, \left(b \adivifp 2^{b'}\right)\right] & \mbox{if }a \geq 0\mbox{ and } a' \geq 0 \\
- \left[0, \left(b \amifp 2^{b'}\right)\right] & \mbox{if }a \geq 0\mbox{ and } b' \le 0 \\
- \left[\left(a \adivifp 2^{a'}\right), -1\right] & \mbox{if }b \le 0\mbox{ and } a' \geq 0 \\
- \left[\left(a \amifp 2^{a'}\right), -1\right] & \mbox{if }b \le 0\mbox{ and } b' \le 0 \\
+ \left[0, \left(b \amifp 2^{\left|b'\right|}\right)\right] & \mbox{if }a \geq 0\mbox{ and } b' \le 0 \\
+ \left[\left(a \adivifp 2^{a'}\right), 0\right] & \mbox{if }b \le 0\mbox{ and } a' \geq 0 \\
+ \left[\left(a \amifp 2^{\left|a'\right|}\right), 0\right] & \mbox{if }b \le 0\mbox{ and } b' \le 0 \\
\end{cases}
@@ -3101,7 +3101,7 @@ have discordand signs, with the first greater than or equal zero, then
\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]
@@ -3117,7 +3117,7 @@ have discordand signs, with the first less than zero, then
\leq
\left(k + \sum_{v \in \cV}k_{v}v \right)
\leq
- -1
+ 0
\f]
@@ -3128,11 +3128,11 @@ both less than zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by:
\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
- -1
+ 0
\f]
@@ -3176,7 +3176,7 @@ have discordand signs, with the first greater than or equal zero, then
\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]
@@ -3192,7 +3192,7 @@ have discordand signs, with the first less than zero, then
\leq
\left(k + \sum_{v \in \cV}k_{v}v \right)
\leq
- -1
+ 0
\f]
Finally, if \f$i + \sum_{v \in V}i_{v}v\f$ and \f$i' + \sum_{v \in V}i'_{v}v\f$ are
@@ -3202,11 +3202,11 @@ both less than zero, then \f$k + \sum_{v \in V}k_{v}v\f$ is approximated by:
\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
- -1
+ 0
\f]
diff --git a/src/linearize_integer.hh b/src/linearize_integer.hh
index 1b6a9de..1a0f625 100644
--- a/src/linearize_integer.hh
+++ b/src/linearize_integer.hh
@@ -1413,7 +1413,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr,
\leq
x \ll y
\leq
- -1
+ 0
\f]
Then let \f$i + \sum_{v \in \cV}i_{v}v \f$ and
@@ -1438,7 +1438,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr,
\leq
\left(k + \sum_{v \in \cV}k_{v}v \right)
\leq
- -1
+ 0
\f]
and we can define the elments of the linear form
@@ -1449,7 +1449,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr,
\leq
k
\leq
- -1
+ 0
\f]
\f[
@@ -1457,7 +1457,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr,
\leq
k_{v}
\leq
- -1
+ 0
\f]
then
@@ -1467,7 +1467,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr,
\approx
\left(i \amifp 2^{i'} \right)
\bowtie
- -1
+ 0
\f]
\f[
@@ -1475,7 +1475,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr,
\approx
\left(i_{v} \amifp 2^{i'_{v}} \right)
\bowtie
- -1
+ 0
\f]
Finally, let \f$x\f$ and \f$y\f$ be two integer constants both less then zero,
@@ -1486,7 +1486,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr,
\leq
x \ll y
\leq
- -1
+ 0
\f]
Then let \f$i + \sum_{v \in \cV}i_{v}v \f$ and
@@ -1511,7 +1511,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr,
\leq
\left(k + \sum_{v \in \cV}k_{v}v \right)
\leq
- -1
+ 0
\f]
and we can define the elments of the linear form
@@ -1522,7 +1522,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr,
\leq
k
\leq
- -1
+ 0
\f]
\f[
@@ -1530,7 +1530,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr,
\leq
k_{v}
\leq
- -1
+ 0
\f]
then
@@ -1540,7 +1540,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr,
\approx
\left(i \adivifp 2^{i'} \right)
\bowtie
- -1
+ 0
\f]
\f[
@@ -1548,7 +1548,7 @@ xor_linearize_int(const Binary_Operator<Target>& bop_expr,
\approx
\left(i_{v} \adivifp 2^{i'_{v}} \right)
\bowtie
- -1
+ 0
\f]
Given an expression \f$e_{1} \leftslice e_{2}\f$ and a composite
@@ -1769,7 +1769,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr,
\leq
x \gg y
\leq
- -1
+ 0
\f]
Then let \f$i + \sum_{v \in \cV}i_{v}v \f$ and
@@ -1794,7 +1794,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr,
\leq
\left(k + \sum_{v \in \cV}k_{v}v \right)
\leq
- -1
+ 0
\f]
and we can define the elments of the linear form
@@ -1805,7 +1805,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr,
\leq
k
\leq
- -1
+ 0
\f]
\f[
@@ -1813,7 +1813,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr,
\leq
k_{v}
\leq
- -1
+ 0
\f]
then
@@ -1823,7 +1823,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr,
\approx
\left(i \adivifp 2^{i'} \right)
\bowtie
- -1
+ 0
\f]
\f[
@@ -1831,7 +1831,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr,
\approx
\left(i_{v} \adivifp 2^{i'_{v}} \right)
\bowtie
- -1
+ 0
\f]
Finally, let \f$x\f$ and \f$y\f$ be two integer constants both less
@@ -1842,7 +1842,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr,
\leq
x \gg y
\leq
- -1
+ 0
\f]
Then let \f$i + \sum_{v \in \cV}i_{v}v \f$ and
@@ -1867,7 +1867,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr,
\leq
\left(k + \sum_{v \in \cV}k_{v}v \right)
\leq
- -1
+ 0
\f]
and we can define the elments of the linear form
@@ -1878,7 +1878,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr,
\leq
k
\leq
- -1
+ 0
\f]
\f[
@@ -1886,7 +1886,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr,
\leq
k_{v}
\leq
- -1
+ 0
\f]
then
@@ -1896,7 +1896,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr,
\approx
\left(i \amifp 2^{i'} \right)
\bowtie
- -1
+ 0
\f]
\f[
@@ -1904,7 +1904,7 @@ lshift_linearize_int(const Binary_Operator<Target>& bop_expr,
\approx
\left(i_{v} \amifp 2^{i'_{v}} \right)
\bowtie
- -1
+ 0
\f]
Given an expression \f$e_{1} \rightslice e_{2}\f$ and a composite
More information about the PPL-devel
mailing list