author  blanchet 
Fri, 14 May 2010 15:02:38 +0200  
changeset 36914  1806aa69bd62 
parent 36390  eee4ee6a5cbe 
child 38019  e207a64e1e0b 
permissions  rwrr 
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 

5 
ML interface on top of Kodkod. 

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  

50 
TotalOrdering of n_ary_index * n_ary_index * n_ary_index * n_ary_index  

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  
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35695
diff
changeset

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

160 
Normal of (int * raw_bound list) list * int list * string  
33192  161 
TimedOut of int list  
162 
Interrupted of int list option  

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 : 
172 
bool > Time.time option > int > int > problem list > outcome 

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  

219 
TotalOrdering of n_ary_index * n_ary_index * n_ary_index * n_ary_index  

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  
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35695
diff
changeset

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

307 
Normal of (int * raw_bound list) list * int list * string  
33192  308 
TimedOut of int list  
309 
Interrupted of int list option  

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 

35718  319 
(** Auxiliary functions on ML representation of Kodkod problems **) 
320 

33192  321 
fun fold_formula (F : 'a fold_expr_funcs) formula = 
322 
case formula of 

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

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

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

326 
 FormulaIf (f, f1, f2) => 

327 
fold_formula F f #> fold_formula F f1 #> fold_formula F f2 

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

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

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

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

332 
 Not f => fold_formula F f 

333 
 Acyclic x => fold_rel_expr F (Rel x) 

334 
 Function (x, r1, r2) => 

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

336 
 Functional (x, r1, r2) => 

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

338 
 TotalOrdering (x1, x2, x3, x4) => 

339 
fold_rel_expr F (Rel x1) #> fold_rel_expr F (Rel x2) 

340 
#> fold_rel_expr F (Rel x3) #> fold_rel_expr F (Rel x4) 

341 
 Subset (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 

342 
 RelEq (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 

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

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

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

346 
 No r => fold_rel_expr F r 

347 
 Lone r => fold_rel_expr F r 

348 
 One r => fold_rel_expr F r 

349 
 Some r => fold_rel_expr F r 

350 
 False => #formula_func F formula 

351 
 True => #formula_func F formula 

352 
 FormulaReg _ => #formula_func F formula 

353 
and fold_rel_expr F rel_expr = 

354 
case rel_expr of 

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

356 
 RelIf (f, r1, r2) => 

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

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

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

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

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

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

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

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

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

366 
 Closure r => fold_rel_expr F r 

367 
 ReflexiveClosure r => fold_rel_expr F r 

368 
 Transpose r => fold_rel_expr F r 

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

370 
 Bits i => fold_int_expr F i 

371 
 Int i => fold_int_expr F i 

372 
 Iden => #rel_expr_func F rel_expr 

373 
 Ints => #rel_expr_func F rel_expr 

374 
 None => #rel_expr_func F rel_expr 

375 
 Univ => #rel_expr_func F rel_expr 

376 
 Atom _ => #rel_expr_func F rel_expr 

377 
 AtomSeq _ => #rel_expr_func F rel_expr 

378 
 Rel _ => #rel_expr_func F rel_expr 

379 
 Var _ => #rel_expr_func F rel_expr 

380 
 RelReg _ => #rel_expr_func F rel_expr 

381 
and fold_int_expr F int_expr = 

382 
case int_expr of 

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

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

385 
 IntIf (f, i1, i2) => 

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

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

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

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

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

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

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

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

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

395 
 Cardinality r => fold_rel_expr F r 

396 
 SetSum r => fold_rel_expr F r 

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

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

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

400 
 BitNot i => fold_int_expr F i 

401 
 Neg i => fold_int_expr F i 

402 
 Absolute i => fold_int_expr F i 

403 
 Signum i => fold_int_expr F i 

404 
 Num _ => #int_expr_func F int_expr 

405 
 IntReg _ => #int_expr_func F int_expr 

406 
and fold_decl F decl = 

407 
case decl of 

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

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

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

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

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

413 
and fold_expr_assign F assign = 

414 
case assign of 

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

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

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

418 

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

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

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

421 
tuple_set_func: tuple_set > 'a > 'a} 
33192  422 

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

424 
fun fold_tuple_set F tuple_set = 

425 
case tuple_set of 

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

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

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

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

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

431 
 TupleSet ts => fold (fold_tuple F) ts 

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

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

434 
 TupleAtomSeq _ => #tuple_set_func F tuple_set 

435 
 TupleSetReg _ => #tuple_set_func F tuple_set 

436 
fun fold_tuple_assign F assign = 

437 
case assign of 

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

439 
 AssignTupleSet (x, ts) => 

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

441 
fun fold_bound expr_F tuple_F (zs, tss) = 

442 
fold (fold_rel_expr expr_F) (map (Rel o fst) zs) 

443 
#> fold (fold_tuple_set tuple_F) tss 

444 
fun fold_int_bound F (_, tss) = fold (fold_tuple_set F) tss 

445 

446 
fun max_arity univ_card = floor (Math.ln 2147483647.0 

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

448 
fun arity_of_rel_expr (RelLet (_, r)) = arity_of_rel_expr r 

449 
 arity_of_rel_expr (RelIf (_, r1, _)) = arity_of_rel_expr r1 

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

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

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

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

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

455 
 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

456 
 arity_of_rel_expr (Project (_, is)) = length is 
33192  457 
 arity_of_rel_expr (Join (r1, r2)) = sum_arities_of_rel_exprs r1 r2  2 
458 
 arity_of_rel_expr (Closure _) = 2 

459 
 arity_of_rel_expr (ReflexiveClosure _) = 2 

460 
 arity_of_rel_expr (Transpose _) = 2 

461 
 arity_of_rel_expr (Comprehension (ds, _)) = 

462 
fold (curry op + o arity_of_decl) ds 0 

463 
 arity_of_rel_expr (Bits _) = 1 

464 
 arity_of_rel_expr (Int _) = 1 

465 
 arity_of_rel_expr Iden = 2 

466 
 arity_of_rel_expr Ints = 1 

467 
 arity_of_rel_expr None = 1 

468 
 arity_of_rel_expr Univ = 1 

469 
 arity_of_rel_expr (Atom _) = 1 

470 
 arity_of_rel_expr (AtomSeq _) = 1 

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

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

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

474 
and sum_arities_of_rel_exprs r1 r2 = arity_of_rel_expr r1 + arity_of_rel_expr r2 

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

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

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

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

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

480 

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

481 
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

482 
 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

483 

35814  484 
val chop_solver = take 2 o space_explode "," 
33192  485 

35814  486 
fun settings_equivalent ([], []) = true 
487 
 settings_equivalent ((key1, value1) :: settings1, 

488 
(key2, value2) :: settings2) = 

489 
key1 = key2 andalso 

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

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

492 
settings_equivalent (settings1, settings2) 

493 
 settings_equivalent _ = false 

494 

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

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

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

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

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

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

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

501 
#int_bounds p1 = #int_bounds p2 andalso 
35814  502 
settings_equivalent (#settings p1, #settings p2) 
33192  503 

35718  504 
(** Serialization of problem **) 
34998  505 

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

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

507 
if j < 0 then string_of_int (~j  1) ^ "'" else string_of_int j 
33192  508 

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

510 
 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

511 
 n_ary_name (n, j) _ _ prefix = prefix ^ string_of_int n ^ "_" ^ base_name j 
33192  512 

513 
fun atom_name j = "A" ^ base_name j 

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

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

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

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

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

519 

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

521 
fun rel_name x = n_ary_name x "s" "r" "m" 

522 
fun var_name x = n_ary_name x "S" "R" "M" 

523 
fun tuple_reg_name x = n_ary_name x "$A" "$P" "$T" 

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

525 

526 
fun inline_comment "" = "" 

527 
 inline_comment comment = 

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

529 
" */" 

530 
fun block_comment "" = "" 

531 
 block_comment comment = prefix_lines "// " comment ^ "\n" 

532 

533 
fun commented_rel_name (x, s) = rel_name x ^ inline_comment s 

534 

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

536 
 string_for_tuple (TupleIndex x) = tuple_name x 

537 
 string_for_tuple (TupleReg x) = tuple_reg_name x 

538 

539 
val no_prec = 100 

540 
val prec_TupleUnion = 1 

541 
val prec_TupleIntersect = 2 

542 
val prec_TupleProduct = 3 

543 
val prec_TupleProject = 4 

544 

545 
fun precedence_ts (TupleUnion _) = prec_TupleUnion 

546 
 precedence_ts (TupleDifference _) = prec_TupleUnion 

547 
 precedence_ts (TupleIntersect _) = prec_TupleIntersect 

548 
 precedence_ts (TupleProduct _) = prec_TupleProduct 

549 
 precedence_ts (TupleProject _) = prec_TupleProject 

550 
 precedence_ts _ = no_prec 

551 

552 
fun string_for_tuple_set tuple_set = 

553 
let 

554 
fun sub tuple_set outer_prec = 

555 
let 

556 
val prec = precedence_ts tuple_set 

557 
val need_parens = (prec < outer_prec) 

558 
in 

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

560 
(case tuple_set of 

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

562 
 TupleDifference (ts1, ts2) => 

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

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

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

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

569 
"{" ^ string_for_tuple t1 ^ 

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

571 
 TupleArea (t1, t2) => 

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

573 
 TupleAtomSeq x => atom_seq_name x 

574 
 TupleSetReg x => tuple_set_reg_name x) ^ 

575 
(if need_parens then ")" else "") 

576 
end 

577 
in sub tuple_set 0 end 

578 

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

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

581 
 string_for_tuple_assign (AssignTupleSet (x, ts)) = 

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

583 

584 
fun string_for_bound (zs, tss) = 

585 
"bounds " ^ commas (map commented_rel_name zs) ^ ": " ^ 

586 
(if length tss = 1 then "" else "[") ^ commas (map string_for_tuple_set tss) ^ 

587 
(if length tss = 1 then "" else "]") ^ "\n" 

588 

589 
fun int_string_for_bound (opt_n, tss) = 

590 
(case opt_n of 

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

591 
SOME n => signed_string_of_int n ^ ": " 
33192  592 
 NONE => "") ^ "[" ^ commas (map string_for_tuple_set tss) ^ "]" 
593 

594 
val prec_All = 1 

595 
val prec_Or = 2 

596 
val prec_Iff = 3 

597 
val prec_Implies = 4 

598 
val prec_And = 5 

599 
val prec_Not = 6 

600 
val prec_Eq = 7 

601 
val prec_Some = 8 

602 
val prec_SHL = 9 

603 
val prec_Add = 10 

604 
val prec_Mult = 11 

605 
val prec_Override = 12 

606 
val prec_Intersect = 13 

607 
val prec_Product = 14 

608 
val prec_IfNo = 15 

609 
val prec_Project = 17 

610 
val prec_Join = 18 

611 
val prec_BitNot = 19 

612 

613 
fun precedence_f (All _) = prec_All 

614 
 precedence_f (Exist _) = prec_All 

615 
 precedence_f (FormulaLet _) = prec_All 

616 
 precedence_f (FormulaIf _) = prec_All 

617 
 precedence_f (Or _) = prec_Or 

618 
 precedence_f (Iff _) = prec_Iff 

619 
 precedence_f (Implies _) = prec_Implies 

620 
 precedence_f (And _) = prec_And 

621 
 precedence_f (Not _) = prec_Not 

622 
 precedence_f (Acyclic _) = no_prec 

623 
 precedence_f (Function _) = no_prec 

624 
 precedence_f (Functional _) = no_prec 

625 
 precedence_f (TotalOrdering _) = no_prec 

626 
 precedence_f (Subset _) = prec_Eq 

627 
 precedence_f (RelEq _) = prec_Eq 

628 
 precedence_f (IntEq _) = prec_Eq 

629 
 precedence_f (LT _) = prec_Eq 

630 
 precedence_f (LE _) = prec_Eq 

631 
 precedence_f (No _) = prec_Some 

632 
 precedence_f (Lone _) = prec_Some 

633 
 precedence_f (One _) = prec_Some 

634 
 precedence_f (Some _) = prec_Some 

635 
 precedence_f False = no_prec 

636 
 precedence_f True = no_prec 

637 
 precedence_f (FormulaReg _) = no_prec 

638 
and precedence_r (RelLet _) = prec_All 

639 
 precedence_r (RelIf _) = prec_All 

640 
 precedence_r (Union _) = prec_Add 

641 
 precedence_r (Difference _) = prec_Add 

642 
 precedence_r (Override _) = prec_Override 

643 
 precedence_r (Intersect _) = prec_Intersect 

644 
 precedence_r (Product _) = prec_Product 

645 
 precedence_r (IfNo _) = prec_IfNo 

646 
 precedence_r (Project _) = prec_Project 

647 
 precedence_r (Join _) = prec_Join 

648 
 precedence_r (Closure _) = prec_BitNot 

649 
 precedence_r (ReflexiveClosure _) = prec_BitNot 

650 
 precedence_r (Transpose _) = prec_BitNot 

651 
 precedence_r (Comprehension _) = no_prec 

652 
 precedence_r (Bits _) = no_prec 

653 
 precedence_r (Int _) = no_prec 

654 
 precedence_r Iden = no_prec 

655 
 precedence_r Ints = no_prec 

656 
 precedence_r None = no_prec 

657 
 precedence_r Univ = no_prec 

658 
 precedence_r (Atom _) = no_prec 

659 
 precedence_r (AtomSeq _) = no_prec 

660 
 precedence_r (Rel _) = no_prec 

661 
 precedence_r (Var _) = no_prec 

662 
 precedence_r (RelReg _) = no_prec 

663 
and precedence_i (Sum _) = prec_All 

664 
 precedence_i (IntLet _) = prec_All 

665 
 precedence_i (IntIf _) = prec_All 

666 
 precedence_i (SHL _) = prec_SHL 

667 
 precedence_i (SHA _) = prec_SHL 

668 
 precedence_i (SHR _) = prec_SHL 

669 
 precedence_i (Add _) = prec_Add 

670 
 precedence_i (Sub _) = prec_Add 

671 
 precedence_i (Mult _) = prec_Mult 

672 
 precedence_i (Div _) = prec_Mult 

673 
 precedence_i (Mod _) = prec_Mult 

674 
 precedence_i (Cardinality _) = no_prec 

675 
 precedence_i (SetSum _) = no_prec 

676 
 precedence_i (BitOr _) = prec_Intersect 

677 
 precedence_i (BitXor _) = prec_Intersect 

678 
 precedence_i (BitAnd _) = prec_Intersect 

679 
 precedence_i (BitNot _) = prec_BitNot 

680 
 precedence_i (Neg _) = prec_BitNot 

681 
 precedence_i (Absolute _) = prec_BitNot 

682 
 precedence_i (Signum _) = prec_BitNot 

683 
 precedence_i (Num _) = no_prec 

684 
 precedence_i (IntReg _) = no_prec 

685 

686 
fun write_problem_file out problems = 

687 
let 

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

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

690 
 out_outmost_f f = out_f f prec_And 

691 
and out_f formula outer_prec = 

692 
let 

693 
val prec = precedence_f formula 

694 
val need_parens = (prec < outer_prec) 

695 
in 

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

697 
(case formula of 

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

699 
 Exist (ds, f) => 

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

701 
 FormulaLet (bs, f) => 

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

703 
 FormulaIf (f, f1, f2) => 

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

705 
out_f f2 prec) 

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

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

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

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

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

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

712 
 Function (x, r1, r2) => 

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

714 
out_r r2 0; out ")") 

715 
 Functional (x, r1, r2) => 

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

717 
out_r r2 0; out ")") 

718 
 TotalOrdering (x1, x2, x3, x4) => 

719 
out ("TOTAL_ORDERING(" ^ rel_name x1 ^ ", " ^ rel_name x2 ^ ", " 

720 
^ rel_name x3 ^ ", " ^ rel_name x4 ^ ")") 

721 
 Subset (r1, r2) => (out_r r1 prec; out " in "; out_r r2 prec) 

722 
 RelEq (r1, r2) => (out_r r1 prec; out " = "; out_r r2 prec) 

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

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

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

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

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

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

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

730 
 False => out "false" 

731 
 True => out "true" 

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

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

734 
end 

735 
and out_r rel_expr outer_prec = 

736 
let 

737 
val prec = precedence_r rel_expr 

738 
val need_parens = (prec < outer_prec) 

739 
in 

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

741 
(case rel_expr of 

742 
RelLet (bs, r) => 

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

744 
 RelIf (f, r1, r2) => 

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

746 
out " else "; out_r r2 prec) 

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

748 
 Difference (r1, r2) => 

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

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

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

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

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

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

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

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

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

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

759 
 Comprehension (ds, f) => 

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

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

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

763 
 Iden => out "iden" 

764 
 Ints => out "ints" 

765 
 None => out "none" 

766 
 Univ => out "univ" 

767 
 Atom j => out (atom_name j) 

768 
 AtomSeq x => out (atom_seq_name x) 

769 
 Rel x => out (rel_name x) 

770 
 Var x => out (var_name x) 

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

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

773 
end 

774 
and out_i int_expr outer_prec = 

775 
let 

776 
val prec = precedence_i int_expr 

777 
val need_parens = (prec < outer_prec) 

778 
in 

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

780 
(case int_expr of 

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

782 
 IntLet (bs, i) => 

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

784 
 IntIf (f, i1, i2) => 

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

786 
out " else "; out_i i2 prec) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

804 
 Num k => out (signed_string_of_int k) 
33192  805 
 IntReg j => out (int_reg_name j)); 
806 
(if need_parens then out ")" else ()) 

807 
end 

808 
and out_decls [] = () 

809 
 out_decls [d] = out_decl d 

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

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

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

813 
 out_decl (DeclLone (x, r)) = 

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

815 
 out_decl (DeclOne (x, r)) = 

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

817 
 out_decl (DeclSome (x, r)) = 

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

819 
 out_decl (DeclSet (x, r)) = 

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

821 
and out_assigns [] = () 

822 
 out_assigns [b] = out_assign b 

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

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

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

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

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

828 
 out_assign (AssignIntReg (j, i)) = 

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

830 
and out_columns [] = () 

831 
 out_columns [i] = out_i i 0 

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

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

834 
int_bounds, expr_assigns, formula} = 

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

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

837 
settings) ^ 

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

839 
implode (map string_for_tuple_assign tuple_assigns) ^ 

840 
implode (map string_for_bound bounds) ^ 

841 
(if int_bounds = [] then 

842 
"" 

843 
else 

844 
"int_bounds: " ^ 

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

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

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

848 
in 

35695  849 
out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^ 
36381  850 
"// " ^ Sledgehammer_Util.timestamp () ^ "\n"); 
33192  851 
map out_problem problems 
852 
end 

853 

35718  854 
(** Parsing of solution **) 
855 

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

857 
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

858 
s = "_" orelse s = "'" orelse s = "$" 
33192  859 

860 
fun strip_blanks [] = [] 

861 
 strip_blanks (" " :: ss) = strip_blanks ss 

862 
 strip_blanks [s1, " "] = [s1] 

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

864 
if is_ident_char s1 andalso is_ident_char s2 then 

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

866 
else 

867 
strip_blanks (s1 :: s2 :: ss) 

868 
 strip_blanks (s :: ss) = s :: strip_blanks ss 

869 

870 
fun scan_non_empty_list scan = scan ::: Scan.repeat ($$ ","  scan) 

871 
fun scan_list scan = scan_non_empty_list scan  Scan.succeed [] 

872 
val scan_nat = Scan.repeat1 (Scan.one Symbol.is_ascii_digit) 

873 
>> (the o Int.fromString o space_implode "") 

874 
val scan_rel_name = $$ "s"  scan_nat >> pair 1 

875 
 $$ "r"  scan_nat >> pair 2 

876 
 ($$ "m"  scan_nat  $$ "_")  scan_nat 

877 
val scan_atom = $$ "A"  scan_nat 

878 
val scan_tuple = $$ "["  scan_list scan_atom  $$ "]" 

879 
val scan_tuple_set = $$ "["  scan_list scan_tuple  $$ "]" 

880 
val scan_assignment = (scan_rel_name  $$ "=")  scan_tuple_set 

881 
val scan_instance = Scan.this_string "relations:"  

882 
$$ "{"  scan_list scan_assignment  $$ "}" 

883 

35336  884 
val parse_instance = 
885 
fst o Scan.finite Symbol.stopper 

886 
(Scan.error (!! (fn _ => 

887 
raise SYNTAX ("Kodkod.parse_instance", 

888 
"illformed Kodkodi output")) 

889 
scan_instance)) 

890 
o strip_blanks o explode 

33192  891 

892 
val problem_marker = "*** PROBLEM " 

893 
val outcome_marker = "OUTCOME\n" 

894 
val instance_marker = "INSTANCE\n" 

895 

896 
fun read_section_body marker = 

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

898 
o Substring.triml (size marker) 

899 

900 
fun read_next_instance s = 

901 
let val s = Substring.position instance_marker s > snd in 

902 
if Substring.isEmpty s then 

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

904 
else 

905 
read_section_body instance_marker s > parse_instance 

906 
end 

907 

908 
fun read_next_outcomes j (s, ps, js) = 

909 
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

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

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

912 
> snd)) then 
33192  913 
(s, ps, js) 
914 
else 

915 
let 

916 
val outcome = read_section_body outcome_marker s2 

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

918 
in 

919 
if String.isSuffix "UNSATISFIABLE" outcome then 

920 
read_next_outcomes j (s, ps, j :: js) 

921 
else if String.isSuffix "SATISFIABLE" outcome then 

922 
read_next_outcomes j (s, (j, read_next_instance s2) :: ps, js) 

923 
else 

924 
raise SYNTAX ("Kodkod.read_next_outcomes", 

925 
"unknown outcome " ^ quote outcome) 

926 
end 

927 
end 

928 

929 
fun read_next_problems (s, ps, js) = 

930 
let val s = Substring.position problem_marker s > snd in 

931 
if Substring.isEmpty s then 

932 
(ps, js) 

933 
else 

934 
let 

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

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

937 
> Int.fromString > the 

938 
val j = j_plus_1  1 

939 
in read_next_problems (read_next_outcomes j (s, ps, js)) end 

940 
end 

941 
handle Option.Option => raise SYNTAX ("Kodkod.read_next_problems", 

942 
"expected number after \"PROBLEM\"") 

943 

944 
fun read_output_file path = 

35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset

945 
(false, read_next_problems (Substring.full (File.read path), [], []) 
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset

946 
>> rev > rev) 
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset

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

35718  949 
(** Main Kodkod entry point **) 
950 

951 
val created_temp_dir = Unsynchronized.ref false 

952 

953 
fun serial_string_and_temporary_dir_for_overlord overlord = 

954 
if overlord then 

955 
("", getenv "ISABELLE_HOME_USER") 

956 
else 

957 
let 

958 
val dir = getenv "ISABELLE_TMP" 

959 
val _ = if !created_temp_dir then () 

960 
else (created_temp_dir := true; File.mkdir (Path.explode dir)) 

961 
in (serial_string (), dir) end 

962 

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

965 
val fudge_ms = 250 

966 

967 
fun milliseconds_until_deadline deadline = 

968 
case deadline of 

969 
NONE => ~1 

970 
 SOME time => 

971 
Int.max (0, Time.toMilliseconds (Time. (time, Time.now ()))  fudge_ms) 

972 

973 
fun uncached_solve_any_problem overlord deadline max_threads max_solutions 

974 
problems = 

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

976 
val j = find_index (curry (op =) True o #formula) problems 
33192  977 
val indexed_problems = if j >= 0 then 
978 
[(j, nth problems j)] 

979 
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

980 
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

981 
(0 upto length problems  1 ~~ problems) 
33192  982 
val triv_js = filter_out (AList.defined (op =) indexed_problems) 
983 
(0 upto length problems  1) 

984 
val reindex = fst o nth indexed_problems 

985 
in 

986 
if null indexed_problems then 

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

987 
Normal ([], triv_js, "") 
33192  988 
else 
989 
let 

34998  990 
val (serial_str, temp_dir) = 
991 
serial_string_and_temporary_dir_for_overlord overlord 

992 
fun path_for suf = 

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

994 
val in_path = path_for "kki" 

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

34998  997 
val out_path = path_for "out" 
998 
val err_path = path_for "err" 

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

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

1002 
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

1003 
else List.app (K () o try File.rm) [in_path, out_path, err_path] 
33192  1004 
in 
1005 
let 

35814  1006 
val ms = milliseconds_until_deadline deadline 
33192  1007 
val outcome = 
1008 
let 

1009 
val code = 

35011
9e55e87434ff
proper treatment of paths passed to the shell  to allow spaces in file names as usual;
wenzelm
parents:
35010
diff
changeset

1010 
bash ("cd " ^ File.shell_quote temp_dir ^ ";\n" ^ 
35079  1011 
"env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \ 
1012 
\JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\ 

1013 
\$JAVA_LIBRARY_PATH\" \ 

1014 
\LD_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\ 

1015 
\$LD_LIBRARY_PATH\" \ 

1016 
\\"$KODKODI\"/bin/kodkodi" ^ 

1017 
(if ms >= 0 then " maxmsecs " ^ string_of_int ms 

1018 
else "") ^ 

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

1020 
" maxsolutions " ^ string_of_int max_solutions ^ 

1021 
(if max_threads > 0 then 

1022 
" maxthreads " ^ string_of_int max_threads 

1023 
else 

1024 
"") ^ 

1025 
" < " ^ File.shell_path in_path ^ 

1026 
" > " ^ File.shell_path out_path ^ 

1027 
" 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

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

1029 
read_output_file out_path 
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset

1030 
> apfst (map (apfst reindex)) > apsnd (map reindex) 
33192  1031 
val js = triv_js @ nontriv_js 
1032 
val first_error = 

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

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

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

36914  1037 
> perhaps (try (unprefix "Solve error: ")) 
35695  1038 
> perhaps (try (unprefix "Error: ")) 
33192  1039 
in 
1040 
if null ps then 

1041 
if code = 2 then 

1042 
TimedOut js 

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

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

1044 
Normal ([], js, first_error) 
33233
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset

1045 
else if first_error > Substring.full 
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35695
diff
changeset

1046 
> Substring.position "exec: java" > snd 
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35695
diff
changeset

1047 
> Substring.isEmpty > not then 
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35695
diff
changeset

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

1049 
else if first_error > Substring.full 
33233
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset

1050 
> Substring.position "NoClassDefFoundError" > snd 
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset

1051 
> Substring.isEmpty > not then 
35696
17ae461d6133
show nice error message in Nitpick when "java" is not available
blanchet
parents:
35695
diff
changeset

1052 
KodkodiNotInstalled 
33192  1053 
else if first_error <> "" then 
35695  1054 
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

1055 
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

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

1057 
else 
33192  1058 
Error ("Unknown error", js) 
1059 
else 

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

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

1062 
in remove_temporary_files (); outcome end 
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset

1063 
handle Exn.Interrupt => 
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset

1064 
let 
35309
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset

1065 
val nontriv_js = 
997aa3a3e4bb
catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
blanchet
parents:
35280
diff
changeset

1066 
read_output_file out_path > snd > snd > map reindex 
33575
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset

1067 
in 
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset

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

1069 
Interrupted (SOME (triv_js @ nontriv_js))) 
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset

1070 
handle Exn.Interrupt => 
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset

1071 
(remove_temporary_files (); Interrupted NONE) 
118517551c12
try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet
parents:
33233
diff
changeset

1072 
end 
33192  1073 
end 
1074 
end 

1075 

35814  1076 
val cached_outcome = 
1077 
Synchronized.var "Kodkod.cached_outcome" 

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

1079 

1080 
fun solve_any_problem overlord deadline max_threads max_solutions problems = 

1081 
let 

1082 
fun do_solve () = uncached_solve_any_problem overlord deadline max_threads 

1083 
max_solutions problems 

1084 
in 

1085 
if overlord then 

1086 
do_solve () 

1087 
else 

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

1089 
max1 = max2 andalso length ps1 = length ps2 andalso 

1090 
forall problems_equivalent (ps1 ~~ ps2)) 

1091 
(the_list (Synchronized.value cached_outcome)) 

1092 
(max_solutions, problems) of 

1093 
SOME outcome => outcome 

1094 
 NONE => 

1095 
let val outcome = do_solve () in 

1096 
(case outcome of 

1097 
Normal (ps, js, "") => 

1098 
Synchronized.change cached_outcome 

1099 
(K (SOME ((max_solutions, problems), outcome))) 

1100 
 _ => ()); 

1101 
outcome 

1102 
end 

1103 
end 

1104 

33192  1105 
end; 