1.1 --- a/src/HOL/Tools/Nitpick/HISTORY Fri May 14 12:01:16 2010 +0200
1.2 +++ b/src/HOL/Tools/Nitpick/HISTORY Fri May 14 14:14:22 2010 +0200
1.3 @@ -14,6 +14,7 @@
1.4 * Fixed soundness bugs related to "destroy_constrs" optimization and record
1.5 getters
1.6 * Fixed soundness bug related to higher-order constructors
1.7 + * Improved precision of set constructs
1.8 * Added cache to speed up repeated Kodkod invocations on the same problems
1.9 * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
1.10 "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Fri May 14 12:01:16 2010 +0200
2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri May 14 14:14:22 2010 +0200
2.3 @@ -840,7 +840,7 @@
2.4 \fragment." ^
2.5 (if exists (not o KK.is_problem_trivially_false o fst)
2.6 unsound_problems then
2.7 - " Only potential counterexamples may be found."
2.8 + " Only potential " ^ das_wort_model ^ "s may be found."
2.9 else
2.10 ""))
2.11 else
3.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri May 14 12:01:16 2010 +0200
3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri May 14 14:14:22 2010 +0200
3.3 @@ -395,9 +395,9 @@
3.4 | ord => ord)
3.5 | name_ord (u1, u2) = raise NUT ("Nitpick_Nut.name_ord", [u1, u2])
3.6
3.7 -fun num_occs_in_nut needle_u stack_u =
3.8 +fun num_occurrences_in_nut needle_u stack_u =
3.9 fold_nut (fn u => if u = needle_u then Integer.add 1 else I) stack_u 0
3.10 -val is_subterm_of = not_equal 0 oo num_occs_in_nut
3.11 +val is_subnut_of = not_equal 0 oo num_occurrences_in_nut
3.12
3.13 fun substitute_in_nut needle_u needle_u' =
3.14 map_nut (fn u => if u = needle_u then needle_u' else u)
3.15 @@ -472,12 +472,7 @@
3.16 let
3.17 val bound_u = BoundName (length Ts, T, Any, s)
3.18 val body_u = sub_abs s T t1
3.19 - in
3.20 - if is_subterm_of bound_u body_u then
3.21 - Op2 (quant, bool_T, Any, bound_u, body_u)
3.22 - else
3.23 - body_u
3.24 - end
3.25 + in Op2 (quant, bool_T, Any, bound_u, body_u) end
3.26 fun do_apply t0 ts =
3.27 let
3.28 val (ts', t2) = split_last ts
3.29 @@ -749,7 +744,7 @@
3.30 end
3.31
3.32 (* A nut is said to be constructive if whenever it evaluates to unknown in our
3.33 - three-valued logic, it would evaluate to a unrepresentable value ("Unrep")
3.34 + three-valued logic, it would evaluate to an unrepresentable value ("Unrep")
3.35 according to the HOL semantics. For example, "Suc n" is constructive if "n"
3.36 is representable or "Unrep", because unknown implies "Unrep". *)
3.37 fun is_constructive u =
3.38 @@ -776,9 +771,16 @@
3.39 case u of
3.40 FreeName _ => true
3.41 | Op1 (SingletonSet, _, _, _) => true
3.42 + | Op1 (Converse, _, _, u1) => is_fully_representable_set u1
3.43 | Op2 (oper, _, _, u1, u2) =>
3.44 - member (op =) [Union, SetDifference, Intersect] oper andalso
3.45 - forall is_fully_representable_set [u1, u2]
3.46 + if oper = Union orelse oper = SetDifference orelse oper = Intersect then
3.47 + forall is_fully_representable_set [u1, u2]
3.48 + else if oper = Apply then
3.49 + case u1 of
3.50 + ConstName (s, _, _) => is_sel_like_and_no_discr s
3.51 + | _ => false
3.52 + else
3.53 + false
3.54 | _ => false
3.55
3.56 fun s_op1 oper T R u1 =
3.57 @@ -792,7 +794,9 @@
3.58 |> optimize_unit
3.59 fun s_op2 oper T R u1 u2 =
3.60 ((case oper of
3.61 - Or =>
3.62 + All => if is_subnut_of u1 u2 then Op2 (All, T, R, u1, u2) else u2
3.63 + | Exist => if is_subnut_of u1 u2 then Op2 (Exist, T, R, u1, u2) else u2
3.64 + | Or =>
3.65 if exists (is_Cst True) [u1, u2] then Cst (True, T, unopt_rep R)
3.66 else if is_Cst False u1 then u2
3.67 else if is_Cst False u2 then u1
3.68 @@ -816,11 +820,11 @@
3.69 if is_Cst Unrep u1 then
3.70 Cst (Unrep, T, R)
3.71 else if is_Cst Unrep u2 then
3.72 - if is_constructive u1 then
3.73 - Cst (Unrep, T, R)
3.74 - else if is_boolean_type T then
3.75 + if is_boolean_type T then
3.76 if is_fully_representable_set u1 then Cst (False, T, Formula Neut)
3.77 else unknown_boolean T R
3.78 + else if is_constructive u1 then
3.79 + Cst (Unrep, T, R)
3.80 else case u1 of
3.81 Op2 (Apply, _, _, ConstName (@{const_name List.append}, _, _), _) =>
3.82 Cst (Unrep, T, R)
3.83 @@ -833,7 +837,7 @@
3.84 fun s_op3 oper T R u1 u2 u3 =
3.85 ((case oper of
3.86 Let =>
3.87 - if inline_nut u2 orelse num_occs_in_nut u1 u3 < 2 then
3.88 + if inline_nut u2 orelse num_occurrences_in_nut u1 u3 < 2 then
3.89 substitute_in_nut u1 u2 u3
3.90 else
3.91 raise SAME ()
3.92 @@ -844,17 +848,6 @@
3.93 (if exists (is_Cst Unrep) us then Cst (Unrep, T, R) else Tuple (T, R, us))
3.94 |> optimize_unit
3.95
3.96 -fun optimize_nut u =
3.97 - case u of
3.98 - Op1 (oper, T, R, u1) => s_op1 oper T R (optimize_nut u1)
3.99 - | Op2 (oper, T, R, u1, u2) =>
3.100 - s_op2 oper T R (optimize_nut u1) (optimize_nut u2)
3.101 - | Op3 (oper, T, R, u1, u2, u3) =>
3.102 - s_op3 oper T R (optimize_nut u1) (optimize_nut u2) (optimize_nut u3)
3.103 - | Tuple (T, R, us) => s_tuple T R (map optimize_nut us)
3.104 - | Construct (us', T, R, us) => Construct (us', T, R, map optimize_nut us)
3.105 - | _ => optimize_unit u
3.106 -
3.107 fun untuple f (Tuple (_, _, us)) = maps (untuple f) us
3.108 | untuple f u = if rep_of u = Unit then [] else [f u]
3.109
3.110 @@ -1033,7 +1026,7 @@
3.111 Op2 (And, bool_T, Any,
3.112 case u2 of
3.113 Op2 (Lambda, _, _, u21, u22) =>
3.114 - if num_occs_in_nut u21 u22 = 0 then
3.115 + if num_occurrences_in_nut u21 u22 = 0 then
3.116 u22
3.117 else
3.118 Op2 (Apply, bool_T, Any, u2, x_u)
3.119 @@ -1075,13 +1068,12 @@
3.120 if is_opt_rep (rep_of u2') orelse
3.121 (range_type T = bool_T andalso
3.122 not (is_Cst False (unrepify_nut_in_nut table false Neut
3.123 - u1 u2
3.124 - |> optimize_nut))) then
3.125 + u1 u2))) then
3.126 opt_rep ofs T R
3.127 else
3.128 unopt_rep R
3.129 in s_op2 Lambda T R u1' u2' end
3.130 - | _ => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u]))
3.131 + | _ => raise NUT ("Nitpick_Nut.choose_reps_in_nut.aux", [u]))
3.132 | Op2 (oper, T, _, u1, u2) =>
3.133 if oper = All orelse oper = Exist then
3.134 let