237 (* generic TPTP-based provers *) |
237 (* generic TPTP-based provers *) |
238 |
238 |
239 fun generic_tptp_prover |
239 fun generic_tptp_prover |
240 (name, {home_var, executable, arguments, proof_delims, known_failures, |
240 (name, {home_var, executable, arguments, proof_delims, known_failures, |
241 max_axiom_clauses, prefers_theory_relevant}) |
241 max_axiom_clauses, prefers_theory_relevant}) |
242 (params as {debug, overlord, respect_no_atp, relevance_threshold, |
242 (params as {debug, overlord, full_types, respect_no_atp, |
243 relevance_convergence, theory_relevant, defs_relevant, |
243 relevance_threshold, relevance_convergence, theory_relevant, |
244 isar_proof, ...}) |
244 defs_relevant, isar_proof, ...}) |
245 minimize_command timeout = |
245 minimize_command timeout = |
246 generic_prover overlord |
246 generic_prover overlord |
247 (get_relevant_facts respect_no_atp relevance_threshold |
247 (relevant_facts full_types respect_no_atp relevance_threshold |
248 relevance_convergence defs_relevant max_axiom_clauses |
248 relevance_convergence defs_relevant max_axiom_clauses |
249 (the_default prefers_theory_relevant theory_relevant)) |
249 (the_default prefers_theory_relevant theory_relevant)) |
250 (prepare_clauses false) |
250 (prepare_clauses false) |
251 (write_tptp_file (debug andalso overlord)) home_var |
251 (write_tptp_file (debug andalso overlord)) home_var |
252 executable (arguments timeout) proof_delims known_failures name params |
252 executable (arguments timeout) proof_delims known_failures name params |
253 minimize_command |
253 minimize_command |
254 |
254 |
312 (* SPASS *) |
312 (* SPASS *) |
313 |
313 |
314 fun generic_dfg_prover |
314 fun generic_dfg_prover |
315 (name, {home_var, executable, arguments, proof_delims, known_failures, |
315 (name, {home_var, executable, arguments, proof_delims, known_failures, |
316 max_axiom_clauses, prefers_theory_relevant}) |
316 max_axiom_clauses, prefers_theory_relevant}) |
317 (params as {overlord, respect_no_atp, relevance_threshold, |
317 (params as {overlord, full_types, respect_no_atp, relevance_threshold, |
318 relevance_convergence, theory_relevant, defs_relevant, ...}) |
318 relevance_convergence, theory_relevant, defs_relevant, ...}) |
319 minimize_command timeout = |
319 minimize_command timeout = |
320 generic_prover overlord |
320 generic_prover overlord |
321 (get_relevant_facts respect_no_atp relevance_threshold |
321 (relevant_facts full_types respect_no_atp relevance_threshold |
322 relevance_convergence defs_relevant max_axiom_clauses |
322 relevance_convergence defs_relevant max_axiom_clauses |
323 (the_default prefers_theory_relevant theory_relevant)) |
323 (the_default prefers_theory_relevant theory_relevant)) |
324 (prepare_clauses true) write_dfg_file home_var executable |
324 (prepare_clauses true) write_dfg_file home_var executable |
325 (arguments timeout) proof_delims known_failures name params |
325 (arguments timeout) proof_delims known_failures name params |
326 minimize_command |
326 minimize_command |
327 |
327 |
328 fun dfg_prover name p = (name, generic_dfg_prover (name, p)) |
328 fun dfg_prover name p = (name, generic_dfg_prover (name, p)) |