equal
deleted
inserted
replaced
13 type type_enc = ATP_Problem_Generate.type_enc |
13 type type_enc = ATP_Problem_Generate.type_enc |
14 type reconstructor = ATP_Proof_Reconstruct.reconstructor |
14 type reconstructor = ATP_Proof_Reconstruct.reconstructor |
15 type play = ATP_Proof_Reconstruct.play |
15 type play = ATP_Proof_Reconstruct.play |
16 type minimize_command = ATP_Proof_Reconstruct.minimize_command |
16 type minimize_command = ATP_Proof_Reconstruct.minimize_command |
17 |
17 |
18 datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize |
18 datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize |
19 |
19 |
20 type params = |
20 type params = |
21 {debug : bool, |
21 {debug : bool, |
22 verbose : bool, |
22 verbose : bool, |
23 overlord : bool, |
23 overlord : bool, |
148 open Sledgehammer_Util |
148 open Sledgehammer_Util |
149 |
149 |
150 |
150 |
151 (** The Sledgehammer **) |
151 (** The Sledgehammer **) |
152 |
152 |
153 datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize |
153 datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize |
154 |
154 |
155 (* Identifier that distinguishes Sledgehammer from other tools that could use |
155 (* Identifier that distinguishes Sledgehammer from other tools that could use |
156 "Async_Manager". *) |
156 "Async_Manager". *) |
157 val SledgehammerN = "Sledgehammer" |
157 val SledgehammerN = "Sledgehammer" |
158 |
158 |
619 #> Config.put Monomorph.keep_partial_instances false |
619 #> Config.put Monomorph.keep_partial_instances false |
620 |
620 |
621 fun suffix_for_mode Auto_Try = "_auto_try" |
621 fun suffix_for_mode Auto_Try = "_auto_try" |
622 | suffix_for_mode Try = "_try" |
622 | suffix_for_mode Try = "_try" |
623 | suffix_for_mode Normal = "" |
623 | suffix_for_mode Normal = "" |
|
624 | suffix_for_mode MaSh = "_mash" |
624 | suffix_for_mode Auto_Minimize = "_auto_min" |
625 | suffix_for_mode Auto_Minimize = "_auto_min" |
625 | suffix_for_mode Minimize = "_min" |
626 | suffix_for_mode Minimize = "_min" |
626 |
627 |
627 (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on |
628 (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on |
628 Linux appears to be the only ATP that does not honor its time limit. *) |
629 Linux appears to be the only ATP that does not honor its time limit. *) |