# HG changeset patch # User blanchet # Date 1268298804 -3600 # Node ID 58acd48904bc3d09df825f312ca6d17b3ee8f22d # Parent 267e15230a318936a207af6b3548402abb219e53 made "Manual_Nits" tests more robust diff -r 267e15230a31 -r 58acd48904bc doc-src/Nitpick/nitpick.tex --- 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 diff -r 267e15230a31 -r 58acd48904bc src/HOL/Nitpick_Examples/Manual_Nits.thy --- 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 \ even (Suc (Suc n))" lemma "\n. even n \ even (Suc n)" -nitpick [card nat = 100, unary_ints, verbose, expect = potential] +nitpick [card nat = 50, unary_ints, verbose, expect = potential] oops -lemma "\n \ 99. even n \ even (Suc n)" -nitpick [card nat = 100, unary_ints, verbose, expect = genuine] +lemma "\n \ 49. even n \ even (Suc n)" +nitpick [card nat = 50, unary_ints, verbose, expect = genuine] oops inductive even' where @@ -243,7 +243,7 @@ "subst\<^isub>2 \ (App t u) = App (subst\<^isub>2 \ t) (subst\<^isub>2 \ u)" lemma "\ loose t 0 \ subst\<^isub>2 \ t = t" -nitpick [card = 1\6, expect = none] +nitpick [card = 1\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\5, expect = none] by auto qed @@ -365,7 +365,7 @@ theorem S\<^isub>3_sound: "w \ S\<^isub>3 \ length [x \ w. x = a] = length [x \ w. x = b]" -nitpick +nitpick [card = 1\6, expect = none] sorry theorem S\<^isub>3_complete: @@ -384,19 +384,19 @@ theorem S\<^isub>4_sound: "w \ S\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" -nitpick +nitpick [card = 1\6, expect = none] sorry theorem S\<^isub>4_complete: "length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>4" -nitpick +nitpick [card = 1\6, expect = none] sorry theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete: "w \ S\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b]" "w \ A\<^isub>4 \ length [x \ w. x = a] = length [x \ w. x = b] + 1" "w \ B\<^isub>4 \ length [x \ w. x = b] = length [x \ w. x = a] + 1" -nitpick +nitpick [card = 1\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\6, expect = none] sorry theorem wf_skew_split: "wf t \ skew t = t" "wf t \ split t = t" -nitpick +nitpick [card = 1\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 \ wf (insort\<^isub>2 t x)" -nitpick +nitpick [card = 1\6, expect = none] sorry theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \ dataset t" -nitpick +nitpick [card = 1\6, expect = none] sorry end