# HG changeset patch # User blanchet # Date 1258451917 -3600 # Node ID c6ca64ac5353f93242eb6f82327fbbe9ccca3d4a # Parent e588744f14dabc1bb5944513cc344df7949e7840# Parent 385381514eedc74e430fa6ead6a366ff8a607441 merged diff -r e588744f14da -r c6ca64ac5353 doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Mon Nov 16 21:57:16 2009 +0100 +++ b/doc-src/Nitpick/nitpick.tex Tue Nov 17 10:58:37 2009 +0100 @@ -2019,9 +2019,11 @@ 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. It is bundled with Kodkodi and requires no further installation or -configuration steps. Alternatively, you can install a standard version of +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 available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi. @@ -2078,11 +2080,11 @@ \url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}. \item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to -\textit{smart}, Nitpick selects the first solver among MiniSatJNI, MiniSat, -PicoSAT, zChaffJNI, zChaff, RSat, BerkMin, BerkMinAlloy, and Jerusat that is -recognized by Isabelle. If none is found, it falls back on SAT4J, which should -always be available. If \textit{verbose} is enabled, Nitpick displays which SAT -solver was chosen. +\textit{smart}, Nitpick selects the first solver among MiniSat, +PicoSAT, zChaff, RSat, BerkMin, BerkMinAlloy, Jerusat, MiniSatJNI, and zChaffJNI +that is recognized by Isabelle. If none is found, it falls back on SAT4J, which +should always be available. If \textit{verbose} (\S\ref{output-format}) is +enabled, Nitpick displays which SAT solver was chosen. \end{enum} \fussy @@ -2469,8 +2471,8 @@ \item[$\bullet$] Local definitions are not supported and result in an error. -\item[$\bullet$] All constants and types whose names start with -\textit{Nitpick}{.} are reserved for internal use. +%\item[$\bullet$] All constants and types whose names start with +%\textit{Nitpick}{.} are reserved for internal use. \end{enum} \let\em=\sl diff -r e588744f14da -r c6ca64ac5353 src/HOL/Tools/Nitpick/kodkod_sat.ML --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Mon Nov 16 21:57:16 2009 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Tue Nov 17 10:58:37 2009 +0100 @@ -28,11 +28,9 @@ (* (string * sat_solver_info) list *) val static_list = - [("MiniSatJNI", Internal (JNI, Incremental, ["MiniSat"])), - ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "", + [("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "", "UNSAT")), ("PicoSAT", External (ToStdout, "PICOSAT_HOME", "picosat", [])), - ("zChaffJNI", Internal (JNI, Batch, ["zChaff"])), ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [], "Instance Satisfiable", "", "Instance Unsatisfiable")), @@ -44,6 +42,8 @@ "solution =", "UNSATISFIABLE !!")), ("BerkMinAlloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])), ("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])), + ("MiniSatJNI", Internal (JNI, Incremental, ["MiniSat"])), + ("zChaffJNI", Internal (JNI, Batch, ["zChaff"])), ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])), ("SAT4JLight", Internal (Java, Incremental, ["LightSAT4J"])), ("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"], diff -r e588744f14da -r c6ca64ac5353 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Nov 16 21:57:16 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Nov 17 10:58:37 2009 +0100 @@ -784,8 +784,8 @@ let (* typ -> ctype *) val ctype_for = fresh_ctype_for_type cdata - (* term -> accumulator -> accumulator *) - val do_term = snd oo consider_term cdata + (* term -> accumulator -> ctype * accumulator *) + val do_term = consider_term cdata (* sign -> term -> accumulator -> accumulator *) fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum | do_formula sn t (accum as (gamma as {bounds, frees, consts}, cset)) = @@ -810,8 +810,11 @@ (* term -> term -> accumulator *) fun do_equals t1 t2 = case sn of - Pos => do_term t accum - | Neg => fold do_term [t1, t2] accum + Pos => do_term t accum |> snd + | Neg => let + val (C1, accum) = do_term t1 accum + val (C2, accum) = do_term t2 accum + in accum ||> add_ctypes_equal C1 C2 end in case t of Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) => @@ -839,10 +842,10 @@ | @{const "op -->"} $ t1 $ t2 => accum |> do_contra_formula t1 |> do_co_formula t2 | Const (@{const_name If}, _) $ t1 $ t2 $ t3 => - accum |> do_term t1 |> fold do_co_formula [t2, t3] + accum |> do_term t1 |> snd |> fold do_co_formula [t2, t3] | Const (@{const_name Let}, _) $ t1 $ t2 => do_co_formula (betapply (t2, t1)) accum - | _ => do_term t accum + | _ => do_term t accum |> snd end |> tap (fn _ => print_g ("\ \ " ^ Syntax.string_of_term ctxt t ^ @@ -873,7 +876,7 @@ I else let - (* term -> accumulator -> accumulator *) + (* term -> accumulator -> ctype * accumulator *) val do_term = consider_term cdata (* typ -> term -> accumulator -> accumulator *) fun do_all abs_T body_t accum =