# HG changeset patch # User blanchet # Date 1268234231 -3600 # Node ID 1a49f6b3e4e71880de336f6f830938438e0acd0f # Parent d9c9b81b16a80221c271fbae795b2e10b41ac3f5# Parent 17ae461d613342f654ee46aab62fd6c600813d99 merged diff -r d9c9b81b16a8 -r 1a49f6b3e4e7 doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Wed Mar 10 15:29:23 2010 +0100 +++ b/doc-src/Nitpick/nitpick.tex Wed Mar 10 16:17:11 2010 +0100 @@ -4,6 +4,7 @@ \usepackage{amssymb} \usepackage[english,french]{babel} \usepackage{color} +\usepackage{footmisc} \usepackage{graphicx} %\usepackage{mathpazo} \usepackage{multicol} @@ -1019,7 +1020,7 @@ can be disabled by setting the \textit{bisim\_depth} option to $-1$. The bisimilarity check is then performed \textsl{after} the counterexample has been found to ensure correctness. If this after-the-fact check fails, the -counterexample is tagged as ``likely genuine'' and Nitpick recommends to try +counterexample is tagged as ``quasi genuine'' and Nitpick recommends to try again with \textit{bisim\_depth} set to a nonnegative integer. Disabling the check for the previous example saves approximately 150~milli\-seconds; the speed gains can be more significant for larger scopes. @@ -1031,7 +1032,7 @@ \textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\ \textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount] -\slshape Nitpick found a likely genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount] +\slshape Nitpick found a quasi genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount] \hbox{}\qquad Free variables: \nopagebreak \\ \hbox{}\qquad\qquad $a = a_1$ \\ \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = @@ -1901,7 +1902,7 @@ \textbf{Warning:} If the option is set to \textit{true}, Nitpick might nonetheless ignore some polymorphic axioms. Counterexamples generated under -these conditions are tagged as ``likely genuine.'' The \textit{debug} +these conditions are tagged as ``quasi genuine.'' The \textit{debug} (\S\ref{output-format}) option can be used to find out which axioms were considered. @@ -2002,7 +2003,7 @@ \begin{enum} \item[$\bullet$] \textbf{\textit{true}}: Tentatively treat the (co)in\-duc\-tive predicate as if it were well-founded. Since this is generally not sound when the -predicate is not well-founded, the counterexamples are tagged as ``likely +predicate is not well-founded, the counterexamples are tagged as ``quasi genuine.'' \item[$\bullet$] \textbf{\textit{false}}: Treat the (co)in\-duc\-tive predicate @@ -2050,7 +2051,7 @@ of $-1$ means that no predicate is generated, in which case Nitpick performs an after-the-fact check to see if the known coinductive datatype values are bidissimilar. If two values are found to be bisimilar, the counterexample is -tagged as ``likely genuine.'' The iteration counts are automatically bounded by +tagged as ``quasi genuine.'' The iteration counts are automatically bounded by the sum of the cardinalities of the coinductive datatypes occurring in the formula to falsify. @@ -2100,7 +2101,7 @@ \begin{enum} \item[$\bullet$] \textbf{\textit{true}}: Finitize the datatype. Since this is -unsound, counterexamples generated under these conditions are tagged as ``likely +unsound, counterexamples generated under these conditions are tagged as ``quasi genuine.'' \item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the datatype. \item[$\bullet$] \textbf{\textit{smart}}: Perform a monotonicity analysis to @@ -2268,7 +2269,7 @@ {\small See also \textit{max\_potential} (\S\ref{output-format}).} \opfalse{check\_genuine}{trust\_genuine} -Specifies whether genuine and likely genuine counterexamples should be given to +Specifies whether genuine and quasi genuine counterexamples should be given to Isabelle's \textit{auto} tactic to assess their validity. If a ``genuine'' counterexample is shown to be spurious, the user is kindly asked to send a bug report to the author at @@ -2282,7 +2283,7 @@ \begin{enum} \item[$\bullet$] \textbf{\textit{genuine}}: Nitpick found a genuine counterexample. -\item[$\bullet$] \textbf{\textit{likely\_genuine}}: Nitpick found a ``likely +\item[$\bullet$] \textbf{\textit{quasi\_genuine}}: Nitpick found a ``quasi genuine'' counterexample (i.e., a counterexample that is genuine unless it contradicts a missing axiom or a dangerous option was used inappropriately). \item[$\bullet$] \textbf{\textit{potential}}: Nitpick found a potential counterexample. @@ -2313,12 +2314,18 @@ The supported solvers are listed below: +\let\foo + \begin{enum} \item[$\bullet$] \textbf{\textit{MiniSat}}: MiniSat is an efficient solver written in \cpp{}. To use MiniSat, set the environment variable \texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat} -executable. The \cpp{} sources and executables for MiniSat are available at +executable.% +\footnote{Important note for Cygwin users: The path must be specified using +native Windows syntax. Make sure to escape backslashes properly.% +\label{cygwin-paths}} +The \cpp{} sources and executables for MiniSat are available at \url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14 and 2.0 beta (2007-07-21). @@ -2333,14 +2340,17 @@ \item[$\bullet$] \textbf{\textit{PicoSAT}}: PicoSAT is an efficient solver written in C. You can install a standard version of PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory -that contains the \texttt{picosat} executable. The C sources for PicoSAT are +that contains the \texttt{picosat} executable.% +\footref{cygwin-paths} +The C sources for PicoSAT are available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi. Nitpick has been tested with version 913. \item[$\bullet$] \textbf{\textit{zChaff}}: zChaff is an efficient solver written in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to -the directory that contains the \texttt{zchaff} executable. The \cpp{} sources -and executables for zChaff are available at +the directory that contains the \texttt{zchaff} executable.% +\footref{cygwin-paths} +The \cpp{} sources and executables for zChaff are available at \url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with versions 2004-05-13, 2004-11-15, and 2007-03-12. @@ -2350,26 +2360,32 @@ \item[$\bullet$] \textbf{\textit{RSat}}: RSat is an efficient solver written in \cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the -directory that contains the \texttt{rsat} executable. The \cpp{} sources for -RSat are available at \url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been -tested with version 2.01. +directory that contains the \texttt{rsat} executable.% +\footref{cygwin-paths} +The \cpp{} sources for RSat are available at +\url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been tested with version +2.01. \item[$\bullet$] \textbf{\textit{BerkMin}}: BerkMin561 is an efficient solver written in C. To use BerkMin, set the environment variable \texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561} -executable. The BerkMin executables are available at +executable.\footref{cygwin-paths} +The BerkMin executables are available at \url{http://eigold.tripod.com/BerkMin.html}. \item[$\bullet$] \textbf{\textit{BerkMin\_Alloy}}: Variant of BerkMin that is included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this version of BerkMin, set the environment variable \texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin} -executable. +executable.% +\footref{cygwin-paths} \item[$\bullet$] \textbf{\textit{Jerusat}}: Jerusat 1.3 is an efficient solver written in C. To use Jerusat, set the environment variable \texttt{JERUSAT\_HOME} to the directory that contains the \texttt{Jerusat1.3} -executable. The C sources for Jerusat are available at +executable.% +\footref{cygwin-paths} +The C sources for Jerusat are available at \url{http://www.cs.tau.ac.il/~ale1/Jerusat1.3.tgz}. \item[$\bullet$] \textbf{\textit{SAT4J}}: SAT4J is a reasonably efficient solver @@ -2384,7 +2400,9 @@ \item[$\bullet$] \textbf{\textit{HaifaSat}}: HaifaSat 1.0 beta is an experimental solver written in \cpp. To use HaifaSat, set the environment variable \texttt{HAIFASAT\_\allowbreak HOME} to the directory that contains the -\texttt{HaifaSat} executable. The \cpp{} sources for HaifaSat are available at +\texttt{HaifaSat} executable.% +\footref{cygwin-paths} +The \cpp{} sources for HaifaSat are available at \url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}. \item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to @@ -2668,7 +2686,7 @@ \postw The return value is a new proof state paired with an outcome string -(``genuine'', ``likely\_genuine'', ``potential'', ``none'', or ``unknown''). The +(``genuine'', ``quasi\_genuine'', ``potential'', ``none'', or ``unknown''). The \textit{params} type is a large record that lets you set Nitpick's options. The current default options can be retrieved by calling the following function defined in the \textit{Nitpick\_Isar} structure: diff -r d9c9b81b16a8 -r 1a49f6b3e4e7 src/HOL/Nitpick_Examples/Integer_Nits.thy --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Wed Mar 10 15:29:23 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Wed Mar 10 16:17:11 2010 +0100 @@ -206,4 +206,39 @@ nitpick [binary_ints, expect = none] sorry +datatype tree = Null | Node nat tree tree + +primrec labels where +"labels Null = {}" | +"labels (Node x t u) = {x} \ labels t \ labels u" + +lemma "labels (Node x t u) \ labels (Node y v w)" +nitpick [expect = genuine] +nitpick [dont_finitize, expect = potential] +oops + +lemma "labels (Node x t u) \ {}" +nitpick [expect = none] +oops + +lemma "card (labels t) > 0" +nitpick [expect = genuine] +nitpick [dont_finitize, expect = potential] +oops + +lemma "(\n \ labels t. n + 2) \ 2" +nitpick [expect = genuine] +nitpick [dont_finitize, expect = potential] +oops + +lemma "t \ Null \ (\n \ labels t. n + 2) \ 2" +nitpick [expect = none] +nitpick [dont_finitize, expect = none] +sorry + +lemma "(\i \ labels (Node x t u). f i\nat) = f x + (\i \ labels t. f i) + (\i \ labels u. f i)" +nitpick [expect = genuine] +nitpick [dont_finitize, expect = none] +oops + end diff -r d9c9b81b16a8 -r 1a49f6b3e4e7 src/HOL/Tools/Nitpick/HISTORY --- a/src/HOL/Tools/Nitpick/HISTORY Wed Mar 10 15:29:23 2010 +0100 +++ b/src/HOL/Tools/Nitpick/HISTORY Wed Mar 10 16:17:11 2010 +0100 @@ -11,6 +11,7 @@ * Improved efficiency of "destroy_constrs" optimization * Fixed soundness bugs related to "destroy_constrs" optimization and record getters + * Fixed soundness bug related to higher-order constructors * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light" diff -r d9c9b81b16a8 -r 1a49f6b3e4e7 src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Wed Mar 10 15:29:23 2010 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Wed Mar 10 16:17:11 2010 +0100 @@ -157,7 +157,8 @@ type raw_bound = n_ary_index * int list list datatype outcome = - NotInstalled | + JavaNotInstalled | + KodkodiNotInstalled | Normal of (int * raw_bound list) list * int list * string | TimedOut of int list | Interrupted of int list option | @@ -303,7 +304,8 @@ type raw_bound = n_ary_index * int list list datatype outcome = - NotInstalled | + JavaNotInstalled | + KodkodiNotInstalled | Normal of (int * raw_bound list) list * int list * string | TimedOut of int list | Interrupted of int list option | @@ -893,7 +895,7 @@ map (fn b => (out_assign b; out ";")) expr_assigns; out "solve "; out_outmost_f formula; out ";\n") in - out ("// This file was generated by Isabelle (probably Nitpick)\n" ^ + out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^ "// " ^ Date.fmt "%Y-%m-%d %H:%M:%S" (Date.fromTimeLocal (Time.now ())) ^ "\n"); map out_problem problems @@ -1083,8 +1085,11 @@ ||> apfst (map (apfst reindex)) ||> apsnd (map reindex) val js = triv_js @ nontriv_js val first_error = - File.fold_lines (fn line => fn "" => line | s => s) err_path "" - handle IO.Io _ => "" | OS.SysErr _ => "" + (File.fold_lines (fn line => fn "" => line | s => s) err_path "" + handle IO.Io _ => "" | OS.SysErr _ => "") + |> perhaps (try (unsuffix "\r")) + |> perhaps (try (unsuffix ".")) + |> perhaps (try (unprefix "Error: ")) in if null ps then if code = 2 then @@ -1092,12 +1097,15 @@ else if code = 0 then Normal ([], js, first_error) else if first_error |> Substring.full + |> Substring.position "exec: java" |> snd + |> Substring.isEmpty |> not then + JavaNotInstalled + else if first_error |> Substring.full |> Substring.position "NoClassDefFoundError" |> snd |> Substring.isEmpty |> not then - NotInstalled + KodkodiNotInstalled else if first_error <> "" then - Error (first_error |> perhaps (try (unsuffix ".")) - |> perhaps (try (unprefix "Error: ")), js) + Error (first_error, js) else if io_error then Error ("I/O error", js) else diff -r d9c9b81b16a8 -r 1a49f6b3e4e7 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Mar 10 15:29:23 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Mar 10 16:17:11 2010 +0100 @@ -149,6 +149,9 @@ (length ts downto 1) ts))] (* unit -> string *) +fun install_java_message () = + "Nitpick requires a Java 1.5 virtual machine called \"java\"." +(* unit -> string *) fun install_kodkodi_message () = "Nitpick requires the external Java program Kodkodi. To install it, download \ \the package from Isabelle's web page and add the \"kodkodi-x.y.z\" \ @@ -726,7 +729,10 @@ else case KK.solve_any_problem overlord deadline max_threads max_solutions (map fst problems) of - KK.NotInstalled => + KK.JavaNotInstalled => + (print_m install_java_message; + (found_really_genuine, max_potential, max_genuine, donno + 1)) + | KK.KodkodiNotInstalled => (print_m install_kodkodi_message; (found_really_genuine, max_potential, max_genuine, donno + 1)) | KK.Normal ([], unsat_js, s) => @@ -911,8 +917,7 @@ in "Nitpick " ^ did_so_and_so ^ (if is_some (!checked_problems) andalso total > 0 then - " after checking " ^ - string_of_int (Int.min (total - 1, unsat)) ^ " of " ^ + " " ^ string_of_int (Int.min (total - 1, unsat)) ^ " of " ^ string_of_int total ^ " scope" ^ plural_s total else "") ^ "." @@ -922,7 +927,7 @@ fun run_batches _ _ [] (found_really_genuine, max_potential, max_genuine, donno) = if donno > 0 andalso max_genuine > 0 then - (print_m (fn () => excipit "ran out of some resource"); "unknown") + (print_m (fn () => excipit "checked"); "unknown") else if max_genuine = original_max_genuine then if max_potential = original_max_potential then (print_m (fn () => @@ -966,10 +971,11 @@ (false, max_potential, max_genuine, 0) handle Exn.Interrupt => do_interrupted ()) handle TimeLimit.TimeOut => - (print_m (fn () => excipit "ran out of time"); + (print_m (fn () => excipit "ran out of time after checking"); if !met_potential > 0 then "potential" else "unknown") - | Exn.Interrupt => if auto orelse debug then raise Interrupt - else error (excipit "was interrupted") + | 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.") diff -r d9c9b81b16a8 -r 1a49f6b3e4e7 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Mar 10 15:29:23 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Mar 10 16:17:11 2010 +0100 @@ -1653,6 +1653,7 @@ else kk_comprehension [KK.DeclOne ((1, ~1), to_r discr_u)] (kk_rel_eq (kk_join (KK.Var (1, ~1)) sel_r) arg_r) + |> is_opt_rep (rep_of arg_u) ? to_guard [arg_u] R1 end) sel_us arg_us in fold1 kk_intersect set_rs end | BoundRel (x, _, _, _) => KK.Var x @@ -1723,10 +1724,8 @@ map2 (kk_not oo kk_n_ary_function kk) (map (unopt_rep o rep_of) func_guard_us) func_guard_rs in - if null guard_fs then - r - else - kk_rel_if (fold1 kk_or guard_fs) (empty_rel_for_rep R) r + if null guard_fs then r + else kk_rel_if (fold1 kk_or guard_fs) (empty_rel_for_rep R) r end (* rep -> rep -> KK.rel_expr -> int -> KK.rel_expr *) and to_project new_R old_R r j0 =