src/HOL/Tools/atp_wrapper.ML
author immler@in.tum.de
Tue Jan 20 16:05:57 2009 +0100 (2009-01-20)
changeset 29590 479a2fce65e6
parent 29587 96599d8d8268
child 29593 7b73bd578db2
permissions -rw-r--r--
modified remote script;
modified handling of errors
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
  val destdir: string ref
wenzelm@28592
    11
  val problem_name: string ref
wenzelm@28592
    12
  val external_prover:
wenzelm@28592
    13
    ((int -> Path.T) -> Proof.context * thm list * thm -> string list * ResHolClause.axiom_name Vector.vector list) ->
wenzelm@28592
    14
    Path.T * string ->
immler@29590
    15
    (string -> string option) ->
wenzelm@28592
    16
    (string * string vector * Proof.context * thm * int -> string) ->
wenzelm@28596
    17
    AtpManager.prover
wenzelm@28596
    18
  val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
wenzelm@28596
    19
  val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
wenzelm@28596
    20
  val tptp_prover: Path.T * string -> AtpManager.prover
wenzelm@28596
    21
  val full_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
wenzelm@28596
    22
  val full_prover: Path.T * string  -> AtpManager.prover
wenzelm@28596
    23
  val vampire_opts: int -> bool -> AtpManager.prover
wenzelm@28596
    24
  val vampire: AtpManager.prover
wenzelm@28596
    25
  val vampire_opts_full: int -> bool -> AtpManager.prover
wenzelm@28596
    26
  val vampire_full: AtpManager.prover
wenzelm@28596
    27
  val eprover_opts: int -> bool  -> AtpManager.prover
wenzelm@28596
    28
  val eprover: AtpManager.prover
wenzelm@28596
    29
  val eprover_opts_full: int -> bool -> AtpManager.prover
wenzelm@28596
    30
  val eprover_full: AtpManager.prover
wenzelm@28596
    31
  val spass_opts: int -> bool  -> AtpManager.prover
wenzelm@28596
    32
  val spass: AtpManager.prover
immler@29590
    33
  val remote_prover_opts: int -> bool -> string -> AtpManager.prover
immler@29590
    34
  val remote_prover: string -> AtpManager.prover
wenzelm@28592
    35
end;
wenzelm@28592
    36
wenzelm@28592
    37
structure AtpWrapper: ATP_WRAPPER =
wenzelm@28592
    38
struct
wenzelm@28596
    39
wenzelm@28596
    40
(** generic ATP wrapper **)
wenzelm@28596
    41
wenzelm@28596
    42
(* global hooks for writing problemfiles *)
wenzelm@28596
    43
wenzelm@28596
    44
val destdir = ref "";   (*Empty means write files to /tmp*)
wenzelm@28596
    45
val problem_name = ref "prob";
wenzelm@28596
    46
wenzelm@28596
    47
wenzelm@28596
    48
(* basic template *)
wenzelm@28596
    49
immler@29590
    50
fun external_prover write_problem_files (cmd, args) find_failure produce_answer subgoalno state =
wenzelm@28596
    51
  let
wenzelm@28596
    52
    (* path to unique problem file *)
wenzelm@28592
    53
    val destdir' = ! destdir
wenzelm@28592
    54
    val problem_name' = ! problem_name
wenzelm@28592
    55
    fun prob_pathname nr =
wenzelm@28596
    56
      let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ string_of_int nr)
wenzelm@28592
    57
      in if destdir' = "" then File.tmp_path probfile
wenzelm@28592
    58
        else if File.exists (Path.explode (destdir'))
wenzelm@28592
    59
        then Path.append  (Path.explode (destdir')) probfile
wenzelm@28592
    60
        else error ("No such directory: " ^ destdir')
wenzelm@28592
    61
      end
wenzelm@28596
    62
wenzelm@28592
    63
    (* write out problem file and call prover *)
wenzelm@28596
    64
    val (ctxt, (chain_ths, goal)) = Proof.get_goal state
wenzelm@28596
    65
    val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
wenzelm@28596
    66
    val (filenames, thm_names_list) = write_problem_files prob_pathname (ctxt, chain_ths, goal)
wenzelm@28596
    67
    val thm_names = nth thm_names_list (subgoalno - 1)
wenzelm@28596
    68
wenzelm@28596
    69
    val cmdline =
wenzelm@28596
    70
      if File.exists cmd then File.shell_path cmd ^ " " ^ args
wenzelm@28596
    71
      else error ("Bad executable: " ^ Path.implode cmd)
wenzelm@28596
    72
    val (proof, rc) = system_out (cmdline ^ " " ^ nth filenames (subgoalno - 1))
wenzelm@28592
    73
wenzelm@28596
    74
    (* remove *temporary* files *)
wenzelm@28596
    75
    val _ = if destdir' = "" then List.app OS.FileSys.remove filenames else ()
immler@29590
    76
    
immler@29590
    77
    (* check for success and print out some information on failure *)
immler@29590
    78
    val failure = find_failure proof
immler@29590
    79
    val success = (rc = 0) andalso (not (isSome failure))
wenzelm@28596
    80
    val message =
immler@29590
    81
      if isSome failure then "Could not prove: " ^ the failure
immler@29590
    82
      else if rc <> 0
immler@29590
    83
      then "Exited with return code " ^ string_of_int rc ^ ": " ^ proof 
immler@29590
    84
      else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
wenzelm@28596
    85
  in (success, message) end;
wenzelm@28596
    86
wenzelm@28592
    87
wenzelm@28596
    88
wenzelm@28596
    89
(** common provers **)
wenzelm@28596
    90
wenzelm@28596
    91
(* generic TPTP-based provers *)
wenzelm@28596
    92
wenzelm@28596
    93
fun tptp_prover_opts_full max_new theory_const full command =
wenzelm@28596
    94
  external_prover
wenzelm@28592
    95
    (ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const)
wenzelm@28592
    96
    command
immler@29590
    97
    ResReconstruct.find_failure_e_vamp_spass
wenzelm@28596
    98
    (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp);
wenzelm@28596
    99
wenzelm@28596
   100
(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
wenzelm@28596
   101
fun tptp_prover_opts max_new theory_const =
wenzelm@28596
   102
  tptp_prover_opts_full max_new theory_const false;
wenzelm@28596
   103
wenzelm@28596
   104
val tptp_prover = tptp_prover_opts 60 true;
wenzelm@28596
   105
wenzelm@28596
   106
(*for structured proofs: prover must support TSTP*)
wenzelm@28596
   107
fun full_prover_opts max_new theory_const =
wenzelm@28596
   108
  tptp_prover_opts_full max_new theory_const true;
wenzelm@28596
   109
wenzelm@28596
   110
val full_prover = full_prover_opts 60 true;
wenzelm@28596
   111
wenzelm@28592
   112
wenzelm@28596
   113
(* Vampire *)
wenzelm@28596
   114
wenzelm@28596
   115
(*NB: Vampire does not work without explicit timelimit*)
wenzelm@28596
   116
wenzelm@28596
   117
fun vampire_opts max_new theory_const = tptp_prover_opts
wenzelm@28596
   118
  max_new theory_const
wenzelm@28596
   119
  (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600");
wenzelm@28596
   120
wenzelm@28596
   121
val vampire = vampire_opts 60 false;
wenzelm@28596
   122
wenzelm@28596
   123
fun vampire_opts_full max_new theory_const = full_prover_opts
wenzelm@28596
   124
  max_new theory_const
wenzelm@28596
   125
  (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600");
wenzelm@28596
   126
wenzelm@28596
   127
val vampire_full = vampire_opts 60 false;
wenzelm@28596
   128
wenzelm@28592
   129
wenzelm@28596
   130
(* E prover *)
wenzelm@28596
   131
wenzelm@28596
   132
fun eprover_opts max_new theory_const = tptp_prover_opts
wenzelm@28596
   133
  max_new theory_const
wenzelm@28596
   134
  (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent");
wenzelm@28596
   135
wenzelm@28596
   136
val eprover = eprover_opts 100 false;
wenzelm@28596
   137
wenzelm@28596
   138
fun eprover_opts_full max_new theory_const = full_prover_opts
wenzelm@28596
   139
  max_new theory_const
wenzelm@28596
   140
  (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent");
wenzelm@28596
   141
wenzelm@28596
   142
val eprover_full = eprover_opts_full 100 false;
wenzelm@28596
   143
wenzelm@28596
   144
wenzelm@28596
   145
(* SPASS *)
wenzelm@28592
   146
wenzelm@28596
   147
fun spass_opts max_new theory_const = external_prover
wenzelm@28596
   148
  (ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const)
wenzelm@28596
   149
  (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof")
immler@29590
   150
  ResReconstruct.find_failure_e_vamp_spass
wenzelm@28596
   151
  ResReconstruct.lemma_list_dfg;
wenzelm@28596
   152
wenzelm@28596
   153
val spass = spass_opts 40 true;
wenzelm@28592
   154
wenzelm@28596
   155
wenzelm@28596
   156
(* remote prover invocation via SystemOnTPTP *)
wenzelm@28596
   157
immler@29590
   158
fun remote_prover_opts max_new theory_const args =
wenzelm@28596
   159
  tptp_prover_opts max_new theory_const
immler@29590
   160
  (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", args);
wenzelm@28596
   161
wenzelm@28596
   162
val remote_prover = remote_prover_opts 60 false;
wenzelm@28592
   163
wenzelm@28592
   164
end;