# HG changeset patch
# User blanchet
# Date 1288821092 -3600
# Node ID 4521d56aef63553721602f87a50fe2c430bb50b6
# Parent  3154f63e2bda72b7c2a54046afb897ae42d0e685
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
updated docs

diff -r 3154f63e2bda -r 4521d56aef63 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Wed Nov 03 22:33:23 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Wed Nov 03 22:51:32 2010 +0100
@@ -1888,7 +1888,7 @@
 \item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
 of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<midarrow\char`\>}.
 \item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
-\item[$\bullet$] \qtybf{time}: An integer (e.g., 60) or floating-point number
+\item[$\bullet$] \qtybf{float\_or\_none}: An integer (e.g., 60) or floating-point number
 (e.g., 0.5) expressing a number of seconds, or the keyword \textit{none}
 ($\infty$ seconds).
 \item[$\bullet$] \qtybf{const\/}: The name of a HOL constant.
@@ -1966,7 +1966,7 @@
 {\small See also \textit{box} (\S\ref{scope-of-search}) and \textit{mono}
 (\S\ref{scope-of-search}).}
 
-\opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{10}$}
+\opdefault{card}{int\_seq}{\upshape 1--10}
 Specifies the default sequence of cardinalities to use. This can be overridden
 on a per-type basis using the \textit{card}~\qty{type} option described above.
 
@@ -2014,7 +2014,7 @@
 {\small See also \textit{bits} (\S\ref{scope-of-search}) and
 \textit{show\_datatypes} (\S\ref{output-format}).}
 
-\opdefault{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12},\mathbf{14},\mathbf{16}$}
+\opdefault{bits}{int\_seq}{\upshape 1,2,3,4,6,8,10,12,14,16}
 Specifies the number of bits to use to represent natural numbers and integers in
 binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
 
@@ -2064,12 +2064,12 @@
 {\small See also \textit{wf} (\S\ref{scope-of-search}) and
 \textit{star\_linear\_preds} (\S\ref{optimizations}).}
 
-\opdefault{iter}{int\_seq}{$\mathbf{0{,}1{,}2{,}4{,}8{,}12{,}16{,}20{,}24{,}28}$}
+\opdefault{iter}{int\_seq}{\upshape 0{,}1{,}2{,}4{,}8{,}12{,}16{,}20{,}24{,}28}
 Specifies the sequence of iteration counts to use when unrolling (co)in\-duc\-tive
 predicates. This can be overridden on a per-predicate basis using the
 \textit{iter} \qty{const} option above.
 
-\opdefault{bisim\_depth}{int\_seq}{$\mathbf{9}$}
+\opdefault{bisim\_depth}{int\_seq}{\upshape 9}
 Specifies the sequence of iteration counts to use when unrolling the
 bisimilarity predicate generated by Nitpick for coinductive datatypes. A value
 of $-1$ means that no predicate is generated, in which case Nitpick performs an
@@ -2214,7 +2214,7 @@
 \opnodefault{show\_all}{bool}
 Abbreviation for \textit{show\_datatypes} and \textit{show\_consts}.
 
-\opdefault{max\_potential}{int}{$\mathbf{1}$}
+\opdefault{max\_potential}{int}{\upshape 1}
 Specifies the maximum number of potential counterexamples to display. Setting
 this option to 0 speeds up the search for a genuine counterexample. This option
 is implicitly set to 0 for automatic runs. If you set this option to a value
@@ -2226,7 +2226,7 @@
 {\small See also \textit{check\_potential} (\S\ref{authentication}) and
 \textit{sat\_solver} (\S\ref{optimizations}).}
 
-\opdefault{max\_genuine}{int}{$\mathbf{1}$}
+\opdefault{max\_genuine}{int}{\upshape 1}
 Specifies the maximum number of genuine counterexamples to display. If you set
 this option to a value greater than 1, you will need an incremental SAT solver,
 such as \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that
@@ -2267,7 +2267,7 @@
 arguments that are not accounted for are left alone, as if the specification had
 been $1,\ldots,1,n_1,\ldots,n_k$.
 
-\opdefault{format}{int\_seq}{$\mathbf{1}$}
+\opdefault{format}{int\_seq}{\upshape 1}
 Specifies the default format to use. Irrespective of the default format, the
 extra arguments to a Skolem constant corresponding to the outer bound variables
 are kept separated from the remaining arguments, the \textbf{for} arguments of
@@ -2484,19 +2484,19 @@
 Unless you are tracking down a bug in Nitpick or distrust the peephole
 optimizer, you should leave this option enabled.
 
-\opdefault{datatype\_sym\_break}{int}{5}
+\opdefault{datatype\_sym\_break}{int}{\upshape 5}
 Specifies an upper bound on the number of datatypes for which Nitpick generates
 symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
 considerably, especially for unsatisfiable problems, but too much of it can slow
 it down.
 
-\opdefault{kodkod\_sym\_break}{int}{15}
+\opdefault{kodkod\_sym\_break}{int}{\upshape 15}
 Specifies an upper bound on the number of relations for which Kodkod generates
 symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
 considerably, especially for unsatisfiable problems, but too much of it can slow
 it down.
 
-\opdefault{max\_threads}{int}{0}
+\opdefault{max\_threads}{int}{\upshape 0}
 Specifies the maximum number of threads to use in Kodkod. If this option is set
 to 0, Kodkod will compute an appropriate value based on the number of processor
 cores available. The option is implicitly set to 1 for automatic runs.
@@ -2510,7 +2510,7 @@
 \label{timeouts}
 
 \begin{enum}
-\opdefault{timeout}{time}{$\mathbf{30}$}
+\opdefault{timeout}{float\_or\_none}{\upshape 30}
 Specifies the maximum number of seconds that the \textbf{nitpick} command should
 spend looking for a counterexample. Nitpick tries to honor this constraint as
 well as it can but offers no guarantees. For automatic runs,
@@ -2521,7 +2521,7 @@
 \nopagebreak
 {\small See also \textit{max\_threads} (\S\ref{optimizations}).}
 
-\opdefault{tac\_timeout}{time}{$\mathbf{0.5}$}
+\opdefault{tac\_timeout}{float\_or\_none}{\upshape 0.5}
 Specifies the maximum number of seconds that the \textit{auto} tactic should use
 when checking a counterexample, and similarly that \textit{lexicographic\_order}
 and \textit{size\_change} should use when checking whether a (co)in\-duc\-tive
diff -r 3154f63e2bda -r 4521d56aef63 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Nov 03 22:33:23 2010 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Nov 03 22:51:32 2010 +0100
@@ -377,10 +377,12 @@
 \item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or
 \textit{smart}.
 \item[$\bullet$] \qtybf{int\/}: An integer.
+\item[$\bullet$] \qtybf{float\_pair\/}: A pair of floating-point numbers
+(e.g., 0.6 0.95).
 \item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
-\item[$\bullet$] \qtybf{time}: An integer (e.g., 60) or floating-point number
-(e.g., 0.5) expressing a number of seconds, or the keyword \textit{none}
-($\infty$ seconds).
+\item[$\bullet$] \qtybf{float\_or\_none\/}: An integer (e.g., 60) or
+floating-point number (e.g., 0.5) expressing a number of seconds, or the keyword
+\textit{none} ($\infty$ seconds).
 \end{enum}
 
 Default values are indicated in square brackets. Boolean options have a negated
@@ -457,7 +459,7 @@
 \opnodefault{atp}{string}
 Legacy alias for \textit{provers}.
 
-\opdefault{timeout}{time}{$\mathbf{30}$}
+\opdefault{timeout}{float\_or\_none}{\upshape 30}
 Specifies the maximum number of seconds that the automatic provers should spend
 searching for a proof. For historical reasons, the default value of this option
 can be overridden using the option ``Sledgehammer: Time Limit'' from the
@@ -503,15 +505,15 @@
 \label{relevance-filter}
 
 \begin{enum}
-\opdefault{relevance\_thresholds}{int\_pair}{45~85}
+\opdefault{relevance\_thresholds}{float\_pair}{\upshape 0.45~0.85}
 Specifies the thresholds above which facts are considered relevant by the
 relevance filter. The first threshold is used for the first iteration of the
 relevance filter and the second threshold is used for the last iteration (if it
 is reached). The effective threshold is quadratically interpolated for the other
-iterations. Each threshold ranges from 0 to 100, where 0 means that all theorems
-are relevant and 100 only theorems that refer to previously seen constants.
+iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems
+are relevant and 1 only theorems that refer to previously seen constants.
 
-\opdefault{max\_relevant}{int\_or\_smart}{\textit{smart}}
+\opsmart{max\_relevant}{int\_or\_smart}
 Specifies the maximum number of facts that may be returned by the relevance
 filter. If the option is set to \textit{smart}, it is set to a value that was
 empirically found to be appropriate for the prover. A typical value would be
@@ -540,7 +542,7 @@
 fails; however, they are usually faster and sometimes more robust than
 \textit{metis} proofs.
 
-\opdefault{isar\_shrink\_factor}{int}{1}
+\opdefault{isar\_shrink\_factor}{int}{\upshape 1}
 Specifies the granularity of the Isar proof. A value of $n$ indicates that each
 Isar proof step should correspond to a group of up to $n$ consecutive proof
 steps in the ATP proof.
diff -r 3154f63e2bda -r 4521d56aef63 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Nov 03 22:33:23 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Nov 03 22:51:32 2010 +0100
@@ -78,7 +78,7 @@
    ("verbose", "false"),
    ("overlord", "false"),
    ("explicit_apply", "false"),
-   ("relevance_thresholds", "45 85"),
+   ("relevance_thresholds", "0.45 0.85"),
    ("max_relevant", "smart"),
    ("isar_proof", "false"),
    ("isar_shrink_factor", "1")]
@@ -206,14 +206,14 @@
                     SOME n => n
                   | NONE => error ("Parameter " ^ quote name ^
                                    " must be assigned an integer value.")
-    fun lookup_int_pair name =
+    fun lookup_real_pair name =
       case lookup name of
-        NONE => (0, 0)
-      | SOME s => case s |> space_explode " " |> map Int.fromString of
-                    [SOME n1, SOME n2] => (n1, n2)
+        NONE => (0.0, 0.0)
+      | SOME s => case s |> space_explode " " |> map Real.fromString of
+                    [SOME r1, SOME r2] => (r1, r2)
                   | _ => error ("Parameter " ^ quote name ^
-                                "must be assigned a pair of integer values \
-                                \(e.g., \"60 95\")")
+                                "must be assigned a pair of floating-point \
+                                \values (e.g., \"0.6 0.95\")")
     fun lookup_int_option name =
       case lookup name of
         SOME "smart" => NONE
@@ -226,9 +226,7 @@
                   |> auto ? single o hd
     val full_types = lookup_bool "full_types"
     val explicit_apply = lookup_bool "explicit_apply"
-    val relevance_thresholds =
-      lookup_int_pair "relevance_thresholds"
-      |> pairself (fn n => 0.01 * Real.fromInt n)
+    val relevance_thresholds = lookup_real_pair "relevance_thresholds"
     val max_relevant = lookup_int_option "max_relevant"
     val isar_proof = lookup_bool "isar_proof"
     val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")