src/HOL/Tools/ATP/atp_systems.ML

 Setup for supported ATPs.
 *)
 
 signature ATP_SYSTEMS =
 sig
-  type tptp_format = ATP_Problem.tptp_format
+  type atp_format = ATP_Problem.atp_format
   type formula_kind = ATP_Problem.formula_kind
   type failure = ATP_Proof.failure
 
   type atp_config =
     {exec : string * string,

      known_failures : (failure * string) list,
      conj_sym_kind : formula_kind,
      prem_kind : formula_kind,
      best_slices :
        Proof.context
-       -> (real * (bool * (int * tptp_format * string * string))) list}
+       -> (real * (bool * (int * atp_format * string * string))) list}
 
   val force_sos : bool Config.T
   val e_smartN : string
   val e_autoN : string
   val e_fun_weightN : string

   val pffN : string
   val phfN : string
   val satallaxN : string
   val snarkN : string
   val spassN : string
+  val spass_newN : string
   val vampireN : string
   val waldmeisterN : string
   val z3_tptpN : string
   val remote_prefix : string
   val remote_atp :
     string -> string -> string list -> (string * string) list
     -> (failure * string) list -> formula_kind -> formula_kind
-    -> (Proof.context -> int * tptp_format * string) -> string * atp_config
+    -> (Proof.context -> int * atp_format * string) -> string * atp_config
   val add_atp : string * atp_config -> theory -> theory
   val get_atp : theory -> string -> atp_config
   val supported_atps : theory -> string list
   val is_atp_installed : theory -> string -> bool
   val refresh_systems_on_tptp : unit -> unit

    known_failures : (failure * string) list,
    conj_sym_kind : formula_kind,
    prem_kind : formula_kind,
    best_slices :
      Proof.context
-     -> (real * (bool * (int * tptp_format * string * string))) list}
+     -> (real * (bool * (int * atp_format * string * string))) list}
 
 (* "best_slices" must be found empirically, taking a wholistic approach since
    the ATPs are run in parallel. The "real" components give the faction of the
    time available given to the slice and should add up to 1.0. The "bool"
    component indicates whether the slice's strategy is complete; the "int", the

 val pffN = "pff"
 val phfN = "phf"
 val satallaxN = "satallax"
 val snarkN = "snark"
 val spassN = "spass"
+val spass_newN = "spass_new"
 val vampireN = "vampire"
 val waldmeisterN = "waldmeister"
 val z3_tptpN = "z3_tptp"
 val remote_prefix = "remote_"
 

       (TimedOut, "SPASS beiseite: Ran out of time"),
       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
       (MalformedInput, "Undefined symbol"),
       (MalformedInput, "Free Variable"),
       (Unprovable, "No formulae and clauses found in input file"),
-      (SpassTooOld, "tptp2dfg"),
       (InternalError, "Please report this error")],
    conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)

       (0.334, (true, (50, FOF, "mono_tags??", no_sosN)))]
      |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
          else I)}
 
 val spass = (spassN, spass_config)
+
+(* Experimental *)
+val spass_new_config : atp_config =
+  {exec = ("SPASS_HOME", "SPASS"),
+   required_execs = [],
+   arguments = #arguments spass_config,
+   proof_delims = #proof_delims spass_config,
+   known_failures = #known_failures spass_config,
+   conj_sym_kind = #conj_sym_kind spass_config,
+   prem_kind = #prem_kind spass_config,
+   best_slices = fn ctxt =>
+     (* FUDGE *)
+     [(0.333, (false, (150, DFG_Sorted, "mono_simple", sosN))) (*,
+      (0.333, (false, (300, DFG_Sorted, "poly_tags??", sosN))),
+      (0.334, (true, (50, DFG_Sorted, "mono_simple", no_sosN)))*)]
+     |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
+         else I)}
+
+val spass_new = (spass_newN, spass_new_config)
 
 
 (* Vampire *)
 
 (* Vampire 1.8 has TFF support, but it's buggy and therefore disabled on

      known_szs_status_failures @
      [(GaveUp, "UNPROVABLE"),
       (GaveUp, "CANNOT PROVE"),
       (Unprovable, "Satisfiability detected"),
       (Unprovable, "Termination reason: Satisfiable"),
-      (VampireTooOld, "not a valid option"),
       (Interrupted, "Aborted by signal SIGINT")],
    conj_sym_kind = Conjecture,
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)

 
 fun refresh_systems_on_tptp () =
   Synchronized.change systems (fn _ => get_systems ())
 
 val atps =
-  [e, leo2, pff, phf, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2,
-   remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine, remote_snark,
-   remote_e_tofof, remote_waldmeister]
+  [e, leo2, pff, phf, satallax, spass, spass_new, vampire, z3_tptp, remote_e,
+   remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_e_sine,
+   remote_snark, remote_e_tofof, remote_waldmeister]
 val setup = fold add_atp atps
 
 end;