added the "max_sledgehammers" option
authorpaulson
Tue Oct 16 16:18:36 2007 +0200 (2007-10-16)
changeset 25047f8712e98756a
parent 25046 3d0137a59dcb
child 25048 5a94a87af697
added the "max_sledgehammers" option
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Oct 16 14:11:35 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Oct 16 16:18:36 2007 +0200
     1.3 @@ -25,6 +25,7 @@
     1.4    val pass_mark    : real ref
     1.5    val convergence  : real ref
     1.6    val max_new      : int ref
     1.7 +  val max_sledgehammers : int ref
     1.8    val follow_defs  : bool ref
     1.9    val add_all : unit -> unit
    1.10    val add_claset : unit -> unit
    1.11 @@ -57,6 +58,8 @@
    1.12  val run_blacklist_filter = ref true;
    1.13  val time_limit = ref 60;
    1.14  val prover = ref Recon.E;
    1.15 +val max_sledgehammers = ref 1;
    1.16 +
    1.17  
    1.18  (*** relevance filter parameters ***)
    1.19  val run_relevance_filter = ref true;
    1.20 @@ -734,7 +737,7 @@
    1.21    FIXME: does not cope with &&, and it isn't easy because one could have multiple
    1.22    subgoals, each involving &&.*)
    1.23  fun write_problem_files probfile (ctxt, chain_ths, th) =
    1.24 -  let val goals = Thm.prems_of th
    1.25 +  let val goals = Library.take (!max_sledgehammers, Thm.prems_of th)  (*raises no exception*)
    1.26        val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals))
    1.27        val thy = ProofContext.theory_of ctxt
    1.28        fun get_neg_subgoals [] _ = []
    1.29 @@ -799,7 +802,7 @@
    1.30  
    1.31  (*writes out the current problems and calls ATPs*)
    1.32  fun isar_atp (ctxt, chain_ths, th) =
    1.33 -  if Thm.no_prems th then ()
    1.34 +  if Thm.no_prems th then warning "Nothing to prove"
    1.35    else
    1.36      let
    1.37        val _ = kill_last_watcher()
    1.38 @@ -820,7 +823,7 @@
    1.39  
    1.40  val isar_atp_writeonly = PrintMode.setmp []
    1.41        (fn (ctxt, chain_ths, th) =>
    1.42 -       if Thm.no_prems th then ()
    1.43 +       if Thm.no_prems th then warning "Nothing to prove"
    1.44         else
    1.45           let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix
    1.46                              else prob_pathname