src/HOL/Tools/atp_wrapper.ML
changeset 28592 824f8390aaa2
child 28596 fcd463a6b6de
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/atp_wrapper.ML	Tue Oct 14 16:01:36 2008 +0200
     1.3 @@ -0,0 +1,150 @@
     1.4 +(*  Title:      HOL/Tools/atp_wrapper.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Fabian Immler, TU Muenchen
     1.7 +
     1.8 +Wrapper functions for external ATPs.
     1.9 +*)
    1.10 +
    1.11 +signature ATP_WRAPPER =
    1.12 +sig
    1.13 +  (* hooks for writing problemfiles *)
    1.14 +  val destdir: string ref
    1.15 +  val problem_name: string ref
    1.16 +  (* basic template *)
    1.17 +  val external_prover:
    1.18 +    ((int -> Path.T) -> Proof.context * thm list * thm -> string list * ResHolClause.axiom_name Vector.vector list) ->
    1.19 +    Path.T * string ->
    1.20 +    (string * int -> bool) ->
    1.21 +    (string * string vector * Proof.context * thm * int -> string) ->
    1.22 +    int -> Proof.state -> Thread.thread
    1.23 +  (* provers as functions returning threads *)
    1.24 +  val tptp_prover_filter_opts_full: int -> bool -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread
    1.25 +  val tptp_prover_filter_opts: int -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread
    1.26 +  val remote_prover_filter_opts: int -> bool -> string -> string -> int -> Proof.state -> Thread.thread
    1.27 +  val full_prover_filter_opts: int -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread
    1.28 +  val tptp_prover: Path.T * string -> int -> Proof.state -> Thread.thread
    1.29 +  val remote_prover: string -> string -> int -> Proof.state -> Thread.thread
    1.30 +  val full_prover: Path.T * string  -> int -> Proof.state -> Thread.thread
    1.31 +  val spass_filter_opts: int -> bool  -> int -> Proof.state -> Thread.thread
    1.32 +  val eprover_filter_opts: int -> bool  -> int -> Proof.state -> Thread.thread
    1.33 +  val eprover_filter_opts_full: int -> bool -> int -> Proof.state -> Thread.thread
    1.34 +  val vampire_filter_opts: int -> bool -> int -> Proof.state -> Thread.thread
    1.35 +  val vampire_filter_opts_full: int -> bool -> int -> Proof.state -> Thread.thread
    1.36 +  val spass: int -> Proof.state -> Thread.thread
    1.37 +  val eprover: int -> Proof.state -> Thread.thread
    1.38 +  val eprover_full: int -> Proof.state -> Thread.thread
    1.39 +  val vampire: int -> Proof.state -> Thread.thread
    1.40 +  val vampire_full: int -> Proof.state -> Thread.thread
    1.41 +end;
    1.42 +
    1.43 +structure AtpWrapper: ATP_WRAPPER =
    1.44 +struct
    1.45 +  
    1.46 +  (* preferences for path and filename to problemfiles *)
    1.47 +  val destdir = ref "";   (*Empty means write files to /tmp*)
    1.48 +  val problem_name = ref "prob";
    1.49 +      
    1.50 +  (*Setting up a Thread for an external prover*)
    1.51 +  fun external_prover write_problem_files (cmd, args) check_success produce_answer subgoalno state =
    1.52 +    let
    1.53 +    val destdir' = ! destdir
    1.54 +    val problem_name' = ! problem_name
    1.55 +    val (ctxt, (chain_ths, goal)) = Proof.get_goal state
    1.56 +    (* path to unique problem file *)
    1.57 +    fun prob_pathname nr =
    1.58 +      let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ Int.toString nr)
    1.59 +      in if destdir' = "" then File.tmp_path probfile
    1.60 +        else if File.exists (Path.explode (destdir'))
    1.61 +        then Path.append  (Path.explode (destdir')) probfile
    1.62 +        else error ("No such directory: " ^ destdir')
    1.63 +      end
    1.64 +    (* write out problem file and call prover *)
    1.65 +    fun call_prover () =
    1.66 +      let
    1.67 +      val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
    1.68 +      val (filenames, thm_names_list) =
    1.69 +        write_problem_files prob_pathname (ctxt, chain_ths, goal)
    1.70 +      val thm_names = List.nth (thm_names_list, subgoalno - 1); (*(i-1)th element for i-th subgoal*)
    1.71 +
    1.72 +      val cmdline =
    1.73 +        if File.exists cmd then File.shell_path cmd ^ " " ^ args
    1.74 +        else error ("Bad executable: " ^ Path.implode cmd);
    1.75 +      val (proof, rc) = system_out (cmdline ^ " " ^ List.nth (filenames, subgoalno - 1))
    1.76 +      val _ =
    1.77 +        if rc <> 0
    1.78 +        then warning ("Sledgehammer with command " ^ quote cmdline ^ " exited with " ^ Int.toString rc)
    1.79 +        else ()
    1.80 +      (* remove *temporary* files *)
    1.81 +      val _ = if destdir' = "" then app (fn file => OS.FileSys.remove file) filenames else ()
    1.82 +      in
    1.83 +        if check_success (proof, rc) then SOME (proof, thm_names, ctxt, goal, subgoalno)
    1.84 +        else NONE
    1.85 +      end
    1.86 +    in
    1.87 +      AtpManager.atp_thread call_prover produce_answer
    1.88 +    end;
    1.89 +
    1.90 +    
    1.91 +  (*=========== TEMPLATES FOR AUTOMATIC PROVERS =================*)
    1.92 +
    1.93 +  fun tptp_prover_filter_opts_full max_new theory_const full command sg =
    1.94 +    external_prover
    1.95 +    (ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const)
    1.96 +    command
    1.97 +    ResReconstruct.check_success_e_vamp_spass
    1.98 +    (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
    1.99 +    sg
   1.100 +    
   1.101 +  (* arbitrary atp with tptp input/output and problemfile as last argument*)
   1.102 +  fun tptp_prover_filter_opts max_new theory_const =
   1.103 +    tptp_prover_filter_opts_full max_new theory_const false;
   1.104 +  (* default settings*)  
   1.105 +  val tptp_prover = tptp_prover_filter_opts 60 true;
   1.106 +
   1.107 +  (* for structured proofs: prover must support TSTP *)
   1.108 +  fun full_prover_filter_opts max_new theory_const =
   1.109 +    tptp_prover_filter_opts_full max_new theory_const true;
   1.110 +  (* default settings*)
   1.111 +  val full_prover = full_prover_filter_opts 60 true;
   1.112 +
   1.113 +  fun vampire_filter_opts max_new theory_const = tptp_prover_filter_opts
   1.114 +    max_new theory_const
   1.115 +    (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*)
   1.116 +  (* default settings*)
   1.117 +  val vampire = vampire_filter_opts 60 false;
   1.118 +    
   1.119 +  (* a vampire for full proof output *)
   1.120 +  fun vampire_filter_opts_full max_new theory_const = full_prover_filter_opts
   1.121 +    max_new theory_const
   1.122 +    (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*)
   1.123 +  (* default settings*)
   1.124 +  val vampire_full = vampire_filter_opts 60 false;
   1.125 +
   1.126 +  fun eprover_filter_opts max_new theory_const = tptp_prover_filter_opts
   1.127 +    max_new theory_const
   1.128 +    (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent")
   1.129 +  (* default settings *)
   1.130 +  val eprover = eprover_filter_opts 100 false;
   1.131 +    
   1.132 +  (* an E for full proof output*)
   1.133 +  fun eprover_filter_opts_full max_new theory_const = full_prover_filter_opts
   1.134 +    max_new theory_const
   1.135 +    (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent")
   1.136 +  (* default settings *)
   1.137 +  val eprover_full = eprover_filter_opts_full 100 false;
   1.138 +
   1.139 +  fun spass_filter_opts max_new theory_const = external_prover
   1.140 +    (ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const)
   1.141 +    (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof")
   1.142 +    ResReconstruct.check_success_e_vamp_spass
   1.143 +    ResReconstruct.lemma_list_dfg
   1.144 +  (* default settings*)
   1.145 +  val spass = spass_filter_opts 40 true;
   1.146 +    
   1.147 +  (* remote prover invocation via SystemOnTPTP *)
   1.148 +  fun remote_prover_filter_opts max_new theory_const name command =
   1.149 +    tptp_prover_filter_opts max_new theory_const
   1.150 +    (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ command)
   1.151 +  val remote_prover = remote_prover_filter_opts 60 false
   1.152 +
   1.153 +end;