src/HOL/Tools/ATP_Manager/atp_wrapper.ML
author boehmes
Mon Aug 31 15:29:26 2009 +0200 (2009-08-31)
changeset 32458 de6834b20e9e
parent 32451 8f0dc876fb1b
child 32510 1b56f8b1e5cc
permissions -rw-r--r--
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
wenzelm@32327
     1
(*  Title:      HOL/Tools/ATP_Manager/atp_wrapper.ML
wenzelm@28592
     2
    Author:     Fabian Immler, TU Muenchen
wenzelm@28592
     3
wenzelm@28592
     4
Wrapper functions for external ATPs.
wenzelm@28592
     5
*)
wenzelm@28592
     6
wenzelm@28592
     7
signature ATP_WRAPPER =
wenzelm@28592
     8
sig
wenzelm@28592
     9
  val destdir: string ref
wenzelm@28592
    10
  val problem_name: string ref
wenzelm@28596
    11
  val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
wenzelm@28596
    12
  val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
wenzelm@28596
    13
  val tptp_prover: Path.T * string -> AtpManager.prover
wenzelm@28596
    14
  val full_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
wenzelm@28596
    15
  val full_prover: Path.T * string  -> AtpManager.prover
wenzelm@28596
    16
  val vampire_opts: int -> bool -> AtpManager.prover
wenzelm@28596
    17
  val vampire: AtpManager.prover
wenzelm@28596
    18
  val vampire_opts_full: int -> bool -> AtpManager.prover
wenzelm@28596
    19
  val vampire_full: AtpManager.prover
wenzelm@28596
    20
  val eprover_opts: int -> bool  -> AtpManager.prover
wenzelm@28596
    21
  val eprover: AtpManager.prover
wenzelm@28596
    22
  val eprover_opts_full: int -> bool -> AtpManager.prover
wenzelm@28596
    23
  val eprover_full: AtpManager.prover
wenzelm@28596
    24
  val spass_opts: int -> bool  -> AtpManager.prover
wenzelm@28596
    25
  val spass: AtpManager.prover
immler@31835
    26
  val remote_prover_opts: int -> bool -> string -> string -> AtpManager.prover
immler@31835
    27
  val remote_prover: string -> string -> AtpManager.prover
immler@31835
    28
  val refresh_systems: unit -> unit
wenzelm@28592
    29
end;
wenzelm@28592
    30
wenzelm@28592
    31
structure AtpWrapper: ATP_WRAPPER =
wenzelm@28592
    32
struct
wenzelm@28596
    33
wenzelm@28596
    34
(** generic ATP wrapper **)
wenzelm@28596
    35
wenzelm@28596
    36
(* global hooks for writing problemfiles *)
wenzelm@28596
    37
wenzelm@28596
    38
val destdir = ref "";   (*Empty means write files to /tmp*)
wenzelm@28596
    39
val problem_name = ref "prob";
wenzelm@28596
    40
wenzelm@28596
    41
wenzelm@28596
    42
(* basic template *)
wenzelm@28596
    43
boehmes@32458
    44
fun with_path cleanup after f path =
boehmes@32458
    45
  Exn.capture f path
boehmes@32458
    46
  |> tap (fn _ => cleanup path)
boehmes@32458
    47
  |> Exn.release
boehmes@32458
    48
  |> tap (after path)
boehmes@32458
    49
immler@31409
    50
fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer
immler@31752
    51
  timeout axiom_clauses filtered_clauses name subgoalno goal =
wenzelm@28596
    52
  let
wenzelm@28596
    53
    (* path to unique problem file *)
wenzelm@28592
    54
    val destdir' = ! destdir
wenzelm@28592
    55
    val problem_name' = ! problem_name
wenzelm@28592
    56
    fun prob_pathname nr =
wenzelm@28596
    57
      let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ string_of_int nr)
wenzelm@28592
    58
      in if destdir' = "" then File.tmp_path probfile
wenzelm@28592
    59
        else if File.exists (Path.explode (destdir'))
wenzelm@28592
    60
        then Path.append  (Path.explode (destdir')) probfile
wenzelm@28592
    61
        else error ("No such directory: " ^ destdir')
wenzelm@28592
    62
      end
wenzelm@28596
    63
immler@31750
    64
    (* get clauses and prepare them for writing *)
immler@30537
    65
    val (ctxt, (chain_ths, th)) = goal
immler@30536
    66
    val thy = ProofContext.theory_of ctxt
wenzelm@28596
    67
    val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
wenzelm@32257
    68
    val goal_cls = #1 (ResAxioms.neg_conjecture_clauses ctxt th subgoalno)
wenzelm@32091
    69
    val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm ctxt th)) goal_cls
immler@31752
    70
    val the_filtered_clauses =
immler@31752
    71
      case filtered_clauses of
immler@31752
    72
          NONE => relevance_filter goal goal_cls
immler@31752
    73
        | SOME fcls => fcls
immler@31409
    74
    val the_axiom_clauses =
immler@31409
    75
      case axiom_clauses of
immler@31752
    76
          NONE => the_filtered_clauses
immler@31409
    77
        | SOME axcls => axcls
wenzelm@32257
    78
    val (thm_names, clauses) =
wenzelm@32257
    79
      preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
immler@31750
    80
immler@31750
    81
    (* write out problem file and call prover *)
boehmes@32458
    82
    fun cmd_line probfile = space_implode " " ["exec", File.shell_path cmd,
boehmes@32458
    83
      args, File.platform_path probfile]
boehmes@32458
    84
    fun run_on probfile =
boehmes@32458
    85
      if File.exists cmd
boehmes@32458
    86
      then writer probfile clauses |> pair (system_out (cmd_line probfile))
boehmes@32458
    87
      else error ("Bad executable: " ^ Path.implode cmd)
wenzelm@28592
    88
immler@31751
    89
    (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
boehmes@32458
    90
    fun cleanup probfile = if destdir' = "" then File.rm probfile else ()
boehmes@32458
    91
    fun export probfile ((proof, _), _) = if destdir' = "" then ()
immler@31838
    92
      else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
wenzelm@32257
    93
boehmes@32458
    94
    val ((proof, rc), conj_pos) = with_path cleanup export run_on
boehmes@32458
    95
      (prob_pathname subgoalno)
boehmes@32458
    96
immler@29590
    97
    (* check for success and print out some information on failure *)
immler@29590
    98
    val failure = find_failure proof
immler@29597
    99
    val success = rc = 0 andalso is_none failure
wenzelm@28596
   100
    val message =
boehmes@32451
   101
      if is_some failure then ("External prover failed.", [])
boehmes@32451
   102
      else if rc <> 0 then ("External prover failed: " ^ proof, [])
boehmes@32451
   103
      else apfst (fn s => "Try this command: " ^ s)
boehmes@32451
   104
        (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno))
immler@31411
   105
    val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
immler@31752
   106
  in (success, message, proof, thm_names, the_filtered_clauses) end;
wenzelm@28596
   107
wenzelm@28592
   108
wenzelm@28596
   109
wenzelm@28596
   110
(** common provers **)
wenzelm@28596
   111
wenzelm@28596
   112
(* generic TPTP-based provers *)
wenzelm@28596
   113
immler@31752
   114
fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses fcls name n goal =
wenzelm@28596
   115
  external_prover
immler@31409
   116
  (ResAtp.get_relevant max_new theory_const)
immler@31409
   117
  (ResAtp.prepare_clauses false)
nipkow@31791
   118
  (ResHolClause.tptp_write_file (AtpManager.get_full_types()))
immler@31409
   119
  command
immler@31409
   120
  ResReconstruct.find_failure
immler@31840
   121
  (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list false)
immler@31752
   122
  timeout ax_clauses fcls name n goal;
wenzelm@28596
   123
wenzelm@28596
   124
(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
wenzelm@28596
   125
fun tptp_prover_opts max_new theory_const =
wenzelm@28596
   126
  tptp_prover_opts_full max_new theory_const false;
wenzelm@28596
   127
wenzelm@31368
   128
fun tptp_prover x = tptp_prover_opts 60 true x;
wenzelm@28596
   129
wenzelm@28596
   130
(*for structured proofs: prover must support TSTP*)
wenzelm@28596
   131
fun full_prover_opts max_new theory_const =
wenzelm@28596
   132
  tptp_prover_opts_full max_new theory_const true;
wenzelm@28596
   133
wenzelm@31368
   134
fun full_prover x = full_prover_opts 60 true x;
wenzelm@28596
   135
wenzelm@28592
   136
wenzelm@28596
   137
(* Vampire *)
wenzelm@28596
   138
wenzelm@28596
   139
(*NB: Vampire does not work without explicit timelimit*)
wenzelm@28596
   140
immler@29593
   141
fun vampire_opts max_new theory_const timeout = tptp_prover_opts
wenzelm@28596
   142
  max_new theory_const
immler@29593
   143
  (Path.explode "$VAMPIRE_HOME/vampire",
wenzelm@32257
   144
    ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
immler@29593
   145
  timeout;
wenzelm@28596
   146
wenzelm@28596
   147
val vampire = vampire_opts 60 false;
wenzelm@28596
   148
immler@29593
   149
fun vampire_opts_full max_new theory_const timeout = full_prover_opts
wenzelm@28596
   150
  max_new theory_const
immler@29593
   151
  (Path.explode "$VAMPIRE_HOME/vampire",
wenzelm@32257
   152
    ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
immler@29593
   153
  timeout;
wenzelm@28596
   154
immler@31832
   155
val vampire_full = vampire_opts_full 60 false;
wenzelm@28596
   156
wenzelm@28592
   157
wenzelm@28596
   158
(* E prover *)
wenzelm@28596
   159
immler@30536
   160
fun eprover_opts max_new theory_const timeout = tptp_prover_opts
wenzelm@28596
   161
  max_new theory_const
immler@30536
   162
  (Path.explode "$E_HOME/eproof",
immler@30536
   163
    "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
immler@30536
   164
  timeout;
wenzelm@28596
   165
wenzelm@28596
   166
val eprover = eprover_opts 100 false;
wenzelm@28596
   167
immler@30536
   168
fun eprover_opts_full max_new theory_const timeout = full_prover_opts
wenzelm@28596
   169
  max_new theory_const
immler@30536
   170
  (Path.explode "$E_HOME/eproof",
immler@30536
   171
    "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
immler@30536
   172
  timeout;
wenzelm@28596
   173
wenzelm@28596
   174
val eprover_full = eprover_opts_full 100 false;
wenzelm@28596
   175
wenzelm@28596
   176
wenzelm@28596
   177
(* SPASS *)
wenzelm@28592
   178
immler@31752
   179
fun spass_opts max_new theory_const timeout ax_clauses fcls name n goal = external_prover
immler@31409
   180
  (ResAtp.get_relevant max_new theory_const)
immler@31409
   181
  (ResAtp.prepare_clauses true)
nipkow@31791
   182
  (ResHolClause.dfg_write_file (AtpManager.get_full_types()))
immler@30536
   183
  (Path.explode "$SPASS_HOME/SPASS",
wenzelm@32257
   184
    "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^
wenzelm@32257
   185
      string_of_int timeout)
immler@30874
   186
  ResReconstruct.find_failure
immler@31840
   187
  (ResReconstruct.lemma_list true)
immler@31752
   188
  timeout ax_clauses fcls name n goal;
wenzelm@28596
   189
wenzelm@28596
   190
val spass = spass_opts 40 true;
wenzelm@28592
   191
wenzelm@28596
   192
wenzelm@28596
   193
(* remote prover invocation via SystemOnTPTP *)
wenzelm@28596
   194
immler@31835
   195
val systems =
immler@31835
   196
  Synchronized.var "atp_wrapper_systems" ([]: string list);
immler@31835
   197
immler@31835
   198
fun get_systems () =
immler@31835
   199
  let
wenzelm@32327
   200
    val (answer, rc) = system_out ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w")
immler@31835
   201
  in
wenzelm@32327
   202
    if rc <> 0 then error ("Failed to get available systems from SystemOnTPTP:\n" ^ answer)
immler@31835
   203
    else split_lines answer
immler@31835
   204
  end;
immler@31835
   205
immler@31835
   206
fun refresh_systems () = Synchronized.change systems (fn _ =>
wenzelm@32257
   207
  get_systems ());
immler@31835
   208
immler@31835
   209
fun get_system prefix = Synchronized.change_result systems (fn systems =>
immler@31835
   210
  let val systems = if null systems then get_systems() else systems
immler@31835
   211
  in (find_first (String.isPrefix prefix) systems, systems) end);
immler@31835
   212
immler@31835
   213
fun remote_prover_opts max_new theory_const args prover_prefix timeout =
wenzelm@32257
   214
  let val sys =
wenzelm@32257
   215
    case get_system prover_prefix of
immler@31835
   216
      NONE => error ("No system like " ^ quote prover_prefix ^ " at SystemOnTPTP")
immler@31835
   217
    | SOME sys => sys
immler@31835
   218
  in tptp_prover_opts max_new theory_const
wenzelm@32327
   219
    (Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
wenzelm@32257
   220
      args ^ " -t " ^ string_of_int timeout ^ " -s " ^ sys) timeout
wenzelm@32257
   221
  end;
wenzelm@28596
   222
wenzelm@28596
   223
val remote_prover = remote_prover_opts 60 false;
wenzelm@28592
   224
wenzelm@28592
   225
end;
immler@30536
   226