1(* Title: HOL/Tools/Sledgehammer/sledgehammer_commands.ML 2 Author: Jasmin Blanchette, TU Muenchen 3 4Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax. 5*) 6 7signature SLEDGEHAMMER_COMMANDS = 8sig 9 type params = Sledgehammer_Prover.params 10 11 val provers : string Unsynchronized.ref 12 val default_params : theory -> (string * string) list -> params 13end; 14 15structure Sledgehammer_Commands : SLEDGEHAMMER_COMMANDS = 16struct 17 18open ATP_Util 19open ATP_Systems 20open ATP_Problem_Generate 21open ATP_Proof 22open ATP_Proof_Reconstruct 23open Sledgehammer_Util 24open Sledgehammer_Fact 25open Sledgehammer_Prover 26open Sledgehammer_Prover_Minimize 27open Sledgehammer_MaSh 28open Sledgehammer 29 30val cvc4N = "cvc4" 31val veritN = "verit" 32val z3N = "z3" 33 34val runN = "run" 35val supported_proversN = "supported_provers" 36val refresh_tptpN = "refresh_tptp" 37 38(** Sledgehammer commands **) 39 40fun add_fact_override ns : fact_override = {add = ns, del = [], only = false} 41fun del_fact_override ns : fact_override = {add = [], del = ns, only = false} 42fun only_fact_override ns : fact_override = {add = ns, del = [], only = true} 43fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) = 44 {add = #add r1 @ #add r2, del = #del r1 @ #del r2, only = #only r1 andalso #only r2} 45fun merge_fact_overrides rs = fold merge_fact_override_pairwise rs (only_fact_override []) 46 47(*** parameters ***) 48 49val provers = Unsynchronized.ref "" 50 51type raw_param = string * string list 52 53val default_default_params = 54 [("debug", "false"), 55 ("verbose", "false"), 56 ("overlord", "false"), 57 ("spy", "false"), 58 ("type_enc", "smart"), 59 ("strict", "false"), 60 ("lam_trans", "smart"), 61 ("uncurried_aliases", "smart"), 62 ("learn", "true"), 63 ("fact_filter", "smart"), 64 ("max_facts", "smart"), 65 ("fact_thresholds", "0.45 0.85"), 66 ("max_mono_iters", "smart"), 67 ("max_new_mono_instances", "smart"), 68 ("isar_proofs", "smart"), 69 ("compress", "smart"), 70 ("try0", "true"), 71 ("smt_proofs", "smart"), 72 ("slice", "true"), 73 ("minimize", "true"), 74 ("preplay_timeout", "1")] 75 76val alias_params = 77 [("prover", ("provers", [])), (* undocumented *) 78 ("dont_preplay", ("preplay_timeout", ["0"])), 79 ("dont_compress", ("compress", ["1"])), 80 ("isar_proof", ("isar_proofs", [])) (* legacy *)] 81val negated_alias_params = 82 [("no_debug", "debug"), 83 ("quiet", "verbose"), 84 ("no_overlord", "overlord"), 85 ("dont_spy", "spy"), 86 ("non_strict", "strict"), 87 ("no_uncurried_aliases", "uncurried_aliases"), 88 ("dont_learn", "learn"), 89 ("no_isar_proofs", "isar_proofs"), 90 ("dont_slice", "slice"), 91 ("dont_minimize", "minimize"), 92 ("dont_try0", "try0"), 93 ("no_smt_proofs", "smt_proofs")] 94 95val property_dependent_params = ["provers", "timeout"] 96 97fun is_known_raw_param s = 98 AList.defined (op =) default_default_params s orelse 99 AList.defined (op =) alias_params s orelse 100 AList.defined (op =) negated_alias_params s orelse 101 member (op =) property_dependent_params s orelse s = "expect" 102 103fun is_prover_list ctxt s = 104 (case space_explode " " s of 105 ss as _ :: _ => forall (is_prover_supported ctxt) ss 106 | _ => false) 107 108fun unalias_raw_param (name, value) = 109 (case AList.lookup (op =) alias_params name of 110 SOME (name', []) => (name', value) 111 | SOME (param' as (name', _)) => 112 if value <> ["false"] then 113 param' 114 else 115 error ("Parameter " ^ quote name ^ " cannot be set to \"false\" (cf. " ^ quote name' ^ ")") 116 | NONE => 117 (case AList.lookup (op =) negated_alias_params name of 118 SOME name' => (name', 119 (case value of 120 ["false"] => ["true"] 121 | ["true"] => ["false"] 122 | [] => ["false"] 123 | _ => value)) 124 | NONE => (name, value))) 125 126val any_type_enc = type_enc_of_string Strict "erased" 127 128(* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts =" 129 can be omitted. For the last four, this is a secret feature. *) 130fun normalize_raw_param ctxt = 131 unalias_raw_param 132 #> (fn (name, value) => 133 if is_known_raw_param name then 134 (name, value) 135 else if null value then 136 if is_prover_list ctxt name then 137 ("provers", [name]) 138 else if can (type_enc_of_string Strict) name then 139 ("type_enc", [name]) 140 else if can (trans_lams_of_string ctxt any_type_enc) name then 141 ("lam_trans", [name]) 142 else if member (op =) fact_filters name then 143 ("fact_filter", [name]) 144 else if is_some (Int.fromString name) then 145 ("max_facts", [name]) 146 else 147 error ("Unknown parameter: " ^ quote name) 148 else 149 error ("Unknown parameter: " ^ quote name)) 150 151(* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are 152 read correctly. *) 153val implode_param = strip_spaces_except_between_idents o space_implode " " 154 155(* FIXME: use "Generic_Data" *) 156structure Data = Theory_Data 157( 158 type T = raw_param list 159 val empty = default_default_params |> map (apsnd single) 160 val extend = I 161 fun merge data : T = AList.merge (op =) (K true) data 162) 163 164fun remotify_prover_if_supported_and_not_already_remote ctxt name = 165 if String.isPrefix remote_prefix name then 166 SOME name 167 else 168 let val remote_name = remote_prefix ^ name in 169 if is_prover_supported ctxt remote_name then SOME remote_name else NONE 170 end 171 172fun remotify_prover_if_not_installed ctxt name = 173 if is_prover_supported ctxt name andalso is_prover_installed ctxt name then SOME name 174 else remotify_prover_if_supported_and_not_already_remote ctxt name 175 176(* The first ATP of the list is used by Auto Sledgehammer. *) 177fun default_provers_param_value mode ctxt = 178 [cvc4N] @ 179 (if is_vampire_noncommercial_license_accepted () = SOME false then [] else [vampireN]) @ 180 [z3N, eN, spassN, veritN] 181 |> map_filter (remotify_prover_if_not_installed ctxt) 182 (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *) 183 |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0)) 184 |> implode_param 185 186fun set_default_raw_param param thy = 187 let val ctxt = Proof_Context.init_global thy in 188 thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param)) 189 end 190 191fun default_raw_params mode thy = 192 let val ctxt = Proof_Context.init_global thy in 193 Data.get thy 194 |> fold (AList.default (op =)) 195 [("provers", [(case !provers of "" => default_provers_param_value mode ctxt | s => s)]), 196 ("timeout", 197 let val timeout = Options.default_int \<^system_option>\<open>sledgehammer_timeout\<close> in 198 [if timeout <= 0 then "none" else string_of_int timeout] 199 end)] 200 end 201 202fun extract_params mode default_params override_params = 203 let 204 val raw_params = rev override_params @ rev default_params 205 val lookup = Option.map implode_param o AList.lookup (op =) raw_params 206 val lookup_string = the_default "" o lookup 207 208 fun general_lookup_bool option default_value name = 209 (case lookup name of 210 SOME s => parse_bool_option option name s 211 | NONE => default_value) 212 val lookup_bool = the o general_lookup_bool false (SOME false) 213 fun lookup_time name = 214 (case lookup name of 215 SOME s => parse_time name s 216 | NONE => Time.zeroTime) 217 fun lookup_int name = 218 (case lookup name of 219 NONE => 0 220 | SOME s => 221 (case Int.fromString s of 222 SOME n => n 223 | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value"))) 224 fun lookup_real name = 225 (case lookup name of 226 NONE => 0.0 227 | SOME s => 228 (case Real.fromString s of 229 SOME n => n 230 | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value"))) 231 fun lookup_real_pair name = 232 (case lookup name of 233 NONE => (0.0, 0.0) 234 | SOME s => 235 (case s |> space_explode " " |> map Real.fromString of 236 [SOME r1, SOME r2] => (r1, r2) 237 | _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floating-point \ 238 \values (e.g., \"0.6 0.95\")"))) 239 fun lookup_option lookup' name = 240 (case lookup name of 241 SOME "smart" => NONE 242 | _ => SOME (lookup' name)) 243 val debug = mode <> Auto_Try andalso lookup_bool "debug" 244 val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") 245 val overlord = lookup_bool "overlord" 246 val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" 247 val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd 248 val type_enc = 249 if mode = Auto_Try then 250 NONE 251 else 252 (case lookup_string "type_enc" of 253 "smart" => NONE 254 | s => (type_enc_of_string Strict s; SOME s)) 255 val strict = mode = Auto_Try orelse lookup_bool "strict" 256 val lam_trans = lookup_option lookup_string "lam_trans" 257 val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" 258 val learn = lookup_bool "learn" 259 val fact_filter = 260 lookup_option lookup_string "fact_filter" 261 |> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf) 262 val max_facts = lookup_option lookup_int "max_facts" 263 val fact_thresholds = lookup_real_pair "fact_thresholds" 264 val max_mono_iters = lookup_option lookup_int "max_mono_iters" 265 val max_new_mono_instances = 266 lookup_option lookup_int "max_new_mono_instances" 267 val isar_proofs = lookup_option lookup_bool "isar_proofs" 268 val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress") 269 val try0 = lookup_bool "try0" 270 val smt_proofs = lookup_option lookup_bool "smt_proofs" 271 val slice = mode <> Auto_Try andalso lookup_bool "slice" 272 val minimize = lookup_bool "minimize" 273 val timeout = lookup_time "timeout" 274 val preplay_timeout = lookup_time "preplay_timeout" 275 val expect = lookup_string "expect" 276 in 277 {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, 278 type_enc = type_enc, strict = strict, lam_trans = lam_trans, 279 uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, 280 max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, 281 max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, 282 compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize, 283 timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} 284 end 285 286fun get_params mode = extract_params mode o default_raw_params mode 287fun default_params thy = get_params Normal thy o map (apsnd single) 288 289val silence_state = 290 Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false) 291 292(* Sledgehammer the given subgoal *) 293 294val default_learn_prover_timeout = 2.0 295 296fun hammer_away override_params writeln_result subcommand opt_i fact_override state0 = 297 let 298 (* We generally want chained facts to be picked up by the relevance filter, because it can then 299 give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs, 300 verbose output, machine learning). However, if the fact is available by no other means (not 301 even backticks), as "f" would be in "using f unfolding f'" after unfolding, we have no choice 302 but to insert it into the state as an additional hypothesis. 303 *) 304 val {facts = chained0, ...} = Proof.goal state0 305 val (inserts, keep_chained) = 306 if null chained0 orelse #only fact_override then 307 (chained0, []) 308 else 309 let val ctxt0 = Proof.context_of state0 in 310 List.partition (is_useful_unnamed_local_fact ctxt0) chained0 311 end 312 val state = state0 313 |> (if null inserts then I else Proof.refine_insert inserts #> Proof.set_facts keep_chained) 314 |> silence_state 315 316 val thy = Proof.theory_of state 317 val ctxt = Proof.context_of state 318 319 val override_params = override_params |> map (normalize_raw_param ctxt) 320 in 321 if subcommand = runN then 322 let val i = the_default 1 opt_i in 323 ignore (run_sledgehammer 324 (get_params Normal thy override_params) Normal writeln_result i fact_override state) 325 end 326 else if subcommand = supported_proversN then 327 supported_provers ctxt 328 else if subcommand = unlearnN then 329 mash_unlearn ctxt 330 else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse 331 subcommand = relearn_isarN orelse subcommand = relearn_proverN then 332 (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt 333 else (); 334 mash_learn ctxt 335 (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *) 336 (get_params Normal thy 337 ([("timeout", [string_of_real default_learn_prover_timeout]), 338 ("slice", ["false"])] @ 339 override_params @ 340 [("preplay_timeout", ["0"])])) 341 fact_override (#facts (Proof.goal state)) 342 (subcommand = learn_proverN orelse subcommand = relearn_proverN)) 343 else if subcommand = refresh_tptpN then 344 refresh_systems_on_tptp () 345 else 346 error ("Unknown subcommand: " ^ quote subcommand) 347 end 348 349fun string_of_raw_param (key, values) = 350 key ^ (case implode_param values of "" => "" | value => " = " ^ value) 351 352val parse_query_bang = \<^keyword>\<open>?\<close> || \<^keyword>\<open>!\<close> || \<^keyword>\<open>!!\<close> 353val parse_key = Scan.repeat1 (Parse.embedded || parse_query_bang) >> implode_param 354val parse_value = Scan.repeat1 (Parse.name || Parse.float_number || parse_query_bang) 355val parse_param = parse_key -- Scan.optional (\<^keyword>\<open>=\<close> |-- parse_value) [] 356val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] 357val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm) 358val parse_fact_override_chunk = 359 (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override) 360 || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override) 361 || (parse_fact_refs >> only_fact_override) 362val parse_fact_override = 363 Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides)) 364 no_fact_override 365 366val _ = 367 Outer_Syntax.command \<^command_keyword>\<open>sledgehammer\<close> 368 "search for first-order proof using automatic theorem provers" 369 (Scan.optional Parse.name runN -- parse_params 370 -- parse_fact_override -- Scan.option Parse.nat >> 371 (fn (((subcommand, params), fact_override), opt_i) => 372 Toplevel.keep_proof 373 (hammer_away params NONE subcommand opt_i fact_override o Toplevel.proof_of))) 374val _ = 375 Outer_Syntax.command \<^command_keyword>\<open>sledgehammer_params\<close> 376 "set and display the default parameters for Sledgehammer" 377 (parse_params >> (fn params => 378 Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => 379 writeln ("Default parameters for Sledgehammer:\n" ^ 380 (case rev (default_raw_params Normal thy) of 381 [] => "none" 382 | params => params |> map string_of_raw_param |> sort_strings |> cat_lines)))))) 383 384fun try_sledgehammer auto state = 385 let 386 val thy = Proof.theory_of state 387 val mode = if auto then Auto_Try else Try 388 val i = 1 389 in 390 run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (silence_state state) 391 end 392 393val _ = Try.tool_setup (sledgehammerN, (40, \<^system_option>\<open>auto_sledgehammer\<close>, try_sledgehammer)) 394 395val _ = 396 Query_Operation.register {name = sledgehammerN, pri = 0} 397 (fn {state = st, args, writeln_result, ...} => 398 (case try Toplevel.proof_of st of 399 SOME state => 400 let 401 val [provers_arg, isar_proofs_arg, try0_arg] = args 402 val override_params = 403 ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @ 404 [("isar_proofs", [if isar_proofs_arg = "true" then "true" else "smart"]), 405 ("try0", [try0_arg]), 406 ("debug", ["false"]), 407 ("verbose", ["false"]), 408 ("overlord", ["false"])]); 409 in hammer_away override_params (SOME writeln_result) runN NONE no_fact_override state end 410 | NONE => error "Unknown proof context")) 411 412end; 413