42 (*certificates*) |
42 (*certificates*) |
43 val fixed_certificates: bool Config.T |
43 val fixed_certificates: bool Config.T |
44 val select_certificates: string -> Context.generic -> Context.generic |
44 val select_certificates: string -> Context.generic -> Context.generic |
45 |
45 |
46 (*solvers*) |
46 (*solvers*) |
47 type solver = bool -> Proof.context -> (int * thm) list -> int list * thm |
47 type solver = bool option -> Proof.context -> (int * thm) list -> |
|
48 int list * thm |
48 val add_solver: solver_config -> theory -> theory |
49 val add_solver: solver_config -> theory -> theory |
49 val set_solver_options: string -> string -> Context.generic -> |
50 val set_solver_options: string -> string -> Context.generic -> |
50 Context.generic |
51 Context.generic |
51 val all_solver_names_of: Context.generic -> string list |
52 val all_solver_names_of: Context.generic -> string list |
52 val solver_name_of: Context.generic -> string |
53 val solver_name_of: Context.generic -> string |
160 let val local_solver = getenv env_var |
161 let val local_solver = getenv env_var |
161 in if local_solver <> "" then SOME local_solver else NONE end |
162 in if local_solver <> "" then SOME local_solver else NONE end |
162 |
163 |
163 local |
164 local |
164 |
165 |
165 fun choose (force_remote, env_var, is_remote, name) = |
166 fun choose (rm, env_var, is_remote, name) = |
166 let |
167 let |
|
168 val force_local = (case rm of SOME false => true | _ => false) |
|
169 val force_remote = (case rm of SOME true => true | _ => false) |
167 val lsolver = get_local_solver env_var |
170 val lsolver = get_local_solver env_var |
168 val remote_url = getenv "REMOTE_SMT_URL" |
171 val remote_url = getenv "REMOTE_SMT_URL" |
|
172 val trace = if is_some rm then K () else tracing |
169 in |
173 in |
170 if not force_remote andalso is_some lsolver |
174 if not force_remote andalso is_some lsolver |
171 then |
175 then |
172 (tracing ("Invoking local SMT solver " ^ quote (the lsolver) ^ " ..."); |
176 (trace ("Invoking local SMT solver " ^ quote (the lsolver) ^ " ..."); |
173 [the lsolver]) |
177 [the lsolver]) |
174 else if is_remote |
178 else if not force_local andalso is_remote |
175 then |
179 then |
176 (tracing ("Invoking remote SMT solver " ^ quote name ^ " at " ^ |
180 (trace ("Invoking remote SMT solver " ^ quote name ^ " at " ^ |
177 quote remote_url ^ " ..."); |
181 quote remote_url ^ " ..."); |
178 [getenv "REMOTE_SMT", name]) |
182 [getenv "REMOTE_SMT", name]) |
179 else if force_remote |
183 else if force_remote |
180 then error ("SMT solver " ^ quote name ^ " is not remotely available.") |
184 then error ("The SMT solver " ^ quote name ^ " is not remotely available.") |
181 else error ("Undefined Isabelle environment variable: " ^ quote env_var) |
185 else error ("The SMT solver " ^ quote name ^ " has not been found " ^ |
|
186 "on this computer. Please set the Isabelle environment variable " ^ |
|
187 quote env_var ^ ".") |
182 end |
188 end |
183 |
189 |
184 fun make_cmd solver args problem_path proof_path = space_implode " " ( |
190 fun make_cmd solver args problem_path proof_path = space_implode " " ( |
185 map File.shell_quote (solver @ args) @ |
191 map File.shell_quote (solver @ args) @ |
186 [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path]) |
192 [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path]) |
268 tracing (Pretty.string_of (Pretty.big_list "SMT used facts:" |
274 tracing (Pretty.string_of (Pretty.big_list "SMT used facts:" |
269 (map (Display.pretty_thm ctxt) thms))) |
275 (map (Display.pretty_thm ctxt) thms))) |
270 else () |
276 else () |
271 end |
277 end |
272 |
278 |
273 fun gen_solver name info force_remote ctxt irules = |
279 fun gen_solver name info rm ctxt irules = |
274 let |
280 let |
275 val {env_var, is_remote, options, more_options, interface, reconstruct} = |
281 val {env_var, is_remote, options, more_options, interface, reconstruct} = |
276 info |
282 info |
277 val {extra_norm, translate} = interface |
283 val {extra_norm, translate} = interface |
278 val (with_datatypes, translate') = |
284 val (with_datatypes, translate') = |
279 set_has_datatypes (Config.get ctxt datatypes) translate |
285 set_has_datatypes (Config.get ctxt datatypes) translate |
280 val cmd = (force_remote, env_var, is_remote, name) |
286 val cmd = (rm, env_var, is_remote, name) |
281 in |
287 in |
282 (irules, ctxt) |
288 (irules, ctxt) |
283 |-> SMT_Normalize.normalize extra_norm with_datatypes |
289 |-> SMT_Normalize.normalize extra_norm with_datatypes |
284 |-> invoke translate' name cmd more_options options |
290 |-> invoke translate' name cmd more_options options |
285 |-> reconstruct |
291 |-> reconstruct |
399 val has_topsort = Term.exists_type (Term.exists_subtype (fn |
405 val has_topsort = Term.exists_type (Term.exists_subtype (fn |
400 TFree (_, []) => true |
406 TFree (_, []) => true |
401 | TVar (_, []) => true |
407 | TVar (_, []) => true |
402 | _ => false)) |
408 | _ => false)) |
403 |
409 |
404 fun smt_solver force_remote ctxt irules = |
410 fun smt_solver rm ctxt irules = |
405 (* without this test, we would run into problems when atomizing the rules: *) |
411 (* without this test, we would run into problems when atomizing the rules: *) |
406 if exists (has_topsort o Thm.prop_of o snd) irules |
412 if exists (has_topsort o Thm.prop_of o snd) irules |
407 then raise SMT (Other_Failure "proof state contains the universal sort {}") |
413 then raise SMT (Other_Failure "proof state contains the universal sort {}") |
408 else solver_of (Context.Proof ctxt) force_remote ctxt irules |
414 else solver_of (Context.Proof ctxt) rm ctxt irules |
409 |
415 |
410 fun smt_filter rm time_limit st xrules i = |
416 fun smt_filter run_remote time_limit st xrules i = |
411 let |
417 let |
412 val {context, facts, goal} = Proof.goal st |
418 val {context, facts, goal} = Proof.goal st |
413 val ctxt = |
419 val ctxt = |
414 context |
420 context |
415 |> Config.put timeout (Time.toSeconds time_limit) |
421 |> Config.put timeout (Time.toSeconds time_limit) |
418 val cprop = |
424 val cprop = |
419 Thm.cprem_of goal i |
425 Thm.cprem_of goal i |
420 |> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt |
426 |> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt |
421 |> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg |
427 |> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg |
422 val irs = map (pair ~1) (Thm.assume cprop :: facts) |
428 val irs = map (pair ~1) (Thm.assume cprop :: facts) |
|
429 val rm = SOME run_remote |
423 in |
430 in |
424 split_list xrules |
431 split_list xrules |
425 ||> distinct (op =) o fst o smt_solver rm ctxt o append irs o map_index I |
432 ||> distinct (op =) o fst o smt_solver rm ctxt o append irs o map_index I |
426 |-> map_filter o try o nth |
433 |-> map_filter o try o nth |
427 |> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs= ~1}) |
434 |> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs= ~1}) |
436 fun smt_tac' pass_exns ctxt rules = |
443 fun smt_tac' pass_exns ctxt rules = |
437 CONVERSION (SMT_Normalize.atomize_conv ctxt) |
444 CONVERSION (SMT_Normalize.atomize_conv ctxt) |
438 THEN' Tactic.rtac @{thm ccontr} |
445 THEN' Tactic.rtac @{thm ccontr} |
439 THEN' SUBPROOF (fn {context=cx, prems, ...} => |
446 THEN' SUBPROOF (fn {context=cx, prems, ...} => |
440 let |
447 let |
441 fun solve () = snd (smt_solver false cx (map (pair ~1) (rules @ prems))) |
448 fun solve () = snd (smt_solver NONE cx (map (pair ~1) (rules @ prems))) |
442 val trace = trace_msg cx (prefix "SMT: " o string_of_failure cx) |
449 val trace = trace_msg cx (prefix "SMT: " o string_of_failure cx) |
443 in |
450 in |
444 (if pass_exns then SOME (solve ()) |
451 (if pass_exns then SOME (solve ()) |
445 else (SOME (solve ()) handle SMT fail => (trace fail; NONE))) |
452 else (SOME (solve ()) handle SMT fail => (trace fail; NONE))) |
446 |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac) |
453 |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac) |