author  wenzelm 
Sat, 28 Mar 2020 22:18:28 +0100  
changeset 71664  1f3d9a9dd42a 
parent 67560  0fa87bd86566 
child 72183  13dc5fe14a49 
permissions  rwrr 
33982  1 
(* Title: HOL/Tools/Nitpick/kodkod.ML 
33192  2 
Author: Jasmin Blanchette, TU Muenchen 
55888  3 
Copyright 20082014 
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 

50488
1b3eb579e08b
use modern SAT solvers with modern Kodkod versions
blanchet
parents:
50487
diff
changeset

128 
val kodkodi_version : unit > int list 
1b3eb579e08b
use modern SAT solvers with modern Kodkod versions
blanchet
parents:
50487
diff
changeset

129 

33192  130 
val fold_formula : 'a fold_expr_funcs > formula > 'a > 'a 
131 
val fold_rel_expr : 'a fold_expr_funcs > rel_expr > 'a > 'a 

132 
val fold_int_expr : 'a fold_expr_funcs > int_expr > 'a > 'a 

133 
val fold_decl : 'a fold_expr_funcs > decl > 'a > 'a 

134 
val fold_expr_assign : 'a fold_expr_funcs > expr_assign > 'a > 'a 

135 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

136 
type 'a fold_tuple_funcs = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

137 
{tuple_func: tuple > 'a > 'a, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

138 
tuple_set_func: tuple_set > 'a > 'a} 
33192  139 

140 
val fold_tuple : 'a fold_tuple_funcs > tuple > 'a > 'a 

141 
val fold_tuple_set : 'a fold_tuple_funcs > tuple_set > 'a > 'a 

142 
val fold_tuple_assign : 'a fold_tuple_funcs > tuple_assign > 'a > 'a 

143 
val fold_bound : 

144 
'a fold_expr_funcs > 'a fold_tuple_funcs > bound > 'a > 'a 

145 
val fold_int_bound : 'a fold_tuple_funcs > int_bound > 'a > 'a 

146 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

147 
type problem = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

148 
{comment: string, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

149 
settings: setting list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

150 
univ_card: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

151 
tuple_assigns: tuple_assign list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

152 
bounds: bound list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

153 
int_bounds: int_bound list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

154 
expr_assigns: expr_assign list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

155 
formula: formula} 
33192  156 

157 
type raw_bound = n_ary_index * int list list 

158 

159 
datatype outcome = 

49024  160 
JavaNotFound  
38516
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38198
diff
changeset

161 
JavaTooOld  
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35695
diff
changeset

162 
KodkodiNotInstalled  
50487  163 
KodkodiTooOld  
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset

164 
Normal of (int * raw_bound list) list * int list * string  
33192  165 
TimedOut of int list  
166 
Error of string * int list 

167 

168 
exception SYNTAX of string * string 

169 

170 
val max_arity : int > int 

171 
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

172 
val is_problem_trivially_false : problem > bool 
35814  173 
val problems_equivalent : problem * problem > bool 
33192  174 
val solve_any_problem : 
54816
10d48c2a3e32
made timeouts in Sledgehammer not be 'option's  simplified lots of code
blanchet
parents:
53093
diff
changeset

175 
bool > bool > Time.time > int > int > problem list > outcome 
33192  176 
end; 
177 

178 
structure Kodkod : KODKOD = 

179 
struct 

180 

181 
type n_ary_index = int * int 

182 

183 
type setting = string * string 

184 

185 
datatype tuple = 

186 
Tuple of int list  

187 
TupleIndex of n_ary_index  

188 
TupleReg of n_ary_index 

189 

190 
datatype tuple_set = 

191 
TupleUnion of tuple_set * tuple_set  

192 
TupleDifference of tuple_set * tuple_set  

193 
TupleIntersect of tuple_set * tuple_set  

194 
TupleProduct of tuple_set * tuple_set  

195 
TupleProject of tuple_set * int  

196 
TupleSet of tuple list  

197 
TupleRange of tuple * tuple  

198 
TupleArea of tuple * tuple  

199 
TupleAtomSeq of int * int  

200 
TupleSetReg of n_ary_index 

201 

202 
datatype tuple_assign = 

203 
AssignTuple of n_ary_index * tuple  

204 
AssignTupleSet of n_ary_index * tuple_set 

205 

206 
type bound = (n_ary_index * string) list * tuple_set list 

207 
type int_bound = int option * tuple_set list 

208 

209 
datatype formula = 

210 
All of decl list * formula  

211 
Exist of decl list * formula  

212 
FormulaLet of expr_assign list * formula  

213 
FormulaIf of formula * formula * formula  

214 
Or of formula * formula  

215 
Iff of formula * formula  

216 
Implies of formula * formula  

217 
And of formula * formula  

218 
Not of formula  

219 
Acyclic of n_ary_index  

220 
Function of n_ary_index * rel_expr * rel_expr  

221 
Functional of n_ary_index * rel_expr * rel_expr  

38126  222 
TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr  
33192  223 
Subset of rel_expr * rel_expr  
224 
RelEq of rel_expr * rel_expr  

225 
IntEq of int_expr * int_expr  

226 
LT of int_expr * int_expr  

227 
LE of int_expr * int_expr  

228 
No of rel_expr  

229 
Lone of rel_expr  

230 
One of rel_expr  

231 
Some of rel_expr  

232 
False  

233 
True  

234 
FormulaReg of int 

235 
and rel_expr = 

236 
RelLet of expr_assign list * rel_expr  

237 
RelIf of formula * rel_expr * rel_expr  

238 
Union of rel_expr * rel_expr  

239 
Difference of rel_expr * rel_expr  

240 
Override of rel_expr * rel_expr  

241 
Intersect of rel_expr * rel_expr  

242 
Product of rel_expr * rel_expr  

243 
IfNo of rel_expr * rel_expr  

244 
Project of rel_expr * int_expr list  

245 
Join of rel_expr * rel_expr  

246 
Closure of rel_expr  

247 
ReflexiveClosure of rel_expr  

248 
Transpose of rel_expr  

249 
Comprehension of decl list * formula  

250 
Bits of int_expr  

251 
Int of int_expr  

252 
Iden  

253 
Ints  

254 
None  

255 
Univ  

256 
Atom of int  

257 
AtomSeq of int * int  

258 
Rel of n_ary_index  

259 
Var of n_ary_index  

260 
RelReg of n_ary_index 

261 
and int_expr = 

262 
Sum of decl list * int_expr  

263 
IntLet of expr_assign list * int_expr  

264 
IntIf of formula * int_expr * int_expr  

265 
SHL of int_expr * int_expr  

266 
SHA of int_expr * int_expr  

267 
SHR of int_expr * int_expr  

268 
Add of int_expr * int_expr  

269 
Sub of int_expr * int_expr  

270 
Mult of int_expr * int_expr  

271 
Div of int_expr * int_expr  

272 
Mod of int_expr * int_expr  

273 
Cardinality of rel_expr  

274 
SetSum of rel_expr  

275 
BitOr of int_expr * int_expr  

276 
BitXor of int_expr * int_expr  

277 
BitAnd of int_expr * int_expr  

278 
BitNot of int_expr  

279 
Neg of int_expr  

280 
Absolute of int_expr  

281 
Signum of int_expr  

282 
Num of int  

283 
IntReg of int 

284 
and decl = 

285 
DeclNo of n_ary_index * rel_expr  

286 
DeclLone of n_ary_index * rel_expr  

287 
DeclOne of n_ary_index * rel_expr  

288 
DeclSome of n_ary_index * rel_expr  

289 
DeclSet of n_ary_index * rel_expr 

290 
and expr_assign = 

291 
AssignFormulaReg of int * formula  

292 
AssignRelReg of n_ary_index * rel_expr  

293 
AssignIntReg of int * int_expr 

294 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

295 
type problem = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

296 
{comment: string, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

297 
settings: setting list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

298 
univ_card: int, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

299 
tuple_assigns: tuple_assign list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

300 
bounds: bound list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

301 
int_bounds: int_bound list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

302 
expr_assigns: expr_assign list, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

303 
formula: formula} 
33192  304 

305 
type raw_bound = n_ary_index * int list list 

306 

307 
datatype outcome = 

49024  308 
JavaNotFound  
38516
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38198
diff
changeset

309 
JavaTooOld  
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35695
diff
changeset

310 
KodkodiNotInstalled  
50487  311 
KodkodiTooOld  
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset

312 
Normal of (int * raw_bound list) list * int list * string  
33192  313 
TimedOut of int list  
314 
Error of string * int list 

315 

316 
exception SYNTAX of string * string 

317 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

318 
type 'a fold_expr_funcs = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

319 
{formula_func: formula > 'a > 'a, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

320 
rel_expr_func: rel_expr > 'a > 'a, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

321 
int_expr_func: int_expr > 'a > 'a} 
33192  322 

50488
1b3eb579e08b
use modern SAT solvers with modern Kodkod versions
blanchet
parents:
50487
diff
changeset

323 
fun kodkodi_version () = 
1b3eb579e08b
use modern SAT solvers with modern Kodkod versions
blanchet
parents:
50487
diff
changeset

324 
getenv "KODKODI_VERSION" 
1b3eb579e08b
use modern SAT solvers with modern Kodkod versions
blanchet
parents:
50487
diff
changeset

325 
> space_explode "." 
1b3eb579e08b
use modern SAT solvers with modern Kodkod versions
blanchet
parents:
50487
diff
changeset

326 
> map (the_default 0 o Int.fromString) 
1b3eb579e08b
use modern SAT solvers with modern Kodkod versions
blanchet
parents:
50487
diff
changeset

327 

50487  328 
fun is_kodkodi_too_old () = 
67560  329 
is_less (dict_ord int_ord (kodkodi_version (), [1, 2, 14])) 
38126  330 

331 
(** Auxiliary functions on Kodkod problems **) 

35718  332 

33192  333 
fun fold_formula (F : 'a fold_expr_funcs) formula = 
334 
case formula of 

335 
All (ds, f) => fold (fold_decl F) ds #> fold_formula F f 

336 
 Exist (ds, f) => fold (fold_decl F) ds #> fold_formula F f 

337 
 FormulaLet (bs, f) => fold (fold_expr_assign F) bs #> fold_formula F f 

338 
 FormulaIf (f, f1, f2) => 

339 
fold_formula F f #> fold_formula F f1 #> fold_formula F f2 

340 
 Or (f1, f2) => fold_formula F f1 #> fold_formula F f2 

341 
 Iff (f1, f2) => fold_formula F f1 #> fold_formula F f2 

342 
 Implies (f1, f2) => fold_formula F f1 #> fold_formula F f2 

343 
 And (f1, f2) => fold_formula F f1 #> fold_formula F f2 

344 
 Not f => fold_formula F f 

345 
 Acyclic x => fold_rel_expr F (Rel x) 

346 
 Function (x, r1, r2) => 

347 
fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2 

348 
 Functional (x, r1, r2) => 

349 
fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2 

38126  350 
 TotalOrdering (x, r1, r2, r3) => 
351 
fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2 

352 
#> fold_rel_expr F r3 

33192  353 
 Subset (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 
354 
 RelEq (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 

355 
 IntEq (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 

356 
 LT (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 

357 
 LE (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 

358 
 No r => fold_rel_expr F r 

359 
 Lone r => fold_rel_expr F r 

360 
 One r => fold_rel_expr F r 

361 
 Some r => fold_rel_expr F r 

362 
 False => #formula_func F formula 

363 
 True => #formula_func F formula 

364 
 FormulaReg _ => #formula_func F formula 

365 
and fold_rel_expr F rel_expr = 

366 
case rel_expr of 

367 
RelLet (bs, r) => fold (fold_expr_assign F) bs #> fold_rel_expr F r 

368 
 RelIf (f, r1, r2) => 

369 
fold_formula F f #> fold_rel_expr F r1 #> fold_rel_expr F r2 

370 
 Union (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 

371 
 Difference (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 

372 
 Override (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 

373 
 Intersect (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 

374 
 Product (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 

375 
 IfNo (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 

376 
 Project (r1, is) => fold_rel_expr F r1 #> fold (fold_int_expr F) is 

377 
 Join (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 

378 
 Closure r => fold_rel_expr F r 

379 
 ReflexiveClosure r => fold_rel_expr F r 

380 
 Transpose r => fold_rel_expr F r 

381 
 Comprehension (ds, f) => fold (fold_decl F) ds #> fold_formula F f 

382 
 Bits i => fold_int_expr F i 

383 
 Int i => fold_int_expr F i 

384 
 Iden => #rel_expr_func F rel_expr 

385 
 Ints => #rel_expr_func F rel_expr 

386 
 None => #rel_expr_func F rel_expr 

387 
 Univ => #rel_expr_func F rel_expr 

388 
 Atom _ => #rel_expr_func F rel_expr 

389 
 AtomSeq _ => #rel_expr_func F rel_expr 

390 
 Rel _ => #rel_expr_func F rel_expr 

391 
 Var _ => #rel_expr_func F rel_expr 

392 
 RelReg _ => #rel_expr_func F rel_expr 

393 
and fold_int_expr F int_expr = 

394 
case int_expr of 

395 
Sum (ds, i) => fold (fold_decl F) ds #> fold_int_expr F i 

396 
 IntLet (bs, i) => fold (fold_expr_assign F) bs #> fold_int_expr F i 

397 
 IntIf (f, i1, i2) => 

398 
fold_formula F f #> fold_int_expr F i1 #> fold_int_expr F i2 

399 
 SHL (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 

400 
 SHA (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 

401 
 SHR (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 

402 
 Add (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 

403 
 Sub (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 

404 
 Mult (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 

405 
 Div (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 

406 
 Mod (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 

407 
 Cardinality r => fold_rel_expr F r 

408 
 SetSum r => fold_rel_expr F r 

409 
 BitOr (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 

410 
 BitXor (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 

411 
 BitAnd (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2 

412 
 BitNot i => fold_int_expr F i 

413 
 Neg i => fold_int_expr F i 

414 
 Absolute i => fold_int_expr F i 

415 
 Signum i => fold_int_expr F i 

416 
 Num _ => #int_expr_func F int_expr 

417 
 IntReg _ => #int_expr_func F int_expr 

418 
and fold_decl F decl = 

419 
case decl of 

420 
DeclNo (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r 

421 
 DeclLone (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r 

422 
 DeclOne (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r 

423 
 DeclSome (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r 

424 
 DeclSet (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r 

425 
and fold_expr_assign F assign = 

426 
case assign of 

427 
AssignFormulaReg (x, f) => fold_formula F (FormulaReg x) #> fold_formula F f 

428 
 AssignRelReg (x, r) => fold_rel_expr F (RelReg x) #> fold_rel_expr F r 

429 
 AssignIntReg (x, i) => fold_int_expr F (IntReg x) #> fold_int_expr F i 

430 

36390
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

431 
type 'a fold_tuple_funcs = 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

432 
{tuple_func: tuple > 'a > 'a, 
eee4ee6a5cbe
remove "show_skolems" option and change style of record declarations
blanchet
parents:
36385
diff
changeset

433 
tuple_set_func: tuple_set > 'a > 'a} 
33192  434 

435 
fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F 

55889  436 

33192  437 
fun fold_tuple_set F tuple_set = 
438 
case tuple_set of 

439 
TupleUnion (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 

440 
 TupleDifference (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 

441 
 TupleIntersect (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 

442 
 TupleProduct (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 

443 
 TupleProject (ts, _) => fold_tuple_set F ts 

444 
 TupleSet ts => fold (fold_tuple F) ts 

445 
 TupleRange (t1, t2) => fold_tuple F t1 #> fold_tuple F t2 

446 
 TupleArea (t1, t2) => fold_tuple F t1 #> fold_tuple F t2 

447 
 TupleAtomSeq _ => #tuple_set_func F tuple_set 

448 
 TupleSetReg _ => #tuple_set_func F tuple_set 

55889  449 

33192  450 
fun fold_tuple_assign F assign = 
451 
case assign of 

452 
AssignTuple (x, t) => fold_tuple F (TupleReg x) #> fold_tuple F t 

453 
 AssignTupleSet (x, ts) => 

454 
fold_tuple_set F (TupleSetReg x) #> fold_tuple_set F ts 

55889  455 

33192  456 
fun fold_bound expr_F tuple_F (zs, tss) = 
457 
fold (fold_rel_expr expr_F) (map (Rel o fst) zs) 

458 
#> fold (fold_tuple_set tuple_F) tss 

55889  459 

33192  460 
fun fold_int_bound F (_, tss) = fold (fold_tuple_set F) tss 
461 

462 
fun max_arity univ_card = floor (Math.ln 2147483647.0 

463 
/ Math.ln (Real.fromInt univ_card)) 

55889  464 

33192  465 
fun arity_of_rel_expr (RelLet (_, r)) = arity_of_rel_expr r 
466 
 arity_of_rel_expr (RelIf (_, r1, _)) = arity_of_rel_expr r1 

467 
 arity_of_rel_expr (Union (r1, _)) = arity_of_rel_expr r1 

468 
 arity_of_rel_expr (Difference (r1, _)) = arity_of_rel_expr r1 

469 
 arity_of_rel_expr (Override (r1, _)) = arity_of_rel_expr r1 

470 
 arity_of_rel_expr (Intersect (r1, _)) = arity_of_rel_expr r1 

471 
 arity_of_rel_expr (Product (r1, r2)) = sum_arities_of_rel_exprs r1 r2 

472 
 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

473 
 arity_of_rel_expr (Project (_, is)) = length is 
33192  474 
 arity_of_rel_expr (Join (r1, r2)) = sum_arities_of_rel_exprs r1 r2  2 
475 
 arity_of_rel_expr (Closure _) = 2 

476 
 arity_of_rel_expr (ReflexiveClosure _) = 2 

477 
 arity_of_rel_expr (Transpose _) = 2 

478 
 arity_of_rel_expr (Comprehension (ds, _)) = 

479 
fold (curry op + o arity_of_decl) ds 0 

480 
 arity_of_rel_expr (Bits _) = 1 

481 
 arity_of_rel_expr (Int _) = 1 

482 
 arity_of_rel_expr Iden = 2 

483 
 arity_of_rel_expr Ints = 1 

484 
 arity_of_rel_expr None = 1 

485 
 arity_of_rel_expr Univ = 1 

486 
 arity_of_rel_expr (Atom _) = 1 

487 
 arity_of_rel_expr (AtomSeq _) = 1 

488 
 arity_of_rel_expr (Rel (n, _)) = n 

489 
 arity_of_rel_expr (Var (n, _)) = n 

490 
 arity_of_rel_expr (RelReg (n, _)) = n 

491 
and sum_arities_of_rel_exprs r1 r2 = arity_of_rel_expr r1 + arity_of_rel_expr r2 

492 
and arity_of_decl (DeclNo ((n, _), _)) = n 

493 
 arity_of_decl (DeclLone ((n, _), _)) = n 

494 
 arity_of_decl (DeclOne ((n, _), _)) = n 

495 
 arity_of_decl (DeclSome ((n, _), _)) = n 

496 
 arity_of_decl (DeclSet ((n, _), _)) = n 

497 

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

498 
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

499 
 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

500 

35814  501 
val chop_solver = take 2 o space_explode "," 
33192  502 

35814  503 
fun settings_equivalent ([], []) = true 
504 
 settings_equivalent ((key1, value1) :: settings1, 

505 
(key2, value2) :: settings2) = 

506 
key1 = key2 andalso 

507 
(value1 = value2 orelse key1 = "delay" orelse 

508 
(key1 = "solver" andalso chop_solver value1 = chop_solver value2)) andalso 

509 
settings_equivalent (settings1, settings2) 

510 
 settings_equivalent _ = false 

511 

512 
fun problems_equivalent (p1 : problem, p2 : problem) = 

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

513 
#univ_card p1 = #univ_card p2 andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset

514 
#formula p1 = #formula p2 andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset

515 
#bounds p1 = #bounds p2 andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset

516 
#expr_assigns p1 = #expr_assigns p2 andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset

517 
#tuple_assigns p1 = #tuple_assigns p2 andalso 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset

518 
#int_bounds p1 = #int_bounds p2 andalso 
35814  519 
settings_equivalent (#settings p1, #settings p2) 
33192  520 

35718  521 
(** Serialization of problem **) 
34998  522 

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

523 
fun base_name j = 
c4628a1dcf75
added support for binary nat/int representation to Nitpick
blanchet
parents:
34121
diff
changeset

524 
if j < 0 then string_of_int (~j  1) ^ "'" else string_of_int j 
33192  525 

526 
fun n_ary_name (1, j) prefix _ _ = prefix ^ base_name j 

527 
 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

528 
 n_ary_name (n, j) _ _ prefix = prefix ^ string_of_int n ^ "_" ^ base_name j 
33192  529 

530 
fun atom_name j = "A" ^ base_name j 

531 
fun atom_seq_name (k, 0) = "u" ^ base_name k 

532 
 atom_seq_name (k, j0) = "u" ^ base_name k ^ "@" ^ base_name j0 

533 
fun formula_reg_name j = "$f" ^ base_name j 

534 
fun rel_reg_name j = "$e" ^ base_name j 

535 
fun int_reg_name j = "$i" ^ base_name j 

536 

537 
fun tuple_name x = n_ary_name x "A" "P" "T" 

50487  538 
fun rel_name x = n_ary_name x "s" "r" "m" 
33192  539 
fun var_name x = n_ary_name x "S" "R" "M" 
540 
fun tuple_reg_name x = n_ary_name x "$A" "$P" "$T" 

541 
fun tuple_set_reg_name x = n_ary_name x "$a" "$p" "$t" 

542 

543 
fun inline_comment "" = "" 

544 
 inline_comment comment = 

545 
" /* " ^ translate_string (fn "\n" => " "  "*" => "* "  s => s) comment ^ 

546 
" */" 

55889  547 

33192  548 
fun block_comment "" = "" 
549 
 block_comment comment = prefix_lines "// " comment ^ "\n" 

550 

50487  551 
fun commented_rel_name (x, s) = rel_name x ^ inline_comment s 
33192  552 

553 
fun string_for_tuple (Tuple js) = "[" ^ commas (map atom_name js) ^ "]" 

554 
 string_for_tuple (TupleIndex x) = tuple_name x 

555 
 string_for_tuple (TupleReg x) = tuple_reg_name x 

556 

557 
val no_prec = 100 

558 
val prec_TupleUnion = 1 

559 
val prec_TupleIntersect = 2 

560 
val prec_TupleProduct = 3 

561 
val prec_TupleProject = 4 

562 

563 
fun precedence_ts (TupleUnion _) = prec_TupleUnion 

564 
 precedence_ts (TupleDifference _) = prec_TupleUnion 

565 
 precedence_ts (TupleIntersect _) = prec_TupleIntersect 

566 
 precedence_ts (TupleProduct _) = prec_TupleProduct 

567 
 precedence_ts (TupleProject _) = prec_TupleProject 

568 
 precedence_ts _ = no_prec 

569 

570 
fun string_for_tuple_set tuple_set = 

571 
let 

572 
fun sub tuple_set outer_prec = 

573 
let 

574 
val prec = precedence_ts tuple_set 

575 
val need_parens = (prec < outer_prec) 

576 
in 

577 
(if need_parens then "(" else "") ^ 

578 
(case tuple_set of 

579 
TupleUnion (ts1, ts2) => sub ts1 prec ^ " + " ^ sub ts2 (prec + 1) 

580 
 TupleDifference (ts1, ts2) => 

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

581 
sub ts1 prec ^ "  " ^ sub ts2 (prec + 1) 
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35187
diff
changeset

582 
 TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts2 prec 
33192  583 
 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

584 
 TupleProject (ts, c) => sub ts prec ^ "[" ^ string_of_int c ^ "]" 
33192  585 
 TupleSet ts => "{" ^ commas (map string_for_tuple ts) ^ "}" 
586 
 TupleRange (t1, t2) => 

587 
"{" ^ string_for_tuple t1 ^ 

588 
(if t1 = t2 then "" else " .. " ^ string_for_tuple t2) ^ "}" 

589 
 TupleArea (t1, t2) => 

590 
"{" ^ string_for_tuple t1 ^ " # " ^ string_for_tuple t2 ^ "}" 

591 
 TupleAtomSeq x => atom_seq_name x 

592 
 TupleSetReg x => tuple_set_reg_name x) ^ 

593 
(if need_parens then ")" else "") 

594 
end 

595 
in sub tuple_set 0 end 

596 

597 
fun string_for_tuple_assign (AssignTuple (x, t)) = 

598 
tuple_reg_name x ^ " := " ^ string_for_tuple t ^ "\n" 

599 
 string_for_tuple_assign (AssignTupleSet (x, ts)) = 

600 
tuple_set_reg_name x ^ " := " ^ string_for_tuple_set ts ^ "\n" 

601 

50487  602 
fun string_for_bound (zs, tss) = 
603 
"bounds " ^ commas (map commented_rel_name zs) ^ ": " ^ 

33192  604 
(if length tss = 1 then "" else "[") ^ commas (map string_for_tuple_set tss) ^ 
605 
(if length tss = 1 then "" else "]") ^ "\n" 

606 

607 
fun int_string_for_bound (opt_n, tss) = 

608 
(case opt_n of 

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

609 
SOME n => signed_string_of_int n ^ ": " 
33192  610 
 NONE => "") ^ "[" ^ commas (map string_for_tuple_set tss) ^ "]" 
611 

612 
val prec_All = 1 

613 
val prec_Or = 2 

614 
val prec_Iff = 3 

615 
val prec_Implies = 4 

616 
val prec_And = 5 

617 
val prec_Not = 6 

618 
val prec_Eq = 7 

619 
val prec_Some = 8 

620 
val prec_SHL = 9 

621 
val prec_Add = 10 

622 
val prec_Mult = 11 

623 
val prec_Override = 12 

624 
val prec_Intersect = 13 

625 
val prec_Product = 14 

626 
val prec_IfNo = 15 

627 
val prec_Project = 17 

628 
val prec_Join = 18 

629 
val prec_BitNot = 19 

630 

631 
fun precedence_f (All _) = prec_All 

632 
 precedence_f (Exist _) = prec_All 

633 
 precedence_f (FormulaLet _) = prec_All 

634 
 precedence_f (FormulaIf _) = prec_All 

635 
 precedence_f (Or _) = prec_Or 

636 
 precedence_f (Iff _) = prec_Iff 

637 
 precedence_f (Implies _) = prec_Implies 

638 
 precedence_f (And _) = prec_And 

639 
 precedence_f (Not _) = prec_Not 

640 
 precedence_f (Acyclic _) = no_prec 

641 
 precedence_f (Function _) = no_prec 

642 
 precedence_f (Functional _) = no_prec 

643 
 precedence_f (TotalOrdering _) = no_prec 

644 
 precedence_f (Subset _) = prec_Eq 

645 
 precedence_f (RelEq _) = prec_Eq 

646 
 precedence_f (IntEq _) = prec_Eq 

647 
 precedence_f (LT _) = prec_Eq 

648 
 precedence_f (LE _) = prec_Eq 

649 
 precedence_f (No _) = prec_Some 

650 
 precedence_f (Lone _) = prec_Some 

651 
 precedence_f (One _) = prec_Some 

652 
 precedence_f (Some _) = prec_Some 

653 
 precedence_f False = no_prec 

654 
 precedence_f True = no_prec 

655 
 precedence_f (FormulaReg _) = no_prec 

656 
and precedence_r (RelLet _) = prec_All 

657 
 precedence_r (RelIf _) = prec_All 

658 
 precedence_r (Union _) = prec_Add 

659 
 precedence_r (Difference _) = prec_Add 

660 
 precedence_r (Override _) = prec_Override 

661 
 precedence_r (Intersect _) = prec_Intersect 

662 
 precedence_r (Product _) = prec_Product 

663 
 precedence_r (IfNo _) = prec_IfNo 

664 
 precedence_r (Project _) = prec_Project 

665 
 precedence_r (Join _) = prec_Join 

666 
 precedence_r (Closure _) = prec_BitNot 

667 
 precedence_r (ReflexiveClosure _) = prec_BitNot 

668 
 precedence_r (Transpose _) = prec_BitNot 

669 
 precedence_r (Comprehension _) = no_prec 

670 
 precedence_r (Bits _) = no_prec 

671 
 precedence_r (Int _) = no_prec 

672 
 precedence_r Iden = no_prec 

673 
 precedence_r Ints = no_prec 

674 
 precedence_r None = no_prec 

675 
 precedence_r Univ = no_prec 

676 
 precedence_r (Atom _) = no_prec 

677 
 precedence_r (AtomSeq _) = no_prec 

678 
 precedence_r (Rel _) = no_prec 

679 
 precedence_r (Var _) = no_prec 

680 
 precedence_r (RelReg _) = no_prec 

681 
and precedence_i (Sum _) = prec_All 

682 
 precedence_i (IntLet _) = prec_All 

683 
 precedence_i (IntIf _) = prec_All 

684 
 precedence_i (SHL _) = prec_SHL 

685 
 precedence_i (SHA _) = prec_SHL 

686 
 precedence_i (SHR _) = prec_SHL 

687 
 precedence_i (Add _) = prec_Add 

688 
 precedence_i (Sub _) = prec_Add 

689 
 precedence_i (Mult _) = prec_Mult 

690 
 precedence_i (Div _) = prec_Mult 

691 
 precedence_i (Mod _) = prec_Mult 

692 
 precedence_i (Cardinality _) = no_prec 

693 
 precedence_i (SetSum _) = no_prec 

694 
 precedence_i (BitOr _) = prec_Intersect 

695 
 precedence_i (BitXor _) = prec_Intersect 

696 
 precedence_i (BitAnd _) = prec_Intersect 

697 
 precedence_i (BitNot _) = prec_BitNot 

698 
 precedence_i (Neg _) = prec_BitNot 

699 
 precedence_i (Absolute _) = prec_BitNot 

700 
 precedence_i (Signum _) = prec_BitNot 

701 
 precedence_i (Num _) = no_prec 

702 
 precedence_i (IntReg _) = no_prec 

703 

704 
fun write_problem_file out problems = 

705 
let 

706 
fun out_outmost_f (And (f1, f2)) = 

707 
(out_outmost_f f1; out "\n && "; out_outmost_f f2) 

708 
 out_outmost_f f = out_f f prec_And 

709 
and out_f formula outer_prec = 

710 
let 

711 
val prec = precedence_f formula 

712 
val need_parens = (prec < outer_prec) 

713 
in 

714 
(if need_parens then out "(" else ()); 

715 
(case formula of 

716 
All (ds, f) => (out "all ["; out_decls ds; out "]  "; out_f f prec) 

717 
 Exist (ds, f) => 

718 
(out "some ["; out_decls ds; out "]  "; out_f f prec) 

719 
 FormulaLet (bs, f) => 

720 
(out "let ["; out_assigns bs; out "]  "; out_f f prec) 

721 
 FormulaIf (f, f1, f2) => 

722 
(out "if "; out_f f prec; out " then "; out_f f1 prec; out " else "; 

723 
out_f f2 prec) 

724 
 Or (f1, f2) => (out_f f1 prec; out "  "; out_f f2 prec) 

725 
 Iff (f1, f2) => (out_f f1 prec; out " <=> "; out_f f2 prec) 

726 
 Implies (f1, f2) => (out_f f1 (prec + 1); out " => "; out_f f2 prec) 

727 
 And (f1, f2) => (out_f f1 prec; out " && "; out_f f2 prec) 

728 
 Not f => (out "! "; out_f f prec) 

729 
 Acyclic x => out ("ACYCLIC(" ^ rel_name x ^ ")") 

730 
 Function (x, r1, r2) => 

731 
(out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " > one "; 

732 
out_r r2 0; out ")") 

733 
 Functional (x, r1, r2) => 

734 
(out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " > lone "; 

735 
out_r r2 0; out ")") 

38126  736 
 TotalOrdering (x, r1, r2, r3) => 
737 
(out ("TOTAL_ORDERING(" ^ rel_name x ^ ", "); out_r r1 0; out ", "; 

738 
out_r r2 0; out ", "; out_r r3 0; out ")") 

33192  739 
 Subset (r1, r2) => (out_r r1 prec; out " in "; out_r r2 prec) 
740 
 RelEq (r1, r2) => (out_r r1 prec; out " = "; out_r r2 prec) 

741 
 IntEq (i1, i2) => (out_i i1 prec; out " = "; out_i i2 prec) 

742 
 LT (i1, i2) => (out_i i1 prec; out " < "; out_i i2 prec) 

743 
 LE (i1, i2) => (out_i i1 prec; out " <= "; out_i i2 prec) 

744 
 No r => (out "no "; out_r r prec) 

745 
 Lone r => (out "lone "; out_r r prec) 

746 
 One r => (out "one "; out_r r prec) 

747 
 Some r => (out "some "; out_r r prec) 

748 
 False => out "false" 

749 
 True => out "true" 

750 
 FormulaReg j => out (formula_reg_name j)); 

751 
(if need_parens then out ")" else ()) 

752 
end 

753 
and out_r rel_expr outer_prec = 

754 
let 

755 
val prec = precedence_r rel_expr 

756 
val need_parens = (prec < outer_prec) 

757 
in 

758 
(if need_parens then out "(" else ()); 

759 
(case rel_expr of 

760 
RelLet (bs, r) => 

761 
(out "let ["; out_assigns bs; out "]  "; out_r r prec) 

762 
 RelIf (f, r1, r2) => 

763 
(out "if "; out_f f prec; out " then "; out_r r1 prec; 

764 
out " else "; out_r r2 prec) 

765 
 Union (r1, r2) => (out_r r1 prec; out " + "; out_r r2 (prec + 1)) 

766 
 Difference (r1, r2) => 

767 
(out_r r1 prec; out "  "; out_r r2 (prec + 1)) 

768 
 Override (r1, r2) => (out_r r1 prec; out " ++ "; out_r r2 prec) 

769 
 Intersect (r1, r2) => (out_r r1 prec; out " & "; out_r r2 prec) 

770 
 Product (r1, r2) => (out_r r1 prec; out ">"; out_r r2 prec) 

771 
 IfNo (r1, r2) => (out_r r1 prec; out "\\"; out_r r2 prec) 

772 
 Project (r1, is) => (out_r r1 prec; out "["; out_columns is; out "]") 

773 
 Join (r1, r2) => (out_r r1 prec; out "."; out_r r2 (prec + 1)) 

774 
 Closure r => (out "^"; out_r r prec) 

775 
 ReflexiveClosure r => (out "*"; out_r r prec) 

776 
 Transpose r => (out "~"; out_r r prec) 

777 
 Comprehension (ds, f) => 

778 
(out "{["; out_decls ds; out "]  "; out_f f 0; out "}") 

779 
 Bits i => (out "Bits["; out_i i 0; out "]") 

780 
 Int i => (out "Int["; out_i i 0; out "]") 

781 
 Iden => out "iden" 

782 
 Ints => out "ints" 

783 
 None => out "none" 

784 
 Univ => out "univ" 

785 
 Atom j => out (atom_name j) 

786 
 AtomSeq x => out (atom_seq_name x) 

787 
 Rel x => out (rel_name x) 

788 
 Var x => out (var_name x) 

789 
 RelReg (_, j) => out (rel_reg_name j)); 

790 
(if need_parens then out ")" else ()) 

791 
end 

792 
and out_i int_expr outer_prec = 

793 
let 

794 
val prec = precedence_i int_expr 

795 
val need_parens = (prec < outer_prec) 

796 
in 

797 
(if need_parens then out "(" else ()); 

798 
(case int_expr of 

799 
Sum (ds, i) => (out "sum ["; out_decls ds; out "]  "; out_i i prec) 

800 
 IntLet (bs, i) => 

801 
(out "let ["; out_assigns bs; out "]  "; out_i i prec) 

802 
 IntIf (f, i1, i2) => 

803 
(out "if "; out_f f prec; out " then "; out_i i1 prec; 

804 
out " else "; out_i i2 prec) 

805 
 SHL (i1, i2) => (out_i i1 prec; out " << "; out_i i2 (prec + 1)) 

806 
 SHA (i1, i2) => (out_i i1 prec; out " >> "; out_i i2 (prec + 1)) 

807 
 SHR (i1, i2) => (out_i i1 prec; out " >>> "; out_i i2 (prec + 1)) 

808 
 Add (i1, i2) => (out_i i1 prec; out " + "; out_i i2 (prec + 1)) 

809 
 Sub (i1, i2) => (out_i i1 prec; out "  "; out_i i2 (prec + 1)) 

810 
 Mult (i1, i2) => (out_i i1 prec; out " * "; out_i i2 (prec + 1)) 

811 
 Div (i1, i2) => (out_i i1 prec; out " / "; out_i i2 (prec + 1)) 

812 
 Mod (i1, i2) => (out_i i1 prec; out " % "; out_i i2 (prec + 1)) 

813 
 Cardinality r => (out "#("; out_r r 0; out ")") 

814 
 SetSum r => (out "sum("; out_r r 0; out ")") 

815 
 BitOr (i1, i2) => (out_i i1 prec; out "  "; out_i i2 prec) 

816 
 BitXor (i1, i2) => (out_i i1 prec; out " ^ "; out_i i2 prec) 

817 
 BitAnd (i1, i2) => (out_i i1 prec; out " & "; out_i i2 prec) 

818 
 BitNot i => (out "~"; out_i i prec) 

819 
 Neg i => (out ""; out_i i prec) 

820 
 Absolute i => (out "abs "; out_i i prec) 

821 
 Signum i => (out "sgn "; out_i i prec) 

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

822 
 Num k => out (signed_string_of_int k) 
33192  823 
 IntReg j => out (int_reg_name j)); 
824 
(if need_parens then out ")" else ()) 

825 
end 

826 
and out_decls [] = () 

827 
 out_decls [d] = out_decl d 

828 
 out_decls (d :: ds) = (out_decl d; out ", "; out_decls ds) 

829 
and out_decl (DeclNo (x, r)) = 

830 
(out (var_name x); out " : no "; out_r r 0) 

831 
 out_decl (DeclLone (x, r)) = 

832 
(out (var_name x); out " : lone "; out_r r 0) 

833 
 out_decl (DeclOne (x, r)) = 

834 
(out (var_name x); out " : one "; out_r r 0) 

835 
 out_decl (DeclSome (x, r)) = 

836 
(out (var_name x); out " : some "; out_r r 0) 

837 
 out_decl (DeclSet (x, r)) = 

838 
(out (var_name x); out " : set "; out_r r 0) 

839 
and out_assigns [] = () 

840 
 out_assigns [b] = out_assign b 

841 
 out_assigns (b :: bs) = (out_assign b; out ", "; out_assigns bs) 

842 
and out_assign (AssignFormulaReg (j, f)) = 

843 
(out (formula_reg_name j); out " := "; out_f f 0) 

844 
 out_assign (AssignRelReg ((_, j), r)) = 

845 
(out (rel_reg_name j); out " := "; out_r r 0) 

846 
 out_assign (AssignIntReg (j, i)) = 

847 
(out (int_reg_name j); out " := "; out_i i 0) 

848 
and out_columns [] = () 

849 
 out_columns [i] = out_i i 0 

850 
 out_columns (i :: is) = (out_i i 0; out ", "; out_columns is) 

851 
and out_problem {comment, settings, univ_card, tuple_assigns, bounds, 

852 
int_bounds, expr_assigns, formula} = 

853 
(out ("\n" ^ block_comment comment ^ 

854 
implode (map (fn (key, value) => key ^ ": " ^ value ^ "\n") 

855 
settings) ^ 

856 
"univ: " ^ atom_seq_name (univ_card, 0) ^ "\n" ^ 

857 
implode (map string_for_tuple_assign tuple_assigns) ^ 

50487  858 
implode (map string_for_bound bounds) ^ 
33192  859 
(if int_bounds = [] then 
860 
"" 

861 
else 

862 
"int_bounds: " ^ 

863 
commas (map int_string_for_bound int_bounds) ^ "\n")); 

864 
map (fn b => (out_assign b; out ";")) expr_assigns; 

865 
out "solve "; out_outmost_f formula; out ";\n") 

866 
in 

35695  867 
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

868 
"// " ^ ATP_Util.timestamp () ^ "\n"); 
33192  869 
map out_problem problems 
870 
end 

871 

35718  872 
(** Parsing of solution **) 
873 

33192  874 
fun is_ident_char s = 
34936
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset

875 
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

876 
s = "_" orelse s = "'" orelse s = "$" 
33192  877 

878 
fun strip_blanks [] = [] 

879 
 strip_blanks (" " :: ss) = strip_blanks ss 

880 
 strip_blanks [s1, " "] = [s1] 

881 
 strip_blanks (s1 :: " " :: s2 :: ss) = 

882 
if is_ident_char s1 andalso is_ident_char s2 then 

883 
s1 :: " " :: strip_blanks (s2 :: ss) 

884 
else 

885 
strip_blanks (s1 :: s2 :: ss) 

886 
 strip_blanks (s :: ss) = s :: strip_blanks ss 

887 

38198  888 
val scan_nat = 
889 
Scan.repeat1 (Scan.one Symbol.is_ascii_digit) 

53093  890 
>> (the o Int.fromString o implode) 
50487  891 
val scan_rel_name = 
38126  892 
($$ "s"  scan_nat >> pair 1 
893 
 $$ "r"  scan_nat >> pair 2 

894 
 ($$ "m"  scan_nat  $$ "_")  scan_nat)  Scan.option ($$ "'") 

895 
>> (fn ((n, j), SOME _) => (n, ~j  1) 

50487  896 
 ((n, j), NONE) => (n, j)) 
33192  897 
val scan_atom = $$ "A"  scan_nat 
38198  898 
fun parse_non_empty_list scan = scan ::: Scan.repeat ($$ ","  scan) 
899 
fun parse_list scan = parse_non_empty_list scan  Scan.succeed [] 

900 
val parse_tuple = $$ "["  parse_list scan_atom  $$ "]" 

901 
val parse_tuple_set = $$ "["  parse_list parse_tuple  $$ "]" 

50487  902 
val parse_assignment = (scan_rel_name  $$ "=")  parse_tuple_set 
903 
val parse_instance = 

38126  904 
Scan.this_string "relations:" 
50487  905 
 $$ "{"  parse_list parse_assignment  $$ "}" 
33192  906 

50487  907 
val extract_instance = 
35336  908 
fst o Scan.finite Symbol.stopper 
909 
(Scan.error (!! (fn _ => 

38198  910 
raise SYNTAX ("Kodkod.extract_instance", 
35336  911 
"illformed Kodkodi output")) 
50487  912 
parse_instance)) 
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40411
diff
changeset

913 
o strip_blanks o raw_explode 
33192  914 

915 
val problem_marker = "*** PROBLEM " 

916 
val outcome_marker = "OUTCOME\n" 

917 
val instance_marker = "INSTANCE\n" 

918 

919 
fun read_section_body marker = 

920 
Substring.string o fst o Substring.position "\n\n" 

921 
o Substring.triml (size marker) 

922 

50487  923 
fun read_next_instance s = 
33192  924 
let val s = Substring.position instance_marker s > snd in 
925 
if Substring.isEmpty s then 

926 
raise SYNTAX ("Kodkod.read_next_instance", "expected \"INSTANCE\" marker") 

927 
else 

50487  928 
read_section_body instance_marker s > extract_instance 
33192  929 
end 
930 

50487  931 
fun read_next_outcomes j (s, ps, js) = 
33192  932 
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

933 
if Substring.isEmpty s2 orelse 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset

934 
not (Substring.isEmpty (Substring.position problem_marker s1 
c4f04bee79f3
some work on Nitpick's support for quotient types;
blanchet
parents:
34124
diff
changeset

935 
> snd)) then 
33192  936 
(s, ps, js) 
937 
else 

938 
let 

939 
val outcome = read_section_body outcome_marker s2 

940 
val s = Substring.triml (size outcome_marker) s2 

941 
in 

942 
if String.isSuffix "UNSATISFIABLE" outcome then 

50487  943 
read_next_outcomes j (s, ps, j :: js) 
33192  944 
else if String.isSuffix "SATISFIABLE" outcome then 
50487  945 
read_next_outcomes j (s, (j, read_next_instance s2) :: ps, js) 
33192  946 
else 
947 
raise SYNTAX ("Kodkod.read_next_outcomes", 

948 
"unknown outcome " ^ quote outcome) 

949 
end 

950 
end 

951 

50487  952 
fun read_next_problems (s, ps, js) = 
33192  953 
let val s = Substring.position problem_marker s > snd in 
954 
if Substring.isEmpty s then 

955 
(ps, js) 

956 
else 

957 
let 

958 
val s = Substring.triml (size problem_marker) s 

959 
val j_plus_1 = s > Substring.takel (not_equal #" ") > Substring.string 

960 
> Int.fromString > the 

961 
val j = j_plus_1  1 

50487  962 
in read_next_problems (read_next_outcomes j (s, ps, js)) end 
33192  963 
end 
964 
handle Option.Option => raise SYNTAX ("Kodkod.read_next_problems", 

965 
"expected number after \"PROBLEM\"") 

966 

50487  967 
fun read_output_file path = 
38126  968 
(false, 
50487  969 
read_next_problems (Substring.full (File.read path), [], []) 
38126  970 
>> rev > rev) 
35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset

971 
handle IO.Io _ => (true, ([], []))  OS.SysErr _ => (true, ([], [])) 
33192  972 

35718  973 
(** Main Kodkod entry point **) 
974 

975 
val created_temp_dir = Unsynchronized.ref false 

976 

977 
fun serial_string_and_temporary_dir_for_overlord overlord = 

978 
if overlord then 

979 
("", getenv "ISABELLE_HOME_USER") 

980 
else 

981 
let 

982 
val dir = getenv "ISABELLE_TMP" 

983 
val _ = if !created_temp_dir then () 

40743  984 
else (created_temp_dir := true; Isabelle_System.mkdirs (Path.explode dir)) 
35718  985 
in (serial_string (), dir) end 
986 

35814  987 
(* The fudge term below is to account for Kodkodi's slow startup time, which 
988 
is partly due to the JVM and partly due to the ML "bash" function. *) 

989 
val fudge_ms = 250 

990 

991 
fun milliseconds_until_deadline deadline = 

62826  992 
Int.max (0, Time.toMilliseconds (deadline  Time.now ())  fudge_ms) 
35814  993 

994 
fun uncached_solve_any_problem overlord deadline max_threads max_solutions 

995 
problems = 

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

997 
val j = find_index (curry (op =) True o #formula) problems 
33192  998 
val indexed_problems = if j >= 0 then 
999 
[(j, nth problems j)] 

1000 
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

1001 
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

1002 
(0 upto length problems  1 ~~ problems) 
33192  1003 
val triv_js = filter_out (AList.defined (op =) indexed_problems) 
1004 
(0 upto length problems  1) 

1005 
val reindex = fst o nth indexed_problems 

1006 
in 

1007 
if null indexed_problems then 

35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset

1008 
Normal ([], triv_js, "") 
33192  1009 
else 
1010 
let 

34998  1011 
val (serial_str, temp_dir) = 
1012 
serial_string_and_temporary_dir_for_overlord overlord 

1013 
fun path_for suf = 

1014 
Path.explode (temp_dir ^ "/kodkodi" ^ serial_str ^ "." ^ suf) 

1015 
val in_path = path_for "kki" 

33192  1016 
val in_buf = Unsynchronized.ref Buffer.empty 
1017 
fun out s = Unsynchronized.change in_buf (Buffer.add s) 

34998  1018 
val out_path = path_for "out" 
1019 
val err_path = path_for "err" 

33192  1020 
val _ = write_problem_file out (map snd indexed_problems) 
1021 
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

1022 
fun remove_temporary_files () = 
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset

1023 
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

1024 
else List.app (K () o try File.rm) [in_path, out_path, err_path] 
33192  1025 
in 
1026 
let 

35814  1027 
val ms = milliseconds_until_deadline deadline 
33192  1028 
val outcome = 
1029 
let 

1030 
val code = 

64304  1031 
Isabelle_System.bash ("cd " ^ Bash.string temp_dir ^ ";\n\ 
62549
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
55889
diff
changeset

1032 
\\"$KODKODI/bin/kodkodi\"" ^ 
35079  1033 
(if ms >= 0 then " maxmsecs " ^ string_of_int ms 
1034 
else "") ^ 

1035 
(if max_solutions > 1 then " solveall" else "") ^ 

1036 
" maxsolutions " ^ string_of_int max_solutions ^ 

1037 
(if max_threads > 0 then 

1038 
" maxthreads " ^ string_of_int max_threads 

1039 
else 

1040 
"") ^ 

62549
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
55889
diff
changeset

1041 
" < " ^ File.bash_path in_path ^ 
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
55889
diff
changeset

1042 
" > " ^ File.bash_path out_path ^ 
9498623b27f0
File.bash_string operations in ML as in Scala  exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
55889
diff
changeset

1043 
" 2> " ^ File.bash_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

1044 
val (io_error, (ps, nontriv_js)) = 
50487  1045 
read_output_file out_path 
35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset

1046 
> apfst (map (apfst reindex)) > apsnd (map reindex) 
33192  1047 
val js = triv_js @ nontriv_js 
1048 
val first_error = 

35695  1049 
(File.fold_lines (fn line => fn "" => line  s => s) err_path "" 
1050 
handle IO.Io _ => ""  OS.SysErr _ => "") 

1051 
> perhaps (try (unsuffix "\r")) 

1052 
> perhaps (try (unsuffix ".")) 

36914  1053 
> perhaps (try (unprefix "Solve error: ")) 
35695  1054 
> perhaps (try (unprefix "Error: ")) 
38516
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38198
diff
changeset

1055 
fun has_error s = 
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38198
diff
changeset

1056 
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

1057 
> Substring.isEmpty > not 
33192  1058 
in 
1059 
if null ps then 

1060 
if code = 2 then 

1061 
TimedOut js 

35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset

1062 
else if code = 0 then 
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset

1063 
Normal ([], js, first_error) 
47490
f4348634595b
more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
wenzelm
parents:
43850
diff
changeset

1064 
else if code = 127 then 
49024  1065 
JavaNotFound 
38516
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38198
diff
changeset

1066 
else if has_error "UnsupportedClassVersionError" then 
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38198
diff
changeset

1067 
JavaTooOld 
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38198
diff
changeset

1068 
else if has_error "NoClassDefFoundError" then 
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35695
diff
changeset

1069 
KodkodiNotInstalled 
50487  1070 
else if is_kodkodi_too_old () then 
1071 
KodkodiTooOld 

33192  1072 
else if first_error <> "" then 
35695  1073 
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

1074 
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

1075 
Error ("I/O error", js) 
35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset

1076 
else 
33192  1077 
Error ("Unknown error", js) 
1078 
else 

35333
f61de25f71f9
distinguish between Kodkodi warnings and errors in Nitpick;
blanchet
parents:
35309
diff
changeset

1079 
Normal (ps, js, first_error) 
33192  1080 
end 
33575
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset

1081 
in remove_temporary_files (); outcome end 
71664  1082 
handle exn => (remove_temporary_files (); Exn.reraise exn) 
33192  1083 
end 
1084 
end 

1085 

35814  1086 
val cached_outcome = 
1087 
Synchronized.var "Kodkod.cached_outcome" 

1088 
(NONE : ((int * problem list) * outcome) option) 

1089 

41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
40743
diff
changeset

1090 
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

1091 
problems = 
35814  1092 
let 
38189  1093 
fun do_solve () = 
1094 
uncached_solve_any_problem overlord deadline max_threads max_solutions 

1095 
problems 

35814  1096 
in 
41793
c7a2669ae75d
tweaked Nitpick based on C++ memory model example
blanchet
parents:
40743
diff
changeset

1097 
if debug orelse overlord then 
35814  1098 
do_solve () 
1099 
else 

1100 
case AList.lookup (fn ((max1, ps1), (max2, ps2)) => 

1101 
max1 = max2 andalso length ps1 = length ps2 andalso 

1102 
forall problems_equivalent (ps1 ~~ ps2)) 

1103 
(the_list (Synchronized.value cached_outcome)) 

1104 
(max_solutions, problems) of 

1105 
SOME outcome => outcome 

1106 
 NONE => 

1107 
let val outcome = do_solve () in 

1108 
(case outcome of 

39326  1109 
Normal (_, _, "") => 
35814  1110 
Synchronized.change cached_outcome 
1111 
(K (SOME ((max_solutions, problems), outcome))) 

1112 
 _ => ()); 

1113 
outcome 

1114 
end 

1115 
end 

1116 

33192  1117 
end; 