# HG changeset patch
# User blanchet
# Date 1355309767 -3600
# Node ID 1b3eb579e08b481e7a416e01e9015305ed7309d3
# Parent  9486641e691bf6f149b21d62907c9502c0bb2cfa
use modern SAT solvers with modern Kodkod versions

diff -r 9486641e691b -r 1b3eb579e08b src/Doc/Nitpick/document/root.tex
--- 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}
diff -r 9486641e691b -r 1b3eb579e08b src/HOL/Tools/Nitpick/kodkod.ML
--- 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 **)
 
diff -r 9486641e691b -r 1b3eb579e08b src/HOL/Tools/Nitpick/kodkod_sat.ML
--- 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