# HG changeset patch # User blanchet # Date 1300446323 -3600 # Node ID 1d7735ae42737d184d11876010a34891e9e730c3 # Parent 03c2d29ec790fdac5694a0279715023013c8955f more optimizations of bounds for "need" diff -r 03c2d29ec790 -r 1d7735ae4273 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Mar 18 11:43:28 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Mar 18 12:05:23 2011 +0100 @@ -313,7 +313,6 @@ in ([(x, bound_comment ctxt debug nick T R)], let - val ts = KK.TupleAtomSeq (epsilon - delta, delta + j0) val complete_need_vals = (length need_vals = card) val (my_need_vals, other_need_vals) = need_vals @@ -322,13 +321,22 @@ exists (fn FreeRel (x', _, _, _) => x = x' | _ => false) sel_us | _ => false) + fun upper_bound_ts () = + if complete_need_vals then + my_need_vals |> map (KK.Tuple o single o snd) |> KK.TupleSet + else if not (null other_need_vals) then + index_seq (delta + j0) (epsilon - delta) + |> filter_out (member (op = o apsnd snd) other_need_vals) + |> map (KK.Tuple o single) |> KK.TupleSet + else + KK.TupleAtomSeq (epsilon - delta, delta + j0) in if explicit_max = 0 orelse - (complete_need_vals andalso null my_need_vals) then + (complete_need_vals andalso null my_need_vals) (* ### needed? *) then [KK.TupleSet []] else if R2 = Formula Neut then - [ts] |> not exclusive ? cons (KK.TupleSet []) + [upper_bound_ts ()] |> not exclusive ? cons (KK.TupleSet []) else [KK.TupleSet [], if T1 = T2 andalso epsilon > delta andalso @@ -339,7 +347,7 @@ KK.TupleAtomSeq (j, j0))) |> foldl1 KK.TupleUnion else - KK.TupleProduct (ts, upper_bound_for_rep R2)] + KK.TupleProduct (upper_bound_ts (), upper_bound_for_rep R2)] end) end | bound_for_sel_rel _ _ _ _ u = @@ -1525,7 +1533,9 @@ else accum) | aux _ = I - in SOME (index_seq 0 card, []) |> fold aux need_us |> Option.map snd end + in + SOME (index_seq 0 card, []) |> fold aux need_us |> Option.map (rev o snd) + end fun needed_value_axioms_for_datatype _ _ NONE = [KK.False] | needed_value_axioms_for_datatype ofs kk (SOME fixed) =