# HG changeset patch # User blanchet # Date 1273839262 -7200 # Node ID 0010f08e288e8c39b8edf1e849f1c72db04e0c2a # Parent 55b97cb3806e5875f9459081b00e80cb76537429 improve precision of set constructs in Nitpick diff -r 55b97cb3806e -r 0010f08e288e src/HOL/Tools/Nitpick/HISTORY --- a/src/HOL/Tools/Nitpick/HISTORY Fri May 14 12:01:16 2010 +0200 +++ b/src/HOL/Tools/Nitpick/HISTORY Fri May 14 14:14:22 2010 +0200 @@ -14,6 +14,7 @@ * Fixed soundness bugs related to "destroy_constrs" optimization and record getters * Fixed soundness bug related to higher-order constructors + * Improved precision of set constructs * Added cache to speed up repeated Kodkod invocations on the same problems * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light" diff -r 55b97cb3806e -r 0010f08e288e src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Fri May 14 12:01:16 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri May 14 14:14:22 2010 +0200 @@ -840,7 +840,7 @@ \fragment." ^ (if exists (not o KK.is_problem_trivially_false o fst) unsound_problems then - " Only potential counterexamples may be found." + " Only potential " ^ das_wort_model ^ "s may be found." else "")) else diff -r 55b97cb3806e -r 0010f08e288e src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri May 14 12:01:16 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri May 14 14:14:22 2010 +0200 @@ -395,9 +395,9 @@ | ord => ord) | name_ord (u1, u2) = raise NUT ("Nitpick_Nut.name_ord", [u1, u2]) -fun num_occs_in_nut needle_u stack_u = +fun num_occurrences_in_nut needle_u stack_u = fold_nut (fn u => if u = needle_u then Integer.add 1 else I) stack_u 0 -val is_subterm_of = not_equal 0 oo num_occs_in_nut +val is_subnut_of = not_equal 0 oo num_occurrences_in_nut fun substitute_in_nut needle_u needle_u' = map_nut (fn u => if u = needle_u then needle_u' else u) @@ -472,12 +472,7 @@ let val bound_u = BoundName (length Ts, T, Any, s) val body_u = sub_abs s T t1 - in - if is_subterm_of bound_u body_u then - Op2 (quant, bool_T, Any, bound_u, body_u) - else - body_u - end + in Op2 (quant, bool_T, Any, bound_u, body_u) end fun do_apply t0 ts = let val (ts', t2) = split_last ts @@ -749,7 +744,7 @@ end (* A nut is said to be constructive if whenever it evaluates to unknown in our - three-valued logic, it would evaluate to a unrepresentable value ("Unrep") + three-valued logic, it would evaluate to an unrepresentable value ("Unrep") according to the HOL semantics. For example, "Suc n" is constructive if "n" is representable or "Unrep", because unknown implies "Unrep". *) fun is_constructive u = @@ -776,9 +771,16 @@ case u of FreeName _ => true | Op1 (SingletonSet, _, _, _) => true + | Op1 (Converse, _, _, u1) => is_fully_representable_set u1 | Op2 (oper, _, _, u1, u2) => - member (op =) [Union, SetDifference, Intersect] oper andalso - forall is_fully_representable_set [u1, u2] + if oper = Union orelse oper = SetDifference orelse oper = Intersect then + forall is_fully_representable_set [u1, u2] + else if oper = Apply then + case u1 of + ConstName (s, _, _) => is_sel_like_and_no_discr s + | _ => false + else + false | _ => false fun s_op1 oper T R u1 = @@ -792,7 +794,9 @@ |> optimize_unit fun s_op2 oper T R u1 u2 = ((case oper of - Or => + All => if is_subnut_of u1 u2 then Op2 (All, T, R, u1, u2) else u2 + | Exist => if is_subnut_of u1 u2 then Op2 (Exist, T, R, u1, u2) else u2 + | Or => if exists (is_Cst True) [u1, u2] then Cst (True, T, unopt_rep R) else if is_Cst False u1 then u2 else if is_Cst False u2 then u1 @@ -816,11 +820,11 @@ if is_Cst Unrep u1 then Cst (Unrep, T, R) else if is_Cst Unrep u2 then - if is_constructive u1 then - Cst (Unrep, T, R) - else if is_boolean_type T then + if is_boolean_type T then if is_fully_representable_set u1 then Cst (False, T, Formula Neut) else unknown_boolean T R + else if is_constructive u1 then + Cst (Unrep, T, R) else case u1 of Op2 (Apply, _, _, ConstName (@{const_name List.append}, _, _), _) => Cst (Unrep, T, R) @@ -833,7 +837,7 @@ fun s_op3 oper T R u1 u2 u3 = ((case oper of Let => - if inline_nut u2 orelse num_occs_in_nut u1 u3 < 2 then + if inline_nut u2 orelse num_occurrences_in_nut u1 u3 < 2 then substitute_in_nut u1 u2 u3 else raise SAME () @@ -844,17 +848,6 @@ (if exists (is_Cst Unrep) us then Cst (Unrep, T, R) else Tuple (T, R, us)) |> optimize_unit -fun optimize_nut u = - case u of - Op1 (oper, T, R, u1) => s_op1 oper T R (optimize_nut u1) - | Op2 (oper, T, R, u1, u2) => - s_op2 oper T R (optimize_nut u1) (optimize_nut u2) - | Op3 (oper, T, R, u1, u2, u3) => - s_op3 oper T R (optimize_nut u1) (optimize_nut u2) (optimize_nut u3) - | Tuple (T, R, us) => s_tuple T R (map optimize_nut us) - | Construct (us', T, R, us) => Construct (us', T, R, map optimize_nut us) - | _ => optimize_unit u - fun untuple f (Tuple (_, _, us)) = maps (untuple f) us | untuple f u = if rep_of u = Unit then [] else [f u] @@ -1033,7 +1026,7 @@ Op2 (And, bool_T, Any, case u2 of Op2 (Lambda, _, _, u21, u22) => - if num_occs_in_nut u21 u22 = 0 then + if num_occurrences_in_nut u21 u22 = 0 then u22 else Op2 (Apply, bool_T, Any, u2, x_u) @@ -1075,13 +1068,12 @@ if is_opt_rep (rep_of u2') orelse (range_type T = bool_T andalso not (is_Cst False (unrepify_nut_in_nut table false Neut - u1 u2 - |> optimize_nut))) then + u1 u2))) then opt_rep ofs T R else unopt_rep R in s_op2 Lambda T R u1' u2' end - | _ => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u])) + | _ => raise NUT ("Nitpick_Nut.choose_reps_in_nut.aux", [u])) | Op2 (oper, T, _, u1, u2) => if oper = All orelse oper = Exist then let