# HG changeset patch # User blanchet # Date 1280954872 -7200 # Node ID a9877c14550fa142c94ceeea82aeb81cfc72042b # Parent 44d635ce6da49f63be6bfa8e0fcc712da83e7bf2 avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug) diff -r 44d635ce6da4 -r a9877c14550f src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Aug 04 21:56:17 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Aug 04 22:47:52 2010 +0200 @@ -747,11 +747,11 @@ fun gt ({kk_subset, kk_join, kk_closure, ...} : kodkod_constrs) z r1 r2 = kk_subset r1 (kk_join r2 (kk_closure (KK.Rel (suc_rel_for_atom_seq z)))) -fun constr_ord (({const = (s1, _), delta = delta1, epsilon = epsilon1, ...}, - {const = (s2, _), delta = delta2, epsilon = epsilon2, ...}) - : constr_spec * constr_spec) = - prod_ord int_ord (prod_ord int_ord string_ord) - ((delta1, (epsilon2, s1)), (delta2, (epsilon2, s2))) +fun constr_quadruple ({const = (s, T), delta, epsilon, ...} : constr_spec) = + (delta, (epsilon, (num_binder_types T, s))) +val constr_ord = + prod_ord int_ord (prod_ord int_ord (prod_ord int_ord string_ord)) + o pairself constr_quadruple fun datatype_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...}, {card = card2, self_rec = self_rec2, constrs = constr2, ...}) @@ -799,21 +799,21 @@ fun sym_break_axioms_for_constr_pair hol_ctxt binarize (kk as {kk_all, kk_or, kk_iff, kk_implies, kk_and, kk_some, kk_subset, kk_intersect, kk_join, kk_project, ...}) rel_table nfas dtypes - (({const = const1 as (_, T1), delta = delta1, epsilon = epsilon1, ...}, + (constr_ord, + ({const = const1 as (_, T1), delta = delta1, epsilon = epsilon1, ...}, {const = const2 as (_, T2), delta = delta2, epsilon = epsilon2, ...}) : constr_spec * constr_spec) = let val dataT = body_type T1 val nfa = nfas |> find_first (exists (curry (op =) dataT o fst)) |> these val rec_Ts = nfa |> map fst - val same_constr = (const1 = const2) fun rec_and_nonrec_sels (x as (_, T)) = index_seq 0 (num_sels_for_constr_type T) |> map (binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x) |> List.partition (member (op =) rec_Ts o range_type o snd) val sel_xs1 = rec_and_nonrec_sels const1 |> op @ in - if same_constr andalso null sel_xs1 then + if constr_ord = EQUAL andalso null sel_xs1 then [] else let @@ -833,7 +833,7 @@ fun filter_out_sels no_direct sel_xs = apsnd (filter_out (fn ((x, _), T) => - (same_constr andalso x = hd sel_xs) orelse + (constr_ord = EQUAL andalso x = hd sel_xs) orelse (T = dataT andalso (no_direct orelse not (member (op =) sel_xs x))))) (* FIXME: why the last disjunct above? *) @@ -844,8 +844,9 @@ in [kk_all [KK.DeclOne ((1, 0), discr_rel_expr rel_table const1), KK.DeclOne ((1, 1), discr_rel_expr rel_table const2)] - ((if same_constr then kk_implies else kk_iff) + (kk_implies (if delta2 >= epsilon1 then KK.True + else if delta1 >= epsilon2 - 1 then KK.False else gt kk z (KK.Var (1, 1)) (KK.Var (1, 0))) (kk_or (if is_nil_like_constr_type dtypes T1 then @@ -853,7 +854,8 @@ else kk_some (kk_intersect (subterms_r false sel_xs2 1) (all_ge kk z (KK.Var (1, 0))))) - (if same_constr then + (case constr_ord of + EQUAL => kk_and (lex_order_rel_expr kk dtypes (sel_quadruples2 ())) (if length rec_sel_xs2 > 1 then @@ -862,20 +864,26 @@ (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))) else KK.True) - else + | LESS => kk_all [KK.DeclOne ((1, 2), subterms_r false sel_xs1 0)] - (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))))))] + (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))) + | GREATER => KK.False)))] end end fun sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas dtypes ({constrs, ...} : datatype_spec) = - let val constrs = sort constr_ord constrs in - maps (sym_break_axioms_for_constr_pair hol_ctxt binarize kk rel_table nfas - dtypes) - ((constrs ~~ constrs) @ all_distinct_unordered_pairs_of constrs) - end + let + val constrs = sort constr_ord constrs + val constr_pairs = all_distinct_unordered_pairs_of constrs + in + map (pair EQUAL) (constrs ~~ constrs) @ + map (pair LESS) constr_pairs @ + map (pair GREATER) (map swap constr_pairs) + |> maps (sym_break_axioms_for_constr_pair hol_ctxt binarize kk rel_table + nfas dtypes) + end val min_sym_break_card = 7