src/HOL/Tools/atp_wrapper.ML
author immler@in.tum.de
Wed Jun 03 16:56:41 2009 +0200 (2009-06-03)
changeset 31409 d8537ba165b5
parent 31368 763f4b0fd579
child 31410 c231efe693ce
permissions -rw-r--r--
split preparing clauses and writing problemfile;
included results of count_constants in return-type of prover;
optionally pass counted constants to prover;
removed unused external_prover from signature
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@31409
    44
  timeout axiom_clauses const_counts 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
wenzelm@28592
    57
    (* write out problem file and call prover *)
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@30536
    61
    val probfile = prob_pathname subgoalno
immler@30536
    62
    val fname = File.platform_path probfile
immler@31409
    63
    val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno)
immler@31409
    64
      handle THM ("assume: variables", _, _) =>
immler@31409
    65
        error "Sledgehammer: Goal contains type variables (TVars)"
immler@31409
    66
    val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls
immler@31409
    67
    val the_axiom_clauses =
immler@31409
    68
      case axiom_clauses of
immler@31409
    69
          NONE => relevance_filter goal goal_cls
immler@31409
    70
        | SOME axcls => axcls
immler@31409
    71
    val (thm_names, clauses) = preparer goal_cls the_axiom_clauses thy
immler@31409
    72
    val the_const_counts = case const_counts of
immler@31409
    73
      NONE =>
immler@31409
    74
        ResHolClause.count_constants(
immler@31409
    75
          case axiom_clauses of
immler@31409
    76
            NONE => clauses
immler@31409
    77
            | SOME axcls => #2(preparer goal_cls (relevance_filter goal goal_cls) thy)
immler@31409
    78
          )
immler@31409
    79
      | SOME ccs => ccs
immler@31409
    80
    val _ = writer fname the_const_counts clauses
wenzelm@28596
    81
    val cmdline =
wenzelm@30899
    82
      if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args
wenzelm@28596
    83
      else error ("Bad executable: " ^ Path.implode cmd)
immler@30536
    84
    val (proof, rc) = system_out (cmdline ^ " " ^ fname)
wenzelm@28592
    85
wenzelm@28596
    86
    (* remove *temporary* files *)
immler@30536
    87
    val _ = if destdir' = "" then OS.FileSys.remove fname else ()
immler@29590
    88
    
immler@29590
    89
    (* check for success and print out some information on failure *)
immler@29590
    90
    val failure = find_failure proof
immler@29597
    91
    val success = rc = 0 andalso is_none failure
wenzelm@28596
    92
    val message =
wenzelm@30896
    93
      if is_some failure then "External prover failed."
wenzelm@30896
    94
      else if rc <> 0 then "External prover failed: " ^ proof
immler@31037
    95
      else "Try this command: " ^ produce_answer name (proof, thm_names, ctxt, th, subgoalno)
immler@30535
    96
wenzelm@30896
    97
    val _ =
wenzelm@30896
    98
      if is_some failure
immler@30015
    99
      then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof)
immler@30015
   100
      else ()
wenzelm@30896
   101
    val _ =
wenzelm@30896
   102
      if rc <> 0
immler@30015
   103
      then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof)
immler@30015
   104
      else ()
immler@31409
   105
  in (success, message, proof, thm_names, the_const_counts) end;
wenzelm@28596
   106
wenzelm@28592
   107
wenzelm@28596
   108
wenzelm@28596
   109
(** common provers **)
wenzelm@28596
   110
wenzelm@28596
   111
(* generic TPTP-based provers *)
wenzelm@28596
   112
immler@31409
   113
fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses ccs name n goal =
wenzelm@28596
   114
  external_prover
immler@31409
   115
  (ResAtp.get_relevant max_new theory_const)
immler@31409
   116
  (ResAtp.prepare_clauses false)
immler@31409
   117
  (ResHolClause.tptp_write_file)
immler@31409
   118
  command
immler@31409
   119
  ResReconstruct.find_failure
immler@31409
   120
  (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
immler@31409
   121
  timeout ax_clauses ccs name n goal;
wenzelm@28596
   122
wenzelm@28596
   123
(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
wenzelm@28596
   124
fun tptp_prover_opts max_new theory_const =
wenzelm@28596
   125
  tptp_prover_opts_full max_new theory_const false;
wenzelm@28596
   126
wenzelm@31368
   127
fun tptp_prover x = tptp_prover_opts 60 true x;
wenzelm@28596
   128
wenzelm@28596
   129
(*for structured proofs: prover must support TSTP*)
wenzelm@28596
   130
fun full_prover_opts max_new theory_const =
wenzelm@28596
   131
  tptp_prover_opts_full max_new theory_const true;
wenzelm@28596
   132
wenzelm@31368
   133
fun full_prover x = full_prover_opts 60 true x;
wenzelm@28596
   134
wenzelm@28592
   135
wenzelm@28596
   136
(* Vampire *)
wenzelm@28596
   137
wenzelm@28596
   138
(*NB: Vampire does not work without explicit timelimit*)
wenzelm@28596
   139
immler@29593
   140
fun vampire_opts max_new theory_const timeout = tptp_prover_opts
wenzelm@28596
   141
  max_new theory_const
immler@29593
   142
  (Path.explode "$VAMPIRE_HOME/vampire",
immler@29593
   143
               ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
immler@29593
   144
  timeout;
wenzelm@28596
   145
wenzelm@28596
   146
val vampire = vampire_opts 60 false;
wenzelm@28596
   147
immler@29593
   148
fun vampire_opts_full max_new theory_const timeout = full_prover_opts
wenzelm@28596
   149
  max_new theory_const
immler@29593
   150
  (Path.explode "$VAMPIRE_HOME/vampire",
immler@29593
   151
               ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
immler@29593
   152
  timeout;
wenzelm@28596
   153
wenzelm@28596
   154
val vampire_full = vampire_opts 60 false;
wenzelm@28596
   155
wenzelm@28592
   156
wenzelm@28596
   157
(* E prover *)
wenzelm@28596
   158
immler@30536
   159
fun eprover_opts max_new theory_const timeout = tptp_prover_opts
wenzelm@28596
   160
  max_new theory_const
immler@30536
   161
  (Path.explode "$E_HOME/eproof",
immler@30536
   162
    "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
immler@30536
   163
  timeout;
wenzelm@28596
   164
wenzelm@28596
   165
val eprover = eprover_opts 100 false;
wenzelm@28596
   166
immler@30536
   167
fun eprover_opts_full max_new theory_const timeout = full_prover_opts
wenzelm@28596
   168
  max_new theory_const
immler@30536
   169
  (Path.explode "$E_HOME/eproof",
immler@30536
   170
    "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
immler@30536
   171
  timeout;
wenzelm@28596
   172
wenzelm@28596
   173
val eprover_full = eprover_opts_full 100 false;
wenzelm@28596
   174
wenzelm@28596
   175
wenzelm@28596
   176
(* SPASS *)
wenzelm@28592
   177
immler@31409
   178
fun spass_opts max_new theory_const timeout ax_clauses ccs name n goal = external_prover
immler@31409
   179
  (ResAtp.get_relevant max_new theory_const)
immler@31409
   180
  (ResAtp.prepare_clauses true)
immler@31409
   181
  ResHolClause.dfg_write_file
immler@30536
   182
  (Path.explode "$SPASS_HOME/SPASS",
immler@30536
   183
    "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
immler@30874
   184
  ResReconstruct.find_failure
immler@30536
   185
  ResReconstruct.lemma_list_dfg
immler@31409
   186
  timeout ax_clauses ccs name n goal;
wenzelm@28596
   187
wenzelm@28596
   188
val spass = spass_opts 40 true;
wenzelm@28592
   189
wenzelm@28596
   190
wenzelm@28596
   191
(* remote prover invocation via SystemOnTPTP *)
wenzelm@28596
   192
immler@29593
   193
fun remote_prover_opts max_new theory_const args timeout =
wenzelm@28596
   194
  tptp_prover_opts max_new theory_const
wenzelm@30979
   195
  (Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP", args ^ " -t " ^ string_of_int timeout)
immler@29593
   196
  timeout;
wenzelm@28596
   197
wenzelm@28596
   198
val remote_prover = remote_prover_opts 60 false;
wenzelm@28592
   199
wenzelm@28592
   200
end;
immler@30536
   201
immler@30536
   202