88 val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))] |
88 val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))] |
89 val mesh_facts = mesh_facts slack_max_facts mess |
89 val mesh_facts = mesh_facts slack_max_facts mess |
90 val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts |
90 val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts |
91 (* adapted from "mirabelle_sledgehammer.ML" *) |
91 (* adapted from "mirabelle_sledgehammer.ML" *) |
92 fun set_file_name heading (SOME dir) = |
92 fun set_file_name heading (SOME dir) = |
93 Config.put Sledgehammer_Provers.dest_dir dir |
93 let val prob_prefix = "goal_" ^ string_of_int j ^ "_" ^ heading in |
94 #> Config.put Sledgehammer_Provers.problem_prefix |
94 Config.put Sledgehammer_Provers.dest_dir dir |
95 ("goal_" ^ string_of_int j ^ "_" ^ heading ^ "__") |
95 #> Config.put Sledgehammer_Provers.problem_prefix |
96 #> Config.put SMT_Config.debug_files |
96 (prob_prefix ^ "__") |
97 (dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_" |
97 #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix) |
98 ^ serial_string ()) |
98 end |
99 | set_file_name _ NONE = I |
99 | set_file_name _ NONE = I |
100 fun prove ok heading get facts = |
100 fun prove ok heading get facts = |
101 let |
101 let |
102 val facts = |
102 val facts = |
103 facts |> map get |
103 facts |> map get |