src/HOL/Tools/atp_wrapper.ML
author immler@in.tum.de
Mon Jun 22 17:07:09 2009 +0200 (2009-06-22)
changeset 31752 19a5f1c8a844
parent 31751 fda2cf4fef58
child 31791 c9a1caf218c8
permissions -rw-r--r--
use results of relevance-filter to determine additional clauses;
(needed for minimize to be able to prove the same problems as sledgehammer)
wenzelm@28592
     1
(*  Title:      HOL/Tools/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@29590
    26
  val remote_prover_opts: int -> bool -> string -> AtpManager.prover
immler@29590
    27
  val remote_prover: string -> AtpManager.prover
wenzelm@28592
    28
end;
wenzelm@28592
    29
wenzelm@28592
    30
structure AtpWrapper: ATP_WRAPPER =
wenzelm@28592
    31
struct
wenzelm@28596
    32
wenzelm@28596
    33
(** generic ATP wrapper **)
wenzelm@28596
    34
wenzelm@28596
    35
(* global hooks for writing problemfiles *)
wenzelm@28596
    36
wenzelm@28596
    37
val destdir = ref "";   (*Empty means write files to /tmp*)
wenzelm@28596
    38
val problem_name = ref "prob";
wenzelm@28596
    39
wenzelm@28596
    40
wenzelm@28596
    41
(* basic template *)
wenzelm@28596
    42
immler@31409
    43
fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer
immler@31752
    44
  timeout axiom_clauses filtered_clauses name subgoalno goal =
wenzelm@28596
    45
  let
wenzelm@28596
    46
    (* path to unique problem file *)
wenzelm@28592
    47
    val destdir' = ! destdir
wenzelm@28592
    48
    val problem_name' = ! problem_name
wenzelm@28592
    49
    fun prob_pathname nr =
wenzelm@28596
    50
      let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ string_of_int nr)
wenzelm@28592
    51
      in if destdir' = "" then File.tmp_path probfile
wenzelm@28592
    52
        else if File.exists (Path.explode (destdir'))
wenzelm@28592
    53
        then Path.append  (Path.explode (destdir')) probfile
wenzelm@28592
    54
        else error ("No such directory: " ^ destdir')
wenzelm@28592
    55
      end
wenzelm@28596
    56
immler@31750
    57
    (* get clauses and prepare them for writing *)
immler@30537
    58
    val (ctxt, (chain_ths, th)) = goal
immler@30536
    59
    val thy = ProofContext.theory_of ctxt
wenzelm@28596
    60
    val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
immler@31409
    61
    val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno)
immler@31409
    62
      handle THM ("assume: variables", _, _) =>
immler@31409
    63
        error "Sledgehammer: Goal contains type variables (TVars)"
immler@31409
    64
    val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls
immler@31752
    65
    val the_filtered_clauses =
immler@31752
    66
      case filtered_clauses of
immler@31752
    67
          NONE => relevance_filter goal goal_cls
immler@31752
    68
        | SOME fcls => fcls
immler@31409
    69
    val the_axiom_clauses =
immler@31409
    70
      case axiom_clauses of
immler@31752
    71
          NONE => the_filtered_clauses
immler@31409
    72
        | SOME axcls => axcls
immler@31752
    73
    val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
immler@31750
    74
immler@31750
    75
    (* write out problem file and call prover *)
immler@31750
    76
    val probfile = prob_pathname subgoalno
immler@31750
    77
    val fname = File.platform_path probfile
immler@31752
    78
    val _ = writer fname clauses
wenzelm@28596
    79
    val cmdline =
wenzelm@30899
    80
      if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args
wenzelm@28596
    81
      else error ("Bad executable: " ^ Path.implode cmd)
immler@30536
    82
    val (proof, rc) = system_out (cmdline ^ " " ^ fname)
wenzelm@28592
    83
immler@31751
    84
    (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
immler@31751
    85
    val _ =
immler@31751
    86
      if destdir' = "" then OS.FileSys.remove fname
immler@31751
    87
      else
immler@31751
    88
        let val out = TextIO.openOut (fname ^ "_proof")
immler@31751
    89
        val _ = TextIO.output (out, proof)
immler@31751
    90
        in TextIO.closeOut out end
immler@29590
    91
    
immler@29590
    92
    (* check for success and print out some information on failure *)
immler@29590
    93
    val failure = find_failure proof
immler@29597
    94
    val success = rc = 0 andalso is_none failure
wenzelm@28596
    95
    val message =
wenzelm@30896
    96
      if is_some failure then "External prover failed."
wenzelm@30896
    97
      else if rc <> 0 then "External prover failed: " ^ proof
immler@31037
    98
      else "Try this command: " ^ produce_answer name (proof, thm_names, ctxt, th, subgoalno)
immler@31411
    99
    val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
immler@31752
   100
  in (success, message, proof, thm_names, the_filtered_clauses) end;
wenzelm@28596
   101
wenzelm@28592
   102
wenzelm@28596
   103
wenzelm@28596
   104
(** common provers **)
wenzelm@28596
   105
wenzelm@28596
   106
(* generic TPTP-based provers *)
wenzelm@28596
   107
immler@31752
   108
fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses fcls name n goal =
wenzelm@28596
   109
  external_prover
immler@31409
   110
  (ResAtp.get_relevant max_new theory_const)
immler@31409
   111
  (ResAtp.prepare_clauses false)
immler@31409
   112
  (ResHolClause.tptp_write_file)
immler@31409
   113
  command
immler@31409
   114
  ResReconstruct.find_failure
immler@31409
   115
  (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
immler@31752
   116
  timeout ax_clauses fcls name n goal;
wenzelm@28596
   117
wenzelm@28596
   118
(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
wenzelm@28596
   119
fun tptp_prover_opts max_new theory_const =
wenzelm@28596
   120
  tptp_prover_opts_full max_new theory_const false;
wenzelm@28596
   121
wenzelm@31368
   122
fun tptp_prover x = tptp_prover_opts 60 true x;
wenzelm@28596
   123
wenzelm@28596
   124
(*for structured proofs: prover must support TSTP*)
wenzelm@28596
   125
fun full_prover_opts max_new theory_const =
wenzelm@28596
   126
  tptp_prover_opts_full max_new theory_const true;
wenzelm@28596
   127
wenzelm@31368
   128
fun full_prover x = full_prover_opts 60 true x;
wenzelm@28596
   129
wenzelm@28592
   130
wenzelm@28596
   131
(* Vampire *)
wenzelm@28596
   132
wenzelm@28596
   133
(*NB: Vampire does not work without explicit timelimit*)
wenzelm@28596
   134
immler@29593
   135
fun vampire_opts max_new theory_const timeout = tptp_prover_opts
wenzelm@28596
   136
  max_new theory_const
immler@29593
   137
  (Path.explode "$VAMPIRE_HOME/vampire",
immler@29593
   138
               ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
immler@29593
   139
  timeout;
wenzelm@28596
   140
wenzelm@28596
   141
val vampire = vampire_opts 60 false;
wenzelm@28596
   142
immler@29593
   143
fun vampire_opts_full max_new theory_const timeout = full_prover_opts
wenzelm@28596
   144
  max_new theory_const
immler@29593
   145
  (Path.explode "$VAMPIRE_HOME/vampire",
immler@29593
   146
               ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
immler@29593
   147
  timeout;
wenzelm@28596
   148
wenzelm@28596
   149
val vampire_full = vampire_opts 60 false;
wenzelm@28596
   150
wenzelm@28592
   151
wenzelm@28596
   152
(* E prover *)
wenzelm@28596
   153
immler@30536
   154
fun eprover_opts max_new theory_const timeout = tptp_prover_opts
wenzelm@28596
   155
  max_new theory_const
immler@30536
   156
  (Path.explode "$E_HOME/eproof",
immler@30536
   157
    "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
immler@30536
   158
  timeout;
wenzelm@28596
   159
wenzelm@28596
   160
val eprover = eprover_opts 100 false;
wenzelm@28596
   161
immler@30536
   162
fun eprover_opts_full max_new theory_const timeout = full_prover_opts
wenzelm@28596
   163
  max_new theory_const
immler@30536
   164
  (Path.explode "$E_HOME/eproof",
immler@30536
   165
    "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
immler@30536
   166
  timeout;
wenzelm@28596
   167
wenzelm@28596
   168
val eprover_full = eprover_opts_full 100 false;
wenzelm@28596
   169
wenzelm@28596
   170
wenzelm@28596
   171
(* SPASS *)
wenzelm@28592
   172
immler@31752
   173
fun spass_opts max_new theory_const timeout ax_clauses fcls name n goal = external_prover
immler@31409
   174
  (ResAtp.get_relevant max_new theory_const)
immler@31409
   175
  (ResAtp.prepare_clauses true)
immler@31409
   176
  ResHolClause.dfg_write_file
immler@30536
   177
  (Path.explode "$SPASS_HOME/SPASS",
immler@30536
   178
    "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
immler@30874
   179
  ResReconstruct.find_failure
immler@30536
   180
  ResReconstruct.lemma_list_dfg
immler@31752
   181
  timeout ax_clauses fcls name n goal;
wenzelm@28596
   182
wenzelm@28596
   183
val spass = spass_opts 40 true;
wenzelm@28592
   184
wenzelm@28596
   185
wenzelm@28596
   186
(* remote prover invocation via SystemOnTPTP *)
wenzelm@28596
   187
immler@29593
   188
fun remote_prover_opts max_new theory_const args timeout =
wenzelm@28596
   189
  tptp_prover_opts max_new theory_const
wenzelm@30979
   190
  (Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP", args ^ " -t " ^ string_of_int timeout)
immler@29593
   191
  timeout;
wenzelm@28596
   192
wenzelm@28596
   193
val remote_prover = remote_prover_opts 60 false;
wenzelm@28592
   194
wenzelm@28592
   195
end;
immler@30536
   196
immler@30536
   197