src/HOL/Tools/atp_wrapper.ML
changeset 28592 824f8390aaa2
child 28596 fcd463a6b6de
equal deleted inserted replaced
28591:790d1863be28 28592:824f8390aaa2
       
     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); (*(i-1)th element for i-th 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", "--tstp-in --tstp-out -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", "--tstp-in --tstp-out -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;