--- 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
--- 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"],
--- 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 ("\<Gamma> \<turnstile> " ^
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 =