--- a/doc-src/Nitpick/nitpick.tex Thu Mar 11 09:09:51 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Thu Mar 11 10:13:24 2010 +0100
@@ -150,12 +150,12 @@
\textbf{begin}
\postw
-The results presented here were obtained using the JNI version of MiniSat and
-with multithreading disabled to reduce nondeterminism and a time limit of
-15~seconds (instead of 30~seconds). This was done by adding the line
+The results presented here were obtained using the JNI (Java Native Interface)
+version of MiniSat and with multithreading disabled to reduce nondeterminism.
+This was done by adding the line
\prew
-\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1, \,\textit{timeout} = 15$\,s$]
+\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1]
\postw
after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
@@ -2203,11 +2203,9 @@
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
-greater than 1, you will need an incremental SAT solver: For efficiency, it is
-recommended to install the JNI version of MiniSat and set \textit{sat\_solver} =
-\textit{MiniSat\_JNI}. Also be aware that many of the counterexamples may look
-identical, unless the \textit{show\_all} (\S\ref{output-format}) option is
-enabled.
+greater than 1, you will need an incremental SAT solver, such as
+\textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that many of
+the counterexamples may be identical.
\nopagebreak
{\small See also \textit{check\_potential} (\S\ref{authentication}) and
@@ -2215,11 +2213,9 @@
\opdefault{max\_genuine}{int}{$\mathbf{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:
-For efficiency, it is recommended to install the JNI version of MiniSat and set
-\textit{sat\_solver} = \textit{MiniSat\_JNI}. Also be aware that many of the
-counterexamples may look identical, unless the \textit{show\_all}
-(\S\ref{output-format}) option is enabled.
+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
+many of the counterexamples may be identical.
\nopagebreak
{\small See also \textit{check\_genuine} (\S\ref{authentication}) and
@@ -2330,13 +2326,11 @@
and 2.0 beta (2007-07-21).
\item[$\bullet$] \textbf{\textit{MiniSat\_JNI}}: The JNI (Java Native Interface)
-version of MiniSat is bundled in \texttt{nativesolver.\allowbreak tgz}, which
-you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
+version of MiniSat is bundled with Kodkodi and is precompiled for the major
+platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
+which you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
version of MiniSat, the JNI version can be used incrementally.
-%%% No longer true:
-%%% "It is bundled with Kodkodi and requires no further installation or
-%%% configuration steps. Alternatively,"
\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
@@ -2355,8 +2349,9 @@
versions 2004-05-13, 2004-11-15, and 2007-03-12.
\item[$\bullet$] \textbf{\textit{zChaff\_JNI}}: The JNI version of zChaff is
-bundled in \texttt{native\-solver.\allowbreak tgz}, which you will find on
-Kodkod's web site \cite{kodkod-2009}.
+bundled with Kodkodi and is precompiled for the major
+platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
+which you will find on Kodkod's web site \cite{kodkod-2009}.
\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
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Thu Mar 11 09:09:51 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Thu Mar 11 10:13:24 2010 +0100
@@ -13,7 +13,7 @@
chapter {* 3. First Steps *}
-nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 15 s]
+nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1]
subsection {* 3.1. Propositional Logic *}
@@ -136,11 +136,11 @@
"even n \<Longrightarrow> even (Suc (Suc n))"
lemma "\<exists>n. even n \<and> even (Suc n)"
-nitpick [card nat = 100, unary_ints, verbose, expect = potential]
+nitpick [card nat = 50, unary_ints, verbose, expect = potential]
oops
-lemma "\<exists>n \<le> 99. even n \<and> even (Suc n)"
-nitpick [card nat = 100, unary_ints, verbose, expect = genuine]
+lemma "\<exists>n \<le> 49. even n \<and> even (Suc n)"
+nitpick [card nat = 50, unary_ints, verbose, expect = genuine]
oops
inductive even' where
@@ -243,7 +243,7 @@
"subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
-nitpick [card = 1\<midarrow>6, expect = none]
+nitpick [card = 1\<midarrow>5, expect = none]
sorry
subsection {* 3.11. Scope Monotonicity *}
@@ -317,7 +317,7 @@
case Leaf thus ?case by simp
next
case (Branch t u) thus ?case
- nitpick [non_std, show_all]
+ nitpick [non_std, card = 1\<midarrow>5, expect = none]
by auto
qed
@@ -365,7 +365,7 @@
theorem S\<^isub>3_sound:
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-nitpick
+nitpick [card = 1\<midarrow>6, expect = none]
sorry
theorem S\<^isub>3_complete:
@@ -384,19 +384,19 @@
theorem S\<^isub>4_sound:
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-nitpick
+nitpick [card = 1\<midarrow>6, expect = none]
sorry
theorem S\<^isub>4_complete:
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
-nitpick
+nitpick [card = 1\<midarrow>6, expect = none]
sorry
theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
"w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
"w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
"w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
-nitpick
+nitpick [card = 1\<midarrow>6, expect = none]
sorry
subsection {* 4.2. AA Trees *}
@@ -450,13 +450,13 @@
theorem dataset_skew_split:
"dataset (skew t) = dataset t"
"dataset (split t) = dataset t"
-nitpick
+nitpick [card = 1\<midarrow>6, expect = none]
sorry
theorem wf_skew_split:
"wf t \<Longrightarrow> skew t = t"
"wf t \<Longrightarrow> split t = t"
-nitpick
+nitpick [card = 1\<midarrow>6, expect = none]
sorry
primrec insort\<^isub>1 where
@@ -480,11 +480,11 @@
(if x > y then insort\<^isub>2 u x else u))"
theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
-nitpick
+nitpick [card = 1\<midarrow>6, expect = none]
sorry
theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
-nitpick
+nitpick [card = 1\<midarrow>6, expect = none]
sorry
end