# HG changeset patch
# User wenzelm
# Date 1635614581 -7200
# Node ID 85d8d9eeb4e180ece1e78b6f4220dadb677cdc30
# Parent  f831b6e589dc69e525d6cc450a9320dc39ed04c4
discontinued pointless check of kodkodi_version, it is implicit in the bundled component;

diff -r f831b6e589dc -r 85d8d9eeb4e1 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Sat Oct 30 17:10:10 2021 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sat Oct 30 19:23:01 2021 +0200
@@ -125,8 +125,6 @@
      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
@@ -312,11 +310,6 @@
    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)
-
 
 (** Auxiliary functions on Kodkod problems **)
 
diff -r f831b6e589dc -r 85d8d9eeb4e1 src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Sat Oct 30 17:10:10 2021 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Sat Oct 30 19:23:01 2021 +0200
@@ -18,7 +18,7 @@
 open Kodkod
 
 datatype sink = ToStdout | ToFile
-datatype availability = Java | JNI of int list
+datatype availability = Java | JNI
 datatype mode = Batch | Incremental
 
 datatype sat_solver_info =
@@ -30,11 +30,11 @@
 val berkmin_exec = getenv "BERKMIN_EXE"
 
 val static_list =
-  [("Lingeling_JNI", Internal (JNI [1, 5], Batch, ["Lingeling"])),
+  [("Lingeling_JNI", Internal (JNI, Batch, ["Lingeling"])),
    ("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
-   ("CryptoMiniSat_JNI", Internal (JNI [1, 5], Batch, ["CryptoMiniSat"])),
+   ("CryptoMiniSat_JNI", Internal (JNI, Batch, ["CryptoMiniSat"])),
    ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "", "UNSAT")),
-   ("MiniSat_JNI", Internal (JNI [], Incremental, ["MiniSat"])),
+   ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
    ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
                           "Instance Satisfiable", "",
                           "Instance Unsatisfiable")),
@@ -62,16 +62,13 @@
 
 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 from_version, mode, ss)) =
-    if (incremental andalso mode = Batch) orelse
-       is_less (dict_ord int_ord (kodkodi_version (), from_version))
-    then NONE
+  | dynamic_entry_for_info incremental (name, Internal (JNI, mode, ss)) =
+    if incremental andalso mode = Batch then NONE
     else if exists File.is_dir (Path.split (getenv "KODKODI_JAVA_LIBRARY_PATH"))
     then SOME (name, K ss) else NONE
   | dynamic_entry_for_info false (name, External (home, exec, args)) =
     dynamic_entry_for_external name ToStdout home exec args []
-  | dynamic_entry_for_info false
-        (name, ExternalV2 (dev, home, exec, args, m1, m2, m3)) =
+  | dynamic_entry_for_info false (name, ExternalV2 (dev, home, exec, args, m1, m2, m3)) =
     dynamic_entry_for_external name dev home exec args [m1, m2, m3]
   | dynamic_entry_for_info true _ = NONE