src/HOL/Tools/ATP_Manager/atp_wrapper.ML
author boehmes
Thu, 03 Sep 2009 17:55:31 +0200
changeset 32510 1b56f8b1e5cc
parent 32458 de6834b20e9e
child 32574 719426c9e1eb
permissions -rw-r--r--
added runtime information to sledgehammer
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32327
0971cc0b6a57 src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
wenzelm
parents: 32257
diff changeset
     1
(*  Title:      HOL/Tools/ATP_Manager/atp_wrapper.ML
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     2
    Author:     Fabian Immler, TU Muenchen
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     3
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     4
Wrapper functions for external ATPs.
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     5
*)
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     6
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     7
signature ATP_WRAPPER =
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     8
sig
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     9
  val destdir: string ref
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    10
  val problem_name: string ref
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    11
  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
    12
  val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    13
  val tptp_prover: Path.T * string -> AtpManager.prover
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    14
  val full_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    15
  val full_prover: Path.T * string  -> AtpManager.prover
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    16
  val vampire_opts: int -> bool -> AtpManager.prover
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    17
  val vampire: AtpManager.prover
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    18
  val vampire_opts_full: int -> bool -> AtpManager.prover
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    19
  val vampire_full: AtpManager.prover
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    20
  val eprover_opts: int -> bool  -> AtpManager.prover
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    21
  val eprover: AtpManager.prover
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    22
  val eprover_opts_full: int -> bool -> AtpManager.prover
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    23
  val eprover_full: AtpManager.prover
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    24
  val spass_opts: int -> bool  -> AtpManager.prover
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    25
  val spass: AtpManager.prover
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
    26
  val remote_prover_opts: int -> bool -> string -> string -> AtpManager.prover
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
    27
  val remote_prover: string -> string -> AtpManager.prover
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
    28
  val refresh_systems: unit -> unit
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    29
end;
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    30
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    31
structure AtpWrapper: ATP_WRAPPER =
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    32
struct
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    33
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    34
(** generic ATP wrapper **)
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    35
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    36
(* global hooks for writing problemfiles *)
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    37
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    38
val destdir = ref "";   (*Empty means write files to /tmp*)
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    39
val problem_name = ref "prob";
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    40
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
(* basic template *)
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    43
32458
de6834b20e9e sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents: 32451
diff changeset
    44
fun with_path cleanup after f path =
de6834b20e9e sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents: 32451
diff changeset
    45
  Exn.capture f path
de6834b20e9e sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents: 32451
diff changeset
    46
  |> tap (fn _ => cleanup path)
de6834b20e9e sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents: 32451
diff changeset
    47
  |> Exn.release
de6834b20e9e sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents: 32451
diff changeset
    48
  |> tap (after path)
de6834b20e9e sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents: 32451
diff changeset
    49
31409
d8537ba165b5 split preparing clauses and writing problemfile;
immler@in.tum.de
parents: 31368
diff changeset
    50
fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer
31752
19a5f1c8a844 use results of relevance-filter to determine additional clauses;
immler@in.tum.de
parents: 31751
diff changeset
    51
  timeout axiom_clauses filtered_clauses name subgoalno goal =
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    52
  let
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    53
    (* path to unique problem file *)
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    54
    val destdir' = ! destdir
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    55
    val problem_name' = ! problem_name
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    56
    fun prob_pathname nr =
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    57
      let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ string_of_int nr)
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    58
      in if destdir' = "" then File.tmp_path probfile
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    59
        else if File.exists (Path.explode (destdir'))
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    60
        then Path.append  (Path.explode (destdir')) probfile
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    61
        else error ("No such directory: " ^ destdir')
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    62
      end
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    63
31750
f28b7365fabf restructured external_prover
immler@in.tum.de
parents: 31411
diff changeset
    64
    (* get clauses and prepare them for writing *)
30537
0dd8dfe424cf use goal instead of Proof State
immler@in.tum.de
parents: 30536
diff changeset
    65
    val (ctxt, (chain_ths, th)) = goal
30536
07b4f050e4df split relevance-filter and writing of problem-files;
immler@in.tum.de
parents: 30535
diff changeset
    66
    val thy = ProofContext.theory_of ctxt
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    67
    val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
32257
bad5a99c16d8 neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents: 32091
diff changeset
    68
    val goal_cls = #1 (ResAxioms.neg_conjecture_clauses ctxt th subgoalno)
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 31840
diff changeset
    69
    val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm ctxt th)) goal_cls
31752
19a5f1c8a844 use results of relevance-filter to determine additional clauses;
immler@in.tum.de
parents: 31751
diff changeset
    70
    val the_filtered_clauses =
19a5f1c8a844 use results of relevance-filter to determine additional clauses;
immler@in.tum.de
parents: 31751
diff changeset
    71
      case filtered_clauses of
19a5f1c8a844 use results of relevance-filter to determine additional clauses;
immler@in.tum.de
parents: 31751
diff changeset
    72
          NONE => relevance_filter goal goal_cls
19a5f1c8a844 use results of relevance-filter to determine additional clauses;
immler@in.tum.de
parents: 31751
diff changeset
    73
        | SOME fcls => fcls
31409
d8537ba165b5 split preparing clauses and writing problemfile;
immler@in.tum.de
parents: 31368
diff changeset
    74
    val the_axiom_clauses =
d8537ba165b5 split preparing clauses and writing problemfile;
immler@in.tum.de
parents: 31368
diff changeset
    75
      case axiom_clauses of
31752
19a5f1c8a844 use results of relevance-filter to determine additional clauses;
immler@in.tum.de
parents: 31751
diff changeset
    76
          NONE => the_filtered_clauses
31409
d8537ba165b5 split preparing clauses and writing problemfile;
immler@in.tum.de
parents: 31368
diff changeset
    77
        | SOME axcls => axcls
32257
bad5a99c16d8 neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents: 32091
diff changeset
    78
    val (thm_names, clauses) =
bad5a99c16d8 neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents: 32091
diff changeset
    79
      preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
31750
f28b7365fabf restructured external_prover
immler@in.tum.de
parents: 31411
diff changeset
    80
f28b7365fabf restructured external_prover
immler@in.tum.de
parents: 31411
diff changeset
    81
    (* write out problem file and call prover *)
32510
1b56f8b1e5cc added runtime information to sledgehammer
boehmes
parents: 32458
diff changeset
    82
    fun cmd_line probfile = "TIMEFORMAT='%3U'; ((time " ^ space_implode " "
1b56f8b1e5cc added runtime information to sledgehammer
boehmes
parents: 32458
diff changeset
    83
      [File.shell_path cmd, args, File.platform_path probfile] ^ ") 2>&1)"
1b56f8b1e5cc added runtime information to sledgehammer
boehmes
parents: 32458
diff changeset
    84
    fun split_time s =
1b56f8b1e5cc added runtime information to sledgehammer
boehmes
parents: 32458
diff changeset
    85
      let
1b56f8b1e5cc added runtime information to sledgehammer
boehmes
parents: 32458
diff changeset
    86
        val split = String.tokens (fn c => str c = "\n")
1b56f8b1e5cc added runtime information to sledgehammer
boehmes
parents: 32458
diff changeset
    87
        val (proof, t) = s |> split |> split_last |> apfst cat_lines
1b56f8b1e5cc added runtime information to sledgehammer
boehmes
parents: 32458
diff changeset
    88
        val num = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int)
1b56f8b1e5cc added runtime information to sledgehammer
boehmes
parents: 32458
diff changeset
    89
        val time = num --| Scan.$$ "." -- num >> (fn (a, b) => a * 1000 + b)
1b56f8b1e5cc added runtime information to sledgehammer
boehmes
parents: 32458
diff changeset
    90
        val as_time = the_default 0 o Scan.read Symbol.stopper time o explode
1b56f8b1e5cc added runtime information to sledgehammer
boehmes
parents: 32458
diff changeset
    91
      in (proof, as_time t) end
32458
de6834b20e9e sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents: 32451
diff changeset
    92
    fun run_on probfile =
de6834b20e9e sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents: 32451
diff changeset
    93
      if File.exists cmd
32510
1b56f8b1e5cc added runtime information to sledgehammer
boehmes
parents: 32458
diff changeset
    94
      then
1b56f8b1e5cc added runtime information to sledgehammer
boehmes
parents: 32458
diff changeset
    95
        writer probfile clauses
1b56f8b1e5cc added runtime information to sledgehammer
boehmes
parents: 32458
diff changeset
    96
        |> pair (apfst split_time (system_out (cmd_line probfile)))
32458
de6834b20e9e sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents: 32451
diff changeset
    97
      else error ("Bad executable: " ^ Path.implode cmd)
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    98
31751
fda2cf4fef58 export proof when exporting problemfile
immler@in.tum.de
parents: 31750
diff changeset
    99
    (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
32458
de6834b20e9e sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents: 32451
diff changeset
   100
    fun cleanup probfile = if destdir' = "" then File.rm probfile else ()
32510
1b56f8b1e5cc added runtime information to sledgehammer
boehmes
parents: 32458
diff changeset
   101
    fun export probfile (((proof, _), _), _) = if destdir' = "" then ()
31838
607a984b70e3 use structure File instead of TextIO;
immler@in.tum.de
parents: 31835
diff changeset
   102
      else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
32257
bad5a99c16d8 neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents: 32091
diff changeset
   103
32510
1b56f8b1e5cc added runtime information to sledgehammer
boehmes
parents: 32458
diff changeset
   104
    val (((proof, time), rc), conj_pos) = with_path cleanup export run_on
32458
de6834b20e9e sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents: 32451
diff changeset
   105
      (prob_pathname subgoalno)
de6834b20e9e sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents: 32451
diff changeset
   106
29590
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29587
diff changeset
   107
    (* check for success and print out some information on failure *)
479a2fce65e6 modified remote script;
immler@in.tum.de
parents: 29587
diff changeset
   108
    val failure = find_failure proof
29597
immler@in.tum.de
parents: 29593
diff changeset
   109
    val success = rc = 0 andalso is_none failure
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   110
    val message =
32451
8f0dc876fb1b propagate theorem names, in addition to generated return message
boehmes
parents: 32327
diff changeset
   111
      if is_some failure then ("External prover failed.", [])
8f0dc876fb1b propagate theorem names, in addition to generated return message
boehmes
parents: 32327
diff changeset
   112
      else if rc <> 0 then ("External prover failed: " ^ proof, [])
8f0dc876fb1b propagate theorem names, in addition to generated return message
boehmes
parents: 32327
diff changeset
   113
      else apfst (fn s => "Try this command: " ^ s)
8f0dc876fb1b propagate theorem names, in addition to generated return message
boehmes
parents: 32327
diff changeset
   114
        (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno))
31411
1d00ab68bc8d additional debugging
immler@in.tum.de
parents: 31410
diff changeset
   115
    val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
32510
1b56f8b1e5cc added runtime information to sledgehammer
boehmes
parents: 32458
diff changeset
   116
  in (success, message, time, proof, thm_names, the_filtered_clauses) end;
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   117
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   118
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   119
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   120
(** common provers **)
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   121
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   122
(* generic TPTP-based provers *)
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   123
31752
19a5f1c8a844 use results of relevance-filter to determine additional clauses;
immler@in.tum.de
parents: 31751
diff changeset
   124
fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses fcls name n goal =
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   125
  external_prover
31409
d8537ba165b5 split preparing clauses and writing problemfile;
immler@in.tum.de
parents: 31368
diff changeset
   126
  (ResAtp.get_relevant max_new theory_const)
d8537ba165b5 split preparing clauses and writing problemfile;
immler@in.tum.de
parents: 31368
diff changeset
   127
  (ResAtp.prepare_clauses false)
31791
c9a1caf218c8 New ATP option: full types
nipkow
parents: 31752
diff changeset
   128
  (ResHolClause.tptp_write_file (AtpManager.get_full_types()))
31409
d8537ba165b5 split preparing clauses and writing problemfile;
immler@in.tum.de
parents: 31368
diff changeset
   129
  command
d8537ba165b5 split preparing clauses and writing problemfile;
immler@in.tum.de
parents: 31368
diff changeset
   130
  ResReconstruct.find_failure
31840
beeaa1ed1f47 check if conjectures have been used in proof
immler@in.tum.de
parents: 31838
diff changeset
   131
  (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list false)
31752
19a5f1c8a844 use results of relevance-filter to determine additional clauses;
immler@in.tum.de
parents: 31751
diff changeset
   132
  timeout ax_clauses fcls name n goal;
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   133
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   134
(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   135
fun tptp_prover_opts max_new theory_const =
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   136
  tptp_prover_opts_full max_new theory_const false;
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   137
31368
763f4b0fd579 made SML/NJ happy;
wenzelm
parents: 31037
diff changeset
   138
fun tptp_prover x = tptp_prover_opts 60 true x;
28596
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
(*for structured proofs: prover must support TSTP*)
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   141
fun full_prover_opts max_new theory_const =
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   142
  tptp_prover_opts_full max_new theory_const true;
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   143
31368
763f4b0fd579 made SML/NJ happy;
wenzelm
parents: 31037
diff changeset
   144
fun full_prover x = full_prover_opts 60 true x;
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   145
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   146
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   147
(* Vampire *)
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   148
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   149
(*NB: Vampire does not work without explicit timelimit*)
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   150
29593
7b73bd578db2 pass timeout to prover;
immler@in.tum.de
parents: 29590
diff changeset
   151
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
   152
  max_new theory_const
29593
7b73bd578db2 pass timeout to prover;
immler@in.tum.de
parents: 29590
diff changeset
   153
  (Path.explode "$VAMPIRE_HOME/vampire",
32257
bad5a99c16d8 neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents: 32091
diff changeset
   154
    ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
29593
7b73bd578db2 pass timeout to prover;
immler@in.tum.de
parents: 29590
diff changeset
   155
  timeout;
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   156
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   157
val vampire = vampire_opts 60 false;
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   158
29593
7b73bd578db2 pass timeout to prover;
immler@in.tum.de
parents: 29590
diff changeset
   159
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
   160
  max_new theory_const
29593
7b73bd578db2 pass timeout to prover;
immler@in.tum.de
parents: 29590
diff changeset
   161
  (Path.explode "$VAMPIRE_HOME/vampire",
32257
bad5a99c16d8 neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents: 32091
diff changeset
   162
    ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
29593
7b73bd578db2 pass timeout to prover;
immler@in.tum.de
parents: 29590
diff changeset
   163
  timeout;
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   164
31832
immler@in.tum.de
parents: 31791
diff changeset
   165
val vampire_full = vampire_opts_full 60 false;
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   166
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   167
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   168
(* E prover *)
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   169
30536
07b4f050e4df split relevance-filter and writing of problem-files;
immler@in.tum.de
parents: 30535
diff changeset
   170
fun eprover_opts max_new theory_const timeout = tptp_prover_opts
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   171
  max_new theory_const
30536
07b4f050e4df split relevance-filter and writing of problem-files;
immler@in.tum.de
parents: 30535
diff changeset
   172
  (Path.explode "$E_HOME/eproof",
07b4f050e4df split relevance-filter and writing of problem-files;
immler@in.tum.de
parents: 30535
diff changeset
   173
    "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
07b4f050e4df split relevance-filter and writing of problem-files;
immler@in.tum.de
parents: 30535
diff changeset
   174
  timeout;
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   175
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   176
val eprover = eprover_opts 100 false;
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   177
30536
07b4f050e4df split relevance-filter and writing of problem-files;
immler@in.tum.de
parents: 30535
diff changeset
   178
fun eprover_opts_full max_new theory_const timeout = full_prover_opts
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   179
  max_new theory_const
30536
07b4f050e4df split relevance-filter and writing of problem-files;
immler@in.tum.de
parents: 30535
diff changeset
   180
  (Path.explode "$E_HOME/eproof",
07b4f050e4df split relevance-filter and writing of problem-files;
immler@in.tum.de
parents: 30535
diff changeset
   181
    "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
07b4f050e4df split relevance-filter and writing of problem-files;
immler@in.tum.de
parents: 30535
diff changeset
   182
  timeout;
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   183
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   184
val eprover_full = eprover_opts_full 100 false;
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   185
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   186
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   187
(* SPASS *)
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   188
31752
19a5f1c8a844 use results of relevance-filter to determine additional clauses;
immler@in.tum.de
parents: 31751
diff changeset
   189
fun spass_opts max_new theory_const timeout ax_clauses fcls name n goal = external_prover
31409
d8537ba165b5 split preparing clauses and writing problemfile;
immler@in.tum.de
parents: 31368
diff changeset
   190
  (ResAtp.get_relevant max_new theory_const)
d8537ba165b5 split preparing clauses and writing problemfile;
immler@in.tum.de
parents: 31368
diff changeset
   191
  (ResAtp.prepare_clauses true)
31791
c9a1caf218c8 New ATP option: full types
nipkow
parents: 31752
diff changeset
   192
  (ResHolClause.dfg_write_file (AtpManager.get_full_types()))
30536
07b4f050e4df split relevance-filter and writing of problem-files;
immler@in.tum.de
parents: 30535
diff changeset
   193
  (Path.explode "$SPASS_HOME/SPASS",
32257
bad5a99c16d8 neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents: 32091
diff changeset
   194
    "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^
bad5a99c16d8 neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents: 32091
diff changeset
   195
      string_of_int timeout)
30874
34927a1e0ae8 reverted to explicitly check the presence of a refutation
immler@in.tum.de
parents: 30542
diff changeset
   196
  ResReconstruct.find_failure
31840
beeaa1ed1f47 check if conjectures have been used in proof
immler@in.tum.de
parents: 31838
diff changeset
   197
  (ResReconstruct.lemma_list true)
31752
19a5f1c8a844 use results of relevance-filter to determine additional clauses;
immler@in.tum.de
parents: 31751
diff changeset
   198
  timeout ax_clauses fcls name n goal;
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   199
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   200
val spass = spass_opts 40 true;
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   201
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   202
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   203
(* remote prover invocation via SystemOnTPTP *)
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   204
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   205
val systems =
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   206
  Synchronized.var "atp_wrapper_systems" ([]: string list);
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   207
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   208
fun get_systems () =
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   209
  let
32327
0971cc0b6a57 src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
wenzelm
parents: 32257
diff changeset
   210
    val (answer, rc) = system_out ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w")
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   211
  in
32327
0971cc0b6a57 src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
wenzelm
parents: 32257
diff changeset
   212
    if rc <> 0 then error ("Failed to get available systems from SystemOnTPTP:\n" ^ answer)
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   213
    else split_lines answer
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   214
  end;
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   215
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   216
fun refresh_systems () = Synchronized.change systems (fn _ =>
32257
bad5a99c16d8 neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents: 32091
diff changeset
   217
  get_systems ());
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   218
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   219
fun get_system prefix = Synchronized.change_result systems (fn systems =>
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   220
  let val systems = if null systems then get_systems() else systems
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   221
  in (find_first (String.isPrefix prefix) systems, systems) end);
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   222
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   223
fun remote_prover_opts max_new theory_const args prover_prefix timeout =
32257
bad5a99c16d8 neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents: 32091
diff changeset
   224
  let val sys =
bad5a99c16d8 neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents: 32091
diff changeset
   225
    case get_system prover_prefix of
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   226
      NONE => error ("No system like " ^ quote prover_prefix ^ " at SystemOnTPTP")
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   227
    | SOME sys => sys
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   228
  in tptp_prover_opts max_new theory_const
32327
0971cc0b6a57 src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
wenzelm
parents: 32257
diff changeset
   229
    (Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
32257
bad5a99c16d8 neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents: 32091
diff changeset
   230
      args ^ " -t " ^ string_of_int timeout ^ " -s " ^ sys) timeout
bad5a99c16d8 neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents: 32091
diff changeset
   231
  end;
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   232
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   233
val remote_prover = remote_prover_opts 60 false;
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   234
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   235
end;
30536
07b4f050e4df split relevance-filter and writing of problem-files;
immler@in.tum.de
parents: 30535
diff changeset
   236