1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Mar 11 09:09:51 2010 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Thu Mar 11 10:13:24 2010 +0100
     1.3 @@ -150,12 +150,12 @@
     1.4  \textbf{begin}
     1.5  \postw
     1.6  
     1.7 -The results presented here were obtained using the JNI version of MiniSat and
     1.8 -with multithreading disabled to reduce nondeterminism and a time limit of
     1.9 -15~seconds (instead of 30~seconds). This was done by adding the line
    1.10 +The results presented here were obtained using the JNI (Java Native Interface)
    1.11 +version of MiniSat and with multithreading disabled to reduce nondeterminism.
    1.12 +This was done by adding the line
    1.13  
    1.14  \prew
    1.15 -\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1, \,\textit{timeout} = 15$\,s$]
    1.16 +\textbf{nitpick\_params} [\textit{sat\_solver}~= \textit{MiniSat\_JNI}, \,\textit{max\_threads}~= 1]
    1.17  \postw
    1.18  
    1.19  after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
    1.20 @@ -2203,11 +2203,9 @@
    1.21  Specifies the maximum number of potential counterexamples to display. Setting
    1.22  this option to 0 speeds up the search for a genuine counterexample. This option
    1.23  is implicitly set to 0 for automatic runs. If you set this option to a value
    1.24 -greater than 1, you will need an incremental SAT solver: For efficiency, it is
    1.25 -recommended to install the JNI version of MiniSat and set \textit{sat\_solver} =
    1.26 -\textit{MiniSat\_JNI}. Also be aware that many of the counterexamples may look
    1.27 -identical, unless the \textit{show\_all} (\S\ref{output-format}) option is
    1.28 -enabled.
    1.29 +greater than 1, you will need an incremental SAT solver, such as
    1.30 +\textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that many of
    1.31 +the counterexamples may be identical.
    1.32  
    1.33  \nopagebreak
    1.34  {\small See also \textit{check\_potential} (\S\ref{authentication}) and
    1.35 @@ -2215,11 +2213,9 @@
    1.36  
    1.37  \opdefault{max\_genuine}{int}{$\mathbf{1}$}
    1.38  Specifies the maximum number of genuine counterexamples to display. If you set
    1.39 -this option to a value greater than 1, you will need an incremental SAT solver:
    1.40 -For efficiency, it is recommended to install the JNI version of MiniSat and set
    1.41 -\textit{sat\_solver} = \textit{MiniSat\_JNI}. Also be aware that many of the
    1.42 -counterexamples may look identical, unless the \textit{show\_all}
    1.43 -(\S\ref{output-format}) option is enabled.
    1.44 +this option to a value greater than 1, you will need an incremental SAT solver,
    1.45 +such as \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that
    1.46 +many of the counterexamples may be identical.
    1.47  
    1.48  \nopagebreak
    1.49  {\small See also \textit{check\_genuine} (\S\ref{authentication}) and
    1.50 @@ -2330,13 +2326,11 @@
    1.51  and 2.0 beta (2007-07-21).
    1.52  
    1.53  \item[$\bullet$] \textbf{\textit{MiniSat\_JNI}}: The JNI (Java Native Interface)
    1.54 -version of MiniSat is bundled in \texttt{nativesolver.\allowbreak tgz}, which
    1.55 -you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
    1.56 +version of MiniSat is bundled with Kodkodi and is precompiled for the major
    1.57 +platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
    1.58 +which you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
    1.59  version of MiniSat, the JNI version can be used incrementally.
    1.60  
    1.61 -%%% No longer true:
    1.62 -%%% "It is bundled with Kodkodi and requires no further installation or
    1.63 -%%% configuration steps. Alternatively,"
    1.64  \item[$\bullet$] \textbf{\textit{PicoSAT}}: PicoSAT is an efficient solver
    1.65  written in C. You can install a standard version of
    1.66  PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
    1.67 @@ -2355,8 +2349,9 @@
    1.68  versions 2004-05-13, 2004-11-15, and 2007-03-12.
    1.69  
    1.70  \item[$\bullet$] \textbf{\textit{zChaff\_JNI}}: The JNI version of zChaff is
    1.71 -bundled in \texttt{native\-solver.\allowbreak tgz}, which you will find on
    1.72 -Kodkod's web site \cite{kodkod-2009}.
    1.73 +bundled with Kodkodi and is precompiled for the major
    1.74 +platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
    1.75 +which you will find on Kodkod's web site \cite{kodkod-2009}.
    1.76  
    1.77  \item[$\bullet$] \textbf{\textit{RSat}}: RSat is an efficient solver written in
    1.78  \cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the

     2.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Mar 11 09:09:51 2010 +0100
     2.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Mar 11 10:13:24 2010 +0100
     2.3 @@ -13,7 +13,7 @@
     2.4  
     2.5  chapter {* 3. First Steps *}
     2.6  
     2.7 -nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 15 s]
     2.8 +nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1]
     2.9  
    2.10  subsection {* 3.1. Propositional Logic *}
    2.11  
    2.12 @@ -136,11 +136,11 @@
    2.13  "even n \<Longrightarrow> even (Suc (Suc n))"
    2.14  
    2.15  lemma "\<exists>n. even n \<and> even (Suc n)"
    2.16 -nitpick [card nat = 100, unary_ints, verbose, expect = potential]
    2.17 +nitpick [card nat = 50, unary_ints, verbose, expect = potential]
    2.18  oops
    2.19  
    2.20 -lemma "\<exists>n \<le> 99. even n \<and> even (Suc n)"
    2.21 -nitpick [card nat = 100, unary_ints, verbose, expect = genuine]
    2.22 +lemma "\<exists>n \<le> 49. even n \<and> even (Suc n)"
    2.23 +nitpick [card nat = 50, unary_ints, verbose, expect = genuine]
    2.24  oops
    2.25  
    2.26  inductive even' where
    2.27 @@ -243,7 +243,7 @@
    2.28  "subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
    2.29  
    2.30  lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
    2.31 -nitpick [card = 1\<midarrow>6, expect = none]
    2.32 +nitpick [card = 1\<midarrow>5, expect = none]
    2.33  sorry
    2.34  
    2.35  subsection {* 3.11. Scope Monotonicity *}
    2.36 @@ -317,7 +317,7 @@
    2.37    case Leaf thus ?case by simp
    2.38  next
    2.39    case (Branch t u) thus ?case
    2.40 -  nitpick [non_std, show_all]
    2.41 +  nitpick [non_std, card = 1\<midarrow>5, expect = none]
    2.42    by auto
    2.43  qed
    2.44  
    2.45 @@ -365,7 +365,7 @@
    2.46  
    2.47  theorem S\<^isub>3_sound:
    2.48  "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    2.49 -nitpick
    2.50 +nitpick [card = 1\<midarrow>6, expect = none]
    2.51  sorry
    2.52  
    2.53  theorem S\<^isub>3_complete:
    2.54 @@ -384,19 +384,19 @@
    2.55  
    2.56  theorem S\<^isub>4_sound:
    2.57  "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    2.58 -nitpick
    2.59 +nitpick [card = 1\<midarrow>6, expect = none]
    2.60  sorry
    2.61  
    2.62  theorem S\<^isub>4_complete:
    2.63  "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
    2.64 -nitpick
    2.65 +nitpick [card = 1\<midarrow>6, expect = none]
    2.66  sorry
    2.67  
    2.68  theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
    2.69  "w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    2.70  "w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
    2.71  "w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
    2.72 -nitpick
    2.73 +nitpick [card = 1\<midarrow>6, expect = none]
    2.74  sorry
    2.75  
    2.76  subsection {* 4.2. AA Trees *}
    2.77 @@ -450,13 +450,13 @@
    2.78  theorem dataset_skew_split:
    2.79  "dataset (skew t) = dataset t"
    2.80  "dataset (split t) = dataset t"
    2.81 -nitpick
    2.82 +nitpick [card = 1\<midarrow>6, expect = none]
    2.83  sorry
    2.84  
    2.85  theorem wf_skew_split:
    2.86  "wf t \<Longrightarrow> skew t = t"
    2.87  "wf t \<Longrightarrow> split t = t"
    2.88 -nitpick
    2.89 +nitpick [card = 1\<midarrow>6, expect = none]
    2.90  sorry
    2.91  
    2.92  primrec insort\<^isub>1 where
    2.93 @@ -480,11 +480,11 @@
    2.94                         (if x > y then insort\<^isub>2 u x else u))"
    2.95  
    2.96  theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
    2.97 -nitpick
    2.98 +nitpick [card = 1\<midarrow>6, expect = none]
    2.99  sorry
   2.100  
   2.101  theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
   2.102 -nitpick
   2.103 +nitpick [card = 1\<midarrow>6, expect = none]
   2.104  sorry
   2.105  
   2.106  end