author | haftmann |
Fri, 16 Jan 2009 08:29:11 +0100 | |
changeset 29505 | c6d2d23909d1 |
parent 28596 | fcd463a6b6de |
child 29587 | 96599d8d8268 |
permissions | -rw-r--r-- |
28592 | 1 |
(* Title: HOL/Tools/atp_wrapper.ML |
2 |
ID: $Id$ |
|
3 |
Author: Fabian Immler, TU Muenchen |
|
4 |
||
5 |
Wrapper functions for external ATPs. |
|
6 |
*) |
|
7 |
||
8 |
signature ATP_WRAPPER = |
|
9 |
sig |
|
10 |
val destdir: string ref |
|
11 |
val problem_name: string ref |
|
12 |
val external_prover: |
|
13 |
((int -> Path.T) -> Proof.context * thm list * thm -> string list * ResHolClause.axiom_name Vector.vector list) -> |
|
14 |
Path.T * string -> |
|
15 |
(string * int -> bool) -> |
|
16 |
(string * string vector * Proof.context * thm * int -> string) -> |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
17 |
AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
18 |
val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
19 |
val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
20 |
val tptp_prover: Path.T * string -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
21 |
val full_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
22 |
val full_prover: Path.T * string -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
23 |
val vampire_opts: int -> bool -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
24 |
val vampire: AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
25 |
val vampire_opts_full: int -> bool -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
26 |
val vampire_full: AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
27 |
val eprover_opts: int -> bool -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
28 |
val eprover: AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
29 |
val eprover_opts_full: int -> bool -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
30 |
val eprover_full: AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
31 |
val spass_opts: int -> bool -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
32 |
val spass: AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
33 |
val remote_prover_opts: int -> bool -> string -> string -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
34 |
val remote_prover: string -> string -> AtpManager.prover |
28592 | 35 |
end; |
36 |
||
37 |
structure AtpWrapper: ATP_WRAPPER = |
|
38 |
struct |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
39 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
40 |
(** generic ATP wrapper **) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
41 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
42 |
(* global hooks for writing problemfiles *) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
43 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
44 |
val destdir = ref ""; (*Empty means write files to /tmp*) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
45 |
val problem_name = ref "prob"; |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
46 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
47 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
48 |
(* basic template *) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
49 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
50 |
fun external_prover write_problem_files (cmd, args) check_success produce_answer subgoalno state = |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
51 |
let |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
52 |
(* path to unique problem file *) |
28592 | 53 |
val destdir' = ! destdir |
54 |
val problem_name' = ! problem_name |
|
55 |
fun prob_pathname nr = |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
56 |
let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ string_of_int nr) |
28592 | 57 |
in if destdir' = "" then File.tmp_path probfile |
58 |
else if File.exists (Path.explode (destdir')) |
|
59 |
then Path.append (Path.explode (destdir')) probfile |
|
60 |
else error ("No such directory: " ^ destdir') |
|
61 |
end |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
62 |
|
28592 | 63 |
(* write out problem file and call prover *) |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
64 |
val (ctxt, (chain_ths, goal)) = Proof.get_goal state |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
65 |
val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
66 |
val (filenames, thm_names_list) = write_problem_files prob_pathname (ctxt, chain_ths, goal) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
67 |
val thm_names = nth thm_names_list (subgoalno - 1) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
68 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
69 |
val cmdline = |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
70 |
if File.exists cmd then File.shell_path cmd ^ " " ^ args |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
71 |
else error ("Bad executable: " ^ Path.implode cmd) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
72 |
val (proof, rc) = system_out (cmdline ^ " " ^ nth filenames (subgoalno - 1)) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
73 |
val _ = |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
74 |
if rc <> 0 then |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
75 |
warning ("Sledgehammer prover exited with return code " ^ string_of_int rc ^ "\n" ^ cmdline) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
76 |
else () |
28592 | 77 |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
78 |
(* remove *temporary* files *) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
79 |
val _ = if destdir' = "" then List.app OS.FileSys.remove filenames else () |
28592 | 80 |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
81 |
val success = check_success (proof, rc) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
82 |
val message = |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
83 |
if success |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
84 |
then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
85 |
else "Failed." |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
86 |
in (success, message) end; |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
87 |
|
28592 | 88 |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
89 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
90 |
(** common provers **) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
91 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
92 |
(* generic TPTP-based provers *) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
93 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
94 |
fun tptp_prover_opts_full max_new theory_const full command = |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
95 |
external_prover |
28592 | 96 |
(ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const) |
97 |
command |
|
98 |
ResReconstruct.check_success_e_vamp_spass |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
99 |
(if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp); |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
100 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
101 |
(*arbitrary ATP with TPTP input/output and problemfile as last argument*) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
102 |
fun tptp_prover_opts max_new theory_const = |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
103 |
tptp_prover_opts_full max_new theory_const false; |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
104 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
105 |
val tptp_prover = tptp_prover_opts 60 true; |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
106 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
107 |
(*for structured proofs: prover must support TSTP*) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
108 |
fun full_prover_opts max_new theory_const = |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
109 |
tptp_prover_opts_full max_new theory_const true; |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
110 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
111 |
val full_prover = full_prover_opts 60 true; |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
112 |
|
28592 | 113 |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
114 |
(* Vampire *) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
115 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
116 |
(*NB: Vampire does not work without explicit timelimit*) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
117 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
118 |
fun vampire_opts max_new theory_const = tptp_prover_opts |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
119 |
max_new theory_const |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
120 |
(Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600"); |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
121 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
122 |
val vampire = vampire_opts 60 false; |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
123 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
124 |
fun vampire_opts_full max_new theory_const = full_prover_opts |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
125 |
max_new theory_const |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
126 |
(Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600"); |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
127 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
128 |
val vampire_full = vampire_opts 60 false; |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
129 |
|
28592 | 130 |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
131 |
(* E prover *) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
132 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
133 |
fun eprover_opts max_new theory_const = tptp_prover_opts |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
134 |
max_new theory_const |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
135 |
(Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent"); |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
136 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
137 |
val eprover = eprover_opts 100 false; |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
138 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
139 |
fun eprover_opts_full max_new theory_const = full_prover_opts |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
140 |
max_new theory_const |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
141 |
(Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent"); |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
142 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
143 |
val eprover_full = eprover_opts_full 100 false; |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
144 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
145 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
146 |
(* SPASS *) |
28592 | 147 |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
148 |
fun spass_opts max_new theory_const = external_prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
149 |
(ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
150 |
(Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof") |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
151 |
ResReconstruct.check_success_e_vamp_spass |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
152 |
ResReconstruct.lemma_list_dfg; |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
153 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
154 |
val spass = spass_opts 40 true; |
28592 | 155 |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
156 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
157 |
(* remote prover invocation via SystemOnTPTP *) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
158 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
159 |
fun remote_prover_opts max_new theory_const name command = |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
160 |
tptp_prover_opts max_new theory_const |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
161 |
(Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ command); |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
162 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
163 |
val remote_prover = remote_prover_opts 60 false; |
28592 | 164 |
|
165 |
end; |