src/HOL/Tools/ATP/atp_systems.ML

   type failure = ATP_Proof.failure
 
   type atp_config =
     {exec: string * string,
      required_execs: (string * string) list,
-     arguments: bool -> Time.time -> string,
+     arguments: bool -> Time.time -> (unit -> (string * real) list) -> string,
      has_incomplete_mode: bool,
      proof_delims: (string * string) list,
      known_failures: (failure * string) list,
      default_max_relevant: int,
      explicit_forall: bool,
      use_conjecture_for_hypotheses: bool}
+
+  (* for experimentation purposes -- do not use in production code *)
+  val e_generate_weights : bool Unsynchronized.ref
+  val e_weight_factor : real Unsynchronized.ref
+  val e_default_weight : real Unsynchronized.ref
 
   val eN : string
   val spassN : string
   val vampireN : string
   val sine_eN : string

 (* ATP configuration *)
 
 type atp_config =
   {exec: string * string,
    required_execs: (string * string) list,
-   arguments: bool -> Time.time -> string,
+   arguments: bool -> Time.time -> (unit -> (string * real) list) -> string,
    has_incomplete_mode: bool,
    proof_delims: (string * string) list,
    known_failures: (failure * string) list,
    default_max_relevant: int,
    explicit_forall: bool,

     else 1000
 
 val tstp_proof_delims =
   ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
 
+val e_generate_weights = Unsynchronized.ref false
+val e_weight_factor = Unsynchronized.ref 4.0
+val e_default_weight = Unsynchronized.ref 0.5
+
+fun e_weights weights =
+  if !e_generate_weights then
+    "(1*FunWeight(ConstPrio," ^
+    string_of_int (Real.ceil (!e_default_weight * !e_weight_factor)) ^
+    ",1,1.5,1.5,1.5" ^
+    (weights ()
+     |> map (fn (s, w) => "," ^ s ^ ":" ^
+                          string_of_int (Real.ceil (w * !e_weight_factor)))
+     |> implode) ^ ")+5*AutoDev)"
+  else
+    "AutoDev"
+
 val e_config : atp_config =
   {exec = ("E_HOME", "eproof"),
    required_execs = [],
-   arguments = fn _ => fn timeout =>
-     "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent \
-     \--cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout),
+   arguments = fn _ => fn timeout => fn weights =>
+     "--tstp-in --tstp-out -l5 -x'" ^ e_weights weights ^ "' -tAutoDev \
+     \--silent --cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout),
    has_incomplete_mode = false,
    proof_delims = [tstp_proof_delims],
    known_failures =
      [(Unprovable, "SZS status: CounterSatisfiable"),
       (Unprovable, "SZS status CounterSatisfiable"),

 (* The "-VarWeight=3" option helps the higher-order problems, probably by
    counteracting the presence of "hAPP". *)
 val spass_config : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/spass"),
    required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
-   arguments = fn complete => fn timeout =>
+   arguments = fn complete => fn timeout => fn _ =>
      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
       \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
      |> not complete ? prefix "-SOS=1 ",
    has_incomplete_mode = true,
    proof_delims = [("Here is a proof", "Formulae used in the proof")],

 (* Vampire *)
 
 val vampire_config : atp_config =
   {exec = ("VAMPIRE_HOME", "vampire"),
    required_execs = [],
-   arguments = fn complete => fn timeout =>
+   arguments = fn complete => fn timeout => fn _ =>
      (* This would work too but it's less tested: "--proof tptp " ^ *)
      "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
      " --thanks \"Andrei and Krystof\" --input_file"
      |> not complete ? prefix "--sos on ",
    has_incomplete_mode = true,

 fun remote_config system_name system_versions proof_delims known_failures
                   default_max_relevant use_conjecture_for_hypotheses
                   : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_execs = [],
-   arguments = fn _ => fn timeout =>
+   arguments = fn _ => fn timeout => fn _ =>
      " -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
      ^ " -s " ^ the_system system_name system_versions,
    has_incomplete_mode = false,
    proof_delims = insert (op =) tstp_proof_delims proof_delims,
    known_failures =