# HG changeset patch # User blanchet # Date 1268843025 -3600 # Node ID 234eaa50835940d196651f37866b40de4dbf624b # Parent b1a7ad9ab647b35a45dfb57c962a19987d77f5da added one-entry cache around Kodkod invocation diff -r b1a7ad9ab647 -r 234eaa508359 src/HOL/Tools/Nitpick/HISTORY --- a/src/HOL/Tools/Nitpick/HISTORY Wed Mar 17 16:27:11 2010 +0100 +++ b/src/HOL/Tools/Nitpick/HISTORY Wed Mar 17 17:23:45 2010 +0100 @@ -14,6 +14,7 @@ * Fixed soundness bugs related to "destroy_constrs" optimization and record getters * Fixed soundness bug related to higher-order constructors + * Added cache to speed up repeated Kodkod invocations on the same problems * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light" diff -r b1a7ad9ab647 -r 234eaa508359 src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Wed Mar 17 16:27:11 2010 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Wed Mar 17 17:23:45 2010 +0100 @@ -169,7 +169,7 @@ val max_arity : int -> int val arity_of_rel_expr : rel_expr -> int val is_problem_trivially_false : problem -> bool - val problems_equivalent : problem -> problem -> bool + val problems_equivalent : problem * problem -> bool val solve_any_problem : bool -> Time.time option -> int -> int -> problem list -> outcome end; @@ -500,19 +500,28 @@ fun is_problem_trivially_false ({formula = False, ...} : problem) = true | is_problem_trivially_false _ = false -(* string -> bool *) -val is_relevant_setting = not o member (op =) ["solver", "delay"] +(* string -> string list *) +val chop_solver = take 2 o space_explode "," -(* problem -> problem -> bool *) -fun problems_equivalent (p1 : problem) (p2 : problem) = +(* setting list * setting list -> bool *) +fun settings_equivalent ([], []) = true + | settings_equivalent ((key1, value1) :: settings1, + (key2, value2) :: settings2) = + key1 = key2 andalso + (value1 = value2 orelse key1 = "delay" orelse + (key1 = "solver" andalso chop_solver value1 = chop_solver value2)) andalso + settings_equivalent (settings1, settings2) + | settings_equivalent _ = false + +(* problem * problem -> bool *) +fun problems_equivalent (p1 : problem, p2 : problem) = #univ_card p1 = #univ_card p2 andalso #formula p1 = #formula p2 andalso #bounds p1 = #bounds p2 andalso #expr_assigns p1 = #expr_assigns p2 andalso #tuple_assigns p1 = #tuple_assigns p2 andalso #int_bounds p1 = #int_bounds p2 andalso - filter (is_relevant_setting o fst) (#settings p1) - = filter (is_relevant_setting o fst) (#settings p2) + settings_equivalent (#settings p1, #settings p2) (** Serialization of problem **) @@ -1005,10 +1014,6 @@ |>> rev ||> rev) handle IO.Io _ => (true, ([], [])) | OS.SysErr _ => (true, ([], [])) -(* The fudge term below is to account for Kodkodi's slow start-up time, which - is partly due to the JVM and partly due to the ML "bash" function. *) -val fudge_ms = 250 - (** Main Kodkod entry point **) val created_temp_dir = Unsynchronized.ref false @@ -1024,8 +1029,20 @@ else (created_temp_dir := true; File.mkdir (Path.explode dir)) in (serial_string (), dir) end +(* The fudge term below is to account for Kodkodi's slow start-up time, which + is partly due to the JVM and partly due to the ML "bash" function. *) +val fudge_ms = 250 + +(* Time.time option -> int *) +fun milliseconds_until_deadline deadline = + case deadline of + NONE => ~1 + | SOME time => + Int.max (0, Time.toMilliseconds (Time.- (time, Time.now ())) - fudge_ms) + (* bool -> Time.time option -> int -> int -> problem list -> outcome *) -fun solve_any_problem overlord deadline max_threads max_solutions problems = +fun uncached_solve_any_problem overlord deadline max_threads max_solutions + problems = let val j = find_index (curry (op =) True o #formula) problems val indexed_problems = if j >= 0 then @@ -1061,12 +1078,7 @@ else List.app (K () o try File.rm) [in_path, out_path, err_path] in let - val ms = - case deadline of - NONE => ~1 - | SOME time => - Int.max (0, Time.toMilliseconds (Time.- (time, Time.now ())) - - fudge_ms) + val ms = milliseconds_until_deadline deadline val outcome = let val code = @@ -1135,4 +1147,35 @@ end end +val cached_outcome = + Synchronized.var "Kodkod.cached_outcome" + (NONE : ((int * problem list) * outcome) option) + +(* bool -> Time.time option -> int -> int -> problem list -> outcome *) +fun solve_any_problem overlord deadline max_threads max_solutions problems = + let + (* unit -> outcome *) + fun do_solve () = uncached_solve_any_problem overlord deadline max_threads + max_solutions problems + in + if overlord then + do_solve () + else + case AList.lookup (fn ((max1, ps1), (max2, ps2)) => + max1 = max2 andalso length ps1 = length ps2 andalso + forall problems_equivalent (ps1 ~~ ps2)) + (the_list (Synchronized.value cached_outcome)) + (max_solutions, problems) of + SOME outcome => outcome + | NONE => + let val outcome = do_solve () in + (case outcome of + Normal (ps, js, "") => + Synchronized.change cached_outcome + (K (SOME ((max_solutions, problems), outcome))) + | _ => ()); + outcome + end + end + end; diff -r b1a7ad9ab647 -r 234eaa508359 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Mar 17 16:27:11 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Mar 17 17:23:45 2010 +0100 @@ -777,8 +777,8 @@ |> filter (fn j => j >= 0 andalso scopes_equivalent - (#scope (snd (nth problems j))) - (#scope (snd (nth problems (j + 1))))) + (#scope (snd (nth problems j)), + #scope (snd (nth problems (j + 1))))) val bye_js = sort_distinct int_ord (map fst sat_ps @ unsat_js @ co_js) val problems = @@ -862,8 +862,7 @@ SOME problem => (problems |> (null problems orelse - not (KK.problems_equivalent (fst problem) - (fst (hd problems)))) + not (KK.problems_equivalent (fst problem, fst (hd problems)))) ? cons problem, donno) | NONE => (problems, donno + 1)) val (problems, donno) = @@ -904,7 +903,7 @@ (* rich_problem list -> scope -> int *) fun scope_count (problems : rich_problem list) scope = - length (filter (scopes_equivalent scope o #scope o snd) problems) + length (filter (curry scopes_equivalent scope o #scope o snd) problems) (* string -> string *) fun excipit did_so_and_so = let diff -r b1a7ad9ab647 -r 234eaa508359 src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Mar 17 16:27:11 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Mar 17 17:23:45 2010 +0100 @@ -46,7 +46,7 @@ val spec_of_type : scope -> typ -> int * int val pretties_for_scope : scope -> bool -> Pretty.T list val multiline_string_for_scope : scope -> string - val scopes_equivalent : scope -> scope -> bool + val scopes_equivalent : scope * scope -> bool val scope_less_eq : scope -> scope -> bool val all_scopes : hol_context -> bool -> int -> (typ option * int list) list @@ -213,8 +213,8 @@ | lines => space_implode "\n" lines end -(* scope -> scope -> bool *) -fun scopes_equivalent (s1 : scope) (s2 : scope) = +(* scope * scope -> bool *) +fun scopes_equivalent (s1 : scope, s2 : scope) = #datatypes s1 = #datatypes s2 andalso #card_assigns s1 = #card_assigns s2 fun scope_less_eq (s1 : scope) (s2 : scope) = (s1, s2) |> pairself (map snd o #card_assigns) |> op ~~ |> forall (op <=)