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

Author: Alberto Gioia alberto.gioia1@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