--- a/src/Doc/Nitpick/document/root.tex Wed Dec 12 11:18:06 2012 +0100
+++ b/src/Doc/Nitpick/document/root.tex Wed Dec 12 11:56:07 2012 +0100
@@ -169,10 +169,10 @@
\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
file with the absolute path to Kodkodi. For example, if the
\texttt{components} file does not exist yet and you extracted Kodkodi to
-\texttt{/usr/local/kodkodi-1.5.1}, create it with the single line
+\texttt{/usr/local/kodkodi-1.5.2}, create it with the single line
\prew
-\texttt{/usr/local/kodkodi-1.5.1}
+\texttt{/usr/local/kodkodi-1.5.2}
\postw
(including an invisible newline character) in it.
@@ -204,7 +204,7 @@
after the \textbf{begin} keyword. The JNI version of MiniSat is bundled with
Kodkodi and is precompiled for Linux, Mac~OS~X, and Windows (Cygwin). Other SAT
-solvers can also be installed, as explained in \S\ref{optimizations}. If you
+solvers can also be used, as explained in \S\ref{optimizations}. If you
have already configured SAT solvers in Isabelle (e.g., for Refute), these will
also be available to Nitpick.
@@ -2347,6 +2347,11 @@
\begin{enum}
+\item[\labelitemi] \textbf{\textit{Lingeling\_JNI}:}
+Lingeling is an efficient solver written in C. The JNI (Java Native Interface)
+version of Lingeling is bundled with Kodkodi and is precompiled for Linux and
+Mac~OS~X. It is also available from the Kodkod web site \cite{kodkod-2009}.
+
\item[\labelitemi] \textbf{\textit{CryptoMiniSat}:} CryptoMiniSat is the winner of
the 2010 SAT Race. To use CryptoMiniSat, set the environment variable
\texttt{CRYPTO\-MINISAT\_}\discretionary{}{}{}\texttt{HOME} to the directory that contains the \texttt{crypto\-minisat}
@@ -2363,11 +2368,6 @@
for Linux and Mac~OS~X. It is also available from the Kodkod web site
\cite{kodkod-2009}.
-\item[\labelitemi] \textbf{\textit{Lingeling\_JNI}:}
-Lingeling is an efficient solver written in C. The JNI (Java Native Interface)
-version of Lingeling is bundled with Kodkodi and is precompiled for Linux and
-Mac~OS~X. It is also available from the Kodkod web site \cite{kodkod-2009}.
-
\item[\labelitemi] \textbf{\textit{MiniSat}:} MiniSat is an efficient solver
written in \cpp{}. To use MiniSat, set the environment variable
\texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
--- a/src/HOL/Tools/Nitpick/kodkod.ML Wed Dec 12 11:18:06 2012 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Wed Dec 12 11:56:07 2012 +0100
@@ -125,6 +125,8 @@
rel_expr_func: rel_expr -> 'a -> 'a,
int_expr_func: int_expr -> 'a -> 'a}
+ val kodkodi_version : unit -> int list
+
val fold_formula : 'a fold_expr_funcs -> formula -> 'a -> 'a
val fold_rel_expr : 'a fold_expr_funcs -> rel_expr -> 'a -> 'a
val fold_int_expr : 'a fold_expr_funcs -> int_expr -> 'a -> 'a
@@ -318,12 +320,13 @@
rel_expr_func: rel_expr -> 'a -> 'a,
int_expr_func: int_expr -> 'a -> 'a}
+fun kodkodi_version () =
+ getenv "KODKODI_VERSION"
+ |> space_explode "."
+ |> map (the_default 0 o Int.fromString)
+
fun is_kodkodi_too_old () =
- case getenv "KODKODI_VERSION" of
- "" => true
- | s => dict_ord int_ord (s |> space_explode "."
- |> map (the_default 0 o Int.fromString),
- [1, 2, 14]) = LESS
+ dict_ord int_ord (kodkodi_version (), [1, 2, 14]) = LESS
(** Auxiliary functions on Kodkod problems **)
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Wed Dec 12 11:18:06 2012 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Wed Dec 12 11:56:07 2012 +0100
@@ -18,7 +18,9 @@
open Kodkod
datatype sink = ToStdout | ToFile
-datatype availability = Java | JNI
+datatype availability =
+ Java |
+ JNI of int list
datatype mode = Batch | Incremental
datatype sat_solver_info =
@@ -31,12 +33,12 @@
(* (string * sat_solver_info) list *)
val static_list =
- [("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
+ [("Lingeling_JNI", Internal (JNI [1, 5], Batch, ["Lingeling"])),
+ ("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
+ ("CryptoMiniSat_JNI", Internal (JNI [1, 5], Batch, ["CryptoMiniSat"])),
+ ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
"UNSAT")),
- ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
- ("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
- ("CryptoMiniSat_JNI", Internal (JNI, Batch, ["CryptoMiniSat"])),
- ("Lingeling_JNI", Internal (JNI, Batch, ["Lingeling"])),
+ ("MiniSat_JNI", Internal (JNI [], Incremental, ["MiniSat"])),
("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
"Instance Satisfiable", "",
"Instance Unsatisfiable")),
@@ -74,8 +76,10 @@
end)
fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
if incremental andalso mode = Batch then NONE else SOME (name, K ss)
- | dynamic_entry_for_info incremental (name, Internal (JNI, mode, ss)) =
- if incremental andalso mode = Batch then
+ | dynamic_entry_for_info incremental
+ (name, Internal (JNI from_version, mode, ss)) =
+ if (incremental andalso mode = Batch) orelse
+ dict_ord int_ord (kodkodi_version (), from_version) = LESS then
NONE
else
let