equal
deleted
inserted
replaced
8 signature SLEDGEHAMMER_MINIMIZE = |
8 signature SLEDGEHAMMER_MINIMIZE = |
9 sig |
9 sig |
10 type locality = Sledgehammer_Filter.locality |
10 type locality = Sledgehammer_Filter.locality |
11 type params = Sledgehammer_Provers.params |
11 type params = Sledgehammer_Provers.params |
12 |
12 |
|
13 val binary_threshold : int Unsynchronized.ref |
13 val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list |
14 val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list |
14 val minimize_facts : |
15 val minimize_facts : |
15 string -> params -> bool -> int -> int -> Proof.state |
16 string -> params -> bool -> int -> int -> Proof.state |
16 -> ((string * locality) * thm list) list |
17 -> ((string * locality) * thm list) list |
17 -> ((string * locality) * thm list) list option * string |
18 -> ((string * locality) * thm list) list option * string |
76 |
77 |
77 (* minimalization of facts *) |
78 (* minimalization of facts *) |
78 |
79 |
79 (* The sublinear algorithm works well in almost all situations, except when the |
80 (* The sublinear algorithm works well in almost all situations, except when the |
80 external prover cannot return the list of used facts and hence returns all |
81 external prover cannot return the list of used facts and hence returns all |
81 facts as used. In that case, the binary algorithm is much more |
82 facts as used. In that case, the binary algorithm is much more appropriate. |
82 appropriate. We can usually detect that situation just by looking at the |
83 We can usually detect the situation by looking at the number of used facts |
83 number of used facts reported by the prover. *) |
84 reported by the prover. *) |
84 val binary_threshold = 50 |
85 val binary_threshold = Unsynchronized.ref 20 |
85 |
86 |
86 fun filter_used_facts used = filter (member (op =) used o fst) |
87 fun filter_used_facts used = filter (member (op =) used o fst) |
87 |
88 |
88 fun sublinear_minimize _ [] p = p |
89 fun sublinear_minimize _ [] p = p |
89 | sublinear_minimize test (x :: xs) (seen, result) = |
90 | sublinear_minimize test (x :: xs) (seen, result) = |
149 val new_timeout = |
150 val new_timeout = |
150 Int.min (msecs, Time.toMilliseconds time + fudge_msecs) |
151 Int.min (msecs, Time.toMilliseconds time + fudge_msecs) |
151 |> Time.fromMilliseconds |
152 |> Time.fromMilliseconds |
152 val facts = filter_used_facts used_facts facts |
153 val facts = filter_used_facts used_facts facts |
153 val (min_thms, {message, ...}) = |
154 val (min_thms, {message, ...}) = |
154 if length facts >= binary_threshold then |
155 if length facts >= !binary_threshold then |
155 binary_minimize (do_test new_timeout) facts |
156 binary_minimize (do_test new_timeout) facts |
156 else |
157 else |
157 sublinear_minimize (do_test new_timeout) facts ([], result) |
158 sublinear_minimize (do_test new_timeout) facts ([], result) |
158 val n = length min_thms |
159 val n = length min_thms |
159 val _ = print silent (fn () => cat_lines |
160 val _ = print silent (fn () => cat_lines |