equal
deleted
inserted
replaced
58 \ATPs remotely." |
58 \ATPs remotely." |
59 |
59 |
60 fun string_for_failure Unprovable = "The ATP problem is unprovable." |
60 fun string_for_failure Unprovable = "The ATP problem is unprovable." |
61 | string_for_failure IncompleteUnprovable = |
61 | string_for_failure IncompleteUnprovable = |
62 "The ATP cannot prove the problem." |
62 "The ATP cannot prove the problem." |
63 | string_for_failure CantConnect = "Can't connect to remote ATP." |
63 | string_for_failure CantConnect = "Can't connect to remote server." |
64 | string_for_failure TimedOut = "Timed out." |
64 | string_for_failure TimedOut = "Timed out." |
65 | string_for_failure OutOfResources = "The ATP ran out of resources." |
65 | string_for_failure OutOfResources = "The ATP ran out of resources." |
66 | string_for_failure OldSpass = |
66 | string_for_failure OldSpass = |
67 "Warning: Isabelle requires a more recent version of SPASS with \ |
67 "Warning: Isabelle requires a more recent version of SPASS with \ |
68 \support for the TPTP syntax. To install it, download and extract the \ |
68 \support for the TPTP syntax. To install it, download and extract the \ |
84 fun known_failure_in_output output = |
84 fun known_failure_in_output output = |
85 find_first (fn (_, pattern) => String.isSubstring pattern output) |
85 find_first (fn (_, pattern) => String.isSubstring pattern output) |
86 #> Option.map fst |
86 #> Option.map fst |
87 |
87 |
88 val known_perl_failures = |
88 val known_perl_failures = |
89 [(NoPerl, "env: perl"), |
89 [(CantConnect, "HTTP error"), |
|
90 (NoPerl, "env: perl"), |
90 (NoLibwwwPerl, "Can't locate HTTP")] |
91 (NoLibwwwPerl, "Can't locate HTTP")] |
91 |
92 |
92 (* named provers *) |
93 (* named provers *) |
93 |
94 |
94 structure Data = Theory_Data |
95 structure Data = Theory_Data |
152 required_execs = [("SPASS_HOME", "SPASS")], |
153 required_execs = [("SPASS_HOME", "SPASS")], |
153 (* "div 2" accounts for the fact that SPASS is often run twice. *) |
154 (* "div 2" accounts for the fact that SPASS is often run twice. *) |
154 arguments = fn complete => fn timeout => |
155 arguments = fn complete => fn timeout => |
155 ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ |
156 ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ |
156 \-VarWeight=3 -TimeLimit=" ^ |
157 \-VarWeight=3 -TimeLimit=" ^ |
157 string_of_int (to_generous_secs timeout div 2)) |
158 string_of_int ((to_generous_secs timeout + 1) div 2)) |
158 |> not complete ? prefix "-SOS=1 ", |
159 |> not complete ? prefix "-SOS=1 ", |
159 proof_delims = [("Here is a proof", "Formulae used in the proof")], |
160 proof_delims = [("Here is a proof", "Formulae used in the proof")], |
160 known_failures = |
161 known_failures = |
161 known_perl_failures @ |
162 known_perl_failures @ |
162 [(IncompleteUnprovable, "SPASS beiseite: Completion found"), |
163 [(IncompleteUnprovable, "SPASS beiseite: Completion found"), |
228 " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^ |
229 " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^ |
229 the_system atp_prefix, |
230 the_system atp_prefix, |
230 proof_delims = insert (op =) tstp_proof_delims proof_delims, |
231 proof_delims = insert (op =) tstp_proof_delims proof_delims, |
231 known_failures = |
232 known_failures = |
232 known_failures @ known_perl_failures @ |
233 known_failures @ known_perl_failures @ |
233 [(CantConnect, "HTTP-Error"), |
234 [(TimedOut, "says Timeout")], |
234 (TimedOut, "says Timeout")], |
|
235 max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter, |
235 max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter, |
236 prefers_theory_relevant = prefers_theory_relevant, |
236 prefers_theory_relevant = prefers_theory_relevant, |
237 explicit_forall = explicit_forall} |
237 explicit_forall = explicit_forall} |
238 |
238 |
239 val remote_name = prefix "remote_" |
239 val remote_name = prefix "remote_" |