src/HOL/Tools/ATP/atp_systems.ML
author blanchet
Fri Jun 10 12:01:15 2011 +0200 (2011-06-10)
changeset 43354 396aaa15dd8b
parent 43288 7a4eebdebb23
child 43466 52f040bcfae7
permissions -rw-r--r--
pass --trim option to "eproof" script to speed up proof reconstruction
     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 format = ATP_Problem.format
    11   type formula_kind = ATP_Problem.formula_kind
    12   type failure = ATP_Proof.failure
    13 
    14   type atp_config =
    15     {exec : string * string,
    16      required_execs : (string * string) list,
    17      arguments :
    18        Proof.context -> bool -> int -> Time.time
    19        -> (unit -> (string * real) list) -> string,
    20      proof_delims : (string * string) list,
    21      known_failures : (failure * string) list,
    22      conj_sym_kind : formula_kind,
    23      prem_kind : formula_kind,
    24      formats : format list,
    25      best_slices : Proof.context -> (real * (bool * (int * string list))) list}
    26 
    27   val e_weight_method : string Config.T
    28   val e_default_fun_weight : real Config.T
    29   val e_fun_weight_base : real Config.T
    30   val e_fun_weight_span : real Config.T
    31   val e_default_sym_offs_weight : real Config.T
    32   val e_sym_offs_weight_base : real Config.T
    33   val e_sym_offs_weight_span : real Config.T
    34   val spass_force_sos : bool Config.T
    35   val vampire_force_sos : bool Config.T
    36   val eN : string
    37   val spassN : string
    38   val vampireN : string
    39   val leo2N : string
    40   val satallaxN : string
    41   val sine_eN : string
    42   val snarkN : string
    43   val tofof_eN : string
    44   val waldmeisterN : string
    45   val z3_atpN : string
    46   val remote_prefix : string
    47   val remote_atp :
    48     string -> string -> string list -> (string * string) list
    49     -> (failure * string) list -> formula_kind -> formula_kind -> format list
    50     -> (Proof.context -> int * string list) -> string * atp_config
    51   val add_atp : string * atp_config -> theory -> theory
    52   val get_atp : theory -> string -> atp_config
    53   val supported_atps : theory -> string list
    54   val is_atp_installed : theory -> string -> bool
    55   val refresh_systems_on_tptp : unit -> unit
    56   val setup : theory -> theory
    57 end;
    58 
    59 structure ATP_Systems : ATP_SYSTEMS =
    60 struct
    61 
    62 open ATP_Problem
    63 open ATP_Proof
    64 
    65 (* ATP configuration *)
    66 
    67 type atp_config =
    68   {exec : string * string,
    69    required_execs : (string * string) list,
    70    arguments :
    71      Proof.context -> bool -> int -> Time.time -> (unit -> (string * real) list)
    72      -> string,
    73    proof_delims : (string * string) list,
    74    known_failures : (failure * string) list,
    75    conj_sym_kind : formula_kind,
    76    prem_kind : formula_kind,
    77    formats : format list,
    78    best_slices : Proof.context -> (real * (bool * (int * string list))) list}
    79 
    80 (* "best_slices" must be found empirically, taking a wholistic approach since
    81    the ATPs are run in parallel. The "real" components give the faction of the
    82    time available given to the slice; these should add up to 1.0. The "bool"
    83    component indicates whether the slice's strategy is complete; the "int", the
    84    preferred number of facts to pass; the "string list", the preferred type
    85    systems, which should be of the form [sound] or [unsound, sound], where
    86    "sound" is a sound type system and "unsound" is an unsound one.
    87 
    88    The last slice should be the most "normal" one, because it will get all the
    89    time available if the other slices fail early and also because it is used for
    90    remote provers and if slicing is disabled. *)
    91 
    92 val known_perl_failures =
    93   [(CantConnect, "HTTP error"),
    94    (NoPerl, "env: perl"),
    95    (NoLibwwwPerl, "Can't locate HTTP")]
    96 
    97 (* named ATPs *)
    98 
    99 val eN = "e"
   100 val spassN = "spass"
   101 val vampireN = "vampire"
   102 val z3_atpN = "z3_atp"
   103 val leo2N = "leo2"
   104 val satallaxN = "satallax"
   105 val sine_eN = "sine_e"
   106 val snarkN = "snark"
   107 val tofof_eN = "tofof_e"
   108 val waldmeisterN = "waldmeister"
   109 val remote_prefix = "remote_"
   110 
   111 structure Data = Theory_Data
   112 (
   113   type T = (atp_config * stamp) Symtab.table
   114   val empty = Symtab.empty
   115   val extend = I
   116   fun merge data : T = Symtab.merge (eq_snd op =) data
   117     handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
   118 )
   119 
   120 fun to_secs time = (Time.toMilliseconds time + 999) div 1000
   121 
   122 
   123 (* E *)
   124 
   125 val tstp_proof_delims =
   126   [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"),
   127    ("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")]
   128 
   129 val e_slicesN = "slices"
   130 val e_autoN = "auto"
   131 val e_fun_weightN = "fun_weight"
   132 val e_sym_offset_weightN = "sym_offset_weight"
   133 
   134 val e_weight_method =
   135   Attrib.setup_config_string @{binding atp_e_weight_method} (K e_slicesN)
   136 (* FUDGE *)
   137 val e_default_fun_weight =
   138   Attrib.setup_config_real @{binding atp_e_default_fun_weight} (K 20.0)
   139 val e_fun_weight_base =
   140   Attrib.setup_config_real @{binding atp_e_fun_weight_base} (K 0.0)
   141 val e_fun_weight_span =
   142   Attrib.setup_config_real @{binding atp_e_fun_weight_span} (K 40.0)
   143 val e_default_sym_offs_weight =
   144   Attrib.setup_config_real @{binding atp_e_default_sym_offs_weight} (K 1.0)
   145 val e_sym_offs_weight_base =
   146   Attrib.setup_config_real @{binding atp_e_sym_offs_weight_base} (K ~20.0)
   147 val e_sym_offs_weight_span =
   148   Attrib.setup_config_real @{binding atp_e_sym_offs_weight_span} (K 60.0)
   149 
   150 fun e_weight_method_case method fw sow =
   151   if method = e_fun_weightN then fw
   152   else if method = e_sym_offset_weightN then sow
   153   else raise Fail ("unexpected" ^ quote method)
   154 
   155 fun scaled_e_weight ctxt method w =
   156   w * Config.get ctxt
   157           (e_weight_method_case method e_fun_weight_span e_sym_offs_weight_span)
   158   + Config.get ctxt
   159         (e_weight_method_case method e_fun_weight_base e_sym_offs_weight_base)
   160   |> Real.ceil |> signed_string_of_int
   161 
   162 fun e_weight_arguments ctxt method weights =
   163   if method = e_autoN then
   164     "-xAutoDev"
   165   else
   166     "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
   167     \--destructive-er-aggressive --destructive-er --presat-simplify \
   168     \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
   169     \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
   170     \-H'(4*" ^ e_weight_method_case method "FunWeight" "SymOffsetWeight" ^
   171     "(SimulateSOS, " ^
   172     (e_weight_method_case method e_default_fun_weight e_default_sym_offs_weight
   173      |> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
   174     ",20,1.5,1.5,1" ^
   175     (weights ()
   176      |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight ctxt method w)
   177      |> implode) ^
   178     "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\
   179     \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\
   180     \FIFOWeight(PreferProcessed))'"
   181 
   182 fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.2w") = LESS)
   183 
   184 fun effective_e_weight_method ctxt =
   185   if is_old_e_version () then e_autoN else Config.get ctxt e_weight_method
   186 
   187 (* The order here must correspond to the order in "e_config" below. *)
   188 fun method_for_slice ctxt slice =
   189   let val method = effective_e_weight_method ctxt in
   190     if method = e_slicesN then
   191       case slice of
   192         0 => e_sym_offset_weightN
   193       | 1 => e_autoN
   194       | 2 => e_fun_weightN
   195       | _ => raise Fail "no such slice"
   196     else
   197       method
   198   end
   199 
   200 val e_config : atp_config =
   201   {exec = ("E_HOME", "eproof"),
   202    required_execs = [],
   203    arguments =
   204      fn ctxt => fn full_proof => fn slice => fn timeout => fn weights =>
   205         "--tstp-in --tstp-out -l5 " ^
   206         e_weight_arguments ctxt (method_for_slice ctxt slice) weights ^
   207         " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs timeout) ^
   208         (if full_proof orelse is_old_e_version () then "" else " --trim"),
   209    proof_delims = tstp_proof_delims,
   210    known_failures =
   211      [(Unprovable, "SZS status: CounterSatisfiable"),
   212       (Unprovable, "SZS status CounterSatisfiable"),
   213       (ProofMissing, "SZS status Theorem"),
   214       (TimedOut, "Failure: Resource limit exceeded (time)"),
   215       (TimedOut, "time limit exceeded"),
   216       (OutOfResources,
   217        "# Cannot determine problem status within resource limit"),
   218       (OutOfResources, "SZS status: ResourceOut"),
   219       (OutOfResources, "SZS status ResourceOut")],
   220    conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *)
   221    prem_kind = Conjecture,
   222    formats = [FOF],
   223    best_slices = fn ctxt =>
   224      (* FUDGE *)
   225      if effective_e_weight_method ctxt = e_slicesN then
   226        [(0.333, (true, (100, ["mangled_preds_heavy"]))) (* sym_offset_weight *),
   227         (0.333, (true, (800, ["poly_preds?"]))) (* auto *),
   228         (0.334, (true, (200, ["mangled_tags!", "mangled_tags?"])))
   229                                                                (* fun_weight *)]
   230      else
   231        [(1.0, (true, (200, ["mangled_tags!", "mangled_tags?"])))]}
   232 
   233 val e = (eN, e_config)
   234 
   235 
   236 (* SPASS *)
   237 
   238 val spass_force_sos =
   239   Attrib.setup_config_bool @{binding atp_spass_force_sos} (K false)
   240 
   241 (* The "-VarWeight=3" option helps the higher-order problems, probably by
   242    counteracting the presence of "hAPP". *)
   243 val spass_config : atp_config =
   244   {exec = ("ISABELLE_ATP", "scripts/spass"),
   245    required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
   246    arguments = fn ctxt => fn _ => fn slice => fn timeout => fn _ =>
   247      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
   248       \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs timeout))
   249      |> (slice < 2 orelse Config.get ctxt spass_force_sos) ? prefix "-SOS=1 ",
   250    proof_delims = [("Here is a proof", "Formulae used in the proof")],
   251    known_failures =
   252      known_perl_failures @
   253      [(GaveUp, "SPASS beiseite: Completion found"),
   254       (TimedOut, "SPASS beiseite: Ran out of time"),
   255       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
   256       (MalformedInput, "Undefined symbol"),
   257       (MalformedInput, "Free Variable"),
   258       (SpassTooOld, "tptp2dfg"),
   259       (InternalError, "Please report this error")],
   260    conj_sym_kind = Axiom, (* FIXME: try out Hypothesis *)
   261    prem_kind = Conjecture,
   262    formats = [FOF],
   263    best_slices = fn ctxt =>
   264      (* FUDGE *)
   265      [(0.333, (false, (150, ["mangled_preds_heavy"]))) (* SOS *),
   266       (0.333, (false, (150, ["mangled_preds?"]))) (* SOS *),
   267       (0.334, (true, (150, ["poly_preds"]))) (* ~SOS *)]
   268      |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
   269          else I)}
   270 
   271 val spass = (spassN, spass_config)
   272 
   273 
   274 (* Vampire *)
   275 
   276 val vampire_force_sos =
   277   Attrib.setup_config_bool @{binding atp_vampire_force_sos} (K false)
   278 
   279 val vampire_config : atp_config =
   280   {exec = ("VAMPIRE_HOME", "vampire"),
   281    required_execs = [],
   282    arguments = fn ctxt => fn _ => fn slice => fn timeout => fn _ =>
   283      "--proof tptp --mode casc -t " ^ string_of_int (to_secs timeout) ^
   284      " --thanks \"Andrei and Krystof\" --input_file"
   285      |> (slice < 2 orelse Config.get ctxt vampire_force_sos)
   286         ? prefix "--sos on ",
   287    proof_delims =
   288      [("=========== Refutation ==========",
   289        "======= End of refutation ======="),
   290       ("% SZS output start Refutation", "% SZS output end Refutation"),
   291       ("% SZS output start Proof", "% SZS output end Proof")],
   292    known_failures =
   293      [(GaveUp, "UNPROVABLE"),
   294       (GaveUp, "CANNOT PROVE"),
   295       (GaveUp, "SZS status GaveUp"),
   296       (ProofIncomplete, "predicate_definition_introduction,[]"),
   297       (TimedOut, "SZS status Timeout"),
   298       (Unprovable, "Satisfiability detected"),
   299       (Unprovable, "Termination reason: Satisfiable"),
   300       (VampireTooOld, "not a valid option"),
   301       (Interrupted, "Aborted by signal SIGINT")],
   302    conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *)
   303    prem_kind = Conjecture,
   304    formats = [FOF],
   305    best_slices = fn ctxt =>
   306      (* FUDGE *)
   307      [(0.333, (false, (200, ["mangled_preds_heavy"]))) (* SOS *),
   308       (0.333, (false, (300, ["mangled_tags?"]))) (* SOS *),
   309       (0.334, (true, (400, ["poly_preds"]))) (* ~SOS *)]
   310      |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
   311          else I)}
   312 
   313 val vampire = (vampireN, vampire_config)
   314 
   315 
   316 (* Z3 with TPTP syntax *)
   317 
   318 val z3_atp_config : atp_config =
   319   {exec = ("Z3_HOME", "z3"),
   320    required_execs = [],
   321    arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
   322      "MBQI=true -p -t:" ^ string_of_int (to_secs timeout),
   323    proof_delims = [],
   324    known_failures =
   325      [(Unprovable, "\nsat"),
   326       (GaveUp, "\nunknown"),
   327       (GaveUp, "SZS status Satisfiable"),
   328       (ProofMissing, "\nunsat"),
   329       (ProofMissing, "SZS status Unsatisfiable")],
   330    conj_sym_kind = Hypothesis,
   331    prem_kind = Hypothesis,
   332    formats = [FOF],
   333    best_slices =
   334      (* FUDGE (FIXME) *)
   335      K [(1.0, (false, (250, [])))]}
   336 
   337 val z3_atp = (z3_atpN, z3_atp_config)
   338 
   339 
   340 (* Remote ATP invocation via SystemOnTPTP *)
   341 
   342 val systems = Synchronized.var "atp_systems" ([] : string list)
   343 
   344 fun get_systems () =
   345   case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
   346     (output, 0) => split_lines output
   347   | (output, _) =>
   348     error (case extract_known_failure known_perl_failures output of
   349              SOME failure => string_for_failure failure
   350            | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
   351 
   352 fun find_system name [] systems =
   353     find_first (String.isPrefix (name ^ "---")) systems
   354   | find_system name (version :: versions) systems =
   355     case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
   356       NONE => find_system name versions systems
   357     | res => res
   358 
   359 fun get_system name versions =
   360   Synchronized.change_result systems
   361       (fn systems => (if null systems then get_systems () else systems)
   362                      |> `(`(find_system name versions)))
   363 
   364 fun the_system name versions =
   365   case get_system name versions of
   366     (SOME sys, _) => sys
   367   | (NONE, []) => error ("SystemOnTPTP is currently not available.")
   368   | (NONE, syss) =>
   369     error ("System " ^ quote name ^ " is not available at SystemOnTPTP.\n" ^
   370            "(Available systems: " ^ commas_quote syss ^ ".)")
   371 
   372 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
   373 
   374 fun remote_config system_name system_versions proof_delims known_failures
   375                   conj_sym_kind prem_kind formats best_slice : atp_config =
   376   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
   377    required_execs = [],
   378    arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
   379      "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs timeout))
   380      ^ " -s " ^ the_system system_name system_versions,
   381    proof_delims = union (op =) tstp_proof_delims proof_delims,
   382    known_failures = known_failures @ known_perl_failures @
   383      [(Unprovable, "says Satisfiable"),
   384       (Unprovable, "says CounterSatisfiable"),
   385       (GaveUp, "says Unknown"),
   386       (GaveUp, "says GaveUp"),
   387       (ProofMissing, "says Theorem"),
   388       (ProofMissing, "says Unsatisfiable"),
   389       (TimedOut, "says Timeout"),
   390       (Inappropriate, "says Inappropriate")],
   391    conj_sym_kind = conj_sym_kind,
   392    prem_kind = prem_kind,
   393    formats = formats,
   394    best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))]}
   395 
   396 fun remotify_config system_name system_versions
   397         ({proof_delims, known_failures, conj_sym_kind, prem_kind, formats,
   398           best_slices, ...} : atp_config) : atp_config =
   399   remote_config system_name system_versions proof_delims known_failures
   400                 conj_sym_kind prem_kind formats
   401                 (best_slices #> List.last #> snd #> snd)
   402 
   403 fun remote_atp name system_name system_versions proof_delims known_failures
   404         conj_sym_kind prem_kind formats best_slice =
   405   (remote_prefix ^ name,
   406    remote_config system_name system_versions proof_delims known_failures
   407                  conj_sym_kind prem_kind formats best_slice)
   408 fun remotify_atp (name, config) system_name system_versions =
   409   (remote_prefix ^ name, remotify_config system_name system_versions config)
   410 
   411 val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"]
   412 val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
   413 val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"]
   414 val remote_leo2 =
   415   remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
   416              (K (100, ["simple"]) (* FUDGE *))
   417 val remote_satallax =
   418   remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
   419              (K (64, ["simple"]) (* FUDGE *))
   420 val remote_sine_e =
   421   remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config)
   422              Axiom Conjecture [FOF]
   423              (K (500, ["poly_tags_heavy!", "poly_tags_heavy"]) (* FUDGE *))
   424 val remote_snark =
   425   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
   426              [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
   427              [TFF, FOF] (K (100, ["simple"]) (* FUDGE *))
   428 val remote_tofof_e =
   429   remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
   430              Axiom Hypothesis [TFF] (K (150, ["simple"]) (* FUDGE *))
   431 val remote_waldmeister =
   432   remote_atp waldmeisterN "Waldmeister" ["710"]
   433              [("#START OF PROOF", "Proved Goals:")]
   434              [(OutOfResources, "Too many function symbols"),
   435               (Crashed, "Unrecoverable Segmentation Fault")]
   436              Hypothesis Hypothesis [CNF_UEQ]
   437              (K (50, ["mangled_args", "mangled_tags?"]) (* FUDGE *))
   438 
   439 (* Setup *)
   440 
   441 fun add_atp (name, config) thy =
   442   Data.map (Symtab.update_new (name, (config, stamp ()))) thy
   443   handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
   444 
   445 fun get_atp thy name =
   446   the (Symtab.lookup (Data.get thy) name) |> fst
   447   handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
   448 
   449 val supported_atps = Symtab.keys o Data.get
   450 
   451 fun is_atp_installed thy name =
   452   let val {exec, required_execs, ...} = get_atp thy name in
   453     forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
   454   end
   455 
   456 fun refresh_systems_on_tptp () =
   457   Synchronized.change systems (fn _ => get_systems ())
   458 
   459 val atps =
   460   [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
   461    remote_leo2, remote_satallax, remote_sine_e, remote_snark, remote_tofof_e,
   462    remote_waldmeister]
   463 val setup = fold add_atp atps
   464 
   465 end;