1.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 13:15:58 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Tue Jul 27 13:16:37 2010 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4     arguments: bool -> Time.time -> string,
     1.5     proof_delims: (string * string) list,
     1.6     known_failures: (failure * string) list,
     1.7 -   max_axiom_clauses: int,
     1.8 +   max_new_relevant_facts_per_iter: int,
     1.9     prefers_theory_relevant: bool,
    1.10     explicit_forall: bool}
    1.11  
    1.12 @@ -345,6 +345,9 @@
    1.13  fun repair_conjecture_shape_and_theorem_names output conjecture_shape
    1.14                                                thm_names =
    1.15    if String.isSubstring set_ClauseFormulaRelationN output then
    1.16 +    (* This is a hack required for keeping track of axioms after they have been
    1.17 +       clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part
    1.18 +       of this hack. *)
    1.19      let
    1.20        val j0 = hd conjecture_shape
    1.21        val seq = extract_clause_sequence output
    1.22 @@ -369,7 +372,8 @@
    1.23  
    1.24  fun generic_tptp_prover
    1.25          (name, {home_var, executable, arguments, proof_delims, known_failures,
    1.26 -                max_axiom_clauses, prefers_theory_relevant, explicit_forall})
    1.27 +                max_new_relevant_facts_per_iter, prefers_theory_relevant,
    1.28 +                explicit_forall})
    1.29          ({debug, overlord, full_types, explicit_apply, relevance_threshold,
    1.30            relevance_convergence, theory_relevant, defs_relevant, isar_proof,
    1.31            isar_shrink_factor, ...} : params)
    1.32 @@ -386,7 +390,8 @@
    1.33        case filtered_clauses of
    1.34          SOME fcls => fcls
    1.35        | NONE => relevant_facts full_types relevance_threshold
    1.36 -                    relevance_convergence defs_relevant max_axiom_clauses
    1.37 +                    relevance_convergence defs_relevant
    1.38 +                    max_new_relevant_facts_per_iter
    1.39                      (the_default prefers_theory_relevant theory_relevant)
    1.40                      relevance_override goal hyp_ts concl_t
    1.41      val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
    1.42 @@ -529,7 +534,7 @@
    1.43         "# Cannot determine problem status within resource limit"),
    1.44        (OutOfResources, "SZS status: ResourceOut"),
    1.45        (OutOfResources, "SZS status ResourceOut")],
    1.46 -   max_axiom_clauses = 100,
    1.47 +   max_new_relevant_facts_per_iter = 80 (* FIXME *),
    1.48     prefers_theory_relevant = false,
    1.49     explicit_forall = false}
    1.50  val e = tptp_prover "e" e_config
    1.51 @@ -554,7 +559,7 @@
    1.52        (MalformedInput, "Undefined symbol"),
    1.53        (MalformedInput, "Free Variable"),
    1.54        (OldSpass, "tptp2dfg")],
    1.55 -   max_axiom_clauses = 40,
    1.56 +   max_new_relevant_facts_per_iter = 26 (* FIXME *),
    1.57     prefers_theory_relevant = true,
    1.58     explicit_forall = true}
    1.59  val spass = tptp_prover "spass" spass_config
    1.60 @@ -576,7 +581,7 @@
    1.61        (IncompleteUnprovable, "CANNOT PROVE"),
    1.62        (Unprovable, "Satisfiability detected"),
    1.63        (OutOfResources, "Refutation not found")],
    1.64 -   max_axiom_clauses = 60,
    1.65 +   max_new_relevant_facts_per_iter = 40 (* FIXME *),
    1.66     prefers_theory_relevant = false,
    1.67     explicit_forall = false}
    1.68  val vampire = tptp_prover "vampire" vampire_config
    1.69 @@ -610,7 +615,7 @@
    1.70     (MalformedOutput, "Remote script could not extract proof")]
    1.71  
    1.72  fun remote_config atp_prefix args
    1.73 -        ({proof_delims, known_failures, max_axiom_clauses,
    1.74 +        ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
    1.75            prefers_theory_relevant, explicit_forall, ...} : prover_config)
    1.76          : prover_config =
    1.77    {home_var = "ISABELLE_ATP_MANAGER",
    1.78 @@ -620,7 +625,7 @@
    1.79       the_system atp_prefix,
    1.80     proof_delims = insert (op =) tstp_proof_delims proof_delims,
    1.81     known_failures = remote_known_failures @ known_failures,
    1.82 -   max_axiom_clauses = max_axiom_clauses,
    1.83 +   max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
    1.84     prefers_theory_relevant = prefers_theory_relevant,
    1.85     explicit_forall = explicit_forall}
    1.86