src/HOL/Tools/ATP_Manager/atp_systems.ML
author blanchet
Tue, 27 Jul 2010 18:33:10 +0200
changeset 38023 962b0a7f544b
parent 38022 d9c4d87838f3
child 38032 54448f5d151f
permissions -rw-r--r--
more refactoring
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36376
e83d52a52449 renamed module "ATP_Wrapper" to "ATP_Systems"
blanchet
parents: 36371
diff changeset
     1
(*  Title:      HOL/Tools/ATP_Manager/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
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    10
  datatype failure =
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    11
    Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    12
    OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    13
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    14
  type prover_config =
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    15
    {home_var: string,
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    16
     executable: string,
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    17
     arguments: bool -> Time.time -> string,
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    18
     proof_delims: (string * string) list,
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    19
     known_failures: (failure * string) list,
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    20
     max_new_relevant_facts_per_iter: int,
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    21
     prefers_theory_relevant: bool,
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    22
     explicit_forall: bool}
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    23
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    24
  val add_prover: string * prover_config -> theory -> theory
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    25
  val get_prover: theory -> string -> prover_config
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    26
  val available_atps: theory -> unit
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
    27
  val refresh_systems_on_tptp : unit -> unit
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36370
diff changeset
    28
  val default_atps_param_value : unit -> string
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
    29
  val setup : theory -> theory
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    30
end;
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    31
36376
e83d52a52449 renamed module "ATP_Wrapper" to "ATP_Systems"
blanchet
parents: 36371
diff changeset
    32
structure ATP_Systems : ATP_SYSTEMS =
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
    33
struct
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    34
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    35
(* prover configuration *)
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
    36
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    37
datatype failure =
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    38
  Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    39
  OldSpass | MalformedInput | MalformedOutput | UnknownError
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
    40
32941
72d48e333b77 eliminated extraneous wrapping of public records;
wenzelm
parents: 32936
diff changeset
    41
type prover_config =
36917
8674cdb0b8cc query _HOME environment variables at run-time, not at build-time
blanchet
parents: 36910
diff changeset
    42
  {home_var: string,
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    43
   executable: string,
37514
b147d01b8ebc if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again
blanchet
parents: 37509
diff changeset
    44
   arguments: bool -> Time.time -> string,
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    45
   proof_delims: (string * string) list,
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    46
   known_failures: (failure * string) list,
38009
34e1ac9cb71d shrink the "max_new_relevant_facts_per_iter" fudge factors, now that we count formulas and not clauses
blanchet
parents: 38005
diff changeset
    47
   max_new_relevant_facts_per_iter: int,
37994
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37989
diff changeset
    48
   prefers_theory_relevant: bool,
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37989
diff changeset
    49
   explicit_forall: bool}
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    50
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    51
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    52
(* named provers *)
38001
a9b47b85ca24 reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
blanchet
parents: 38000
diff changeset
    53
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    54
structure Data = Theory_Data
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    55
(
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    56
  type T = (prover_config * stamp) Symtab.table
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    57
  val empty = Symtab.empty
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    58
  val extend = I
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    59
  fun merge data : T = Symtab.merge (eq_snd op =) data
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    60
    handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    61
)
38017
3ad3e3ca2451 move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
blanchet
parents: 38015
diff changeset
    62
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    63
fun add_prover (name, config) thy =
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    64
  Data.map (Symtab.update_new (name, (config, stamp ()))) thy
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    65
  handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
38017
3ad3e3ca2451 move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
blanchet
parents: 38015
diff changeset
    66
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    67
fun get_prover thy name =
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    68
  the (Symtab.lookup (Data.get thy) name) |> fst
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    69
  handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
37962
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents: 37926
diff changeset
    70
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    71
fun available_atps thy =
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    72
  priority ("Available ATPs: " ^
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    73
            commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
    74
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    75
fun available_atps thy =
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    76
  priority ("Available ATPs: " ^
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
    77
            commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    78
36382
b90fc0d75bca cosmetics
blanchet
parents: 36377
diff changeset
    79
fun to_generous_secs time = (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
    80
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    81
(* E prover *)
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
    82
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
    83
val tstp_proof_delims =
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
    84
  ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
    85
35969
c9565298df9e added support for Sledgehammer parameters;
blanchet
parents: 35869
diff changeset
    86
val e_config : prover_config =
36917
8674cdb0b8cc query _HOME environment variables at run-time, not at build-time
blanchet
parents: 36910
diff changeset
    87
  {home_var = "E_HOME",
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
    88
   executable = "eproof",
37514
b147d01b8ebc if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again
blanchet
parents: 37509
diff changeset
    89
   arguments = fn _ => fn timeout =>
36382
b90fc0d75bca cosmetics
blanchet
parents: 36377
diff changeset
    90
     "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
b90fc0d75bca cosmetics
blanchet
parents: 36377
diff changeset
    91
     string_of_int (to_generous_secs timeout),
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
    92
   proof_delims = [tstp_proof_delims],
36265
41c9e755e552 distinguish between the different ATP errors in the user interface;
blanchet
parents: 36264
diff changeset
    93
   known_failures =
37995
06f02b15ef8a generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents: 37994
diff changeset
    94
     [(Unprovable, "SZS status: CounterSatisfiable"),
06f02b15ef8a generate full first-order formulas (FOF) in Sledgehammer
blanchet
parents: 37994
diff changeset
    95
      (Unprovable, "SZS status CounterSatisfiable"),
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    96
      (TimedOut, "Failure: Resource limit exceeded (time)"),
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    97
      (TimedOut, "time limit exceeded"),
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    98
      (OutOfResources,
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
    99
       "# Cannot determine problem status within resource limit"),
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   100
      (OutOfResources, "SZS status: ResourceOut"),
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   101
      (OutOfResources, "SZS status ResourceOut")],
38009
34e1ac9cb71d shrink the "max_new_relevant_facts_per_iter" fudge factors, now that we count formulas and not clauses
blanchet
parents: 38005
diff changeset
   102
   max_new_relevant_facts_per_iter = 80 (* FIXME *),
37994
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37989
diff changeset
   103
   prefers_theory_relevant = false,
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37989
diff changeset
   104
   explicit_forall = false}
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   105
val e = ("e", e_config)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   106
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   107
36219
16670b4f0baa set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
blanchet
parents: 36190
diff changeset
   108
(* The "-VarWeight=3" option helps the higher-order problems, probably by
16670b4f0baa set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
blanchet
parents: 36190
diff changeset
   109
   counteracting the presence of "hAPP". *)
37498
b426cbdb5a23 removed Sledgehammer's support for the DFG syntax;
blanchet
parents: 37480
diff changeset
   110
val spass_config : prover_config =
37962
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents: 37926
diff changeset
   111
  {home_var = "ISABELLE_ATP_MANAGER",
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents: 37926
diff changeset
   112
   executable = "SPASS_TPTP",
37550
fc2f979b9a08 split SPASS time slot between SOS and non-SOS, in case SOS times out
blanchet
parents: 37514
diff changeset
   113
   (* "div 2" accounts for the fact that SPASS is often run twice. *)
37514
b147d01b8ebc if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again
blanchet
parents: 37509
diff changeset
   114
   arguments = fn complete => fn timeout =>
37962
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents: 37926
diff changeset
   115
     ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
37550
fc2f979b9a08 split SPASS time slot between SOS and non-SOS, in case SOS times out
blanchet
parents: 37514
diff changeset
   116
      \-VarWeight=3 -TimeLimit=" ^
fc2f979b9a08 split SPASS time slot between SOS and non-SOS, in case SOS times out
blanchet
parents: 37514
diff changeset
   117
      string_of_int (to_generous_secs timeout div 2))
37514
b147d01b8ebc if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again
blanchet
parents: 37509
diff changeset
   118
     |> not complete ? prefix "-SOS=1 ",
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   119
   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
   120
   known_failures =
37413
e856582fe9c4 improve ATP-specific error messages
blanchet
parents: 37347
diff changeset
   121
     [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   122
      (TimedOut, "SPASS beiseite: Ran out of time"),
36965
67ae217c6b5c identify common SPASS error more clearly
blanchet
parents: 36924
diff changeset
   123
      (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
37413
e856582fe9c4 improve ATP-specific error messages
blanchet
parents: 37347
diff changeset
   124
      (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
   125
      (MalformedInput, "Free Variable"),
37962
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents: 37926
diff changeset
   126
      (OldSpass, "tptp2dfg")],
38009
34e1ac9cb71d shrink the "max_new_relevant_facts_per_iter" fudge factors, now that we count formulas and not clauses
blanchet
parents: 38005
diff changeset
   127
   max_new_relevant_facts_per_iter = 26 (* FIXME *),
37994
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37989
diff changeset
   128
   prefers_theory_relevant = true,
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37989
diff changeset
   129
   explicit_forall = true}
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   130
val spass = ("spass", spass_config)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   131
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   132
(* Vampire *)
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   133
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   134
val vampire_config : prover_config =
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   135
  {home_var = "VAMPIRE_HOME",
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   136
   executable = "vampire",
37514
b147d01b8ebc if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again
blanchet
parents: 37509
diff changeset
   137
   arguments = fn _ => fn timeout =>
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   138
     "--output_syntax tptp --mode casc -t " ^
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   139
     string_of_int (to_generous_secs timeout),
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   140
   proof_delims =
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   141
     [("=========== Refutation ==========",
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   142
       "======= End of refutation ======="),
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   143
      ("% SZS output start Refutation", "% SZS output end Refutation")],
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   144
   known_failures =
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   145
     [(Unprovable, "UNPROVABLE"),
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   146
      (IncompleteUnprovable, "CANNOT PROVE"),
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   147
      (Unprovable, "Satisfiability detected"),
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   148
      (OutOfResources, "Refutation not found")],
38009
34e1ac9cb71d shrink the "max_new_relevant_facts_per_iter" fudge factors, now that we count formulas and not clauses
blanchet
parents: 38005
diff changeset
   149
   max_new_relevant_facts_per_iter = 40 (* FIXME *),
37994
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37989
diff changeset
   150
   prefers_theory_relevant = false,
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37989
diff changeset
   151
   explicit_forall = false}
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   152
val vampire = ("vampire", vampire_config)
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   153
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   154
(* Remote prover invocation via SystemOnTPTP *)
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   155
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   156
val systems = Synchronized.var "atp_systems" ([]: string list)
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   157
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   158
fun get_systems () =
36370
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   159
  case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   160
    (answer, 0) => split_lines answer
a4f601daa175 centralized ATP-specific error handling in "atp_wrapper.ML"
blanchet
parents: 36369
diff changeset
   161
  | (answer, _) =>
37627
1d1754ccd233 more precise error message for remote ATPs
blanchet
parents: 37625
diff changeset
   162
    error ("Failed to get available systems at SystemOnTPTP:\n" ^
1d1754ccd233 more precise error message for remote ATPs
blanchet
parents: 37625
diff changeset
   163
           perhaps (try (unsuffix "\n")) answer)
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   164
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
   165
fun refresh_systems_on_tptp () =
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   166
  Synchronized.change systems (fn _ => get_systems ())
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   167
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   168
fun get_system prefix = Synchronized.change_result systems (fn systems =>
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
   169
  (if null systems then get_systems () else systems)
32942
b6711ec9de26 misc tuning and recovery of Isabelle coding style;
wenzelm
parents: 32941
diff changeset
   170
  |> `(find_first (String.isPrefix prefix)));
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
   171
32948
e95a4be101a8 natural argument order for prover;
wenzelm
parents: 32944
diff changeset
   172
fun the_system prefix =
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
   173
  (case get_system prefix of
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   174
    NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.")
32942
b6711ec9de26 misc tuning and recovery of Isabelle coding style;
wenzelm
parents: 32941
diff changeset
   175
  | SOME sys => sys);
31835
b686d4df54c2 check for current versions on server
immler@in.tum.de
parents: 31832
diff changeset
   176
36265
41c9e755e552 distinguish between the different ATP errors in the user interface;
blanchet
parents: 36264
diff changeset
   177
val remote_known_failures =
37627
1d1754ccd233 more precise error message for remote ATPs
blanchet
parents: 37625
diff changeset
   178
  [(CantConnect, "HTTP-Error"),
1d1754ccd233 more precise error message for remote ATPs
blanchet
parents: 37625
diff changeset
   179
   (TimedOut, "says Timeout"),
36377
b3dce4c715d0 now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script
blanchet
parents: 36376
diff changeset
   180
   (MalformedOutput, "Remote script could not extract proof")]
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   181
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   182
fun remote_config atp_prefix args
38009
34e1ac9cb71d shrink the "max_new_relevant_facts_per_iter" fudge factors, now that we count formulas and not clauses
blanchet
parents: 38005
diff changeset
   183
        ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
37994
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37989
diff changeset
   184
          prefers_theory_relevant, explicit_forall, ...} : prover_config)
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37989
diff changeset
   185
        : prover_config =
36917
8674cdb0b8cc query _HOME environment variables at run-time, not at build-time
blanchet
parents: 36910
diff changeset
   186
  {home_var = "ISABELLE_ATP_MANAGER",
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
   187
   executable = "SystemOnTPTP",
37514
b147d01b8ebc if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again
blanchet
parents: 37509
diff changeset
   188
   arguments = fn _ => fn timeout =>
36382
b90fc0d75bca cosmetics
blanchet
parents: 36377
diff changeset
   189
     args ^ " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
b90fc0d75bca cosmetics
blanchet
parents: 36377
diff changeset
   190
     the_system atp_prefix,
36369
d2cd0d04b8e6 handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents: 36289
diff changeset
   191
   proof_delims = insert (op =) tstp_proof_delims proof_delims,
36265
41c9e755e552 distinguish between the different ATP errors in the user interface;
blanchet
parents: 36264
diff changeset
   192
   known_failures = remote_known_failures @ known_failures,
38009
34e1ac9cb71d shrink the "max_new_relevant_facts_per_iter" fudge factors, now that we count formulas and not clauses
blanchet
parents: 38005
diff changeset
   193
   max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
37994
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37989
diff changeset
   194
   prefers_theory_relevant = prefers_theory_relevant,
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37989
diff changeset
   195
   explicit_forall = explicit_forall}
28596
fcd463a6b6de tuned interfaces -- plain prover function, without thread;
wenzelm
parents: 28592
diff changeset
   196
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   197
val remote_name = prefix "remote_"
32864
a226f29d4bdc re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents: 32740
diff changeset
   198
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   199
fun remote_prover prover atp_prefix args config =
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   200
  (remote_name (fst prover), remote_config atp_prefix args config)
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   201
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   202
val remote_e = remote_prover e "EP---" "" e_config
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   203
val remote_spass = remote_prover spass "SPASS---" "-x" spass_config
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   204
val remote_vampire = remote_prover vampire "Vampire---9" "" vampire_config
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   205
36917
8674cdb0b8cc query _HOME environment variables at run-time, not at build-time
blanchet
parents: 36910
diff changeset
   206
fun maybe_remote (name, _) ({home_var, ...} : prover_config) =
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   207
  name |> getenv home_var = "" ? remote_name
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36370
diff changeset
   208
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36370
diff changeset
   209
fun default_atps_param_value () =
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36370
diff changeset
   210
  space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   211
                     remote_name (fst vampire)]
36371
8c83ea1a7740 move the Sledgehammer menu options to "sledgehammer_isar.ML"
blanchet
parents: 36370
diff changeset
   212
37509
f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes
blanchet
parents: 37506
diff changeset
   213
val provers = [e, spass, vampire, remote_e, remote_spass, remote_vampire]
38023
962b0a7f544b more refactoring
blanchet
parents: 38022
diff changeset
   214
val setup = fold add_prover provers
35867
16279c4c7a33 move all ATP setup code into ATP_Wrapper
blanchet
parents: 35865
diff changeset
   215
28592
824f8390aaa2 renamed AtpThread to AtpWrapper;
wenzelm
parents:
diff changeset
   216
end;