--- 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:
--- 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} \<union> labels t \<union> labels u"
+
+lemma "labels (Node x t u) \<noteq> labels (Node y v w)"
+nitpick [expect = genuine]
+nitpick [dont_finitize, expect = potential]
+oops
+
+lemma "labels (Node x t u) \<noteq> {}"
+nitpick [expect = none]
+oops
+
+lemma "card (labels t) > 0"
+nitpick [expect = genuine]
+nitpick [dont_finitize, expect = potential]
+oops
+
+lemma "(\<Sum>n \<in> labels t. n + 2) \<ge> 2"
+nitpick [expect = genuine]
+nitpick [dont_finitize, expect = potential]
+oops
+
+lemma "t \<noteq> Null \<Longrightarrow> (\<Sum>n \<in> labels t. n + 2) \<ge> 2"
+nitpick [expect = none]
+nitpick [dont_finitize, expect = none]
+sorry
+
+lemma "(\<Sum>i \<in> labels (Node x t u). f i\<Colon>nat) = f x + (\<Sum>i \<in> labels t. f i) + (\<Sum>i \<in> labels u. f i)"
+nitpick [expect = genuine]
+nitpick [dont_finitize, expect = none]
+oops
+
end
--- 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"
--- 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
--- 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.")
--- 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 =