src/HOL/Tools/ATP_Manager/atp_systems.ML

   {home_var: string,
    executable: string,
    arguments: bool -> Time.time -> string,
    proof_delims: (string * string) list,
    known_failures: (failure * string) list,
-   max_axiom_clauses: int,
+   max_new_relevant_facts_per_iter: int,
    prefers_theory_relevant: bool,
    explicit_forall: bool}
 
 
 (* basic template *)

   #> parse_clause_formula_relation #> fst
 
 fun repair_conjecture_shape_and_theorem_names output conjecture_shape
                                               thm_names =
   if String.isSubstring set_ClauseFormulaRelationN output then
+    (* This is a hack required for keeping track of axioms after they have been
+       clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part
+       of this hack. *)
     let
       val j0 = hd conjecture_shape
       val seq = extract_clause_sequence output
       val name_map = extract_clause_formula_relation output
       fun renumber_conjecture j =

 
 (* generic TPTP-based provers *)
 
 fun generic_tptp_prover
         (name, {home_var, executable, arguments, proof_delims, known_failures,
-                max_axiom_clauses, prefers_theory_relevant, explicit_forall})
+                max_new_relevant_facts_per_iter, prefers_theory_relevant,
+                explicit_forall})
         ({debug, overlord, full_types, explicit_apply, relevance_threshold,
           relevance_convergence, theory_relevant, defs_relevant, isar_proof,
           isar_shrink_factor, ...} : params)
         minimize_command timeout
         ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}

     val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
     val the_filtered_clauses =
       case filtered_clauses of
         SOME fcls => fcls
       | NONE => relevant_facts full_types relevance_threshold
-                    relevance_convergence defs_relevant max_axiom_clauses
+                    relevance_convergence defs_relevant
+                    max_new_relevant_facts_per_iter
                     (the_default prefers_theory_relevant theory_relevant)
                     relevance_override goal hyp_ts concl_t
     val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
     val (internal_thm_names, clauses) =
       prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses

       (TimedOut, "time limit exceeded"),
       (OutOfResources,
        "# Cannot determine problem status within resource limit"),
       (OutOfResources, "SZS status: ResourceOut"),
       (OutOfResources, "SZS status ResourceOut")],
-   max_axiom_clauses = 100,
+   max_new_relevant_facts_per_iter = 80 (* FIXME *),
    prefers_theory_relevant = false,
    explicit_forall = false}
 val e = tptp_prover "e" e_config
 
 

       (TimedOut, "SPASS beiseite: Ran out of time"),
       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
       (MalformedInput, "Undefined symbol"),
       (MalformedInput, "Free Variable"),
       (OldSpass, "tptp2dfg")],
-   max_axiom_clauses = 40,
+   max_new_relevant_facts_per_iter = 26 (* FIXME *),
    prefers_theory_relevant = true,
    explicit_forall = true}
 val spass = tptp_prover "spass" spass_config
 
 (* Vampire *)

    known_failures =
      [(Unprovable, "UNPROVABLE"),
       (IncompleteUnprovable, "CANNOT PROVE"),
       (Unprovable, "Satisfiability detected"),
       (OutOfResources, "Refutation not found")],
-   max_axiom_clauses = 60,
+   max_new_relevant_facts_per_iter = 40 (* FIXME *),
    prefers_theory_relevant = false,
    explicit_forall = false}
 val vampire = tptp_prover "vampire" vampire_config
 
 (* Remote prover invocation via SystemOnTPTP *)

   [(CantConnect, "HTTP-Error"),
    (TimedOut, "says Timeout"),
    (MalformedOutput, "Remote script could not extract proof")]
 
 fun remote_config atp_prefix args
-        ({proof_delims, known_failures, max_axiom_clauses,
+        ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
           prefers_theory_relevant, explicit_forall, ...} : prover_config)
         : prover_config =
   {home_var = "ISABELLE_ATP_MANAGER",
    executable = "SystemOnTPTP",
    arguments = fn _ => fn timeout =>
      args ^ " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
      the_system atp_prefix,
    proof_delims = insert (op =) tstp_proof_delims proof_delims,
    known_failures = remote_known_failures @ known_failures,
-   max_axiom_clauses = max_axiom_clauses,
+   max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
    prefers_theory_relevant = prefers_theory_relevant,
    explicit_forall = explicit_forall}
 
 fun remote_tptp_prover prover atp_prefix args config =
   tptp_prover (remotify (fst prover)) (remote_config atp_prefix args config)