updated Nitpick's documentation w.r.t. finitization
authorblanchet
Tue Dec 07 11:56:56 2010 +0100 (2010-12-07)
changeset 410538e2f2398aae7
parent 41052 3db267a01c1d
child 41054 e58d1cdda832
updated Nitpick's documentation w.r.t. finitization
doc-src/Nitpick/nitpick.tex
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Dec 07 11:56:53 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Dec 07 11:56:56 2010 +0100
     1.3 @@ -2108,14 +2108,9 @@
     1.4  per-type basis using the \textit{box}~\qty{type} option described above.
     1.5  
     1.6  \opargboolorsmart{finitize}{type}{dont\_finitize}
     1.7 -Specifies whether Nitpick should attempt to finitize a given type, which can be
     1.8 -a function type or an infinite ``shallow datatype'' (an infinite datatype whose
     1.9 -constructors don't appear in the problem).
    1.10 -
    1.11 -For function types, Nitpick performs a monotonicity analysis to detect functions
    1.12 -that are constant at all but finitely many points (e.g., finite sets) and treats
    1.13 -such occurrences specially, thereby increasing the precision. The option can
    1.14 -then take the following values:
    1.15 +Specifies whether Nitpick should attempt to finitize an infinite ``shallow
    1.16 +datatype'' (an infinite datatype whose constructors don't appear in the
    1.17 +problem). The option can then take the following values:
    1.18  
    1.19  \begin{enum}
    1.20  \item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the type.
    1.21 @@ -2132,12 +2127,9 @@
    1.22  genuine.''
    1.23  \item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the datatype.
    1.24  \item[$\bullet$] \textbf{\textit{smart}:} Perform a monotonicity analysis to
    1.25 -detect whether the datatype can be safely finitized before finitizing it.
    1.26 +detect whether the datatype can be soundly finitized before finitizing it.
    1.27  \end{enum}
    1.28  
    1.29 -Like other drastic optimizations, finitization can sometimes prevent the
    1.30 -discovery of counterexamples.
    1.31 -
    1.32  \nopagebreak
    1.33  {\small See also \textit{box} (\S\ref{scope-of-search}), \textit{mono}
    1.34  (\S\ref{scope-of-search}), \textit{verbose} (\S\ref{output-format}), and