Module: ppl/ppl Branch: bounded_arithmetic Commit: 126e67ad12f38972e01d0dbe529e970a70c059a6 URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=126e67ad12f38...
Author: Alberto Gioia alberto.gioia1@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]