author  blanchet 
Tue, 07 Dec 2010 11:56:01 +0100  
changeset 41047  9f1d3fcef1ca 
parent 41045  2a41709f34c1 
child 41049  0edd245892ed 
permissions  rwrr 
33982  1 
(* Title: HOL/Tools/Nitpick/nitpick_kodkod.ML 
33192  2 
Author: Jasmin Blanchette, TU Muenchen 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

3 
Copyright 2008, 2009, 2010 
33192  4 

5 
Kodkod problem generator part of Kodkod. 

6 
*) 

7 

8 
signature NITPICK_KODKOD = 

9 
sig 

35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
34982
diff
changeset

10 
type hol_context = Nitpick_HOL.hol_context 
38126  11 
type datatype_spec = Nitpick_Scope.datatype_spec 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

12 
type kodkod_constrs = Nitpick_Peephole.kodkod_constrs 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

13 
type nut = Nitpick_Nut.nut 
33192  14 

15 
structure NameTable : TABLE 

16 

17 
val univ_card : 

18 
int > int > int > Kodkod.bound list > Kodkod.formula > int 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

19 
val check_bits : int > Kodkod.formula > unit 
38182  20 
val check_arity : string > int > int > unit 
33192  21 
val kk_tuple : bool > int > int list > Kodkod.tuple 
22 
val tuple_set_from_atom_schema : (int * int) list > Kodkod.tuple_set 

23 
val sequential_int_bounds : int > Kodkod.int_bound list 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

24 
val pow_of_two_int_bounds : int > int > Kodkod.int_bound list 
38126  25 
val bounds_and_axioms_for_built_in_rels_in_formulas : 
39345  26 
bool > int > int > int > int > Kodkod.formula list 
38126  27 
> Kodkod.bound list * Kodkod.formula list 
33192  28 
val bound_for_plain_rel : Proof.context > bool > nut > Kodkod.bound 
29 
val bound_for_sel_rel : 

38126  30 
Proof.context > bool > datatype_spec list > nut > Kodkod.bound 
33192  31 
val merge_bounds : Kodkod.bound list > Kodkod.bound list 
32 
val declarative_axiom_for_plain_rel : kodkod_constrs > nut > Kodkod.formula 

33 
val declarative_axioms_for_datatypes : 

38126  34 
hol_context > bool > int > int > int Typtab.table > kodkod_constrs 
35 
> nut NameTable.table > datatype_spec list > Kodkod.formula list 

33192  36 
val kodkod_formula_from_nut : 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

37 
int Typtab.table > kodkod_constrs > nut > Kodkod.formula 
33192  38 
end; 
39 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

40 
structure Nitpick_Kodkod : NITPICK_KODKOD = 
33192  41 
struct 
42 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

43 
open Nitpick_Util 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

44 
open Nitpick_HOL 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

45 
open Nitpick_Scope 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

46 
open Nitpick_Peephole 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

47 
open Nitpick_Rep 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

48 
open Nitpick_Nut 
33192  49 

34126  50 
structure KK = Kodkod 
51 

38126  52 
fun pull x xs = x :: filter_out (curry (op =) x) xs 
33192  53 

38196  54 
fun is_datatype_acyclic ({co = false, standard = true, deep = true, ...} 
55 
: datatype_spec) = true 

56 
 is_datatype_acyclic _ = false 

33192  57 

34126  58 
fun flip_nums n = index_seq 1 n @ [0] > map KK.Num 
33192  59 

60 
fun univ_card nat_card int_card main_j0 bounds formula = 

61 
let 

62 
fun rel_expr_func r k = 

63 
Int.max (k, case r of 

34126  64 
KK.Atom j => j + 1 
65 
 KK.AtomSeq (k', j0) => j0 + k' 

33192  66 
 _ => 0) 
67 
fun tuple_func t k = 

68 
case t of 

34126  69 
KK.Tuple js => fold Integer.max (map (Integer.add 1) js) k 
33192  70 
 _ => k 
71 
fun tuple_set_func ts k = 

34126  72 
Int.max (k, case ts of KK.TupleAtomSeq (k', j0) => j0 + k'  _ => 0) 
33192  73 
val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func, 
74 
int_expr_func = K I} 

75 
val tuple_F = {tuple_func = tuple_func, tuple_set_func = tuple_set_func} 

34126  76 
val card = fold (KK.fold_bound expr_F tuple_F) bounds 1 
77 
> KK.fold_formula expr_F formula 

33192  78 
in Int.max (main_j0 + fold Integer.max [2, nat_card, int_card] 0, card) end 
79 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

80 
fun check_bits bits formula = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

81 
let 
34126  82 
fun int_expr_func (KK.Num k) () = 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

83 
if is_twos_complement_representable bits k then 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

84 
() 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

85 
else 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

86 
raise TOO_SMALL ("Nitpick_Kodkod.check_bits", 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

87 
"\"bits\" value " ^ string_of_int bits ^ 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

88 
" too small for problem") 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

89 
 int_expr_func _ () = () 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

90 
val expr_F = {formula_func = K I, rel_expr_func = K I, 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

91 
int_expr_func = int_expr_func} 
34126  92 
in KK.fold_formula expr_F formula () end 
33192  93 

38182  94 
fun check_arity guilty_party univ_card n = 
34126  95 
if n > KK.max_arity univ_card then 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

96 
raise TOO_LARGE ("Nitpick_Kodkod.check_arity", 
38182  97 
"arity " ^ string_of_int n ^ 
98 
(if guilty_party = "" then 

99 
"" 

100 
else 

101 
" of Kodkod relation associated with " ^ 

41045
2a41709f34c1
use heuristic to determine whether to keep or drop an existing "let"  and drop all higherorder lets
blanchet
parents:
39898
diff
changeset

102 
quote (original_name guilty_party)) ^ 
38182  103 
" too large for universe of cardinality " ^ 
104 
string_of_int univ_card) 

33192  105 
else 
106 
() 

107 

108 
fun kk_tuple debug univ_card js = 

109 
if debug then 

34126  110 
KK.Tuple js 
33192  111 
else 
34126  112 
KK.TupleIndex (length js, 
113 
fold (fn j => fn accum => accum * univ_card + j) js 0) 

33192  114 

34126  115 
val tuple_set_from_atom_schema = foldl1 KK.TupleProduct o map KK.TupleAtomSeq 
33192  116 
val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep 
117 

34126  118 
val single_atom = KK.TupleSet o single o KK.Tuple o single 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

119 
fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))] 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

120 
fun pow_of_two_int_bounds bits j0 = 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

121 
let 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

122 
fun aux 0 _ _ = [] 
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset

123 
 aux 1 pow_of_two j = [(SOME (~ pow_of_two), [single_atom j])] 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

124 
 aux iter pow_of_two j = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

125 
(SOME pow_of_two, [single_atom j]) :: 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

126 
aux (iter  1) (2 * pow_of_two) (j + 1) 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

127 
in aux (bits + 1) 1 j0 end 
33192  128 

38126  129 
fun built_in_rels_in_formulas formulas = 
33192  130 
let 
39345  131 
fun rel_expr_func (KK.Rel (x as (_, j))) = 
38126  132 
(j < 0 andalso x <> unsigned_bit_word_sel_rel andalso 
133 
x <> signed_bit_word_sel_rel) 

134 
? insert (op =) x 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

135 
 rel_expr_func _ = I 
33192  136 
val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func, 
137 
int_expr_func = K I} 

38126  138 
in fold (KK.fold_formula expr_F) formulas [] end 
33192  139 

140 
val max_table_size = 65536 

141 

142 
fun check_table_size k = 

143 
if k > max_table_size then 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

144 
raise TOO_LARGE ("Nitpick_Kodkod.check_table_size", 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

145 
"precomputed table too large (" ^ string_of_int k ^ ")") 
33192  146 
else 
147 
() 

148 

149 
fun tabulate_func1 debug univ_card (k, j0) f = 

150 
(check_table_size k; 

151 
map_filter (fn j1 => let val j2 = f j1 in 

152 
if j2 >= 0 then 

153 
SOME (kk_tuple debug univ_card [j1 + j0, j2 + j0]) 

154 
else 

155 
NONE 

156 
end) (index_seq 0 k)) 

157 
fun tabulate_op2 debug univ_card (k, j0) res_j0 f = 

158 
(check_table_size (k * k); 

159 
map_filter (fn j => let 

160 
val j1 = j div k 

161 
val j2 = j  j1 * k 

162 
val j3 = f (j1, j2) 

163 
in 

164 
if j3 >= 0 then 

165 
SOME (kk_tuple debug univ_card 

166 
[j1 + j0, j2 + j0, j3 + res_j0]) 

167 
else 

168 
NONE 

169 
end) (index_seq 0 (k * k))) 

170 
fun tabulate_op2_2 debug univ_card (k, j0) res_j0 f = 

171 
(check_table_size (k * k); 

172 
map_filter (fn j => let 

173 
val j1 = j div k 

174 
val j2 = j  j1 * k 

175 
val (j3, j4) = f (j1, j2) 

176 
in 

177 
if j3 >= 0 andalso j4 >= 0 then 

178 
SOME (kk_tuple debug univ_card 

179 
[j1 + j0, j2 + j0, j3 + res_j0, 

180 
j4 + res_j0]) 

181 
else 

182 
NONE 

183 
end) (index_seq 0 (k * k))) 

184 
fun tabulate_nat_op2 debug univ_card (k, j0) f = 

185 
tabulate_op2 debug univ_card (k, j0) j0 (atom_for_nat (k, 0) o f) 

186 
fun tabulate_int_op2 debug univ_card (k, j0) f = 

187 
tabulate_op2 debug univ_card (k, j0) j0 

188 
(atom_for_int (k, 0) o f o pairself (int_for_atom (k, 0))) 

189 
fun tabulate_int_op2_2 debug univ_card (k, j0) f = 

190 
tabulate_op2_2 debug univ_card (k, j0) j0 

191 
(pairself (atom_for_int (k, 0)) o f 

192 
o pairself (int_for_atom (k, 0))) 

193 

194 
fun isa_div (m, n) = m div n handle General.Div => 0 

195 
fun isa_mod (m, n) = m mod n handle General.Div => m 

196 
fun isa_gcd (m, 0) = m 

197 
 isa_gcd (m, n) = isa_gcd (n, isa_mod (m, n)) 

198 
fun isa_lcm (m, n) = isa_div (m * n, isa_gcd (m, n)) 

199 
val isa_zgcd = isa_gcd o pairself abs 

200 
fun isa_norm_frac (m, n) = 

201 
if n < 0 then isa_norm_frac (~m, ~n) 

202 
else if m = 0 orelse n = 0 then (0, 1) 

203 
else let val p = isa_zgcd (m, n) in (isa_div (m, p), isa_div (n, p)) end 

204 

39345  205 
fun tabulate_built_in_rel debug univ_card nat_card int_card j0 
38124  206 
(x as (n, _)) = 
38182  207 
(check_arity "" univ_card n; 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

208 
if x = not3_rel then 
33192  209 
("not3", tabulate_func1 debug univ_card (2, j0) (curry (op ) 1)) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

210 
else if x = suc_rel then 
38126  211 
("suc", tabulate_func1 debug univ_card (univ_card  j0  1, j0) 
212 
(Integer.add 1)) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

213 
else if x = nat_add_rel then 
33192  214 
("nat_add", tabulate_nat_op2 debug univ_card (nat_card, j0) (op +)) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

215 
else if x = int_add_rel then 
33192  216 
("int_add", tabulate_int_op2 debug univ_card (int_card, j0) (op +)) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

217 
else if x = nat_subtract_rel then 
33192  218 
("nat_subtract", 
33705
947184dc75c9
removed a few global names in Nitpick (styp, nat_less, pairf)
blanchet
parents:
33631
diff
changeset

219 
tabulate_op2 debug univ_card (nat_card, j0) j0 (uncurry nat_minus)) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

220 
else if x = int_subtract_rel then 
33192  221 
("int_subtract", tabulate_int_op2 debug univ_card (int_card, j0) (op )) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

222 
else if x = nat_multiply_rel then 
33192  223 
("nat_multiply", tabulate_nat_op2 debug univ_card (nat_card, j0) (op * )) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

224 
else if x = int_multiply_rel then 
33192  225 
("int_multiply", tabulate_int_op2 debug univ_card (int_card, j0) (op * )) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

226 
else if x = nat_divide_rel then 
33192  227 
("nat_divide", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_div) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

228 
else if x = int_divide_rel then 
33192  229 
("int_divide", tabulate_int_op2 debug univ_card (int_card, j0) isa_div) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

230 
else if x = nat_less_rel then 
33192  231 
("nat_less", tabulate_nat_op2 debug univ_card (nat_card, j0) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35312
diff
changeset

232 
(int_from_bool o op <)) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

233 
else if x = int_less_rel then 
33192  234 
("int_less", tabulate_int_op2 debug univ_card (int_card, j0) 
35385
29f81babefd7
improved precision of infinite "shallow" datatypes in Nitpick;
blanchet
parents:
35312
diff
changeset

235 
(int_from_bool o op <)) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

236 
else if x = gcd_rel then 
33192  237 
("gcd", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_gcd) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

238 
else if x = lcm_rel then 
33192  239 
("lcm", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_lcm) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

240 
else if x = norm_frac_rel then 
33192  241 
("norm_frac", tabulate_int_op2_2 debug univ_card (int_card, j0) 
242 
isa_norm_frac) 

243 
else 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

244 
raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation")) 
33192  245 

39345  246 
fun bound_for_built_in_rel debug univ_card nat_card int_card main_j0 
38126  247 
(x as (n, j)) = 
248 
if n = 2 andalso j <= suc_rels_base then 

249 
let val (y as (k, j0), tabulate) = atom_seq_for_suc_rel x in 

250 
([(x, "suc")], 

251 
if tabulate then 

252 
[KK.TupleSet (tabulate_func1 debug univ_card (k  1, j0) 

253 
(Integer.add 1))] 

254 
else 

255 
[KK.TupleSet [], tuple_set_from_atom_schema [y, y]]) 

256 
end 

257 
else 

258 
let 

39345  259 
val (nick, ts) = tabulate_built_in_rel debug univ_card nat_card int_card 
260 
main_j0 x 

38126  261 
in ([(x, nick)], [KK.TupleSet ts]) end 
33192  262 

38126  263 
fun axiom_for_built_in_rel (x as (n, j)) = 
264 
if n = 2 andalso j <= suc_rels_base then 

265 
let val (y as (k, j0), tabulate) = atom_seq_for_suc_rel x in 

38160  266 
if tabulate then 
38126  267 
NONE 
38160  268 
else if k < 2 then 
269 
SOME (KK.No (KK.Rel x)) 

38126  270 
else 
271 
SOME (KK.TotalOrdering (x, KK.AtomSeq y, KK.Atom j0, KK.Atom (j0 + 1))) 

272 
end 

273 
else 

274 
NONE 

39345  275 
fun bounds_and_axioms_for_built_in_rels_in_formulas debug univ_card nat_card 
38126  276 
int_card main_j0 formulas = 
277 
let val rels = built_in_rels_in_formulas formulas in 

39345  278 
(map (bound_for_built_in_rel debug univ_card nat_card int_card main_j0) 
38126  279 
rels, 
280 
map_filter axiom_for_built_in_rel rels) 

39316
b6c4385ab400
change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
blanchet
parents:
38212
diff
changeset

281 
end 
33192  282 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

283 
fun bound_comment ctxt debug nick T R = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

284 
short_name nick ^ 
34982
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

285 
(if debug then " :: " ^ unyxml (Syntax.string_of_typ ctxt T) else "") ^ 
7b8c366e34a2
added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
blanchet
parents:
34936
diff
changeset

286 
" : " ^ string_for_rep R 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

287 

33192  288 
fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) = 
289 
([(x, bound_comment ctxt debug nick T R)], 

290 
if nick = @{const_name bisim_iterator_max} then 

291 
case R of 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

292 
Atom (k, j0) => [single_atom (k  1 + j0)] 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

293 
 _ => raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u]) 
33192  294 
else 
34126  295 
[KK.TupleSet [], upper_bound_for_rep R]) 
33192  296 
 bound_for_plain_rel _ _ u = 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

297 
raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u]) 
33192  298 

299 
fun bound_for_sel_rel ctxt debug dtypes 

35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

300 
(FreeRel (x, T as Type (@{type_name fun}, [T1, T2]), 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

301 
R as Func (Atom (_, j0), R2), nick)) = 
33192  302 
let 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

303 
val {delta, epsilon, exclusive, explicit_max, ...} = 
33192  304 
constr_spec dtypes (original_name nick, T1) 
305 
in 

306 
([(x, bound_comment ctxt debug nick T R)], 

307 
if explicit_max = 0 then 

34126  308 
[KK.TupleSet []] 
33192  309 
else 
34126  310 
let val ts = KK.TupleAtomSeq (epsilon  delta, delta + j0) in 
33192  311 
if R2 = Formula Neut then 
34126  312 
[ts] > not exclusive ? cons (KK.TupleSet []) 
33192  313 
else 
35072
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

314 
[KK.TupleSet [], 
35178  315 
if T1 = T2 andalso epsilon > delta andalso 
38196  316 
is_datatype_acyclic (the (datatype_spec dtypes T1)) then 
35072
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

317 
index_seq delta (epsilon  delta) 
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

318 
> map (fn j => 
38126  319 
KK.TupleProduct (KK.TupleSet [KK.Tuple [j + j0]], 
35072
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

320 
KK.TupleAtomSeq (j, j0))) 
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

321 
> foldl1 KK.TupleUnion 
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

322 
else 
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

323 
KK.TupleProduct (ts, upper_bound_for_rep R2)] 
33192  324 
end) 
325 
end 

326 
 bound_for_sel_rel _ _ _ u = 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

327 
raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u]) 
33192  328 

329 
fun merge_bounds bs = 

330 
let 

331 
fun arity (zs, _) = fst (fst (hd zs)) 

332 
fun add_bound ds b [] = List.revAppend (ds, [b]) 

333 
 add_bound ds b (c :: cs) = 

334 
if arity b = arity c andalso snd b = snd c then 

335 
List.revAppend (ds, (fst c @ fst b, snd c) :: cs) 

336 
else 

337 
add_bound (c :: ds) b cs 

338 
in fold (add_bound []) bs [] end 

339 

34126  340 
fun unary_var_seq j0 n = map (curry KK.Var 1) (index_seq j0 n) 
33192  341 

34126  342 
val singleton_from_combination = foldl1 KK.Product o map KK.Atom 
33192  343 
fun all_singletons_for_rep R = 
344 
if is_lone_rep R then 

345 
all_combinations_for_rep R > map singleton_from_combination 

346 
else 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

347 
raise REP ("Nitpick_Kodkod.all_singletons_for_rep", [R]) 
33192  348 

34126  349 
fun unpack_products (KK.Product (r1, r2)) = 
33192  350 
unpack_products r1 @ unpack_products r2 
351 
 unpack_products r = [r] 

34126  352 
fun unpack_joins (KK.Join (r1, r2)) = unpack_joins r1 @ unpack_joins r2 
33192  353 
 unpack_joins r = [r] 
354 

355 
val empty_rel_for_rep = empty_n_ary_rel o arity_of_rep 

356 
fun full_rel_for_rep R = 

357 
case atom_schema_of_rep R of 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

358 
[] => raise REP ("Nitpick_Kodkod.full_rel_for_rep", [R]) 
34126  359 
 schema => foldl1 KK.Product (map KK.AtomSeq schema) 
33192  360 

361 
fun decls_for_atom_schema j0 schema = 

34126  362 
map2 (fn j => fn x => KK.DeclOne ((1, j), KK.AtomSeq x)) 
33192  363 
(index_seq j0 (length schema)) schema 
364 

365 
fun d_n_ary_function ({kk_all, kk_join, kk_lone, kk_one, ...} : kodkod_constrs) 

366 
R r = 

367 
let val body_R = body_rep R in 

368 
if is_lone_rep body_R then 

369 
let 

370 
val binder_schema = atom_schema_of_reps (binder_reps R) 

371 
val body_schema = atom_schema_of_rep body_R 

372 
val one = is_one_rep body_R 

34126  373 
val opt_x = case r of KK.Rel x => SOME x  _ => NONE 
33192  374 
in 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

375 
if opt_x <> NONE andalso length binder_schema = 1 andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

376 
length body_schema = 1 then 
34126  377 
(if one then KK.Function else KK.Functional) 
378 
(the opt_x, KK.AtomSeq (hd binder_schema), 

379 
KK.AtomSeq (hd body_schema)) 

33192  380 
else 
381 
let 

382 
val decls = decls_for_atom_schema ~1 binder_schema 

383 
val vars = unary_var_seq ~1 (length binder_schema) 

384 
val kk_xone = if one then kk_one else kk_lone 

385 
in kk_all decls (kk_xone (fold kk_join vars r)) end 

386 
end 

387 
else 

34126  388 
KK.True 
33192  389 
end 
34126  390 
fun kk_n_ary_function kk R (r as KK.Rel x) = 
33192  391 
if not (is_opt_rep R) then 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

392 
if x = suc_rel then 
34126  393 
KK.False 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

394 
else if x = nat_add_rel then 
33192  395 
formula_for_bool (card_of_rep (body_rep R) = 1) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

396 
else if x = nat_multiply_rel then 
33192  397 
formula_for_bool (card_of_rep (body_rep R) <= 2) 
398 
else 

399 
d_n_ary_function kk R r 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

400 
else if x = nat_subtract_rel then 
34126  401 
KK.True 
33192  402 
else 
403 
d_n_ary_function kk R r 

404 
 kk_n_ary_function kk R r = d_n_ary_function kk R r 

405 

34126  406 
fun kk_disjoint_sets _ [] = KK.True 
33192  407 
 kk_disjoint_sets (kk as {kk_and, kk_no, kk_intersect, ...} : kodkod_constrs) 
408 
(r :: rs) = 

409 
fold (kk_and o kk_no o kk_intersect r) rs (kk_disjoint_sets kk rs) 

410 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

411 
fun basic_rel_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r = 
33192  412 
if inline_rel_expr r then 
413 
f r 

414 
else 

34126  415 
let val x = (KK.arity_of_rel_expr r, j) in 
416 
kk_rel_let [KK.AssignRelReg (x, r)] (f (KK.RelReg x)) 

33192  417 
end 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

418 
val single_rel_rel_let = basic_rel_rel_let 0 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

419 
fun double_rel_rel_let kk f r1 r2 = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

420 
single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1 
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset

421 
fun triple_rel_rel_let kk f r1 r2 r3 = 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

422 
double_rel_rel_let kk 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

423 
(fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2 
33192  424 

425 
fun atom_from_formula ({kk_rel_if, ...} : kodkod_constrs) j0 f = 

34126  426 
kk_rel_if f (KK.Atom (j0 + 1)) (KK.Atom j0) 
33192  427 
fun rel_expr_from_formula kk R f = 
428 
case unopt_rep R of 

429 
Atom (2, j0) => atom_from_formula kk j0 f 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

430 
 _ => raise REP ("Nitpick_Kodkod.rel_expr_from_formula", [R]) 
33192  431 

432 
fun unpack_vect_in_chunks ({kk_project_seq, ...} : kodkod_constrs) chunk_arity 

433 
num_chunks r = 

434 
List.tabulate (num_chunks, fn j => kk_project_seq r (j * chunk_arity) 

435 
chunk_arity) 

436 

437 
fun kk_n_fold_join 

438 
(kk as {kk_intersect, kk_product, kk_join, kk_project_seq, ...}) one R1 

439 
res_R r1 r2 = 

440 
case arity_of_rep R1 of 

441 
1 => kk_join r1 r2 

442 
 arity1 => 

38164  443 
let val unpacked_rs1 = unpack_products r1 in 
33192  444 
if one andalso length unpacked_rs1 = arity1 then 
445 
fold kk_join unpacked_rs1 r2 

38164  446 
else if one andalso inline_rel_expr r1 then 
447 
fold kk_join (unpack_vect_in_chunks kk 1 arity1 r1) r2 

33192  448 
else 
449 
kk_project_seq 

450 
(kk_intersect (kk_product r1 (full_rel_for_rep res_R)) r2) 

451 
arity1 (arity_of_rep res_R) 

452 
end 

453 

454 
fun kk_case_switch (kk as {kk_union, kk_product, ...}) R1 R2 r rs1 rs2 = 

455 
if rs1 = rs2 then r 

456 
else kk_n_fold_join kk true R1 R2 r (fold1 kk_union (map2 kk_product rs1 rs2)) 

457 

458 
val lone_rep_fallback_max_card = 4096 

459 
val some_j0 = 0 

460 

461 
fun lone_rep_fallback kk new_R old_R r = 

462 
if old_R = new_R then 

463 
r 

464 
else 

465 
let val card = card_of_rep old_R in 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

466 
if is_lone_rep old_R andalso is_lone_rep new_R andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

467 
card = card_of_rep new_R then 
33192  468 
if card >= lone_rep_fallback_max_card then 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

469 
raise TOO_LARGE ("Nitpick_Kodkod.lone_rep_fallback", 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

470 
"too high cardinality (" ^ string_of_int card ^ ")") 
33192  471 
else 
472 
kk_case_switch kk old_R new_R r (all_singletons_for_rep old_R) 

473 
(all_singletons_for_rep new_R) 

474 
else 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

475 
raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R]) 
33192  476 
end 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

477 
and atom_from_rel_expr kk x old_R r = 
33192  478 
case old_R of 
479 
Func (R1, R2) => 

480 
let 

481 
val dom_card = card_of_rep R1 

482 
val R2' = case R2 of Atom _ => R2  _ => Atom (card_of_rep R2, some_j0) 

483 
in 

484 
atom_from_rel_expr kk x (Vect (dom_card, R2')) 

485 
(vect_from_rel_expr kk dom_card R2' old_R r) 

486 
end 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

487 
 Opt _ => raise REP ("Nitpick_Kodkod.atom_from_rel_expr", [old_R]) 
33192  488 
 _ => lone_rep_fallback kk (Atom x) old_R r 
489 
and struct_from_rel_expr kk Rs old_R r = 

490 
case old_R of 

491 
Atom _ => lone_rep_fallback kk (Struct Rs) old_R r 

492 
 Struct Rs' => 

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

493 
if Rs' = Rs then 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

494 
r 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

495 
else if map card_of_rep Rs' = map card_of_rep Rs then 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

496 
let 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

497 
val old_arities = map arity_of_rep Rs' 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

498 
val old_offsets = offset_list old_arities 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

499 
val old_rs = map2 (#kk_project_seq kk r) old_offsets old_arities 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

500 
in 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

501 
fold1 (#kk_product kk) 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

502 
(map3 (rel_expr_from_rel_expr kk) Rs Rs' old_rs) 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

503 
end 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

504 
else 
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

505 
lone_rep_fallback kk (Struct Rs) old_R r 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

506 
 _ => raise REP ("Nitpick_Kodkod.struct_from_rel_expr", [old_R]) 
33192  507 
and vect_from_rel_expr kk k R old_R r = 
508 
case old_R of 

509 
Atom _ => lone_rep_fallback kk (Vect (k, R)) old_R r 

510 
 Vect (k', R') => 

511 
if k = k' andalso R = R' then r 

512 
else lone_rep_fallback kk (Vect (k, R)) old_R r 

513 
 Func (R1, Formula Neut) => 

514 
if k = card_of_rep R1 then 

515 
fold1 (#kk_product kk) 

516 
(map (fn arg_r => 

517 
rel_expr_from_formula kk R (#kk_subset kk arg_r r)) 

518 
(all_singletons_for_rep R1)) 

519 
else 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

520 
raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R]) 
33192  521 
 Func (R1, R2) => 
522 
fold1 (#kk_product kk) 

523 
(map (fn arg_r => 

524 
rel_expr_from_rel_expr kk R R2 

525 
(kk_n_fold_join kk true R1 R2 arg_r r)) 

526 
(all_singletons_for_rep R1)) 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

527 
 _ => raise REP ("Nitpick_Kodkod.vect_from_rel_expr", [old_R]) 
33192  528 
and func_from_no_opt_rel_expr kk R1 R2 (Atom x) r = 
529 
let 

530 
val dom_card = card_of_rep R1 

531 
val R2' = case R2 of Atom _ => R2  _ => Atom (card_of_rep R2, some_j0) 

532 
in 

533 
func_from_no_opt_rel_expr kk R1 R2 (Vect (dom_card, R2')) 

534 
(vect_from_rel_expr kk dom_card R2' (Atom x) r) 

535 
end 

536 
 func_from_no_opt_rel_expr kk R1 (Formula Neut) old_R r = 

537 
(case old_R of 

538 
Vect (k, Atom (2, j0)) => 

539 
let 

540 
val args_rs = all_singletons_for_rep R1 

541 
val vals_rs = unpack_vect_in_chunks kk 1 k r 

542 
fun empty_or_singleton_set_for arg_r val_r = 

34126  543 
#kk_join kk val_r (#kk_product kk (KK.Atom (j0 + 1)) arg_r) 
33192  544 
in 
545 
fold1 (#kk_union kk) (map2 empty_or_singleton_set_for args_rs vals_rs) 

546 
end 

547 
 Func (R1', Formula Neut) => 

548 
if R1 = R1' then 

549 
r 

550 
else 

551 
let 

552 
val schema = atom_schema_of_rep R1 

553 
val r1 = fold1 (#kk_product kk) (unary_var_seq ~1 (length schema)) 

554 
> rel_expr_from_rel_expr kk R1' R1 

33582
bdf98e327f0b
fixed soundness bug in Nitpick related to sets of sets;
blanchet
parents:
33571
diff
changeset

555 
val kk_xeq = (if is_one_rep R1' then #kk_subset else #kk_rel_eq) kk 
33192  556 
in 
33582
bdf98e327f0b
fixed soundness bug in Nitpick related to sets of sets;
blanchet
parents:
33571
diff
changeset

557 
#kk_comprehension kk (decls_for_atom_schema ~1 schema) (kk_xeq r1 r) 
33192  558 
end 
559 
 Func (R1', Atom (2, j0)) => 

560 
func_from_no_opt_rel_expr kk R1 (Formula Neut) 

34126  561 
(Func (R1', Formula Neut)) (#kk_join kk r (KK.Atom (j0 + 1))) 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

562 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  563 
[old_R, Func (R1, Formula Neut)])) 
564 
 func_from_no_opt_rel_expr kk R1 R2 old_R r = 

565 
case old_R of 

566 
Vect (k, R) => 

567 
let 

568 
val args_rs = all_singletons_for_rep R1 

569 
val vals_rs = unpack_vect_in_chunks kk (arity_of_rep R) k r 

570 
> map (rel_expr_from_rel_expr kk R2 R) 

571 
in fold1 (#kk_union kk) (map2 (#kk_product kk) args_rs vals_rs) end 

572 
 Func (R1', Formula Neut) => 

573 
(case R2 of 

574 
Atom (x as (2, j0)) => 

575 
let val schema = atom_schema_of_rep R1 in 

576 
if length schema = 1 then 

34126  577 
#kk_override kk (#kk_product kk (KK.AtomSeq (hd schema)) 
578 
(KK.Atom j0)) 

579 
(#kk_product kk r (KK.Atom (j0 + 1))) 

33192  580 
else 
581 
let 

582 
val r1 = fold1 (#kk_product kk) (unary_var_seq ~1 (length schema)) 

583 
> rel_expr_from_rel_expr kk R1' R1 

34126  584 
val r2 = KK.Var (1, ~(length schema)  1) 
33192  585 
val r3 = atom_from_formula kk j0 (#kk_subset kk r1 r) 
586 
in 

587 
#kk_comprehension kk (decls_for_atom_schema ~1 (schema @ [x])) 

33582
bdf98e327f0b
fixed soundness bug in Nitpick related to sets of sets;
blanchet
parents:
33571
diff
changeset

588 
(#kk_subset kk r2 r3) 
33192  589 
end 
590 
end 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

591 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  592 
[old_R, Func (R1, R2)])) 
593 
 Func (R1', R2') => 

594 
if R1 = R1' andalso R2 = R2' then 

595 
r 

596 
else 

597 
let 

598 
val dom_schema = atom_schema_of_rep R1 

599 
val ran_schema = atom_schema_of_rep R2 

600 
val dom_prod = fold1 (#kk_product kk) 

601 
(unary_var_seq ~1 (length dom_schema)) 

602 
> rel_expr_from_rel_expr kk R1' R1 

603 
val ran_prod = fold1 (#kk_product kk) 

604 
(unary_var_seq (~(length dom_schema)  1) 

605 
(length ran_schema)) 

606 
> rel_expr_from_rel_expr kk R2' R2 

607 
val app = kk_n_fold_join kk true R1' R2' dom_prod r 

33582
bdf98e327f0b
fixed soundness bug in Nitpick related to sets of sets;
blanchet
parents:
33571
diff
changeset

608 
val kk_xeq = (if is_one_rep R2' then #kk_subset else #kk_rel_eq) kk 
33192  609 
in 
610 
#kk_comprehension kk (decls_for_atom_schema ~1 

611 
(dom_schema @ ran_schema)) 

33582
bdf98e327f0b
fixed soundness bug in Nitpick related to sets of sets;
blanchet
parents:
33571
diff
changeset

612 
(kk_xeq ran_prod app) 
33192  613 
end 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

614 
 _ => raise REP ("Nitpick_Kodkod.func_from_no_opt_rel_expr", 
33192  615 
[old_R, Func (R1, R2)]) 
616 
and rel_expr_from_rel_expr kk new_R old_R r = 

617 
let 

618 
val unopt_old_R = unopt_rep old_R 

619 
val unopt_new_R = unopt_rep new_R 

620 
in 

621 
if unopt_old_R <> old_R andalso unopt_new_R = new_R then 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

622 
raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", [old_R, new_R]) 
33192  623 
else if unopt_new_R = unopt_old_R then 
624 
r 

625 
else 

626 
(case unopt_new_R of 

627 
Atom x => atom_from_rel_expr kk x 

628 
 Struct Rs => struct_from_rel_expr kk Rs 

629 
 Vect (k, R') => vect_from_rel_expr kk k R' 

630 
 Func (R1, R2) => func_from_no_opt_rel_expr kk R1 R2 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

631 
 _ => raise REP ("Nitpick_Kodkod.rel_expr_from_rel_expr", 
33192  632 
[old_R, new_R])) 
633 
unopt_old_R r 

634 
end 

635 
and rel_expr_to_func kk R1 R2 = rel_expr_from_rel_expr kk (Func (R1, R2)) 

636 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

637 
fun bit_set_from_atom ({kk_join, ...} : kodkod_constrs) T r = 
34126  638 
kk_join r (KK.Rel (if T = @{typ "unsigned_bit word"} then 
639 
unsigned_bit_word_sel_rel 

640 
else 

641 
signed_bit_word_sel_rel)) 

642 
val int_expr_from_atom = KK.SetSum ooo bit_set_from_atom 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

643 
fun atom_from_int_expr (kk as {kk_rel_eq, kk_comprehension, ...} 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

644 
: kodkod_constrs) T R i = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

645 
kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R)) 
34126  646 
(kk_rel_eq (bit_set_from_atom kk T (KK.Var (1, ~1))) 
647 
(KK.Bits i)) 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

648 

33192  649 
fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) = 
650 
kk_n_ary_function kk (R > nick = @{const_name List.set} ? unopt_rep) 

34126  651 
(KK.Rel x) 
33192  652 
 declarative_axiom_for_plain_rel ({kk_lone, kk_one, ...} : kodkod_constrs) 
653 
(FreeRel (x, _, R, _)) = 

34126  654 
if is_one_rep R then kk_one (KK.Rel x) 
655 
else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (KK.Rel x) 

656 
else KK.True 

33192  657 
 declarative_axiom_for_plain_rel _ u = 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

658 
raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u]) 
33192  659 

660 
fun const_triple rel_table (x as (s, T)) = 

661 
case the_name rel_table (ConstName (s, T, Any)) of 

34126  662 
FreeRel ((n, j), _, R, _) => (KK.Rel (n, j), R, n) 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

663 
 _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x]) 
33192  664 

665 
fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr 

666 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

667 
fun nfa_transitions_for_sel hol_ctxt binarize 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

668 
({kk_project, ...} : kodkod_constrs) rel_table 
38126  669 
(dtypes : datatype_spec list) constr_x n = 
33192  670 
let 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

671 
val x as (_, T) = 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

672 
binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize constr_x n 
33192  673 
val (r, R, arity) = const_triple rel_table x 
674 
val type_schema = type_schema_of_rep T R 

675 
in 

676 
map_filter (fn (j, T) => 

677 
if forall (not_equal T o #typ) dtypes then NONE 

38126  678 
else SOME ((x, kk_project r (map KK.Num [0, j])), T)) 
33192  679 
(index_seq 1 (arity  1) ~~ tl type_schema) 
680 
end 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

681 
fun nfa_transitions_for_constr hol_ctxt binarize kk rel_table dtypes 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

682 
(x as (_, T)) = 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

683 
maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x) 
33192  684 
(index_seq 0 (num_sels_for_constr_type T)) 
38126  685 
fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : datatype_spec) = NONE 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

686 
 nfa_entry_for_datatype _ _ _ _ _ {standard = false, ...} = NONE 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

687 
 nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

688 
 nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

689 
{typ, constrs, ...} = 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

690 
SOME (typ, maps (nfa_transitions_for_constr hol_ctxt binarize kk rel_table 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

691 
dtypes o #const) constrs) 
33192  692 

34126  693 
val empty_rel = KK.Product (KK.None, KK.None) 
33192  694 

35177  695 
fun direct_path_rel_exprs nfa start_T final_T = 
696 
case AList.lookup (op =) nfa final_T of 

38126  697 
SOME trans => map (snd o fst) (filter (curry (op =) start_T o snd) trans) 
33192  698 
 NONE => [] 
35177  699 
and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T 
700 
final_T = 

701 
fold kk_union (direct_path_rel_exprs nfa start_T final_T) 

702 
(if start_T = final_T then KK.Iden else empty_rel) 

703 
 any_path_rel_expr (kk as {kk_union, ...}) nfa (T :: Ts) start_T final_T = 

704 
kk_union (any_path_rel_expr kk nfa Ts start_T final_T) 

705 
(knot_path_rel_expr kk nfa Ts start_T T final_T) 

706 
and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa Ts 

707 
start_T knot_T final_T = 

708 
kk_join (kk_join (any_path_rel_expr kk nfa Ts knot_T final_T) 

709 
(kk_reflexive_closure (loop_path_rel_expr kk nfa Ts knot_T))) 

710 
(any_path_rel_expr kk nfa Ts start_T knot_T) 

711 
and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T = 

712 
fold kk_union (direct_path_rel_exprs nfa start_T start_T) empty_rel 

713 
 loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (T :: Ts) 

714 
start_T = 

715 
if start_T = T then 

716 
kk_closure (loop_path_rel_expr kk nfa Ts start_T) 

33192  717 
else 
35177  718 
kk_union (loop_path_rel_expr kk nfa Ts start_T) 
719 
(knot_path_rel_expr kk nfa Ts start_T T start_T) 

33192  720 

39898  721 
fun add_nfa_to_graph [] = I 
722 
 add_nfa_to_graph ((_, []) :: nfa) = add_nfa_to_graph nfa 

723 
 add_nfa_to_graph ((T, ((_, T') :: transitions)) :: nfa) = 

724 
add_nfa_to_graph ((T, transitions) :: nfa) o Typ_Graph.add_edge (T, T') o 

725 
Typ_Graph.default_node (T', ()) o Typ_Graph.default_node (T, ()) 

33192  726 

727 
fun strongly_connected_sub_nfas nfa = 

39898  728 
add_nfa_to_graph nfa Typ_Graph.empty 
729 
> Typ_Graph.strong_conn 

730 
> map (fn keys => filter (member (op =) keys o fst) nfa) 

33192  731 

38126  732 
fun acyclicity_axiom_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa 
733 
start_T = 

734 
kk_no (kk_intersect 

735 
(loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T) 

736 
KK.Iden) 

38195
a8cef06e0480
Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
blanchet
parents:
38194
diff
changeset

737 
(* Cycle breaking in the bounds takes care of singly recursive datatypes, hence 
a8cef06e0480
Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
blanchet
parents:
38194
diff
changeset

738 
the first equation. *) 
39345  739 
fun acyclicity_axioms_for_datatypes _ [_] = [] 
38195
a8cef06e0480
Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
blanchet
parents:
38194
diff
changeset

740 
 acyclicity_axioms_for_datatypes kk nfas = 
a8cef06e0480
Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
blanchet
parents:
38194
diff
changeset

741 
maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa) nfas 
38126  742 

743 
fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r = 

744 
kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z))) 

745 
fun gt ({kk_subset, kk_join, kk_closure, ...} : kodkod_constrs) z r1 r2 = 

746 
kk_subset r1 (kk_join r2 (kk_closure (KK.Rel (suc_rel_for_atom_seq z)))) 

747 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

748 
fun constr_quadruple ({const = (s, T), delta, epsilon, ...} : constr_spec) = 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

749 
(delta, (epsilon, (num_binder_types T, s))) 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

750 
val constr_ord = 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

751 
prod_ord int_ord (prod_ord int_ord (prod_ord int_ord string_ord)) 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

752 
o pairself constr_quadruple 
38126  753 

754 
fun datatype_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...}, 

755 
{card = card2, self_rec = self_rec2, constrs = constr2, ...}) 

756 
: datatype_spec * datatype_spec) = 

757 
prod_ord int_ord (prod_ord bool_ord int_ord) 

758 
((card1, (self_rec1, length constr1)), 

759 
(card2, (self_rec2, length constr2))) 

760 

761 
(* We must absolutely tabulate "suc" for all datatypes whose selector bounds 

762 
break cycles; otherwise, we may end up with two incompatible symmetry 

763 
breaking orders, leading to spurious models. *) 

764 
fun should_tabulate_suc_for_type dtypes T = 

38127  765 
is_asymmetric_nondatatype T orelse 
38126  766 
case datatype_spec dtypes T of 
767 
SOME {self_rec, ...} => self_rec 

768 
 NONE => false 

769 

770 
fun lex_order_rel_expr (kk as {kk_implies, kk_and, kk_subset, kk_join, ...}) 

771 
dtypes sel_quadruples = 

772 
case sel_quadruples of 

773 
[] => KK.True 

774 
 ((r, Func (Atom _, Atom x), 2), (_, Type (_, [_, T]))) :: sel_quadruples' => 

775 
let val z = (x, should_tabulate_suc_for_type dtypes T) in 

776 
if null sel_quadruples' then 

777 
gt kk z (kk_join (KK.Var (1, 1)) r) (kk_join (KK.Var (1, 0)) r) 

778 
else 

779 
kk_and (kk_subset (kk_join (KK.Var (1, 1)) r) 

780 
(all_ge kk z (kk_join (KK.Var (1, 0)) r))) 

781 
(kk_implies (kk_subset (kk_join (KK.Var (1, 1)) r) 

782 
(kk_join (KK.Var (1, 0)) r)) 

783 
(lex_order_rel_expr kk dtypes sel_quadruples')) 

784 
end 

785 
(* Skip constructors components that aren't atoms, since we cannot compare 

786 
these easily. *) 

787 
 _ :: sel_quadruples' => lex_order_rel_expr kk dtypes sel_quadruples' 

788 

38193  789 
fun is_nil_like_constr_type dtypes T = 
790 
case datatype_spec dtypes T of 

791 
SOME {constrs, ...} => 

792 
(case filter_out (is_self_recursive_constr_type o snd o #const) constrs of 

793 
[{const = (_, T'), ...}] => T = T' 

794 
 _ => false) 

795 
 NONE => false 

38126  796 

797 
fun sym_break_axioms_for_constr_pair hol_ctxt binarize 

39345  798 
(kk as {kk_all, kk_or, kk_implies, kk_and, kk_some, kk_intersect, 
799 
kk_join, ...}) rel_table nfas dtypes 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

800 
(constr_ord, 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

801 
({const = const1 as (_, T1), delta = delta1, epsilon = epsilon1, ...}, 
39345  802 
{const = const2 as (_, _), delta = delta2, epsilon = epsilon2, ...}) 
38191  803 
: constr_spec * constr_spec) = 
38126  804 
let 
805 
val dataT = body_type T1 

806 
val nfa = nfas > find_first (exists (curry (op =) dataT o fst)) > these 

807 
val rec_Ts = nfa > map fst 

808 
fun rec_and_nonrec_sels (x as (_, T)) = 

809 
index_seq 0 (num_sels_for_constr_type T) 

810 
> map (binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x) 

811 
> List.partition (member (op =) rec_Ts o range_type o snd) 

812 
val sel_xs1 = rec_and_nonrec_sels const1 > op @ 

813 
in 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

814 
if constr_ord = EQUAL andalso null sel_xs1 then 
38126  815 
[] 
816 
else 

817 
let 

818 
val z = 

819 
(case #2 (const_triple rel_table (discr_for_constr const1)) of 

820 
Func (Atom x, Formula _) => x 

821 
 R => raise REP ("Nitpick_Kodkod.sym_break_axioms_for_constr_pair", 

822 
[R]), should_tabulate_suc_for_type dtypes dataT) 

823 
val (rec_sel_xs2, nonrec_sel_xs2) = rec_and_nonrec_sels const2 

824 
val sel_xs2 = rec_sel_xs2 @ nonrec_sel_xs2 

825 
fun sel_quadruples2 () = sel_xs2 > map (`(const_triple rel_table)) 

826 
(* If the two constructors are the same, we drop the first selector 

827 
because that one is always checked by the lexicographic order. 

828 
We sometimes also filter out direct subterms, because those are 

829 
already handled by the acyclicity breaking in the bound 

830 
declarations. *) 

831 
fun filter_out_sels no_direct sel_xs = 

832 
apsnd (filter_out 

833 
(fn ((x, _), T) => 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

834 
(constr_ord = EQUAL andalso x = hd sel_xs) orelse 
38126  835 
(T = dataT andalso 
836 
(no_direct orelse not (member (op =) sel_xs x))))) 

837 
fun subterms_r no_direct sel_xs j = 

838 
loop_path_rel_expr kk (map (filter_out_sels no_direct sel_xs) nfa) 

839 
(filter_out (curry (op =) dataT) (map fst nfa)) dataT 

840 
> kk_join (KK.Var (1, j)) 

841 
in 

842 
[kk_all [KK.DeclOne ((1, 0), discr_rel_expr rel_table const1), 

843 
KK.DeclOne ((1, 1), discr_rel_expr rel_table const2)] 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

844 
(kk_implies 
38126  845 
(if delta2 >= epsilon1 then KK.True 
38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

846 
else if delta1 >= epsilon2  1 then KK.False 
38126  847 
else gt kk z (KK.Var (1, 1)) (KK.Var (1, 0))) 
848 
(kk_or 

38193  849 
(if is_nil_like_constr_type dtypes T1 then 
38126  850 
KK.True 
851 
else 

852 
kk_some (kk_intersect (subterms_r false sel_xs2 1) 

853 
(all_ge kk z (KK.Var (1, 0))))) 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

854 
(case constr_ord of 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

855 
EQUAL => 
38126  856 
kk_and 
857 
(lex_order_rel_expr kk dtypes (sel_quadruples2 ())) 

38197  858 
(kk_all [KK.DeclOne ((1, 2), 
859 
subterms_r true sel_xs1 0)] 

860 
(gt kk z (KK.Var (1, 1)) (KK.Var (1, 2)))) 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

861 
 LESS => 
38126  862 
kk_all [KK.DeclOne ((1, 2), 
863 
subterms_r false sel_xs1 0)] 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

864 
(gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))) 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

865 
 GREATER => KK.False)))] 
38126  866 
end 
867 
end 

868 

869 
fun sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas dtypes 

870 
({constrs, ...} : datatype_spec) = 

38194
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

871 
let 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

872 
val constrs = sort constr_ord constrs 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

873 
val constr_pairs = all_distinct_unordered_pairs_of constrs 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

874 
in 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

875 
map (pair EQUAL) (constrs ~~ constrs) @ 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

876 
map (pair LESS) constr_pairs @ 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

877 
map (pair GREATER) (map swap constr_pairs) 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

878 
> maps (sym_break_axioms_for_constr_pair hol_ctxt binarize kk rel_table 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

879 
nfas dtypes) 
a9877c14550f
avoid "<=>" in sym break constraint generation (since these are SATunfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet
parents:
38193
diff
changeset

880 
end 
38126  881 

882 
val min_sym_break_card = 7 

883 

884 
fun sym_break_axioms_for_datatypes hol_ctxt binarize datatype_sym_break kk 

885 
rel_table nfas dtypes = 

886 
if datatype_sym_break = 0 then 

887 
[] 

888 
else 

889 
maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas 

890 
dtypes) 

38196  891 
(dtypes > filter is_datatype_acyclic 
38126  892 
> filter (fn {constrs = [_], ...} => false 
38127  893 
 {card, constrs, ...} => 
894 
card >= min_sym_break_card andalso 

895 
forall (forall (not o is_higher_order_type) 

896 
o binder_types o snd o #const) constrs) 

38126  897 
> (fn dtypes' => 
898 
dtypes' 

899 
> length dtypes' > datatype_sym_break 

38212
a7e92239922f
improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
blanchet
parents:
38197
diff
changeset

900 
? (sort (datatype_ord o swap) 
38126  901 
#> take datatype_sym_break))) 
33192  902 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

903 
fun sel_axiom_for_sel hol_ctxt binarize j0 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

904 
(kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...}) 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

905 
rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec) 
33192  906 
n = 
907 
let 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

908 
val x = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

909 
val (r, R, _) = const_triple rel_table x 
33192  910 
val R2 = dest_Func R > snd 
911 
val z = (epsilon  delta, delta + j0) 

912 
in 

913 
if exclusive then 

914 
kk_n_ary_function kk (Func (Atom z, R2)) r 

915 
else 

34126  916 
let val r' = kk_join (KK.Var (1, 0)) r in 
917 
kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)] 

918 
(kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r) 

919 
(kk_n_ary_function kk R2 r') (kk_no r')) 

33192  920 
end 
921 
end 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

922 
fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table 
33192  923 
(constr as {const, delta, epsilon, explicit_max, ...}) = 
924 
let 

925 
val honors_explicit_max = 

926 
explicit_max < 0 orelse epsilon  delta <= explicit_max 

927 
in 

928 
if explicit_max = 0 then 

929 
[formula_for_bool honors_explicit_max] 

930 
else 

931 
let 

35178  932 
val dom_r = discr_rel_expr rel_table const 
33192  933 
val max_axiom = 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

934 
if honors_explicit_max then 
34126  935 
KK.True 
38121
a9d96531c2ee
gracefully handle the case where no integers occur in the formula and the "max" option is used
blanchet
parents:
37476
diff
changeset

936 
else if bits = 0 orelse 
a9d96531c2ee
gracefully handle the case where no integers occur in the formula and the "max" option is used
blanchet
parents:
37476
diff
changeset

937 
is_twos_complement_representable bits (epsilon  delta) then 
35178  938 
KK.LE (KK.Cardinality dom_r, KK.Num explicit_max) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

939 
else 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

940 
raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr", 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

941 
"\"bits\" value " ^ string_of_int bits ^ 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

942 
" too small for \"max\"") 
33192  943 
in 
944 
max_axiom :: 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

945 
map (sel_axiom_for_sel hol_ctxt binarize j0 kk rel_table dom_r constr) 
33192  946 
(index_seq 0 (num_sels_for_constr_type (snd const))) 
947 
end 

948 
end 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

949 
fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table 
38126  950 
({constrs, ...} : datatype_spec) = 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

951 
maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs 
33192  952 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

953 
fun uniqueness_axiom_for_constr hol_ctxt binarize 
33192  954 
({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...} 
955 
: kodkod_constrs) rel_table ({const, ...} : constr_spec) = 

956 
let 

957 
fun conjunct_for_sel r = 

34126  958 
kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r) 
33192  959 
val num_sels = num_sels_for_constr_type (snd const) 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

960 
val triples = 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

961 
map (const_triple rel_table 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

962 
o binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const) 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

963 
(~1 upto num_sels  1) 
33192  964 
val set_r = triples > hd > #1 
965 
in 

966 
if num_sels = 0 then 

967 
kk_lone set_r 

968 
else 

34126  969 
kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1]) 
33192  970 
(kk_implies 
971 
(fold1 kk_and (map (conjunct_for_sel o #1) (tl triples))) 

34126  972 
(kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1)))) 
33192  973 
end 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

974 
fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table 
38126  975 
({constrs, ...} : datatype_spec) = 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

976 
map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs 
33192  977 

978 
fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon  delta 

979 
fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...}) 

980 
rel_table 

38126  981 
({card, constrs, ...} : datatype_spec) = 
33192  982 
if forall #exclusive constrs then 
983 
[Integer.sum (map effective_constr_max constrs) = card > formula_for_bool] 

984 
else 

985 
let val rs = map (discr_rel_expr rel_table o #const) constrs in 

34126  986 
[kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)), 
33192  987 
kk_disjoint_sets kk rs] 
988 
end 

989 

35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

990 
fun other_axioms_for_datatype _ _ _ _ _ _ {deep = false, ...} = [] 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

991 
 other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

992 
(dtype as {typ, ...}) = 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

993 
let val j0 = offset_of_type ofs typ in 
35190
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

994 
sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table dtype @ 
ce653cc27a94
make sure that Nitpick uses binary notation consistently if "binary_ints" is enabled
blanchet
parents:
35185
diff
changeset

995 
uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table dtype @ 
33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

996 
partition_axioms_for_datatype j0 kk rel_table dtype 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33232
diff
changeset

997 
end 
33192  998 

38126  999 
fun declarative_axioms_for_datatypes hol_ctxt binarize datatype_sym_break bits 
1000 
ofs kk rel_table dtypes = 

1001 
let 

1002 
val nfas = 

1003 
dtypes > map_filter (nfa_entry_for_datatype hol_ctxt binarize kk 

1004 
rel_table dtypes) 

1005 
> strongly_connected_sub_nfas 

1006 
in 

1007 
acyclicity_axioms_for_datatypes kk nfas @ 

1008 
sym_break_axioms_for_datatypes hol_ctxt binarize datatype_sym_break kk 

1009 
rel_table nfas dtypes @ 

1010 
maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table) 

1011 
dtypes 

1012 
end 

33192  1013 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1014 
fun kodkod_formula_from_nut ofs 
33192  1015 
(kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not, 
35072
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

1016 
kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, 
39456  1017 
kk_lone, kk_some, kk_rel_let, kk_rel_if, kk_union, 
35072
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

1018 
kk_difference, kk_intersect, kk_product, kk_join, kk_closure, 
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

1019 
kk_comprehension, kk_project, kk_project_seq, kk_not3, 
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

1020 
kk_nat_less, kk_int_less, ...}) u = 
33192  1021 
let 
1022 
val main_j0 = offset_of_type ofs bool_T 

1023 
val bool_j0 = main_j0 

1024 
val bool_atom_R = Atom (2, main_j0) 

34126  1025 
val false_atom = KK.Atom bool_j0 
1026 
val true_atom = KK.Atom (bool_j0 + 1) 

33192  1027 
fun formula_from_opt_atom polar j0 r = 
1028 
case polar of 

34126  1029 
Neg => kk_not (kk_rel_eq r (KK.Atom j0)) 
1030 
 _ => kk_rel_eq r (KK.Atom (j0 + 1)) 

33192  1031 
val formula_from_atom = formula_from_opt_atom Pos 
1032 
val unpack_formulas = 

1033 
map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1 

1034 
fun kk_vect_set_bool_op connective k r1 r2 = 

1035 
fold1 kk_and (map2 connective (unpack_formulas k r1) 

1036 
(unpack_formulas k r2)) 

1037 
fun to_f u = 

1038 
case rep_of u of 

1039 
Formula polar => 

1040 
(case u of 

34126  1041 
Cst (False, _, _) => KK.False 
1042 
 Cst (True, _, _) => KK.True 

33854
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1043 
 Op1 (Not, _, _, u1) => 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1044 
kk_not (to_f_with_polarity (flip_polarity polar) u1) 
33192  1045 
 Op1 (Finite, _, _, u1) => 
1046 
let val opt1 = is_opt_rep (rep_of u1) in 

1047 
case polar of 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

1048 
Neut => 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

1049 
if opt1 then raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u]) 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

1050 
else KK.True 
33192  1051 
 Pos => formula_for_bool (not opt1) 
34126  1052 
 Neg => KK.True 
33192  1053 
end 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

1054 
 Op1 (IsUnknown, _, _, u1) => kk_no (to_r u1) 
33192  1055 
 Op1 (Cast, _, _, u1) => to_f_with_polarity polar u1 
33854
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1056 
 Op2 (All, _, _, u1, u2) => 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1057 
kk_all (untuple to_decl u1) (to_f_with_polarity polar u2) 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1058 
 Op2 (Exist, _, _, u1, u2) => 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1059 
kk_exist (untuple to_decl u1) (to_f_with_polarity polar u2) 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1060 
 Op2 (Or, _, _, u1, u2) => 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1061 
kk_or (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1062 
 Op2 (And, _, _, u1, u2) => 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1063 
kk_and (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 
33192  1064 
 Op2 (Less, T, Formula polar, u1, u2) => 
1065 
formula_from_opt_atom polar bool_j0 

1066 
(to_r (Op2 (Less, T, Opt bool_atom_R, u1, u2))) 

1067 
 Op2 (Subset, _, _, u1, u2) => 

1068 
let 

1069 
val dom_T = domain_type (type_of u1) 

1070 
val R1 = rep_of u1 

1071 
val R2 = rep_of u2 

1072 
val (dom_R, ran_R) = 

1073 
case min_rep R1 R2 of 

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

1074 
Func Rp => Rp 
33192  1075 
 R => (Atom (card_of_domain_from_rep 2 R, 
1076 
offset_of_type ofs dom_T), 

1077 
if is_opt_rep R then Opt bool_atom_R else Formula Neut) 

1078 
val set_R = Func (dom_R, ran_R) 

1079 
in 

1080 
if not (is_opt_rep ran_R) then 

1081 
to_set_bool_op kk_implies kk_subset u1 u2 

1082 
else if polar = Neut then 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

1083 
raise NUT ("Nitpick_Kodkod.to_f (Subset)", [u]) 
33192  1084 
else 
1085 
let 

33886
cde73f8dbe4e
fix soundness bug in Nitpick's Kodkod generator for the relational composition case
blanchet
parents:
33863
diff
changeset

1086 
(* FIXME: merge with similar code below *) 
33192  1087 
fun set_to_r widen u = 
1088 
if widen then 

1089 
kk_difference (full_rel_for_rep dom_R) 

1090 
(kk_join (to_rep set_R u) false_atom) 

1091 
else 

1092 
kk_join (to_rep set_R u) true_atom 

1093 
val widen1 = (polar = Pos andalso is_opt_rep R1) 

1094 
val widen2 = (polar = Neg andalso is_opt_rep R2) 

1095 
in kk_subset (set_to_r widen1 u1) (set_to_r widen2 u2) end 

1096 
end 

1097 
 Op2 (DefEq, _, _, u1, u2) => 

1098 
(case min_rep (rep_of u1) (rep_of u2) of 

38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

1099 
Formula polar => 
33192  1100 
kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 
1101 
 min_R => 

1102 
let 

1103 
fun args (Op2 (Apply, _, _, u1, u2)) = u2 :: args u1 

1104 
 args (Tuple (_, _, us)) = us 

1105 
 args _ = [] 

1106 
val opt_arg_us = filter (is_opt_rep o rep_of) (args u1) 

1107 
in 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

1108 
if null opt_arg_us orelse not (is_Opt min_R) orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

1109 
is_eval_name u1 then 
33192  1110 
fold (kk_or o (kk_no o to_r)) opt_arg_us 
1111 
(kk_rel_eq (to_rep min_R u1) (to_rep min_R u2)) 

1112 
else 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

1113 
kk_subset (to_rep min_R u1) (to_rep min_R u2) 
33192  1114 
end) 
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1115 
 Op2 (Eq, _, _, u1, u2) => 
33192  1116 
(case min_rep (rep_of u1) (rep_of u2) of 
38190
b02e204b613a
get rid of all "optimizations" regarding "unit" and other cardinality1 types
blanchet
parents:
38182
diff
changeset

1117 
Formula polar => 
33192  1118 
kk_iff (to_f_with_polarity polar u1) (to_f_with_polarity polar u2) 
1119 
 min_R => 

1120 
if is_opt_rep min_R then 

1121 
if polar = Neut then 

1122 
(* continuation of hackish optimization *) 

1123 
kk_rel_eq (to_rep min_R u1) (to_rep min_R u2) 

1124 
else if is_Cst Unrep u1 then 

1125 
to_could_be_unrep (polar = Neg) u2 

1126 
else if is_Cst Unrep u2 then 

1127 
to_could_be_unrep (polar = Neg) u1 

1128 
else 

1129 
let 

1130 
val r1 = to_rep min_R u1 

1131 
val r2 = to_rep min_R u2 

1132 
val both_opt = forall (is_opt_rep o rep_of) [u1, u2] 

1133 
in 

1134 
(if polar = Pos then 

1135 
if not both_opt then 

1136 
kk_rel_eq r1 r2 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

1137 
else if is_lone_rep min_R andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

1138 
arity_of_rep min_R = 1 then 
33192  1139 
kk_some (kk_intersect r1 r2) 
1140 
else 

1141 
raise SAME () 

1142 
else 

1143 
if is_lone_rep min_R then 

1144 
if arity_of_rep min_R = 1 then 

35072
d79308423aea
optimize Nitpick's encoding for other datatypes than list that have a constant constructor like "Nil";
blanchet
parents:
35070
diff
changeset

1145 
kk_lone (kk_union r1 r2) 
33192  1146 
else if not both_opt then 
1147 
(r1, r2) > is_opt_rep (rep_of u2) ? swap 

34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

1148 
> kk_subset 
33192  1149 
else 
1150 
raise SAME () 

1151 
else 

1152 
raise SAME ()) 

1153 
handle SAME () => 

1154 
formula_from_opt_atom polar bool_j0 

1155 
(to_guard [u1, u2] bool_atom_R 

1156 
(rel_expr_from_formula kk bool_atom_R 

1157 
(kk_rel_eq r1 r2))) 

1158 
end 

1159 
else 

1160 
let 

1161 
val r1 = to_rep min_R u1 

1162 
val r2 = to_rep min_R u2 

1163 
in 

1164 
if is_one_rep min_R then 

1165 
let 

1166 
val rs1 = unpack_products r1 

1167 
val rs2 = unpack_products r2 

1168 
in 

34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

1169 
if length rs1 = length rs2 andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

1170 
map KK.arity_of_rel_expr rs1 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34288
diff
changeset

1171 
= map KK.arity_of_rel_expr rs2 then 
33192  1172 
fold1 kk_and (map2 kk_subset rs1 rs2) 
1173 
else 

1174 
kk_subset r1 r2 

1175 
end 

1176 
else 

1177 
kk_rel_eq r1 r2 

1178 
end) 

1179 
 Op2 (Apply, T, _, u1, u2) => 

1180 
(case (polar, rep_of u1) of 

1181 
(Neg, Func (R, Formula Neut)) => kk_subset (to_opt R u2) (to_r u1) 

1182 
 _ => 

1183 
to_f_with_polarity polar 

1184 
(Op2 (Apply, T, Opt (Atom (2, offset_of_type ofs T)), u1, u2))) 

1185 
 Op3 (Let, _, _, u1, u2, u3) => 

33854
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1186 
kk_formula_let [to_expr_assign u1 u2] (to_f_with_polarity polar u3) 
33192  1187 
 Op3 (If, _, _, u1, u2, u3) => 
33854
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1188 
kk_formula_if (to_f u1) (to_f_with_polarity polar u2) 
26a4cb3a7eae
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
blanchet
parents:
33744
diff
changeset

1189 
(to_f_with_polarity polar u3) 
34126  1190 
 FormulaReg (j, _, _) => KK.FormulaReg j 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

1191 
 _ => raise NUT ("Nitpick_Kodkod.to_f", [u])) 
33192  1192 
 Atom (2, j0) => formula_from_atom j0 (to_r u) 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

1193 
 _ => raise NUT ("Nitpick_Kodkod.to_f", [u]) 
33192  1194 
and to_f_with_polarity polar u = 
1195 
case rep_of u of 

1196 
Formula _ => to_f u 

1197 
 Atom (2, j0) => formula_from_atom j0 (to_r u) 

1198 
 Opt (Atom (2, j0)) => formula_from_opt_atom polar j0 (to_r u) 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

1199 
 _ => raise NUT ("Nitpick_Kodkod.to_f_with_polarity", [u]) 
33192  1200 
and to_r u = 
1201 
case u of 

1202 
Cst (False, _, Atom _) => false_atom 

1203 
 Cst (True, _, Atom _) => true_atom 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1204 
 Cst (Iden, _, Func (Struct [R1, R2], Formula Neut)) => 
33192  1205 
if R1 = R2 andalso arity_of_rep R1 = 1 then 
34126  1206 
kk_intersect KK.Iden (kk_product (full_rel_for_rep R1) KK.Univ) 
33192  1207 
else 
1208 
let 

1209 
val schema1 = atom_schema_of_rep R1 

1210 
val schema2 = atom_schema_of_rep R2 

1211 
val arity1 = length schema1 

1212 
val arity2 = length schema2 

1213 
val r1 = fold1 kk_product (unary_var_seq 0 arity1) 

1214 
val r2 = fold1 kk_product (unary_var_seq arity1 arity2) 

1215 
val min_R = min_rep R1 R2 

1216 
in 

1217 
kk_comprehension 

1218 
(decls_for_atom_schema 0 (schema1 @ schema2)) 

1219 
(kk_rel_eq (rel_expr_from_rel_expr kk min_R R1 r1) 

1220 
(rel_expr_from_rel_expr kk min_R R2 r2)) 

1221 
end 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1222 
 Cst (Iden, _, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

1223 
 Cst (Iden, T as Type (@{type_name fun}, [T1, _]), R as Func (R1, _)) => 
33192  1224 
to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut))) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1225 
 Cst (Num j, T, R) => 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1226 
if is_word_type T then 
34126  1227 
atom_from_int_expr kk T R (KK.Num j) 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1228 
else if T = int_T then 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1229 
case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of 
34126  1230 
~1 => if is_opt_rep R then KK.None 
33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

1231 
else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u]) 
34126  1232 
 j' => KK.Atom j' 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1233 
else 
34126  1234 
if j < card_of_rep R then KK.Atom (j + offset_of_type ofs T) 
1235 
else if is_opt_rep R then KK.None 

34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1236 
else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u]) 
33192  1237 
 Cst (Unknown, _, R) => empty_rel_for_rep R 
1238 
 Cst (Unrep, _, R) => empty_rel_for_rep R 

34126  1239 
 Cst (Suc, T as @{typ "unsigned_bit word => unsigned_bit word"}, R) => 
1240 
to_bit_word_unary_op T R (curry KK.Add (KK.Num 1)) 

1241 
 Cst (Suc, @{typ "nat => nat"}, Func (Atom x, _)) => 

1242 
kk_intersect (KK.Rel suc_rel) (kk_product KK.Univ (KK.AtomSeq x)) 

35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset

1243 
 Cst (Suc, _, Func (Atom _, _)) => KK.Rel suc_rel 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

1244 
 Cst (Add, Type (_, [@{typ nat}, _]), _) => KK.Rel nat_add_rel 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

1245 
 Cst (Add, Type (_, [@{typ int}, _]), _) => KK.Rel int_add_rel 
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

1246 
 Cst (Add, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) => 
34126  1247 
to_bit_word_binary_op T R NONE (SOME (curry KK.Add)) 
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35407
diff
changeset

1248 
 Cst (Add, T as Type (_, [@{typ "signed_bit word"}, _]), R) => 
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

1249 
to_bit_word_binary_op T R 
