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 
(* hooks for writing problemfiles *)


11 
val destdir: string ref


12 
val problem_name: string ref


13 
(* basic template *)


14 
val external_prover:


15 
((int > Path.T) > Proof.context * thm list * thm > string list * ResHolClause.axiom_name Vector.vector list) >


16 
Path.T * string >


17 
(string * int > bool) >


18 
(string * string vector * Proof.context * thm * int > string) >


19 
int > Proof.state > Thread.thread


20 
(* provers as functions returning threads *)


21 
val tptp_prover_filter_opts_full: int > bool > bool > Path.T * string > int > Proof.state > Thread.thread


22 
val tptp_prover_filter_opts: int > bool > Path.T * string > int > Proof.state > Thread.thread


23 
val remote_prover_filter_opts: int > bool > string > string > int > Proof.state > Thread.thread


24 
val full_prover_filter_opts: int > bool > Path.T * string > int > Proof.state > Thread.thread


25 
val tptp_prover: Path.T * string > int > Proof.state > Thread.thread


26 
val remote_prover: string > string > int > Proof.state > Thread.thread


27 
val full_prover: Path.T * string > int > Proof.state > Thread.thread


28 
val spass_filter_opts: int > bool > int > Proof.state > Thread.thread


29 
val eprover_filter_opts: int > bool > int > Proof.state > Thread.thread


30 
val eprover_filter_opts_full: int > bool > int > Proof.state > Thread.thread


31 
val vampire_filter_opts: int > bool > int > Proof.state > Thread.thread


32 
val vampire_filter_opts_full: int > bool > int > Proof.state > Thread.thread


33 
val spass: int > Proof.state > Thread.thread


34 
val eprover: int > Proof.state > Thread.thread


35 
val eprover_full: int > Proof.state > Thread.thread


36 
val vampire: int > Proof.state > Thread.thread


37 
val vampire_full: int > Proof.state > Thread.thread


38 
end;


39 


40 
structure AtpWrapper: ATP_WRAPPER =


41 
struct


42 


43 
(* preferences for path and filename to problemfiles *)


44 
val destdir = ref ""; (*Empty means write files to /tmp*)


45 
val problem_name = ref "prob";


46 


47 
(*Setting up a Thread for an external prover*)


48 
fun external_prover write_problem_files (cmd, args) check_success produce_answer subgoalno state =


49 
let


50 
val destdir' = ! destdir


51 
val problem_name' = ! problem_name


52 
val (ctxt, (chain_ths, goal)) = Proof.get_goal state


53 
(* path to unique problem file *)


54 
fun prob_pathname nr =


55 
let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ Int.toString nr)


56 
in if destdir' = "" then File.tmp_path probfile


57 
else if File.exists (Path.explode (destdir'))


58 
then Path.append (Path.explode (destdir')) probfile


59 
else error ("No such directory: " ^ destdir')


60 
end


61 
(* write out problem file and call prover *)


62 
fun call_prover () =


63 
let


64 
val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths


65 
val (filenames, thm_names_list) =


66 
write_problem_files prob_pathname (ctxt, chain_ths, goal)


67 
val thm_names = List.nth (thm_names_list, subgoalno  1); (*(i1)th element for ith subgoal*)


68 


69 
val cmdline =


70 
if File.exists cmd then File.shell_path cmd ^ " " ^ args


71 
else error ("Bad executable: " ^ Path.implode cmd);


72 
val (proof, rc) = system_out (cmdline ^ " " ^ List.nth (filenames, subgoalno  1))


73 
val _ =


74 
if rc <> 0


75 
then warning ("Sledgehammer with command " ^ quote cmdline ^ " exited with " ^ Int.toString rc)


76 
else ()


77 
(* remove *temporary* files *)


78 
val _ = if destdir' = "" then app (fn file => OS.FileSys.remove file) filenames else ()


79 
in


80 
if check_success (proof, rc) then SOME (proof, thm_names, ctxt, goal, subgoalno)


81 
else NONE


82 
end


83 
in


84 
AtpManager.atp_thread call_prover produce_answer


85 
end;


86 


87 


88 
(*=========== TEMPLATES FOR AUTOMATIC PROVERS =================*)


89 


90 
fun tptp_prover_filter_opts_full max_new theory_const full command sg =


91 
external_prover


92 
(ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const)


93 
command


94 
ResReconstruct.check_success_e_vamp_spass


95 
(if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)


96 
sg


97 


98 
(* arbitrary atp with tptp input/output and problemfile as last argument*)


99 
fun tptp_prover_filter_opts max_new theory_const =


100 
tptp_prover_filter_opts_full max_new theory_const false;


101 
(* default settings*)


102 
val tptp_prover = tptp_prover_filter_opts 60 true;


103 


104 
(* for structured proofs: prover must support TSTP *)


105 
fun full_prover_filter_opts max_new theory_const =


106 
tptp_prover_filter_opts_full max_new theory_const true;


107 
(* default settings*)


108 
val full_prover = full_prover_filter_opts 60 true;


109 


110 
fun vampire_filter_opts max_new theory_const = tptp_prover_filter_opts


111 
max_new theory_const


112 
(Path.explode "$VAMPIRE_HOME/vampire", "output_syntax tptp mode casc t 3600") (* vampire does not work without timelimit*)


113 
(* default settings*)


114 
val vampire = vampire_filter_opts 60 false;


115 


116 
(* a vampire for full proof output *)


117 
fun vampire_filter_opts_full max_new theory_const = full_prover_filter_opts


118 
max_new theory_const


119 
(Path.explode "$VAMPIRE_HOME/vampire", "output_syntax tptp mode casc t 3600") (* vampire does not work without timelimit*)


120 
(* default settings*)


121 
val vampire_full = vampire_filter_opts 60 false;


122 


123 
fun eprover_filter_opts max_new theory_const = tptp_prover_filter_opts


124 
max_new theory_const


125 
(Path.explode "$E_HOME/eproof", "tstpin tstpout l5 xAutoDev tAutoDev silent")


126 
(* default settings *)


127 
val eprover = eprover_filter_opts 100 false;


128 


129 
(* an E for full proof output*)


130 
fun eprover_filter_opts_full max_new theory_const = full_prover_filter_opts


131 
max_new theory_const


132 
(Path.explode "$E_HOME/eproof", "tstpin tstpout l5 xAutoDev tAutoDev silent")


133 
(* default settings *)


134 
val eprover_full = eprover_filter_opts_full 100 false;


135 


136 
fun spass_filter_opts max_new theory_const = external_prover


137 
(ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const)


138 
(Path.explode "$SPASS_HOME/SPASS", "Auto SOS=1 PGiven=0 PProblem=0 Splits=0 FullRed=0 DocProof")


139 
ResReconstruct.check_success_e_vamp_spass


140 
ResReconstruct.lemma_list_dfg


141 
(* default settings*)


142 
val spass = spass_filter_opts 40 true;


143 


144 
(* remote prover invocation via SystemOnTPTP *)


145 
fun remote_prover_filter_opts max_new theory_const name command =


146 
tptp_prover_filter_opts max_new theory_const


147 
(Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ command)


148 
val remote_prover = remote_prover_filter_opts 60 false


149 


150 
end;
