author | immler@in.tum.de |
Wed, 03 Jun 2009 16:56:41 +0200 | |
changeset 31409 | d8537ba165b5 |
parent 31368 | 763f4b0fd579 |
child 31410 | c231efe693ce |
permissions | -rw-r--r-- |
28592 | 1 |
(* Title: HOL/Tools/atp_wrapper.ML |
2 |
Author: Fabian Immler, TU Muenchen |
|
3 |
||
4 |
Wrapper functions for external ATPs. |
|
5 |
*) |
|
6 |
||
7 |
signature ATP_WRAPPER = |
|
8 |
sig |
|
9 |
val destdir: string ref |
|
10 |
val problem_name: string ref |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
11 |
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
|
12 |
val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
13 |
val tptp_prover: Path.T * string -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
14 |
val full_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
15 |
val full_prover: Path.T * string -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
16 |
val vampire_opts: int -> bool -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
17 |
val vampire: AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
18 |
val vampire_opts_full: int -> bool -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
19 |
val vampire_full: AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
20 |
val eprover_opts: int -> bool -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
21 |
val eprover: AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
22 |
val eprover_opts_full: int -> bool -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
23 |
val eprover_full: AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
24 |
val spass_opts: int -> bool -> AtpManager.prover |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
25 |
val spass: AtpManager.prover |
29590 | 26 |
val remote_prover_opts: int -> bool -> string -> AtpManager.prover |
27 |
val remote_prover: string -> AtpManager.prover |
|
28592 | 28 |
end; |
29 |
||
30 |
structure AtpWrapper: ATP_WRAPPER = |
|
31 |
struct |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
32 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
33 |
(** generic ATP wrapper **) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
34 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
35 |
(* global hooks for writing problemfiles *) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
36 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
37 |
val destdir = ref ""; (*Empty means write files to /tmp*) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
38 |
val problem_name = ref "prob"; |
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 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
41 |
(* basic template *) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
42 |
|
31409
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
43 |
fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
44 |
timeout axiom_clauses const_counts name subgoalno goal = |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
45 |
let |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
46 |
(* path to unique problem file *) |
28592 | 47 |
val destdir' = ! destdir |
48 |
val problem_name' = ! problem_name |
|
49 |
fun prob_pathname nr = |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
50 |
let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ string_of_int nr) |
28592 | 51 |
in if destdir' = "" then File.tmp_path probfile |
52 |
else if File.exists (Path.explode (destdir')) |
|
53 |
then Path.append (Path.explode (destdir')) probfile |
|
54 |
else error ("No such directory: " ^ destdir') |
|
55 |
end |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
56 |
|
28592 | 57 |
(* write out problem file and call prover *) |
30537 | 58 |
val (ctxt, (chain_ths, th)) = goal |
30536
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
59 |
val thy = ProofContext.theory_of ctxt |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
60 |
val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths |
30536
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
61 |
val probfile = prob_pathname subgoalno |
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
62 |
val fname = File.platform_path probfile |
31409
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
63 |
val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno) |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
64 |
handle THM ("assume: variables", _, _) => |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
65 |
error "Sledgehammer: Goal contains type variables (TVars)" |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
66 |
val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
67 |
val the_axiom_clauses = |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
68 |
case axiom_clauses of |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
69 |
NONE => relevance_filter goal goal_cls |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
70 |
| SOME axcls => axcls |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
71 |
val (thm_names, clauses) = preparer goal_cls the_axiom_clauses thy |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
72 |
val the_const_counts = case const_counts of |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
73 |
NONE => |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
74 |
ResHolClause.count_constants( |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
75 |
case axiom_clauses of |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
76 |
NONE => clauses |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
77 |
| SOME axcls => #2(preparer goal_cls (relevance_filter goal goal_cls) thy) |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
78 |
) |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
79 |
| SOME ccs => ccs |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
80 |
val _ = writer fname the_const_counts clauses |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
81 |
val cmdline = |
30899
d394a17d4fdb
external_prover: "exec" the command line, in order to preserve the exact process context of the "system" invocation (this recovers interruptibility of E-1.0, which assumes to be the process group leader);
wenzelm
parents:
30896
diff
changeset
|
82 |
if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
83 |
else error ("Bad executable: " ^ Path.implode cmd) |
30536
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
84 |
val (proof, rc) = system_out (cmdline ^ " " ^ fname) |
28592 | 85 |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
86 |
(* remove *temporary* files *) |
30536
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
87 |
val _ = if destdir' = "" then OS.FileSys.remove fname else () |
29590 | 88 |
|
89 |
(* check for success and print out some information on failure *) |
|
90 |
val failure = find_failure proof |
|
29597 | 91 |
val success = rc = 0 andalso is_none failure |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
92 |
val message = |
30896
ec3f33437fe3
more generic error message, which also covers more fundamental failure;
wenzelm
parents:
30874
diff
changeset
|
93 |
if is_some failure then "External prover failed." |
ec3f33437fe3
more generic error message, which also covers more fundamental failure;
wenzelm
parents:
30874
diff
changeset
|
94 |
else if rc <> 0 then "External prover failed: " ^ proof |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
30979
diff
changeset
|
95 |
else "Try this command: " ^ produce_answer name (proof, thm_names, ctxt, th, subgoalno) |
30535 | 96 |
|
30896
ec3f33437fe3
more generic error message, which also covers more fundamental failure;
wenzelm
parents:
30874
diff
changeset
|
97 |
val _ = |
ec3f33437fe3
more generic error message, which also covers more fundamental failure;
wenzelm
parents:
30874
diff
changeset
|
98 |
if is_some failure |
30015
1baeda435aa6
detailed information on atp-failure via Output.debug
immler@in.tum.de
parents:
29597
diff
changeset
|
99 |
then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof) |
1baeda435aa6
detailed information on atp-failure via Output.debug
immler@in.tum.de
parents:
29597
diff
changeset
|
100 |
else () |
30896
ec3f33437fe3
more generic error message, which also covers more fundamental failure;
wenzelm
parents:
30874
diff
changeset
|
101 |
val _ = |
ec3f33437fe3
more generic error message, which also covers more fundamental failure;
wenzelm
parents:
30874
diff
changeset
|
102 |
if rc <> 0 |
30015
1baeda435aa6
detailed information on atp-failure via Output.debug
immler@in.tum.de
parents:
29597
diff
changeset
|
103 |
then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof) |
1baeda435aa6
detailed information on atp-failure via Output.debug
immler@in.tum.de
parents:
29597
diff
changeset
|
104 |
else () |
31409
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
105 |
in (success, message, proof, thm_names, the_const_counts) end; |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
106 |
|
28592 | 107 |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
108 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
109 |
(** common provers **) |
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 |
(* generic TPTP-based provers *) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
112 |
|
31409
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
113 |
fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses ccs name n goal = |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
114 |
external_prover |
31409
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
115 |
(ResAtp.get_relevant max_new theory_const) |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
116 |
(ResAtp.prepare_clauses false) |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
117 |
(ResHolClause.tptp_write_file) |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
118 |
command |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
119 |
ResReconstruct.find_failure |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
120 |
(if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp) |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
121 |
timeout ax_clauses ccs name n goal; |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
122 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
123 |
(*arbitrary ATP with TPTP input/output and problemfile as last argument*) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
124 |
fun tptp_prover_opts max_new theory_const = |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
125 |
tptp_prover_opts_full max_new theory_const false; |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
126 |
|
31368 | 127 |
fun tptp_prover x = tptp_prover_opts 60 true x; |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
128 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
129 |
(*for structured proofs: prover must support TSTP*) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
130 |
fun full_prover_opts max_new theory_const = |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
131 |
tptp_prover_opts_full max_new theory_const true; |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
132 |
|
31368 | 133 |
fun full_prover x = full_prover_opts 60 true x; |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
134 |
|
28592 | 135 |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
136 |
(* Vampire *) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
137 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
138 |
(*NB: Vampire does not work without explicit timelimit*) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
139 |
|
29593 | 140 |
fun vampire_opts max_new theory_const timeout = tptp_prover_opts |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
141 |
max_new theory_const |
29593 | 142 |
(Path.explode "$VAMPIRE_HOME/vampire", |
143 |
("--output_syntax tptp --mode casc -t " ^ string_of_int timeout)) |
|
144 |
timeout; |
|
28596
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 |
val vampire = vampire_opts 60 false; |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
147 |
|
29593 | 148 |
fun vampire_opts_full max_new theory_const timeout = full_prover_opts |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
149 |
max_new theory_const |
29593 | 150 |
(Path.explode "$VAMPIRE_HOME/vampire", |
151 |
("--output_syntax tptp --mode casc -t " ^ string_of_int timeout)) |
|
152 |
timeout; |
|
28596
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 vampire_full = vampire_opts 60 false; |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
155 |
|
28592 | 156 |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
157 |
(* E prover *) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
158 |
|
30536
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
159 |
fun eprover_opts max_new theory_const timeout = tptp_prover_opts |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
160 |
max_new theory_const |
30536
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
161 |
(Path.explode "$E_HOME/eproof", |
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
162 |
"--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout) |
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
163 |
timeout; |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
164 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
165 |
val eprover = eprover_opts 100 false; |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
166 |
|
30536
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
167 |
fun eprover_opts_full max_new theory_const timeout = full_prover_opts |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
168 |
max_new theory_const |
30536
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
169 |
(Path.explode "$E_HOME/eproof", |
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
170 |
"--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout) |
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
171 |
timeout; |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
172 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
173 |
val eprover_full = eprover_opts_full 100 false; |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
174 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
175 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
176 |
(* SPASS *) |
28592 | 177 |
|
31409
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
178 |
fun spass_opts max_new theory_const timeout ax_clauses ccs name n goal = external_prover |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
179 |
(ResAtp.get_relevant max_new theory_const) |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
180 |
(ResAtp.prepare_clauses true) |
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
181 |
ResHolClause.dfg_write_file |
30536
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
182 |
(Path.explode "$SPASS_HOME/SPASS", |
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
183 |
"-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout) |
30874
34927a1e0ae8
reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents:
30542
diff
changeset
|
184 |
ResReconstruct.find_failure |
30536
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
185 |
ResReconstruct.lemma_list_dfg |
31409
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset
|
186 |
timeout ax_clauses ccs name n goal; |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
187 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
188 |
val spass = spass_opts 40 true; |
28592 | 189 |
|
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
190 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
191 |
(* remote prover invocation via SystemOnTPTP *) |
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
192 |
|
29593 | 193 |
fun remote_prover_opts max_new theory_const args timeout = |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
194 |
tptp_prover_opts max_new theory_const |
30979
10eb446df3c7
renamed contrib/SystemOnTPTP/remote to lib/script/SystemOnTPTP, thus leaving contrib empty within the official distribution;
wenzelm
parents:
30899
diff
changeset
|
195 |
(Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP", args ^ " -t " ^ string_of_int timeout) |
29593 | 196 |
timeout; |
28596
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
197 |
|
fcd463a6b6de
tuned interfaces -- plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset
|
198 |
val remote_prover = remote_prover_opts 60 false; |
28592 | 199 |
|
200 |
end; |
|
30536
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
201 |
|
07b4f050e4df
split relevance-filter and writing of problem-files;
immler@in.tum.de
parents:
30535
diff
changeset
|
202 |