equal
deleted
inserted
replaced
6 Central manager component for ATP threads. |
6 Central manager component for ATP threads. |
7 *) |
7 *) |
8 |
8 |
9 signature ATP_MANAGER = |
9 signature ATP_MANAGER = |
10 sig |
10 sig |
11 type cnf_thm = Clausifier.cnf_thm |
|
12 type name_pool = Metis_Clauses.name_pool |
11 type name_pool = Metis_Clauses.name_pool |
13 type relevance_override = Sledgehammer_Fact_Filter.relevance_override |
12 type relevance_override = Sledgehammer_Fact_Filter.relevance_override |
14 type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command |
13 type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command |
15 type params = |
14 type params = |
16 {debug: bool, |
15 {debug: bool, |
29 minimize_timeout: Time.time} |
28 minimize_timeout: Time.time} |
30 type problem = |
29 type problem = |
31 {subgoal: int, |
30 {subgoal: int, |
32 goal: Proof.context * (thm list * thm), |
31 goal: Proof.context * (thm list * thm), |
33 relevance_override: relevance_override, |
32 relevance_override: relevance_override, |
34 axiom_clauses: cnf_thm list option, |
33 axiom_clauses: ((string * int) * thm) list option, |
35 filtered_clauses: cnf_thm list option} |
34 filtered_clauses: ((string * int) * thm) list option} |
36 datatype failure = |
35 datatype failure = |
37 Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass | |
36 Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass | |
38 MalformedInput | MalformedOutput | UnknownError |
37 MalformedInput | MalformedOutput | UnknownError |
39 type prover_result = |
38 type prover_result = |
40 {outcome: failure option, |
39 {outcome: failure option, |
44 atp_run_time_in_msecs: int, |
43 atp_run_time_in_msecs: int, |
45 output: string, |
44 output: string, |
46 proof: string, |
45 proof: string, |
47 internal_thm_names: string Vector.vector, |
46 internal_thm_names: string Vector.vector, |
48 conjecture_shape: int list list, |
47 conjecture_shape: int list list, |
49 filtered_clauses: cnf_thm list} |
48 filtered_clauses: ((string * int) * thm) list} |
50 type prover = |
49 type prover = |
51 params -> minimize_command -> Time.time -> problem -> prover_result |
50 params -> minimize_command -> Time.time -> problem -> prover_result |
52 |
51 |
53 val kill_atps: unit -> unit |
52 val kill_atps: unit -> unit |
54 val running_atps: unit -> unit |
53 val running_atps: unit -> unit |
96 |
95 |
97 type problem = |
96 type problem = |
98 {subgoal: int, |
97 {subgoal: int, |
99 goal: Proof.context * (thm list * thm), |
98 goal: Proof.context * (thm list * thm), |
100 relevance_override: relevance_override, |
99 relevance_override: relevance_override, |
101 axiom_clauses: cnf_thm list option, |
100 axiom_clauses: ((string * int) * thm) list option, |
102 filtered_clauses: cnf_thm list option} |
101 filtered_clauses: ((string * int) * thm) list option} |
103 |
102 |
104 datatype failure = |
103 datatype failure = |
105 Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass | |
104 Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass | |
106 MalformedInput | MalformedOutput | UnknownError |
105 MalformedInput | MalformedOutput | UnknownError |
107 |
106 |
113 atp_run_time_in_msecs: int, |
112 atp_run_time_in_msecs: int, |
114 output: string, |
113 output: string, |
115 proof: string, |
114 proof: string, |
116 internal_thm_names: string Vector.vector, |
115 internal_thm_names: string Vector.vector, |
117 conjecture_shape: int list list, |
116 conjecture_shape: int list list, |
118 filtered_clauses: cnf_thm list} |
117 filtered_clauses: ((string * int) * thm) list} |
119 |
118 |
120 type prover = |
119 type prover = |
121 params -> minimize_command -> Time.time -> problem -> prover_result |
120 params -> minimize_command -> Time.time -> problem -> prover_result |
122 |
121 |
123 (* named provers *) |
122 (* named provers *) |