src/HOL/Tools/ATP/atp_systems.ML
author blanchet
Sun, 22 May 2011 14:50:32 +0200
changeset 42938 c124032ac96f
parent 42937 cabb3a947894
child 42939 0134d6650092
permissions -rw-r--r--
added Waldmeister
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,
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    25
     best_slices : Proof.context -> (real * (bool * (int * string list))) list}
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    26
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    27
  val e_weight_method : string Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    28
  val e_default_fun_weight : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    29
  val e_fun_weight_base : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    30
  val e_fun_weight_span : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    31
  val e_default_sym_offs_weight : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    32
  val e_sym_offs_weight_base : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    33
  val e_sym_offs_weight_span : real Config.T
42725
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
    34
  val spass_force_sos : bool Config.T
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
    35
  val vampire_force_sos : bool Config.T
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    36
  val eN : string
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    37
  val spassN : string
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    38
  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
    39
  val tofof_eN : string
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    40
  val sine_eN : string
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    41
  val snarkN : string
42938
c124032ac96f added Waldmeister
blanchet
parents: 42937
diff changeset
    42
  val waldmeisterN : 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 z3_atpN : string
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
    44
  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
    45
  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
    46
    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
    47
    -> (failure * string) list -> formula_kind -> formula_kind -> format list
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    48
    -> (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
    49
  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
    50
  val get_atp : theory -> string -> atp_config
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41725
diff changeset
    51
  val supported_atps : theory -> string list
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    52
  val is_atp_installed : theory -> string -> bool
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
    53
  val refresh_systems_on_tptp : unit -> unit
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
    54
  val setup : theory -> theory
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    55
end;
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    56
36376
e83d52a52449 renamed module "ATP_Wrapper" to "ATP_Systems"
blanchet
parents: 36371
diff changeset
    57
structure ATP_Systems : ATP_SYSTEMS =
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    58
struct
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    59
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
    60
open ATP_Problem
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
    61
open ATP_Proof
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
(* ATP configuration *)
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
    64
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    65
type atp_config =
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    66
  {exec : string * string,
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    67
   required_execs : (string * string) list,
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    68
   arguments :
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    69
     Proof.context -> int -> Time.time -> (unit -> (string * real) list)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    70
     -> string,
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    71
   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
    72
   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
    73
   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
    74
   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
    75
   formats : format list,
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    76
   best_slices : Proof.context -> (real * (bool * (int * string list))) list}
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    77
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    78
(* "best_slices" must be found empirically, taking a wholistic approach since
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    79
   the ATPs are run in parallel. The "real" components give the faction of the
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    80
   time available given to the slice; these should add up to 1.0. The "bool"
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    81
   component indicates whether the slice's strategy is complete; the "int", the
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    82
   preferred number of facts to pass; the "string list", the preferred type
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    83
   systems, which should be of the form [sound] or [unsound, sound], where
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    84
   "sound" is a sound type system and "unsound" is an unsound one.
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    85
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    86
   The last slice should be the most "normal" one, because it will get all the
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    87
   time available if the other slices fail early and also because it is used for
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
    88
   remote provers and if slicing is disabled. *)
42710
84fcce345b5d further improved type system setup based on Judgment Days
blanchet
parents: 42709
diff changeset
    89
38061
685d1f0f75b3 handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents: 38049
diff changeset
    90
val known_perl_failures =
38094
d01b8119b2e0 better error and minimizer output
blanchet
parents: 38092
diff changeset
    91
  [(CantConnect, "HTTP error"),
d01b8119b2e0 better error and minimizer output
blanchet
parents: 38092
diff changeset
    92
   (NoPerl, "env: perl"),
38065
9069e1ad1527 improved ATP error handling some more
blanchet
parents: 38064
diff changeset
    93
   (NoLibwwwPerl, "Can't locate HTTP")]
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    94
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    95
(* named ATPs *)
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    96
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    97
val eN = "e"
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    98
val spassN = "spass"
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    99
val vampireN = "vampire"
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   100
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
   101
val tofof_eN = "tofof_e"
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   102
val sine_eN = "sine_e"
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   103
val snarkN = "snark"
42938
c124032ac96f added Waldmeister
blanchet
parents: 42937
diff changeset
   104
val waldmeisterN = "waldmeister"
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   105
val remote_prefix = "remote_"
38001
a9b47b85ca24 reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents: 38000
diff changeset
   106
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   107
structure Data = Theory_Data
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   108
(
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   109
  type T = (atp_config * stamp) Symtab.table
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   110
  val empty = Symtab.empty
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   111
  val extend = I
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   112
  fun merge data : T = Symtab.merge (eq_snd op =) data
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   113
    handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   114
)
38017
3ad3e3ca2451 move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
blanchet
parents: 38015
diff changeset
   115
38737
bdcb23701448 better workaround for E's off-by-one-second issue
blanchet
parents: 38691
diff changeset
   116
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
   117
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   118
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   119
(* E *)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   120
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
   121
(* 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
   122
   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
   123
   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
   124
   lower. *)
38737
bdcb23701448 better workaround for E's off-by-one-second issue
blanchet
parents: 38691
diff changeset
   125
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
   126
  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
   127
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   128
val tstp_proof_delims =
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   129
  ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   130
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   131
val e_slicesN = "slices"
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   132
val e_autoN = "auto"
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   133
val e_fun_weightN = "fun_weight"
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   134
val e_sym_offset_weightN = "sym_offset_weight"
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   135
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   136
val e_weight_method =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   137
  Attrib.setup_config_string @{binding atp_e_weight_method} (K e_slicesN)
41770
a710e96583d5 adjust fudge factors
blanchet
parents: 41769
diff changeset
   138
(* FUDGE *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   139
val e_default_fun_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   140
  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
   141
val e_fun_weight_base =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   142
  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
   143
val e_fun_weight_span =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   144
  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
   145
val e_default_sym_offs_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   146
  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
   147
val e_sym_offs_weight_base =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   148
  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
   149
val e_sym_offs_weight_span =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   150
  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
   151
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   152
fun e_weight_method_case method fw sow =
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   153
  if method = e_fun_weightN then fw
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   154
  else if method = e_sym_offset_weightN then sow
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   155
  else raise Fail ("unexpected" ^ quote method)
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   156
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   157
fun scaled_e_weight ctxt method w =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   158
  w * Config.get ctxt
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   159
          (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
   160
  + Config.get ctxt
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   161
        (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
   162
  |> 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
   163
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   164
fun e_weight_arguments ctxt method weights =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   165
  if method = e_autoN then
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   166
    "-xAutoDev"
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   167
  else
41314
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   168
    "--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
   169
    \--destructive-er-aggressive --destructive-er --presat-simplify \
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   170
    \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   171
    \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   172
    \-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
   173
    "(SimulateSOS, " ^
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   174
    (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
   175
     |> 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
   176
    ",20,1.5,1.5,1" ^
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   177
    (weights ()
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   178
     |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight ctxt method w)
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   179
     |> implode) ^
41314
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   180
    "),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
   181
    \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
   182
    \FIFOWeight(PreferProcessed))'"
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41269
diff changeset
   183
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   184
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
   185
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   186
fun effective_e_weight_method ctxt =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   187
  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
   188
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   189
(* 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
   190
fun method_for_slice ctxt slice =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   191
  let val method = effective_e_weight_method ctxt in
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   192
    if method = e_slicesN then
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   193
      case slice of
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   194
        0 => e_sym_offset_weightN
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   195
      | 1 => e_autoN
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   196
      | 2 => e_fun_weightN
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   197
      | _ => raise Fail "no such slice"
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   198
    else
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   199
      method
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   200
  end
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   201
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   202
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
   203
  {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
   204
   required_execs = [],
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   205
   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
   206
     "--tstp-in --tstp-out -l5 " ^
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   207
     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
   208
     " -tAutoDev --silent --cpu-limit=" ^
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   209
     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
   210
   proof_delims = [tstp_proof_delims],
36265
41c9e755e552 distinguish between the different ATP errors in the user interface;
blanchet
parents: 36264
diff changeset
   211
   known_failures =
37995
06f02b15ef8a generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents: 37994
diff changeset
   212
     [(Unprovable, "SZS status: CounterSatisfiable"),
06f02b15ef8a generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents: 37994
diff changeset
   213
      (Unprovable, "SZS status CounterSatisfiable"),
42844
f133c030856a better error reporting: detect missing E proofs and remove Vampire native format error
blanchet
parents: 42779
diff changeset
   214
      (ProofMissing, "SZS status Theorem"),
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   215
      (TimedOut, "Failure: Resource limit exceeded (time)"),
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   216
      (TimedOut, "time limit exceeded"),
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   217
      (OutOfResources,
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   218
       "# Cannot determine problem status within resource limit"),
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   219
      (OutOfResources, "SZS status: ResourceOut"),
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   220
      (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
   221
   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
   222
   prem_kind = Conjecture,
42937
cabb3a947894 reorganized ATP formats a little bit
blanchet
parents: 42882
diff changeset
   223
   formats = [FOF],
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   224
   best_slices = fn ctxt =>
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   225
     (* FUDGE *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   226
     if effective_e_weight_method ctxt = e_slicesN then
42853
de1fe9eaf3f4 tweaked ATP type systems further based on Judgment Day
blanchet
parents: 42844
diff changeset
   227
       [(0.333, (true, (100, ["poly_preds"]))) (* sym_offset_weight *),
de1fe9eaf3f4 tweaked ATP type systems further based on Judgment Day
blanchet
parents: 42844
diff changeset
   228
        (0.333, (true, (800, ["mangled_preds_heavy"]))) (* auto *),
de1fe9eaf3f4 tweaked ATP type systems further based on Judgment Day
blanchet
parents: 42844
diff changeset
   229
        (0.334, (true, (200, ["mangled_tags!", "mangled_tags?"])))
de1fe9eaf3f4 tweaked ATP type systems further based on Judgment Day
blanchet
parents: 42844
diff changeset
   230
                                                               (* fun_weight *)]
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
   231
     else
42853
de1fe9eaf3f4 tweaked ATP type systems further based on Judgment Day
blanchet
parents: 42844
diff changeset
   232
       [(1.0, (true, (200, ["mangled_tags!", "mangled_tags?"])))]}
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   233
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   234
val e = (eN, e_config)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   235
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   236
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   237
(* SPASS *)
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   238
42725
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   239
val spass_force_sos =
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   240
  Attrib.setup_config_bool @{binding atp_spass_force_sos} (K false)
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   241
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
   242
(* 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
   243
   counteracting the presence of "hAPP". *)
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   244
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
   245
  {exec = ("ISABELLE_ATP", "scripts/spass"),
39002
a2d7be688ea1 add dependency of "spass" script
blanchet
parents: 38999
diff changeset
   246
   required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
42725
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   247
   arguments = fn ctxt => 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
   248
     ("-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
   249
      \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
42853
de1fe9eaf3f4 tweaked ATP type systems further based on Judgment Day
blanchet
parents: 42844
diff changeset
   250
     |> (slice < 2 orelse Config.get ctxt spass_force_sos) ? prefix "-SOS=1 ",
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   251
   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
   252
   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
   253
     known_perl_failures @
37413
e856582fe9c4 improve ATP-specific error messages
blanchet
parents: 37347
diff changeset
   254
     [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   255
      (TimedOut, "SPASS beiseite: Ran out of time"),
36965
67ae217c6b5c identify common SPASS error more clearly
blanchet
parents: 36924
diff changeset
   256
      (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
37413
e856582fe9c4 improve ATP-specific error messages
blanchet
parents: 37347
diff changeset
   257
      (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
   258
      (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
   259
      (SpassTooOld, "tptp2dfg"),
e2a3c435334b more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
blanchet
parents: 39262
diff changeset
   260
      (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
   261
   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
   262
   prem_kind = Conjecture,
42937
cabb3a947894 reorganized ATP formats a little bit
blanchet
parents: 42882
diff changeset
   263
   formats = [FOF],
42725
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   264
   best_slices = fn ctxt =>
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   265
     (* FUDGE *)
42853
de1fe9eaf3f4 tweaked ATP type systems further based on Judgment Day
blanchet
parents: 42844
diff changeset
   266
     [(0.333, (false, (150, ["mangled_preds_heavy"]))) (* SOS *),
de1fe9eaf3f4 tweaked ATP type systems further based on Judgment Day
blanchet
parents: 42844
diff changeset
   267
      (0.333, (false, (150, ["mangled_preds?"]))) (* SOS *),
de1fe9eaf3f4 tweaked ATP type systems further based on Judgment Day
blanchet
parents: 42844
diff changeset
   268
      (0.334, (true, (150, ["poly_preds"]))) (* ~SOS *)]
42725
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   269
     |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   270
         else I)}
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   271
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   272
val spass = (spassN, spass_config)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   273
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   274
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   275
(* Vampire *)
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   276
42725
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   277
val vampire_force_sos =
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   278
  Attrib.setup_config_bool @{binding atp_vampire_force_sos} (K false)
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   279
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   280
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
   281
  {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
   282
   required_execs = [],
42725
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   283
   arguments = fn ctxt => fn slice => fn timeout => fn _ =>
42748
a37095d03074 drop support for Vampire's native output format -- it has too many undocumented oddities, e.g. "BDD definition:" lines
blanchet
parents: 42725
diff changeset
   284
     "--proof tptp --mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
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
   285
     " --thanks \"Andrei and Krystof\" --input_file"
42853
de1fe9eaf3f4 tweaked ATP type systems further based on Judgment Day
blanchet
parents: 42844
diff changeset
   286
     |> (slice < 2 orelse Config.get ctxt vampire_force_sos)
42725
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   287
        ? prefix "--sos on ",
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   288
   proof_delims =
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   289
     [("=========== Refutation ==========",
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   290
       "======= End of refutation ======="),
38033
df99f022751d support latest version of Vampire (1.0) locally
blanchet
parents: 38032
diff changeset
   291
      ("% SZS output start Refutation", "% SZS output end Refutation"),
df99f022751d support latest version of Vampire (1.0) locally
blanchet
parents: 38032
diff changeset
   292
      ("% 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
   293
   known_failures =
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   294
     [(Unprovable, "UNPROVABLE"),
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   295
      (IncompleteUnprovable, "CANNOT PROVE"),
42449
494e4ac5b0f8 detect some unsound proofs before showing them to the user
blanchet
parents: 42443
diff changeset
   296
      (IncompleteUnprovable, "SZS status GaveUp"),
42882
391e41ac038b make sure the Vampire incomplete proof detection code kicks in
blanchet
parents: 42855
diff changeset
   297
      (ProofIncomplete, "predicate_definition_introduction,[]"),
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
   298
      (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
   299
      (Unprovable, "Satisfiability detected"),
38647
5500241da479 play with fudge factor + parse one more Vampire error
blanchet
parents: 38646
diff changeset
   300
      (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
   301
      (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
   302
      (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
   303
   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
   304
   prem_kind = Conjecture,
42937
cabb3a947894 reorganized ATP formats a little bit
blanchet
parents: 42882
diff changeset
   305
   formats = [FOF],
42725
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   306
   best_slices = fn ctxt =>
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   307
     (* FUDGE *)
42853
de1fe9eaf3f4 tweaked ATP type systems further based on Judgment Day
blanchet
parents: 42844
diff changeset
   308
     [(0.333, (false, (400, ["mangled_preds_heavy"]))) (* SOS *),
de1fe9eaf3f4 tweaked ATP type systems further based on Judgment Day
blanchet
parents: 42844
diff changeset
   309
      (0.333, (false, (400, ["mangled_tags?"]))) (* SOS *),
de1fe9eaf3f4 tweaked ATP type systems further based on Judgment Day
blanchet
parents: 42844
diff changeset
   310
      (0.334, (true, (400, ["poly_preds"]))) (* ~SOS *)]
42725
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   311
     |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
64dea91bbe0e added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
blanchet
parents: 42723
diff changeset
   312
         else I)}
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   313
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   314
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
   315
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   316
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   317
(* Z3 with TPTP syntax *)
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   318
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   319
val z3_atp_config : atp_config =
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   320
  {exec = ("Z3_HOME", "z3"),
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   321
   required_execs = [],
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   322
   arguments = fn _ => fn _ => fn timeout => fn _ =>
41766
26dab6eca1c2 make experimental "Z3 ATP" work on Linux as well
blanchet
parents: 41765
diff changeset
   323
     "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
   324
   proof_delims = [],
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   325
   known_failures =
41742
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   326
     [(Unprovable, "\nsat"),
11e862c68b40 automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
blanchet
parents: 41741
diff changeset
   327
      (IncompleteUnprovable, "\nunknown"),
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   328
      (IncompleteUnprovable, "SZS status Satisfiable"),
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   329
      (ProofMissing, "\nunsat"),
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   330
      (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
   331
   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
   332
   prem_kind = Hypothesis,
42937
cabb3a947894 reorganized ATP formats a little bit
blanchet
parents: 42882
diff changeset
   333
   formats = [FOF],
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   334
   best_slices =
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   335
     (* FUDGE (FIXME) *)
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   336
     K [(1.0, (false, (250, [])))]}
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   337
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   338
val z3_atp = (z3_atpN, z3_atp_config)
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   339
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   340
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   341
(* Remote ATP invocation via SystemOnTPTP *)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   342
38061
685d1f0f75b3 handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents: 38049
diff changeset
   343
val systems = Synchronized.var "atp_systems" ([] : string list)
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   344
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   345
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
   346
  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
   347
    (output, 0) => split_lines output
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   348
  | (output, _) =>
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   349
    error (case extract_known_failure known_perl_failures output of
41744
a18e7bbca258 make minimizer verbose
blanchet
parents: 41742
diff changeset
   350
             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
   351
           | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   352
42537
25ceb855a18b improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work
blanchet
parents: 42535
diff changeset
   353
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
   354
    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
   355
  | 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
   356
    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
   357
      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
   358
    | 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
   359
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   360
fun get_system name versions =
38589
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38588
diff changeset
   361
  Synchronized.change_result systems
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38588
diff changeset
   362
      (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
   363
                     |> `(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
   364
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
   365
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
   366
  case get_system name versions of
39010
344028ecc00e show real CPU time
blanchet
parents: 39002
diff changeset
   367
    SOME sys => sys
41269
blanchet
parents: 41238
diff changeset
   368
  | NONE => error ("System " ^ quote name ^
blanchet
parents: 41238
diff changeset
   369
                   " is not available at SystemOnTPTP.")
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   370
41148
f5229ab54284 added timeout max for remote server invocation
blanchet
parents: 40669
diff changeset
   371
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
   372
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
   373
fun remote_config system_name system_versions proof_delims known_failures
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   374
                  conj_sym_kind prem_kind formats best_slice : 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
   375
  {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
   376
   required_execs = [],
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   377
   arguments = fn _ => fn _ => fn timeout => fn _ =>
41148
f5229ab54284 added timeout max for remote server invocation
blanchet
parents: 40669
diff changeset
   378
     " -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
   379
     ^ " -s " ^ the_system system_name system_versions,
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   380
   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
   381
   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
   382
     known_failures @ known_perl_failures @
42571
67e2f2df68d5 recognize more SystemOnTPTP errors
blanchet
parents: 42559
diff changeset
   383
     [(IncompleteUnprovable, "says Unknown"),
42584
8121a31b6754 pick up GaveUp error on SystemOnTPTP
blanchet
parents: 42579
diff changeset
   384
      (IncompleteUnprovable, "says GaveUp"),
42571
67e2f2df68d5 recognize more SystemOnTPTP errors
blanchet
parents: 42559
diff changeset
   385
      (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
   386
   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
   387
   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
   388
   formats = formats,
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   389
   best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))]}
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   390
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
   391
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
   392
        ({proof_delims, known_failures, conj_sym_kind, prem_kind, formats,
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   393
          best_slices, ...} : 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
   394
  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
   395
                conj_sym_kind prem_kind formats
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   396
                (best_slices #> List.last #> snd #> snd)
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   397
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   398
fun remote_atp name system_name system_versions proof_delims known_failures
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   399
        conj_sym_kind prem_kind formats best_slice =
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   400
  (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
   401
   remote_config system_name system_versions proof_delims known_failures
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   402
                 conj_sym_kind prem_kind formats best_slice)
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   403
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
   404
  (remote_prefix ^ name, remotify_config system_name system_versions config)
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   405
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   406
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
   407
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
   408
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
   409
val remote_tofof_e =
42559
791d7153c48d better known failure recognition for ToFoF-E
blanchet
parents: 42537
diff changeset
   410
  remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
42937
cabb3a947894 reorganized ATP formats a little bit
blanchet
parents: 42882
diff changeset
   411
             Axiom Conjecture [TFF] (K (200, ["simple"]) (* FUDGE *))
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   412
val remote_sine_e =
42937
cabb3a947894 reorganized ATP formats a little bit
blanchet
parents: 42882
diff changeset
   413
  remote_atp sine_eN "SInE" ["0.4"] [] [] Axiom Conjecture [FOF]
42853
de1fe9eaf3f4 tweaked ATP type systems further based on Judgment Day
blanchet
parents: 42844
diff changeset
   414
             (K (500, ["poly_tags_heavy!", "poly_tags_heavy"]) (* FUDGE *))
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   415
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
   416
  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
   417
             [("refutation.", "end_refutation.")] [] Hypothesis Conjecture
42937
cabb3a947894 reorganized ATP formats a little bit
blanchet
parents: 42882
diff changeset
   418
             [TFF, FOF] (K (250, ["simple"]) (* FUDGE *))
42938
c124032ac96f added Waldmeister
blanchet
parents: 42937
diff changeset
   419
val remote_waldmeister =
c124032ac96f added Waldmeister
blanchet
parents: 42937
diff changeset
   420
  remote_atp waldmeisterN "Waldmeister" ["710"]
c124032ac96f added Waldmeister
blanchet
parents: 42937
diff changeset
   421
             [("#START OF PROOF", "Proved Goals:")] [] Hypothesis Conjecture
c124032ac96f added Waldmeister
blanchet
parents: 42937
diff changeset
   422
             [FOF] (K (250, ["poly_args"]) (* FUDGE *))
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   423
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   424
(* Setup *)
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   425
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   426
fun add_atp (name, config) thy =
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   427
  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
   428
  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
   429
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   430
fun get_atp thy name =
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   431
  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
   432
  handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   433
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41725
diff changeset
   434
val supported_atps = Symtab.keys o Data.get
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36370
diff changeset
   435
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   436
fun is_atp_installed thy name =
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   437
  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
   438
    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
   439
  end
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36370
diff changeset
   440
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   441
fun refresh_systems_on_tptp () =
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   442
  Synchronized.change systems (fn _ => get_systems ())
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   443
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   444
val atps = [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
42938
c124032ac96f added Waldmeister
blanchet
parents: 42937
diff changeset
   445
            remote_tofof_e, remote_sine_e, remote_snark, remote_waldmeister]
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   446
val setup = fold add_atp atps
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
   447
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   448
end;