equal
deleted
inserted
replaced
118 |
118 |
119 fun suffix_of_mode Auto_Try = "_try" |
119 fun suffix_of_mode Auto_Try = "_try" |
120 | suffix_of_mode Try = "_try" |
120 | suffix_of_mode Try = "_try" |
121 | suffix_of_mode Normal = "" |
121 | suffix_of_mode Normal = "" |
122 | suffix_of_mode MaSh = "" |
122 | suffix_of_mode MaSh = "" |
123 | suffix_of_mode Auto_Minimize = "_min" |
|
124 | suffix_of_mode Minimize = "_min" |
123 | suffix_of_mode Minimize = "_min" |
125 |
124 |
126 (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on Linux appears to be |
125 (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on Linux appears to be |
127 the only ATP that does not honor its time limit. *) |
126 the only ATP that does not honor its time limit. *) |
128 val atp_timeout_slack = seconds 1.0 |
127 val atp_timeout_slack = seconds 1.0 |
152 val (dest_dir, problem_prefix) = |
151 val (dest_dir, problem_prefix) = |
153 if overlord then overlord_file_location_of_prover name |
152 if overlord then overlord_file_location_of_prover name |
154 else (Config.get ctxt atp_dest_dir, Config.get ctxt atp_problem_prefix) |
153 else (Config.get ctxt atp_dest_dir, Config.get ctxt atp_problem_prefix) |
155 val problem_file_name = |
154 val problem_file_name = |
156 Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ |
155 Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ |
157 suffix_of_mode mode ^ "_" ^ string_of_int subgoal) |
156 suffix_of_mode mode ^ "_" ^ string_of_int subgoal) |
158 val prob_path = |
157 val prob_path = |
159 if dest_dir = "" then |
158 if dest_dir = "" then |
160 File.tmp_path problem_file_name |
159 File.tmp_path problem_file_name |
161 else if File.exists (Path.explode dest_dir) then |
160 else if File.exists (Path.explode dest_dir) then |
162 Path.append (Path.explode dest_dir) problem_file_name |
161 Path.append (Path.explode dest_dir) problem_file_name |