# HG changeset patch # User blanchet # Date 1257857200 -3600 # Node ID bdf98e327f0b3686b5a7beda5f20308d40b8f312 # Parent e1e77265fb1d41b4df65e8f5727a22c429969cd8 fixed soundness bug in Nitpick related to sets of sets; (detected thanks to the TPTP) diff -r e1e77265fb1d -r bdf98e327f0b src/HOL/Tools/Nitpick/HISTORY --- a/src/HOL/Tools/Nitpick/HISTORY Thu Nov 05 19:06:35 2009 +0100 +++ b/src/HOL/Tools/Nitpick/HISTORY Tue Nov 10 13:46:40 2009 +0100 @@ -10,6 +10,7 @@ * Optimized Kodkod encoding of datatypes whose constructors don't appear in the formula to falsify * Added support for codatatype view of datatypes + * Fixed soundness bug related to sets of sets * Fixed monotonicity check * Fixed error in display of uncurried constants * Speeded up scope enumeration diff -r e1e77265fb1d -r bdf98e327f0b src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Nov 05 19:06:35 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Nov 10 13:46:40 2009 +0100 @@ -580,9 +580,9 @@ val schema = atom_schema_of_rep R1 val r1 = fold1 (#kk_product kk) (unary_var_seq ~1 (length schema)) |> rel_expr_from_rel_expr kk R1' R1 + val kk_xeq = (if is_one_rep R1' then #kk_subset else #kk_rel_eq) kk in - #kk_comprehension kk (decls_for_atom_schema ~1 schema) - (#kk_subset kk r1 r) + #kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r) end | Func (Unit, (Atom (2, j0))) => #kk_rel_if kk (#kk_rel_eq kk r (Kodkod.Atom (j0 + 1))) @@ -616,7 +616,7 @@ val r3 = atom_from_formula kk j0 (#kk_subset kk r1 r) in #kk_comprehension kk (decls_for_atom_schema ~1 (schema @ [x])) - (#kk_rel_eq kk r2 r3) + (#kk_subset kk r2 r3) end end | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", @@ -641,10 +641,11 @@ (length ran_schema)) |> rel_expr_from_rel_expr kk R2' R2 val app = kk_n_fold_join kk true R1' R2' dom_prod r + val kk_xeq = (if is_one_rep R2' then #kk_subset else #kk_rel_eq) kk in #kk_comprehension kk (decls_for_atom_schema ~1 (dom_schema @ ran_schema)) - (#kk_subset kk ran_prod app) + (kk_xeq ran_prod app) end | _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", [old_R, Func (R1, R2)])