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