src/HOL/Tools/ATP/atp_systems.ML
author blanchet
Tue, 07 Aug 2012 22:54:27 +0200
changeset 48720 95669b431edd
parent 48716 1d2a12bb0640
child 48801 55874425fd32
permissions -rw-r--r--
proper quoting
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
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
    10
  type term_order = ATP_Problem.term_order
45301
866b075aa99b added sorted DFG output for coming version of SPASS
blanchet
parents: 45300
diff changeset
    11
  type atp_format = ATP_Problem.atp_format
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
    12
  type formula_role = ATP_Problem.formula_role
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
    13
  type failure = ATP_Proof.failure
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    14
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46407
diff changeset
    15
  type slice_spec = int * atp_format * string * string * bool
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    16
  type atp_config =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48232
diff changeset
    17
    {exec : string list * string list,
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    18
     arguments :
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
    19
       Proof.context -> bool -> string -> Time.time
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
    20
       -> term_order * (unit -> (string * int) list)
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
    21
          * (unit -> (string * real) list) -> string,
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    22
     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
    23
     known_failures : (failure * string) list,
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
    24
     prem_role : formula_role,
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
    25
     best_slices : Proof.context -> (real * (slice_spec * string)) list,
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
    26
     best_max_mono_iters : int,
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
    27
     best_max_new_mono_instances : int}
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    28
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
    29
  val default_max_mono_iters : int
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
    30
  val default_max_new_mono_instances : int
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
    31
  val force_sos : bool Config.T
47032
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
    32
  val term_order : string Config.T
43566
a818d5a34cca filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents: 43529
diff changeset
    33
  val e_smartN : string
a818d5a34cca filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents: 43529
diff changeset
    34
  val e_autoN : string
a818d5a34cca filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents: 43529
diff changeset
    35
  val e_fun_weightN : string
a818d5a34cca filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents: 43529
diff changeset
    36
  val e_sym_offset_weightN : string
47032
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
    37
  val e_selection_heuristic : string Config.T
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    38
  val e_default_fun_weight : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    39
  val e_fun_weight_base : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    40
  val e_fun_weight_span : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    41
  val e_default_sym_offs_weight : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    42
  val e_sym_offs_weight_base : real Config.T
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    43
  val e_sym_offs_weight_span : real Config.T
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
    44
  val alt_ergoN : string
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
    45
  val dummy_thfN : string
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    46
  val eN : string
48651
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
    47
  val e_malesN : string
44590
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
    48
  val e_sineN : string
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
    49
  val e_tofofN : string
45338
b9d5d3625e9a added remote iProver(-Eq) for experimentation
blanchet
parents: 45304
diff changeset
    50
  val iproverN : string
b9d5d3625e9a added remote iProver(-Eq) for experimentation
blanchet
parents: 45304
diff changeset
    51
  val iprover_eqN : string
44590
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
    52
  val leo2N : string
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
    53
  val satallaxN : string
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
    54
  val snarkN : string
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    55
  val spassN : string
48131
1016664b8feb started adding polymophic SPASS output
blanchet
parents: 48130
diff changeset
    56
  val spass_polyN : string
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    57
  val vampireN : string
42938
c124032ac96f added Waldmeister
blanchet
parents: 42937
diff changeset
    58
  val waldmeisterN : string
44423
f74707e12d30 exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents: 44422
diff changeset
    59
  val z3_tptpN : string
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
    60
  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
    61
  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
    62
    string -> string -> string list -> (string * string) list
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
    63
    -> (failure * string) list -> formula_role
47606
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47506
diff changeset
    64
    -> (Proof.context -> slice_spec * string) -> string * (unit -> atp_config)
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47506
diff changeset
    65
  val add_atp : string * (unit -> atp_config) -> theory -> theory
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47506
diff changeset
    66
  val get_atp : theory -> string -> (unit -> atp_config)
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41725
diff changeset
    67
  val supported_atps : theory -> string list
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    68
  val is_atp_installed : theory -> string -> bool
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
    69
  val refresh_systems_on_tptp : unit -> unit
47055
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
    70
  val effective_term_order : Proof.context -> string -> term_order
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
    71
  val setup : theory -> theory
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    72
end;
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    73
36376
e83d52a52449 renamed module "ATP_Wrapper" to "ATP_Systems"
blanchet
parents: 36371
diff changeset
    74
structure ATP_Systems : ATP_SYSTEMS =
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    75
struct
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    76
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
    77
open ATP_Problem
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
    78
open ATP_Proof
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 45876
diff changeset
    79
open ATP_Problem_Generate
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
    80
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    81
(* ATP configuration *)
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
    82
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
    83
val default_max_mono_iters = 3 (* FUDGE *)
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
    84
val default_max_new_mono_instances = 200 (* FUDGE *)
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
    85
46409
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46407
diff changeset
    86
type slice_spec = int * atp_format * string * string * bool
d4754183ccce made option available to users (mostly for experiments)
blanchet
parents: 46407
diff changeset
    87
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
    88
type atp_config =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48232
diff changeset
    89
  {exec : string list * string list,
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
    90
   arguments :
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
    91
     Proof.context -> bool -> string -> Time.time
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
    92
     -> term_order * (unit -> (string * int) list)
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
    93
        * (unit -> (string * real) list) -> string,
42578
1eaf4d437d4c define type system in ATP module so that ATPs can suggest a type system
blanchet
parents: 42577
diff changeset
    94
   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
    95
   known_failures : (failure * string) list,
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
    96
   prem_role : formula_role,
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
    97
   best_slices : Proof.context -> (real * (slice_spec * string)) list,
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
    98
   best_max_mono_iters : int,
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
    99
   best_max_new_mono_instances : int}
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   100
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   101
(* "best_slices" must be found empirically, taking a wholistic approach since
46407
30e9720cc0b9 optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents: 46402
diff changeset
   102
   the ATPs are run in parallel. The "real" component gives the faction of the
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   103
   time available given to the slice and should add up to 1.0. The "int"
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   104
   component indicates the preferred number of facts to pass; the first
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   105
   "string", the preferred type system (which should be sound or quasi-sound);
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   106
   the second "string", the preferred lambda translation scheme; the "bool",
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   107
   whether uncurried aliased should be generated; the third "string", extra
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   108
   information to the prover (e.g., SOS or no SOS).
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   109
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   110
   The last slice should be the most "normal" one, because it will get all the
43569
b342cd125533 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents: 43567
diff changeset
   111
   time available if the other slices fail early and also because it is used if
b342cd125533 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents: 43567
diff changeset
   112
   slicing is disabled (e.g., by the minimizer). *)
42710
84fcce345b5d further improved type system setup based on Judgment Days
blanchet
parents: 42709
diff changeset
   113
38061
685d1f0f75b3 handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents: 38049
diff changeset
   114
val known_perl_failures =
38094
d01b8119b2e0 better error and minimizer output
blanchet
parents: 38092
diff changeset
   115
  [(CantConnect, "HTTP error"),
d01b8119b2e0 better error and minimizer output
blanchet
parents: 38092
diff changeset
   116
   (NoPerl, "env: perl"),
38065
9069e1ad1527 improved ATP error handling some more
blanchet
parents: 38064
diff changeset
   117
   (NoLibwwwPerl, "Can't locate HTTP")]
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   118
45203
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   119
fun known_szs_failures wrap =
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   120
  [(Unprovable, wrap "CounterSatisfiable"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   121
   (Unprovable, wrap "Satisfiable"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   122
   (GaveUp, wrap "GaveUp"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   123
   (GaveUp, wrap "Unknown"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   124
   (GaveUp, wrap "Incomplete"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   125
   (ProofMissing, wrap "Theorem"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   126
   (ProofMissing, wrap "Unsatisfiable"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   127
   (TimedOut, wrap "Timeout"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   128
   (Inappropriate, wrap "Inappropriate"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   129
   (OutOfResources, wrap "ResourceOut"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   130
   (OutOfResources, wrap "MemoryOut"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   131
   (Interrupted, wrap "Forced"),
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   132
   (Interrupted, wrap "User")]
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   133
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   134
val known_szs_status_failures = known_szs_failures (prefix "SZS status ")
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   135
val known_says_failures = known_szs_failures (prefix " says ")
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   136
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   137
(* named ATPs *)
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   138
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   139
val alt_ergoN = "alt_ergo"
47055
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   140
val dummy_thfN = "dummy_thf" (* for experiments *)
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   141
val eN = "e"
48651
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   142
val e_malesN = "e_males"
44590
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
   143
val e_sineN = "e_sine"
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
   144
val e_tofofN = "e_tofof"
45338
b9d5d3625e9a added remote iProver(-Eq) for experimentation
blanchet
parents: 45304
diff changeset
   145
val iproverN = "iprover"
b9d5d3625e9a added remote iProver(-Eq) for experimentation
blanchet
parents: 45304
diff changeset
   146
val iprover_eqN = "iprover_eq"
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   147
val leo2N = "leo2"
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   148
val satallaxN = "satallax"
44590
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
   149
val snarkN = "snark"
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   150
val spassN = "spass"
48131
1016664b8feb started adding polymophic SPASS output
blanchet
parents: 48130
diff changeset
   151
val spass_polyN = "spass_poly"
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   152
val vampireN = "vampire"
44590
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
   153
val waldmeisterN = "waldmeister"
44423
f74707e12d30 exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents: 44422
diff changeset
   154
val z3_tptpN = "z3_tptp"
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   155
val remote_prefix = "remote_"
38001
a9b47b85ca24 reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents: 38000
diff changeset
   156
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   157
structure Data = Theory_Data
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   158
(
47606
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47506
diff changeset
   159
  type T = ((unit -> atp_config) * stamp) Symtab.table
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   160
  val empty = Symtab.empty
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   161
  val extend = I
46407
30e9720cc0b9 optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents: 46402
diff changeset
   162
  fun merge data : T =
30e9720cc0b9 optimization: slice caching in case two consecutive slices are nearly identical
blanchet
parents: 46402
diff changeset
   163
    Symtab.merge (eq_snd (op =)) data
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   164
    handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   165
)
38017
3ad3e3ca2451 move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
blanchet
parents: 38015
diff changeset
   166
43981
404ae49ce29f give E at least two seconds -- anything else risks causing too early timeouts in the minimizer, because of too conservative time computations in E and eproof scripts
blanchet
parents: 43850
diff changeset
   167
fun to_secs min time = Int.max (min, (Time.toMilliseconds time + 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
   168
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   169
val sosN = "sos"
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   170
val no_sosN = "no_sos"
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   171
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   172
val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   173
47032
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
   174
val smartN = "smart"
47073
c73f7b0c7ebc generate weights and precedences for predicates as well
blanchet
parents: 47055
diff changeset
   175
(* val kboN = "kbo" *)
47032
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
   176
val lpoN = "lpo"
47034
77da780ddd6b implement term order attribute (for experiments)
blanchet
parents: 47033
diff changeset
   177
val xweightsN = "_weights"
77da780ddd6b implement term order attribute (for experiments)
blanchet
parents: 47033
diff changeset
   178
val xprecN = "_prec"
77da780ddd6b implement term order attribute (for experiments)
blanchet
parents: 47033
diff changeset
   179
val xsimpN = "_simp" (* SPASS-specific *)
47032
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
   180
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   181
(* Possible values for "atp_term_order":
47049
72bd3311ecba added term_order option to Mirabelle
blanchet
parents: 47039
diff changeset
   182
   "smart", "(kbo|lpo)(_weights)?(_prec|_simp)?" *)
47032
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
   183
val term_order =
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
   184
  Attrib.setup_config_string @{binding atp_term_order} (K smartN)
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
   185
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   186
(* Alt-Ergo *)
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   187
48130
blanchet
parents: 48129
diff changeset
   188
val alt_ergo_tff1 = TFF (Polymorphic, TPTP_Explicit)
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   189
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   190
val alt_ergo_config : atp_config =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48232
diff changeset
   191
  {exec = (["WHY3_HOME"], ["why3"]),
48651
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   192
   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   193
       "--format tff1 --prover alt-ergo --timelimit " ^
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   194
       string_of_int (to_secs 1 timeout),
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   195
   proof_delims = [],
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   196
   known_failures =
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   197
     [(ProofMissing, ": Valid"),
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   198
      (TimedOut, ": Timeout"),
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   199
      (GaveUp, ": Unknown")],
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   200
   prem_role = Hypothesis,
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   201
   best_slices = fn _ =>
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   202
     (* FUDGE *)
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   203
     [(1.0, ((100, alt_ergo_tff1, "poly_native", liftingN, false), ""))],
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   204
   best_max_mono_iters = default_max_mono_iters,
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   205
   best_max_new_mono_instances = default_max_new_mono_instances}
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   206
47646
9460f3f22365 tried to make SML/NJ happy
blanchet
parents: 47606
diff changeset
   207
val alt_ergo = (alt_ergoN, fn () => alt_ergo_config)
46643
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   208
a88bccd2b567 added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization)
blanchet
parents: 46481
diff changeset
   209
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   210
(* E *)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   211
48653
6ac7fd9b3a54 support older versions of Vampire
blanchet
parents: 48651
diff changeset
   212
fun is_e_at_least_1_3 () = (string_ord (getenv "E_VERSION", "1.3") <> LESS)
6ac7fd9b3a54 support older versions of Vampire
blanchet
parents: 48651
diff changeset
   213
fun is_e_at_least_1_6 () = (string_ord (getenv "E_VERSION", "1.6") <> LESS)
44420
3d0921b91a86 avoid TFF format with older Vampire versions
blanchet
parents: 44418
diff changeset
   214
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   215
val tstp_proof_delims =
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42955
diff changeset
   216
  [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42955
diff changeset
   217
   ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   218
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   219
val e_smartN = "smart"
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   220
val e_autoN = "auto"
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   221
val e_fun_weightN = "fun_weight"
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   222
val e_sym_offset_weightN = "sym_offset_weight"
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   223
47032
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
   224
val e_selection_heuristic =
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
   225
  Attrib.setup_config_string @{binding atp_e_selection_heuristic} (K e_smartN)
41770
a710e96583d5 adjust fudge factors
blanchet
parents: 41769
diff changeset
   226
(* FUDGE *)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   227
val e_default_fun_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   228
  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
   229
val e_fun_weight_base =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   230
  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
   231
val e_fun_weight_span =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   232
  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
   233
val e_default_sym_offs_weight =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   234
  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
   235
val e_sym_offs_weight_base =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   236
  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
   237
val e_sym_offs_weight_span =
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   238
  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
   239
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   240
fun e_selection_heuristic_case heuristic fw sow =
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   241
  if heuristic = e_fun_weightN then fw
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   242
  else if heuristic = e_sym_offset_weightN then sow
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   243
  else raise Fail ("unexpected " ^ quote heuristic)
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   244
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   245
fun scaled_e_selection_weight ctxt heuristic w =
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   246
  w * Config.get ctxt (e_selection_heuristic_case heuristic
47029
72802e2edda4 renamed E weight attribute
blanchet
parents: 46643
diff changeset
   247
                           e_fun_weight_span e_sym_offs_weight_span)
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   248
  + Config.get ctxt (e_selection_heuristic_case heuristic
47029
72802e2edda4 renamed E weight attribute
blanchet
parents: 46643
diff changeset
   249
                         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
   250
  |> 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
   251
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   252
fun e_selection_weight_arguments ctxt heuristic sel_weights =
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   253
  if heuristic = e_autoN then
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   254
    "-xAuto"
41725
7cca2de89296 added support for bleeding-edge E weighting function "SymOffsetsWeight"
blanchet
parents: 41335
diff changeset
   255
  else
43622
blanchet
parents: 43575
diff changeset
   256
    (* supplied by Stephan Schulz *)
41314
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   257
    "--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
   258
    \--destructive-er-aggressive --destructive-er --presat-simplify \
47505
e33d957ae2bf avoid option introduced in E 1.2 when invoking older versions of E
blanchet
parents: 47499
diff changeset
   259
    \--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
e33d957ae2bf avoid option introduced in E 1.2 when invoking older versions of E
blanchet
parents: 47499
diff changeset
   260
    \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   261
    e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48232
diff changeset
   262
    "(SimulateSOS," ^
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   263
    (e_selection_heuristic_case heuristic
47029
72802e2edda4 renamed E weight attribute
blanchet
parents: 46643
diff changeset
   264
         e_default_fun_weight e_default_sym_offs_weight
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   265
     |> 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
   266
    ",20,1.5,1.5,1" ^
47030
7e80e14247fc internal renamings
blanchet
parents: 47029
diff changeset
   267
    (sel_weights ()
47029
72802e2edda4 renamed E weight attribute
blanchet
parents: 46643
diff changeset
   268
     |> map (fn (s, w) => "," ^ s ^ ":" ^
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   269
                          scaled_e_selection_weight ctxt heuristic w)
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   270
     |> implode) ^
41314
2dc1dfc1bc69 use the options provided by Stephan Schulz -- much better
blanchet
parents: 41313
diff changeset
   271
    "),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
   272
    \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
   273
    \FIFOWeight(PreferProcessed))'"
41313
a96ac4d180b7 optionally supply constant weights to E -- turned off by default until properly parameterized
blanchet
parents: 41269
diff changeset
   274
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   275
val e_ord_weights =
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   276
  map (fn (s, w) => s ^ ":" ^ string_of_int w) #> space_implode ","
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   277
fun e_ord_precedence [_] = ""
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   278
  | e_ord_precedence info = info |> map fst |> space_implode "<"
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   279
47039
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47038
diff changeset
   280
fun e_term_order_info_arguments false false _ = ""
1b36a05a070d added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")
blanchet
parents: 47038
diff changeset
   281
  | e_term_order_info_arguments gen_weights gen_prec ord_info =
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   282
    let val ord_info = ord_info () in
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   283
      (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' "
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   284
       else "") ^
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   285
      (if gen_prec then "--precedence='" ^ e_ord_precedence ord_info ^ "' "
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   286
       else "")
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   287
    end
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   288
48232
712d49104b13 don't ask E to generate a detailed proofs if not needed
blanchet
parents: 48131
diff changeset
   289
fun e_shell_level_argument full_proof =
48653
6ac7fd9b3a54 support older versions of Vampire
blanchet
parents: 48651
diff changeset
   290
  if is_e_at_least_1_6 () then
48232
712d49104b13 don't ask E to generate a detailed proofs if not needed
blanchet
parents: 48131
diff changeset
   291
    " --pcl-shell-level=" ^ (if full_proof then "0" else "2")
712d49104b13 don't ask E to generate a detailed proofs if not needed
blanchet
parents: 48131
diff changeset
   292
  else
712d49104b13 don't ask E to generate a detailed proofs if not needed
blanchet
parents: 48131
diff changeset
   293
    ""
712d49104b13 don't ask E to generate a detailed proofs if not needed
blanchet
parents: 48131
diff changeset
   294
47032
73cdeed236c0 more weight attribute tuning
blanchet
parents: 47031
diff changeset
   295
fun effective_e_selection_heuristic ctxt =
48653
6ac7fd9b3a54 support older versions of Vampire
blanchet
parents: 48651
diff changeset
   296
  if is_e_at_least_1_3 () then Config.get ctxt e_selection_heuristic
48232
712d49104b13 don't ask E to generate a detailed proofs if not needed
blanchet
parents: 48131
diff changeset
   297
  else e_autoN
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   298
48653
6ac7fd9b3a54 support older versions of Vampire
blanchet
parents: 48651
diff changeset
   299
fun e_kbo () = if is_e_at_least_1_3 () then "KBO6" else "KBO"
47505
e33d957ae2bf avoid option introduced in E 1.2 when invoking older versions of E
blanchet
parents: 47499
diff changeset
   300
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   301
val e_config : atp_config =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48232
diff changeset
   302
  {exec = (["E_HOME"], ["eproof_ram", "eproof"]),
48651
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   303
   arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout =>
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   304
       fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   305
       "--tstp-in --tstp-out --output-level=5 --silent " ^
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   306
       e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   307
       e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   308
       "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   309
       "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   310
       e_shell_level_argument full_proof,
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48232
diff changeset
   311
   proof_delims = tstp_proof_delims,
36265
41c9e755e552 distinguish between the different ATP errors in the user interface;
blanchet
parents: 36264
diff changeset
   312
   known_failures =
45203
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   313
     [(TimedOut, "Failure: Resource limit exceeded (time)"),
47972
96c9b8381909 better handling of incomplete TSTP proofs
blanchet
parents: 47962
diff changeset
   314
      (TimedOut, "time limit exceeded")] @
96c9b8381909 better handling of incomplete TSTP proofs
blanchet
parents: 47962
diff changeset
   315
     known_szs_status_failures,
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   316
   prem_role = Conjecture,
42646
4781fcd53572 replaced some Unsynchronized.refs with Config.Ts
blanchet
parents: 42643
diff changeset
   317
   best_slices = fn ctxt =>
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   318
     let val heuristic = effective_e_selection_heuristic ctxt in
43474
423cd1ecf714 optimized E's time slicing, based on latest exhaustive Judgment Day results
blanchet
parents: 43473
diff changeset
   319
       (* FUDGE *)
47038
2409b484e1cc continued implementation of term ordering attributes
blanchet
parents: 47034
diff changeset
   320
       if heuristic = e_smartN then
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   321
         [(0.333, ((500, FOF, "mono_tags??", combsN, false), e_fun_weightN)),
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   322
          (0.334, ((50, FOF, "mono_guards??", combsN, false), e_fun_weightN)),
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   323
          (0.333, ((1000, FOF, "mono_tags??", combsN, false), e_sym_offset_weightN))]
43473
fb2713b803e6 deal with ATP time slices in a more flexible/robust fashion
blanchet
parents: 43467
diff changeset
   324
       else
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   325
         [(1.0, ((500, FOF, "mono_tags??", combsN, false), heuristic))]
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   326
     end,
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   327
   best_max_mono_iters = default_max_mono_iters,
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   328
   best_max_new_mono_instances = default_max_new_mono_instances}
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   329
47646
9460f3f22365 tried to make SML/NJ happy
blanchet
parents: 47606
diff changeset
   330
val e = (eN, fn () => e_config)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   331
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   332
48651
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   333
(* E-MaLeS *)
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   334
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   335
val e_males_config : atp_config =
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   336
  {exec = (["E_MALES_HOME"], ["emales.py"]),
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   337
   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   338
       "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p",
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   339
   proof_delims = tstp_proof_delims,
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   340
   known_failures = #known_failures e_config,
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   341
   prem_role = Conjecture,
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   342
   best_slices =
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   343
     (* FUDGE *)
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   344
     K [(1.0, ((1000, FOF, "mono_tags??", combsN, false), ""))],
48651
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   345
   best_max_mono_iters = default_max_mono_iters,
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   346
   best_max_new_mono_instances = default_max_new_mono_instances}
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   347
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   348
val e_males = (e_malesN, fn () => e_males_config)
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   349
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   350
48700
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   351
(* iProver *)
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   352
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   353
val iprover_config : atp_config =
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   354
  {exec = (["IPROVER_HOME"], ["iprover"]),
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   355
   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
48720
95669b431edd proper quoting
blanchet
parents: 48716
diff changeset
   356
       "--clausifier \"$IPROVER_HOME\"/vclausify_rel --time_out_real " ^
48700
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   357
       string_of_real (Time.toReal timeout),
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   358
   proof_delims = tstp_proof_delims,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   359
   known_failures =
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   360
     [(ProofIncomplete, "% SZS output start CNFRefutation")] @
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   361
     known_szs_status_failures,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   362
   prem_role = Hypothesis,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   363
   best_slices =
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   364
     (* FUDGE *)
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   365
     K [(1.0, ((150, FOF, "mono_guards??", liftingN, false), ""))],
48700
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   366
   best_max_mono_iters = default_max_mono_iters,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   367
   best_max_new_mono_instances = default_max_new_mono_instances}
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   368
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   369
val iprover = (iproverN, fn () => iprover_config)
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   370
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   371
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   372
(* iProver-Eq *)
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   373
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   374
val iprover_eq_config : atp_config =
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   375
  {exec = (["IPROVER_EQ_HOME"], ["iprover-eq"]),
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   376
   arguments = #arguments iprover_config,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   377
   proof_delims = #proof_delims iprover_config,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   378
   known_failures = #known_failures iprover_config,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   379
   prem_role = #prem_role iprover_config,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   380
   best_slices = #best_slices iprover_config,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   381
   best_max_mono_iters = #best_max_mono_iters iprover_config,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   382
   best_max_new_mono_instances = #best_max_new_mono_instances iprover_config}
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   383
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   384
val iprover_eq = (iprover_eqN, fn () => iprover_eq_config)
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   385
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   386
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   387
(* LEO-II *)
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   388
48004
989a34fa72b3 don't generate definitions for LEO-II -- this cuases more harm than good
blanchet
parents: 47985
diff changeset
   389
(* LEO-II supports definitions, but it performs significantly better on our
989a34fa72b3 don't generate definitions for LEO-II -- this cuases more harm than good
blanchet
parents: 47985
diff changeset
   390
   benchmarks when they are not used. *)
989a34fa72b3 don't generate definitions for LEO-II -- this cuases more harm than good
blanchet
parents: 47985
diff changeset
   391
val leo2_thf0 =
48130
blanchet
parents: 48129
diff changeset
   392
  THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs)
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44596
diff changeset
   393
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   394
val leo2_config : atp_config =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48232
diff changeset
   395
  {exec = (["LEO2_HOME"], ["leo"]),
48651
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   396
   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   397
       "--foatp e --atp e=\"$E_HOME\"/eprover \
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   398
       \--atp epclextract=\"$E_HOME\"/epclextract \
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   399
       \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout),
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   400
   proof_delims = tstp_proof_delims,
45207
1d13334628a9 one more LEO-II failure
blanchet
parents: 45203
diff changeset
   401
   known_failures =
47974
08d2dcc2dab9 improved LEO-II definition handling -- still hoping for a fix directly in LEO-II
blanchet
parents: 47972
diff changeset
   402
     [(TimedOut, "CPU time limit exceeded, terminating"),
47972
96c9b8381909 better handling of incomplete TSTP proofs
blanchet
parents: 47962
diff changeset
   403
      (GaveUp, "No.of.Axioms")] @
96c9b8381909 better handling of incomplete TSTP proofs
blanchet
parents: 47962
diff changeset
   404
     known_szs_status_failures,
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   405
   prem_role = Hypothesis,
47914
94f37848b7c9 LEO-II's "--sos" option confusingly disables rather than enables SOS, and SOS seems to be ignored anyway; also, pass a number of facts that's more appropriate for each prover
blanchet
parents: 47912
diff changeset
   406
   best_slices =
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   407
     (* FUDGE *)
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   408
     K [(1.0, ((40, leo2_thf0, "mono_native_higher", keep_lamsN, false), ""))],
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   409
   best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   410
   best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
39491
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   411
47646
9460f3f22365 tried to make SML/NJ happy
blanchet
parents: 47606
diff changeset
   412
val leo2 = (leo2N, fn () => leo2_config)
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   413
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   414
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   415
(* Satallax *)
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   416
48004
989a34fa72b3 don't generate definitions for LEO-II -- this cuases more harm than good
blanchet
parents: 47985
diff changeset
   417
val satallax_thf0 =
48130
blanchet
parents: 48129
diff changeset
   418
  THF (Monomorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44596
diff changeset
   419
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   420
val satallax_config : atp_config =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48232
diff changeset
   421
  {exec = (["SATALLAX_HOME"], ["satallax"]),
48651
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   422
   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   423
       "-p hocore -t " ^ string_of_int (to_secs 1 timeout),
45162
170dffc6df75 parse Satallax unsat cores
blanchet
parents: 44786
diff changeset
   424
   proof_delims =
170dffc6df75 parse Satallax unsat cores
blanchet
parents: 44786
diff changeset
   425
     [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
45203
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   426
   known_failures = known_szs_status_failures,
47981
df35a8dd6368 gracefully handle definition-looking premises
blanchet
parents: 47976
diff changeset
   427
   prem_role = Hypothesis,
44416
cabd06b69c18 added formats to the slice and use TFF for remote Vampire
blanchet
parents: 44391
diff changeset
   428
   best_slices =
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44596
diff changeset
   429
     (* FUDGE *)
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   430
     K [(1.0, ((60, satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))],
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   431
   best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   432
   best_max_new_mono_instances = default_max_new_mono_instances div 2 (* FUDGE *)}
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   433
47646
9460f3f22365 tried to make SML/NJ happy
blanchet
parents: 47606
diff changeset
   434
val satallax = (satallaxN, fn () => satallax_config)
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   435
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   436
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   437
(* SPASS *)
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
   438
48005
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   439
val spass_H1SOS = "-Heuristic=1 -SOS"
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   440
val spass_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0"
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   441
val spass_H2SOS = "-Heuristic=2 -SOS"
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   442
val spass_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   443
val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
47055
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   444
48005
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   445
(* FIXME: Make "SPASS_NEW_HOME" legacy. *)
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   446
val spass_config : atp_config =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48232
diff changeset
   447
  {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
48005
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   448
   arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ =>
48651
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   449
       ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   450
       |> extra_options <> "" ? prefix (extra_options ^ " "),
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   451
   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
   452
   known_failures =
48005
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   453
     [(OldSPASS, "Unrecognized option Isabelle"),
47950
9cb132898ac8 invite users to upgrade their SPASS (so we can get rid of old code)
blanchet
parents: 47949
diff changeset
   454
      (GaveUp, "SPASS beiseite: Completion found"),
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   455
      (TimedOut, "SPASS beiseite: Ran out of time"),
36965
67ae217c6b5c identify common SPASS error more clearly
blanchet
parents: 36924
diff changeset
   456
      (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
37413
e856582fe9c4 improve ATP-specific error messages
blanchet
parents: 37347
diff changeset
   457
      (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
   458
      (MalformedInput, "Free Variable"),
44391
7b4104df2be6 gracefully handle empty SPASS problems
blanchet
parents: 44235
diff changeset
   459
      (Unprovable, "No formulae and clauses found in input file"),
47972
96c9b8381909 better handling of incomplete TSTP proofs
blanchet
parents: 47962
diff changeset
   460
      (InternalError, "Please report this error")] @
96c9b8381909 better handling of incomplete TSTP proofs
blanchet
parents: 47962
diff changeset
   461
      known_perl_failures,
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   462
   prem_role = Conjecture,
48005
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   463
   best_slices = fn _ =>
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   464
     (* FUDGE *)
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   465
     [(0.1667, ((150, DFG Monomorphic, "mono_native", combsN, true), "")),
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   466
      (0.1667, ((500, DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)),
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   467
      (0.1666, ((50, DFG Monomorphic,  "mono_native", liftingN, true), spass_H2LR0LT0)),
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   468
      (0.1000, ((250, DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0)),
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   469
      (0.1000, ((1000, DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)),
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   470
      (0.1000, ((150, DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)),
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   471
      (0.1000, ((300, DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)),
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   472
      (0.1000, ((100, DFG Monomorphic, "mono_native", combs_and_liftingN, true), ""))],
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   473
   best_max_mono_iters = default_max_mono_iters,
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   474
   best_max_new_mono_instances = default_max_new_mono_instances}
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   475
48005
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   476
val spass = (spassN, fn () => spass_config)
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   477
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   478
(* Vampire *)
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   479
48007
955ea323ddcc tweaked remote Vampire setup
blanchet
parents: 48005
diff changeset
   480
(* Vampire 1.8 has TFF support, but the support was buggy until revision
955ea323ddcc tweaked remote Vampire setup
blanchet
parents: 48005
diff changeset
   481
   1435 (or shortly before). *)
48653
6ac7fd9b3a54 support older versions of Vampire
blanchet
parents: 48651
diff changeset
   482
fun is_vampire_at_least_1_8 () =
6ac7fd9b3a54 support older versions of Vampire
blanchet
parents: 48651
diff changeset
   483
  string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS
6ac7fd9b3a54 support older versions of Vampire
blanchet
parents: 48651
diff changeset
   484
fun is_vampire_beyond_1_8 () =
47055
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   485
  string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
44420
3d0921b91a86 avoid TFF format with older Vampire versions
blanchet
parents: 44418
diff changeset
   486
48130
blanchet
parents: 48129
diff changeset
   487
val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit)
44589
0a1dfc6365e9 first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents: 44586
diff changeset
   488
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   489
val vampire_config : atp_config =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48232
diff changeset
   490
  {exec = (["VAMPIRE_HOME"], ["vampire"]),
43569
b342cd125533 removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents: 43567
diff changeset
   491
   arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
48651
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   492
       "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
48653
6ac7fd9b3a54 support older versions of Vampire
blanchet
parents: 48651
diff changeset
   493
       " --proof tptp --output_axiom_names on" ^
6ac7fd9b3a54 support older versions of Vampire
blanchet
parents: 48651
diff changeset
   494
       (if is_vampire_at_least_1_8 () then
6ac7fd9b3a54 support older versions of Vampire
blanchet
parents: 48651
diff changeset
   495
          " --forced_options propositional_to_bdd=off"
6ac7fd9b3a54 support older versions of Vampire
blanchet
parents: 48651
diff changeset
   496
        else
6ac7fd9b3a54 support older versions of Vampire
blanchet
parents: 48651
diff changeset
   497
          "") ^
6ac7fd9b3a54 support older versions of Vampire
blanchet
parents: 48651
diff changeset
   498
       " --thanks \"Andrei and Krystof\" --input_file"
48651
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   499
       |> sos = sosN ? prefix "--sos on ",
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   500
   proof_delims =
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   501
     [("=========== Refutation ==========",
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   502
       "======= End of refutation ======="),
38033
df99f022751d support latest version of Vampire (1.0) locally
blanchet
parents: 38032
diff changeset
   503
      ("% SZS output start Refutation", "% SZS output end Refutation"),
df99f022751d support latest version of Vampire (1.0) locally
blanchet
parents: 38032
diff changeset
   504
      ("% 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
   505
   known_failures =
43050
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 42999
diff changeset
   506
     [(GaveUp, "UNPROVABLE"),
59284a13abc4 support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents: 42999
diff changeset
   507
      (GaveUp, "CANNOT PROVE"),
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   508
      (Unprovable, "Satisfiability detected"),
38647
5500241da479 play with fudge factor + parse one more Vampire error
blanchet
parents: 38646
diff changeset
   509
      (Unprovable, "Termination reason: Satisfiable"),
47972
96c9b8381909 better handling of incomplete TSTP proofs
blanchet
parents: 47962
diff changeset
   510
      (Interrupted, "Aborted by signal SIGINT")] @
96c9b8381909 better handling of incomplete TSTP proofs
blanchet
parents: 47962
diff changeset
   511
     known_szs_status_failures,
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   512
   prem_role = Conjecture,
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
   513
   best_slices = fn ctxt =>
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   514
     (* FUDGE *)
48653
6ac7fd9b3a54 support older versions of Vampire
blanchet
parents: 48651
diff changeset
   515
     (if is_vampire_beyond_1_8 () then
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   516
        [(0.333, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN)),
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   517
         (0.333, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN)),
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   518
         (0.334, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN))]
47055
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   519
      else
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   520
        [(0.333, ((150, FOF, "poly_guards??", combs_or_liftingN, false), sosN)),
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   521
         (0.333, ((500, FOF, "mono_tags??", combs_or_liftingN, false), sosN)),
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   522
         (0.334, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN))])
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   523
     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   524
         else I),
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   525
   best_max_mono_iters = default_max_mono_iters,
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   526
   best_max_new_mono_instances = default_max_new_mono_instances}
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   527
47646
9460f3f22365 tried to make SML/NJ happy
blanchet
parents: 47606
diff changeset
   528
val vampire = (vampireN, fn () => vampire_config)
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   529
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   530
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   531
(* Z3 with TPTP syntax *)
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   532
48130
blanchet
parents: 48129
diff changeset
   533
val z3_tff0 = TFF (Monomorphic, TPTP_Implicit)
44589
0a1dfc6365e9 first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents: 44586
diff changeset
   534
44423
f74707e12d30 exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents: 44422
diff changeset
   535
val z3_tptp_config : atp_config =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48232
diff changeset
   536
  {exec = (["Z3_HOME"], ["z3"]),
43354
396aaa15dd8b pass --trim option to "eproof" script to speed up proof reconstruction
blanchet
parents: 43288
diff changeset
   537
   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
48651
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   538
       "MBQI=true DISPLAY_UNSAT_CORE=true -tptp -t:" ^
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   539
       string_of_int (to_secs 1 timeout),
48539
0debf65972c7 extract Z3 unsat cores (for "z3_tptp")
blanchet
parents: 48376
diff changeset
   540
   proof_delims = [("\ncore(", ").")],
45203
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   541
   known_failures = known_szs_status_failures,
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   542
   prem_role = Hypothesis,
42723
c1909691bbf0 allow each slice to have its own type system
blanchet
parents: 42710
diff changeset
   543
   best_slices =
44423
f74707e12d30 exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents: 44422
diff changeset
   544
     (* FUDGE *)
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   545
     K [(0.5, ((250, z3_tff0, "mono_native", combsN, false), "")),
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   546
        (0.25, ((125, z3_tff0, "mono_native", combsN, false), "")),
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   547
        (0.125, ((62, z3_tff0, "mono_native", combsN, false), "")),
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   548
        (0.125, ((31, z3_tff0, "mono_native", combsN, false), ""))],
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   549
   best_max_mono_iters = default_max_mono_iters,
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   550
   best_max_new_mono_instances = default_max_new_mono_instances}
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   551
47646
9460f3f22365 tried to make SML/NJ happy
blanchet
parents: 47606
diff changeset
   552
val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   553
44590
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
   554
48131
1016664b8feb started adding polymophic SPASS output
blanchet
parents: 48130
diff changeset
   555
(* Not really a prover: Experimental Polymorphic THF and DFG output *)
44590
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
   556
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44596
diff changeset
   557
fun dummy_config format type_enc : atp_config =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48232
diff changeset
   558
  {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
44590
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
   559
   arguments = K (K (K (K (K "")))),
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
   560
   proof_delims = [],
45203
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   561
   known_failures = known_szs_status_failures,
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   562
   prem_role = Hypothesis,
45521
0cd6e59bd0b5 give each time slice its own lambda translation
blanchet
parents: 45365
diff changeset
   563
   best_slices =
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   564
     K [(1.0, ((200, format, type_enc,
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   565
                if is_format_higher_order format then keep_lamsN
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   566
                else combsN, false), ""))],
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   567
   best_max_mono_iters = default_max_mono_iters,
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   568
   best_max_new_mono_instances = default_max_new_mono_instances}
44590
3a8a31be92d2 added dummy PFF prover, for debugging purposes
blanchet
parents: 44589
diff changeset
   569
48004
989a34fa72b3 don't generate definitions for LEO-II -- this cuases more harm than good
blanchet
parents: 47985
diff changeset
   570
val dummy_thf_format =
48130
blanchet
parents: 48129
diff changeset
   571
  THF (Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
46435
e9c90516bc0d renamed type encoding
blanchet
parents: 46429
diff changeset
   572
val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher"
47646
9460f3f22365 tried to make SML/NJ happy
blanchet
parents: 47606
diff changeset
   573
val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44596
diff changeset
   574
48131
1016664b8feb started adding polymophic SPASS output
blanchet
parents: 48130
diff changeset
   575
val spass_poly_format = DFG Polymorphic
1016664b8feb started adding polymophic SPASS output
blanchet
parents: 48130
diff changeset
   576
val spass_poly_config = dummy_config spass_poly_format "tc_native"
1016664b8feb started adding polymophic SPASS output
blanchet
parents: 48130
diff changeset
   577
val spass_poly = (spass_polyN, fn () => spass_poly_config)
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   578
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   579
(* Remote ATP invocation via SystemOnTPTP *)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   580
38061
685d1f0f75b3 handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on
blanchet
parents: 38049
diff changeset
   581
val systems = Synchronized.var "atp_systems" ([] : string list)
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   582
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   583
fun get_systems () =
44589
0a1dfc6365e9 first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents: 44586
diff changeset
   584
  case Isabelle_System.bash_output
0a1dfc6365e9 first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents: 44586
diff changeset
   585
           "\"$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
   586
    (output, 0) => split_lines output
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   587
  | (output, _) =>
2416666e6f94 refactoring: move ATP proof and error extraction code to "ATP_Proof" module
blanchet
parents: 39375
diff changeset
   588
    error (case extract_known_failure known_perl_failures output of
41744
a18e7bbca258 make minimizer verbose
blanchet
parents: 41742
diff changeset
   589
             SOME failure => string_for_failure failure
47499
4b0daca2bf88 redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents: 47149
diff changeset
   590
           | NONE => trim_line output ^ ".")
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   591
42537
25ceb855a18b improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work
blanchet
parents: 42535
diff changeset
   592
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
   593
    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
   594
  | 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
   595
    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
   596
      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
   597
    | 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
   598
38a926e033ad make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version
blanchet
parents: 38685
diff changeset
   599
fun get_system name versions =
38589
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38588
diff changeset
   600
  Synchronized.change_result systems
b03f8fe043ec added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents: 38588
diff changeset
   601
      (fn systems => (if null systems then get_systems () else systems)
42955
576bd30cc4ea clearer SystemOnTPTP errors
blanchet
parents: 42954
diff changeset
   602
                     |> `(`(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
   603
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
   604
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
   605
  case get_system name versions of
42955
576bd30cc4ea clearer SystemOnTPTP errors
blanchet
parents: 42954
diff changeset
   606
    (SOME sys, _) => sys
46480
24990fae5f92 better error message
blanchet
parents: 46455
diff changeset
   607
  | (NONE, []) => error ("SystemOnTPTP is not available.")
42955
576bd30cc4ea clearer SystemOnTPTP errors
blanchet
parents: 42954
diff changeset
   608
  | (NONE, syss) =>
46480
24990fae5f92 better error message
blanchet
parents: 46455
diff changeset
   609
    case syss |> filter_out (String.isPrefix "%")
24990fae5f92 better error message
blanchet
parents: 46455
diff changeset
   610
              |> filter_out (curry (op =) "") of
24990fae5f92 better error message
blanchet
parents: 46455
diff changeset
   611
      [] => error ("SystemOnTPTP is not available.")
24990fae5f92 better error message
blanchet
parents: 46455
diff changeset
   612
    | [msg] => error ("SystemOnTPTP is not available: " ^ msg ^ ".")
24990fae5f92 better error message
blanchet
parents: 46455
diff changeset
   613
    | syss =>
24990fae5f92 better error message
blanchet
parents: 46455
diff changeset
   614
      error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
24990fae5f92 better error message
blanchet
parents: 46455
diff changeset
   615
             "(Available systems: " ^ commas_quote syss ^ ".)")
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   616
41148
f5229ab54284 added timeout max for remote server invocation
blanchet
parents: 40669
diff changeset
   617
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
   618
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
   619
fun remote_config system_name system_versions proof_delims known_failures
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   620
                  prem_role best_slice : atp_config =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48232
diff changeset
   621
  {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]),
47074
101976132929 improve "remote_satallax" by exploiting unsat core
blanchet
parents: 47073
diff changeset
   622
   arguments = fn _ => fn _ => fn command => fn timeout => fn _ =>
48651
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   623
       (if command <> "" then "-c " ^ quote command ^ " " else "") ^
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   624
       "-s " ^ the_system system_name system_versions ^ " " ^
fb461f81e76e added E-MaLeS to list of provers for testing
blanchet
parents: 48558
diff changeset
   625
       "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)),
42962
3b50fdeb6cfc started adding support for THF output (but no lambdas)
blanchet
parents: 42955
diff changeset
   626
   proof_delims = union (op =) tstp_proof_delims proof_delims,
45203
e3c13fa443ef more uniform SZS status handling
blanchet
parents: 45162
diff changeset
   627
   known_failures = known_failures @ known_perl_failures @ known_says_failures,
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   628
   prem_role = prem_role,
48716
1d2a12bb0640 stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
blanchet
parents: 48715
diff changeset
   629
   best_slices = fn ctxt => [(1.0, best_slice ctxt)],
47962
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   630
   best_max_mono_iters = default_max_mono_iters,
137883567114 lower the monomorphization thresholds for less scalable provers
blanchet
parents: 47955
diff changeset
   631
   best_max_new_mono_instances = default_max_new_mono_instances}
42443
724e612ba248 implemented general slicing for ATPs, especially E 1.2w and above
blanchet
parents: 42332
diff changeset
   632
43500
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   633
fun remotify_config system_name system_versions best_slice
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   634
        ({proof_delims, known_failures, prem_role, ...} : atp_config)
47912
12de57c5eee5 get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
blanchet
parents: 47900
diff changeset
   635
        : 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
   636
  remote_config system_name system_versions proof_delims known_failures
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   637
                prem_role best_slice
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   638
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   639
fun remote_atp name system_name system_versions proof_delims known_failures
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   640
               prem_role best_slice =
40060
5ef6747aa619 first step in adding support for an SMT backend to Sledgehammer
blanchet
parents: 40059
diff changeset
   641
  (remote_prefix ^ name,
47912
12de57c5eee5 get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
blanchet
parents: 47900
diff changeset
   642
   fn () => remote_config system_name system_versions proof_delims
47976
6b13451135a9 tuned names
blanchet
parents: 47974
diff changeset
   643
                          known_failures prem_role best_slice)
43500
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   644
fun remotify_atp (name, config) system_name system_versions best_slice =
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   645
  (remote_prefix ^ name,
47606
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47506
diff changeset
   646
   remotify_config system_name system_versions best_slice o config)
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   647
48130
blanchet
parents: 48129
diff changeset
   648
val explicit_tff0 = TFF (Monomorphic, TPTP_Explicit)
44589
0a1dfc6365e9 first step towards polymorphic TFF + changed defaults for Vampire
blanchet
parents: 44586
diff changeset
   649
43500
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   650
val remote_e =
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   651
  remotify_atp e "EP" ["1.0", "1.1", "1.2"]
47074
101976132929 improve "remote_satallax" by exploiting unsat core
blanchet
parents: 47073
diff changeset
   652
      (K ((750, FOF, "mono_tags??", combsN, false), "") (* FUDGE *))
48700
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   653
val remote_iprover =
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   654
  remotify_atp iprover "iProver" []
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   655
      (K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   656
val remote_iprover_eq =
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   657
  remotify_atp iprover_eq "iProver-Eq" []
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   658
      (K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   659
val remote_leo2 =
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   660
  remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
47074
101976132929 improve "remote_satallax" by exploiting unsat core
blanchet
parents: 47073
diff changeset
   661
      (K ((100, leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *))
44099
5e14f591515e support local HOATPs
blanchet
parents: 44096
diff changeset
   662
val remote_satallax =
47074
101976132929 improve "remote_satallax" by exploiting unsat core
blanchet
parents: 47073
diff changeset
   663
  remotify_atp satallax "Satallax" ["2.3", "2.2", "2"]
47076
f4838ce57772 removed Satallax option, now that this is the default
blanchet
parents: 47074
diff changeset
   664
      (K ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
43500
4c357b7aa710 provide appropriate type system and number of fact defaults for remote ATPs
blanchet
parents: 43497
diff changeset
   665
val remote_vampire =
48077
25efe19cd4e9 tweaked remote Vampire version
blanchet
parents: 48007
diff changeset
   666
  remotify_atp vampire "Vampire" ["2.6", "2.5", "1.8"]
47074
101976132929 improve "remote_satallax" by exploiting unsat core
blanchet
parents: 47073
diff changeset
   667
      (K ((250, vampire_tff0, "mono_native", combs_or_liftingN, false), "") (* FUDGE *))
44423
f74707e12d30 exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
blanchet
parents: 44422
diff changeset
   668
val remote_z3_tptp =
44754
265174356212 added dummy polymorphic THF system
blanchet
parents: 44596
diff changeset
   669
  remotify_atp z3_tptp "Z3" ["3.0"]
47074
101976132929 improve "remote_satallax" by exploiting unsat core
blanchet
parents: 47073
diff changeset
   670
      (K ((250, z3_tff0, "mono_native", combsN, false), "") (* FUDGE *))
44092
bf489e54d7f8 renamed E wrappers for consistency with CASC conventions
blanchet
parents: 43989
diff changeset
   671
val remote_e_sine =
47912
12de57c5eee5 get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
blanchet
parents: 47900
diff changeset
   672
  remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
47074
101976132929 improve "remote_satallax" by exploiting unsat core
blanchet
parents: 47073
diff changeset
   673
      (K ((500, FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
41740
4b09f8b9e012 added "Z3 as an ATP" support to Sledgehammer locally
blanchet
parents: 41738
diff changeset
   674
val remote_snark =
42939
0134d6650092 added support for remote Waldmeister
blanchet
parents: 42938
diff changeset
   675
  remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
47912
12de57c5eee5 get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
blanchet
parents: 47900
diff changeset
   676
      [("refutation.", "end_refutation.")] [] Hypothesis
47074
101976132929 improve "remote_satallax" by exploiting unsat core
blanchet
parents: 47073
diff changeset
   677
      (K ((100, explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
44092
bf489e54d7f8 renamed E wrappers for consistency with CASC conventions
blanchet
parents: 43989
diff changeset
   678
val remote_e_tofof =
47912
12de57c5eee5 get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
blanchet
parents: 47900
diff changeset
   679
  remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis
47074
101976132929 improve "remote_satallax" by exploiting unsat core
blanchet
parents: 47073
diff changeset
   680
      (K ((150, explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
42938
c124032ac96f added Waldmeister
blanchet
parents: 42937
diff changeset
   681
val remote_waldmeister =
c124032ac96f added Waldmeister
blanchet
parents: 42937
diff changeset
   682
  remote_atp waldmeisterN "Waldmeister" ["710"]
45521
0cd6e59bd0b5 give each time slice its own lambda translation
blanchet
parents: 45365
diff changeset
   683
      [("#START OF PROOF", "Proved Goals:")]
0cd6e59bd0b5 give each time slice its own lambda translation
blanchet
parents: 45365
diff changeset
   684
      [(OutOfResources, "Too many function symbols"),
47506
da72e05849ef more helpful error message
blanchet
parents: 47505
diff changeset
   685
       (Inappropriate, "****  Unexpected end of file."),
45521
0cd6e59bd0b5 give each time slice its own lambda translation
blanchet
parents: 45365
diff changeset
   686
       (Crashed, "Unrecoverable Segmentation Fault")]
47912
12de57c5eee5 get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
blanchet
parents: 47900
diff changeset
   687
      Hypothesis
47898
6213900d6d5f use raw monomorphic encoding with Waldmeister, to avoid overloading it with too many function symbols (as would be the case using mangled monomorphic encodings)
blanchet
parents: 47787
diff changeset
   688
      (K ((50, CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *))
38454
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   689
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   690
(* Setup *)
9043eefe8d71 detect old Vampire and give a nicer error message
blanchet
parents: 38433
diff changeset
   691
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   692
fun add_atp (name, config) thy =
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   693
  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
   694
  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
   695
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   696
fun get_atp thy name =
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   697
  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
   698
  handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   699
41727
ab3f6d76fb23 available_provers ~> supported_provers (for clarity)
blanchet
parents: 41725
diff changeset
   700
val supported_atps = Symtab.keys o Data.get
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36370
diff changeset
   701
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   702
fun is_atp_installed thy name =
48376
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48232
diff changeset
   703
  let val {exec, ...} = get_atp thy name () in
416e4123baf3 use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
blanchet
parents: 48232
diff changeset
   704
    exists (fn var => getenv var <> "") (fst exec)
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   705
  end
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36370
diff changeset
   706
40059
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   707
fun refresh_systems_on_tptp () =
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   708
  Synchronized.change systems (fn _ => get_systems ())
6ad9081665db use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents: 39491
diff changeset
   709
47055
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   710
fun effective_term_order ctxt atp =
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   711
  let val ord = Config.get ctxt term_order in
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   712
    if ord = smartN then
48005
eeede26f2721 killed SPASS 3.5/3.7 FLOTTER hack -- requires users to upgrade to SPASS 3.8
blanchet
parents: 48004
diff changeset
   713
      if atp = spassN then
47073
c73f7b0c7ebc generate weights and precedences for predicates as well
blanchet
parents: 47055
diff changeset
   714
        {is_lpo = false, gen_weights = true, gen_prec = true, gen_simp = false}
47055
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   715
      else
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   716
        {is_lpo = false, gen_weights = false, gen_prec = false,
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   717
         gen_simp = false}
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   718
    else
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   719
      let val is_lpo = String.isSubstring lpoN ord in
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   720
        {is_lpo = is_lpo,
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   721
         gen_weights = not is_lpo andalso String.isSubstring xweightsN ord,
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   722
         gen_prec = String.isSubstring xprecN ord,
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   723
         gen_simp = String.isSubstring xsimpN ord}
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   724
      end
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   725
  end
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   726
47606
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47506
diff changeset
   727
val atps=
48700
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   728
  [alt_ergo, e, e_males, iprover, iprover_eq, leo2, satallax, spass, spass_poly,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   729
   vampire, z3_tptp, dummy_thf, remote_e, remote_e_sine, remote_e_tofof,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   730
   remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax,
d06138bfeb45 added iProver(-Eq) local
blanchet
parents: 48653
diff changeset
   731
   remote_vampire, remote_z3_tptp, remote_snark, remote_waldmeister]
47055
16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents: 47053
diff changeset
   732
47606
06dde48a1503 true delayed evaluation of "SPASS_VERSION" environment variable
blanchet
parents: 47506
diff changeset
   733
val setup = fold add_atp atps
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
   734
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   735
end;