author  blanchet 
Fri, 29 Oct 2010 12:49:05 +0200  
changeset 40265  ee578bc82cbc 
parent 39456  37f1a961a918 
child 40381  96c37a685a13 
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 

39456  5 
ML interface for Kodkod. 
33192  6 
*) 
7 

8 
signature KODKOD = 

9 
sig 

10 
type n_ary_index = int * int 

11 
type setting = string * string 

12 

13 
datatype tuple = 

14 
Tuple of int list  

15 
TupleIndex of n_ary_index  

16 
TupleReg of n_ary_index 

17 

18 
datatype tuple_set = 

19 
TupleUnion of tuple_set * tuple_set  

20 
TupleDifference of tuple_set * tuple_set  

21 
TupleIntersect of tuple_set * tuple_set  

22 
TupleProduct of tuple_set * tuple_set  

23 
TupleProject of tuple_set * int  

24 
TupleSet of tuple list  

25 
TupleRange of tuple * tuple  

26 
TupleArea of tuple * tuple  

27 
TupleAtomSeq of int * int  

28 
TupleSetReg of n_ary_index 

29 

30 
datatype tuple_assign = 

31 
AssignTuple of n_ary_index * tuple  

32 
AssignTupleSet of n_ary_index * tuple_set 

33 

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

35 
type int_bound = int option * tuple_set list 

36 

37 
datatype formula = 

38 
All of decl list * formula  

39 
Exist of decl list * formula  

40 
FormulaLet of expr_assign list * formula  

41 
FormulaIf of formula * formula * formula  

42 
Or of formula * formula  

43 
Iff of formula * formula  

44 
Implies of formula * formula  

45 
And of formula * formula  

46 
Not of formula  

47 
Acyclic of n_ary_index  

48 
Function of n_ary_index * rel_expr * rel_expr  

49 
Functional of n_ary_index * rel_expr * rel_expr  

38126  50 
TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr  
33192  51 
Subset of rel_expr * rel_expr  
52 
RelEq of rel_expr * rel_expr  

53 
IntEq of int_expr * int_expr  

54 
LT of int_expr * int_expr  

55 
LE of int_expr * int_expr  

56 
No of rel_expr  

57 
Lone of rel_expr  

58 
One of rel_expr  

59 
Some of rel_expr  

60 
False  

61 
True  

62 
FormulaReg of int 

63 
and rel_expr = 

64 
RelLet of expr_assign list * rel_expr  

65 
RelIf of formula * rel_expr * rel_expr  

66 
Union of rel_expr * rel_expr  

67 
Difference of rel_expr * rel_expr  

68 
Override of rel_expr * rel_expr  

69 
Intersect of rel_expr * rel_expr  

70 
Product of rel_expr * rel_expr  

71 
IfNo of rel_expr * rel_expr  

72 
Project of rel_expr * int_expr list  

73 
Join of rel_expr * rel_expr  

74 
Closure of rel_expr  

75 
ReflexiveClosure of rel_expr  

76 
Transpose of rel_expr  

77 
Comprehension of decl list * formula  

78 
Bits of int_expr  

79 
Int of int_expr  

80 
Iden  

81 
Ints  

82 
None  

83 
Univ  

84 
Atom of int  

85 
AtomSeq of int * int  

86 
Rel of n_ary_index  

87 
Var of n_ary_index  

88 
RelReg of n_ary_index 

89 
and int_expr = 

90 
Sum of decl list * int_expr  

91 
IntLet of expr_assign list * int_expr  

92 
IntIf of formula * int_expr * int_expr  

93 
SHL of int_expr * int_expr  

94 
SHA of int_expr * int_expr  

95 
SHR of int_expr * int_expr  

96 
Add of int_expr * int_expr  

97 
Sub of int_expr * int_expr  

98 
Mult of int_expr * int_expr  

99 
Div of int_expr * int_expr  

100 
Mod of int_expr * int_expr  

101 
Cardinality of rel_expr  

102 
SetSum of rel_expr  

103 
BitOr of int_expr * int_expr  

104 
BitXor of int_expr * int_expr  

105 
BitAnd of int_expr * int_expr  

106 
BitNot of int_expr  

107 
Neg of int_expr  

108 
Absolute of int_expr  

109 
Signum of int_expr  

110 
Num of int  

111 
IntReg of int 

112 
and decl = 

113 
DeclNo of n_ary_index * rel_expr  

114 
DeclLone of n_ary_index * rel_expr  

115 
DeclOne of n_ary_index * rel_expr  

116 
DeclSome of n_ary_index * rel_expr  

117 
DeclSet of n_ary_index * rel_expr 

118 
and expr_assign = 

119 
AssignFormulaReg of int * formula  

120 
AssignRelReg of n_ary_index * rel_expr  

121 
AssignIntReg of int * int_expr 

122 

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

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

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

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

126 
int_expr_func: int_expr > 'a > 'a} 
33192  127 

128 
val fold_formula : 'a fold_expr_funcs > formula > 'a > 'a 

129 
val fold_rel_expr : 'a fold_expr_funcs > rel_expr > 'a > 'a 

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

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

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

133 

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

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

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

136 
tuple_set_func: tuple_set > 'a > 'a} 
33192  137 

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

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

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

141 
val fold_bound : 

142 
'a fold_expr_funcs > 'a fold_tuple_funcs > bound > 'a > 'a 

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

144 

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

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

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

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

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

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

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

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

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

153 
formula: formula} 
33192  154 

155 
type raw_bound = n_ary_index * int list list 

156 

157 
datatype outcome = 

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

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

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

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

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

164 
Error of string * int list 

165 

166 
exception SYNTAX of string * string 

167 

168 
val max_arity : int > int 

169 
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

170 
val is_problem_trivially_false : problem > bool 
35814  171 
val problems_equivalent : problem * problem > bool 
33192  172 
val solve_any_problem : 
173 
bool > Time.time option > int > int > problem list > outcome 

174 
end; 

175 

176 
structure Kodkod : KODKOD = 

177 
struct 

178 

179 
type n_ary_index = int * int 

180 

181 
type setting = string * string 

182 

183 
datatype tuple = 

184 
Tuple of int list  

185 
TupleIndex of n_ary_index  

186 
TupleReg of n_ary_index 

187 

188 
datatype tuple_set = 

189 
TupleUnion of tuple_set * tuple_set  

190 
TupleDifference of tuple_set * tuple_set  

191 
TupleIntersect of tuple_set * tuple_set  

192 
TupleProduct of tuple_set * tuple_set  

193 
TupleProject of tuple_set * int  

194 
TupleSet of tuple list  

195 
TupleRange of tuple * tuple  

196 
TupleArea of tuple * tuple  

197 
TupleAtomSeq of int * int  

198 
TupleSetReg of n_ary_index 

199 

200 
datatype tuple_assign = 

201 
AssignTuple of n_ary_index * tuple  

202 
AssignTupleSet of n_ary_index * tuple_set 

203 

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

205 
type int_bound = int option * tuple_set list 

206 

207 
datatype formula = 

208 
All of decl list * formula  

209 
Exist of decl list * formula  

210 
FormulaLet of expr_assign list * formula  

211 
FormulaIf of formula * formula * formula  

212 
Or of formula * formula  

213 
Iff of formula * formula  

214 
Implies of formula * formula  

215 
And of formula * formula  

216 
Not of formula  

217 
Acyclic of n_ary_index  

218 
Function of n_ary_index * rel_expr * rel_expr  

219 
Functional of n_ary_index * rel_expr * rel_expr  

38126  220 
TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr  
33192  221 
Subset of rel_expr * rel_expr  
222 
RelEq of rel_expr * rel_expr  

223 
IntEq of int_expr * int_expr  

224 
LT of int_expr * int_expr  

225 
LE of int_expr * int_expr  

226 
No of rel_expr  

227 
Lone of rel_expr  

228 
One of rel_expr  

229 
Some of rel_expr  

230 
False  

231 
True  

232 
FormulaReg of int 

233 
and rel_expr = 

234 
RelLet of expr_assign list * rel_expr  

235 
RelIf of formula * rel_expr * rel_expr  

236 
Union of rel_expr * rel_expr  

237 
Difference of rel_expr * rel_expr  

238 
Override of rel_expr * rel_expr  

239 
Intersect of rel_expr * rel_expr  

240 
Product of rel_expr * rel_expr  

241 
IfNo of rel_expr * rel_expr  

242 
Project of rel_expr * int_expr list  

243 
Join of rel_expr * rel_expr  

244 
Closure of rel_expr  

245 
ReflexiveClosure of rel_expr  

246 
Transpose of rel_expr  

247 
Comprehension of decl list * formula  

248 
Bits of int_expr  

249 
Int of int_expr  

250 
Iden  

251 
Ints  

252 
None  

253 
Univ  

254 
Atom of int  

255 
AtomSeq of int * int  

256 
Rel of n_ary_index  

257 
Var of n_ary_index  

258 
RelReg of n_ary_index 

259 
and int_expr = 

260 
Sum of decl list * int_expr  

261 
IntLet of expr_assign list * int_expr  

262 
IntIf of formula * int_expr * int_expr  

263 
SHL of int_expr * int_expr  

264 
SHA of int_expr * int_expr  

265 
SHR of int_expr * int_expr  

266 
Add of int_expr * int_expr  

267 
Sub of int_expr * int_expr  

268 
Mult of int_expr * int_expr  

269 
Div of int_expr * int_expr  

270 
Mod of int_expr * int_expr  

271 
Cardinality of rel_expr  

272 
SetSum of rel_expr  

273 
BitOr of int_expr * int_expr  

274 
BitXor of int_expr * int_expr  

275 
BitAnd of int_expr * int_expr  

276 
BitNot of int_expr  

277 
Neg of int_expr  

278 
Absolute of int_expr  

279 
Signum of int_expr  

280 
Num of int  

281 
IntReg of int 

282 
and decl = 

283 
DeclNo of n_ary_index * rel_expr  

284 
DeclLone of n_ary_index * rel_expr  

285 
DeclOne of n_ary_index * rel_expr  

286 
DeclSome of n_ary_index * rel_expr  

287 
DeclSet of n_ary_index * rel_expr 

288 
and expr_assign = 

289 
AssignFormulaReg of int * formula  

290 
AssignRelReg of n_ary_index * rel_expr  

291 
AssignIntReg of int * int_expr 

292 

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

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

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

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

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

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

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

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

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

301 
formula: formula} 
33192  302 

303 
type raw_bound = n_ary_index * int list list 

304 

305 
datatype outcome = 

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

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

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

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

309 
Normal of (int * raw_bound list) list * int list * string  
33192  310 
TimedOut of int list  
311 
Interrupted of int list option  

312 
Error of string * int list 

313 

314 
exception SYNTAX of string * string 

315 

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

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

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

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

319 
int_expr_func: int_expr > 'a > 'a} 
33192  320 

38126  321 
fun is_new_kodkodi_version () = 
322 
case getenv "KODKODI_VERSION" of 

323 
"" => false 

324 
 s => dict_ord int_ord (s > space_explode "." 

38130  325 
> map (the_default 0 o Int.fromString), 
38126  326 
[1, 2, 13]) = GREATER 
327 

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

35718  329 

33192  330 
fun fold_formula (F : 'a fold_expr_funcs) formula = 
331 
case formula of 

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

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

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

335 
 FormulaIf (f, f1, f2) => 

336 
fold_formula F f #> fold_formula F f1 #> fold_formula F f2 

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

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

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

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

341 
 Not f => fold_formula F f 

342 
 Acyclic x => fold_rel_expr F (Rel x) 

343 
 Function (x, r1, r2) => 

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

345 
 Functional (x, r1, r2) => 

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

38126  347 
 TotalOrdering (x, r1, r2, r3) => 
348 
fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2 

349 
#> fold_rel_expr F r3 

33192  350 
 Subset (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 
351 
 RelEq (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2 

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

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

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

355 
 No r => fold_rel_expr F r 

356 
 Lone r => fold_rel_expr F r 

357 
 One r => fold_rel_expr F r 

358 
 Some r => fold_rel_expr F r 

359 
 False => #formula_func F formula 

360 
 True => #formula_func F formula 

361 
 FormulaReg _ => #formula_func F formula 

362 
and fold_rel_expr F rel_expr = 

363 
case rel_expr of 

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

365 
 RelIf (f, r1, r2) => 

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

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

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

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

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

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

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

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

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

375 
 Closure r => fold_rel_expr F r 

376 
 ReflexiveClosure r => fold_rel_expr F r 

377 
 Transpose r => fold_rel_expr F r 

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

379 
 Bits i => fold_int_expr F i 

380 
 Int i => fold_int_expr F i 

381 
 Iden => #rel_expr_func F rel_expr 

382 
 Ints => #rel_expr_func F rel_expr 

383 
 None => #rel_expr_func F rel_expr 

384 
 Univ => #rel_expr_func F rel_expr 

385 
 Atom _ => #rel_expr_func F rel_expr 

386 
 AtomSeq _ => #rel_expr_func F rel_expr 

387 
 Rel _ => #rel_expr_func F rel_expr 

388 
 Var _ => #rel_expr_func F rel_expr 

389 
 RelReg _ => #rel_expr_func F rel_expr 

390 
and fold_int_expr F int_expr = 

391 
case int_expr of 

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

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

394 
 IntIf (f, i1, i2) => 

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

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

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

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

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

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

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

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

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

404 
 Cardinality r => fold_rel_expr F r 

405 
 SetSum r => fold_rel_expr F r 

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

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

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

409 
 BitNot i => fold_int_expr F i 

410 
 Neg i => fold_int_expr F i 

411 
 Absolute i => fold_int_expr F i 

412 
 Signum i => fold_int_expr F i 

413 
 Num _ => #int_expr_func F int_expr 

414 
 IntReg _ => #int_expr_func F int_expr 

415 
and fold_decl F decl = 

416 
case decl of 

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

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

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

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

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

422 
and fold_expr_assign F assign = 

423 
case assign of 

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

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

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

427 

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

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

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

430 
tuple_set_func: tuple_set > 'a > 'a} 
33192  431 

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

433 
fun fold_tuple_set F tuple_set = 

434 
case tuple_set of 

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

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

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

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

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

440 
 TupleSet ts => fold (fold_tuple F) ts 

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

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

443 
 TupleAtomSeq _ => #tuple_set_func F tuple_set 

444 
 TupleSetReg _ => #tuple_set_func F tuple_set 

445 
fun fold_tuple_assign F assign = 

446 
case assign of 

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

448 
 AssignTupleSet (x, ts) => 

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

450 
fun fold_bound expr_F tuple_F (zs, tss) = 

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

452 
#> fold (fold_tuple_set tuple_F) tss 

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

454 

455 
fun max_arity univ_card = floor (Math.ln 2147483647.0 

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

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

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

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

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

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

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

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

464 
 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

465 
 arity_of_rel_expr (Project (_, is)) = length is 
33192  466 
 arity_of_rel_expr (Join (r1, r2)) = sum_arities_of_rel_exprs r1 r2  2 
467 
 arity_of_rel_expr (Closure _) = 2 

468 
 arity_of_rel_expr (ReflexiveClosure _) = 2 

469 
 arity_of_rel_expr (Transpose _) = 2 

470 
 arity_of_rel_expr (Comprehension (ds, _)) = 

471 
fold (curry op + o arity_of_decl) ds 0 

472 
 arity_of_rel_expr (Bits _) = 1 

473 
 arity_of_rel_expr (Int _) = 1 

474 
 arity_of_rel_expr Iden = 2 

475 
 arity_of_rel_expr Ints = 1 

476 
 arity_of_rel_expr None = 1 

477 
 arity_of_rel_expr Univ = 1 

478 
 arity_of_rel_expr (Atom _) = 1 

479 
 arity_of_rel_expr (AtomSeq _) = 1 

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

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

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

483 
and sum_arities_of_rel_exprs r1 r2 = arity_of_rel_expr r1 + arity_of_rel_expr r2 

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

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

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

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

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

489 

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

490 
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

491 
 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

492 

35814  493 
val chop_solver = take 2 o space_explode "," 
33192  494 

35814  495 
fun settings_equivalent ([], []) = true 
496 
 settings_equivalent ((key1, value1) :: settings1, 

497 
(key2, value2) :: settings2) = 

498 
key1 = key2 andalso 

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

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

501 
settings_equivalent (settings1, settings2) 

502 
 settings_equivalent _ = false 

503 

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

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

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

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

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

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

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

510 
#int_bounds p1 = #int_bounds p2 andalso 
35814  511 
settings_equivalent (#settings p1, #settings p2) 
33192  512 

35718  513 
(** Serialization of problem **) 
34998  514 

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

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

516 
if j < 0 then string_of_int (~j  1) ^ "'" else string_of_int j 
33192  517 

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

519 
 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

520 
 n_ary_name (n, j) _ _ prefix = prefix ^ string_of_int n ^ "_" ^ base_name j 
33192  521 

522 
fun atom_name j = "A" ^ base_name j 

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

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

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

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

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

528 

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

38126  530 
fun rel_name new_kodkodi (n, j) = 
531 
n_ary_name (n, if new_kodkodi then j 

532 
else if j >= 0 then 2 * j 

533 
else 2 * ~j  1) "s" "r" "m" 

33192  534 
fun var_name x = n_ary_name x "S" "R" "M" 
535 
fun tuple_reg_name x = n_ary_name x "$A" "$P" "$T" 

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

537 

538 
fun inline_comment "" = "" 

539 
 inline_comment comment = 

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

541 
" */" 

542 
fun block_comment "" = "" 

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

544 

38126  545 
fun commented_rel_name new_kodkodi (x, s) = 
546 
rel_name new_kodkodi x ^ inline_comment s 

33192  547 

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

549 
 string_for_tuple (TupleIndex x) = tuple_name x 

550 
 string_for_tuple (TupleReg x) = tuple_reg_name x 

551 

552 
val no_prec = 100 

553 
val prec_TupleUnion = 1 

554 
val prec_TupleIntersect = 2 

555 
val prec_TupleProduct = 3 

556 
val prec_TupleProject = 4 

557 

558 
fun precedence_ts (TupleUnion _) = prec_TupleUnion 

559 
 precedence_ts (TupleDifference _) = prec_TupleUnion 

560 
 precedence_ts (TupleIntersect _) = prec_TupleIntersect 

561 
 precedence_ts (TupleProduct _) = prec_TupleProduct 

562 
 precedence_ts (TupleProject _) = prec_TupleProject 

563 
 precedence_ts _ = no_prec 

564 

565 
fun string_for_tuple_set tuple_set = 

566 
let 

567 
fun sub tuple_set outer_prec = 

568 
let 

569 
val prec = precedence_ts tuple_set 

570 
val need_parens = (prec < outer_prec) 

571 
in 

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

573 
(case tuple_set of 

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

575 
 TupleDifference (ts1, ts2) => 

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

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

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

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

582 
"{" ^ string_for_tuple t1 ^ 

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

584 
 TupleArea (t1, t2) => 

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

586 
 TupleAtomSeq x => atom_seq_name x 

587 
 TupleSetReg x => tuple_set_reg_name x) ^ 

588 
(if need_parens then ")" else "") 

589 
end 

590 
in sub tuple_set 0 end 

591 

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

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

594 
 string_for_tuple_assign (AssignTupleSet (x, ts)) = 

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

596 

38126  597 
fun string_for_bound new_kodkodi (zs, tss) = 
598 
"bounds " ^ commas (map (commented_rel_name new_kodkodi) zs) ^ ": " ^ 

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

601 

602 
fun int_string_for_bound (opt_n, tss) = 

603 
(case opt_n of 

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

604 
SOME n => signed_string_of_int n ^ ": " 
33192  605 
 NONE => "") ^ "[" ^ commas (map string_for_tuple_set tss) ^ "]" 
606 

607 
val prec_All = 1 

608 
val prec_Or = 2 

609 
val prec_Iff = 3 

610 
val prec_Implies = 4 

611 
val prec_And = 5 

612 
val prec_Not = 6 

613 
val prec_Eq = 7 

614 
val prec_Some = 8 

615 
val prec_SHL = 9 

616 
val prec_Add = 10 

617 
val prec_Mult = 11 

618 
val prec_Override = 12 

619 
val prec_Intersect = 13 

620 
val prec_Product = 14 

621 
val prec_IfNo = 15 

622 
val prec_Project = 17 

623 
val prec_Join = 18 

624 
val prec_BitNot = 19 

625 

626 
fun precedence_f (All _) = prec_All 

627 
 precedence_f (Exist _) = prec_All 

628 
 precedence_f (FormulaLet _) = prec_All 

629 
 precedence_f (FormulaIf _) = prec_All 

630 
 precedence_f (Or _) = prec_Or 

631 
 precedence_f (Iff _) = prec_Iff 

632 
 precedence_f (Implies _) = prec_Implies 

633 
 precedence_f (And _) = prec_And 

634 
 precedence_f (Not _) = prec_Not 

635 
 precedence_f (Acyclic _) = no_prec 

636 
 precedence_f (Function _) = no_prec 

637 
 precedence_f (Functional _) = no_prec 

638 
 precedence_f (TotalOrdering _) = no_prec 

639 
 precedence_f (Subset _) = prec_Eq 

640 
 precedence_f (RelEq _) = prec_Eq 

641 
 precedence_f (IntEq _) = prec_Eq 

642 
 precedence_f (LT _) = prec_Eq 

643 
 precedence_f (LE _) = prec_Eq 

644 
 precedence_f (No _) = prec_Some 

645 
 precedence_f (Lone _) = prec_Some 

646 
 precedence_f (One _) = prec_Some 

647 
 precedence_f (Some _) = prec_Some 

648 
 precedence_f False = no_prec 

649 
 precedence_f True = no_prec 

650 
 precedence_f (FormulaReg _) = no_prec 

651 
and precedence_r (RelLet _) = prec_All 

652 
 precedence_r (RelIf _) = prec_All 

653 
 precedence_r (Union _) = prec_Add 

654 
 precedence_r (Difference _) = prec_Add 

655 
 precedence_r (Override _) = prec_Override 

656 
 precedence_r (Intersect _) = prec_Intersect 

657 
 precedence_r (Product _) = prec_Product 

658 
 precedence_r (IfNo _) = prec_IfNo 

659 
 precedence_r (Project _) = prec_Project 

660 
 precedence_r (Join _) = prec_Join 

661 
 precedence_r (Closure _) = prec_BitNot 

662 
 precedence_r (ReflexiveClosure _) = prec_BitNot 

663 
 precedence_r (Transpose _) = prec_BitNot 

664 
 precedence_r (Comprehension _) = no_prec 

665 
 precedence_r (Bits _) = no_prec 

666 
 precedence_r (Int _) = no_prec 

667 
 precedence_r Iden = no_prec 

668 
 precedence_r Ints = no_prec 

669 
 precedence_r None = no_prec 

670 
 precedence_r Univ = no_prec 

671 
 precedence_r (Atom _) = no_prec 

672 
 precedence_r (AtomSeq _) = no_prec 

673 
 precedence_r (Rel _) = no_prec 

674 
 precedence_r (Var _) = no_prec 

675 
 precedence_r (RelReg _) = no_prec 

676 
and precedence_i (Sum _) = prec_All 

677 
 precedence_i (IntLet _) = prec_All 

678 
 precedence_i (IntIf _) = prec_All 

679 
 precedence_i (SHL _) = prec_SHL 

680 
 precedence_i (SHA _) = prec_SHL 

681 
 precedence_i (SHR _) = prec_SHL 

682 
 precedence_i (Add _) = prec_Add 

683 
 precedence_i (Sub _) = prec_Add 

684 
 precedence_i (Mult _) = prec_Mult 

685 
 precedence_i (Div _) = prec_Mult 

686 
 precedence_i (Mod _) = prec_Mult 

687 
 precedence_i (Cardinality _) = no_prec 

688 
 precedence_i (SetSum _) = no_prec 

689 
 precedence_i (BitOr _) = prec_Intersect 

690 
 precedence_i (BitXor _) = prec_Intersect 

691 
 precedence_i (BitAnd _) = prec_Intersect 

692 
 precedence_i (BitNot _) = prec_BitNot 

693 
 precedence_i (Neg _) = prec_BitNot 

694 
 precedence_i (Absolute _) = prec_BitNot 

695 
 precedence_i (Signum _) = prec_BitNot 

696 
 precedence_i (Num _) = no_prec 

697 
 precedence_i (IntReg _) = no_prec 

698 

699 
fun write_problem_file out problems = 

700 
let 

38126  701 
val new_kodkodi = is_new_kodkodi_version () 
702 
val rel_name = rel_name new_kodkodi 

33192  703 
fun out_outmost_f (And (f1, f2)) = 
704 
(out_outmost_f f1; out "\n && "; out_outmost_f f2) 

705 
 out_outmost_f f = out_f f prec_And 

706 
and out_f formula outer_prec = 

707 
let 

708 
val prec = precedence_f formula 

709 
val need_parens = (prec < outer_prec) 

710 
in 

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

712 
(case formula of 

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

714 
 Exist (ds, f) => 

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

716 
 FormulaLet (bs, f) => 

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

718 
 FormulaIf (f, f1, f2) => 

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

720 
out_f f2 prec) 

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

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

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

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

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

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

727 
 Function (x, r1, r2) => 

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

729 
out_r r2 0; out ")") 

730 
 Functional (x, r1, r2) => 

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

732 
out_r r2 0; out ")") 

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

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

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

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

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

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

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

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

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

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

745 
 False => out "false" 

746 
 True => out "true" 

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

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

749 
end 

750 
and out_r rel_expr outer_prec = 

751 
let 

752 
val prec = precedence_r rel_expr 

753 
val need_parens = (prec < outer_prec) 

754 
in 

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

756 
(case rel_expr of 

757 
RelLet (bs, r) => 

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

759 
 RelIf (f, r1, r2) => 

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

761 
out " else "; out_r r2 prec) 

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

763 
 Difference (r1, r2) => 

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

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

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

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

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

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

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

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

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

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

774 
 Comprehension (ds, f) => 

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

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

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

778 
 Iden => out "iden" 

779 
 Ints => out "ints" 

780 
 None => out "none" 

781 
 Univ => out "univ" 

782 
 Atom j => out (atom_name j) 

783 
 AtomSeq x => out (atom_seq_name x) 

784 
 Rel x => out (rel_name x) 

785 
 Var x => out (var_name x) 

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

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

788 
end 

789 
and out_i int_expr outer_prec = 

790 
let 

791 
val prec = precedence_i int_expr 

792 
val need_parens = (prec < outer_prec) 

793 
in 

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

795 
(case int_expr of 

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

797 
 IntLet (bs, i) => 

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

799 
 IntIf (f, i1, i2) => 

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

801 
out " else "; out_i i2 prec) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

819 
 Num k => out (signed_string_of_int k) 
33192  820 
 IntReg j => out (int_reg_name j)); 
821 
(if need_parens then out ")" else ()) 

822 
end 

823 
and out_decls [] = () 

824 
 out_decls [d] = out_decl d 

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

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

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

828 
 out_decl (DeclLone (x, r)) = 

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

830 
 out_decl (DeclOne (x, r)) = 

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

832 
 out_decl (DeclSome (x, r)) = 

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

834 
 out_decl (DeclSet (x, r)) = 

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

836 
and out_assigns [] = () 

837 
 out_assigns [b] = out_assign b 

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

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

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

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

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

843 
 out_assign (AssignIntReg (j, i)) = 

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

845 
and out_columns [] = () 

846 
 out_columns [i] = out_i i 0 

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

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

849 
int_bounds, expr_assigns, formula} = 

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

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

852 
settings) ^ 

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

854 
implode (map string_for_tuple_assign tuple_assigns) ^ 

38126  855 
implode (map (string_for_bound new_kodkodi) bounds) ^ 
33192  856 
(if int_bounds = [] then 
857 
"" 

858 
else 

859 
"int_bounds: " ^ 

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

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

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

863 
in 

35695  864 
out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^ 
38019
e207a64e1e0b
complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
blanchet
parents:
36914
diff
changeset

865 
"// " ^ ATP_Problem.timestamp () ^ "\n"); 
33192  866 
map out_problem problems 
867 
end 

868 

35718  869 
(** Parsing of solution **) 
870 

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

872 
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

873 
s = "_" orelse s = "'" orelse s = "$" 
33192  874 

875 
fun strip_blanks [] = [] 

876 
 strip_blanks (" " :: ss) = strip_blanks ss 

877 
 strip_blanks [s1, " "] = [s1] 

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

879 
if is_ident_char s1 andalso is_ident_char s2 then 

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

881 
else 

882 
strip_blanks (s1 :: s2 :: ss) 

883 
 strip_blanks (s :: ss) = s :: strip_blanks ss 

884 

38198  885 
val scan_nat = 
886 
Scan.repeat1 (Scan.one Symbol.is_ascii_digit) 

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

38126  888 
fun scan_rel_name new_kodkodi = 
889 
($$ "s"  scan_nat >> pair 1 

890 
 $$ "r"  scan_nat >> pair 2 

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

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

893 
 ((n, j), NONE) => (n, if new_kodkodi then j 

894 
else if j mod 2 = 0 then j div 2 

38130  895 
else ~(j + 1) div 2)) 
33192  896 
val scan_atom = $$ "A"  scan_nat 
38198  897 
fun parse_non_empty_list scan = scan ::: Scan.repeat ($$ ","  scan) 
898 
fun parse_list scan = parse_non_empty_list scan  Scan.succeed [] 

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

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

901 
fun parse_assignment new_kodkodi = 

902 
(scan_rel_name new_kodkodi  $$ "=")  parse_tuple_set 

903 
fun parse_instance new_kodkodi = 

38126  904 
Scan.this_string "relations:" 
38198  905 
 $$ "{"  parse_list (parse_assignment new_kodkodi)  $$ "}" 
33192  906 

38198  907 
fun extract_instance new_kodkodi = 
35336  908 
fst o Scan.finite Symbol.stopper 
909 
(Scan.error (!! (fn _ => 

38198  910 
raise SYNTAX ("Kodkod.extract_instance", 
35336  911 
"illformed Kodkodi output")) 
38198  912 
(parse_instance new_kodkodi))) 
35336  913 
o strip_blanks o 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 

38126  923 
fun read_next_instance new_kodkodi 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 

38198  928 
read_section_body instance_marker s > extract_instance new_kodkodi 
33192  929 
end 
930 

38126  931 
fun read_next_outcomes new_kodkodi 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 

38126  943 
read_next_outcomes new_kodkodi j (s, ps, j :: js) 
33192  944 
else if String.isSuffix "SATISFIABLE" outcome then 
38126  945 
read_next_outcomes new_kodkodi j 
946 
(s, (j, read_next_instance new_kodkodi s2) :: ps, js) 

33192  947 
else 
948 
raise SYNTAX ("Kodkod.read_next_outcomes", 

949 
"unknown outcome " ^ quote outcome) 

950 
end 

951 
end 

952 

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

956 
(ps, js) 

957 
else 

958 
let 

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

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

961 
> Int.fromString > the 

962 
val j = j_plus_1  1 

38126  963 
in 
964 
read_next_problems new_kodkodi 

965 
(read_next_outcomes new_kodkodi j (s, ps, js)) 

966 
end 

33192  967 
end 
968 
handle Option.Option => raise SYNTAX ("Kodkod.read_next_problems", 

969 
"expected number after \"PROBLEM\"") 

970 

38126  971 
fun read_output_file new_kodkodi path = 
972 
(false, 

973 
read_next_problems new_kodkodi (Substring.full (File.read path), [], []) 

974 
>> rev > rev) 

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

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

35718  977 
(** Main Kodkod entry point **) 
978 

979 
val created_temp_dir = Unsynchronized.ref false 

980 

981 
fun serial_string_and_temporary_dir_for_overlord overlord = 

982 
if overlord then 

983 
("", getenv "ISABELLE_HOME_USER") 

984 
else 

985 
let 

986 
val dir = getenv "ISABELLE_TMP" 

987 
val _ = if !created_temp_dir then () 

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

989 
in (serial_string (), dir) end 

990 

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

993 
val fudge_ms = 250 

994 

995 
fun milliseconds_until_deadline deadline = 

996 
case deadline of 

997 
NONE => ~1 

998 
 SOME time => 

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

1000 

1001 
fun uncached_solve_any_problem overlord deadline max_threads max_solutions 

1002 
problems = 

33192  1003 
let 
38126  1004 
val new_kodkodi = is_new_kodkodi_version () 
34121
5e831d805118
get rid of polymorphic equality in Nitpick's code + a few minor cleanups
blanchet
parents:
33982
diff
changeset

1005 
val j = find_index (curry (op =) True o #formula) problems 
33192  1006 
val indexed_problems = if j >= 0 then 
1007 
[(j, nth problems j)] 

1008 
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

1009 
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

1010 
(0 upto length problems  1 ~~ problems) 
33192  1011 
val triv_js = filter_out (AList.defined (op =) indexed_problems) 
1012 
(0 upto length problems  1) 

1013 
val reindex = fst o nth indexed_problems 

1014 
in 

1015 
if null indexed_problems then 

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

1016 
Normal ([], triv_js, "") 
33192  1017 
else 
1018 
let 

34998  1019 
val (serial_str, temp_dir) = 
1020 
serial_string_and_temporary_dir_for_overlord overlord 

1021 
fun path_for suf = 

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

1023 
val in_path = path_for "kki" 

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

34998  1026 
val out_path = path_for "out" 
1027 
val err_path = path_for "err" 

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

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

1031 
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

1032 
else List.app (K () o try File.rm) [in_path, out_path, err_path] 
33192  1033 
in 
1034 
let 

35814  1035 
val ms = milliseconds_until_deadline deadline 
33192  1036 
val outcome = 
1037 
let 

1038 
val code = 

40265
ee578bc82cbc
no need for setting up the kodkodi environment since Kodkodi 1.2.9
blanchet
parents:
39456
diff
changeset

1039 
bash ("cd " ^ File.shell_quote temp_dir ^ ";\n\ 
35079  1040 
\\"$KODKODI\"/bin/kodkodi" ^ 
1041 
(if ms >= 0 then " maxmsecs " ^ string_of_int ms 

1042 
else "") ^ 

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

1044 
" maxsolutions " ^ string_of_int max_solutions ^ 

1045 
(if max_threads > 0 then 

1046 
" maxthreads " ^ string_of_int max_threads 

1047 
else 

1048 
"") ^ 

1049 
" < " ^ File.shell_path in_path ^ 

1050 
" > " ^ File.shell_path out_path ^ 

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

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

1054 
> apfst (map (apfst reindex)) > apsnd (map reindex) 
33192  1055 
val js = triv_js @ nontriv_js 
1056 
val first_error = 

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

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

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

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

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

1064 
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

1065 
> Substring.isEmpty > not 
33192  1066 
in 
1067 
if null ps then 

1068 
if code = 2 then 

1069 
TimedOut js 

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

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

1071 
Normal ([], js, first_error) 
38516
307669429dc1
gracefully handle the case where the JVM is too old in Nitpick
blanchet
parents:
38198
diff
changeset

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

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

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

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

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

1077 
KodkodiNotInstalled 
33192  1078 
else if first_error <> "" then 
35695  1079 
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

1080 
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

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

1082 
else 
33192  1083 
Error ("Unknown error", js) 
1084 
else 

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

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

1087 
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

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

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

1090 
val nontriv_js = 
38126  1091 
read_output_file new_kodkodi out_path 
1092 
> 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

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

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

1095 
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

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

1097 
(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

1098 
end 
33192  1099 
end 
1100 
end 

1101 

35814  1102 
val cached_outcome = 
1103 
Synchronized.var "Kodkod.cached_outcome" 

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

1105 

1106 
fun solve_any_problem overlord deadline max_threads max_solutions problems = 

1107 
let 

38189  1108 
fun do_solve () = 
1109 
uncached_solve_any_problem overlord deadline max_threads max_solutions 

1110 
problems 

35814  1111 
in 
1112 
if overlord then 

1113 
do_solve () 

1114 
else 

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

1116 
max1 = max2 andalso length ps1 = length ps2 andalso 

1117 
forall problems_equivalent (ps1 ~~ ps2)) 

1118 
(the_list (Synchronized.value cached_outcome)) 

1119 
(max_solutions, problems) of 

1120 
SOME outcome => outcome 

1121 
 NONE => 

1122 
let val outcome = do_solve () in 

1123 
(case outcome of 

39326  1124 
Normal (_, _, "") => 
35814  1125 
Synchronized.change cached_outcome 
1126 
(K (SOME ((max_solutions, problems), outcome))) 

1127 
 _ => ()); 

1128 
outcome 

1129 
end 

1130 
end 

1131 

33192  1132 
end; 