equal
deleted
inserted
replaced
65 type prover = |
65 type prover = |
66 params -> ((string * string list) list -> string -> minimize_command) |
66 params -> ((string * string list) list -> string -> minimize_command) |
67 -> prover_problem -> prover_result |
67 -> prover_problem -> prover_result |
68 |
68 |
69 val SledgehammerN : string |
69 val SledgehammerN : string |
|
70 val smtN : string |
70 val overlord_file_location_of_prover : string -> string * string |
71 val overlord_file_location_of_prover : string -> string * string |
71 val proof_banner : mode -> string -> string |
72 val proof_banner : mode -> string -> string |
72 val extract_proof_method : params -> proof_method -> string * (string * string list) list |
73 val extract_proof_method : params -> proof_method -> string * (string * string list) list |
73 val is_proof_method : string -> bool |
74 val is_proof_method : string -> bool |
74 val is_atp : theory -> string -> bool |
75 val is_atp : theory -> string -> bool |
107 datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize |
108 datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize |
108 |
109 |
109 (* Identifier that distinguishes Sledgehammer from other tools that could use |
110 (* Identifier that distinguishes Sledgehammer from other tools that could use |
110 "Async_Manager". *) |
111 "Async_Manager". *) |
111 val SledgehammerN = "Sledgehammer" |
112 val SledgehammerN = "Sledgehammer" |
|
113 |
|
114 val smtN = "smt" |
112 |
115 |
113 val proof_method_names = [metisN, smtN] |
116 val proof_method_names = [metisN, smtN] |
114 val is_proof_method = member (op =) proof_method_names |
117 val is_proof_method = member (op =) proof_method_names |
115 |
118 |
116 val is_atp = member (op =) o supported_atps |
119 val is_atp = member (op =) o supported_atps |