src/HOL/Tools/ATP/atp_systems.ML
author haftmann
Wed Dec 08 13:34:50 2010 +0100 (2010-12-08)
changeset 41075 4bed56dc95fb
parent 40669 5c316d1327d4
child 41148 f5229ab54284
permissions -rw-r--r--
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
     1 (*  Title:      HOL/Tools/ATP/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   type failure = ATP_Proof.failure
    11 
    12   type atp_config =
    13     {exec: string * string,
    14      required_execs: (string * string) list,
    15      arguments: bool -> Time.time -> string,
    16      has_incomplete_mode: bool,
    17      proof_delims: (string * string) list,
    18      known_failures: (failure * string) list,
    19      default_max_relevant: int,
    20      explicit_forall: bool,
    21      use_conjecture_for_hypotheses: bool}
    22 
    23   val eN : string
    24   val spassN : string
    25   val vampireN : string
    26   val sine_eN : string
    27   val snarkN : string
    28   val remote_prefix : string
    29   val add_atp : string * atp_config -> theory -> theory
    30   val get_atp : theory -> string -> atp_config
    31   val available_atps : theory -> string list
    32   val is_atp_installed : theory -> string -> bool
    33   val refresh_systems_on_tptp : unit -> unit
    34   val setup : theory -> theory
    35 end;
    36 
    37 structure ATP_Systems : ATP_SYSTEMS =
    38 struct
    39 
    40 open ATP_Proof
    41 
    42 (* ATP configuration *)
    43 
    44 type atp_config =
    45   {exec: string * string,
    46    required_execs: (string * string) list,
    47    arguments: bool -> Time.time -> string,
    48    has_incomplete_mode: bool,
    49    proof_delims: (string * string) list,
    50    known_failures: (failure * string) list,
    51    default_max_relevant: int,
    52    explicit_forall: bool,
    53    use_conjecture_for_hypotheses: bool}
    54 
    55 val known_perl_failures =
    56   [(CantConnect, "HTTP error"),
    57    (NoPerl, "env: perl"),
    58    (NoLibwwwPerl, "Can't locate HTTP")]
    59 
    60 (* named ATPs *)
    61 
    62 val eN = "e"
    63 val spassN = "spass"
    64 val vampireN = "vampire"
    65 val sine_eN = "sine_e"
    66 val snarkN = "snark"
    67 val remote_prefix = "remote_"
    68 
    69 structure Data = Theory_Data
    70 (
    71   type T = (atp_config * stamp) Symtab.table
    72   val empty = Symtab.empty
    73   val extend = I
    74   fun merge data : T = Symtab.merge (eq_snd op =) data
    75     handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
    76 )
    77 
    78 fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
    79 
    80 
    81 (* E *)
    82 
    83 (* Give E an extra second to reconstruct the proof. Older versions even get two
    84    seconds, because the "eproof" script wrongly subtracted an entire second to
    85    account for the overhead of the script itself, which is in fact much
    86    lower. *)
    87 fun e_bonus () =
    88   case getenv "E_VERSION" of
    89     "" => 2000
    90   | version =>
    91     if exists (fn s => String.isPrefix s version) ["0.9", "1.0"] then 2000
    92     else 1000
    93 
    94 val tstp_proof_delims =
    95   ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
    96 
    97 val e_config : atp_config =
    98   {exec = ("E_HOME", "eproof"),
    99    required_execs = [],
   100    arguments = fn _ => fn timeout =>
   101      "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent \
   102      \--cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout),
   103    has_incomplete_mode = false,
   104    proof_delims = [tstp_proof_delims],
   105    known_failures =
   106      [(Unprovable, "SZS status: CounterSatisfiable"),
   107       (Unprovable, "SZS status CounterSatisfiable"),
   108       (TimedOut, "Failure: Resource limit exceeded (time)"),
   109       (TimedOut, "time limit exceeded"),
   110       (OutOfResources,
   111        "# Cannot determine problem status within resource limit"),
   112       (OutOfResources, "SZS status: ResourceOut"),
   113       (OutOfResources, "SZS status ResourceOut")],
   114    default_max_relevant = 500 (* FUDGE *),
   115    explicit_forall = false,
   116    use_conjecture_for_hypotheses = true}
   117 
   118 val e = (eN, e_config)
   119 
   120 
   121 (* SPASS *)
   122 
   123 (* The "-VarWeight=3" option helps the higher-order problems, probably by
   124    counteracting the presence of "hAPP". *)
   125 val spass_config : atp_config =
   126   {exec = ("ISABELLE_ATP", "scripts/spass"),
   127    required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
   128    arguments = fn complete => fn timeout =>
   129      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
   130       \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
   131      |> not complete ? prefix "-SOS=1 ",
   132    has_incomplete_mode = true,
   133    proof_delims = [("Here is a proof", "Formulae used in the proof")],
   134    known_failures =
   135      known_perl_failures @
   136      [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
   137       (TimedOut, "SPASS beiseite: Ran out of time"),
   138       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
   139       (MalformedInput, "Undefined symbol"),
   140       (MalformedInput, "Free Variable"),
   141       (SpassTooOld, "tptp2dfg"),
   142       (InternalError, "Please report this error")],
   143    default_max_relevant = 350 (* FUDGE *),
   144    explicit_forall = true,
   145    use_conjecture_for_hypotheses = true}
   146 
   147 val spass = (spassN, spass_config)
   148 
   149 
   150 (* Vampire *)
   151 
   152 val vampire_config : atp_config =
   153   {exec = ("VAMPIRE_HOME", "vampire"),
   154    required_execs = [],
   155    arguments = fn complete => fn timeout =>
   156      ("--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
   157       " --thanks Andrei --input_file")
   158      |> not complete ? prefix "--sos on ",
   159    has_incomplete_mode = true,
   160    proof_delims =
   161      [("=========== Refutation ==========",
   162        "======= End of refutation ======="),
   163       ("% SZS output start Refutation", "% SZS output end Refutation"),
   164       ("% SZS output start Proof", "% SZS output end Proof")],
   165    known_failures =
   166      [(Unprovable, "UNPROVABLE"),
   167       (IncompleteUnprovable, "CANNOT PROVE"),
   168       (TimedOut, "SZS status Timeout"),
   169       (Unprovable, "Satisfiability detected"),
   170       (Unprovable, "Termination reason: Satisfiable"),
   171       (VampireTooOld, "not a valid option"),
   172       (Interrupted, "Aborted by signal SIGINT")],
   173    default_max_relevant = 400 (* FUDGE *),
   174    explicit_forall = false,
   175    use_conjecture_for_hypotheses = true}
   176 
   177 val vampire = (vampireN, vampire_config)
   178 
   179 
   180 (* Remote ATP invocation via SystemOnTPTP *)
   181 
   182 val systems = Synchronized.var "atp_systems" ([] : string list)
   183 
   184 fun get_systems () =
   185   case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
   186     (output, 0) => split_lines output
   187   | (output, _) =>
   188     error (case extract_known_failure known_perl_failures output of
   189              SOME failure => string_for_failure "ATP" failure
   190            | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
   191 
   192 fun find_system name [] systems = find_first (String.isPrefix name) systems
   193   | find_system name (version :: versions) systems =
   194     case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
   195       NONE => find_system name versions systems
   196     | res => res
   197 
   198 fun get_system name versions =
   199   Synchronized.change_result systems
   200       (fn systems => (if null systems then get_systems () else systems)
   201                      |> `(find_system name versions))
   202 
   203 fun the_system name versions =
   204   case get_system name versions of
   205     SOME sys => sys
   206   | NONE => error ("System " ^ quote name ^ " not available at SystemOnTPTP.")
   207 
   208 fun remote_config system_name system_versions proof_delims known_failures
   209                   default_max_relevant use_conjecture_for_hypotheses
   210                   : atp_config =
   211   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
   212    required_execs = [],
   213    arguments = fn _ => fn timeout =>
   214      " -t " ^ string_of_int (to_secs 0 timeout) ^ " -s " ^
   215      the_system system_name system_versions,
   216    has_incomplete_mode = false,
   217    proof_delims = insert (op =) tstp_proof_delims proof_delims,
   218    known_failures =
   219      known_failures @ known_perl_failures @
   220      [(TimedOut, "says Timeout")],
   221    default_max_relevant = default_max_relevant,
   222    explicit_forall = true,
   223    use_conjecture_for_hypotheses = use_conjecture_for_hypotheses}
   224 
   225 fun remotify_config system_name system_versions
   226         ({proof_delims, known_failures, default_max_relevant,
   227           use_conjecture_for_hypotheses, ...} : atp_config) : atp_config =
   228   remote_config system_name system_versions proof_delims known_failures
   229                 default_max_relevant use_conjecture_for_hypotheses
   230 
   231 fun remote_atp name system_name system_versions proof_delims known_failures
   232                default_max_relevant use_conjecture_for_hypotheses =
   233   (remote_prefix ^ name,
   234    remote_config system_name system_versions proof_delims known_failures
   235                  default_max_relevant use_conjecture_for_hypotheses)
   236 fun remotify_atp (name, config) system_name system_versions =
   237   (remote_prefix ^ name, remotify_config system_name system_versions config)
   238 
   239 val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"]
   240 val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
   241 val remote_sine_e =
   242   remote_atp sine_eN "SInE" [] [] [(IncompleteUnprovable, "says Unknown")]
   243                 800 (* FUDGE *) true
   244 val remote_snark =
   245   remote_atp snarkN "SNARK---" [] [("refutation.", "end_refutation.")] []
   246              250 (* FUDGE *) true
   247 
   248 (* Setup *)
   249 
   250 fun add_atp (name, config) thy =
   251   Data.map (Symtab.update_new (name, (config, stamp ()))) thy
   252   handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
   253 
   254 fun get_atp thy name =
   255   the (Symtab.lookup (Data.get thy) name) |> fst
   256   handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
   257 
   258 val available_atps = Symtab.keys o Data.get
   259 
   260 fun is_atp_installed thy name =
   261   let val {exec, required_execs, ...} = get_atp thy name in
   262     forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
   263   end
   264 
   265 fun refresh_systems_on_tptp () =
   266   Synchronized.change systems (fn _ => get_systems ())
   267 
   268 val atps = [e, spass, vampire, remote_e, remote_vampire, remote_sine_e,
   269             remote_snark]
   270 val setup = fold add_atp atps
   271 
   272 end;