--- a/src/HOL/Tools/atp_minimal.ML Wed Jun 03 07:12:57 2009 -0700
+++ b/src/HOL/Tools/atp_minimal.ML Wed Jun 03 16:56:41 2009 +0200
@@ -83,9 +83,9 @@
("# Cannot determine problem status within resource limit", Timeout),
("Error", Error)]
-fun produce_answer (success, message, result_string, thm_name_vec) =
+fun produce_answer (success, message, result_string, thm_name_vec, const_counts) =
if success then
- (Success (Vector.foldr op:: [] thm_name_vec), result_string)
+ (Success (Vector.foldr op:: [] thm_name_vec, const_counts), result_string)
else
let
val failure = failure_strings |> get_first (fn (s, t) =>
@@ -100,7 +100,7 @@
(* wrapper for calling external prover *)
-fun sh_test_thms prover prover_name time_limit subgoalno state name_thms_pairs =
+fun sh_test_thms prover prover_name time_limit subgoalno state counts name_thms_pairs =
let
val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
val name_thm_pairs =
@@ -108,7 +108,8 @@
val _ = debug_fn (fn () => print_names name_thm_pairs)
val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
val (result, proof) =
- produce_answer (prover time_limit (SOME axclauses) prover_name subgoalno (Proof.get_goal state))
+ produce_answer
+ (prover time_limit (SOME axclauses) counts prover_name subgoalno (Proof.get_goal state))
val _ = println (string_of_result result)
val _ = debug proof
in
@@ -126,11 +127,11 @@
val _ = debug_fn (fn () => app (fn (n, tl) =>
(debug n; app (fn t => debug (" " ^ Display.string_of_thm t)) tl)) name_thms_pairs)
val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
- fun test_thms thms = case test_thms_fun thms of (Success _, _) => true | _ => false
+ fun test_thms counts thms = case test_thms_fun counts thms of (Success _, _) => true | _ => false
in
(* try prove first to check result and get used theorems *)
- (case test_thms_fun name_thms_pairs of
- (Success used, _) =>
+ (case test_thms_fun NONE name_thms_pairs of
+ (Success (used, const_counts), _) =>
let
val ordered_used = order_unique used
val to_use =
@@ -138,7 +139,7 @@
filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
else
name_thms_pairs
- val min_thms = minimal test_thms to_use
+ val min_thms = (minimal (test_thms (SOME const_counts)) to_use)
val min_names = order_unique (map fst min_thms)
val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
val _ = debug_fn (fn () => print_names min_thms)