1.1 --- a/doc-src/Nitpick/nitpick.tex Wed Mar 10 08:04:50 2010 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Wed Mar 10 14:21:01 2010 +0100
1.3 @@ -4,6 +4,7 @@
1.4 \usepackage{amssymb}
1.5 \usepackage[english,french]{babel}
1.6 \usepackage{color}
1.7 +\usepackage{footmisc}
1.8 \usepackage{graphicx}
1.9 %\usepackage{mathpazo}
1.10 \usepackage{multicol}
1.11 @@ -1019,7 +1020,7 @@
1.12 can be disabled by setting the \textit{bisim\_depth} option to $-1$. The
1.13 bisimilarity check is then performed \textsl{after} the counterexample has been
1.14 found to ensure correctness. If this after-the-fact check fails, the
1.15 -counterexample is tagged as ``likely genuine'' and Nitpick recommends to try
1.16 +counterexample is tagged as ``quasi genuine'' and Nitpick recommends to try
1.17 again with \textit{bisim\_depth} set to a nonnegative integer. Disabling the
1.18 check for the previous example saves approximately 150~milli\-seconds; the speed
1.19 gains can be more significant for larger scopes.
1.20 @@ -1031,7 +1032,7 @@
1.21 \textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
1.22 \,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
1.23 \textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
1.24 -\slshape Nitpick found a likely genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
1.25 +\slshape Nitpick found a quasi genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
1.26 \hbox{}\qquad Free variables: \nopagebreak \\
1.27 \hbox{}\qquad\qquad $a = a_1$ \\
1.28 \hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega =
1.29 @@ -1901,7 +1902,7 @@
1.30
1.31 \textbf{Warning:} If the option is set to \textit{true}, Nitpick might
1.32 nonetheless ignore some polymorphic axioms. Counterexamples generated under
1.33 -these conditions are tagged as ``likely genuine.'' The \textit{debug}
1.34 +these conditions are tagged as ``quasi genuine.'' The \textit{debug}
1.35 (\S\ref{output-format}) option can be used to find out which axioms were
1.36 considered.
1.37
1.38 @@ -2002,7 +2003,7 @@
1.39 \begin{enum}
1.40 \item[$\bullet$] \textbf{\textit{true}}: Tentatively treat the (co)in\-duc\-tive
1.41 predicate as if it were well-founded. Since this is generally not sound when the
1.42 -predicate is not well-founded, the counterexamples are tagged as ``likely
1.43 +predicate is not well-founded, the counterexamples are tagged as ``quasi
1.44 genuine.''
1.45
1.46 \item[$\bullet$] \textbf{\textit{false}}: Treat the (co)in\-duc\-tive predicate
1.47 @@ -2050,7 +2051,7 @@
1.48 of $-1$ means that no predicate is generated, in which case Nitpick performs an
1.49 after-the-fact check to see if the known coinductive datatype values are
1.50 bidissimilar. If two values are found to be bisimilar, the counterexample is
1.51 -tagged as ``likely genuine.'' The iteration counts are automatically bounded by
1.52 +tagged as ``quasi genuine.'' The iteration counts are automatically bounded by
1.53 the sum of the cardinalities of the coinductive datatypes occurring in the
1.54 formula to falsify.
1.55
1.56 @@ -2100,7 +2101,7 @@
1.57
1.58 \begin{enum}
1.59 \item[$\bullet$] \textbf{\textit{true}}: Finitize the datatype. Since this is
1.60 -unsound, counterexamples generated under these conditions are tagged as ``likely
1.61 +unsound, counterexamples generated under these conditions are tagged as ``quasi
1.62 genuine.''
1.63 \item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the datatype.
1.64 \item[$\bullet$] \textbf{\textit{smart}}: Perform a monotonicity analysis to
1.65 @@ -2268,7 +2269,7 @@
1.66 {\small See also \textit{max\_potential} (\S\ref{output-format}).}
1.67
1.68 \opfalse{check\_genuine}{trust\_genuine}
1.69 -Specifies whether genuine and likely genuine counterexamples should be given to
1.70 +Specifies whether genuine and quasi genuine counterexamples should be given to
1.71 Isabelle's \textit{auto} tactic to assess their validity. If a ``genuine''
1.72 counterexample is shown to be spurious, the user is kindly asked to send a bug
1.73 report to the author at
1.74 @@ -2282,7 +2283,7 @@
1.75
1.76 \begin{enum}
1.77 \item[$\bullet$] \textbf{\textit{genuine}}: Nitpick found a genuine counterexample.
1.78 -\item[$\bullet$] \textbf{\textit{likely\_genuine}}: Nitpick found a ``likely
1.79 +\item[$\bullet$] \textbf{\textit{quasi\_genuine}}: Nitpick found a ``quasi
1.80 genuine'' counterexample (i.e., a counterexample that is genuine unless
1.81 it contradicts a missing axiom or a dangerous option was used inappropriately).
1.82 \item[$\bullet$] \textbf{\textit{potential}}: Nitpick found a potential counterexample.
1.83 @@ -2313,12 +2314,18 @@
1.84
1.85 The supported solvers are listed below:
1.86
1.87 +\let\foo
1.88 +
1.89 \begin{enum}
1.90
1.91 \item[$\bullet$] \textbf{\textit{MiniSat}}: MiniSat is an efficient solver
1.92 written in \cpp{}. To use MiniSat, set the environment variable
1.93 \texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
1.94 -executable. The \cpp{} sources and executables for MiniSat are available at
1.95 +executable.%
1.96 +\footnote{Important note for Cygwin users: The path must be specified using
1.97 +native Windows syntax. Make sure to escape backslashes properly.%
1.98 +\label{cygwin-paths}}
1.99 +The \cpp{} sources and executables for MiniSat are available at
1.100 \url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
1.101 and 2.0 beta (2007-07-21).
1.102
1.103 @@ -2333,14 +2340,17 @@
1.104 \item[$\bullet$] \textbf{\textit{PicoSAT}}: PicoSAT is an efficient solver
1.105 written in C. You can install a standard version of
1.106 PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
1.107 -that contains the \texttt{picosat} executable. The C sources for PicoSAT are
1.108 +that contains the \texttt{picosat} executable.%
1.109 +\footref{cygwin-paths}
1.110 +The C sources for PicoSAT are
1.111 available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi.
1.112 Nitpick has been tested with version 913.
1.113
1.114 \item[$\bullet$] \textbf{\textit{zChaff}}: zChaff is an efficient solver written
1.115 in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
1.116 -the directory that contains the \texttt{zchaff} executable. The \cpp{} sources
1.117 -and executables for zChaff are available at
1.118 +the directory that contains the \texttt{zchaff} executable.%
1.119 +\footref{cygwin-paths}
1.120 +The \cpp{} sources and executables for zChaff are available at
1.121 \url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
1.122 versions 2004-05-13, 2004-11-15, and 2007-03-12.
1.123
1.124 @@ -2350,26 +2360,32 @@
1.125
1.126 \item[$\bullet$] \textbf{\textit{RSat}}: RSat is an efficient solver written in
1.127 \cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the
1.128 -directory that contains the \texttt{rsat} executable. The \cpp{} sources for
1.129 -RSat are available at \url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been
1.130 -tested with version 2.01.
1.131 +directory that contains the \texttt{rsat} executable.%
1.132 +\footref{cygwin-paths}
1.133 +The \cpp{} sources for RSat are available at
1.134 +\url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been tested with version
1.135 +2.01.
1.136
1.137 \item[$\bullet$] \textbf{\textit{BerkMin}}: BerkMin561 is an efficient solver
1.138 written in C. To use BerkMin, set the environment variable
1.139 \texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561}
1.140 -executable. The BerkMin executables are available at
1.141 +executable.\footref{cygwin-paths}
1.142 +The BerkMin executables are available at
1.143 \url{http://eigold.tripod.com/BerkMin.html}.
1.144
1.145 \item[$\bullet$] \textbf{\textit{BerkMin\_Alloy}}: Variant of BerkMin that is
1.146 included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this
1.147 version of BerkMin, set the environment variable
1.148 \texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
1.149 -executable.
1.150 +executable.%
1.151 +\footref{cygwin-paths}
1.152
1.153 \item[$\bullet$] \textbf{\textit{Jerusat}}: Jerusat 1.3 is an efficient solver
1.154 written in C. To use Jerusat, set the environment variable
1.155 \texttt{JERUSAT\_HOME} to the directory that contains the \texttt{Jerusat1.3}
1.156 -executable. The C sources for Jerusat are available at
1.157 +executable.%
1.158 +\footref{cygwin-paths}
1.159 +The C sources for Jerusat are available at
1.160 \url{http://www.cs.tau.ac.il/~ale1/Jerusat1.3.tgz}.
1.161
1.162 \item[$\bullet$] \textbf{\textit{SAT4J}}: SAT4J is a reasonably efficient solver
1.163 @@ -2384,7 +2400,9 @@
1.164 \item[$\bullet$] \textbf{\textit{HaifaSat}}: HaifaSat 1.0 beta is an
1.165 experimental solver written in \cpp. To use HaifaSat, set the environment
1.166 variable \texttt{HAIFASAT\_\allowbreak HOME} to the directory that contains the
1.167 -\texttt{HaifaSat} executable. The \cpp{} sources for HaifaSat are available at
1.168 +\texttt{HaifaSat} executable.%
1.169 +\footref{cygwin-paths}
1.170 +The \cpp{} sources for HaifaSat are available at
1.171 \url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}.
1.172
1.173 \item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
1.174 @@ -2668,7 +2686,7 @@
1.175 \postw
1.176
1.177 The return value is a new proof state paired with an outcome string
1.178 -(``genuine'', ``likely\_genuine'', ``potential'', ``none'', or ``unknown''). The
1.179 +(``genuine'', ``quasi\_genuine'', ``potential'', ``none'', or ``unknown''). The
1.180 \textit{params} type is a large record that lets you set Nitpick's options. The
1.181 current default options can be retrieved by calling the following function
1.182 defined in the \textit{Nitpick\_Isar} structure:
2.1 --- a/src/HOL/Nitpick_Examples/Integer_Nits.thy Wed Mar 10 08:04:50 2010 +0100
2.2 +++ b/src/HOL/Nitpick_Examples/Integer_Nits.thy Wed Mar 10 14:21:01 2010 +0100
2.3 @@ -206,4 +206,39 @@
2.4 nitpick [binary_ints, expect = none]
2.5 sorry
2.6
2.7 +datatype tree = Null | Node nat tree tree
2.8 +
2.9 +primrec labels where
2.10 +"labels Null = {}" |
2.11 +"labels (Node x t u) = {x} \<union> labels t \<union> labels u"
2.12 +
2.13 +lemma "labels (Node x t u) \<noteq> labels (Node y v w)"
2.14 +nitpick [expect = genuine]
2.15 +nitpick [dont_finitize, expect = potential]
2.16 +oops
2.17 +
2.18 +lemma "labels (Node x t u) \<noteq> {}"
2.19 +nitpick [expect = none]
2.20 +oops
2.21 +
2.22 +lemma "card (labels t) > 0"
2.23 +nitpick [expect = genuine]
2.24 +nitpick [dont_finitize, expect = potential]
2.25 +oops
2.26 +
2.27 +lemma "(\<Sum>n \<in> labels t. n + 2) \<ge> 2"
2.28 +nitpick [expect = genuine]
2.29 +nitpick [dont_finitize, expect = potential]
2.30 +oops
2.31 +
2.32 +lemma "t \<noteq> Null \<Longrightarrow> (\<Sum>n \<in> labels t. n + 2) \<ge> 2"
2.33 +nitpick [expect = none]
2.34 +nitpick [dont_finitize, expect = none]
2.35 +sorry
2.36 +
2.37 +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)"
2.38 +nitpick [expect = genuine]
2.39 +nitpick [dont_finitize, expect = none]
2.40 +oops
2.41 +
2.42 end
3.1 --- a/src/HOL/Tools/Nitpick/HISTORY Wed Mar 10 08:04:50 2010 +0100
3.2 +++ b/src/HOL/Tools/Nitpick/HISTORY Wed Mar 10 14:21:01 2010 +0100
3.3 @@ -11,6 +11,7 @@
3.4 * Improved efficiency of "destroy_constrs" optimization
3.5 * Fixed soundness bugs related to "destroy_constrs" optimization and record
3.6 getters
3.7 + * Fixed soundness bug related to higher-order constructors
3.8 * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
3.9 "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
3.10
4.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML Wed Mar 10 08:04:50 2010 +0100
4.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Wed Mar 10 14:21:01 2010 +0100
4.3 @@ -893,7 +893,7 @@
4.4 map (fn b => (out_assign b; out ";")) expr_assigns;
4.5 out "solve "; out_outmost_f formula; out ";\n")
4.6 in
4.7 - out ("// This file was generated by Isabelle (probably Nitpick)\n" ^
4.8 + out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^
4.9 "// " ^ Date.fmt "%Y-%m-%d %H:%M:%S"
4.10 (Date.fromTimeLocal (Time.now ())) ^ "\n");
4.11 map out_problem problems
4.12 @@ -1083,8 +1083,11 @@
4.13 ||> apfst (map (apfst reindex)) ||> apsnd (map reindex)
4.14 val js = triv_js @ nontriv_js
4.15 val first_error =
4.16 - File.fold_lines (fn line => fn "" => line | s => s) err_path ""
4.17 - handle IO.Io _ => "" | OS.SysErr _ => ""
4.18 + (File.fold_lines (fn line => fn "" => line | s => s) err_path ""
4.19 + handle IO.Io _ => "" | OS.SysErr _ => "")
4.20 + |> perhaps (try (unsuffix "\r"))
4.21 + |> perhaps (try (unsuffix "."))
4.22 + |> perhaps (try (unprefix "Error: "))
4.23 in
4.24 if null ps then
4.25 if code = 2 then
4.26 @@ -1096,8 +1099,7 @@
4.27 |> Substring.isEmpty |> not then
4.28 NotInstalled
4.29 else if first_error <> "" then
4.30 - Error (first_error |> perhaps (try (unsuffix "."))
4.31 - |> perhaps (try (unprefix "Error: ")), js)
4.32 + Error (first_error, js)
4.33 else if io_error then
4.34 Error ("I/O error", js)
4.35 else
5.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Mar 10 08:04:50 2010 +0100
5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Mar 10 14:21:01 2010 +0100
5.3 @@ -1653,6 +1653,7 @@
5.4 else
5.5 kk_comprehension [KK.DeclOne ((1, ~1), to_r discr_u)]
5.6 (kk_rel_eq (kk_join (KK.Var (1, ~1)) sel_r) arg_r)
5.7 + |> is_opt_rep (rep_of arg_u) ? to_guard [arg_u] R1
5.8 end) sel_us arg_us
5.9 in fold1 kk_intersect set_rs end
5.10 | BoundRel (x, _, _, _) => KK.Var x
5.11 @@ -1723,10 +1724,8 @@
5.12 map2 (kk_not oo kk_n_ary_function kk)
5.13 (map (unopt_rep o rep_of) func_guard_us) func_guard_rs
5.14 in
5.15 - if null guard_fs then
5.16 - r
5.17 - else
5.18 - kk_rel_if (fold1 kk_or guard_fs) (empty_rel_for_rep R) r
5.19 + if null guard_fs then r
5.20 + else kk_rel_if (fold1 kk_or guard_fs) (empty_rel_for_rep R) r
5.21 end
5.22 (* rep -> rep -> KK.rel_expr -> int -> KK.rel_expr *)
5.23 and to_project new_R old_R r j0 =