42 |> sort_distinct string_ord |> space_implode " ") |
42 |> sort_distinct string_ord |> space_implode " ") |
43 else |
43 else |
44 "") |
44 "") |
45 end |
45 end |
46 |
46 |
47 fun test_theorems ({debug, verbose, overlord, atps, full_types, isar_proof, |
47 fun test_theorems ({debug, verbose, overlord, provers, full_types, isar_proof, |
48 isar_shrink_factor, ...} : params) |
48 isar_shrink_factor, ...} : params) |
49 (prover : prover) explicit_apply timeout subgoal state |
49 (atp : atp) explicit_apply timeout subgoal state axioms = |
50 axioms = |
|
51 let |
50 let |
52 val _ = |
51 val _ = |
53 priority ("Testing " ^ n_theorems (map fst axioms) ^ "...") |
52 priority ("Testing " ^ n_theorems (map fst axioms) ^ "...") |
54 val params = |
53 val params = |
55 {blocking = true, debug = debug, verbose = verbose, overlord = overlord, |
54 {blocking = true, debug = debug, verbose = verbose, overlord = overlord, |
56 atps = atps, full_types = full_types, explicit_apply = explicit_apply, |
55 provers = provers, full_types = full_types, |
57 relevance_thresholds = (1.01, 1.01), |
56 explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01), |
58 max_relevant = SOME 65536 (* a large number *), isar_proof = isar_proof, |
57 max_relevant = SOME 65536 (* a large number *), isar_proof = isar_proof, |
59 isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""} |
58 isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""} |
60 val axioms = maps (fn (n, ths) => map (pair n) ths) axioms |
59 val axioms = maps (fn (n, ths) => map (pair n) ths) axioms |
61 val {context = ctxt, goal, ...} = Proof.goal state |
60 val {context = ctxt, goal, ...} = Proof.goal state |
62 val problem = |
61 val atp_problem = |
63 {state = state, goal = goal, subgoal = subgoal, |
62 {state = state, goal = goal, subgoal = subgoal, |
64 axioms = map (prepare_axiom ctxt) axioms, only = true} |
63 axioms = map (prepare_axiom ctxt) axioms, only = true} |
65 val result as {outcome, used_thm_names, ...} = prover params (K "") problem |
64 val result as {outcome, used_thm_names, ...} = atp params (K "") atp_problem |
66 in |
65 in |
67 priority (case outcome of |
66 priority (case outcome of |
68 NONE => |
67 NONE => |
69 if length used_thm_names = length axioms then |
68 if length used_thm_names = length axioms then |
70 "Found proof." |
69 "Found proof." |
79 fun filter_used_facts used = filter (member (op =) used o fst) |
78 fun filter_used_facts used = filter (member (op =) used o fst) |
80 |
79 |
81 fun sublinear_minimize _ [] p = p |
80 fun sublinear_minimize _ [] p = p |
82 | sublinear_minimize test (x :: xs) (seen, result) = |
81 | sublinear_minimize test (x :: xs) (seen, result) = |
83 case test (xs @ seen) of |
82 case test (xs @ seen) of |
84 result as {outcome = NONE, used_thm_names, ...} : prover_result => |
83 result as {outcome = NONE, used_thm_names, ...} : atp_result => |
85 sublinear_minimize test (filter_used_facts used_thm_names xs) |
84 sublinear_minimize test (filter_used_facts used_thm_names xs) |
86 (filter_used_facts used_thm_names seen, result) |
85 (filter_used_facts used_thm_names seen, result) |
87 | _ => sublinear_minimize test xs (x :: seen, result) |
86 | _ => sublinear_minimize test xs (x :: seen, result) |
88 |
87 |
89 (* Give the ATP some slack. The ATP gets further slack because the Sledgehammer |
88 (* Give the ATP some slack. The ATP gets further slack because the Sledgehammer |
90 preprocessing time is included in the estimate below but isn't part of the |
89 preprocessing time is included in the estimate below but isn't part of the |
91 timeout. *) |
90 timeout. *) |
92 val fudge_msecs = 1000 |
91 val fudge_msecs = 1000 |
93 |
92 |
94 fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set." |
93 fun minimize_theorems {provers = [], ...} _ _ _ _ = error "No prover is set." |
95 | minimize_theorems (params as {debug, atps = atp :: _, full_types, |
94 | minimize_theorems (params as {debug, provers = prover :: _, full_types, |
96 isar_proof, isar_shrink_factor, timeout, ...}) |
95 isar_proof, isar_shrink_factor, timeout, ...}) |
97 i (_ : int) state axioms = |
96 i (_ : int) state axioms = |
98 let |
97 let |
99 val thy = Proof.theory_of state |
98 val thy = Proof.theory_of state |
100 val prover = get_prover_fun thy atp |
99 val atp = get_atp_fun thy prover |
101 val msecs = Time.toMilliseconds timeout |
100 val msecs = Time.toMilliseconds timeout |
102 val _ = priority ("Sledgehammer minimize: ATP " ^ quote atp ^ ".") |
101 val _ = priority ("Sledgehammer minimize: prover " ^ quote prover ^ ".") |
103 val {context = ctxt, goal, ...} = Proof.goal state |
102 val {context = ctxt, goal, ...} = Proof.goal state |
104 val (_, hyp_ts, concl_t) = strip_subgoal goal i |
103 val (_, hyp_ts, concl_t) = strip_subgoal goal i |
105 val explicit_apply = |
104 val explicit_apply = |
106 not (forall (Meson.is_fol_term thy) |
105 not (forall (Meson.is_fol_term thy) |
107 (concl_t :: hyp_ts @ maps (map prop_of o snd) axioms)) |
106 (concl_t :: hyp_ts @ maps (map prop_of o snd) axioms)) |
108 fun do_test timeout = |
107 fun do_test timeout = |
109 test_theorems params prover explicit_apply timeout i state |
108 test_theorems params atp explicit_apply timeout i state |
110 val timer = Timer.startRealTimer () |
109 val timer = Timer.startRealTimer () |
111 in |
110 in |
112 (case do_test timeout axioms of |
111 (case do_test timeout axioms of |
113 result as {outcome = NONE, pool, used_thm_names, |
112 result as {outcome = NONE, pool, used_thm_names, |
114 conjecture_shape, ...} => |
113 conjecture_shape, ...} => |