author | wenzelm |
Sat, 16 Jul 2011 20:52:41 +0200 | |
changeset 43850 | 7f2cbc713344 |
parent 43085 | 0a2f5b86bdd7 |
child 47490 | f4348634595b |
permissions | -rw-r--r-- |
33982 | 1 |
(* Title: HOL/Tools/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 |
|
39456 | 5 |
ML interface for Kodkod. |
33192 | 6 |
*) |
7 |
||
8 |
signature KODKOD = |
|
9 |
sig |
|
10 |
type n_ary_index = int * int |
|
11 |
type setting = string * string |
|
12 |
||
13 |
datatype tuple = |
|
14 |
Tuple of int list | |
|
15 |
TupleIndex of n_ary_index | |
|
16 |
TupleReg of n_ary_index |
|
17 |
||
18 |
datatype tuple_set = |
|
19 |
TupleUnion of tuple_set * tuple_set | |
|
20 |
TupleDifference of tuple_set * tuple_set | |
|
21 |
TupleIntersect of tuple_set * tuple_set | |
|
22 |
TupleProduct of tuple_set * tuple_set | |
|
23 |
TupleProject of tuple_set * int | |
|
24 |
TupleSet of tuple list | |
|
25 |
TupleRange of tuple * tuple | |
|
26 |
TupleArea of tuple * tuple | |
|
27 |
TupleAtomSeq of int * int | |
|
28 |
TupleSetReg of n_ary_index |
|
29 |
||
30 |
datatype tuple_assign = |
|
31 |
AssignTuple of n_ary_index * tuple | |
|
32 |
AssignTupleSet of n_ary_index * tuple_set |
|
33 |
||
34 |
type bound = (n_ary_index * string) list * tuple_set list |
|
35 |
type int_bound = int option * tuple_set list |
|
36 |
||
37 |
datatype formula = |
|
38 |
All of decl list * formula | |
|
39 |
Exist of decl list * formula | |
|
40 |
FormulaLet of expr_assign list * formula | |
|
41 |
FormulaIf of formula * formula * formula | |
|
42 |
Or of formula * formula | |
|
43 |
Iff of formula * formula | |
|
44 |
Implies of formula * formula | |
|
45 |
And of formula * formula | |
|
46 |
Not of formula | |
|
47 |
Acyclic of n_ary_index | |
|
48 |
Function of n_ary_index * rel_expr * rel_expr | |
|
49 |
Functional of n_ary_index * rel_expr * rel_expr | |
|
38126 | 50 |
TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr | |
33192 | 51 |
Subset of rel_expr * rel_expr | |
52 |
RelEq of rel_expr * rel_expr | |
|
53 |
IntEq of int_expr * int_expr | |
|
54 |
LT of int_expr * int_expr | |
|
55 |
LE of int_expr * int_expr | |
|
56 |
No of rel_expr | |
|
57 |
Lone of rel_expr | |
|
58 |
One of rel_expr | |
|
59 |
Some of rel_expr | |
|
60 |
False | |
|
61 |
True | |
|
62 |
FormulaReg of int |
|
63 |
and rel_expr = |
|
64 |
RelLet of expr_assign list * rel_expr | |
|
65 |
RelIf of formula * rel_expr * rel_expr | |
|
66 |
Union of rel_expr * rel_expr | |
|
67 |
Difference of rel_expr * rel_expr | |
|
68 |
Override of rel_expr * rel_expr | |
|
69 |
Intersect of rel_expr * rel_expr | |
|
70 |
Product of rel_expr * rel_expr | |
|
71 |
IfNo of rel_expr * rel_expr | |
|
72 |
Project of rel_expr * int_expr list | |
|
73 |
Join of rel_expr * rel_expr | |
|
74 |
Closure of rel_expr | |
|
75 |
ReflexiveClosure of rel_expr | |
|
76 |
Transpose of rel_expr | |
|
77 |
Comprehension of decl list * formula | |
|
78 |
Bits of int_expr | |
|
79 |
Int of int_expr | |
|
80 |
Iden | |
|
81 |
Ints | |
|
82 |
None | |
|
83 |
Univ | |
|
84 |
Atom of int | |
|
85 |
AtomSeq of int * int | |
|
86 |
Rel of n_ary_index | |
|
87 |
Var of n_ary_index | |
|
88 |
RelReg of n_ary_index |
|
89 |
and int_expr = |
|
90 |
Sum of decl list * int_expr | |
|
91 |
IntLet of expr_assign list * int_expr | |
|
92 |
IntIf of formula * int_expr * int_expr | |
|
93 |
SHL of int_expr * int_expr | |
|
94 |
SHA of int_expr * int_expr | |
|
95 |
SHR of int_expr * int_expr | |
|
96 |
Add of int_expr * int_expr | |
|
97 |
Sub of int_expr * int_expr | |
|
98 |
Mult of int_expr * int_expr | |
|
99 |
Div of int_expr * int_expr | |
|
100 |
Mod of int_expr * int_expr | |
|
101 |
Cardinality of rel_expr | |
|
102 |
SetSum of rel_expr | |
|
103 |
BitOr of int_expr * int_expr | |
|
104 |
BitXor of int_expr * int_expr | |
|
105 |
BitAnd of int_expr * int_expr | |
|
106 |
BitNot of int_expr | |
|
107 |
Neg of int_expr | |
|
108 |
Absolute of int_expr | |
|
109 |
Signum of int_expr | |
|
110 |
Num of int | |
|
111 |
IntReg of int |
|
112 |
and decl = |
|
113 |
DeclNo of n_ary_index * rel_expr | |
|
114 |
DeclLone of n_ary_index * rel_expr | |
|
115 |
DeclOne of n_ary_index * rel_expr | |
|
116 |
DeclSome of n_ary_index * rel_expr | |
|
117 |
DeclSet of n_ary_index * rel_expr |
|
118 |
and expr_assign = |
|
119 |
AssignFormulaReg of int * formula | |
|
120 |
AssignRelReg of n_ary_index * rel_expr | |
|
121 |
AssignIntReg of int * int_expr |
|
122 |
||
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
123 |
type 'a fold_expr_funcs = |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
124 |
{formula_func: formula -> 'a -> 'a, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
125 |
rel_expr_func: rel_expr -> 'a -> 'a, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
126 |
int_expr_func: int_expr -> 'a -> 'a} |
33192 | 127 |
|
128 |
val fold_formula : 'a fold_expr_funcs -> formula -> 'a -> 'a |
|
129 |
val fold_rel_expr : 'a fold_expr_funcs -> rel_expr -> 'a -> 'a |
|
130 |
val fold_int_expr : 'a fold_expr_funcs -> int_expr -> 'a -> 'a |
|
131 |
val fold_decl : 'a fold_expr_funcs -> decl -> 'a -> 'a |
|
132 |
val fold_expr_assign : 'a fold_expr_funcs -> expr_assign -> 'a -> 'a |
|
133 |
||
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
134 |
type 'a fold_tuple_funcs = |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
135 |
{tuple_func: tuple -> 'a -> 'a, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
136 |
tuple_set_func: tuple_set -> 'a -> 'a} |
33192 | 137 |
|
138 |
val fold_tuple : 'a fold_tuple_funcs -> tuple -> 'a -> 'a |
|
139 |
val fold_tuple_set : 'a fold_tuple_funcs -> tuple_set -> 'a -> 'a |
|
140 |
val fold_tuple_assign : 'a fold_tuple_funcs -> tuple_assign -> 'a -> 'a |
|
141 |
val fold_bound : |
|
142 |
'a fold_expr_funcs -> 'a fold_tuple_funcs -> bound -> 'a -> 'a |
|
143 |
val fold_int_bound : 'a fold_tuple_funcs -> int_bound -> 'a -> 'a |
|
144 |
||
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
145 |
type problem = |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
146 |
{comment: string, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
147 |
settings: setting list, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
148 |
univ_card: int, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
149 |
tuple_assigns: tuple_assign list, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
150 |
bounds: bound list, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
151 |
int_bounds: int_bound list, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
152 |
expr_assigns: expr_assign list, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
153 |
formula: formula} |
33192 | 154 |
|
155 |
type raw_bound = n_ary_index * int list list |
|
156 |
||
157 |
datatype outcome = |
|
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35695
diff
changeset
|
158 |
JavaNotInstalled | |
38516
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38198
diff
changeset
|
159 |
JavaTooOld | |
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35695
diff
changeset
|
160 |
KodkodiNotInstalled | |
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset
|
161 |
Normal of (int * raw_bound list) list * int list * string | |
33192 | 162 |
TimedOut of int list | |
163 |
Error of string * int list |
|
164 |
||
165 |
exception SYNTAX of string * string |
|
166 |
||
167 |
val max_arity : int -> int |
|
168 |
val arity_of_rel_expr : rel_expr -> int |
|
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35079
diff
changeset
|
169 |
val is_problem_trivially_false : problem -> bool |
35814 | 170 |
val problems_equivalent : problem * problem -> bool |
33192 | 171 |
val solve_any_problem : |
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
40743
diff
changeset
|
172 |
bool -> bool -> Time.time option -> int -> int -> problem list -> outcome |
33192 | 173 |
end; |
174 |
||
175 |
structure Kodkod : KODKOD = |
|
176 |
struct |
|
177 |
||
178 |
type n_ary_index = int * int |
|
179 |
||
180 |
type setting = string * string |
|
181 |
||
182 |
datatype tuple = |
|
183 |
Tuple of int list | |
|
184 |
TupleIndex of n_ary_index | |
|
185 |
TupleReg of n_ary_index |
|
186 |
||
187 |
datatype tuple_set = |
|
188 |
TupleUnion of tuple_set * tuple_set | |
|
189 |
TupleDifference of tuple_set * tuple_set | |
|
190 |
TupleIntersect of tuple_set * tuple_set | |
|
191 |
TupleProduct of tuple_set * tuple_set | |
|
192 |
TupleProject of tuple_set * int | |
|
193 |
TupleSet of tuple list | |
|
194 |
TupleRange of tuple * tuple | |
|
195 |
TupleArea of tuple * tuple | |
|
196 |
TupleAtomSeq of int * int | |
|
197 |
TupleSetReg of n_ary_index |
|
198 |
||
199 |
datatype tuple_assign = |
|
200 |
AssignTuple of n_ary_index * tuple | |
|
201 |
AssignTupleSet of n_ary_index * tuple_set |
|
202 |
||
203 |
type bound = (n_ary_index * string) list * tuple_set list |
|
204 |
type int_bound = int option * tuple_set list |
|
205 |
||
206 |
datatype formula = |
|
207 |
All of decl list * formula | |
|
208 |
Exist of decl list * formula | |
|
209 |
FormulaLet of expr_assign list * formula | |
|
210 |
FormulaIf of formula * formula * formula | |
|
211 |
Or of formula * formula | |
|
212 |
Iff of formula * formula | |
|
213 |
Implies of formula * formula | |
|
214 |
And of formula * formula | |
|
215 |
Not of formula | |
|
216 |
Acyclic of n_ary_index | |
|
217 |
Function of n_ary_index * rel_expr * rel_expr | |
|
218 |
Functional of n_ary_index * rel_expr * rel_expr | |
|
38126 | 219 |
TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr | |
33192 | 220 |
Subset of rel_expr * rel_expr | |
221 |
RelEq of rel_expr * rel_expr | |
|
222 |
IntEq of int_expr * int_expr | |
|
223 |
LT of int_expr * int_expr | |
|
224 |
LE of int_expr * int_expr | |
|
225 |
No of rel_expr | |
|
226 |
Lone of rel_expr | |
|
227 |
One of rel_expr | |
|
228 |
Some of rel_expr | |
|
229 |
False | |
|
230 |
True | |
|
231 |
FormulaReg of int |
|
232 |
and rel_expr = |
|
233 |
RelLet of expr_assign list * rel_expr | |
|
234 |
RelIf of formula * rel_expr * rel_expr | |
|
235 |
Union of rel_expr * rel_expr | |
|
236 |
Difference of rel_expr * rel_expr | |
|
237 |
Override of rel_expr * rel_expr | |
|
238 |
Intersect of rel_expr * rel_expr | |
|
239 |
Product of rel_expr * rel_expr | |
|
240 |
IfNo of rel_expr * rel_expr | |
|
241 |
Project of rel_expr * int_expr list | |
|
242 |
Join of rel_expr * rel_expr | |
|
243 |
Closure of rel_expr | |
|
244 |
ReflexiveClosure of rel_expr | |
|
245 |
Transpose of rel_expr | |
|
246 |
Comprehension of decl list * formula | |
|
247 |
Bits of int_expr | |
|
248 |
Int of int_expr | |
|
249 |
Iden | |
|
250 |
Ints | |
|
251 |
None | |
|
252 |
Univ | |
|
253 |
Atom of int | |
|
254 |
AtomSeq of int * int | |
|
255 |
Rel of n_ary_index | |
|
256 |
Var of n_ary_index | |
|
257 |
RelReg of n_ary_index |
|
258 |
and int_expr = |
|
259 |
Sum of decl list * int_expr | |
|
260 |
IntLet of expr_assign list * int_expr | |
|
261 |
IntIf of formula * int_expr * int_expr | |
|
262 |
SHL of int_expr * int_expr | |
|
263 |
SHA of int_expr * int_expr | |
|
264 |
SHR of int_expr * int_expr | |
|
265 |
Add of int_expr * int_expr | |
|
266 |
Sub of int_expr * int_expr | |
|
267 |
Mult of int_expr * int_expr | |
|
268 |
Div of int_expr * int_expr | |
|
269 |
Mod of int_expr * int_expr | |
|
270 |
Cardinality of rel_expr | |
|
271 |
SetSum of rel_expr | |
|
272 |
BitOr of int_expr * int_expr | |
|
273 |
BitXor of int_expr * int_expr | |
|
274 |
BitAnd of int_expr * int_expr | |
|
275 |
BitNot of int_expr | |
|
276 |
Neg of int_expr | |
|
277 |
Absolute of int_expr | |
|
278 |
Signum of int_expr | |
|
279 |
Num of int | |
|
280 |
IntReg of int |
|
281 |
and decl = |
|
282 |
DeclNo of n_ary_index * rel_expr | |
|
283 |
DeclLone of n_ary_index * rel_expr | |
|
284 |
DeclOne of n_ary_index * rel_expr | |
|
285 |
DeclSome of n_ary_index * rel_expr | |
|
286 |
DeclSet of n_ary_index * rel_expr |
|
287 |
and expr_assign = |
|
288 |
AssignFormulaReg of int * formula | |
|
289 |
AssignRelReg of n_ary_index * rel_expr | |
|
290 |
AssignIntReg of int * int_expr |
|
291 |
||
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
292 |
type problem = |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
293 |
{comment: string, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
294 |
settings: setting list, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
295 |
univ_card: int, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
296 |
tuple_assigns: tuple_assign list, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
297 |
bounds: bound list, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
298 |
int_bounds: int_bound list, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
299 |
expr_assigns: expr_assign list, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
300 |
formula: formula} |
33192 | 301 |
|
302 |
type raw_bound = n_ary_index * int list list |
|
303 |
||
304 |
datatype outcome = |
|
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35695
diff
changeset
|
305 |
JavaNotInstalled | |
38516
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38198
diff
changeset
|
306 |
JavaTooOld | |
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35695
diff
changeset
|
307 |
KodkodiNotInstalled | |
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset
|
308 |
Normal of (int * raw_bound list) list * int list * string | |
33192 | 309 |
TimedOut of int list | |
310 |
Error of string * int list |
|
311 |
||
312 |
exception SYNTAX of string * string |
|
313 |
||
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
314 |
type 'a fold_expr_funcs = |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
315 |
{formula_func: formula -> 'a -> 'a, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
316 |
rel_expr_func: rel_expr -> 'a -> 'a, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
317 |
int_expr_func: int_expr -> 'a -> 'a} |
33192 | 318 |
|
38126 | 319 |
fun is_new_kodkodi_version () = |
320 |
case getenv "KODKODI_VERSION" of |
|
321 |
"" => false |
|
322 |
| s => dict_ord int_ord (s |> space_explode "." |
|
38130 | 323 |
|> map (the_default 0 o Int.fromString), |
38126 | 324 |
[1, 2, 13]) = GREATER |
325 |
||
326 |
(** Auxiliary functions on Kodkod problems **) |
|
35718 | 327 |
|
33192 | 328 |
fun fold_formula (F : 'a fold_expr_funcs) formula = |
329 |
case formula of |
|
330 |
All (ds, f) => fold (fold_decl F) ds #> fold_formula F f |
|
331 |
| Exist (ds, f) => fold (fold_decl F) ds #> fold_formula F f |
|
332 |
| FormulaLet (bs, f) => fold (fold_expr_assign F) bs #> fold_formula F f |
|
333 |
| FormulaIf (f, f1, f2) => |
|
334 |
fold_formula F f #> fold_formula F f1 #> fold_formula F f2 |
|
335 |
| Or (f1, f2) => fold_formula F f1 #> fold_formula F f2 |
|
336 |
| Iff (f1, f2) => fold_formula F f1 #> fold_formula F f2 |
|
337 |
| Implies (f1, f2) => fold_formula F f1 #> fold_formula F f2 |
|
338 |
| And (f1, f2) => fold_formula F f1 #> fold_formula F f2 |
|
339 |
| Not f => fold_formula F f |
|
340 |
| Acyclic x => fold_rel_expr F (Rel x) |
|
341 |
| Function (x, r1, r2) => |
|
342 |
fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
343 |
| Functional (x, r1, r2) => |
|
344 |
fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
38126 | 345 |
| TotalOrdering (x, r1, r2, r3) => |
346 |
fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
347 |
#> fold_rel_expr F r3 |
|
33192 | 348 |
| Subset (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
349 |
| RelEq (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
350 |
| IntEq (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
351 |
| LT (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
352 |
| LE (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
353 |
| No r => fold_rel_expr F r |
|
354 |
| Lone r => fold_rel_expr F r |
|
355 |
| One r => fold_rel_expr F r |
|
356 |
| Some r => fold_rel_expr F r |
|
357 |
| False => #formula_func F formula |
|
358 |
| True => #formula_func F formula |
|
359 |
| FormulaReg _ => #formula_func F formula |
|
360 |
and fold_rel_expr F rel_expr = |
|
361 |
case rel_expr of |
|
362 |
RelLet (bs, r) => fold (fold_expr_assign F) bs #> fold_rel_expr F r |
|
363 |
| RelIf (f, r1, r2) => |
|
364 |
fold_formula F f #> fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
365 |
| Union (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
366 |
| Difference (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
367 |
| Override (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
368 |
| Intersect (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
369 |
| Product (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
370 |
| IfNo (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
371 |
| Project (r1, is) => fold_rel_expr F r1 #> fold (fold_int_expr F) is |
|
372 |
| Join (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 |
|
373 |
| Closure r => fold_rel_expr F r |
|
374 |
| ReflexiveClosure r => fold_rel_expr F r |
|
375 |
| Transpose r => fold_rel_expr F r |
|
376 |
| Comprehension (ds, f) => fold (fold_decl F) ds #> fold_formula F f |
|
377 |
| Bits i => fold_int_expr F i |
|
378 |
| Int i => fold_int_expr F i |
|
379 |
| Iden => #rel_expr_func F rel_expr |
|
380 |
| Ints => #rel_expr_func F rel_expr |
|
381 |
| None => #rel_expr_func F rel_expr |
|
382 |
| Univ => #rel_expr_func F rel_expr |
|
383 |
| Atom _ => #rel_expr_func F rel_expr |
|
384 |
| AtomSeq _ => #rel_expr_func F rel_expr |
|
385 |
| Rel _ => #rel_expr_func F rel_expr |
|
386 |
| Var _ => #rel_expr_func F rel_expr |
|
387 |
| RelReg _ => #rel_expr_func F rel_expr |
|
388 |
and fold_int_expr F int_expr = |
|
389 |
case int_expr of |
|
390 |
Sum (ds, i) => fold (fold_decl F) ds #> fold_int_expr F i |
|
391 |
| IntLet (bs, i) => fold (fold_expr_assign F) bs #> fold_int_expr F i |
|
392 |
| IntIf (f, i1, i2) => |
|
393 |
fold_formula F f #> fold_int_expr F i1 #> fold_int_expr F i2 |
|
394 |
| SHL (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
395 |
| SHA (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
396 |
| SHR (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
397 |
| Add (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
398 |
| Sub (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
399 |
| Mult (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
400 |
| Div (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
401 |
| Mod (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
402 |
| Cardinality r => fold_rel_expr F r |
|
403 |
| SetSum r => fold_rel_expr F r |
|
404 |
| BitOr (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
405 |
| BitXor (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
406 |
| BitAnd (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 |
|
407 |
| BitNot i => fold_int_expr F i |
|
408 |
| Neg i => fold_int_expr F i |
|
409 |
| Absolute i => fold_int_expr F i |
|
410 |
| Signum i => fold_int_expr F i |
|
411 |
| Num _ => #int_expr_func F int_expr |
|
412 |
| IntReg _ => #int_expr_func F int_expr |
|
413 |
and fold_decl F decl = |
|
414 |
case decl of |
|
415 |
DeclNo (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r |
|
416 |
| DeclLone (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r |
|
417 |
| DeclOne (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r |
|
418 |
| DeclSome (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r |
|
419 |
| DeclSet (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r |
|
420 |
and fold_expr_assign F assign = |
|
421 |
case assign of |
|
422 |
AssignFormulaReg (x, f) => fold_formula F (FormulaReg x) #> fold_formula F f |
|
423 |
| AssignRelReg (x, r) => fold_rel_expr F (RelReg x) #> fold_rel_expr F r |
|
424 |
| AssignIntReg (x, i) => fold_int_expr F (IntReg x) #> fold_int_expr F i |
|
425 |
||
36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
426 |
type 'a fold_tuple_funcs = |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
427 |
{tuple_func: tuple -> 'a -> 'a, |
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset
|
428 |
tuple_set_func: tuple_set -> 'a -> 'a} |
33192 | 429 |
|
430 |
fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F |
|
431 |
fun fold_tuple_set F tuple_set = |
|
432 |
case tuple_set of |
|
433 |
TupleUnion (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 |
|
434 |
| TupleDifference (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 |
|
435 |
| TupleIntersect (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 |
|
436 |
| TupleProduct (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 |
|
437 |
| TupleProject (ts, _) => fold_tuple_set F ts |
|
438 |
| TupleSet ts => fold (fold_tuple F) ts |
|
439 |
| TupleRange (t1, t2) => fold_tuple F t1 #> fold_tuple F t2 |
|
440 |
| TupleArea (t1, t2) => fold_tuple F t1 #> fold_tuple F t2 |
|
441 |
| TupleAtomSeq _ => #tuple_set_func F tuple_set |
|
442 |
| TupleSetReg _ => #tuple_set_func F tuple_set |
|
443 |
fun fold_tuple_assign F assign = |
|
444 |
case assign of |
|
445 |
AssignTuple (x, t) => fold_tuple F (TupleReg x) #> fold_tuple F t |
|
446 |
| AssignTupleSet (x, ts) => |
|
447 |
fold_tuple_set F (TupleSetReg x) #> fold_tuple_set F ts |
|
448 |
fun fold_bound expr_F tuple_F (zs, tss) = |
|
449 |
fold (fold_rel_expr expr_F) (map (Rel o fst) zs) |
|
450 |
#> fold (fold_tuple_set tuple_F) tss |
|
451 |
fun fold_int_bound F (_, tss) = fold (fold_tuple_set F) tss |
|
452 |
||
453 |
fun max_arity univ_card = floor (Math.ln 2147483647.0 |
|
454 |
/ Math.ln (Real.fromInt univ_card)) |
|
455 |
fun arity_of_rel_expr (RelLet (_, r)) = arity_of_rel_expr r |
|
456 |
| arity_of_rel_expr (RelIf (_, r1, _)) = arity_of_rel_expr r1 |
|
457 |
| arity_of_rel_expr (Union (r1, _)) = arity_of_rel_expr r1 |
|
458 |
| arity_of_rel_expr (Difference (r1, _)) = arity_of_rel_expr r1 |
|
459 |
| arity_of_rel_expr (Override (r1, _)) = arity_of_rel_expr r1 |
|
460 |
| arity_of_rel_expr (Intersect (r1, _)) = arity_of_rel_expr r1 |
|
461 |
| arity_of_rel_expr (Product (r1, r2)) = sum_arities_of_rel_exprs r1 r2 |
|
462 |
| arity_of_rel_expr (IfNo (r1, _)) = arity_of_rel_expr r1 |
|
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35187
diff
changeset
|
463 |
| arity_of_rel_expr (Project (_, is)) = length is |
33192 | 464 |
| arity_of_rel_expr (Join (r1, r2)) = sum_arities_of_rel_exprs r1 r2 - 2 |
465 |
| arity_of_rel_expr (Closure _) = 2 |
|
466 |
| arity_of_rel_expr (ReflexiveClosure _) = 2 |
|
467 |
| arity_of_rel_expr (Transpose _) = 2 |
|
468 |
| arity_of_rel_expr (Comprehension (ds, _)) = |
|
469 |
fold (curry op + o arity_of_decl) ds 0 |
|
470 |
| arity_of_rel_expr (Bits _) = 1 |
|
471 |
| arity_of_rel_expr (Int _) = 1 |
|
472 |
| arity_of_rel_expr Iden = 2 |
|
473 |
| arity_of_rel_expr Ints = 1 |
|
474 |
| arity_of_rel_expr None = 1 |
|
475 |
| arity_of_rel_expr Univ = 1 |
|
476 |
| arity_of_rel_expr (Atom _) = 1 |
|
477 |
| arity_of_rel_expr (AtomSeq _) = 1 |
|
478 |
| arity_of_rel_expr (Rel (n, _)) = n |
|
479 |
| arity_of_rel_expr (Var (n, _)) = n |
|
480 |
| arity_of_rel_expr (RelReg (n, _)) = n |
|
481 |
and sum_arities_of_rel_exprs r1 r2 = arity_of_rel_expr r1 + arity_of_rel_expr r2 |
|
482 |
and arity_of_decl (DeclNo ((n, _), _)) = n |
|
483 |
| arity_of_decl (DeclLone ((n, _), _)) = n |
|
484 |
| arity_of_decl (DeclOne ((n, _), _)) = n |
|
485 |
| arity_of_decl (DeclSome ((n, _), _)) = n |
|
486 |
| arity_of_decl (DeclSet ((n, _), _)) = n |
|
487 |
||
35185
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35079
diff
changeset
|
488 |
fun is_problem_trivially_false ({formula = False, ...} : problem) = true |
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35079
diff
changeset
|
489 |
| is_problem_trivially_false _ = false |
9b8f351cced6
added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
blanchet
parents:
35079
diff
changeset
|
490 |
|
35814 | 491 |
val chop_solver = take 2 o space_explode "," |
33192 | 492 |
|
35814 | 493 |
fun settings_equivalent ([], []) = true |
494 |
| settings_equivalent ((key1, value1) :: settings1, |
|
495 |
(key2, value2) :: settings2) = |
|
496 |
key1 = key2 andalso |
|
497 |
(value1 = value2 orelse key1 = "delay" orelse |
|
498 |
(key1 = "solver" andalso chop_solver value1 = chop_solver value2)) andalso |
|
499 |
settings_equivalent (settings1, settings2) |
|
500 |
| settings_equivalent _ = false |
|
501 |
||
502 |
fun problems_equivalent (p1 : problem, p2 : problem) = |
|
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
503 |
#univ_card p1 = #univ_card p2 andalso |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
504 |
#formula p1 = #formula p2 andalso |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
505 |
#bounds p1 = #bounds p2 andalso |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
506 |
#expr_assigns p1 = #expr_assigns p2 andalso |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
507 |
#tuple_assigns p1 = #tuple_assigns p2 andalso |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
508 |
#int_bounds p1 = #int_bounds p2 andalso |
35814 | 509 |
settings_equivalent (#settings p1, #settings p2) |
33192 | 510 |
|
35718 | 511 |
(** Serialization of problem **) |
34998 | 512 |
|
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
513 |
fun base_name j = |
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
514 |
if j < 0 then string_of_int (~j - 1) ^ "'" else string_of_int j |
33192 | 515 |
|
516 |
fun n_ary_name (1, j) prefix _ _ = prefix ^ base_name j |
|
517 |
| n_ary_name (2, j) _ prefix _ = prefix ^ base_name j |
|
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
518 |
| n_ary_name (n, j) _ _ prefix = prefix ^ string_of_int n ^ "_" ^ base_name j |
33192 | 519 |
|
520 |
fun atom_name j = "A" ^ base_name j |
|
521 |
fun atom_seq_name (k, 0) = "u" ^ base_name k |
|
522 |
| atom_seq_name (k, j0) = "u" ^ base_name k ^ "@" ^ base_name j0 |
|
523 |
fun formula_reg_name j = "$f" ^ base_name j |
|
524 |
fun rel_reg_name j = "$e" ^ base_name j |
|
525 |
fun int_reg_name j = "$i" ^ base_name j |
|
526 |
||
527 |
fun tuple_name x = n_ary_name x "A" "P" "T" |
|
38126 | 528 |
fun rel_name new_kodkodi (n, j) = |
529 |
n_ary_name (n, if new_kodkodi then j |
|
530 |
else if j >= 0 then 2 * j |
|
531 |
else 2 * ~j - 1) "s" "r" "m" |
|
33192 | 532 |
fun var_name x = n_ary_name x "S" "R" "M" |
533 |
fun tuple_reg_name x = n_ary_name x "$A" "$P" "$T" |
|
534 |
fun tuple_set_reg_name x = n_ary_name x "$a" "$p" "$t" |
|
535 |
||
536 |
fun inline_comment "" = "" |
|
537 |
| inline_comment comment = |
|
538 |
" /* " ^ translate_string (fn "\n" => " " | "*" => "* " | s => s) comment ^ |
|
539 |
" */" |
|
540 |
fun block_comment "" = "" |
|
541 |
| block_comment comment = prefix_lines "// " comment ^ "\n" |
|
542 |
||
38126 | 543 |
fun commented_rel_name new_kodkodi (x, s) = |
544 |
rel_name new_kodkodi x ^ inline_comment s |
|
33192 | 545 |
|
546 |
fun string_for_tuple (Tuple js) = "[" ^ commas (map atom_name js) ^ "]" |
|
547 |
| string_for_tuple (TupleIndex x) = tuple_name x |
|
548 |
| string_for_tuple (TupleReg x) = tuple_reg_name x |
|
549 |
||
550 |
val no_prec = 100 |
|
551 |
val prec_TupleUnion = 1 |
|
552 |
val prec_TupleIntersect = 2 |
|
553 |
val prec_TupleProduct = 3 |
|
554 |
val prec_TupleProject = 4 |
|
555 |
||
556 |
fun precedence_ts (TupleUnion _) = prec_TupleUnion |
|
557 |
| precedence_ts (TupleDifference _) = prec_TupleUnion |
|
558 |
| precedence_ts (TupleIntersect _) = prec_TupleIntersect |
|
559 |
| precedence_ts (TupleProduct _) = prec_TupleProduct |
|
560 |
| precedence_ts (TupleProject _) = prec_TupleProject |
|
561 |
| precedence_ts _ = no_prec |
|
562 |
||
563 |
fun string_for_tuple_set tuple_set = |
|
564 |
let |
|
565 |
fun sub tuple_set outer_prec = |
|
566 |
let |
|
567 |
val prec = precedence_ts tuple_set |
|
568 |
val need_parens = (prec < outer_prec) |
|
569 |
in |
|
570 |
(if need_parens then "(" else "") ^ |
|
571 |
(case tuple_set of |
|
572 |
TupleUnion (ts1, ts2) => sub ts1 prec ^ " + " ^ sub ts2 (prec + 1) |
|
573 |
| TupleDifference (ts1, ts2) => |
|
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35187
diff
changeset
|
574 |
sub ts1 prec ^ " - " ^ sub ts2 (prec + 1) |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35187
diff
changeset
|
575 |
| TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts2 prec |
33192 | 576 |
| TupleProduct (ts1, ts2) => sub ts1 prec ^ "->" ^ sub ts2 prec |
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
577 |
| TupleProject (ts, c) => sub ts prec ^ "[" ^ string_of_int c ^ "]" |
33192 | 578 |
| TupleSet ts => "{" ^ commas (map string_for_tuple ts) ^ "}" |
579 |
| TupleRange (t1, t2) => |
|
580 |
"{" ^ string_for_tuple t1 ^ |
|
581 |
(if t1 = t2 then "" else " .. " ^ string_for_tuple t2) ^ "}" |
|
582 |
| TupleArea (t1, t2) => |
|
583 |
"{" ^ string_for_tuple t1 ^ " # " ^ string_for_tuple t2 ^ "}" |
|
584 |
| TupleAtomSeq x => atom_seq_name x |
|
585 |
| TupleSetReg x => tuple_set_reg_name x) ^ |
|
586 |
(if need_parens then ")" else "") |
|
587 |
end |
|
588 |
in sub tuple_set 0 end |
|
589 |
||
590 |
fun string_for_tuple_assign (AssignTuple (x, t)) = |
|
591 |
tuple_reg_name x ^ " := " ^ string_for_tuple t ^ "\n" |
|
592 |
| string_for_tuple_assign (AssignTupleSet (x, ts)) = |
|
593 |
tuple_set_reg_name x ^ " := " ^ string_for_tuple_set ts ^ "\n" |
|
594 |
||
38126 | 595 |
fun string_for_bound new_kodkodi (zs, tss) = |
596 |
"bounds " ^ commas (map (commented_rel_name new_kodkodi) zs) ^ ": " ^ |
|
33192 | 597 |
(if length tss = 1 then "" else "[") ^ commas (map string_for_tuple_set tss) ^ |
598 |
(if length tss = 1 then "" else "]") ^ "\n" |
|
599 |
||
600 |
fun int_string_for_bound (opt_n, tss) = |
|
601 |
(case opt_n of |
|
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
602 |
SOME n => signed_string_of_int n ^ ": " |
33192 | 603 |
| NONE => "") ^ "[" ^ commas (map string_for_tuple_set tss) ^ "]" |
604 |
||
605 |
val prec_All = 1 |
|
606 |
val prec_Or = 2 |
|
607 |
val prec_Iff = 3 |
|
608 |
val prec_Implies = 4 |
|
609 |
val prec_And = 5 |
|
610 |
val prec_Not = 6 |
|
611 |
val prec_Eq = 7 |
|
612 |
val prec_Some = 8 |
|
613 |
val prec_SHL = 9 |
|
614 |
val prec_Add = 10 |
|
615 |
val prec_Mult = 11 |
|
616 |
val prec_Override = 12 |
|
617 |
val prec_Intersect = 13 |
|
618 |
val prec_Product = 14 |
|
619 |
val prec_IfNo = 15 |
|
620 |
val prec_Project = 17 |
|
621 |
val prec_Join = 18 |
|
622 |
val prec_BitNot = 19 |
|
623 |
||
624 |
fun precedence_f (All _) = prec_All |
|
625 |
| precedence_f (Exist _) = prec_All |
|
626 |
| precedence_f (FormulaLet _) = prec_All |
|
627 |
| precedence_f (FormulaIf _) = prec_All |
|
628 |
| precedence_f (Or _) = prec_Or |
|
629 |
| precedence_f (Iff _) = prec_Iff |
|
630 |
| precedence_f (Implies _) = prec_Implies |
|
631 |
| precedence_f (And _) = prec_And |
|
632 |
| precedence_f (Not _) = prec_Not |
|
633 |
| precedence_f (Acyclic _) = no_prec |
|
634 |
| precedence_f (Function _) = no_prec |
|
635 |
| precedence_f (Functional _) = no_prec |
|
636 |
| precedence_f (TotalOrdering _) = no_prec |
|
637 |
| precedence_f (Subset _) = prec_Eq |
|
638 |
| precedence_f (RelEq _) = prec_Eq |
|
639 |
| precedence_f (IntEq _) = prec_Eq |
|
640 |
| precedence_f (LT _) = prec_Eq |
|
641 |
| precedence_f (LE _) = prec_Eq |
|
642 |
| precedence_f (No _) = prec_Some |
|
643 |
| precedence_f (Lone _) = prec_Some |
|
644 |
| precedence_f (One _) = prec_Some |
|
645 |
| precedence_f (Some _) = prec_Some |
|
646 |
| precedence_f False = no_prec |
|
647 |
| precedence_f True = no_prec |
|
648 |
| precedence_f (FormulaReg _) = no_prec |
|
649 |
and precedence_r (RelLet _) = prec_All |
|
650 |
| precedence_r (RelIf _) = prec_All |
|
651 |
| precedence_r (Union _) = prec_Add |
|
652 |
| precedence_r (Difference _) = prec_Add |
|
653 |
| precedence_r (Override _) = prec_Override |
|
654 |
| precedence_r (Intersect _) = prec_Intersect |
|
655 |
| precedence_r (Product _) = prec_Product |
|
656 |
| precedence_r (IfNo _) = prec_IfNo |
|
657 |
| precedence_r (Project _) = prec_Project |
|
658 |
| precedence_r (Join _) = prec_Join |
|
659 |
| precedence_r (Closure _) = prec_BitNot |
|
660 |
| precedence_r (ReflexiveClosure _) = prec_BitNot |
|
661 |
| precedence_r (Transpose _) = prec_BitNot |
|
662 |
| precedence_r (Comprehension _) = no_prec |
|
663 |
| precedence_r (Bits _) = no_prec |
|
664 |
| precedence_r (Int _) = no_prec |
|
665 |
| precedence_r Iden = no_prec |
|
666 |
| precedence_r Ints = no_prec |
|
667 |
| precedence_r None = no_prec |
|
668 |
| precedence_r Univ = no_prec |
|
669 |
| precedence_r (Atom _) = no_prec |
|
670 |
| precedence_r (AtomSeq _) = no_prec |
|
671 |
| precedence_r (Rel _) = no_prec |
|
672 |
| precedence_r (Var _) = no_prec |
|
673 |
| precedence_r (RelReg _) = no_prec |
|
674 |
and precedence_i (Sum _) = prec_All |
|
675 |
| precedence_i (IntLet _) = prec_All |
|
676 |
| precedence_i (IntIf _) = prec_All |
|
677 |
| precedence_i (SHL _) = prec_SHL |
|
678 |
| precedence_i (SHA _) = prec_SHL |
|
679 |
| precedence_i (SHR _) = prec_SHL |
|
680 |
| precedence_i (Add _) = prec_Add |
|
681 |
| precedence_i (Sub _) = prec_Add |
|
682 |
| precedence_i (Mult _) = prec_Mult |
|
683 |
| precedence_i (Div _) = prec_Mult |
|
684 |
| precedence_i (Mod _) = prec_Mult |
|
685 |
| precedence_i (Cardinality _) = no_prec |
|
686 |
| precedence_i (SetSum _) = no_prec |
|
687 |
| precedence_i (BitOr _) = prec_Intersect |
|
688 |
| precedence_i (BitXor _) = prec_Intersect |
|
689 |
| precedence_i (BitAnd _) = prec_Intersect |
|
690 |
| precedence_i (BitNot _) = prec_BitNot |
|
691 |
| precedence_i (Neg _) = prec_BitNot |
|
692 |
| precedence_i (Absolute _) = prec_BitNot |
|
693 |
| precedence_i (Signum _) = prec_BitNot |
|
694 |
| precedence_i (Num _) = no_prec |
|
695 |
| precedence_i (IntReg _) = no_prec |
|
696 |
||
697 |
fun write_problem_file out problems = |
|
698 |
let |
|
38126 | 699 |
val new_kodkodi = is_new_kodkodi_version () |
700 |
val rel_name = rel_name new_kodkodi |
|
33192 | 701 |
fun out_outmost_f (And (f1, f2)) = |
702 |
(out_outmost_f f1; out "\n && "; out_outmost_f f2) |
|
703 |
| out_outmost_f f = out_f f prec_And |
|
704 |
and out_f formula outer_prec = |
|
705 |
let |
|
706 |
val prec = precedence_f formula |
|
707 |
val need_parens = (prec < outer_prec) |
|
708 |
in |
|
709 |
(if need_parens then out "(" else ()); |
|
710 |
(case formula of |
|
711 |
All (ds, f) => (out "all ["; out_decls ds; out "] | "; out_f f prec) |
|
712 |
| Exist (ds, f) => |
|
713 |
(out "some ["; out_decls ds; out "] | "; out_f f prec) |
|
714 |
| FormulaLet (bs, f) => |
|
715 |
(out "let ["; out_assigns bs; out "] | "; out_f f prec) |
|
716 |
| FormulaIf (f, f1, f2) => |
|
717 |
(out "if "; out_f f prec; out " then "; out_f f1 prec; out " else "; |
|
718 |
out_f f2 prec) |
|
719 |
| Or (f1, f2) => (out_f f1 prec; out " || "; out_f f2 prec) |
|
720 |
| Iff (f1, f2) => (out_f f1 prec; out " <=> "; out_f f2 prec) |
|
721 |
| Implies (f1, f2) => (out_f f1 (prec + 1); out " => "; out_f f2 prec) |
|
722 |
| And (f1, f2) => (out_f f1 prec; out " && "; out_f f2 prec) |
|
723 |
| Not f => (out "! "; out_f f prec) |
|
724 |
| Acyclic x => out ("ACYCLIC(" ^ rel_name x ^ ")") |
|
725 |
| Function (x, r1, r2) => |
|
726 |
(out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> one "; |
|
727 |
out_r r2 0; out ")") |
|
728 |
| Functional (x, r1, r2) => |
|
729 |
(out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> lone "; |
|
730 |
out_r r2 0; out ")") |
|
38126 | 731 |
| TotalOrdering (x, r1, r2, r3) => |
732 |
(out ("TOTAL_ORDERING(" ^ rel_name x ^ ", "); out_r r1 0; out ", "; |
|
733 |
out_r r2 0; out ", "; out_r r3 0; out ")") |
|
33192 | 734 |
| Subset (r1, r2) => (out_r r1 prec; out " in "; out_r r2 prec) |
735 |
| RelEq (r1, r2) => (out_r r1 prec; out " = "; out_r r2 prec) |
|
736 |
| IntEq (i1, i2) => (out_i i1 prec; out " = "; out_i i2 prec) |
|
737 |
| LT (i1, i2) => (out_i i1 prec; out " < "; out_i i2 prec) |
|
738 |
| LE (i1, i2) => (out_i i1 prec; out " <= "; out_i i2 prec) |
|
739 |
| No r => (out "no "; out_r r prec) |
|
740 |
| Lone r => (out "lone "; out_r r prec) |
|
741 |
| One r => (out "one "; out_r r prec) |
|
742 |
| Some r => (out "some "; out_r r prec) |
|
743 |
| False => out "false" |
|
744 |
| True => out "true" |
|
745 |
| FormulaReg j => out (formula_reg_name j)); |
|
746 |
(if need_parens then out ")" else ()) |
|
747 |
end |
|
748 |
and out_r rel_expr outer_prec = |
|
749 |
let |
|
750 |
val prec = precedence_r rel_expr |
|
751 |
val need_parens = (prec < outer_prec) |
|
752 |
in |
|
753 |
(if need_parens then out "(" else ()); |
|
754 |
(case rel_expr of |
|
755 |
RelLet (bs, r) => |
|
756 |
(out "let ["; out_assigns bs; out "] | "; out_r r prec) |
|
757 |
| RelIf (f, r1, r2) => |
|
758 |
(out "if "; out_f f prec; out " then "; out_r r1 prec; |
|
759 |
out " else "; out_r r2 prec) |
|
760 |
| Union (r1, r2) => (out_r r1 prec; out " + "; out_r r2 (prec + 1)) |
|
761 |
| Difference (r1, r2) => |
|
762 |
(out_r r1 prec; out " - "; out_r r2 (prec + 1)) |
|
763 |
| Override (r1, r2) => (out_r r1 prec; out " ++ "; out_r r2 prec) |
|
764 |
| Intersect (r1, r2) => (out_r r1 prec; out " & "; out_r r2 prec) |
|
765 |
| Product (r1, r2) => (out_r r1 prec; out "->"; out_r r2 prec) |
|
766 |
| IfNo (r1, r2) => (out_r r1 prec; out "\\"; out_r r2 prec) |
|
767 |
| Project (r1, is) => (out_r r1 prec; out "["; out_columns is; out "]") |
|
768 |
| Join (r1, r2) => (out_r r1 prec; out "."; out_r r2 (prec + 1)) |
|
769 |
| Closure r => (out "^"; out_r r prec) |
|
770 |
| ReflexiveClosure r => (out "*"; out_r r prec) |
|
771 |
| Transpose r => (out "~"; out_r r prec) |
|
772 |
| Comprehension (ds, f) => |
|
773 |
(out "{["; out_decls ds; out "] | "; out_f f 0; out "}") |
|
774 |
| Bits i => (out "Bits["; out_i i 0; out "]") |
|
775 |
| Int i => (out "Int["; out_i i 0; out "]") |
|
776 |
| Iden => out "iden" |
|
777 |
| Ints => out "ints" |
|
778 |
| None => out "none" |
|
779 |
| Univ => out "univ" |
|
780 |
| Atom j => out (atom_name j) |
|
781 |
| AtomSeq x => out (atom_seq_name x) |
|
782 |
| Rel x => out (rel_name x) |
|
783 |
| Var x => out (var_name x) |
|
784 |
| RelReg (_, j) => out (rel_reg_name j)); |
|
785 |
(if need_parens then out ")" else ()) |
|
786 |
end |
|
787 |
and out_i int_expr outer_prec = |
|
788 |
let |
|
789 |
val prec = precedence_i int_expr |
|
790 |
val need_parens = (prec < outer_prec) |
|
791 |
in |
|
792 |
(if need_parens then out "(" else ()); |
|
793 |
(case int_expr of |
|
794 |
Sum (ds, i) => (out "sum ["; out_decls ds; out "] | "; out_i i prec) |
|
795 |
| IntLet (bs, i) => |
|
796 |
(out "let ["; out_assigns bs; out "] | "; out_i i prec) |
|
797 |
| IntIf (f, i1, i2) => |
|
798 |
(out "if "; out_f f prec; out " then "; out_i i1 prec; |
|
799 |
out " else "; out_i i2 prec) |
|
800 |
| SHL (i1, i2) => (out_i i1 prec; out " << "; out_i i2 (prec + 1)) |
|
801 |
| SHA (i1, i2) => (out_i i1 prec; out " >> "; out_i i2 (prec + 1)) |
|
802 |
| SHR (i1, i2) => (out_i i1 prec; out " >>> "; out_i i2 (prec + 1)) |
|
803 |
| Add (i1, i2) => (out_i i1 prec; out " + "; out_i i2 (prec + 1)) |
|
804 |
| Sub (i1, i2) => (out_i i1 prec; out " - "; out_i i2 (prec + 1)) |
|
805 |
| Mult (i1, i2) => (out_i i1 prec; out " * "; out_i i2 (prec + 1)) |
|
806 |
| Div (i1, i2) => (out_i i1 prec; out " / "; out_i i2 (prec + 1)) |
|
807 |
| Mod (i1, i2) => (out_i i1 prec; out " % "; out_i i2 (prec + 1)) |
|
808 |
| Cardinality r => (out "#("; out_r r 0; out ")") |
|
809 |
| SetSum r => (out "sum("; out_r r 0; out ")") |
|
810 |
| BitOr (i1, i2) => (out_i i1 prec; out " | "; out_i i2 prec) |
|
811 |
| BitXor (i1, i2) => (out_i i1 prec; out " ^ "; out_i i2 prec) |
|
812 |
| BitAnd (i1, i2) => (out_i i1 prec; out " & "; out_i i2 prec) |
|
813 |
| BitNot i => (out "~"; out_i i prec) |
|
814 |
| Neg i => (out "-"; out_i i prec) |
|
815 |
| Absolute i => (out "abs "; out_i i prec) |
|
816 |
| Signum i => (out "sgn "; out_i i prec) |
|
34124
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset
|
817 |
| Num k => out (signed_string_of_int k) |
33192 | 818 |
| IntReg j => out (int_reg_name j)); |
819 |
(if need_parens then out ")" else ()) |
|
820 |
end |
|
821 |
and out_decls [] = () |
|
822 |
| out_decls [d] = out_decl d |
|
823 |
| out_decls (d :: ds) = (out_decl d; out ", "; out_decls ds) |
|
824 |
and out_decl (DeclNo (x, r)) = |
|
825 |
(out (var_name x); out " : no "; out_r r 0) |
|
826 |
| out_decl (DeclLone (x, r)) = |
|
827 |
(out (var_name x); out " : lone "; out_r r 0) |
|
828 |
| out_decl (DeclOne (x, r)) = |
|
829 |
(out (var_name x); out " : one "; out_r r 0) |
|
830 |
| out_decl (DeclSome (x, r)) = |
|
831 |
(out (var_name x); out " : some "; out_r r 0) |
|
832 |
| out_decl (DeclSet (x, r)) = |
|
833 |
(out (var_name x); out " : set "; out_r r 0) |
|
834 |
and out_assigns [] = () |
|
835 |
| out_assigns [b] = out_assign b |
|
836 |
| out_assigns (b :: bs) = (out_assign b; out ", "; out_assigns bs) |
|
837 |
and out_assign (AssignFormulaReg (j, f)) = |
|
838 |
(out (formula_reg_name j); out " := "; out_f f 0) |
|
839 |
| out_assign (AssignRelReg ((_, j), r)) = |
|
840 |
(out (rel_reg_name j); out " := "; out_r r 0) |
|
841 |
| out_assign (AssignIntReg (j, i)) = |
|
842 |
(out (int_reg_name j); out " := "; out_i i 0) |
|
843 |
and out_columns [] = () |
|
844 |
| out_columns [i] = out_i i 0 |
|
845 |
| out_columns (i :: is) = (out_i i 0; out ", "; out_columns is) |
|
846 |
and out_problem {comment, settings, univ_card, tuple_assigns, bounds, |
|
847 |
int_bounds, expr_assigns, formula} = |
|
848 |
(out ("\n" ^ block_comment comment ^ |
|
849 |
implode (map (fn (key, value) => key ^ ": " ^ value ^ "\n") |
|
850 |
settings) ^ |
|
851 |
"univ: " ^ atom_seq_name (univ_card, 0) ^ "\n" ^ |
|
852 |
implode (map string_for_tuple_assign tuple_assigns) ^ |
|
38126 | 853 |
implode (map (string_for_bound new_kodkodi) bounds) ^ |
33192 | 854 |
(if int_bounds = [] then |
855 |
"" |
|
856 |
else |
|
857 |
"int_bounds: " ^ |
|
858 |
commas (map int_string_for_bound int_bounds) ^ "\n")); |
|
859 |
map (fn b => (out_assign b; out ";")) expr_assigns; |
|
860 |
out "solve "; out_outmost_f formula; out ";\n") |
|
861 |
in |
|
35695 | 862 |
out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^ |
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
41793
diff
changeset
|
863 |
"// " ^ ATP_Util.timestamp () ^ "\n"); |
33192 | 864 |
map out_problem problems |
865 |
end |
|
866 |
||
35718 | 867 |
(** Parsing of solution **) |
868 |
||
33192 | 869 |
fun is_ident_char s = |
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
870 |
Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
871 |
s = "_" orelse s = "'" orelse s = "$" |
33192 | 872 |
|
873 |
fun strip_blanks [] = [] |
|
874 |
| strip_blanks (" " :: ss) = strip_blanks ss |
|
875 |
| strip_blanks [s1, " "] = [s1] |
|
876 |
| strip_blanks (s1 :: " " :: s2 :: ss) = |
|
877 |
if is_ident_char s1 andalso is_ident_char s2 then |
|
878 |
s1 :: " " :: strip_blanks (s2 :: ss) |
|
879 |
else |
|
880 |
strip_blanks (s1 :: s2 :: ss) |
|
881 |
| strip_blanks (s :: ss) = s :: strip_blanks ss |
|
882 |
||
38198 | 883 |
val scan_nat = |
884 |
Scan.repeat1 (Scan.one Symbol.is_ascii_digit) |
|
885 |
>> (the o Int.fromString o space_implode "") |
|
38126 | 886 |
fun scan_rel_name new_kodkodi = |
887 |
($$ "s" |-- scan_nat >> pair 1 |
|
888 |
|| $$ "r" |-- scan_nat >> pair 2 |
|
889 |
|| ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat) -- Scan.option ($$ "'") |
|
890 |
>> (fn ((n, j), SOME _) => (n, ~j - 1) |
|
891 |
| ((n, j), NONE) => (n, if new_kodkodi then j |
|
892 |
else if j mod 2 = 0 then j div 2 |
|
38130 | 893 |
else ~(j + 1) div 2)) |
33192 | 894 |
val scan_atom = $$ "A" |-- scan_nat |
38198 | 895 |
fun parse_non_empty_list scan = scan ::: Scan.repeat ($$ "," |-- scan) |
896 |
fun parse_list scan = parse_non_empty_list scan || Scan.succeed [] |
|
897 |
val parse_tuple = $$ "[" |-- parse_list scan_atom --| $$ "]" |
|
898 |
val parse_tuple_set = $$ "[" |-- parse_list parse_tuple --| $$ "]" |
|
899 |
fun parse_assignment new_kodkodi = |
|
900 |
(scan_rel_name new_kodkodi --| $$ "=") -- parse_tuple_set |
|
901 |
fun parse_instance new_kodkodi = |
|
38126 | 902 |
Scan.this_string "relations:" |
38198 | 903 |
|-- $$ "{" |-- parse_list (parse_assignment new_kodkodi) --| $$ "}" |
33192 | 904 |
|
38198 | 905 |
fun extract_instance new_kodkodi = |
35336 | 906 |
fst o Scan.finite Symbol.stopper |
907 |
(Scan.error (!! (fn _ => |
|
38198 | 908 |
raise SYNTAX ("Kodkod.extract_instance", |
35336 | 909 |
"ill-formed Kodkodi output")) |
38198 | 910 |
(parse_instance new_kodkodi))) |
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40411
diff
changeset
|
911 |
o strip_blanks o raw_explode |
33192 | 912 |
|
913 |
val problem_marker = "*** PROBLEM " |
|
914 |
val outcome_marker = "---OUTCOME---\n" |
|
915 |
val instance_marker = "---INSTANCE---\n" |
|
916 |
||
917 |
fun read_section_body marker = |
|
918 |
Substring.string o fst o Substring.position "\n\n" |
|
919 |
o Substring.triml (size marker) |
|
920 |
||
38126 | 921 |
fun read_next_instance new_kodkodi s = |
33192 | 922 |
let val s = Substring.position instance_marker s |> snd in |
923 |
if Substring.isEmpty s then |
|
924 |
raise SYNTAX ("Kodkod.read_next_instance", "expected \"INSTANCE\" marker") |
|
925 |
else |
|
38198 | 926 |
read_section_body instance_marker s |> extract_instance new_kodkodi |
33192 | 927 |
end |
928 |
||
38126 | 929 |
fun read_next_outcomes new_kodkodi j (s, ps, js) = |
33192 | 930 |
let val (s1, s2) = Substring.position outcome_marker s in |
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
931 |
if Substring.isEmpty s2 orelse |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
932 |
not (Substring.isEmpty (Substring.position problem_marker s1 |
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset
|
933 |
|> snd)) then |
33192 | 934 |
(s, ps, js) |
935 |
else |
|
936 |
let |
|
937 |
val outcome = read_section_body outcome_marker s2 |
|
938 |
val s = Substring.triml (size outcome_marker) s2 |
|
939 |
in |
|
940 |
if String.isSuffix "UNSATISFIABLE" outcome then |
|
38126 | 941 |
read_next_outcomes new_kodkodi j (s, ps, j :: js) |
33192 | 942 |
else if String.isSuffix "SATISFIABLE" outcome then |
38126 | 943 |
read_next_outcomes new_kodkodi j |
944 |
(s, (j, read_next_instance new_kodkodi s2) :: ps, js) |
|
33192 | 945 |
else |
946 |
raise SYNTAX ("Kodkod.read_next_outcomes", |
|
947 |
"unknown outcome " ^ quote outcome) |
|
948 |
end |
|
949 |
end |
|
950 |
||
38126 | 951 |
fun read_next_problems new_kodkodi (s, ps, js) = |
33192 | 952 |
let val s = Substring.position problem_marker s |> snd in |
953 |
if Substring.isEmpty s then |
|
954 |
(ps, js) |
|
955 |
else |
|
956 |
let |
|
957 |
val s = Substring.triml (size problem_marker) s |
|
958 |
val j_plus_1 = s |> Substring.takel (not_equal #" ") |> Substring.string |
|
959 |
|> Int.fromString |> the |
|
960 |
val j = j_plus_1 - 1 |
|
38126 | 961 |
in |
962 |
read_next_problems new_kodkodi |
|
963 |
(read_next_outcomes new_kodkodi j (s, ps, js)) |
|
964 |
end |
|
33192 | 965 |
end |
966 |
handle Option.Option => raise SYNTAX ("Kodkod.read_next_problems", |
|
967 |
"expected number after \"PROBLEM\"") |
|
968 |
||
38126 | 969 |
fun read_output_file new_kodkodi path = |
970 |
(false, |
|
971 |
read_next_problems new_kodkodi (Substring.full (File.read path), [], []) |
|
972 |
|>> rev ||> rev) |
|
35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
973 |
handle IO.Io _ => (true, ([], [])) | OS.SysErr _ => (true, ([], [])) |
33192 | 974 |
|
35718 | 975 |
(** Main Kodkod entry point **) |
976 |
||
977 |
val created_temp_dir = Unsynchronized.ref false |
|
978 |
||
979 |
fun serial_string_and_temporary_dir_for_overlord overlord = |
|
980 |
if overlord then |
|
981 |
("", getenv "ISABELLE_HOME_USER") |
|
982 |
else |
|
983 |
let |
|
984 |
val dir = getenv "ISABELLE_TMP" |
|
985 |
val _ = if !created_temp_dir then () |
|
40743 | 986 |
else (created_temp_dir := true; Isabelle_System.mkdirs (Path.explode dir)) |
35718 | 987 |
in (serial_string (), dir) end |
988 |
||
35814 | 989 |
(* The fudge term below is to account for Kodkodi's slow start-up time, which |
990 |
is partly due to the JVM and partly due to the ML "bash" function. *) |
|
991 |
val fudge_ms = 250 |
|
992 |
||
993 |
fun milliseconds_until_deadline deadline = |
|
994 |
case deadline of |
|
995 |
NONE => ~1 |
|
996 |
| SOME time => |
|
997 |
Int.max (0, Time.toMilliseconds (Time.- (time, Time.now ())) - fudge_ms) |
|
998 |
||
999 |
fun uncached_solve_any_problem overlord deadline max_threads max_solutions |
|
1000 |
problems = |
|
33192 | 1001 |
let |
38126 | 1002 |
val new_kodkodi = is_new_kodkodi_version () |
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset
|
1003 |
val j = find_index (curry (op =) True o #formula) problems |
33192 | 1004 |
val indexed_problems = if j >= 0 then |
1005 |
[(j, nth problems j)] |
|
1006 |
else |
|
35187
3acab6c90d4a
don't destroy "Suc" in Nitpick and fix logic of Kodkod filtering (accidentally flipped in previous change)
blanchet
parents:
35185
diff
changeset
|
1007 |
filter_out (is_problem_trivially_false o snd) |
3acab6c90d4a
don't destroy "Suc" in Nitpick and fix logic of Kodkod filtering (accidentally flipped in previous change)
blanchet
parents:
35185
diff
changeset
|
1008 |
(0 upto length problems - 1 ~~ problems) |
33192 | 1009 |
val triv_js = filter_out (AList.defined (op =) indexed_problems) |
1010 |
(0 upto length problems - 1) |
|
1011 |
val reindex = fst o nth indexed_problems |
|
1012 |
in |
|
1013 |
if null indexed_problems then |
|
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset
|
1014 |
Normal ([], triv_js, "") |
33192 | 1015 |
else |
1016 |
let |
|
34998 | 1017 |
val (serial_str, temp_dir) = |
1018 |
serial_string_and_temporary_dir_for_overlord overlord |
|
1019 |
fun path_for suf = |
|
1020 |
Path.explode (temp_dir ^ "/kodkodi" ^ serial_str ^ "." ^ suf) |
|
1021 |
val in_path = path_for "kki" |
|
33192 | 1022 |
val in_buf = Unsynchronized.ref Buffer.empty |
1023 |
fun out s = Unsynchronized.change in_buf (Buffer.add s) |
|
34998 | 1024 |
val out_path = path_for "out" |
1025 |
val err_path = path_for "err" |
|
33192 | 1026 |
val _ = write_problem_file out (map snd indexed_problems) |
1027 |
val _ = File.write_buffer in_path (!in_buf) |
|
33575
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset
|
1028 |
fun remove_temporary_files () = |
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset
|
1029 |
if overlord then () |
35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1030 |
else List.app (K () o try File.rm) [in_path, out_path, err_path] |
33192 | 1031 |
in |
1032 |
let |
|
35814 | 1033 |
val ms = milliseconds_until_deadline deadline |
33192 | 1034 |
val outcome = |
1035 |
let |
|
1036 |
val code = |
|
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43085
diff
changeset
|
1037 |
Isabelle_System.bash ("cd " ^ File.shell_quote temp_dir ^ ";\n\ |
35079 | 1038 |
\\"$KODKODI\"/bin/kodkodi" ^ |
1039 |
(if ms >= 0 then " -max-msecs " ^ string_of_int ms |
|
1040 |
else "") ^ |
|
1041 |
(if max_solutions > 1 then " -solve-all" else "") ^ |
|
1042 |
" -max-solutions " ^ string_of_int max_solutions ^ |
|
1043 |
(if max_threads > 0 then |
|
1044 |
" -max-threads " ^ string_of_int max_threads |
|
1045 |
else |
|
1046 |
"") ^ |
|
1047 |
" < " ^ File.shell_path in_path ^ |
|
1048 |
" > " ^ File.shell_path out_path ^ |
|
1049 |
" 2> " ^ File.shell_path err_path) |
|
35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1050 |
val (io_error, (ps, nontriv_js)) = |
38126 | 1051 |
read_output_file new_kodkodi out_path |
35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1052 |
||> apfst (map (apfst reindex)) ||> apsnd (map reindex) |
33192 | 1053 |
val js = triv_js @ nontriv_js |
1054 |
val first_error = |
|
35695 | 1055 |
(File.fold_lines (fn line => fn "" => line | s => s) err_path "" |
1056 |
handle IO.Io _ => "" | OS.SysErr _ => "") |
|
1057 |
|> perhaps (try (unsuffix "\r")) |
|
1058 |
|> perhaps (try (unsuffix ".")) |
|
36914 | 1059 |
|> perhaps (try (unprefix "Solve error: ")) |
35695 | 1060 |
|> perhaps (try (unprefix "Error: ")) |
38516
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38198
diff
changeset
|
1061 |
fun has_error s = |
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38198
diff
changeset
|
1062 |
first_error |> Substring.full |> Substring.position s |> snd |
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38198
diff
changeset
|
1063 |
|> Substring.isEmpty |> not |
33192 | 1064 |
in |
1065 |
if null ps then |
|
1066 |
if code = 2 then |
|
1067 |
TimedOut js |
|
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset
|
1068 |
else if code = 0 then |
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset
|
1069 |
Normal ([], js, first_error) |
38516
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38198
diff
changeset
|
1070 |
else if has_error "exec: java" then |
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35695
diff
changeset
|
1071 |
JavaNotInstalled |
38516
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38198
diff
changeset
|
1072 |
else if has_error "UnsupportedClassVersionError" then |
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38198
diff
changeset
|
1073 |
JavaTooOld |
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38198
diff
changeset
|
1074 |
else if has_error "NoClassDefFoundError" then |
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35695
diff
changeset
|
1075 |
KodkodiNotInstalled |
33192 | 1076 |
else if first_error <> "" then |
35695 | 1077 |
Error (first_error, js) |
35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1078 |
else if io_error then |
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset
|
1079 |
Error ("I/O error", js) |
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset
|
1080 |
else |
33192 | 1081 |
Error ("Unknown error", js) |
1082 |
else |
|
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset
|
1083 |
Normal (ps, js, first_error) |
33192 | 1084 |
end |
33575
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset
|
1085 |
in remove_temporary_files (); outcome end |
33192 | 1086 |
end |
1087 |
end |
|
1088 |
||
35814 | 1089 |
val cached_outcome = |
1090 |
Synchronized.var "Kodkod.cached_outcome" |
|
1091 |
(NONE : ((int * problem list) * outcome) option) |
|
1092 |
||
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
40743
diff
changeset
|
1093 |
fun solve_any_problem debug overlord deadline max_threads max_solutions |
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
40743
diff
changeset
|
1094 |
problems = |
35814 | 1095 |
let |
38189 | 1096 |
fun do_solve () = |
1097 |
uncached_solve_any_problem overlord deadline max_threads max_solutions |
|
1098 |
problems |
|
35814 | 1099 |
in |
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
40743
diff
changeset
|
1100 |
if debug orelse overlord then |
35814 | 1101 |
do_solve () |
1102 |
else |
|
1103 |
case AList.lookup (fn ((max1, ps1), (max2, ps2)) => |
|
1104 |
max1 = max2 andalso length ps1 = length ps2 andalso |
|
1105 |
forall problems_equivalent (ps1 ~~ ps2)) |
|
1106 |
(the_list (Synchronized.value cached_outcome)) |
|
1107 |
(max_solutions, problems) of |
|
1108 |
SOME outcome => outcome |
|
1109 |
| NONE => |
|
1110 |
let val outcome = do_solve () in |
|
1111 |
(case outcome of |
|
39326 | 1112 |
Normal (_, _, "") => |
35814 | 1113 |
Synchronized.change cached_outcome |
1114 |
(K (SOME ((max_solutions, problems), outcome))) |
|
1115 |
| _ => ()); |
|
1116 |
outcome |
|
1117 |
end |
|
1118 |
end |
|
1119 |
||
33192 | 1120 |
end; |