# HG changeset patch
# User blanchet
# Date 1282210193 -7200
# Node ID ce117ef51999a8d956147fe97a8e712162a9b1ad
# Parent  db482afec7f0bce0664d613c7e2286120495929b
added remote SInE and remote SNARK

diff -r db482afec7f0 -r ce117ef51999 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 19 11:02:59 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 19 11:29:53 2010 +0200
@@ -229,14 +229,13 @@
     NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.")
   | SOME sys => sys);
 
-fun remote_config atp_prefix
-        ({proof_delims, known_failures, default_max_relevant_per_iter,
-          default_theory_relevant, ...} : prover_config) : prover_config =
+fun remote_config system_prefix proof_delims known_failures
+                  default_max_relevant_per_iter default_theory_relevant =
   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_execs = [],
    arguments = fn _ => fn timeout =>
      " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
-     the_system atp_prefix,
+     the_system system_prefix,
    proof_delims = insert (op =) tstp_proof_delims proof_delims,
    known_failures =
      known_failures @ known_perl_failures @
@@ -245,27 +244,42 @@
    default_theory_relevant = default_theory_relevant,
    explicit_forall = true}
 
-val remote_name = prefix "remote_"
-fun remote_prover (name, config) atp_prefix =
-  (remote_name name, remote_config atp_prefix config)
+fun remotify_config system_prefix
+        ({proof_delims, known_failures, default_max_relevant_per_iter,
+          default_theory_relevant, ...} : prover_config) : prover_config =
+  remote_config system_prefix proof_delims known_failures
+                default_max_relevant_per_iter default_theory_relevant
 
-val remote_e = remote_prover e "EP---"
-val remote_vampire = remote_prover vampire "Vampire---9"
+val remotify_name = prefix "remote_"
+fun remote_prover name system_prefix proof_delims known_failures
+                  default_max_relevant_per_iter default_theory_relevant =
+  (remotify_name name,
+   remote_config system_prefix proof_delims known_failures
+                 default_max_relevant_per_iter default_theory_relevant)
+fun remotify_prover (name, config) system_prefix =
+  (remotify_name name, remotify_config system_prefix config)
 
+val remote_e = remotify_prover e "EP---"
+val remote_vampire = remotify_prover vampire "Vampire---9"
+val remote_sine_e = remote_prover "sine_e" "SInE---" [] [] 150 (* FIXME *) false
+val remote_snark =
+  remote_prover "snark" "SNARK---" [("refutation.", "end_refutation.")] []
+                50 (* FIXME *) false
 
 (* Setup *)
 
 fun is_installed ({exec, required_execs, ...} : prover_config) =
   forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
 fun maybe_remote (name, config) =
-  name |> not (is_installed config) ? remote_name
+  name |> not (is_installed config) ? remotify_name
 
 fun default_atps_param_value () =
   space_implode " " ([maybe_remote e] @
                      (if is_installed (snd spass) then [fst spass] else []) @
-                     [remote_name (fst vampire)])
+                     [remotify_name (fst vampire), fst remote_sine_e])
 
-val provers = [e, spass, vampire, remote_e, remote_vampire]
+val provers = [e, spass, vampire, remote_e, remote_vampire, remote_sine_e,
+               remote_snark]
 val setup = fold add_prover provers
 
 end;