src/HOL/Tools/ATP_Manager/atp_systems.ML
author blanchet
Tue Jul 27 18:33:10 2010 +0200 (2010-07-27)
changeset 38023 962b0a7f544b
parent 38022 d9c4d87838f3
child 38032 54448f5d151f
permissions -rw-r--r--
more refactoring
     1 (*  Title:      HOL/Tools/ATP_Manager/atp_systems.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Setup for supported ATPs.
     6 *)
     7 
     8 signature ATP_SYSTEMS =
     9 sig
    10   datatype failure =
    11     Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
    12     OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
    13 
    14   type prover_config =
    15     {home_var: string,
    16      executable: string,
    17      arguments: bool -> Time.time -> string,
    18      proof_delims: (string * string) list,
    19      known_failures: (failure * string) list,
    20      max_new_relevant_facts_per_iter: int,
    21      prefers_theory_relevant: bool,
    22      explicit_forall: bool}
    23 
    24   val add_prover: string * prover_config -> theory -> theory
    25   val get_prover: theory -> string -> prover_config
    26   val available_atps: theory -> unit
    27   val refresh_systems_on_tptp : unit -> unit
    28   val default_atps_param_value : unit -> string
    29   val setup : theory -> theory
    30 end;
    31 
    32 structure ATP_Systems : ATP_SYSTEMS =
    33 struct
    34 
    35 (* prover configuration *)
    36 
    37 datatype failure =
    38   Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
    39   OldSpass | MalformedInput | MalformedOutput | UnknownError
    40 
    41 type prover_config =
    42   {home_var: string,
    43    executable: string,
    44    arguments: bool -> Time.time -> string,
    45    proof_delims: (string * string) list,
    46    known_failures: (failure * string) list,
    47    max_new_relevant_facts_per_iter: int,
    48    prefers_theory_relevant: bool,
    49    explicit_forall: bool}
    50 
    51 
    52 (* named provers *)
    53 
    54 structure Data = Theory_Data
    55 (
    56   type T = (prover_config * stamp) Symtab.table
    57   val empty = Symtab.empty
    58   val extend = I
    59   fun merge data : T = Symtab.merge (eq_snd op =) data
    60     handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
    61 )
    62 
    63 fun add_prover (name, config) thy =
    64   Data.map (Symtab.update_new (name, (config, stamp ()))) thy
    65   handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
    66 
    67 fun get_prover thy name =
    68   the (Symtab.lookup (Data.get thy) name) |> fst
    69   handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
    70 
    71 fun available_atps thy =
    72   priority ("Available ATPs: " ^
    73             commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
    74 
    75 fun available_atps thy =
    76   priority ("Available ATPs: " ^
    77             commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
    78 
    79 fun to_generous_secs time = (Time.toMilliseconds time + 999) div 1000
    80 
    81 (* E prover *)
    82 
    83 val tstp_proof_delims =
    84   ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
    85 
    86 val e_config : prover_config =
    87   {home_var = "E_HOME",
    88    executable = "eproof",
    89    arguments = fn _ => fn timeout =>
    90      "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
    91      string_of_int (to_generous_secs timeout),
    92    proof_delims = [tstp_proof_delims],
    93    known_failures =
    94      [(Unprovable, "SZS status: CounterSatisfiable"),
    95       (Unprovable, "SZS status CounterSatisfiable"),
    96       (TimedOut, "Failure: Resource limit exceeded (time)"),
    97       (TimedOut, "time limit exceeded"),
    98       (OutOfResources,
    99        "# Cannot determine problem status within resource limit"),
   100       (OutOfResources, "SZS status: ResourceOut"),
   101       (OutOfResources, "SZS status ResourceOut")],
   102    max_new_relevant_facts_per_iter = 80 (* FIXME *),
   103    prefers_theory_relevant = false,
   104    explicit_forall = false}
   105 val e = ("e", e_config)
   106 
   107 
   108 (* The "-VarWeight=3" option helps the higher-order problems, probably by
   109    counteracting the presence of "hAPP". *)
   110 val spass_config : prover_config =
   111   {home_var = "ISABELLE_ATP_MANAGER",
   112    executable = "SPASS_TPTP",
   113    (* "div 2" accounts for the fact that SPASS is often run twice. *)
   114    arguments = fn complete => fn timeout =>
   115      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
   116       \-VarWeight=3 -TimeLimit=" ^
   117       string_of_int (to_generous_secs timeout div 2))
   118      |> not complete ? prefix "-SOS=1 ",
   119    proof_delims = [("Here is a proof", "Formulae used in the proof")],
   120    known_failures =
   121      [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
   122       (TimedOut, "SPASS beiseite: Ran out of time"),
   123       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
   124       (MalformedInput, "Undefined symbol"),
   125       (MalformedInput, "Free Variable"),
   126       (OldSpass, "tptp2dfg")],
   127    max_new_relevant_facts_per_iter = 26 (* FIXME *),
   128    prefers_theory_relevant = true,
   129    explicit_forall = true}
   130 val spass = ("spass", spass_config)
   131 
   132 (* Vampire *)
   133 
   134 val vampire_config : prover_config =
   135   {home_var = "VAMPIRE_HOME",
   136    executable = "vampire",
   137    arguments = fn _ => fn timeout =>
   138      "--output_syntax tptp --mode casc -t " ^
   139      string_of_int (to_generous_secs timeout),
   140    proof_delims =
   141      [("=========== Refutation ==========",
   142        "======= End of refutation ======="),
   143       ("% SZS output start Refutation", "% SZS output end Refutation")],
   144    known_failures =
   145      [(Unprovable, "UNPROVABLE"),
   146       (IncompleteUnprovable, "CANNOT PROVE"),
   147       (Unprovable, "Satisfiability detected"),
   148       (OutOfResources, "Refutation not found")],
   149    max_new_relevant_facts_per_iter = 40 (* FIXME *),
   150    prefers_theory_relevant = false,
   151    explicit_forall = false}
   152 val vampire = ("vampire", vampire_config)
   153 
   154 (* Remote prover invocation via SystemOnTPTP *)
   155 
   156 val systems = Synchronized.var "atp_systems" ([]: string list)
   157 
   158 fun get_systems () =
   159   case bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" of
   160     (answer, 0) => split_lines answer
   161   | (answer, _) =>
   162     error ("Failed to get available systems at SystemOnTPTP:\n" ^
   163            perhaps (try (unsuffix "\n")) answer)
   164 
   165 fun refresh_systems_on_tptp () =
   166   Synchronized.change systems (fn _ => get_systems ())
   167 
   168 fun get_system prefix = Synchronized.change_result systems (fn systems =>
   169   (if null systems then get_systems () else systems)
   170   |> `(find_first (String.isPrefix prefix)));
   171 
   172 fun the_system prefix =
   173   (case get_system prefix of
   174     NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.")
   175   | SOME sys => sys);
   176 
   177 val remote_known_failures =
   178   [(CantConnect, "HTTP-Error"),
   179    (TimedOut, "says Timeout"),
   180    (MalformedOutput, "Remote script could not extract proof")]
   181 
   182 fun remote_config atp_prefix args
   183         ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
   184           prefers_theory_relevant, explicit_forall, ...} : prover_config)
   185         : prover_config =
   186   {home_var = "ISABELLE_ATP_MANAGER",
   187    executable = "SystemOnTPTP",
   188    arguments = fn _ => fn timeout =>
   189      args ^ " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
   190      the_system atp_prefix,
   191    proof_delims = insert (op =) tstp_proof_delims proof_delims,
   192    known_failures = remote_known_failures @ known_failures,
   193    max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
   194    prefers_theory_relevant = prefers_theory_relevant,
   195    explicit_forall = explicit_forall}
   196 
   197 val remote_name = prefix "remote_"
   198 
   199 fun remote_prover prover atp_prefix args config =
   200   (remote_name (fst prover), remote_config atp_prefix args config)
   201 
   202 val remote_e = remote_prover e "EP---" "" e_config
   203 val remote_spass = remote_prover spass "SPASS---" "-x" spass_config
   204 val remote_vampire = remote_prover vampire "Vampire---9" "" vampire_config
   205 
   206 fun maybe_remote (name, _) ({home_var, ...} : prover_config) =
   207   name |> getenv home_var = "" ? remote_name
   208 
   209 fun default_atps_param_value () =
   210   space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
   211                      remote_name (fst vampire)]
   212 
   213 val provers = [e, spass, vampire, remote_e, remote_spass, remote_vampire]
   214 val setup = fold add_prover provers
   215 
   216 end;