src/HOL/Tools/atp_wrapper.ML
author wenzelm
Tue Oct 14 16:01:36 2008 +0200 (2008-10-14)
changeset 28592 824f8390aaa2
child 28596 fcd463a6b6de
permissions -rw-r--r--
renamed AtpThread to AtpWrapper;
wenzelm@28592
     1
(*  Title:      HOL/Tools/atp_wrapper.ML
wenzelm@28592
     2
    ID:         $Id$
wenzelm@28592
     3
    Author:     Fabian Immler, TU Muenchen
wenzelm@28592
     4
wenzelm@28592
     5
Wrapper functions for external ATPs.
wenzelm@28592
     6
*)
wenzelm@28592
     7
wenzelm@28592
     8
signature ATP_WRAPPER =
wenzelm@28592
     9
sig
wenzelm@28592
    10
  (* hooks for writing problemfiles *)
wenzelm@28592
    11
  val destdir: string ref
wenzelm@28592
    12
  val problem_name: string ref
wenzelm@28592
    13
  (* basic template *)
wenzelm@28592
    14
  val external_prover:
wenzelm@28592
    15
    ((int -> Path.T) -> Proof.context * thm list * thm -> string list * ResHolClause.axiom_name Vector.vector list) ->
wenzelm@28592
    16
    Path.T * string ->
wenzelm@28592
    17
    (string * int -> bool) ->
wenzelm@28592
    18
    (string * string vector * Proof.context * thm * int -> string) ->
wenzelm@28592
    19
    int -> Proof.state -> Thread.thread
wenzelm@28592
    20
  (* provers as functions returning threads *)
wenzelm@28592
    21
  val tptp_prover_filter_opts_full: int -> bool -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread
wenzelm@28592
    22
  val tptp_prover_filter_opts: int -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread
wenzelm@28592
    23
  val remote_prover_filter_opts: int -> bool -> string -> string -> int -> Proof.state -> Thread.thread
wenzelm@28592
    24
  val full_prover_filter_opts: int -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread
wenzelm@28592
    25
  val tptp_prover: Path.T * string -> int -> Proof.state -> Thread.thread
wenzelm@28592
    26
  val remote_prover: string -> string -> int -> Proof.state -> Thread.thread
wenzelm@28592
    27
  val full_prover: Path.T * string  -> int -> Proof.state -> Thread.thread
wenzelm@28592
    28
  val spass_filter_opts: int -> bool  -> int -> Proof.state -> Thread.thread
wenzelm@28592
    29
  val eprover_filter_opts: int -> bool  -> int -> Proof.state -> Thread.thread
wenzelm@28592
    30
  val eprover_filter_opts_full: int -> bool -> int -> Proof.state -> Thread.thread
wenzelm@28592
    31
  val vampire_filter_opts: int -> bool -> int -> Proof.state -> Thread.thread
wenzelm@28592
    32
  val vampire_filter_opts_full: int -> bool -> int -> Proof.state -> Thread.thread
wenzelm@28592
    33
  val spass: int -> Proof.state -> Thread.thread
wenzelm@28592
    34
  val eprover: int -> Proof.state -> Thread.thread
wenzelm@28592
    35
  val eprover_full: int -> Proof.state -> Thread.thread
wenzelm@28592
    36
  val vampire: int -> Proof.state -> Thread.thread
wenzelm@28592
    37
  val vampire_full: int -> Proof.state -> Thread.thread
wenzelm@28592
    38
end;
wenzelm@28592
    39
wenzelm@28592
    40
structure AtpWrapper: ATP_WRAPPER =
wenzelm@28592
    41
struct
wenzelm@28592
    42
  
wenzelm@28592
    43
  (* preferences for path and filename to problemfiles *)
wenzelm@28592
    44
  val destdir = ref "";   (*Empty means write files to /tmp*)
wenzelm@28592
    45
  val problem_name = ref "prob";
wenzelm@28592
    46
      
wenzelm@28592
    47
  (*Setting up a Thread for an external prover*)
wenzelm@28592
    48
  fun external_prover write_problem_files (cmd, args) check_success produce_answer subgoalno state =
wenzelm@28592
    49
    let
wenzelm@28592
    50
    val destdir' = ! destdir
wenzelm@28592
    51
    val problem_name' = ! problem_name
wenzelm@28592
    52
    val (ctxt, (chain_ths, goal)) = Proof.get_goal state
wenzelm@28592
    53
    (* path to unique problem file *)
wenzelm@28592
    54
    fun prob_pathname nr =
wenzelm@28592
    55
      let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ Int.toString nr)
wenzelm@28592
    56
      in if destdir' = "" then File.tmp_path probfile
wenzelm@28592
    57
        else if File.exists (Path.explode (destdir'))
wenzelm@28592
    58
        then Path.append  (Path.explode (destdir')) probfile
wenzelm@28592
    59
        else error ("No such directory: " ^ destdir')
wenzelm@28592
    60
      end
wenzelm@28592
    61
    (* write out problem file and call prover *)
wenzelm@28592
    62
    fun call_prover () =
wenzelm@28592
    63
      let
wenzelm@28592
    64
      val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
wenzelm@28592
    65
      val (filenames, thm_names_list) =
wenzelm@28592
    66
        write_problem_files prob_pathname (ctxt, chain_ths, goal)
wenzelm@28592
    67
      val thm_names = List.nth (thm_names_list, subgoalno - 1); (*(i-1)th element for i-th subgoal*)
wenzelm@28592
    68
wenzelm@28592
    69
      val cmdline =
wenzelm@28592
    70
        if File.exists cmd then File.shell_path cmd ^ " " ^ args
wenzelm@28592
    71
        else error ("Bad executable: " ^ Path.implode cmd);
wenzelm@28592
    72
      val (proof, rc) = system_out (cmdline ^ " " ^ List.nth (filenames, subgoalno - 1))
wenzelm@28592
    73
      val _ =
wenzelm@28592
    74
        if rc <> 0
wenzelm@28592
    75
        then warning ("Sledgehammer with command " ^ quote cmdline ^ " exited with " ^ Int.toString rc)
wenzelm@28592
    76
        else ()
wenzelm@28592
    77
      (* remove *temporary* files *)
wenzelm@28592
    78
      val _ = if destdir' = "" then app (fn file => OS.FileSys.remove file) filenames else ()
wenzelm@28592
    79
      in
wenzelm@28592
    80
        if check_success (proof, rc) then SOME (proof, thm_names, ctxt, goal, subgoalno)
wenzelm@28592
    81
        else NONE
wenzelm@28592
    82
      end
wenzelm@28592
    83
    in
wenzelm@28592
    84
      AtpManager.atp_thread call_prover produce_answer
wenzelm@28592
    85
    end;
wenzelm@28592
    86
wenzelm@28592
    87
    
wenzelm@28592
    88
  (*=========== TEMPLATES FOR AUTOMATIC PROVERS =================*)
wenzelm@28592
    89
wenzelm@28592
    90
  fun tptp_prover_filter_opts_full max_new theory_const full command sg =
wenzelm@28592
    91
    external_prover
wenzelm@28592
    92
    (ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const)
wenzelm@28592
    93
    command
wenzelm@28592
    94
    ResReconstruct.check_success_e_vamp_spass
wenzelm@28592
    95
    (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
wenzelm@28592
    96
    sg
wenzelm@28592
    97
    
wenzelm@28592
    98
  (* arbitrary atp with tptp input/output and problemfile as last argument*)
wenzelm@28592
    99
  fun tptp_prover_filter_opts max_new theory_const =
wenzelm@28592
   100
    tptp_prover_filter_opts_full max_new theory_const false;
wenzelm@28592
   101
  (* default settings*)  
wenzelm@28592
   102
  val tptp_prover = tptp_prover_filter_opts 60 true;
wenzelm@28592
   103
wenzelm@28592
   104
  (* for structured proofs: prover must support TSTP *)
wenzelm@28592
   105
  fun full_prover_filter_opts max_new theory_const =
wenzelm@28592
   106
    tptp_prover_filter_opts_full max_new theory_const true;
wenzelm@28592
   107
  (* default settings*)
wenzelm@28592
   108
  val full_prover = full_prover_filter_opts 60 true;
wenzelm@28592
   109
wenzelm@28592
   110
  fun vampire_filter_opts max_new theory_const = tptp_prover_filter_opts
wenzelm@28592
   111
    max_new theory_const
wenzelm@28592
   112
    (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*)
wenzelm@28592
   113
  (* default settings*)
wenzelm@28592
   114
  val vampire = vampire_filter_opts 60 false;
wenzelm@28592
   115
    
wenzelm@28592
   116
  (* a vampire for full proof output *)
wenzelm@28592
   117
  fun vampire_filter_opts_full max_new theory_const = full_prover_filter_opts
wenzelm@28592
   118
    max_new theory_const
wenzelm@28592
   119
    (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*)
wenzelm@28592
   120
  (* default settings*)
wenzelm@28592
   121
  val vampire_full = vampire_filter_opts 60 false;
wenzelm@28592
   122
wenzelm@28592
   123
  fun eprover_filter_opts max_new theory_const = tptp_prover_filter_opts
wenzelm@28592
   124
    max_new theory_const
wenzelm@28592
   125
    (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent")
wenzelm@28592
   126
  (* default settings *)
wenzelm@28592
   127
  val eprover = eprover_filter_opts 100 false;
wenzelm@28592
   128
    
wenzelm@28592
   129
  (* an E for full proof output*)
wenzelm@28592
   130
  fun eprover_filter_opts_full max_new theory_const = full_prover_filter_opts
wenzelm@28592
   131
    max_new theory_const
wenzelm@28592
   132
    (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent")
wenzelm@28592
   133
  (* default settings *)
wenzelm@28592
   134
  val eprover_full = eprover_filter_opts_full 100 false;
wenzelm@28592
   135
wenzelm@28592
   136
  fun spass_filter_opts max_new theory_const = external_prover
wenzelm@28592
   137
    (ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const)
wenzelm@28592
   138
    (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof")
wenzelm@28592
   139
    ResReconstruct.check_success_e_vamp_spass
wenzelm@28592
   140
    ResReconstruct.lemma_list_dfg
wenzelm@28592
   141
  (* default settings*)
wenzelm@28592
   142
  val spass = spass_filter_opts 40 true;
wenzelm@28592
   143
    
wenzelm@28592
   144
  (* remote prover invocation via SystemOnTPTP *)
wenzelm@28592
   145
  fun remote_prover_filter_opts max_new theory_const name command =
wenzelm@28592
   146
    tptp_prover_filter_opts max_new theory_const
wenzelm@28592
   147
    (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ command)
wenzelm@28592
   148
  val remote_prover = remote_prover_filter_opts 60 false
wenzelm@28592
   149
wenzelm@28592
   150
end;