12 val external_prover:int -> |
12 val external_prover:int -> |
13 ((int -> Path.T) -> Proof.context * Thm.thm list * Thm.thm -> string list * ResHolClause.axiom_name Vector.vector list) -> |
13 ((int -> Path.T) -> Proof.context * Thm.thm list * Thm.thm -> string list * ResHolClause.axiom_name Vector.vector list) -> |
14 string -> |
14 string -> |
15 (string * int -> bool) -> |
15 (string * int -> bool) -> |
16 (string * string vector * Proof.context * Thm.thm * int -> string) -> |
16 (string * string vector * Proof.context * Thm.thm * int -> string) -> |
17 Toplevel.state -> Thread.thread * string |
17 Proof.state -> Thread.thread * string |
18 (* settings for writing problemfiles *) |
18 (* settings for writing problemfiles *) |
19 val destdir: string ref |
19 val destdir: string ref |
20 val problem_name: string ref |
20 val problem_name: string ref |
21 (* provers as functions returning threads *) |
21 (* provers as functions returning threads *) |
22 val tptp_prover_filter_opts_full: int -> bool -> bool -> string -> Toplevel.state -> (Thread.thread * string) |
22 val tptp_prover_filter_opts_full: int -> bool -> bool -> string -> Proof.state -> (Thread.thread * string) |
23 val tptp_prover_filter_opts: int -> bool -> string -> Toplevel.state -> (Thread.thread * string) |
23 val tptp_prover_filter_opts: int -> bool -> string -> Proof.state -> (Thread.thread * string) |
24 val full_prover_filter_opts: int -> bool -> string -> Toplevel.state -> (Thread.thread * string) |
24 val full_prover_filter_opts: int -> bool -> string -> Proof.state -> (Thread.thread * string) |
25 val tptp_prover: string -> Toplevel.state -> (Thread.thread * string) |
25 val tptp_prover: string -> Proof.state -> (Thread.thread * string) |
26 val full_prover: string -> Toplevel.state -> (Thread.thread * string) val spass_filter_opts: int -> bool -> Toplevel.state -> (Thread.thread * string) |
26 val full_prover: string -> Proof.state -> (Thread.thread * string) |
27 val eprover_filter_opts: int -> bool -> Toplevel.state -> (Thread.thread * string) |
27 val spass_filter_opts: int -> bool -> Proof.state -> (Thread.thread * string) |
28 val eprover_filter_opts_full: int -> bool -> Toplevel.state -> (Thread.thread * string) |
28 val eprover_filter_opts: int -> bool -> Proof.state -> (Thread.thread * string) |
29 val vampire_filter_opts: int -> bool -> Toplevel.state -> (Thread.thread * string) |
29 val eprover_filter_opts_full: int -> bool -> Proof.state -> (Thread.thread * string) |
30 val vampire_filter_opts_full: int -> bool -> Toplevel.state -> (Thread.thread * string) |
30 val vampire_filter_opts: int -> bool -> Proof.state -> (Thread.thread * string) |
31 val spass: Toplevel.state -> (Thread.thread * string) |
31 val vampire_filter_opts_full: int -> bool -> Proof.state -> (Thread.thread * string) |
32 val eprover: Toplevel.state -> (Thread.thread * string) |
32 val spass: Proof.state -> (Thread.thread * string) |
33 val eprover_full: Toplevel.state -> (Thread.thread * string) |
33 val eprover: Proof.state -> (Thread.thread * string) |
34 val vampire: Toplevel.state -> (Thread.thread * string) |
34 val eprover_full: Proof.state -> (Thread.thread * string) |
35 val vampire_full: Toplevel.state -> (Thread.thread * string) |
35 val vampire: Proof.state -> (Thread.thread * string) |
36 val setup: theory -> theory |
36 val vampire_full: Proof.state -> (Thread.thread * string) |
37 end; |
37 end; |
38 |
38 |
39 structure AtpThread : ATP_THREAD = |
39 structure AtpThread : ATP_THREAD = |
40 struct |
40 struct |
41 |
41 |
69 fun external_prover subgoalno write_problem_files command check_success produce_answer state = |
69 fun external_prover subgoalno write_problem_files command check_success produce_answer state = |
70 let |
70 let |
71 (*creating description from provername and subgoal*) |
71 (*creating description from provername and subgoal*) |
72 val call::path = rev (String.tokens (fn c => c = #"/") command) |
72 val call::path = rev (String.tokens (fn c => c = #"/") command) |
73 val name::options = String.tokens (fn c => c = #" ") call |
73 val name::options = String.tokens (fn c => c = #" ") call |
74 val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state) |
74 val (ctxt, (chain_ths, goal)) = Proof.get_goal state |
75 val description = "External prover '" ^ name ^ "' for Subgoal " ^ Int.toString subgoalno |
75 val description = "External prover '" ^ name ^ "' for Subgoal " ^ Int.toString subgoalno |
76 ^ ":\n" ^ Display.string_of_cterm (List.nth(cprems_of goal, subgoalno-1)) |
76 ^ ":\n" ^ Display.string_of_cterm (List.nth(cprems_of goal, subgoalno-1)) |
77 (* path to unique problemfile *) |
77 (* path to unique problemfile *) |
78 fun prob_pathname nr = |
78 fun prob_pathname nr = |
79 let val probfile = Path.basic (!problem_name ^ serial_string () ^ "_" ^ Int.toString nr) |
79 let val probfile = Path.basic (!problem_name ^ serial_string () ^ "_" ^ Int.toString nr) |
178 (* default settings*) |
178 (* default settings*) |
179 val spass = spass_filter_opts 40 true; |
179 val spass = spass_filter_opts 40 true; |
180 |
180 |
181 (*TODO: Thread running some selected or recommended provers of "System On TPTP" *) |
181 (*TODO: Thread running some selected or recommended provers of "System On TPTP" *) |
182 |
182 |
183 |
|
184 |
|
185 fun add_prover name prover_fun = AtpManager.Provers.map (Symtab.update (name, prover_fun)) |
|
186 |
|
187 (* include 'original' provers and provers with structured output *) |
|
188 val setup = |
|
189 (* original setups *) |
|
190 add_prover "spass" spass #> |
|
191 add_prover "vampire" vampire #> |
|
192 add_prover "e" eprover #> |
|
193 (* provers with stuctured output *) |
|
194 add_prover "vampire_full" vampire_full #> |
|
195 add_prover "e_full" eprover_full #> |
|
196 (* on some problems better results *) |
|
197 add_prover "spass_no_tc" (spass_filter_opts 40 false); |
|
198 |
|
199 end; |
183 end; |