src/HOL/Tools/ATP_Manager/atp_systems.ML
changeset 37498 b426cbdb5a23
parent 37480 d5a85d35ef62
child 37499 5ff37037fbec
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jun 22 13:17:59 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jun 22 14:28:22 2010 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4  
     1.5  fun shape_of_clauses _ [] = []
     1.6    | shape_of_clauses j ([] :: clauses) = [] :: shape_of_clauses j clauses
     1.7 -  | shape_of_clauses j ((lit :: lits) :: clauses) =
     1.8 +  | shape_of_clauses j ((_ :: lits) :: clauses) =
     1.9      let val shape = shape_of_clauses (j + 1) (lits :: clauses) in
    1.10        (j :: hd shape) :: tl shape
    1.11      end
    1.12 @@ -123,7 +123,7 @@
    1.13           : problem) =
    1.14    let
    1.15      (* get clauses and prepare them for writing *)
    1.16 -    val (ctxt, (chained_ths, th)) = goal;
    1.17 +    val (ctxt, (_, th)) = goal;
    1.18      val thy = ProofContext.theory_of ctxt;
    1.19      val goal_clss = #1 (neg_conjecture_clauses ctxt th subgoal)
    1.20      val goal_cls = List.concat goal_clss
    1.21 @@ -136,7 +136,7 @@
    1.22          NONE => the_filtered_clauses
    1.23        | SOME axcls => axcls);
    1.24      val (internal_thm_names, clauses) =
    1.25 -      prepare goal_cls chained_ths the_axiom_clauses the_filtered_clauses thy;
    1.26 +      prepare goal_cls the_axiom_clauses the_filtered_clauses thy
    1.27  
    1.28      (* path to unique problem file *)
    1.29      val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
    1.30 @@ -243,16 +243,15 @@
    1.31                  max_axiom_clauses, prefers_theory_relevant})
    1.32          (params as {debug, overlord, full_types, respect_no_atp,
    1.33                      relevance_threshold, relevance_convergence, theory_relevant,
    1.34 -                    defs_relevant, isar_proof, ...})
    1.35 +                    defs_relevant, ...})
    1.36          minimize_command timeout =
    1.37    generic_prover overlord
    1.38        (relevant_facts full_types respect_no_atp relevance_threshold
    1.39                        relevance_convergence defs_relevant max_axiom_clauses
    1.40                        (the_default prefers_theory_relevant theory_relevant))
    1.41 -      (prepare_clauses false full_types)
    1.42 -      (write_tptp_file (debug andalso overlord)) home_var
    1.43 -      executable (arguments timeout) proof_delims known_failures name params
    1.44 -      minimize_command
    1.45 +      (prepare_clauses full_types) (write_tptp_file (debug andalso overlord))
    1.46 +      home_var executable (arguments timeout) proof_delims known_failures name
    1.47 +      params minimize_command
    1.48  
    1.49  fun tptp_prover name p = (name, generic_tptp_prover (name, p));
    1.50  
    1.51 @@ -313,31 +312,14 @@
    1.52  
    1.53  (* SPASS *)
    1.54  
    1.55 -fun generic_dfg_prover
    1.56 -        (name, {home_var, executable, arguments, proof_delims, known_failures,
    1.57 -                max_axiom_clauses, prefers_theory_relevant})
    1.58 -        (params as {overlord, full_types, respect_no_atp, relevance_threshold,
    1.59 -                    relevance_convergence, theory_relevant, defs_relevant, ...})
    1.60 -        minimize_command timeout =
    1.61 -  generic_prover overlord
    1.62 -      (relevant_facts full_types respect_no_atp relevance_threshold
    1.63 -                      relevance_convergence defs_relevant max_axiom_clauses
    1.64 -                      (the_default prefers_theory_relevant theory_relevant))
    1.65 -      (prepare_clauses true full_types) write_dfg_file home_var executable
    1.66 -      (arguments timeout) proof_delims known_failures name params
    1.67 -      minimize_command
    1.68 -
    1.69 -fun dfg_prover name p = (name, generic_dfg_prover (name, p))
    1.70 -
    1.71  (* The "-VarWeight=3" option helps the higher-order problems, probably by
    1.72     counteracting the presence of "hAPP". *)
    1.73 -fun generic_spass_config dfg : prover_config =
    1.74 +val spass_config : prover_config =
    1.75    {home_var = "SPASS_HOME",
    1.76     executable = "SPASS",
    1.77     arguments = fn timeout =>
    1.78 -     "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
    1.79 -     \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout)
    1.80 -     |> not dfg ? prefix "-TPTP ",
    1.81 +     "-TPTP -Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
    1.82 +     \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout),
    1.83     proof_delims = [("Here is a proof", "Formulae used in the proof")],
    1.84     known_failures =
    1.85       [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
    1.86 @@ -349,10 +331,6 @@
    1.87        (OldSpass, "Unrecognized option TPTP")],
    1.88     max_axiom_clauses = 40,
    1.89     prefers_theory_relevant = true}
    1.90 -val spass_dfg_config = generic_spass_config true
    1.91 -val spass_dfg = dfg_prover "spass_dfg" spass_dfg_config
    1.92 -
    1.93 -val spass_config = generic_spass_config false
    1.94  val spass = tptp_prover "spass" spass_config
    1.95  
    1.96  (* remote prover invocation via SystemOnTPTP *)
    1.97 @@ -414,8 +392,7 @@
    1.98    space_implode " " [maybe_remote e e_config, maybe_remote spass spass_config,
    1.99                       remotify (fst vampire)]
   1.100  
   1.101 -val provers =
   1.102 -  [spass, spass_dfg, vampire, e, remote_vampire, remote_spass, remote_e]
   1.103 +val provers = [spass, vampire, e, remote_vampire, remote_spass, remote_e]
   1.104  val prover_setup = fold add_prover provers
   1.105  
   1.106  val setup =