--- a/NEWS Wed Nov 03 20:19:24 2010 +0100
+++ b/NEWS Wed Nov 03 22:26:53 2010 +0100
@@ -325,6 +325,14 @@
- Renamed options:
sledgehammer [atps = ...] ~> sledgehammer [provers = ...]
sledgehammer [atp = ...] ~> sledgehammer [prover = ...]
+ sledgehammer [timeout = 77 s] ~> sledgehammer [timeout = 77]
+ (and "ms" and "min" are no longer supported)
+ INCOMPATIBILITY.
+
+* Nitpick:
+ - Renamed options:
+ nitpick [timeout = 77 s] ~> nitpick [timeout = 77]
+ nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777]
INCOMPATIBILITY.
* Changed SMT configuration options:
--- a/doc-src/Nitpick/nitpick.tex Wed Nov 03 20:19:24 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Wed Nov 03 22:26:53 2010 +0100
@@ -261,7 +261,7 @@
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
\hbox{}\qquad\qquad $x = a_3$ \\[2\smallskipamount]
-Total time: 768 ms.
+Total time: 0.76 s.
\postw
Nitpick found a counterexample in which $'a$ has cardinality 3. (For
@@ -797,7 +797,7 @@
Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
\hbox{}\qquad Empty assignment \\[2\smallskipamount]
Nitpick could not find a better counterexample. It checked 0 of 1 scope. \\[2\smallskipamount]
-Total time: 1439 ms.
+Total time: 1.43 s.
\postw
No genuine counterexample is possible because Nitpick cannot rule out the
@@ -850,7 +850,7 @@
& 2 := \{0, 2, 4, 6, 8, 1^\Q, 3^\Q, 5^\Q, 7^\Q, 9^\Q\}, \\[-2pt]
& 1 := \{0, 2, 4, 1^\Q, 3^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\}, \\[-2pt]
& 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\[2\smallskipamount]
-Total time: 2420 ms.
+Total time: 2.42 s.
\postw
Nitpick's output is very instructive. First, it tells us that the predicate is
@@ -1012,7 +1012,7 @@
\hbox{}\qquad\qquad $\textit{b} = a_2$ \\
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount]
-Total time: 1027 ms.
+Total time: 1.02 s.
\postw
The lazy list $\textit{xs}$ is simply $[a_1, a_1, a_1, \ldots]$, whereas
@@ -1160,7 +1160,7 @@
4 := \textit{Var}~0,\>
5 := \textit{Var}~0)\end{aligned}$ \\
\hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount]
-Total time: $3560$ ms.
+Total time: 3.56 s.
\postw
Using \textit{eval}, we find out that $\textit{subst}~\sigma~t =
@@ -1255,7 +1255,7 @@
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\
\hbox{}\qquad\qquad $\textit{ys} = [b_1, b_1]$ \\[2\smallskipamount]
-Total time: 1636 ms.
+Total time: 1.63 s.
\postw
In theory, it should be sufficient to test a single scope:
@@ -1849,7 +1849,7 @@
using \textbf{nitpick\_\allowbreak params}. For example:
\prew
-\textbf{nitpick\_params} [\textit{verbose}, \,\textit{timeout} = 60$\,s$]
+\textbf{nitpick\_params} [\textit{verbose}, \,\textit{timeout} = 60]
\postw
The options are categorized as follows:\ mode of operation
@@ -1887,10 +1887,10 @@
\item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
\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 followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
-(milliseconds), or the keyword \textit{none} ($\infty$ years).
+\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{const\/}: The name of a HOL constant.
\item[$\bullet$] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
\item[$\bullet$] \qtybf{term\_list\/}: A space-separated list of HOL terms (e.g.,
@@ -2510,8 +2510,8 @@
\label{timeouts}
\begin{enum}
-\opdefault{timeout}{time}{$\mathbf{30}$ s}
-Specifies the maximum amount of time that the \textbf{nitpick} command should
+\opdefault{timeout}{time}{$\mathbf{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,
\textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share
@@ -2521,8 +2521,8 @@
\nopagebreak
{\small See also \textit{max\_threads} (\S\ref{optimizations}).}
-\opdefault{tac\_timeout}{time}{$\mathbf{500}$\,ms}
-Specifies the maximum amount of time that the \textit{auto} tactic should use
+\opdefault{tac\_timeout}{time}{$\mathbf{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
predicate is well-founded. Nitpick tries to honor this constraint as well as it
@@ -2863,7 +2863,7 @@
which can become invalid if you change the definition of an inductive predicate
that is registered in the cache. To clear the cache,
run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
-501$\,\textit{ms}$).
+$0.51$).
\item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a
\textbf{guess} command in a structured proof.
--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Nov 03 20:19:24 2010 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Nov 03 22:26:53 2010 +0100
@@ -378,9 +378,9 @@
\textit{smart}.
\item[$\bullet$] \qtybf{int\/}: An integer.
\item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
-\item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes),
-$s$ (seconds), or \textit{ms}
-(milliseconds), or the keyword \textit{none} ($\infty$ years).
+\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).
\end{enum}
Default values are indicated in square brackets. Boolean options have a negated
@@ -457,8 +457,8 @@
\opnodefault{atp}{string}
Legacy alias for \textit{provers}.
-\opdefault{timeout}{time}{$\mathbf{30}$ s}
-Specifies the maximum amount of time that the automatic provers should spend
+\opdefault{timeout}{time}{$\mathbf{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
``Isabelle'' menu in Proof General.
--- a/src/HOL/Mutabelle/MutabelleExtra.thy Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy Wed Nov 03 22:26:53 2010 +0100
@@ -27,7 +27,7 @@
quickcheck_params [size = 5, iterations = 1000]
(*
-nitpick_params [timeout = 5 s, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
+nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
*)
ML {* Auto_Tools.time_limit := 10 *}
--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Wed Nov 03 22:26:53 2010 +0100
@@ -12,7 +12,7 @@
begin
nitpick_params [card = 1\<midarrow>6, unary_ints, max_potential = 0,
- sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
subsection {* Curry in a Hurry *}
--- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Wed Nov 03 22:26:53 2010 +0100
@@ -12,7 +12,7 @@
begin
nitpick_params [card = 1\<midarrow>8, max_potential = 0,
- sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
primrec rot where
"rot Nibble0 = Nibble1" | "rot Nibble1 = Nibble2" | "rot Nibble2 = Nibble3" |
--- a/src/HOL/Nitpick_Examples/Hotel_Nits.thy Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Hotel_Nits.thy Wed Nov 03 22:26:53 2010 +0100
@@ -13,7 +13,7 @@
begin
nitpick_params [max_potential = 0, sat_solver = MiniSat_JNI, max_threads = 1,
- timeout = 120 s]
+ timeout = 120]
typedecl guest
typedecl key
--- a/src/HOL/Nitpick_Examples/Induct_Nits.thy Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy Wed Nov 03 22:26:53 2010 +0100
@@ -12,7 +12,7 @@
begin
nitpick_params [card = 1\<midarrow>8, unary_ints, sat_solver = MiniSat_JNI,
- max_threads = 1, timeout = 60 s]
+ max_threads = 1, timeout = 60]
inductive p1 :: "nat \<Rightarrow> bool" where
"p1 0" |
--- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Wed Nov 03 22:26:53 2010 +0100
@@ -12,7 +12,7 @@
begin
nitpick_params [card = 1\<midarrow>5, bits = 1,2,3,4,6,
- sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
lemma "Suc x = x + 1"
nitpick [unary_ints, expect = none]
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Nov 03 22:26:53 2010 +0100
@@ -17,7 +17,7 @@
chapter {* 3. First Steps *}
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
subsection {* 3.1. Propositional Logic *}
--- a/src/HOL/Nitpick_Examples/Pattern_Nits.thy Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy Wed Nov 03 22:26:53 2010 +0100
@@ -12,7 +12,7 @@
begin
nitpick_params [card = 10, max_potential = 0, sat_solver = MiniSat_JNI,
- max_threads = 1, timeout = 60 s]
+ max_threads = 1, timeout = 60]
lemma "x = (case u of () \<Rightarrow> y)"
nitpick [expect = genuine]
--- a/src/HOL/Nitpick_Examples/Record_Nits.thy Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Record_Nits.thy Wed Nov 03 22:26:53 2010 +0100
@@ -12,7 +12,7 @@
begin
nitpick_params [card = 1\<midarrow>6, max_potential = 0,
- sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
record point2d =
xc :: int
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Nov 03 22:26:53 2010 +0100
@@ -12,7 +12,7 @@
begin
nitpick_params [card = 1\<midarrow>6, max_potential = 0,
- sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60 s]
+ sat_solver = MiniSat_JNI, max_threads = 1, timeout = 60]
lemma "P \<and> Q"
apply (rule conjI)
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Wed Nov 03 22:26:53 2010 +0100
@@ -12,7 +12,7 @@
begin
nitpick_params [card = 4, sat_solver = MiniSat_JNI, max_threads = 1,
- timeout = 60 s]
+ timeout = 60]
fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
"f1 a b c d e = a + b + c + d + e"
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Nov 03 22:26:53 2010 +0100
@@ -12,7 +12,7 @@
begin
nitpick_params [card = 1\<midarrow>4, sat_solver = MiniSat_JNI, max_threads = 1,
- timeout = 60 s]
+ timeout = 60]
typedef three = "{0\<Colon>nat, 1, 2}"
by blast
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Nov 03 22:26:53 2010 +0100
@@ -980,9 +980,9 @@
| Exn.Interrupt =>
if auto orelse debug then raise Interrupt
else error (excipit "was interrupted after checking")
- val _ = print_v (fn () => "Total time: " ^
- signed_string_of_int (Time.toMilliseconds
- (Timer.checkRealTimer timer)) ^ " ms.")
+ val _ = print_v (fn () =>
+ "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^
+ ".")
in (outcome_code, !state_ref) end
handle Exn.Interrupt =>
if auto orelse #debug params then
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Nov 03 22:26:53 2010 +0100
@@ -61,8 +61,8 @@
("peephole_optim", "true"),
("datatype_sym_break", "5"),
("kodkod_sym_break", "15"),
- ("timeout", "30 s"),
- ("tac_timeout", "500 ms"),
+ ("timeout", "30"),
+ ("tac_timeout", "0.5"),
("max_threads", "0"),
("debug", "false"),
("verbose", "false"),
@@ -297,8 +297,10 @@
val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
val parse_value =
Scan.repeat1 (Parse.minus >> single
- || Scan.repeat1 (Scan.unless Parse.minus Parse.name)
- || Parse.$$$ "," |-- Parse.number >> prefix "," >> single) >> flat
+ || Scan.repeat1 (Scan.unless Parse.minus
+ (Parse.name || Parse.float_number))
+ || Parse.$$$ "," |-- Parse.number >> prefix "," >> single)
+ >> flat
val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
val parse_params =
Scan.optional (Parse.$$$ "[" |-- Parse.list parse_param --| Parse.$$$ "]") []
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Nov 03 22:26:53 2010 +0100
@@ -52,6 +52,7 @@
val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
+ val string_from_time : Time.time -> string
val nat_subscript : int -> string
val flip_polarity : polarity -> polarity
val prop_T : typ
@@ -237,6 +238,7 @@
val parse_bool_option = Sledgehammer_Util.parse_bool_option
val parse_time_option = Sledgehammer_Util.parse_time_option
+val string_from_time = Sledgehammer_Util.string_from_time
val i_subscript = implode o map (prefix "\<^isub>") o explode
fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Nov 03 22:26:53 2010 +0100
@@ -411,11 +411,12 @@
(proof_banner auto, full_types, minimize_command, tstplike_proof,
fact_names, goal, subgoal)
|>> (fn message =>
- message ^ (if verbose then
- "\nATP real CPU time: " ^
- string_of_int (the msecs) ^ " ms."
- else
- "") ^
+ message ^
+ (if verbose then
+ "\nATP real CPU time: " ^
+ string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
+ else
+ "") ^
(if important_message <> "" then
"\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
important_message
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Nov 03 22:26:53 2010 +0100
@@ -177,7 +177,7 @@
("full_types", [if !full_types then "true" else "false"]),
("timeout", let val timeout = !timeout in
[if timeout <= 0 then "none"
- else string_of_int timeout ^ " s"]
+ else string_of_int timeout]
end)]
end
@@ -322,7 +322,7 @@
end))
val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
-val parse_value = Scan.repeat1 Parse.xname
+val parse_value = Scan.repeat1 (Parse.xname || Parse.float_number)
val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
val parse_fact_refs =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Nov 03 22:26:53 2010 +0100
@@ -124,13 +124,13 @@
| {outcome = SOME TimedOut, ...} =>
(NONE, "Timeout: You can increase the time limit using the \"timeout\" \
\option (e.g., \"timeout = " ^
- string_of_int (10 + msecs div 1000) ^ " s\").")
+ string_of_int (10 + msecs div 1000) ^ "\").")
| {outcome = SOME UnknownError, ...} =>
(* Failure sometimes mean timeout, unfortunately. *)
(NONE, "Failure: No proof was found with the current time limit. You \
\can increase the time limit using the \"timeout\" \
\option (e.g., \"timeout = " ^
- string_of_int (10 + msecs div 1000) ^ " s\").")
+ string_of_int (10 + msecs div 1000) ^ "\").")
| {message, ...} => (NONE, "ATP error: " ^ message))
handle ERROR msg => (NONE, "Error: " ^ msg)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Nov 03 20:19:24 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Nov 03 22:26:53 2010 +0100
@@ -11,6 +11,7 @@
val simplify_spaces : string -> string
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
+ val string_from_time : Time.time -> string
val nat_subscript : int -> string
val unyxml : string -> string
val maybe_quote : string -> string
@@ -49,23 +50,22 @@
space_implode " " (serial_commas "or" ss) ^ ".")
end
+val has_junk =
+ exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o explode
+
fun parse_time_option _ "none" = NONE
| parse_time_option name s =
- let
- val msecs =
- case space_explode " " s of
- [s1, "min"] => 60000 * the (Int.fromString s1)
- | [s1, "s"] => 1000 * the (Int.fromString s1)
- | [s1, "ms"] => the (Int.fromString s1)
- | _ => 0
- in
- if msecs <= 0 then
- error ("Parameter " ^ quote name ^ " must be assigned a positive time \
- \value (e.g., \"60 s\", \"200 ms\") or \"none\".")
+ let val secs = if has_junk s then NONE else Real.fromString s in
+ if is_none secs orelse Real.<= (the secs, 0.0) then
+ error ("Parameter " ^ quote name ^ " must be assigned a positive \
+ \number of seconds (e.g., \"60\", \"0.5\") or \"none\".")
else
- SOME (Time.fromMilliseconds msecs)
+ SOME (seconds (the secs))
end
+fun string_from_time t =
+ string_of_real (0.01 * Real.fromInt (Time.toMilliseconds t div 10)) ^ " s"
+
val subscript = implode o map (prefix "\<^isub>") o explode
fun nat_subscript n =
n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript