# HG changeset patch
# User blanchet
# Date 1668077374 -3600
# Node ID 7956b822f2392bc1b0cd670d9e03daa20cdb1a3f
# Parent  1cebb0ca6d86902dd570b17e6836c1c329263ef9
use timeout with MiniSat

diff -r 1cebb0ca6d86 -r 7956b822f239 src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Thu Nov 10 08:13:28 2022 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Thu Nov 10 11:49:34 2022 +0100
@@ -9,7 +9,7 @@
 sig
   val configured_sat_solvers : bool -> string list
   val smart_sat_solver_name : bool -> string
-  val sat_solver_spec : string -> string * string list
+  val sat_solver_spec : Time.time -> string -> string * string list
 end;
 
 structure Kodkod_SAT : KODKOD_SAT =
@@ -24,24 +24,25 @@
 datatype sat_solver_info =
   Internal of availability * mode * string list |
   External of string * string * string list |
-  ExternalV2 of sink * string * string * string list * string * string * string
+  ExternalV2 of sink * string * string * string * string * string * (Time.time -> string list)
+
+fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 999) div 1000)
 
 (* for compatibility with "SAT_Solver" *)
 val berkmin_exec = getenv "BERKMIN_EXE"
 
 val static_list =
   [("CryptoMiniSat", External ("CRYPTOMINISAT_HOME", "cryptominisat", [])),
-   ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "", "UNSAT")),
-   ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
-                          "Instance Satisfiable", "",
-                          "Instance Unsatisfiable")),
-   ("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat", ["-s"],
-                        "s SATISFIABLE", "v ", "s UNSATISFIABLE")),
+   ("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", "SAT", "", "UNSAT",
+      fn timeout => ["-cpu-lim=" ^ string_of_int (to_secs 1 timeout)])),
+   ("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff",
+      "Instance Satisfiable", "", "Instance Unsatisfiable", K [])),
+   ("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat",
+      "s SATISFIABLE", "v ", "s UNSATISFIABLE", K ["-s"])),
    ("Riss3g", External ("RISS3G_HOME", "riss3g", [])),
    ("BerkMin", ExternalV2 (ToStdout, "BERKMIN_HOME",
-                           if berkmin_exec = "" then "BerkMin561"
-                           else berkmin_exec, [], "Satisfiable          !!",
-                           "solution =", "UNSATISFIABLE          !!")),
+      if berkmin_exec = "" then "BerkMin561" else berkmin_exec, "Satisfiable          !!",
+      "solution =", "UNSATISFIABLE          !!", K [])),
    ("BerkMin_Alloy", External ("BERKMINALLOY_HOME", "berkmin", [])),
    ("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
    ("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"])),
@@ -60,27 +61,27 @@
       end
   in if getenv home = "" then NONE else SOME (name, make_args) end
 
-fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
+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)) =
+  | 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_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_external name dev home exec args [m1, m2, m3]
-  | dynamic_entry_for_info true _ = NONE
+  | dynamic_entry_for_info timeout false (name, ExternalV2 (dev, home, exec, m1, m2, m3, args)) =
+    dynamic_entry_for_external name dev home exec (args timeout) [m1, m2, m3]
+  | dynamic_entry_for_info _ true _ = NONE
 
-fun dynamic_list incremental =
-  map_filter (dynamic_entry_for_info incremental) static_list
+fun dynamic_list timeout incremental =
+  map_filter (dynamic_entry_for_info timeout incremental) static_list
 
-val configured_sat_solvers = map fst o dynamic_list
-val smart_sat_solver_name = fst o hd o dynamic_list
+val configured_sat_solvers = map fst o dynamic_list Time.zeroTime
+val smart_sat_solver_name = fst o hd o dynamic_list Time.zeroTime
 
-fun sat_solver_spec name =
+fun sat_solver_spec timeout name =
   let
-    val dyns = dynamic_list false
+    val dyns = dynamic_list timeout false
     fun enum_solvers solvers =
       commas (distinct (op =) (map (quote o fst) solvers))
   in
diff -r 1cebb0ca6d86 -r 7956b822f239 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Nov 10 08:13:28 2022 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Nov 10 11:49:34 2022 +0100
@@ -517,7 +517,8 @@
         val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
                       multiline_string_for_scope scope
         val kodkod_sat_solver =
-          Kodkod_SAT.sat_solver_spec actual_sat_solver |> snd
+          Kodkod_SAT.sat_solver_spec (deadline - Time.now ()) actual_sat_solver
+          |> snd
         val bit_width = if bits = 0 then 16 else bits + 1
         val delay =
           if unsound then
@@ -629,8 +630,6 @@
           got_all_user_axioms andalso none_true wfs andalso
           sound_finitizes andalso total_consts <> SOME true andalso
           codatatypes_ok
-        fun assms_prop () =
-          Logic.mk_conjunction_list (neg_t :: def_assm_ts @ nondef_assm_ts)
       in
         (pprint_a (Pretty.chunks
              [Pretty.blk (0,