1.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Dec 14 16:48:49 2009 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Dec 17 15:22:11 2009 +0100
1.3 @@ -19,10 +19,12 @@
1.4
1.5 val univ_card :
1.6 int -> int -> int -> Kodkod.bound list -> Kodkod.formula -> int
1.7 + val check_bits : int -> Kodkod.formula -> unit
1.8 val check_arity : int -> int -> unit
1.9 val kk_tuple : bool -> int -> int list -> Kodkod.tuple
1.10 val tuple_set_from_atom_schema : (int * int) list -> Kodkod.tuple_set
1.11 val sequential_int_bounds : int -> Kodkod.int_bound list
1.12 + val pow_of_two_int_bounds : int -> int -> int -> Kodkod.int_bound list
1.13 val bounds_for_built_in_rels_in_formula :
1.14 bool -> int -> int -> int -> int -> Kodkod.formula -> Kodkod.bound list
1.15 val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound
1.16 @@ -31,10 +33,10 @@
1.17 val merge_bounds : Kodkod.bound list -> Kodkod.bound list
1.18 val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
1.19 val declarative_axioms_for_datatypes :
1.20 - extended_context -> int Typtab.table -> kodkod_constrs
1.21 + extended_context -> int -> int Typtab.table -> kodkod_constrs
1.22 -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
1.23 val kodkod_formula_from_nut :
1.24 - int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
1.25 + int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
1.26 end;
1.27
1.28 structure Nitpick_Kodkod : NITPICK_KODKOD =
1.29 @@ -80,18 +82,28 @@
1.30 |> Kodkod.fold_formula expr_F formula
1.31 in Int.max (main_j0 + fold Integer.max [2, nat_card, int_card] 0, card) end
1.32
1.33 -(* Proof.context -> bool -> string -> typ -> rep -> string *)
1.34 -fun bound_comment ctxt debug nick T R =
1.35 - short_name nick ^
1.36 - (if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T)
1.37 - else "") ^ " : " ^ string_for_rep R
1.38 +(* int -> Kodkod.formula -> unit *)
1.39 +fun check_bits bits formula =
1.40 + let
1.41 + (* Kodkod.int_expr -> unit -> unit *)
1.42 + fun int_expr_func (Kodkod.Num k) () =
1.43 + if is_twos_complement_representable bits k then
1.44 + ()
1.45 + else
1.46 + raise TOO_SMALL ("Nitpick_Kodkod.check_bits",
1.47 + "\"bits\" value " ^ string_of_int bits ^
1.48 + " too small for problem")
1.49 + | int_expr_func _ () = ()
1.50 + val expr_F = {formula_func = K I, rel_expr_func = K I,
1.51 + int_expr_func = int_expr_func}
1.52 + in Kodkod.fold_formula expr_F formula () end
1.53
1.54 (* int -> int -> unit *)
1.55 fun check_arity univ_card n =
1.56 if n > Kodkod.max_arity univ_card then
1.57 - raise LIMIT ("Nitpick_Kodkod.check_arity",
1.58 - "arity " ^ string_of_int n ^ " too large for universe of \
1.59 - \cardinality " ^ string_of_int univ_card)
1.60 + raise TOO_LARGE ("Nitpick_Kodkod.check_arity",
1.61 + "arity " ^ string_of_int n ^ " too large for universe of \
1.62 + \cardinality " ^ string_of_int univ_card)
1.63 else
1.64 ()
1.65
1.66 @@ -109,20 +121,34 @@
1.67 (* rep -> Kodkod.tuple_set *)
1.68 val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep
1.69
1.70 +(* int -> Kodkod.tuple_set *)
1.71 +val single_atom = Kodkod.TupleSet o single o Kodkod.Tuple o single
1.72 (* int -> Kodkod.int_bound list *)
1.73 -fun sequential_int_bounds n =
1.74 - [(NONE, map (Kodkod.TupleSet o single o Kodkod.Tuple o single)
1.75 - (index_seq 0 n))]
1.76 +fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))]
1.77 +(* int -> int -> Kodkod.int_bound list *)
1.78 +fun pow_of_two_int_bounds bits j0 univ_card =
1.79 + let
1.80 + (* int -> int -> int -> Kodkod.int_bound list *)
1.81 + fun aux 0 _ _ = []
1.82 + | aux 1 pow_of_two j =
1.83 + if j < univ_card then [(SOME (~ pow_of_two), [single_atom j])] else []
1.84 + | aux iter pow_of_two j =
1.85 + (SOME pow_of_two, [single_atom j]) ::
1.86 + aux (iter - 1) (2 * pow_of_two) (j + 1)
1.87 + in aux (bits + 1) 1 j0 end
1.88
1.89 (* Kodkod.formula -> Kodkod.n_ary_index list *)
1.90 fun built_in_rels_in_formula formula =
1.91 let
1.92 (* Kodkod.rel_expr -> Kodkod.n_ary_index list -> Kodkod.n_ary_index list *)
1.93 - fun rel_expr_func (Kodkod.Rel (n, j)) rels =
1.94 - (case AList.lookup (op =) (#rels initial_pool) n of
1.95 - SOME k => (j < k ? insert (op =) (n, j)) rels
1.96 - | NONE => rels)
1.97 - | rel_expr_func _ rels = rels
1.98 + fun rel_expr_func (r as Kodkod.Rel (x as (n, j))) =
1.99 + if x = unsigned_bit_word_sel_rel orelse x = signed_bit_word_sel_rel then
1.100 + I
1.101 + else
1.102 + (case AList.lookup (op =) (#rels initial_pool) n of
1.103 + SOME k => j < k ? insert (op =) x
1.104 + | NONE => I)
1.105 + | rel_expr_func _ = I
1.106 val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func,
1.107 int_expr_func = K I}
1.108 in Kodkod.fold_formula expr_F formula [] end
1.109 @@ -132,8 +158,8 @@
1.110 (* int -> unit *)
1.111 fun check_table_size k =
1.112 if k > max_table_size then
1.113 - raise LIMIT ("Nitpick_Kodkod.check_table_size",
1.114 - "precomputed table too large (" ^ string_of_int k ^ ")")
1.115 + raise TOO_LARGE ("Nitpick_Kodkod.check_table_size",
1.116 + "precomputed table too large (" ^ string_of_int k ^ ")")
1.117 else
1.118 ()
1.119
1.120 @@ -205,43 +231,39 @@
1.121 -> string * bool * Kodkod.tuple list *)
1.122 fun tabulate_built_in_rel debug univ_card nat_card int_card j0 (x as (n, _)) =
1.123 (check_arity univ_card n;
1.124 - if Kodkod.Rel x = not3_rel then
1.125 + if x = not3_rel then
1.126 ("not3", tabulate_func1 debug univ_card (2, j0) (curry (op -) 1))
1.127 - else if Kodkod.Rel x = suc_rel then
1.128 + else if x = suc_rel then
1.129 ("suc", tabulate_func1 debug univ_card (univ_card - j0 - 1, j0)
1.130 (Integer.add 1))
1.131 - else if Kodkod.Rel x = nat_add_rel then
1.132 + else if x = nat_add_rel then
1.133 ("nat_add", tabulate_nat_op2 debug univ_card (nat_card, j0) (op +))
1.134 - else if Kodkod.Rel x = int_add_rel then
1.135 + else if x = int_add_rel then
1.136 ("int_add", tabulate_int_op2 debug univ_card (int_card, j0) (op +))
1.137 - else if Kodkod.Rel x = nat_subtract_rel then
1.138 + else if x = nat_subtract_rel then
1.139 ("nat_subtract",
1.140 tabulate_op2 debug univ_card (nat_card, j0) j0 (uncurry nat_minus))
1.141 - else if Kodkod.Rel x = int_subtract_rel then
1.142 + else if x = int_subtract_rel then
1.143 ("int_subtract", tabulate_int_op2 debug univ_card (int_card, j0) (op -))
1.144 - else if Kodkod.Rel x = nat_multiply_rel then
1.145 + else if x = nat_multiply_rel then
1.146 ("nat_multiply", tabulate_nat_op2 debug univ_card (nat_card, j0) (op * ))
1.147 - else if Kodkod.Rel x = int_multiply_rel then
1.148 + else if x = int_multiply_rel then
1.149 ("int_multiply", tabulate_int_op2 debug univ_card (int_card, j0) (op * ))
1.150 - else if Kodkod.Rel x = nat_divide_rel then
1.151 + else if x = nat_divide_rel then
1.152 ("nat_divide", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_div)
1.153 - else if Kodkod.Rel x = int_divide_rel then
1.154 + else if x = int_divide_rel then
1.155 ("int_divide", tabulate_int_op2 debug univ_card (int_card, j0) isa_div)
1.156 - else if Kodkod.Rel x = nat_modulo_rel then
1.157 - ("nat_modulo", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_mod)
1.158 - else if Kodkod.Rel x = int_modulo_rel then
1.159 - ("int_modulo", tabulate_int_op2 debug univ_card (int_card, j0) isa_mod)
1.160 - else if Kodkod.Rel x = nat_less_rel then
1.161 + else if x = nat_less_rel then
1.162 ("nat_less", tabulate_nat_op2 debug univ_card (nat_card, j0)
1.163 (int_for_bool o op <))
1.164 - else if Kodkod.Rel x = int_less_rel then
1.165 + else if x = int_less_rel then
1.166 ("int_less", tabulate_int_op2 debug univ_card (int_card, j0)
1.167 (int_for_bool o op <))
1.168 - else if Kodkod.Rel x = gcd_rel then
1.169 + else if x = gcd_rel then
1.170 ("gcd", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_gcd)
1.171 - else if Kodkod.Rel x = lcm_rel then
1.172 + else if x = lcm_rel then
1.173 ("lcm", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_lcm)
1.174 - else if Kodkod.Rel x = norm_frac_rel then
1.175 + else if x = norm_frac_rel then
1.176 ("norm_frac", tabulate_int_op2_2 debug univ_card (int_card, j0)
1.177 isa_norm_frac)
1.178 else
1.179 @@ -260,12 +282,18 @@
1.180 map (bound_for_built_in_rel debug univ_card nat_card int_card j0)
1.181 o built_in_rels_in_formula
1.182
1.183 +(* Proof.context -> bool -> string -> typ -> rep -> string *)
1.184 +fun bound_comment ctxt debug nick T R =
1.185 + short_name nick ^
1.186 + (if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T)
1.187 + else "") ^ " : " ^ string_for_rep R
1.188 +
1.189 (* Proof.context -> bool -> nut -> Kodkod.bound *)
1.190 fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) =
1.191 ([(x, bound_comment ctxt debug nick T R)],
1.192 if nick = @{const_name bisim_iterator_max} then
1.193 case R of
1.194 - Atom (k, j0) => [Kodkod.TupleSet [Kodkod.Tuple [k - 1 + j0]]]
1.195 + Atom (k, j0) => [single_atom (k - 1 + j0)]
1.196 | _ => raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
1.197 else
1.198 [Kodkod.TupleSet [], upper_bound_for_rep R])
1.199 @@ -369,17 +397,17 @@
1.200 else
1.201 Kodkod.True
1.202 end
1.203 -fun kk_n_ary_function kk R (r as Kodkod.Rel _) =
1.204 +fun kk_n_ary_function kk R (r as Kodkod.Rel x) =
1.205 if not (is_opt_rep R) then
1.206 - if r = suc_rel then
1.207 + if x = suc_rel then
1.208 Kodkod.False
1.209 - else if r = nat_add_rel then
1.210 + else if x = nat_add_rel then
1.211 formula_for_bool (card_of_rep (body_rep R) = 1)
1.212 - else if r = nat_multiply_rel then
1.213 + else if x = nat_multiply_rel then
1.214 formula_for_bool (card_of_rep (body_rep R) <= 2)
1.215 else
1.216 d_n_ary_function kk R r
1.217 - else if r = nat_subtract_rel then
1.218 + else if x = nat_subtract_rel then
1.219 Kodkod.True
1.220 else
1.221 d_n_ary_function kk R r
1.222 @@ -393,27 +421,27 @@
1.223
1.224 (* int -> kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr)
1.225 -> Kodkod.rel_expr -> Kodkod.rel_expr *)
1.226 -fun basic_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r =
1.227 +fun basic_rel_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r =
1.228 if inline_rel_expr r then
1.229 f r
1.230 else
1.231 let val x = (Kodkod.arity_of_rel_expr r, j) in
1.232 kk_rel_let [Kodkod.AssignRelReg (x, r)] (f (Kodkod.RelReg x))
1.233 end
1.234 -
1.235 (* kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr) -> Kodkod.rel_expr
1.236 -> Kodkod.rel_expr *)
1.237 -val single_rel_let = basic_rel_let 0
1.238 +val single_rel_rel_let = basic_rel_rel_let 0
1.239 (* kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr)
1.240 -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *)
1.241 -fun double_rel_let kk f r1 r2 =
1.242 - single_rel_let kk (fn r1 => basic_rel_let 1 kk (f r1) r2) r1
1.243 +fun double_rel_rel_let kk f r1 r2 =
1.244 + single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1
1.245 (* kodkod_constrs
1.246 -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr)
1.247 -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr
1.248 -> Kodkod.rel_expr *)
1.249 -fun triple_rel_let kk f r1 r2 r3 =
1.250 - double_rel_let kk (fn r1 => fn r2 => basic_rel_let 2 kk (f r1 r2) r3) r1 r2
1.251 +fun tripl_rel_rel_let kk f r1 r2 r3 =
1.252 + double_rel_rel_let kk
1.253 + (fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2
1.254
1.255 (* kodkod_constrs -> int -> Kodkod.formula -> Kodkod.rel_expr *)
1.256 fun atom_from_formula ({kk_rel_if, ...} : kodkod_constrs) j0 f =
1.257 @@ -469,8 +497,8 @@
1.258 if is_lone_rep old_R andalso is_lone_rep new_R
1.259 andalso card = card_of_rep new_R then
1.260 if card >= lone_rep_fallback_max_card then
1.261 - raise LIMIT ("Nitpick_Kodkod.lone_rep_fallback",
1.262 - "too high cardinality (" ^ string_of_int card ^ ")")
1.263 + raise TOO_LARGE ("Nitpick_Kodkod.lone_rep_fallback",
1.264 + "too high cardinality (" ^ string_of_int card ^ ")")
1.265 else
1.266 kk_case_switch kk old_R new_R r (all_singletons_for_rep old_R)
1.267 (all_singletons_for_rep new_R)
1.268 @@ -672,6 +700,21 @@
1.269 (* kodkod_constrs -> rep -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
1.270 and rel_expr_to_func kk R1 R2 = rel_expr_from_rel_expr kk (Func (R1, R2))
1.271
1.272 +(* kodkod_constrs -> typ -> Kodkod.rel_expr -> Kodkod.rel_expr *)
1.273 +fun bit_set_from_atom ({kk_join, ...} : kodkod_constrs) T r =
1.274 + kk_join r (Kodkod.Rel (if T = @{typ "unsigned_bit word"} then
1.275 + unsigned_bit_word_sel_rel
1.276 + else
1.277 + signed_bit_word_sel_rel))
1.278 +(* kodkod_constrs -> typ -> Kodkod.rel_expr -> Kodkod.int_expr *)
1.279 +val int_expr_from_atom = Kodkod.SetSum ooo bit_set_from_atom
1.280 +(* kodkod_constrs -> typ -> rep -> Kodkod.int_expr -> Kodkod.rel_expr *)
1.281 +fun atom_from_int_expr (kk as {kk_rel_eq, kk_comprehension, ...}
1.282 + : kodkod_constrs) T R i =
1.283 + kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R))
1.284 + (kk_rel_eq (bit_set_from_atom kk T (Kodkod.Var (1, ~1)))
1.285 + (Kodkod.Bits i))
1.286 +
1.287 (* kodkod_constrs -> nut -> Kodkod.formula *)
1.288 fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) =
1.289 kk_n_ary_function kk (R |> nick = @{const_name List.set} ? unopt_rep)
1.290 @@ -804,9 +847,9 @@
1.291 (kk_no r'))
1.292 end
1.293 end
1.294 -(* extended_context -> int -> kodkod_constrs -> nut NameTable.table
1.295 +(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
1.296 -> constr_spec -> Kodkod.formula list *)
1.297 -fun sel_axioms_for_constr ext_ctxt j0 kk rel_table
1.298 +fun sel_axioms_for_constr ext_ctxt bits j0 kk rel_table
1.299 (constr as {const, delta, epsilon, explicit_max, ...}) =
1.300 let
1.301 val honors_explicit_max =
1.302 @@ -818,19 +861,25 @@
1.303 let
1.304 val ran_r = discr_rel_expr rel_table const
1.305 val max_axiom =
1.306 - if honors_explicit_max then Kodkod.True
1.307 - else Kodkod.LE (Kodkod.Cardinality ran_r, Kodkod.Num explicit_max)
1.308 + if honors_explicit_max then
1.309 + Kodkod.True
1.310 + else if is_twos_complement_representable bits (epsilon - delta) then
1.311 + Kodkod.LE (Kodkod.Cardinality ran_r, Kodkod.Num explicit_max)
1.312 + else
1.313 + raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",
1.314 + "\"bits\" value " ^ string_of_int bits ^
1.315 + " too small for \"max\"")
1.316 in
1.317 max_axiom ::
1.318 map (sel_axiom_for_sel ext_ctxt j0 kk rel_table ran_r constr)
1.319 (index_seq 0 (num_sels_for_constr_type (snd const)))
1.320 end
1.321 end
1.322 -(* extended_context -> int -> kodkod_constrs -> nut NameTable.table
1.323 +(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
1.324 -> dtype_spec -> Kodkod.formula list *)
1.325 -fun sel_axioms_for_datatype ext_ctxt j0 kk rel_table
1.326 +fun sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table
1.327 ({constrs, ...} : dtype_spec) =
1.328 - maps (sel_axioms_for_constr ext_ctxt j0 kk rel_table) constrs
1.329 + maps (sel_axioms_for_constr ext_ctxt bits j0 kk rel_table) constrs
1.330
1.331 (* extended_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
1.332 -> Kodkod.formula list *)
1.333 @@ -881,24 +930,25 @@
1.334 kk_disjoint_sets kk rs]
1.335 end
1.336
1.337 -(* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
1.338 - -> dtype_spec -> Kodkod.formula list *)
1.339 -fun other_axioms_for_datatype _ _ _ _ {shallow = true, ...} = []
1.340 - | other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =
1.341 +(* extended_context -> int -> int Typtab.table -> kodkod_constrs
1.342 + -> nut NameTable.table -> dtype_spec -> Kodkod.formula list *)
1.343 +fun other_axioms_for_datatype _ _ _ _ _ {shallow = true, ...} = []
1.344 + | other_axioms_for_datatype ext_ctxt bits ofs kk rel_table
1.345 + (dtype as {typ, ...}) =
1.346 let val j0 = offset_of_type ofs typ in
1.347 - sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @
1.348 + sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table dtype @
1.349 uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
1.350 partition_axioms_for_datatype j0 kk rel_table dtype
1.351 end
1.352
1.353 -(* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
1.354 - -> dtype_spec list -> Kodkod.formula list *)
1.355 -fun declarative_axioms_for_datatypes ext_ctxt ofs kk rel_table dtypes =
1.356 +(* extended_context -> int -> int Typtab.table -> kodkod_constrs
1.357 + -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list *)
1.358 +fun declarative_axioms_for_datatypes ext_ctxt bits ofs kk rel_table dtypes =
1.359 acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes @
1.360 - maps (other_axioms_for_datatype ext_ctxt ofs kk rel_table) dtypes
1.361 + maps (other_axioms_for_datatype ext_ctxt bits ofs kk rel_table) dtypes
1.362
1.363 -(* int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula *)
1.364 -fun kodkod_formula_from_nut ofs liberal
1.365 +(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula *)
1.366 +fun kodkod_formula_from_nut bits ofs liberal
1.367 (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
1.368 kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, kk_one,
1.369 kk_some, kk_rel_let, kk_rel_if, kk_union, kk_difference,
1.370 @@ -924,12 +974,12 @@
1.371 fun kk_notimplies f1 f2 = kk_and f1 (kk_not f2)
1.372 (* Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *)
1.373 val kk_or3 =
1.374 - double_rel_let kk
1.375 + double_rel_rel_let kk
1.376 (fn r1 => fn r2 =>
1.377 kk_rel_if (kk_subset true_atom (kk_union r1 r2)) true_atom
1.378 (kk_intersect r1 r2))
1.379 val kk_and3 =
1.380 - double_rel_let kk
1.381 + double_rel_rel_let kk
1.382 (fn r1 => fn r2 =>
1.383 kk_rel_if (kk_subset false_atom (kk_union r1 r2)) false_atom
1.384 (kk_intersect r1 r2))
1.385 @@ -1153,38 +1203,98 @@
1.386 | Cst (Iden, T, Func (Atom (1, j0), Formula Neut)) => Kodkod.Atom j0
1.387 | Cst (Iden, T as Type ("fun", [T1, _]), R as Func (R1, _)) =>
1.388 to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut)))
1.389 - | Cst (Num j, @{typ int}, R) =>
1.390 - (case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of
1.391 + | Cst (Num j, T, R) =>
1.392 + if is_word_type T then
1.393 + atom_from_int_expr kk T R (Kodkod.Num j)
1.394 + else if T = int_T then
1.395 + case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of
1.396 ~1 => if is_opt_rep R then Kodkod.None
1.397 else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])
1.398 - | j' => Kodkod.Atom j')
1.399 - | Cst (Num j, T, R) =>
1.400 - if j < card_of_rep R then Kodkod.Atom (j + offset_of_type ofs T)
1.401 - else if is_opt_rep R then Kodkod.None
1.402 - else raise NUT ("Nitpick_Kodkod.to_r", [u])
1.403 + | j' => Kodkod.Atom j'
1.404 + else
1.405 + if j < card_of_rep R then Kodkod.Atom (j + offset_of_type ofs T)
1.406 + else if is_opt_rep R then Kodkod.None
1.407 + else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])
1.408 | Cst (Unknown, _, R) => empty_rel_for_rep R
1.409 | Cst (Unrep, _, R) => empty_rel_for_rep R
1.410 | Cst (Suc, T, Func (Atom x, _)) =>
1.411 - if domain_type T <> nat_T then suc_rel
1.412 - else kk_intersect suc_rel (kk_product Kodkod.Univ (Kodkod.AtomSeq x))
1.413 - | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => nat_add_rel
1.414 - | Cst (Add, Type ("fun", [@{typ int}, _]), _) => int_add_rel
1.415 - | Cst (Subtract, Type ("fun", [@{typ nat}, _]), _) => nat_subtract_rel
1.416 - | Cst (Subtract, Type ("fun", [@{typ int}, _]), _) => int_subtract_rel
1.417 - | Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) => nat_multiply_rel
1.418 - | Cst (Multiply, Type ("fun", [@{typ int}, _]), _) => int_multiply_rel
1.419 - | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) => nat_divide_rel
1.420 - | Cst (Divide, Type ("fun", [@{typ int}, _]), _) => int_divide_rel
1.421 - | Cst (Modulo, Type ("fun", [@{typ nat}, _]), _) => nat_modulo_rel
1.422 - | Cst (Modulo, Type ("fun", [@{typ int}, _]), _) => int_modulo_rel
1.423 - | Cst (Gcd, _, _) => gcd_rel
1.424 - | Cst (Lcm, _, _) => lcm_rel
1.425 + if domain_type T <> nat_T then
1.426 + Kodkod.Rel suc_rel
1.427 + else
1.428 + kk_intersect (Kodkod.Rel suc_rel)
1.429 + (kk_product Kodkod.Univ (Kodkod.AtomSeq x))
1.430 + | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => Kodkod.Rel nat_add_rel
1.431 + | Cst (Add, Type ("fun", [@{typ int}, _]), _) => Kodkod.Rel int_add_rel
1.432 + | Cst (Add, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
1.433 + to_bit_word_binary_op T R NONE (SOME (curry Kodkod.Add))
1.434 + | Cst (Add, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
1.435 + to_bit_word_binary_op T R
1.436 + (SOME (fn i1 => fn i2 => fn i3 =>
1.437 + kk_implies (Kodkod.LE (Kodkod.Num 0, Kodkod.BitXor (i1, i2)))
1.438 + (Kodkod.LE (Kodkod.Num 0, Kodkod.BitXor (i2, i3)))))
1.439 + (SOME (curry Kodkod.Add))
1.440 + | Cst (Subtract, Type ("fun", [@{typ nat}, _]), _) =>
1.441 + Kodkod.Rel nat_subtract_rel
1.442 + | Cst (Subtract, Type ("fun", [@{typ int}, _]), _) =>
1.443 + Kodkod.Rel int_subtract_rel
1.444 + | Cst (Subtract, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
1.445 + to_bit_word_binary_op T R NONE
1.446 + (SOME (fn i1 => fn i2 =>
1.447 + Kodkod.IntIf (Kodkod.LE (i1, i2), Kodkod.Num 0,
1.448 + Kodkod.Sub (i1, i2))))
1.449 + | Cst (Subtract, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
1.450 + to_bit_word_binary_op T R
1.451 + (SOME (fn i1 => fn i2 => fn i3 =>
1.452 + kk_implies (Kodkod.LT (Kodkod.BitXor (i1, i2), Kodkod.Num 0))
1.453 + (Kodkod.LT (Kodkod.BitXor (i2, i3), Kodkod.Num 0))))
1.454 + (SOME (curry Kodkod.Sub))
1.455 + | Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) =>
1.456 + Kodkod.Rel nat_multiply_rel
1.457 + | Cst (Multiply, Type ("fun", [@{typ int}, _]), _) =>
1.458 + Kodkod.Rel int_multiply_rel
1.459 + | Cst (Multiply,
1.460 + T as Type ("fun", [Type (@{type_name word}, [bit_T]), _]), R) =>
1.461 + to_bit_word_binary_op T R
1.462 + (SOME (fn i1 => fn i2 => fn i3 =>
1.463 + kk_or (Kodkod.IntEq (i2, Kodkod.Num 0))
1.464 + (Kodkod.IntEq (Kodkod.Div (i3, i2), i1)
1.465 + |> bit_T = @{typ signed_bit}
1.466 + ? kk_and (Kodkod.LE (Kodkod.Num 0,
1.467 + foldl1 Kodkod.BitAnd [i1, i2, i3])))))
1.468 + (SOME (curry Kodkod.Mult))
1.469 + | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) =>
1.470 + Kodkod.Rel nat_divide_rel
1.471 + | Cst (Divide, Type ("fun", [@{typ int}, _]), _) =>
1.472 + Kodkod.Rel int_divide_rel
1.473 + | Cst (Divide, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
1.474 + to_bit_word_binary_op T R NONE
1.475 + (SOME (fn i1 => fn i2 =>
1.476 + Kodkod.IntIf (Kodkod.IntEq (i2, Kodkod.Num 0),
1.477 + Kodkod.Num 0, Kodkod.Div (i1, i2))))
1.478 + | Cst (Divide, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
1.479 + to_bit_word_binary_op T R
1.480 + (SOME (fn i1 => fn i2 => fn i3 =>
1.481 + Kodkod.LE (Kodkod.Num 0, foldl1 Kodkod.BitAnd [i1, i2, i3])))
1.482 + (SOME (fn i1 => fn i2 =>
1.483 + Kodkod.IntIf (kk_and (Kodkod.LT (i1, Kodkod.Num 0))
1.484 + (Kodkod.LT (Kodkod.Num 0, i2)),
1.485 + Kodkod.Sub (Kodkod.Div (Kodkod.Add (i1, Kodkod.Num 1), i2),
1.486 + Kodkod.Num 1),
1.487 + Kodkod.IntIf (kk_and (Kodkod.LT (Kodkod.Num 0, i1))
1.488 + (Kodkod.LT (i2, Kodkod.Num 0)),
1.489 + Kodkod.Sub (Kodkod.Div (Kodkod.Sub (i1, Kodkod.Num 1),
1.490 + i2), Kodkod.Num 1),
1.491 + Kodkod.IntIf (Kodkod.IntEq (i2, Kodkod.Num 0),
1.492 + Kodkod.Num 0, Kodkod.Div (i1, i2))))))
1.493 + | Cst (Gcd, _, _) => Kodkod.Rel gcd_rel
1.494 + | Cst (Lcm, _, _) => Kodkod.Rel lcm_rel
1.495 | Cst (Fracs, _, Func (Atom (1, _), _)) => Kodkod.None
1.496 | Cst (Fracs, _, Func (Struct _, _)) =>
1.497 - kk_project_seq norm_frac_rel 2 2
1.498 - | Cst (NormFrac, _, _) => norm_frac_rel
1.499 - | Cst (NatToInt, _, Func (Atom _, Atom _)) => Kodkod.Iden
1.500 - | Cst (NatToInt, _,
1.501 + kk_project_seq (Kodkod.Rel norm_frac_rel) 2 2
1.502 + | Cst (NormFrac, _, _) => Kodkod.Rel norm_frac_rel
1.503 + | Cst (NatToInt, Type ("fun", [@{typ nat}, _]), Func (Atom _, Atom _)) =>
1.504 + Kodkod.Iden
1.505 + | Cst (NatToInt, Type ("fun", [@{typ nat}, _]),
1.506 Func (Atom (nat_k, nat_j0), Opt (Atom (int_k, int_j0)))) =>
1.507 if nat_j0 = int_j0 then
1.508 kk_intersect Kodkod.Iden
1.509 @@ -1192,7 +1302,10 @@
1.510 Kodkod.Univ)
1.511 else
1.512 raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")
1.513 - | Cst (IntToNat, _, Func (Atom (int_k, int_j0), nat_R)) =>
1.514 + | Cst (NatToInt, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
1.515 + to_bit_word_unary_op T R I
1.516 + | Cst (IntToNat, Type ("fun", [@{typ int}, _]),
1.517 + Func (Atom (int_k, int_j0), nat_R)) =>
1.518 let
1.519 val abs_card = max_int_for_card int_k + 1
1.520 val (nat_k, nat_j0) = the_single (atom_schema_of_rep nat_R)
1.521 @@ -1208,6 +1321,10 @@
1.522 else
1.523 raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"")
1.524 end
1.525 + | Cst (IntToNat, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
1.526 + to_bit_word_unary_op T R
1.527 + (fn i => Kodkod.IntIf (Kodkod.LE (i, Kodkod.Num 0),
1.528 + Kodkod.Num 0, i))
1.529 | Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1)
1.530 | Op1 (Finite, _, Opt (Atom _), _) => Kodkod.None
1.531 | Op1 (Converse, T, R, u1) =>
1.532 @@ -1241,7 +1358,7 @@
1.533 val R' = rep_to_binary_rel_rep ofs T1 (unopt_rep (rep_of u1))
1.534 val R'' = opt_rep ofs T1 R'
1.535 in
1.536 - single_rel_let kk
1.537 + single_rel_rel_let kk
1.538 (fn r =>
1.539 let
1.540 val true_r = kk_closure (kk_join r true_atom)
1.541 @@ -1266,7 +1383,7 @@
1.542 Func (R1, Formula Neut) => to_rep R1 u1
1.543 | Func (Unit, Opt R) => to_guard [u1] R true_atom
1.544 | Func (R1, R2 as Opt _) =>
1.545 - single_rel_let kk
1.546 + single_rel_rel_let kk
1.547 (fn r => kk_rel_if (kk_no r) (empty_rel_for_rep R)
1.548 (rel_expr_to_func kk R1 bool_atom_R
1.549 (Func (R1, Formula Neut)) r))
1.550 @@ -1309,12 +1426,22 @@
1.551 if is_opt_rep (rep_of u1) then kk_rel_if (to_f u2) (to_r u1) false_atom
1.552 else kk_rel_if (to_f u1) (to_r u2) false_atom
1.553 | Op2 (Less, _, _, u1, u2) =>
1.554 - if type_of u1 = nat_T then
1.555 - if is_Cst Unrep u1 then to_compare_with_unrep u2 false_atom
1.556 - else if is_Cst Unrep u2 then to_compare_with_unrep u1 true_atom
1.557 - else kk_nat_less (to_integer u1) (to_integer u2)
1.558 - else
1.559 - kk_int_less (to_integer u1) (to_integer u2)
1.560 + (case type_of u1 of
1.561 + @{typ nat} =>
1.562 + if is_Cst Unrep u1 then to_compare_with_unrep u2 false_atom
1.563 + else if is_Cst Unrep u2 then to_compare_with_unrep u1 true_atom
1.564 + else kk_nat_less (to_integer u1) (to_integer u2)
1.565 + | @{typ int} => kk_int_less (to_integer u1) (to_integer u2)
1.566 + | _ => double_rel_rel_let kk
1.567 + (fn r1 => fn r2 =>
1.568 + kk_rel_if
1.569 + (fold kk_and (map_filter (fn (u, r) =>
1.570 + if is_opt_rep (rep_of u) then SOME (kk_some r)
1.571 + else NONE) [(u1, r1), (u2, r2)]) Kodkod.True)
1.572 + (atom_from_formula kk bool_j0 (Kodkod.LT (pairself
1.573 + (int_expr_from_atom kk (type_of u1)) (r1, r2))))
1.574 + Kodkod.None)
1.575 + (to_r u1) (to_r u2))
1.576 | Op2 (The, T, R, u1, u2) =>
1.577 if is_opt_rep R then
1.578 let val r1 = to_opt (Func (unopt_rep R, bool_atom_R)) u1 in
1.579 @@ -1468,7 +1595,7 @@
1.580 if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then
1.581 Kodkod.Atom (offset_of_type ofs nat_T)
1.582 else
1.583 - fold kk_join [to_integer u1, to_integer u2] nat_subtract_rel
1.584 + fold kk_join (map to_integer [u1, u2]) (Kodkod.Rel nat_subtract_rel)
1.585 | Op2 (Apply, _, R, u1, u2) =>
1.586 if is_Cst Unrep u2 andalso is_set_type (type_of u1)
1.587 andalso is_FreeName u1 then
1.588 @@ -1494,7 +1621,7 @@
1.589 kk_rel_let [to_expr_assign u1 u2] (to_rep R u3)
1.590 | Op3 (If, _, R, u1, u2, u3) =>
1.591 if is_opt_rep (rep_of u1) then
1.592 - triple_rel_let kk
1.593 + tripl_rel_rel_let kk
1.594 (fn r1 => fn r2 => fn r3 =>
1.595 let val empty_r = empty_rel_for_rep R in
1.596 fold1 kk_union
1.597 @@ -1686,7 +1813,7 @@
1.598 | Func (_, Formula Neut) => set_oper r1 r2
1.599 | Func (Unit, _) => connective3 r1 r2
1.600 | Func (R1, _) =>
1.601 - double_rel_let kk
1.602 + double_rel_rel_let kk
1.603 (fn r1 => fn r2 =>
1.604 kk_union
1.605 (kk_product
1.606 @@ -1702,6 +1829,43 @@
1.607 r1 r2
1.608 | _ => raise REP ("Nitpick_Kodkod.to_set_op", [min_R]))
1.609 end
1.610 + (* typ -> rep -> (Kodkod.int_expr -> Kodkod.int_expr) -> Kodkod.rel_expr *)
1.611 + and to_bit_word_unary_op T R oper =
1.612 + let
1.613 + val Ts = strip_type T ||> single |> op @
1.614 + (* int -> Kodkod.int_expr *)
1.615 + fun int_arg j = int_expr_from_atom kk (nth Ts j) (Kodkod.Var (1, j))
1.616 + in
1.617 + kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R))
1.618 + (Kodkod.FormulaLet
1.619 + (map (fn j => Kodkod.AssignIntReg (j, int_arg j)) (0 upto 1),
1.620 + Kodkod.IntEq (Kodkod.IntReg 1, oper (Kodkod.IntReg 0))))
1.621 + end
1.622 + (* typ -> rep
1.623 + -> (Kodkod.int_expr -> Kodkod.int_expr -> Kodkod.int_expr -> bool) option
1.624 + -> (Kodkod.int_expr -> Kodkod.int_expr -> Kodkod.int_expr) option
1.625 + -> Kodkod.rel_expr *)
1.626 + and to_bit_word_binary_op T R opt_guard opt_oper =
1.627 + let
1.628 + val Ts = strip_type T ||> single |> op @
1.629 + (* int -> Kodkod.int_expr *)
1.630 + fun int_arg j = int_expr_from_atom kk (nth Ts j) (Kodkod.Var (1, j))
1.631 + in
1.632 + kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R))
1.633 + (Kodkod.FormulaLet
1.634 + (map (fn j => Kodkod.AssignIntReg (j, int_arg j)) (0 upto 2),
1.635 + fold1 kk_and
1.636 + ((case opt_guard of
1.637 + NONE => []
1.638 + | SOME guard =>
1.639 + [guard (Kodkod.IntReg 0) (Kodkod.IntReg 1)
1.640 + (Kodkod.IntReg 2)]) @
1.641 + (case opt_oper of
1.642 + NONE => []
1.643 + | SOME oper =>
1.644 + [Kodkod.IntEq (Kodkod.IntReg 2,
1.645 + oper (Kodkod.IntReg 0) (Kodkod.IntReg 1))]))))
1.646 + end
1.647 (* rep -> rep -> Kodkod.rel_expr -> nut -> Kodkod.rel_expr *)
1.648 and to_apply res_R func_u arg_u =
1.649 case unopt_rep (rep_of func_u) of