equal
deleted
inserted
replaced
63 in f x end |
63 in f x end |
64 |
64 |
65 fun run ctxt name mk_cmd input = |
65 fun run ctxt name mk_cmd input = |
66 (case SMT_Config.certificates_of ctxt of |
66 (case SMT_Config.certificates_of ctxt of |
67 NONE => |
67 NONE => |
68 if Config.get ctxt SMT_Config.debug_files = "" then |
68 if not (SMT_Config.is_available ctxt name) then |
|
69 error ("The SMT solver " ^ quote name ^ " is not installed.") |
|
70 else if Config.get ctxt SMT_Config.debug_files = "" then |
69 trace_and ctxt ("Invoking SMT solver " ^ quote name ^ " ...") |
71 trace_and ctxt ("Invoking SMT solver " ^ quote name ^ " ...") |
70 (Cache_IO.run mk_cmd) input |
72 (Cache_IO.run mk_cmd) input |
71 else |
73 else |
72 let |
74 let |
73 val base_path = Path.explode (Config.get ctxt SMT_Config.debug_files) |
75 val base_path = Path.explode (Config.get ctxt SMT_Config.debug_files) |
235 fun gen_preprocess ctxt iwthms = SMT_Normalize.normalize iwthms ctxt |
237 fun gen_preprocess ctxt iwthms = SMT_Normalize.normalize iwthms ctxt |
236 |
238 |
237 fun gen_apply (ithms, ctxt) = |
239 fun gen_apply (ithms, ctxt) = |
238 let val (name, {command, reconstruct, ...}) = name_and_info_of ctxt |
240 let val (name, {command, reconstruct, ...}) = name_and_info_of ctxt |
239 in |
241 in |
240 if not (SMT_Config.is_available ctxt name) then |
242 (ithms, ctxt) |
241 error ("The SMT solver " ^ quote name ^ " is not installed.") |
243 |-> invoke name command |
242 else |
244 |> reconstruct ctxt |
243 (ithms, ctxt) |
245 |>> distinct (op =) |
244 |-> invoke name command |
|
245 |> reconstruct ctxt |
|
246 |>> distinct (op =) |
|
247 end |
246 end |
248 |
247 |
249 fun apply_solver ctxt = gen_apply o gen_preprocess ctxt |
248 fun apply_solver ctxt = gen_apply o gen_preprocess ctxt |
250 |
249 |
251 val default_max_relevant = #default_max_relevant oo get_info |
250 val default_max_relevant = #default_max_relevant oo get_info |