src/HOL/Tools/ATP/atp_systems.ML
author blanchet
Fri, 06 May 2011 13:34:59 +0200
changeset 42709 e7af132d48fe
parent 42708 b6a18a14cc5c
child 42710 84fcce345b5d
permissions -rw-r--r--
allow each prover to specify its own formula kind for symbols occurring in the conjecture
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38047
9033c03cc214 consequence of directory renaming
blanchet
parents: 38046
diff changeset
     1
(*  Title:      HOL/Tools/ATP/atp_systems.ML
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     2
    Author:     Fabian Immler, TU Muenchen
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36370
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     4
36376
e83d52a52449 renamed module "ATP_Wrapper" to "ATP_Systems"
blanchet
parents: 36371
diff changeset
     5
Setup for supported ATPs.
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     6
*)
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     7
36376
e83d52a52449 renamed module "ATP_Wrapper" to "ATP_Systems"
blanchet
parents: 36371
diff changeset
     8
signature ATP_SYSTEMS =
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
     9
sig
42577
78414ec6fa4e made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents: 42571
diff changeset
    10
  type format = ATP_Problem.format
78414ec6fa4e made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents: 42571
diff changeset
    11
  type formula_kind = ATP_Problem.formula_kind
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
    12
  type failure = ATP_Proof.failure
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    13
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    14
  type atp_config =
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    15
    {exec : string * string,
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    16
     required_execs : (string * string) list,
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    17
     arguments :
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    18
       Proof.context -> int -> Time.time -> (unit -> (string * real) list)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    19
       -> string,
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    20
     proof_delims : (string * string) list,
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    21
     known_failures : (failure * string) list,
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
    22
     conj_sym_kind : formula_kind,
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
    23
     prem_kind : formula_kind,
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    24
     formats : format list,
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    25
     best_slices : Proof.context -> (real * (bool * int)) list,
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42611
diff changeset
    26
     best_type_systems : string list}
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    27
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    28
  val e_weight_method : string Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    29
  val e_default_fun_weight : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    30
  val e_fun_weight_base : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    31
  val e_fun_weight_span : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    32
  val e_default_sym_offs_weight : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    33
  val e_sym_offs_weight_base : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    34
  val e_sym_offs_weight_span : real Config.T
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    35
  val eN : string
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    36
  val spassN : string
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    37
  val vampireN : string
42535
3c1f302b3ee6 added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format
blanchet
parents: 42521
diff changeset
    38
  val tofof_eN : string
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    39
  val sine_eN : string
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    40
  val snarkN : string
41738
eb98c60a6cf0 added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents: 41727
diff changeset
    41
  val z3_atpN : string
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
    42
  val remote_prefix : string
41738
eb98c60a6cf0 added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents: 41727
diff changeset
    43
  val remote_atp :
eb98c60a6cf0 added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
blanchet
parents: 41727
diff changeset
    44
    string -> string -> string list -> (string * string) list
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
    45
    -> (failure * string) list -> formula_kind -> formula_kind -> format list
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    46
    -> (Proof.context -> int) -> string list -> string * atp_config
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    47
  val add_atp : string * atp_config -> theory -> theory
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    48
  val get_atp : theory -> string -> atp_config
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41725
diff changeset
    49
  val supported_atps : theory -> string list
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    50
  val is_atp_installed : theory -> string -> bool
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
    51
  val refresh_systems_on_tptp : unit -> unit
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
    52
  val setup : theory -> theory
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    53
end;
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    54
36376
e83d52a52449 renamed module "ATP_Wrapper" to "ATP_Systems"
blanchet
parents: 36371
diff changeset
    55
structure ATP_Systems : ATP_SYSTEMS =
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    56
struct
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    57
42577
78414ec6fa4e made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
blanchet
parents: 42571
diff changeset
    58
open ATP_Problem
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
    59
open ATP_Proof
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
    60
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    61
(* ATP configuration *)
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
    62
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    63
type atp_config =
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    64
  {exec : string * string,
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    65
   required_execs : (string * string) list,
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    66
   arguments :
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    67
     Proof.context -> int -> Time.time -> (unit -> (string * real) list)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    68
     -> string,
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    69
   proof_delims : (string * string) list,
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    70
   known_failures : (failure * string) list,
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
    71
   conj_sym_kind : formula_kind,
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
    72
   prem_kind : formula_kind,
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    73
   formats : format list,
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    74
   best_slices : Proof.context -> (real * (bool * int)) list,
42613
23b13b1bd565 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
blanchet
parents: 42611
diff changeset
    75
   best_type_systems : string list}
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    76
38061
685d1f0f75b3 handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents: 38049
diff changeset
    77
val known_perl_failures =
38094
d01b8119b2e0 better error and minimizer output
blanchet
parents: 38092
diff changeset
    78
  [(CantConnect, "HTTP error"),
d01b8119b2e0 better error and minimizer output
blanchet
parents: 38092
diff changeset
    79
   (NoPerl, "env: perl"),
38065
9069e1ad1527 improved ATP error handling some more
blanchet
parents: 38064
diff changeset
    80
   (NoLibwwwPerl, "Can't locate HTTP")]
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    81
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    82
(* named ATPs *)
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    83
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    84
val eN = "e"
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    85
val spassN = "spass"
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    86
val vampireN = "vampire"
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
    87
val z3_atpN = "z3_atp"
42535
3c1f302b3ee6 added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format
blanchet
parents: 42521
diff changeset
    88
val tofof_eN = "tofof_e"
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    89
val sine_eN = "sine_e"
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    90
val snarkN = "snark"
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
    91
val remote_prefix = "remote_"
38001
a9b47b85ca24 reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents: 38000
diff changeset
    92
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    93
structure Data = Theory_Data
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    94
(
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    95
  type T = (atp_config * stamp) Symtab.table
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    96
  val empty = Symtab.empty
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    97
  val extend = I
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    98
  fun merge data : T = Symtab.merge (eq_snd op =) data
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    99
    handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   100
)
38017
3ad3e3ca2451 move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
blanchet
parents: 38015
diff changeset
   101
38737
bdcb23701448 better workaround for E's off-by-one-second issue
blanchet
parents: 38691
diff changeset
   102
fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
36142
f5e15e9aae10 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents: 36064
diff changeset
   103
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   104
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   105
(* E *)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   106
40344
df25b51af013 give E one more second, to prevent cases where it finds a proof but has no time to print it
blanchet
parents: 40060
diff changeset
   107
(* Give E an extra second to reconstruct the proof. Older versions even get two
df25b51af013 give E one more second, to prevent cases where it finds a proof but has no time to print it
blanchet
parents: 40060
diff changeset
   108
   seconds, because the "eproof" script wrongly subtracted an entire second to
df25b51af013 give E one more second, to prevent cases where it finds a proof but has no time to print it
blanchet
parents: 40060
diff changeset
   109
   account for the overhead of the script itself, which is in fact much
df25b51af013 give E one more second, to prevent cases where it finds a proof but has no time to print it
blanchet
parents: 40060
diff changeset
   110
   lower. *)
38737
bdcb23701448 better workaround for E's off-by-one-second issue
blanchet
parents: 38691
diff changeset
   111
fun e_bonus () =
41334
3cb52cbf0eed enable E weight generation with unofficial latest version of E (tentatively called E 1.2B) -- backed by Judgment Day
blanchet
parents: 41317
diff changeset
   112
  if string_ord (getenv "E_VERSION", "1.1") = LESS then 2000 else 1000
38737
bdcb23701448 better workaround for E's off-by-one-second issue
blanchet
parents: 38691
diff changeset
   113
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   114
val tstp_proof_delims =
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   115
  ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   116
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   117
val e_slicesN = "slices"
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   118
val e_autoN = "auto"
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   119
val e_fun_weightN = "fun_weight"
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   120
val e_sym_offset_weightN = "sym_offset_weight"
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   121
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   122
val e_weight_method =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   123
  Attrib.setup_config_string @{binding atp_e_weight_method} (K e_slicesN)
41770
a710e96583d5 adjust fudge factors
blanchet
parents: 41769
diff changeset
   124
(* FUDGE *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   125
val e_default_fun_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   126
  Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   127
val e_fun_weight_base =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   128
  Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   129
val e_fun_weight_span =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   130
  Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   131
val e_default_sym_offs_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   132
  Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   133
val e_sym_offs_weight_base =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   134
  Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   135
val e_sym_offs_weight_span =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   136
  Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   137
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   138
fun e_weight_method_case method fw sow =
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   139
  if method = e_fun_weightN then fw
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   140
  else if method = e_sym_offset_weightN then sow
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   141
  else raise Fail ("unexpected" ^ quote method)
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   142
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   143
fun scaled_e_weight ctxt method w =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   144
  w * Config.get ctxt
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   145
          (e_weight_method_case method e_fun_weight_span e_sym_offs_weight_span)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   146
  + Config.get ctxt
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   147
        (e_weight_method_case method e_fun_weight_base e_sym_offs_weight_base)
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   148
  |> Real.ceil |> signed_string_of_int
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41269
diff changeset
   149
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   150
fun e_weight_arguments ctxt method weights =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   151
  if method = e_autoN then
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   152
    "-xAutoDev"
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   153
  else
41314
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   154
    "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   155
    \--destructive-er-aggressive --destructive-er --presat-simplify \
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   156
    \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   157
    \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   158
    \-H'(4*" ^ e_weight_method_case method "FunWeight" "SymOffsetWeight" ^
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   159
    "(SimulateSOS, " ^
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   160
    (e_weight_method_case method e_default_fun_weight e_default_sym_offs_weight
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   161
     |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
41314
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   162
    ",20,1.5,1.5,1" ^
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   163
    (weights ()
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   164
     |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight ctxt method w)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   165
     |> implode) ^
41314
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   166
    "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   167
    \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   168
    \FIFOWeight(PreferProcessed))'"
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41269
diff changeset
   169
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   170
fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   171
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   172
fun effective_e_weight_method ctxt =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   173
  if is_old_e_version () then e_autoN else Config.get ctxt e_weight_method
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   174
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   175
(* The order here must correspond to the order in "e_config" below. *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   176
fun method_for_slice ctxt slice =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   177
  let val method = effective_e_weight_method ctxt in
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   178
    if method = e_slicesN then
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   179
      case slice of
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   180
        0 => e_sym_offset_weightN
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   181
      | 1 => e_autoN
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   182
      | 2 => e_fun_weightN
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   183
      | _ => raise Fail "no such slice"
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   184
    else
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   185
      method
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   186
  end
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   187
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   188
val e_config : atp_config =
38092
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38090
diff changeset
   189
  {exec = ("E_HOME", "eproof"),
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38090
diff changeset
   190
   required_execs = [],
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   191
   arguments = fn ctxt => fn slice => fn timeout => fn weights =>
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   192
     "--tstp-in --tstp-out -l5 " ^
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   193
     e_weight_arguments ctxt (method_for_slice ctxt slice) weights ^
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   194
     " -tAutoDev --silent --cpu-limit=" ^
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   195
     string_of_int (to_secs (e_bonus ()) timeout),
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   196
   proof_delims = [tstp_proof_delims],
36265
41c9e755e552 distinguish between the different ATP errors in the user interface;
blanchet
parents: 36264
diff changeset
   197
   known_failures =
37995
06f02b15ef8a generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents: 37994
diff changeset
   198
     [(Unprovable, "SZS status: CounterSatisfiable"),
06f02b15ef8a generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents: 37994
diff changeset
   199
      (Unprovable, "SZS status CounterSatisfiable"),
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   200
      (TimedOut, "Failure: Resource limit exceeded (time)"),
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   201
      (TimedOut, "time limit exceeded"),
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   202
      (OutOfResources,
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   203
       "# Cannot determine problem status within resource limit"),
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   204
      (OutOfResources, "SZS status: ResourceOut"),
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   205
      (OutOfResources, "SZS status ResourceOut")],
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   206
   conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *)
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   207
   prem_kind = Conjecture,
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   208
   formats = [Fof],
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   209
   best_slices = fn ctxt =>
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   210
     if effective_e_weight_method ctxt = e_slicesN then
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   211
       [(0.33333, (true, 100 (* FUDGE *))) (* sym_offset_weight *),
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   212
        (0.33333, (true, 1000 (* FUDGE *))) (* auto *),
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   213
        (0.33334, (true, 200 (* FUDGE *))) (* fun_weight *)]
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   214
     else
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   215
       [(1.0, (true, 250 (* FUDGE *)))],
42708
b6a18a14cc5c better type system setup, based on Judgment Day
blanchet
parents: 42692
diff changeset
   216
   (* Actual order, according to Judgment Day: "mangled_preds!",
b6a18a14cc5c better type system setup, based on Judgment Day
blanchet
parents: 42692
diff changeset
   217
      "mangled_tags!", "mangled_tags?", "mangled_preds?". But E "mangled_preds?"
b6a18a14cc5c better type system setup, based on Judgment Day
blanchet
parents: 42692
diff changeset
   218
      works well in combination with Vampire "mangled_tags!". *)
b6a18a14cc5c better type system setup, based on Judgment Day
blanchet
parents: 42692
diff changeset
   219
   best_type_systems = ["mangled_preds?"]}
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   220
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   221
val e = (eN, e_config)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   222
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   223
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   224
(* SPASS *)
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   225
36219
16670b4f0baa set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
blanchet
parents: 36190
diff changeset
   226
(* The "-VarWeight=3" option helps the higher-order problems, probably by
16670b4f0baa set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
blanchet
parents: 36190
diff changeset
   227
   counteracting the presence of "hAPP". *)
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   228
val spass_config : atp_config =
38092
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38090
diff changeset
   229
  {exec = ("ISABELLE_ATP", "scripts/spass"),
39002
a2d7be688ea1 add dependency of "spass" script
blanchet
parents: 38999
diff changeset
   230
   required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   231
   arguments = fn _ => fn slice => fn timeout => fn _ =>
37962
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents: 37926
diff changeset
   232
     ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
38737
bdcb23701448 better workaround for E's off-by-one-second issue
blanchet
parents: 38691
diff changeset
   233
      \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   234
     |> slice = 0 ? prefix "-SOS=1 ",
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   235
   proof_delims = [("Here is a proof", "Formulae used in the proof")],
36289
f75b6a3e1450 set "atps" reference's default value to "(remote_)e (remote_)spass (remote_)vampire", based on what is installed
blanchet
parents: 36287
diff changeset
   236
   known_failures =
38061
685d1f0f75b3 handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents: 38049
diff changeset
   237
     known_perl_failures @
37413
e856582fe9c4 improve ATP-specific error messages
blanchet
parents: 37347
diff changeset
   238
     [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   239
      (TimedOut, "SPASS beiseite: Ran out of time"),
36965
67ae217c6b5c identify common SPASS error more clearly
blanchet
parents: 36924
diff changeset
   240
      (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
37413
e856582fe9c4 improve ATP-specific error messages
blanchet
parents: 37347
diff changeset
   241
      (MalformedInput, "Undefined symbol"),
37414
d0cea0796295 expect SPASS 3.7, and give a friendly warning if an older version is used
blanchet
parents: 37413
diff changeset
   242
      (MalformedInput, "Free Variable"),
39263
e2a3c435334b more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents: 39262
diff changeset
   243
      (SpassTooOld, "tptp2dfg"),
e2a3c435334b more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents: 39262
diff changeset
   244
      (InternalError, "Please report this error")],
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   245
   conj_sym_kind = Axiom, (* FIXME: try out Hypothesis *)
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   246
   prem_kind = Conjecture,
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   247
   formats = [Fof],
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   248
   best_slices =
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   249
     K [(0.66667, (false, 150 (* FUDGE *))) (* with SOS *),
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   250
        (0.33333, (true, 150 (* FUDGE *))) (* without SOS *)],
42692
60359df11dc4 improve suggested type system list based on evaluation
blanchet
parents: 42684
diff changeset
   251
   best_type_systems =
42708
b6a18a14cc5c better type system setup, based on Judgment Day
blanchet
parents: 42692
diff changeset
   252
     ["args", "mangled_preds!", "mangled_tags!", "mangled_tags?"]}
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   253
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   254
val spass = (spassN, spass_config)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   255
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   256
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   257
(* Vampire *)
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   258
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   259
val vampire_config : atp_config =
38092
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38090
diff changeset
   260
  {exec = ("VAMPIRE_HOME", "vampire"),
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38090
diff changeset
   261
   required_execs = [],
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   262
   arguments = fn _ => fn slice => fn timeout => fn _ =>
41203
1393514094d7 fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)
blanchet
parents: 41148
diff changeset
   263
     (* This would work too but it's less tested: "--proof tptp " ^ *)
1393514094d7 fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)
blanchet
parents: 41148
diff changeset
   264
     "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
1393514094d7 fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)
blanchet
parents: 41148
diff changeset
   265
     " --thanks \"Andrei and Krystof\" --input_file"
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   266
     |> slice = 0 ? prefix "--sos on ",
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   267
   proof_delims =
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   268
     [("=========== Refutation ==========",
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   269
       "======= End of refutation ======="),
38033
df99f022751d support latest version of Vampire (1.0) locally
blanchet
parents: 38032
diff changeset
   270
      ("% SZS output start Refutation", "% SZS output end Refutation"),
df99f022751d support latest version of Vampire (1.0) locally
blanchet
parents: 38032
diff changeset
   271
      ("% SZS output start Proof", "% SZS output end Proof")],
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   272
   known_failures =
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   273
     [(Unprovable, "UNPROVABLE"),
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   274
      (IncompleteUnprovable, "CANNOT PROVE"),
42449
494e4ac5b0f8 detect some unsound proofs before showing them to the user
blanchet
parents: 42443
diff changeset
   275
      (IncompleteUnprovable, "SZS status GaveUp"),
42332
474790ed7b0c handle Vampire [predicate definition introduction] steps the same way as missing proof, since such steps do not report which axioms were used
blanchet
parents: 41770
diff changeset
   276
      (ProofMissing, "[predicate definition introduction]"),
474790ed7b0c handle Vampire [predicate definition introduction] steps the same way as missing proof, since such steps do not report which axioms were used
blanchet
parents: 41770
diff changeset
   277
      (ProofMissing, "predicate_definition_introduction,[]"), (* TSTP *)
38092
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38090
diff changeset
   278
      (TimedOut, "SZS status Timeout"),
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   279
      (Unprovable, "Satisfiability detected"),
38647
5500241da479 play with fudge factor + parse one more Vampire error
blanchet
parents: 38646
diff changeset
   280
      (Unprovable, "Termination reason: Satisfiable"),
39263
e2a3c435334b more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents: 39262
diff changeset
   281
      (VampireTooOld, "not a valid option"),
e2a3c435334b more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents: 39262
diff changeset
   282
      (Interrupted, "Aborted by signal SIGINT")],
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   283
   conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *)
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   284
   prem_kind = Conjecture,
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   285
   formats = [Fof],
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   286
   best_slices =
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   287
     K [(0.66667, (false, 450 (* FUDGE *))) (* with SOS *),
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   288
        (0.33333, (true, 450 (* FUDGE *))) (* without SOS *)],
42692
60359df11dc4 improve suggested type system list based on evaluation
blanchet
parents: 42684
diff changeset
   289
   best_type_systems =
42708
b6a18a14cc5c better type system setup, based on Judgment Day
blanchet
parents: 42692
diff changeset
   290
     ["mangled_tags!", "mangled_preds!", "mangled_preds?"]}
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   291
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   292
val vampire = (vampireN, vampire_config)
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   293
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   294
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   295
(* Z3 with TPTP syntax *)
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   296
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   297
val z3_atp_config : atp_config =
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   298
  {exec = ("Z3_HOME", "z3"),
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   299
   required_execs = [],
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   300
   arguments = fn _ => fn _ => fn timeout => fn _ =>
41766
26dab6eca1c2 make experimental "Z3 ATP" work on Linux as well
blanchet
parents: 41765
diff changeset
   301
     "MBQI=true -p -t:" ^ string_of_int (to_secs 0 timeout),
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   302
   proof_delims = [],
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   303
   known_failures =
41742
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   304
     [(Unprovable, "\nsat"),
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   305
      (IncompleteUnprovable, "\nunknown"),
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   306
      (IncompleteUnprovable, "SZS status Satisfiable"),
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   307
      (ProofMissing, "\nunsat"),
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   308
      (ProofMissing, "SZS status Unsatisfiable")],
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   309
   conj_sym_kind = Hypothesis,
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   310
   prem_kind = Hypothesis,
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   311
   formats = [Fof],
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   312
   best_slices = K [(1.0, (false, 250 (* FUDGE *)))],
42692
60359df11dc4 improve suggested type system list based on evaluation
blanchet
parents: 42684
diff changeset
   313
   best_type_systems = [] (* FIXME *)}
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   314
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   315
val z3_atp = (z3_atpN, z3_atp_config)
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   316
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   317
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   318
(* Remote ATP invocation via SystemOnTPTP *)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   319
38061
685d1f0f75b3 handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents: 38049
diff changeset
   320
val systems = Synchronized.var "atp_systems" ([] : string list)
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   321
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   322
fun get_systems () =
38061
685d1f0f75b3 handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents: 38049
diff changeset
   323
  case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   324
    (output, 0) => split_lines output
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   325
  | (output, _) =>
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   326
    error (case extract_known_failure known_perl_failures output of
41744
a18e7bbca258 make minimizer verbose
blanchet
parents: 41742
diff changeset
   327
             SOME failure => string_for_failure failure
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   328
           | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   329
42537
25ceb855a18b improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work
blanchet
parents: 42535
diff changeset
   330
fun find_system name [] systems =
25ceb855a18b improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work
blanchet
parents: 42535
diff changeset
   331
    find_first (String.isPrefix (name ^ "---")) systems
38690
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   332
  | find_system name (version :: versions) systems =
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   333
    case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   334
      NONE => find_system name versions systems
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   335
    | res => res
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   336
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   337
fun get_system name versions =
38589
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38588
diff changeset
   338
  Synchronized.change_result systems
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38588
diff changeset
   339
      (fn systems => (if null systems then get_systems () else systems)
38690
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   340
                     |> `(find_system name versions))
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
   341
38690
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   342
fun the_system name versions =
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   343
  case get_system name versions of
39010
344028ecc00e show real CPU time
blanchet
parents: 39002
diff changeset
   344
    SOME sys => sys
41269
blanchet
parents: 41238
diff changeset
   345
  | NONE => error ("System " ^ quote name ^
blanchet
parents: 41238
diff changeset
   346
                   " is not available at SystemOnTPTP.")
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   347
41148
f5229ab54284 added timeout max for remote server invocation
blanchet
parents: 40669
diff changeset
   348
val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
f5229ab54284 added timeout max for remote server invocation
blanchet
parents: 40669
diff changeset
   349
38690
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   350
fun remote_config system_name system_versions proof_delims known_failures
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   351
                  conj_sym_kind prem_kind formats best_max_relevant
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   352
                  best_type_systems : atp_config =
38092
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38090
diff changeset
   353
  {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
81a003f7de0d speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
blanchet
parents: 38090
diff changeset
   354
   required_execs = [],
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   355
   arguments = fn _ => fn _ => fn timeout => fn _ =>
41148
f5229ab54284 added timeout max for remote server invocation
blanchet
parents: 40669
diff changeset
   356
     " -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
f5229ab54284 added timeout max for remote server invocation
blanchet
parents: 40669
diff changeset
   357
     ^ " -s " ^ the_system system_name system_versions,
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   358
   proof_delims = insert (op =) tstp_proof_delims proof_delims,
38061
685d1f0f75b3 handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents: 38049
diff changeset
   359
   known_failures =
685d1f0f75b3 handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents: 38049
diff changeset
   360
     known_failures @ known_perl_failures @
42571
67e2f2df68d5 recognize more SystemOnTPTP errors
blanchet
parents: 42559
diff changeset
   361
     [(IncompleteUnprovable, "says Unknown"),
42584
8121a31b6754 pick up GaveUp error on SystemOnTPTP
blanchet
parents: 42579
diff changeset
   362
      (IncompleteUnprovable, "says GaveUp"),
42571
67e2f2df68d5 recognize more SystemOnTPTP errors
blanchet
parents: 42559
diff changeset
   363
      (TimedOut, "says Timeout")],
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   364
   conj_sym_kind = conj_sym_kind,
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   365
   prem_kind = prem_kind,
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   366
   formats = formats,
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   367
   best_slices = fn ctxt => [(1.0, (false, best_max_relevant ctxt))],
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   368
   best_type_systems = best_type_systems}
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   369
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   370
fun int_average f xs = fold (Integer.add o f) xs 0 div length xs
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   371
38690
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   372
fun remotify_config system_name system_versions
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   373
        ({proof_delims, known_failures, conj_sym_kind, prem_kind, formats,
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   374
          best_slices, best_type_systems, ...} : atp_config) : atp_config =
38690
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   375
  remote_config system_name system_versions proof_delims known_failures
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   376
                conj_sym_kind prem_kind formats
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   377
                (int_average (snd o snd) o best_slices) best_type_systems
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   378
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   379
fun remote_atp name system_name system_versions proof_delims known_failures
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   380
        conj_sym_kind prem_kind formats best_max_relevant best_type_systems =
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   381
  (remote_prefix ^ name,
38690
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   382
   remote_config system_name system_versions proof_delims known_failures
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   383
                 conj_sym_kind prem_kind formats best_max_relevant
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   384
                 best_type_systems)
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   385
fun remotify_atp (name, config) system_name system_versions =
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   386
  (remote_prefix ^ name, remotify_config system_name system_versions config)
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   387
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   388
val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"]
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   389
val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
42537
25ceb855a18b improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work
blanchet
parents: 42535
diff changeset
   390
val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"]
42535
3c1f302b3ee6 added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format
blanchet
parents: 42521
diff changeset
   391
val remote_tofof_e =
42559
791d7153c48d better known failure recognition for ToFoF-E
blanchet
parents: 42537
diff changeset
   392
  remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   393
             Axiom Conjecture [Tff] (K 200 (* FUDGE *)) ["simple"]
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   394
val remote_sine_e =
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   395
  remote_atp sine_eN "SInE" ["0.4"] [] [] Axiom Conjecture [Fof]
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   396
             (K 500 (* FUDGE *)) ["args", "preds", "tags"]
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   397
val remote_snark =
42537
25ceb855a18b improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work
blanchet
parents: 42535
diff changeset
   398
  remote_atp snarkN "SNARK" ["20080805r024"]
42709
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   399
             [("refutation.", "end_refutation.")] [] Hypothesis Conjecture
e7af132d48fe allow each prover to specify its own formula kind for symbols occurring in the conjecture
blanchet
parents: 42708
diff changeset
   400
             [Tff, Fof] (K 250 (* FUDGE *)) ["simple"]
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   401
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   402
(* Setup *)
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   403
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   404
fun add_atp (name, config) thy =
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   405
  Data.map (Symtab.update_new (name, (config, stamp ()))) thy
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   406
  handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   407
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   408
fun get_atp thy name =
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   409
  the (Symtab.lookup (Data.get thy) name) |> fst
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   410
  handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   411
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41725
diff changeset
   412
val supported_atps = Symtab.keys o Data.get
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36370
diff changeset
   413
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   414
fun is_atp_installed thy name =
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   415
  let val {exec, required_execs, ...} = get_atp thy name in
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   416
    forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   417
  end
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36370
diff changeset
   418
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   419
fun refresh_systems_on_tptp () =
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   420
  Synchronized.change systems (fn _ => get_systems ())
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   421
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   422
val atps = [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
42535
3c1f302b3ee6 added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format
blanchet
parents: 42521
diff changeset
   423
            remote_tofof_e, remote_sine_e, remote_snark]
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   424
val setup = fold add_atp atps
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
   425
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   426
end;