36 |
36 |
37 fun n_facts names = |
37 fun n_facts names = |
38 let val n = length names in |
38 let val n = length names in |
39 string_of_int n ^ " fact" ^ plural_s n ^ |
39 string_of_int n ^ " fact" ^ plural_s n ^ |
40 (if n > 0 then |
40 (if n > 0 then |
41 ": " ^ (names |> map fst |
41 ": " ^ (names |> map fst |> sort_distinct string_ord |
42 |> sort_distinct string_ord |> space_implode " ") |
42 |> space_implode " ") |
43 else |
43 else |
44 "") |
44 "") |
45 end |
45 end |
46 |
46 |
47 fun print silent f = if silent then () else Output.urgent_message (f ()) |
47 fun print silent f = if silent then () else Output.urgent_message (f ()) |
108 | _ => sublinear_minimize test xs (x :: seen, result) |
108 | _ => sublinear_minimize test xs (x :: seen, result) |
109 |
109 |
110 fun binary_minimize test xs = |
110 fun binary_minimize test xs = |
111 let |
111 let |
112 fun pred xs = #outcome (test xs : prover_result) = NONE |
112 fun pred xs = #outcome (test xs : prover_result) = NONE |
113 fun split [] p = p |
|
114 | split [h] (l, r) = (h :: l, r) |
|
115 | split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r) |
|
116 fun min _ _ [] = raise Empty |
113 fun min _ _ [] = raise Empty |
117 | min _ _ [s0] = [s0] |
114 | min _ _ [s0] = [s0] |
118 | min depth sup xs = |
115 | min depth sup xs = |
119 let |
116 let |
|
117 val (l0, r0) = chop ((length xs + 1) div 2) xs |
120 (* |
118 (* |
121 val _ = warning (replicate_string depth " " ^ "{" ^ (" " ^ |
119 val _ = warning (replicate_string depth " " ^ "{ " ^ |
122 n_facts (map fst sup) ^ " and " ^ |
120 "sup: " ^ n_facts (map fst sup)) |
123 n_facts (map fst xs))) |
121 val _ = warning (replicate_string depth " " ^ " " ^ |
|
122 "xs: " ^ n_facts (map fst xs)) |
|
123 val _ = warning (replicate_string depth " " ^ " " ^ |
|
124 "l0: " ^ n_facts (map fst l0)) |
|
125 val _ = warning (replicate_string depth " " ^ " " ^ |
|
126 "r0: " ^ n_facts (map fst r0)) |
124 *) |
127 *) |
125 val (l0, r0) = split xs ([], []) |
|
126 in |
128 in |
127 if pred (sup @ l0) then |
129 if pred (sup @ l0) then |
128 min (depth + 1) sup l0 |
130 min (depth + 1) sup l0 |
129 else if pred (sup @ r0) then |
131 else if pred (sup @ r0) then |
130 min (depth + 1) sup r0 |
132 min (depth + 1) sup r0 |