## cool / src / lib / genAndComp.ml @ 7c4d2eb4

History | View | Annotate | Download (68.2 KB)

1 |
(** Common functions and data structures which are shared |
---|---|

2 |
by the programs which generate (e.g. random) formulae |

3 |
and/or run tests or benchmarks on them. |

4 |
@author Florian Widmann |

5 |
*) |

6 | |

7 | |

8 |
(** Tests whether a string is "almost" empty. |

9 |
@param s A string. |

10 |
@return True iff the string is empty |

11 |
or contains only whitespaces. |

12 |
*) |

13 |
let isEmptyString s = |

14 |
let rec empty i = |

15 |
if i < 0 then true |

16 |
else |

17 |
let c = String.get s i in |

18 |
if c = ' ' || c = '\009' then empty (pred i) |

19 |
else false |

20 |
in |

21 |
empty (pred (String.length s)) |

22 | |

23 | |

24 |
(** This data type is used to return a result of a function invocation. |

25 |
It can either succeed, fail, or time out. |

26 |
*) |

27 |
type 'a resulttype = FINISHED of 'a | FAILED | TIMED_OUT |

28 | |

29 |
(** This exception is raised when the Unix signal "sigalrm" is received. |

30 |
It should not be used for anything else. |

31 |
*) |

32 |
exception Timeout |

33 | |

34 |
(** Evaluates a function on an argument |

35 |
but aborts the evaluation if it takes longer than a given timeout. |

36 |
If the timeout is less then infinity, |

37 |
it is required that the Unix signal "sigalrm" is handled and |

38 |
that the handler raises the exception Timeout. |

39 |
This can for example be achieved via the following code: |

40 |
let alarmHandler (n : int) = raise Timeout in |

41 |
let oldHandler = Sys.signal Sys.sigalrm (Sys.Signal_handle alarmHandler) in |

42 |
... // do something, e.g. invoke evaluate |

43 |
Sys.set_signal Sys.sigalrm oldHandler; |

44 |
@param f A function accepting v as an argument. |

45 |
The function must not raise the exception Timeout. |

46 |
@param v The argument for f. |

47 |
@param timeout The maximal time in seconds |

48 |
that the evaluation of f v is allowed to take. |

49 |
A non-positive number is interpreted as infinity. |

50 |
@return A triple (res, tm, 0) where: |

51 |
res = (FINISHED (f v)) iff f finished within timeout seconds; |

52 |
res = TIMED_OUT iff f does not finish within timeout seconds; and |

53 |
res = FAILED iff f raises an exception within timeout seconds. |

54 |
tm (<= timeout) is the time needed by f. |

55 |
The superflous 0 is a bogus value for the memory usage |

56 |
which is not measured by this function. |

57 |
PROBLEM: If f is a "busy" function, it may happen |

58 |
that the alarm handler is executed after this function, |

59 |
even when the evaluation of f v takes far longer than timeout seconds. |

60 |
In this case this function takes longer than timeout and |

61 |
the exception Timeout will be raised outside the scope of this function. |

62 |
*) |

63 |
let evaluateFkt f v timeout = |

64 |
let noto = timeout <= 0 in |

65 |
try |

66 |
if noto then () else ignore (Unix.alarm timeout); |

67 |
let start = Unix.gettimeofday () in |

68 |
let res = |

69 |
try |

70 |
FINISHED (f v) |

71 |
with Timeout -> assert (not noto); TIMED_OUT |

72 |
| e -> FAILED |

73 |
in |

74 |
let stop = Unix.gettimeofday () in |

75 |
if noto then () else ignore (Unix.alarm 0); |

76 |
let time = if res = TIMED_OUT then float timeout else stop -. start in |

77 |
(res, time, 0) |

78 |
with Timeout -> assert (not noto); (TIMED_OUT, float timeout, 0) |

79 | |

80 |
(** Evaluates a function with a boolean result on an argument in a child process |

81 |
but aborts the evaluation if it takes longer than a given timeout. |

82 |
If the timeout is less then infinity, |

83 |
it is required that the Unix signal "sigalrm" is handled and |

84 |
that the handler raises the exception Timeout (see function "evaluateFkt"). |

85 |
@param f A function accepting v as an argument and returning a boolean value. |

86 |
@param v The argument for f. |

87 |
@param timeout The maximal time in seconds |

88 |
that the evaluation of f v is allowed to take. |

89 |
A non-positive number is interpreted as infinity. |

90 |
@return A triple (res, tm, 0) where: |

91 |
res = (FINISHED (f v)) iff f finished within timeout seconds; |

92 |
res = TIMED_OUT iff f does not finish within timeout seconds; and |

93 |
res = FAILED iff f raises an exception within timeout seconds. |

94 |
tm (<= timeout) is the time needed by f. |

95 |
The superflous 0 is a bogus value for the memory usage |

96 |
which is not measured by this function. |

97 |
PROBLEM: Since the exit codes 0 and 1 are used to return the result, |

98 |
the child process must not fail with exit code 1 for other reasons. |

99 |
A more secure way to transmit the result would be to use a pipe. |

100 |
*) |

101 |
let evaluateFktProc f v timeout = |

102 |
let noto = timeout <= 0 in |

103 |
match Unix.fork () with |

104 |
| 0 -> |

105 |
let res = f v in |

106 |
if res then exit 0 else exit 1 |

107 |
| id -> |

108 |
try |

109 |
if noto then () else ignore (Unix.alarm timeout); |

110 |
let start = Unix.gettimeofday () in |

111 |
let status = snd (Unix.waitpid [] id) in |

112 |
let stop = Unix.gettimeofday () in |

113 |
if noto then () else ignore (Unix.alarm 0); |

114 |
let time = stop -. start in |

115 |
match status with |

116 |
| Unix.WEXITED n when n = 0 || n = 1 -> (FINISHED (n = 0), time, 0) |

117 |
| _ -> (FAILED, time, 0) |

118 |
with Timeout -> |

119 |
assert (not noto); |

120 |
let () = |

121 |
try |

122 |
Unix.kill id Sys.sigkill; |

123 |
ignore (Unix.waitpid [] id) |

124 |
with Unix.Unix_error _ -> () |

125 |
in |

126 |
(TIMED_OUT, float timeout, 0) |

127 | |

128 | |

129 |
(** Generates a list of atomic "formulae" |

130 |
that are assigned a priority. |

131 |
@param litlst A list of "literals" (e.g. True and False). |

132 |
They are assigned the priority 1. |

133 |
@param neg A function that negates a formula. |

134 |
@param prio The priority of the generated atomic "formulae". |

135 |
@param const A function that converts a string into an atomic "formula". |

136 |
@param name A prefix of the names of the generated atomic "formulae". |

137 |
@param nr The number of different atomic "formula". |

138 |
It is taken at least to be 1 (0 if litlst is non-empty). |

139 |
@return A list of pairs (f, p) where f is a formula and p a priority. |

140 |
*) |

141 |
let genLiterals ?litlst ?neg ?(prio = 1) const name nr = |

142 |
let rec genLit acc = function |

143 |
| 0 -> acc |

144 |
| n -> |

145 |
let n = pred n in |

146 |
let s = name ^ (string_of_int n) in |

147 |
let af = const s in |

148 |
let acc1 = (af, prio)::acc in |

149 |
let acc2 = |

150 |
match neg with |

151 |
| None -> acc1 |

152 |
| Some f -> (f af, prio)::acc1 |

153 |
in |

154 |
genLit acc2 n |

155 |
in |

156 |
let acc = |

157 |
match litlst with |

158 |
| None -> [] |

159 |
| Some l -> List.map (fun f -> (f, 1)) l |

160 |
in |

161 |
let nr = if acc = [] then max 1 nr else max 0 nr in |

162 |
genLit acc nr |

163 | |

164 | |

165 |
(** Sums up the priorities in a list. |

166 |
@param lst A list of pairs (f, n) where n is a priority. |

167 |
@return The sum of all priorities in lst. |

168 |
*) |

169 |
let addPrios lst = List.fold_left (fun s (_, n) -> s + n) 0 lst |

170 | |

171 |
(** Chooses the element in a list that corresponds to a value |

172 |
@param n An int value. |

173 |
@param lst A list of pairs (f, n) where n is a priority. |

174 |
@return The first element e in a list |

175 |
such that the sum of all priorities of elements up to e |

176 |
is greater than n. |

177 |
@raise Failure if there is no such element. |

178 |
*) |

179 |
let getConst n lst = |

180 |
let rec getC sum = function |

181 |
| [] -> raise (Failure "Should not happen. It's a bug.") |

182 |
| (f, p)::t -> |

183 |
let sum1 = sum + p in |

184 |
if n < sum1 then f |

185 |
else getC sum1 t |

186 |
in |

187 |
getC 0 lst |

188 | |

189 |
(** Chooses k distinct elements from a list. |

190 |
@param k The number of elements to be chosen. |

191 |
@param ls A list. |

192 |
@return A sublist of ls of length k. |

193 |
*) |

194 |
let rec chooseK k ls = |

195 |
let len = List.length ls in |

196 |
assert (k >= 0 && k <= len); |

197 |
if k = len then ls |

198 |
else |

199 |
let rand = Random.int len in |

200 |
let fld (acc, i) e = |

201 |
if i = rand then (acc, succ i) else (e::acc, succ i) |

202 |
in |

203 |
let (nls, _) = List.fold_left fld ([], 0) ls in |

204 |
chooseK k nls |

205 | |

206 |
(** Creates a formula (program) generator, i.e. a function which takes a size |

207 |
and produces a randomly generated formula (program) of that size. |

208 |
In the following, f stands for formula, p stands for program, |

209 |
and n stand for a priority which must be positive. |

210 |
@param lF A list of pairs (f, n), e.g. (p, 1). |

211 |
The list must not be empty. |

212 |
@param lFF A list of pairs (f->f, n), e.g. (~., 1). |

213 |
The list must not be empty. |

214 |
@param lFFF A list of pairs (f->f->f, n), e.g. (.&., 1). |

215 |
@param lPFF A list of pairs (p->f->f, n), e.g. (<.>., 1). |

216 |
@param lP A list of pairs (p, n), e.g. (a, 1). |

217 |
The list must not be empty unless lPFF is also empty. |

218 |
@param lPP A list of pairs (p->p, n), e.g. ( *., 1). |

219 |
@param lFP A list of pairs (f->p, n), e.g. (?., 1). |

220 |
@param lPPP A list of pairs (p->p->p, n), e.g. (.+., 1). |

221 |
@return A pair (fktF, fktP) where |

222 |
fktF is a function that randomly generates a formula of a given size, and |

223 |
fktP is a function that randomly generates a program of a given size. |

224 |
Both functions use the constructors lF, ..., lPPP. |

225 |
The size of the formula/program is the number of constructors. |

226 |
Note that each formula (program) in lF (lP) counts as one symbol, |

227 |
even when it is a complex formula (program). |

228 |
If lP is empty then fktP must not be invoked. |

229 |
If lP is not empty, but lPP and lFP are both empty, |

230 |
then fktP can only be invoked with size one. |

231 |
*) |

232 |
let mk_generator lF lFF lFFF lPFF lP lPP lFP lPPP = |

233 |
let simpleP = lPP = [] && lFP = [] in |

234 |
let rec genRF = function |

235 |
| n when n <= 0 -> raise (Failure "size of formula must be positive") |

236 |
| 1 -> |

237 |
let prios = addPrios lF in |

238 |
let rand = Random.int prios in |

239 |
getConst rand lF |

240 |
| n -> |

241 |
let prios1 = addPrios lFF in |

242 |
let prios2 = if n = 2 then 0 else addPrios lFFF in |

243 |
let prios3 = if n = 2 && not simpleP then 0 else addPrios lPFF in |

244 |
let rand = Random.int (prios1 + prios2 + prios3) in |

245 |
if rand < prios1 then |

246 |
let const = getConst rand lFF in |

247 |
let subf = genRF (pred n) in |

248 |
const subf |

249 |
else if rand < prios1 + prios2 then |

250 |
let const = getConst (rand-prios1) lFFF in |

251 |
let part = (Random.int (n - 2)) + 1 in |

252 |
let subf1 = genRF part in |

253 |
let subf2 = genRF (n-1-part) in |

254 |
const subf1 subf2 |

255 |
else |

256 |
let const = getConst (rand-prios1-prios2) lPFF in |

257 |
let part = if simpleP then 0 else (Random.int (n - 2)) + 1 in |

258 |
let subp1 = genRP (if simpleP then 1 else part) in |

259 |
let subf2 = genRF (n-1-part) in |

260 |
const subp1 subf2 |

261 |
and genRP = function |

262 |
| n when n <= 0 -> raise (Failure "size of formula must be positive") |

263 |
| 1 -> |

264 |
let prios = addPrios lP in |

265 |
let rand = Random.int prios in |

266 |
getConst rand lP |

267 |
| n -> |

268 |
let prios1 = addPrios lPP in |

269 |
let prios2 = addPrios lFP in |

270 |
let prios3 = if n = 2 then 0 else addPrios lPPP in |

271 |
let rand = Random.int (prios1 + prios2 + prios3) in |

272 |
if rand < prios1 then |

273 |
let const = getConst rand lPP in |

274 |
let subp = genRP (pred n) in |

275 |
const subp |

276 |
else if rand < prios1 + prios2 then |

277 |
let const = getConst (rand-prios1) lFP in |

278 |
let subf = genRF (pred n) in |

279 |
const subf |

280 |
else |

281 |
let const = getConst (rand-prios1-prios2) lPPP in |

282 |
let part = (Random.int (n - 2)) + 1 in |

283 |
let subp1 = genRP part in |

284 |
let subp2 = genRP (n-1-part) in |

285 |
const subp1 subp2 |

286 |
in |

287 |
(genRF, genRP) |

288 | |

289 |
(** Creates a formula (program) generator, i.e. a function which takes a depth |

290 |
and produces a randomly generated formula (program) with the given nesting depth. |

291 |
In the following, f stands for formula, p stands for program, |

292 |
and n stand for a priority which must be positive. |

293 |
@param lF A list of pairs (f, n), e.g. (p, 1). |

294 |
The list must not be empty. |

295 |
@param lFF A list of pairs (f->f, n), e.g. (~., 1). |

296 |
@param lFFF A list of pairs (f->f->f, n), e.g. (.&., 1). |

297 |
@param lPFF A list of pairs (p->f->f, n), e.g. (<.>., 1). |

298 |
At least one of lFF, lFFF, and lPFF must be non-empty. |

299 |
@param lP A list of pairs (p, n), e.g. (a, 1). |

300 |
The list must not be empty unless lPFF is also empty. |

301 |
@param lPP A list of pairs (p->p, n), e.g. ( *., 1). |

302 |
@param lFP A list of pairs (f->p, n), e.g. (?., 1). |

303 |
@param lPPP A list of pairs (p->p->p, n), e.g. (.+., 1). |

304 |
@return A pair (fktF, fktP) where |

305 |
fktF is a function that randomly generates a formula of a given depth, and |

306 |
fktP is a function that randomly generates a program of a given depth. |

307 |
Both functions use the constructors lF, ..., lPPP. |

308 |
Note that the size of the formula/program is not fixed. |

309 |
If lP is empty then fktP must not be invoked. |

310 |
If lP is not empty, but lPP, lFP, and LPPP are all empty, |

311 |
then fktP can only be invoked with depth naught. |

312 |
*) |

313 |
let mk_generatorDepth lF lFF lFFF lPFF lP lPP lFP lPPP = |

314 |
let simpleP = lPP = [] && lFP = [] && lPPP = [] in |

315 |
let rec genRF = function |

316 |
| n when n <= 0 -> |

317 |
let prios = addPrios lF in |

318 |
let rand = Random.int prios in |

319 |
getConst rand lF |

320 |
| n -> |

321 |
let prios1 = addPrios lFF in |

322 |
let prios2 = addPrios lFFF in |

323 |
let prios3 = addPrios lPFF in |

324 |
let rand = Random.int (prios1 + prios2 + prios3) in |

325 |
if rand < prios1 then |

326 |
let const = getConst rand lFF in |

327 |
let subf = genRF (pred n) in |

328 |
const subf |

329 |
else if rand < prios1 + prios2 then |

330 |
let const = getConst (rand-prios1) lFFF in |

331 |
let subf1 = genRF (pred n) in |

332 |
let subf2 = genRF (pred n) in |

333 |
const subf1 subf2 |

334 |
else |

335 |
let const = getConst (rand-prios1-prios2) lPFF in |

336 |
let subp1 = genRP (if simpleP then 0 else pred n) in |

337 |
let subf2 = genRF (pred n) in |

338 |
const subp1 subf2 |

339 |
and genRP = function |

340 |
| n when n <= 0 -> |

341 |
let prios = addPrios lP in |

342 |
let rand = Random.int prios in |

343 |
getConst rand lP |

344 |
| n -> |

345 |
let prios1 = addPrios lPP in |

346 |
let prios2 = addPrios lFP in |

347 |
let prios3 = addPrios lPPP in |

348 |
let rand = Random.int (prios1 + prios2 + prios3) in |

349 |
if rand < prios1 then |

350 |
let const = getConst rand lPP in |

351 |
let subp = genRP (pred n) in |

352 |
const subp |

353 |
else if rand < prios1 + prios2 then |

354 |
let const = getConst (rand-prios1) lFP in |

355 |
let subf = genRF (pred n) in |

356 |
const subf |

357 |
else |

358 |
let const = getConst (rand-prios1-prios2) lPPP in |

359 |
let subp1 = genRP (pred n) in |

360 |
let subp2 = genRP (pred n) in |

361 |
const subp1 subp2 |

362 |
in |

363 |
(genRF, genRP) |

364 | |

365 | |

366 |
(** Runs a list of solvers on a formula and records for each solver |

367 |
how long it took and whether it timed out or failed. |

368 |
If the solvers produce contradicting results, an error message is printed. |

369 |
@param ptime If a solver takes longer than ptime seconds for f |

370 |
then f and the name of the solver are printed. |

371 |
@param fail If fail is true and a solver fails on f |

372 |
then f and the name of the solver are printed. |

373 |
@param timeout A timeout in seconds for each solver. |

374 |
A non-positive number is interpreted as infinity. |

375 |
@param tos If the array tos is non-empty, it must have the same length as solvl. |

376 |
In this case, each prover is only invoked |

377 |
if the corresponding tos entry is false; |

378 |
otherwise the prover is assumed to have timed out of f. |

379 |
(without actually running the solver). |

380 |
Moreover, if a prover times out then tos is updated correspondingly. |

381 |
@param expF Converts the formulae into a string representation. |

382 |
@param solvers A list of solvers together with their names. |

383 |
Each solver is a function which accepts a formula and a timeout as input |

384 |
and returns a triple (res, tm, rss) where |

385 |
res is the result (of type resulttype) of the invocation; |

386 |
tm is the time needed by the solver; and |

387 |
rss is an approximation of the maximum amount of memory in kB |

388 |
which was used by the solver at some time during its runtime. |

389 |
Note: It is the responsibility of the functions in solvers to time out correctly. |

390 |
@param f A formulae. |

391 |
@return A tuple (res, tl) where: |

392 |
tl is a list containing the results of each solver for f (see above); and |

393 |
res is true iff at least one solver returned that f is satisfiable, |

394 |
false iff no solver returned satisfiable and at least one solver returned unsatisfiable, and |

395 |
undefined iff all solvers timed out or failed. |

396 |
*) |

397 |
let runSolvers ?ptime ?(fail=false) ?timeout ?(tos=[| |]) expF solvers f = |

398 |
let timeout = |

399 |
match timeout with |

400 |
| Some tout when tout > 0 -> tout |

401 |
| _ -> 0 |

402 |
in |

403 |
let runS (fstres, idx, acc) (solv, sname) = |

404 |
let ((res, tm, rss) as triple) = |

405 |
if Array.length tos > 0 && tos.(pred idx) then (TIMED_OUT, float_of_int timeout, 0) |

406 |
else solv f timeout |

407 |
in |

408 |
if Array.length tos > 0 && res = TIMED_OUT then tos.(pred idx) <- true else (); |

409 |
let nfstres = |

410 |
match res with |

411 |
| FAILED |

412 |
| TIMED_OUT -> fstres |

413 |
| FINISHED sat -> |

414 |
match fstres with |

415 |
| None -> Some sat |

416 |
| Some fsat -> |

417 |
let _ = |

418 |
if sat <> fsat then begin |

419 |
prerr_endline ("\nSolver \"" ^ sname ^ "\" returned different result for formula: "); |

420 |
prerr_endline (expF f); |

421 |
failwith "results do not match" |

422 |
end else () |

423 |
in |

424 |
fstres |

425 |
in |

426 |
let _ = |

427 |
match ptime with |

428 |
| Some pt when tm >= pt -> |

429 |
let s = " seconds " ^ (if res = TIMED_OUT then "(timed out) " else "") ^ "on formula: " in |

430 |
print_endline ("\nSolver \"" ^ sname ^ "\" took " ^ (string_of_float tm) ^ s); |

431 |
print_endline (expF f) |

432 |
| _ -> () |

433 |
in |

434 |
let _ = |

435 |
if fail && res = FAILED then begin |

436 |
print_endline ("\nSolver \"" ^ sname ^ "\" failed on formula: "); |

437 |
print_endline (expF f) |

438 |
end else () |

439 |
in |

440 |
(nfstres, succ idx, triple::acc) |

441 |
in |

442 |
let (resopt, _, tmsl) = List.fold_left runS (None, 1, []) solvers in |

443 |
(resopt, List.rev tmsl) |

444 | |

445 |
(** Runs a solver for different complexities of formulae. |

446 |
@param inter1 An optional function whose arguments are a complexity |

447 |
and a value of the same type as the result of this function. |

448 |
It is called after each complexity round and passed as argument |

449 |
the current complexity and the intermediate result of this function. |

450 |
@param inter2 An optional function whose arguments are a complexity, |

451 |
two integers, a formula, and a value of the same type as the result of solver. |

452 |
It is called after each invocation of solver and passed as argument |

453 |
the current complexity, the current index, the maximum index, |

454 |
the current input formula and the result of the prover. |

455 |
@param dots The number of dots in the progress bar for every complexity. |

456 |
@param genF A formula generator that takes a complexity as argument. |

457 |
@param comb A function combining the nr(k) individual results |

458 |
within each complexity k. |

459 |
@param init An initial value for comb. |

460 |
@param solver A solver which accepts a formula and produces a result. |

461 |
For example, it might be a function which invokes several "real" solvers. |

462 |
@param nr A function which determines for each complexity |

463 |
the number of formulae that is generated for that complexity. |

464 |
@param start The initial complexity. |

465 |
@param stop The final complexity. |

466 |
@param step A function that produces the next complexity |

467 |
when given the current one. |

468 |
@return A list of pairs (c, r) where c is the complexity |

469 |
and r is the (combined) result returned by the solver for c. |

470 |
*) |

471 |
let iterSolver ?inter1 ?inter2 ?dots genF comb init solver nr start stop step = |

472 |
let pcstep = |

473 |
match dots with |

474 |
| Some n when n > 0 -> 1. /. (float n) |

475 |
| _ -> 0. |

476 |
in |

477 |
let rec iterS2 compl pc i acc = |

478 |
let bnd = nr compl in |

479 |
if i <= bnd then |

480 |
let f = genF compl in |

481 |
let res = solver f in |

482 |
let _ = |

483 |
match inter2 with |

484 |
| None -> () |

485 |
| Some fkt -> fkt compl i bnd f res |

486 |
in |

487 |
let acc1 = comb res acc in |

488 |
let ratio = (float i) /. (float bnd) in |

489 |
let npc = |

490 |
if pc > 0. && ratio >= pc then begin |

491 |
print_string "."; flush stdout; |

492 |
pc +. pcstep; |

493 |
end |

494 |
else pc |

495 |
in |

496 |
iterS2 compl npc (succ i) acc1 |

497 |
else begin |

498 |
print_newline (); |

499 |
acc |

500 |
end |

501 |
in |

502 |
let rec iterS1 compl acc = |

503 |
if compl <= stop then begin |

504 |
print_endline (string_of_int compl); |

505 |
let res = iterS2 compl pcstep 1 init in |

506 |
let nacc = (compl, res)::acc in |

507 |
let _ = |

508 |
match inter1 with |

509 |
| None -> () |

510 |
| Some fkt -> fkt compl (List.rev nacc) |

511 |
in |

512 |
iterS1 (step compl) nacc |

513 |
end |

514 |
else List.rev acc |

515 |
in |

516 |
iterS1 start [] |

517 | |

518 |
(** Runs a list of solvers on formulae of different complexities |

519 |
and outputs some information (e.g. if solvers return different results). |

520 |
@param ko If set to true, a solver will not be invoked again |

521 |
after having timed out for the first time, |

522 |
but will be assumed to time out on all further formulae. |

523 |
The rest of the parameters is passed through to |

524 |
either "iterSolver" or "runSolvers". |

525 |
@return A list which contains for each complexity c a tuple (c, (ns, nu, nd, tl)) where: |

526 |
ns is the number of satisfiable formulae for complexity c; |

527 |
nu is the number of unsatisfiable formulae for complexity c; |

528 |
nd is the number of formulae whose status is unknown |

529 |
because no prover could solve them; and |

530 |
tl is a list which contains for each solver s a |

531 |
tuple (tS, toS, totS, fS, ftS, rssS, |

532 |
tU, toU, totU, fU, ftU, rssU, |

533 |
tN, toN, totN, fN, ftN, rssN) where: |

534 |
tS is the accumulated time needed by s to process all satisfiable formulae; |

535 |
toS is the number of satisfiable formulae on which s timed out; |

536 |
totS is the accumulated time of all satisfiable formulae on which s timed out; |

537 |
fS is the numbe of satisfiable formulae on which s failed; |

538 |
ftS is the accumulated time of all satisfiable formulae on which s failed; |

539 |
rssS is the accumulated approximate memory consumption needed by s |

540 |
to process all satisfiable formulae; |

541 |
similarly for unsatisfiable and unknown formulae. |

542 |
*) |

543 |
let enumSolvers ?inter1 ?inter2 ?dots ?ptime ?fail ?timeout ?(ko = false) expF |

544 |
genF solvers nr start stop step = |

545 |
let comb (resopt, tml) (accS, accU, accN, accT) = |

546 |
match resopt with |

547 |
| Some true -> |

548 |
let map2 (res, tm, rss) |

549 |
(tS, toS, totS, fS, ftS, rssS, tU, toU, totU, fU, ftU, rssU, tN, toN, totN, fN, ftN, rssN) = |

550 |
let tS1 = tm +. tS in |

551 |
let toS1 = if res = TIMED_OUT then succ toS else toS in |

552 |
let totS1 = if res = TIMED_OUT then tm +. totS else totS in |

553 |
let fS1 = if res = FAILED then succ fS else fS in |

554 |
let ftS1 = if res = FAILED then tm +. ftS else ftS in |

555 |
let rssS1 = rss + rssS in |

556 |
(tS1, toS1, totS1, fS1, ftS1, rssS1, tU, toU, totU, fU, ftU, rssU, tN, toN, totN, fN, ftN, rssN) |

557 |
in |

558 |
let accT1 = List.map2 map2 tml accT in |

559 |
(succ accS, accU, accN, accT1) |

560 |
| Some false -> |

561 |
let map2 (res, tm, rss) |

562 |
(tS, toS, totS, fS, ftS, rssS, tU, toU, totU, fU, ftU, rssU, tN, toN, totN, fN, ftN, rssN) = |

563 |
let tU1 = tm +. tU in |

564 |
let toU1 = if res = TIMED_OUT then succ toU else toU in |

565 |
let totU1 = if res = TIMED_OUT then tm +. totU else totU in |

566 |
let fU1 = if res = FAILED then succ fU else fU in |

567 |
let ftU1 = if res = FAILED then tm +. ftU else ftU in |

568 |
let rssU1 = rss + rssU in |

569 |
(tS, toS, totS, fS, ftS, rssS, tU1, toU1, totU1, fU1, ftU1, rssU1, tN, toN, totN, fN, ftN, rssN) |

570 |
in |

571 |
let accT1 = List.map2 map2 tml accT in |

572 |
(accS, succ accU, accN, accT1) |

573 |
| None -> |

574 |
let map2 (res, tm, rss) |

575 |
(tS, toS, totS, fS, ftS, rssS, tU, toU, totU, fU, ftU, rssU, tN, toN, totN, fN, ftN, rssN) = |

576 |
let tN1 = tm +. tN in |

577 |
let toN1 = if res = TIMED_OUT then succ toN else toN in |

578 |
let totN1 = if res = TIMED_OUT then tm +. totN else totN in |

579 |
let fN1 = if res = FAILED then succ fN else fN in |

580 |
let ftN1 = if res = FAILED then tm +. ftN else ftN in |

581 |
let rssN1 = rss + rssN in |

582 |
(tS, toS, totS, fS, ftS, rssS, tU, toU, totU, fU, ftU, rssU, tN1, toN1, totN1, fN1, ftN1, rssN1) |

583 |
in |

584 |
let accT1 = List.map2 map2 tml accT in |

585 |
(accS, accU, succ accN, accT1) |

586 |
in |

587 |
let init = |

588 |
(0, 0, 0, List.map (fun _ -> (0., 0, 0., 0, 0., 0, 0., 0, 0., 0, 0., 0, 0., 0, 0., 0, 0., 0)) solvers) |

589 |
in |

590 |
let tos = if ko then Array.make (List.length solvers) false else [| |] in |

591 |
let solver f = runSolvers ?ptime ?fail ?timeout ~tos expF solvers f in |

592 |
let alarmHandler (n : int) = raise Timeout in |

593 |
let oldHandler = Sys.signal Sys.sigalrm (Sys.Signal_handle alarmHandler) in |

594 |
let res = iterSolver ?inter1 ?inter2 ?dots genF comb init solver nr start stop step in |

595 |
Sys.set_signal Sys.sigalrm oldHandler; |

596 |
res |

597 | |

598 | |

599 |
(** Writes the result returned by "enumSolvers" into a file. |

600 |
@param filename The name of the output file. |

601 |
@param A result as returned by "enumSolvers". |

602 |
*) |

603 |
let outputRawData filename res = |

604 |
let file = open_out filename in |

605 |
let psi i = output_string file ((string_of_int i) ^ " ") in |

606 |
let psf f = output_string file ((string_of_float f) ^ " ") in |

607 |
let iter2 (tS, toS, totS, fS, ftS, rssS, tU, toU, totU, fU, ftU, rssU, tN, toN, totN, fN, ftN, rssN) = |

608 |
psf tS; |

609 |
psi toS; |

610 |
psf totS; |

611 |
psi fS; |

612 |
psf ftS; |

613 |
psi rssS; |

614 |
psf tU; |

615 |
psi toU; |

616 |
psf totU; |

617 |
psi fU; |

618 |
psf ftU; |

619 |
psi rssU; |

620 |
psf tN; |

621 |
psi toN; |

622 |
psf totN; |

623 |
psi fN; |

624 |
psf ftN; |

625 |
psi rssN; |

626 |
in |

627 |
let iter1 (comp, (noS, noU, noN, tml)) = |

628 |
psi comp; |

629 |
psi (noS + noU + noN); |

630 |
psi noS; |

631 |
psi noU ; |

632 |
psi noN ; |

633 |
List.iter iter2 tml; |

634 |
output_string file "\n" |

635 |
in |

636 |
List.iter iter1 res; |

637 |
close_out file |

638 | |

639 |
(** Runs a list of solvers for formulae of different complexities |

640 |
and writes the results into a file. |

641 |
Additionally it creates a gnuplot sample file |

642 |
which outputs (parts of) the results as a graph. |

643 |
@param filenameG The filename of the GnuPlot file. |

644 |
@param filenameD The filename of the file |

645 |
which will store the results (and which is used by filenameG). |

646 |
@param basenameF If provided then all input formulae for the provers |

647 |
will be written into files. There will be one file per complexity n |

648 |
named <basenameF>_n.txt and it will contain all formulae of complexity n. |

649 |
@param nr The number of formula that is generated for each complexity. |

650 |
The rest of the parameters is passed through to "enumSolvers". |

651 |
*) |

652 |
let toGnuPlot ?(filenameG = "plot") ?(filenameD = "data.dat") ?basenameF |

653 |
?dots ?ptime ?fail ?timeout ?ko expF genF solvers nr start stop step = |

654 |
let outputPlot () = |

655 |
let file = open_out filenameG in |

656 |
let ps s = output_string file s in |

657 |
let psl s = output_string file (s ^ "\n") in |

658 |
let fldG mul n (_, lab) = |

659 |
let s6 = string_of_int (n*mul + 6) in |

660 |
let s12 = string_of_int (n*mul + 12) in |

661 |
let s18 = string_of_int (n*mul + 18) in |

662 |
let str = "datafile using 1:(($" ^ s6 ^ "+$" ^ s12 ^ "+$" ^ s18 ^ ")/($3+$4+$5))" ^ |

663 |
" with linespoints title \"" ^ lab ^ " (time)\",\\\n " |

664 |
in |

665 |
ps str; |

666 |
succ n |

667 |
in |

668 |
psl ("datafile = \"" ^ filenameD ^ "\""); |

669 |
psl "#outfile = \"blah\""; |

670 |
psl "#set output outfile"; |

671 |
psl "#set terminal postscript eps # size 5,3.5"; |

672 |
psl "set key top left"; |

673 |
psl "set xlabel \"Size of formulae\""; |

674 |
psl "set xtics nomirror"; |

675 |
psl "set ylabel \"time per formula in seconds\""; |

676 |
psl "#set logscale y"; |

677 |
psl "set ytics nomirror"; |

678 |
psl "set y2label \"percentage of known satisfiable formulae\""; |

679 |
psl "set y2range [0:100]"; |

680 |
psl "set y2tics nomirror"; |

681 |
ps "plot "; |

682 |
let _ = List.fold_left (fldG 18) 0 solvers in |

683 |
let str = "datafile using 1:(100*$3/$2)" ^ |

684 |
" axes x1y2 with linespoints title \"known satisfiable formulae\"" |

685 |
in |

686 |
psl str; |

687 |
psl "pause -1"; |

688 |
close_out file |

689 |
in |

690 |
let inter1 _ res = |

691 |
let filename = filenameD ^ ".tmp" in |

692 |
outputRawData filename res |

693 |
in |

694 |
let inter2 c n bnd f _ = |

695 |
match basenameF with |

696 |
| None -> () |

697 |
| Some bn -> |

698 |
let fn = bn ^ "_" ^ (string_of_int c) ^ ".txt" in |

699 |
let file = |

700 |
if n = 1 then open_out fn else open_out_gen [Open_append; Open_text] 0o666 fn |

701 |
in |

702 |
output_string file (expF f); |

703 |
output_string file "\n\n"; |

704 |
close_out file; |

705 |
in |

706 |
outputPlot (); |

707 |
let fnr _ = nr in |

708 |
let res = |

709 |
enumSolvers ~inter1 ~inter2 ?dots ?ptime ?fail ?timeout ?ko expF genF solvers fnr start stop step |

710 |
in |

711 |
outputRawData filenameD res |

712 | |

713 |
(** Runs a list of solvers for a benchmark, that is a list of formulae |

714 |
and writes the results into a file. |

715 |
Additionally it creates a GnuPlot script with corresponding data file |

716 |
which show the number of formulae solved by each solver |

717 |
for different timeouts (the timeout is per formula). |

718 |
It also creates a Latex file containing a table |

719 |
which shows for each solver and each group of formulae (see below) |

720 |
the number of problems solved (with the maximal timeout) |

721 |
as well as the average time needed for all formulae which could be solved. |

722 |
@param filenameL The filename of the Latex file. |

723 |
@param filenameG The filename of the GnuPlot file. |

724 |
@param filenameD The filename of the file |

725 |
which will store the results. |

726 |
@param basenameF If provided then all benchmark formulae |

727 |
will be written into files. There will be one file per benchmark |

728 |
named <basenameF>_n.txt where n is the position of the formula in benchmarks. |

729 |
@param timeouts A non-empty list of timeouts, that is a list of ints. |

730 |
The values should be increasing. |

731 |
The timeouts are for each individual formula. |

732 |
@param benchmarks A list of functions with unit argument |

733 |
which each produce a formula. |

734 |
This saves memory if the formulae are very big. |

735 |
@param labels A list of integer-string pairs |

736 |
which groups the benchmark formulae. |

737 |
Each pair (n, l) represents one group named l |

738 |
which consists of n formulae in the benchmark. |

739 |
The actual formulae are determined by the order of the list |

740 |
in the obvious way. The labels should exactly cover the benchmarks. |

741 |
The rest of the parameters is passed through to "enumSolvers". |

742 |
*) |

743 |
let outputBenchmarks ?(filenameL = "out.tex") ?(filenameG = "plot") ?(filenameD = "data.dat") |

744 |
?basenameF ?ptime ?fail expF solvers timeouts benchmarks labels = |

745 |
assert (timeouts <> []); |

746 |
let timeout = List.nth timeouts (pred (List.length timeouts)) in |

747 |
let outputPlot () = |

748 |
let file = open_out filenameG in |

749 |
let ps s = output_string file s in |

750 |
let psl s = output_string file (s ^ "\n") in |

751 |
let fldLab i t = |

752 |
ps ("\"" ^ (string_of_int t) ^ "\" " ^ (string_of_int i)); |

753 |
if i < List.length timeouts then ps (", ") else psl (")"); |

754 |
succ i |

755 |
in |

756 |
let fldSolv n (_, lab) = |

757 |
let idx = string_of_int (succ n) in |

758 |
let str = |

759 |
"datafile using 1:"^ idx ^ " with linespoints title \"" ^ lab ^ "\"" |

760 |
in |

761 |
if n < List.length solvers then ps (str ^ ",\\\n ") else psl str; |

762 |
succ n |

763 |
in |

764 |
psl "#set terminal postscript eps # size 5,3.5"; |

765 |
psl ("datafile = \"" ^ filenameG ^ ".dat\""); |

766 |
psl "set key bottom right"; |

767 |
psl "set xlabel \"timeout per formula in seconds\""; |

768 |
psl "set ylabel \"number of problems solved\""; |

769 |
ps "set xtics ("; |

770 |
let _ = List.fold_left fldLab 1 timeouts in |

771 |
ps "plot "; |

772 |
let _ = List.fold_left fldSolv 1 solvers in |

773 |
psl "pause -1"; |

774 |
close_out file |

775 |
in |

776 |
let outputData filename resGnuPlot = |

777 |
let file = open_out filename in |

778 |
let fldD i rl = |

779 |
output_string file (string_of_int i); |

780 |
List.iter (fun n -> output_string file (" " ^ (string_of_int n))) rl; |

781 |
output_string file "\n"; |

782 |
succ i |

783 |
in |

784 |
let _ = List.fold_left fldD 1 resGnuPlot in |

785 |
close_out file |

786 |
in |

787 |
let outputLatex filename resLatex = |

788 |
let round f = |

789 |
let cs = int_of_float (100. *. f) in |

790 |
let ts = cs / 10 + (if cs mod 10 >= 5 then 1 else 0) in |

791 |
(string_of_int (ts / 10)) ^ "." ^ (string_of_int (ts mod 10)) |

792 |
in |

793 |
let file = open_out filename in |

794 |
let ps s = output_string file s in |

795 |
let psl s = output_string file (s ^ "\n") in |

796 |
let fldNames idx (_, lab) = |

797 |
if idx < List.length solvers then ps (" & \\multicolumn{2}{|c|}{" ^ lab ^"}") |

798 |
else ps (" & \\multicolumn{2}{|c||}{" ^ lab ^"}"); |

799 |
succ idx |

800 |
in |

801 |
let iterLines (pcs, pcu, pcd, lines, lab) = |

802 |
let iterL (no, avr) = |

803 |
let str = if avr < 0. then "--" else round avr in |

804 |
ps (" & " ^ (string_of_int no) ^ " & " ^ str) |

805 |
in |

806 |
ps lab; |

807 |
List.iter iterL lines; |

808 |
psl (" & " ^ (round pcs) ^ " & " ^ (round pcu) ^ " & " ^ (round pcd) ^ "\\\\") |

809 |
in |

810 |
psl "\\documentclass{article}"; |

811 |
psl "\\usepackage{arydshln}"; |

812 |
psl "\\begin{document}\n"; |

813 |
psl "\\begin{table}"; |

814 |
psl "\\centering"; |

815 |
ps ("\\begin{tabular}{|l||"); |

816 |
List.iter (fun _ -> ps "r;{.4pt/1pt}r|") solvers; |

817 |
psl "|c|c|c|}\n\\hline"; |

818 |
let _ = List.fold_left fldNames 1 solvers in |

819 |
psl "& sat & unsat & unk\\\\\n\\hline"; |

820 |
List.iter iterLines resLatex; |

821 |
psl "\\hline"; |

822 |
psl "\\end{tabular}"; |

823 |
psl "\\end{table}\n"; |

824 |
psl "\\end{document}"; |

825 |
close_out file |

826 |
in |

827 |
let convertToGnuPlot res t = |

828 |
let ft = (float) t in |

829 |
let init = List.map (fun _ -> 0) solvers in |

830 |
let fldT acc (_, (ns, nu, nd, sl)) = |

831 |
let map2T n (ts, _, _, fs, _, _, tu, _, _, fu, _, _, td, _, _, fd, _, _) = |

832 |
let t = |

833 |
if ns = 1 then ts else if nu = 1 then tu else if nd = 1 then td else (assert false) |

834 |
in |

835 |
if t < ft & (fs+fu+fd) = 0 then succ n else n |

836 |
in |

837 |
List.map2 map2T acc sl |

838 |
in |

839 |
List.fold_left fldT init res |

840 |
in |

841 |
let convertToLatex res = |

842 |
let initTpl = List.map (fun _ -> (0, 0.)) solvers in |

843 |
let fldTab ((cns, cnu, cnd, ctpl, rtpls, cnt, labs) as acc) (idx, (ns, nu, nd, sl)) = |

844 |
let (cns1, cnu1, cnd1, ctpl1, rtpls1, cnt1, labs1) = |

845 |
if labs <> [] && idx >= cnt + fst (List.hd labs) then |

846 |
let rtpl = |

847 |
let mapTpl (no, tm) = |

848 |
if no = 0 then (no, (-1.)) else (no, tm /. (float no)) |

849 |
(* if no = 0 then (no, (-1.)) else (no, tm) *) |

850 |
in |

851 |
List.map mapTpl ctpl |

852 |
in |

853 |
let lab = snd (List.hd labs) in |

854 |
let no = float (cns + cnu + cnd) in |

855 |
let cps = (float (100 * cns)) /. no in |

856 |
let cpu = (float (100 * cnu)) /. no in |

857 |
let cpd = (float (100 * cnd)) /. no in |

858 |
let bigt = (cps, cpu, cpd, rtpl, lab) in |

859 |
(0, 0, 0, initTpl, bigt::rtpls, cnt + fst (List.hd labs), List.tl labs) |

860 |
else acc |

861 |
in |

862 |
let map2Tpl (no, tm) (ts, tos, tots, fs, fts, _, tu, tou, totu, fu, ftu, _, _, _, _, _, _, _) = |

863 |
let no1 = no + ns + nu - tos - fs - tou - fu in |

864 |
let tm1 = tm +. ts +. tu -. tots -. fts -. totu -. ftu in |

865 |
(no1, tm1) |

866 |
in |

867 |
let ctpl2 = List.map2 map2Tpl ctpl1 sl in |

868 |
let cns2 = cns1 + ns in |

869 |
let cnu2 = cnu1 + nu in |

870 |
let cnd2 = cnd1 + nd in |

871 |
(cns2, cnu2, cnd2, ctpl2, rtpls1, cnt1, labs1) |

872 |
in |

873 |
let (lns, lnu, lnd, lastTpl, rtpls, _, labs) = |

874 |
List.fold_left fldTab (0, 0, 0, initTpl, [], 0, labels) res |

875 |
in |

876 |
let rtpl = |

877 |
let mapTpl (no, tm) = |

878 |
if no = 0 then (no, (-1.)) else (no, tm /. (float no)) |

879 |
(* if no = 0 then (no, (-1.)) else (no, tm) *) |

880 |
in |

881 |
List.map mapTpl lastTpl |

882 |
in |

883 |
let lab = if labs = [] then "" else snd (List.hd labs) in |

884 |
let no = float (lns + lnu + lnd) in |

885 |
let lps = (float (100 * lns)) /. no in |

886 |
let lpu = (float (100 * lnu)) /. no in |

887 |
let lpd = (float (100 * lnd)) /. no in |

888 |
List.rev ((lps, lpu, lpd, rtpl, lab)::rtpls) |

889 |
in |

890 |
let inter1 _ res = |

891 |
let filename = filenameD ^ ".tmp" in |

892 |
outputRawData filename res |

893 |
in |

894 |
let inter2 c _ _ f _ = |

895 |
match basenameF with |

896 |
| None -> () |

897 |
| Some bn -> |

898 |
let fn = bn ^ "_" ^ (string_of_int c) ^ ".txt" in |

899 |
let file = open_out fn in |

900 |
output_string file (expF f); |

901 |
output_string file "\n"; |

902 |
close_out file; |

903 |
in |

904 |
outputPlot (); |

905 |
let genF n = (List.nth benchmarks n) () in |

906 |
let stop = pred (List.length benchmarks) in |

907 |
let fnr _ = 1 in |

908 |
let res = |

909 |
enumSolvers ~inter1 ~inter2 ?ptime ?fail ~timeout expF genF solvers fnr 0 stop succ |

910 |
in |

911 |
let resGnuPlot = List.map (convertToGnuPlot res) timeouts in |

912 |
outputData (filenameG ^ ".dat") resGnuPlot; |

913 |
let resLatex = convertToLatex res in |

914 |
outputLatex filenameL resLatex; |

915 |
outputRawData filenameD res |

916 | |

917 | |

918 |
(** Executes an external solver in a child process |

919 |
but aborts the execution if it takes longer than a given timeout. |

920 |
If the timeout is less then infinity, |

921 |
it is required that the Unix signal "sigalrm" is handled and |

922 |
that the handler raises the exception Timeout (see function "evaluateFkt"). |

923 |
@param memtime The sampling interval in seconds |

924 |
for approximating the maximum amount of memory in kB |

925 |
which was used by the external solver at some time during its runtime. |

926 |
If the value is undefined or not positive, the memory usage is not determined. |

927 |
@param inpopt Some optional input |

928 |
which is passed to the external solver on the standard input. |

929 |
@param cmd The program name of the external solver. |

930 |
@param args Arguments for the external solver. |

931 |
@param isSat A regular expression which appears in the output of the external solver |

932 |
iff the input formula is satisfiable. |

933 |
More precisely, isSat has to match a substring of one of the output lines. |

934 |
@param timeout The maximal time in seconds |

935 |
that the external solver is allowed to take. |

936 |
A non-positive number is interpreted as infinity. |

937 |
@return A triple (res, tm, rss) where: |

938 |
res = (FINISHED sat) iff the prover finished within timeout seconds and |

939 |
without returning an error; in this case res is true iff |

940 |
isSat appears in the output of the external solver. |

941 |
res = TIMED_OUT iff the prover did not finish within timeout seconds. |

942 |
res = FAILED iff the prover finished within timeout seconds but returned an error. |

943 |
tm (<= timeout) is the time needed by the external solver. |

944 |
rss is an approximation of the maximum amount of memory in kB |

945 |
which was used by the external solver at some time during its runtime. |

946 |
If the memory usage is not sampled then 0 is returned. |

947 |
Note that res may be incorrect if something goes wrong while invoking the external solver |

948 |
and this function does not notice it. |

949 |
*) |

950 |
let callExt ?memtime inpopt cmd args isSat timeout = |

951 |
let noto = timeout <= 0 in |

952 |
let (mmem, mtime) = |

953 |
match memtime with |

954 |
| Some n when n > 0 -> (true, n) |

955 |
| _ -> (false, 0) |

956 |
in |

957 |
let res = ref false in |

958 |
let argsA = Array.of_list (cmd :: args) in |

959 |
let (in_read, in_write) = Unix.pipe () in |

960 |
let (out_read, out_write) = Unix.pipe () in |

961 |
Unix.set_close_on_exec in_read; |

962 |
Unix.set_close_on_exec out_write; |

963 |
match Unix.fork () with |

964 |
| 0 -> begin |

965 |
Unix.dup2 in_write Unix.stdout; |

966 |
Unix.dup2 in_write Unix.stderr; |

967 |
Unix.close in_write; |

968 |
Unix.dup2 out_read Unix.stdin; |

969 |
Unix.close out_read; |

970 |
try |

971 |
Unix.execv cmd argsA |

972 |
with _ -> |

973 |
prerr_endline "function \"callExt\": external solver not found"; |

974 |
exit 127 |

975 |
end |

976 |
| id1 -> |

977 |
Unix.close in_write; |

978 |
Unix.close out_read; |

979 |
match Unix.fork () with |

980 |
| 0 -> |

981 |
Unix.close in_read; |

982 |
let _ = |

983 |
match inpopt with |

984 |
| None -> Unix.close out_write |

985 |
| Some inp -> |

986 |
let outchan = Unix.out_channel_of_descr out_write in |

987 |
output_string outchan inp; |

988 |
close_out outchan |

989 |
in |

990 |
exit 0 |

991 |
| id2 -> |

992 |
Unix.close out_write; |

993 |
let (mem_read, mem_write) = if mmem then Unix.pipe () else (Unix.stdin, Unix.stdout) in |

994 |
match Unix.fork () with |

995 |
| 0 -> |

996 |
if not mmem then exit 0 |

997 |
else begin |

998 |
Unix.close mem_read; |

999 |
let rss = ref 0 in |

1000 |
let filename = "/proc/" ^ (string_of_int id1) ^ "/status" in |

1001 |
let reg = Str.regexp "VmRSS:\t *\\([0-9]+\\) kB" in |

1002 |
let _ = |

1003 |
try |

1004 |
while true do |

1005 |
let file = open_in filename in |

1006 |
try |

1007 |
while true do |

1008 |
let line = input_line file in |

1009 |
if Str.string_match reg line 0 then |

1010 |
let nrss = int_of_string (Str.matched_group 1 line) in |

1011 |
if nrss > !rss then rss := nrss else () |

1012 |
else () |

1013 |
done |

1014 |
with End_of_file -> |

1015 |
close_in file; |

1016 |
Unix.sleep mtime |

1017 |
done |

1018 |
with Sys_error _ -> () |

1019 |
in |

1020 |
let memchan = Unix.out_channel_of_descr mem_write in |

1021 |
output_string memchan (string_of_int !rss); |

1022 |
close_out memchan; |

1023 |
exit 0 |

1024 |
end |

1025 |
| id3 -> |

1026 |
if mmem then Unix.close mem_write else (); |

1027 |
let inchan = Unix.in_channel_of_descr in_read in |

1028 |
try |

1029 |
if noto then () else ignore (Unix.alarm timeout); |

1030 |
let start = Unix.gettimeofday () in |

1031 |
let () = |

1032 |
try |

1033 |
while true do |

1034 |
let line = input_line inchan in |

1035 |
if !res then () |

1036 |
else |

1037 |
try |

1038 |
let _ = Str.search_forward isSat line 0 in |

1039 |
res := true |

1040 |
with Not_found -> () |

1041 |
done |

1042 |
with End_of_file -> () |

1043 |
in |

1044 |
let stop = Unix.gettimeofday () in |

1045 |
if noto then () else ignore (Unix.alarm 0); |

1046 |
ignore (Unix.waitpid [] id2); |

1047 |
let status = snd (Unix.waitpid [] id1) in |

1048 |
let rss = |

1049 |
if mmem then |

1050 |
let memchan = Unix.in_channel_of_descr mem_read in |

1051 |
let rss = int_of_string (input_line memchan) in |

1052 |
close_in memchan; |

1053 |
rss |

1054 |
else 0 |

1055 |
in |

1056 |
ignore (Unix.waitpid [] id3); |

1057 |
close_in inchan; |

1058 |
let time = stop -. start in |

1059 |
match status with |

1060 |
| Unix.WEXITED 0 -> (FINISHED !res, time, rss) |

1061 |
| _ -> (FAILED, time, rss) |

1062 |
with Timeout -> |

1063 |
assert (not noto); |

1064 |
Unix.kill id1 Sys.sigkill; |

1065 |
ignore (Unix.waitpid [] id1); |

1066 |
Unix.kill id2 Sys.sigkill; |

1067 |
ignore (Unix.waitpid [] id2); |

1068 |
let rss = |

1069 |
if mmem then |

1070 |
let memchan = Unix.in_channel_of_descr mem_read in |

1071 |
let rss = int_of_string (input_line memchan) in |

1072 |
close_in memchan; |

1073 |
rss |

1074 |
else 0 |

1075 |
in |

1076 |
ignore (Unix.waitpid [] id3); |

1077 |
let () = |

1078 |
try |

1079 |
Unix.close in_read; |

1080 |
with Unix.Unix_error _ -> () |

1081 |
in |

1082 |
(TIMED_OUT, float timeout, rss) |

1083 | |

1084 | |

1085 |
(** Constructs a given number of elements |

1086 |
and combines the result. |

1087 |
@param op A binary function that combines |

1088 |
the constructed elements. It should be associative. |

1089 |
@param unit If zero elements are to be constructed |

1090 |
then unit is returned. |

1091 |
@param fkt This function constructs the elements. |

1092 |
It accepts an integer as argument. |

1093 |
@param n The number of elements that are to be constructed. |

1094 |
@return If n <= 0 then unit, |

1095 |
if n = 1 then f 0, |

1096 |
else op (f 0) (op (f 1) (...)) |

1097 |
*) |

1098 |
let const_bigOp op unit fkt n = |

1099 |
let rec intern_const i = |

1100 |
let fi = fkt i in |

1101 |
if i < pred n then |

1102 |
let rest = intern_const (succ i) in |

1103 |
op fi rest |

1104 |
else fi |

1105 |
in |

1106 |
if n <= 0 then unit else intern_const 0 |

1107 | |

1108 |
(** Combines the elements of a list. |

1109 |
@param op A binary function that combines the elements of fl. |

1110 |
It should be associative. |

1111 |
@param unit If fl is the empty list then unit is returned. |

1112 |
@param fl The list of elements. |

1113 |
@return If fl = [] then unit, |

1114 |
if fl = [f] then f, |

1115 |
if fl = [f0; ...; fn] then op f0 (op f1 (...)) |

1116 |
*) |

1117 |
let rec const_bigOpL op unit fl = |

1118 |
match fl with |

1119 |
| [] -> unit |

1120 |
| f::tl -> |

1121 |
if tl = [] then f |

1122 |
else |

1123 |
let rest = const_bigOpL op unit tl in |

1124 |
op f rest |

1125 | |

1126 |
(** Creates a list of ints in increasing order. |

1127 |
@param n The size of the list |

1128 |
@return A list of the form [0; 1; ...; n-1]. |

1129 |
*) |

1130 |
let mk_int_list n = |

1131 |
let rec mk_lst acc = function |

1132 |
| n when n <= 0 -> acc |

1133 |
| n -> |

1134 |
let pn = pred n in |

1135 |
mk_lst (pn::acc) pn |

1136 |
in |

1137 |
mk_lst [] n |

1138 | |

1139 | |

1140 |
(** A record which provides all logical operations needed |

1141 |
to generate the formulae below. |

1142 |
It might, for example, be instantiated with constructors or |

1143 |
string producing functions. |

1144 |
*) |

1145 |
type ('a, 'b) logicFkts = { |

1146 |
l_tt : 'a; |

1147 |
l_ff : 'a; |

1148 |
l_ap : string -> int -> 'a; |

1149 |
l_not : 'a -> 'a; |

1150 |
l_and : 'a -> 'a -> 'a; |

1151 |
l_or : 'a -> 'a -> 'a; |

1152 |
l_imp : 'a -> 'a -> 'a; |

1153 |
l_aa : string -> int -> 'b; |

1154 |
l_box : 'b -> 'a -> 'a; |

1155 |
l_dia : 'b -> 'a -> 'a; |

1156 |
l_aw : 'b list -> 'a -> 'a; |

1157 |
l_ev : 'b list -> 'a -> 'a; |

1158 |
l_until: 'a -> 'a -> 'a; |

1159 |
} |

1160 | |

1161 |
(** An example of an instantiation |

1162 |
which produces strings representing PDL formulae. |

1163 |
*) |

1164 |
let exampleF = { |

1165 |
l_tt = "True"; |

1166 |
l_ff = "False"; |

1167 |
l_ap = (fun s i -> s ^ (string_of_int i)); |

1168 |
l_not = (fun f1 -> "~" ^ f1); |

1169 |
l_and = (fun f1 f2 -> "(" ^ f1 ^ " & " ^ f2 ^ ")"); |

1170 |
l_or = (fun f1 f2 -> "(" ^ f1 ^ " | " ^ f2 ^ ")"); |

1171 |
l_imp = (fun f1 f2 -> "(" ^ f1 ^ " => " ^ f2 ^ ")"); |

1172 |
l_aa = (fun s i -> s ^ (string_of_int i)); |

1173 |
l_box = (fun a f1 -> "[" ^ a ^ "]" ^ f1); |

1174 |
l_dia = (fun a f1 -> "<" ^ a ^ ">" ^ f1); |

1175 |
l_aw = (fun al f1 -> "[*(" ^ (List.hd al) ^ (List.fold_left (fun a s -> a ^ "+" ^ s) "" (List.tl al)) ^ ")]" ^ f1); |

1176 |
l_ev = (fun al f1 -> "<*(" ^ (List.hd al) ^ (List.fold_left (fun a s -> a ^ "+" ^ s) "" (List.tl al)) ^ ")>" ^ f1); |

1177 |
l_until = (fun f1 f2 -> failwith "Until not implemented") |

1178 |
} |

1179 | |

1180 |
(** Generates a formula which forces a binary counter, |

1181 |
represented by some propositional variables, |

1182 |
to increase by one (modulo the bitlength) in all successor states. |

1183 |
@param f All the logical operations needed. |

1184 |
@param a The program which links to the successor states. |

1185 |
@param p A prefix for the propositional variables. |

1186 |
@param bs The bitsize of the counter. |

1187 |
@return A formula f which forces the counter |

1188 |
represented by the propositional variables p^"0", ..., p^(bs-1) |

1189 |
to increase by one (modulo 2^bs) in all successor states |

1190 |
which are related via a. |

1191 |
If there are no such successor states then f is trivially true. |

1192 |
The size of f is quadratic in bs. |

1193 |
*) |

1194 |
let mk_counter f a p bs = |

1195 |
let l_np p j = f.l_not (f.l_ap p j) in |

1196 |
let fkt i = |

1197 |
let f1 = |

1198 |
let fkt1 j = f.l_and (f.l_ap p j) (f.l_box a (l_np p j)) in |

1199 |
const_bigOp f.l_and f.l_tt fkt1 i |

1200 |
in |

1201 |
let f2 = if i < bs then f.l_and (l_np p i) (f.l_box a (f.l_ap p i)) else f.l_tt in |

1202 |
let f3 = |

1203 |
let fkt3 j = |

1204 |
let pj = f.l_ap p (i+1+j) in |

1205 |
let npj = l_np p (i+1+j) in |

1206 |
f.l_and (f.l_imp pj (f.l_box a pj)) (f.l_imp npj (f.l_box a npj)) |

1207 |
in |

1208 |
const_bigOp f.l_and f.l_tt fkt3 (bs-1-i) |

1209 |
in |

1210 |
const_bigOpL f.l_and f.l_tt [f1; f2; f3] |

1211 |
in |

1212 |
const_bigOp f.l_or f.l_ff fkt (succ bs) |

1213 | |

1214 |
(** Generates a formula so that every model which makes it true |

1215 |
has a path of exponential length in the size of the formula. |

1216 |
@param f All the logical operations needed. |

1217 |
@param n A measure of the size which must be positive. |

1218 |
@param unsat If unsat is true then the generated formula will be unsatisfiable. |

1219 |
Of course, the model description does not make sense in this case, |

1220 |
but the tableau procedure still has to build an exponential branch, |

1221 |
before it can detect unsatisfiability. |

1222 |
@return A formula f such that every model which makes f true |

1223 |
has a path of length 2^n. |

1224 |
The size of f is quadratic in n. |

1225 |
*) |

1226 |
let mk_exptime_tbox f n unsat = |

1227 |
let p = "p" in |

1228 |
let a = f.l_aa "a" 0 in |

1229 |
let l_np p j = f.l_not (f.l_ap p j) in |

1230 |
let f0 = const_bigOp f.l_and f.l_tt (l_np p) n in |

1231 |
let f1 = f.l_dia a f.l_tt in |

1232 |
let f2 = mk_counter f a p n in |

1233 |
let f3 = const_bigOp f.l_or f.l_ff (l_np p) n in |

1234 |
let tbox = if unsat then [f1; f2; f3] else [f1; f2] in |

1235 |
(f0, tbox) |

1236 | |

1237 |
let mk_exptime f n unsat = |

1238 |
let (f0, tbox) = mk_exptime_tbox f n unsat in |

1239 |
let ftbox = const_bigOpL f.l_and f.l_tt tbox in |

1240 |
let a = f.l_aa "a" 0 in |

1241 |
let ck = f.l_aw [a] ftbox in |

1242 |
f.l_and f0 ck |

1243 | |

1244 |
(** Generates a formula that captures the fact |

1245 |
that each person sees all the other persons |

1246 |
(but not necessarily herself). |

1247 |
@param f All the logical operations needed. |

1248 |
@param a A prefix for the roles/programs. |

1249 |
@param p A prefix for the propositional variables. |

1250 |
@param n The number of people involved. |

1251 |
@return A formula f which says that |

1252 |
any person can see whether a property, encoded by a^j, holds |

1253 |
for any other person j. |

1254 |
The size of f is quadratic in n. |

1255 |
*) |

1256 |
let mk_know_it_all f a p n = |

1257 |
let fkt1 i = |

1258 |
let pi = f.l_ap p i in |

1259 |
let npi = f.l_not pi in |

1260 |
let fkt2 j = |

1261 |
if j = i then f.l_tt |

1262 |
else |

1263 |
let apj = f.l_aa a j in |

1264 |
let f1 = f.l_imp pi (f.l_box apj pi) in |

1265 |
let f2 = f.l_imp npi (f.l_box apj npi) in |

1266 |
f.l_and f1 f2 |

1267 |
in |

1268 |
const_bigOp f.l_and f.l_tt fkt2 n |

1269 |
in |

1270 |
const_bigOp f.l_and f.l_tt fkt1 n |

1271 | |

1272 |
(** Generates a formula that captures the wise men puzzle. |

1273 |
@param f All the logical operations needed. |

1274 |
@param n The number of wise men which must be positive. |

1275 |
@param k The first k-1 wise men do not know |

1276 |
whether they are wearing a black hat. |

1277 |
The number must be positive and not greater than n. |

1278 |
@return A formula ~f such that f says: |

1279 |
If it is commonly known that at least one wise man is wearing a black hat, |

1280 |
that each wise man can see all other wise men, |

1281 |
and that the first k-1 wise men do not know whether they are wearing a black hat, |

1282 |
then the k-th wise man knows that he is wearing a black hat. |

1283 |
Note that f is a theorem iff n=k. |

1284 |
The size of ~f is quadratic in n. |

1285 |
*) |

1286 |
let mk_wisemen_tbox f n k = |

1287 |
let a = "a" in |

1288 |
let p = "p" in |

1289 |
let f1 = const_bigOp f.l_or f.l_ff (f.l_ap p) n in |

1290 |
let f2 = mk_know_it_all f a p n in |

1291 |
let pk = pred k in |

1292 |
let f3 = |

1293 |
let fkt3 i = f.l_not (f.l_box (f.l_aa a i) (f.l_ap p i)) in |

1294 |
const_bigOp f.l_and f.l_tt fkt3 pk |

1295 |
in |

1296 |
let concl = f.l_box (f.l_aa a pk) (f.l_ap p pk) in |

1297 |
(concl, [f1; f2; f3]) |

1298 | |

1299 |
let mk_wisemen f n k = |

1300 |
let a = "a" in |

1301 |
let (concl, tbox) = mk_wisemen_tbox f n k in |

1302 |
let ftbox = const_bigOpL f.l_and f.l_tt tbox in |

1303 |
let lst = mk_int_list n in |

1304 |
let al = List.map (fun i -> f.l_aa a i) lst in |

1305 |
let ck = f.l_aw al ftbox in |

1306 |
f.l_not (f.l_imp ck concl) |

1307 | |

1308 |
(** Generates a formula that captures the muddy children puzzle. |

1309 |
@param f All the logical operations needed. |

1310 |
@param n The number of children which must be positive. |

1311 |
@param k The number of muddy children |

1312 |
which must be positive and not greater than n. |

1313 |
@return A formula ~f such that f says: |

1314 |
If it is commonly known that at least one child is muddy, |

1315 |
that each child can see all other children, |

1316 |
and that at least k children are muddy, |

1317 |
then the fact that exactly k children are muddy implies |

1318 |
that all muddy children know that they are muddy. |

1319 |
Note that f is a theorem for all 1 <= k <= n. |

1320 |
Depending on k, the size of ~f can be exponential in n. |

1321 |
*) |

1322 |
let mk_muddychildren_tbox f n k = |

1323 |
let a = "a" in |

1324 |
let p = "p" in |

1325 |
let f1 = const_bigOp f.l_or f.l_ff (f.l_ap p) n in |

1326 |
let f2 = mk_know_it_all f a p n in |

1327 |
let alpha nrl = |

1328 |
assert (nrl <> []); |

1329 |
let fkt i = if List.mem i nrl then f.l_ap p i else f.l_not (f.l_ap p i) in |

1330 |
const_bigOp f.l_and f.l_tt fkt n |

1331 |
in |

1332 |
let nrl = mk_int_list k in |

1333 |
let f3 = |

1334 |
let rec mk_choose acc r n = |

1335 |
if n <= 0 then [f.l_not (alpha acc)] |

1336 |
else |

1337 |
let pn = pred n in |

1338 |
let l1 = if r > 0 then mk_choose (pn::acc) (pred r) pn else [] in |

1339 |
let l2 = if n > r then mk_choose acc r pn else [] in |

1340 |
l1 @ l2 |

1341 |
in |

1342 |
let fkt3 i = |

1343 |
let nll = mk_choose [] (succ i) n in |

1344 |
const_bigOpL f.l_and f.l_tt nll |

1345 |
in |

1346 |
const_bigOp f.l_and f.l_tt fkt3 (pred k) |

1347 |
in |

1348 |
let concl = |

1349 |
let c1 = alpha nrl in |

1350 |
let cl = List.map (fun i -> f.l_box (f.l_aa a i) (f.l_ap p i)) nrl in |

1351 |
let c2 = const_bigOpL f.l_and f.l_tt cl in |

1352 |
f.l_imp c1 c2 |

1353 |
in |

1354 |
(concl, [f1; f2; f3]) |

1355 | |

1356 |
let mk_muddychildren f n k = |

1357 |
let a = "a" in |

1358 |
let (concl, tbox) = mk_muddychildren_tbox f n k in |

1359 |
let ftbox = const_bigOpL f.l_and f.l_tt tbox in |

1360 |
let lst = mk_int_list n in |

1361 |
let al = List.map (fun i -> f.l_aa a i) lst in |

1362 |
let ck = f.l_aw al ftbox in |

1363 |
f.l_not (f.l_imp ck concl) |

1364 | |

1365 | |

1366 |
(** Encodes a Sudoku puzzle. |

1367 |
The encoding is based on an initial version by Martin Lange. |

1368 |
Note that a Sudoku can also be encoded as propositional formula. |

1369 |
@param f All the logical operations needed. |

1370 |
@param n The square root of the dimension of the Sudoku. |

1371 |
That is, the Sudoku has n*n rows, columns, and blocks. |

1372 |
@param unary Decides whether the encodings of the rows, columns, blocks, |

1373 |
and input numbers are unary or binary. |

1374 |
@param initV A list of tuples (x, y, r, c, i) |

1375 |
where the first four numbers specify the position of an entry e |

1376 |
and i specifies the value of that entry. More precisely: |

1377 |
0 <= x < n is the row index of the block b in which e lies; |

1378 |
0 <= y < n is the column index of b; |

1379 |
0 <= r < n is the row index of e inside b; |

1380 |
0 <= c < n is the column index of e inside b; |

1381 |
0 <= i < n*n is the value of e. |

1382 |
@return A formula f which encodes the Sudoku puzzle of dimension n*n |

1383 |
with the given initial values. |

1384 |
That is, f is satisfiable iff the Sudoku can be solved, |

1385 |
and each model which makes f true gives rise to a solution of the Sudoku. |

1386 |
The size of f is in O(n^4 * log n) in the binary case |

1387 |
and O(n^4) in the unary case. |

1388 |
*) |

1389 |
let mk_sudoku f n unary initV = |

1390 |
let bits m = |

1391 |
let rec blog i = function |

1392 |
| 0 -> raise (Failure "argument of function \"bits\" must be positive") |

1393 |
| 1 -> i |

1394 |
| m -> blog (i+1) (m/2) |

1395 |
in |

1396 |
blog 1 m |

1397 |
in |

1398 |
let bn = bits (pred n) in |

1399 |
let nn = n*n in |

1400 |
let bnn = bits (pred nn) in |

1401 | |

1402 |
let a = f.l_aa "a" 0 in |

1403 |
let l_box = f.l_box a in |

1404 |
let l_dia = f.l_dia a in |

1405 |
let l_aw = f.l_aw [a] in |

1406 |
let mk_and_lst l = const_bigOpL f.l_and f.l_tt l in |

1407 |
let propR i = f.l_ap "r" i in |

1408 |
let propC i = f.l_ap "c" i in |

1409 |
let propX i = f.l_ap "x" i in |

1410 |
let propY i = f.l_ap "y" i in |

1411 |
let propV i = f.l_ap "v" i in |

1412 | |

1413 |
let eq_counter prop b m = |

1414 |
let fkt i = if m land (1 lsl i) <> 0 then prop i else f.l_not (prop i) in |

1415 |
const_bigOp f.l_and f.l_tt fkt b |

1416 |
in |

1417 |
let eq_coord prop m = if unary then prop m else eq_counter prop bn m in |

1418 |
let eq_value m = if unary then propV m else eq_counter propV bnn m in |

1419 | |

1420 |
let zeroR = eq_coord propR 0 in |

1421 |
let zeroC = eq_coord propC 0 in |

1422 |
let zeroX = eq_coord propX 0 in |

1423 |
let zeroY = eq_coord propY 0 in |

1424 |
let maxR = eq_coord propR (pred n) in |

1425 |
let maxC = eq_coord propC (pred n) in |

1426 |
let maxX = eq_coord propX (pred n) in |

1427 |
let maxY = eq_coord propY (pred n) in |

1428 | |

1429 |
let init = mk_and_lst [zeroR; zeroC; zeroX; zeroY] in |

1430 | |

1431 |
let ax_initV = |

1432 |
let setField (x, y, r, c, i) = |

1433 |
let ante = mk_and_lst [eq_coord propR r; eq_coord propC c; |

1434 |
eq_coord propX x; eq_coord propY y] in |

1435 |
f.l_imp ante (eq_value i) |

1436 |
in |

1437 |
mk_and_lst (List.map setField initV) |

1438 |
in |

1439 | |

1440 |
let is_unique prop m = |

1441 |
let fkt1 i = |

1442 |
let fkt2 j = |

1443 |
let f2 = prop j in |

1444 |
if i = j then f2 else f.l_not f2 |

1445 |
in |

1446 |
const_bigOp f.l_and f.l_tt fkt2 m |

1447 |
in |

1448 |
const_bigOp f.l_or f.l_ff fkt1 m |

1449 |
in |

1450 |
let rec at_most_counter prop m bs = |

1451 |
if bs = 0 then f.l_tt |

1452 |
else |

1453 |
let f1 = f.l_not (prop (pred bs)) in |

1454 |
let f2 = at_most_counter prop m (pred bs) in |

1455 |
if m land (1 lsl (pred bs)) <> 0 then f.l_or f1 f2 else f.l_and f1 f2 |

1456 |
in |

1457 |
let valid_coord prop = if unary then is_unique prop n else at_most_counter prop (pred n) bn in |

1458 |
let ax_validR = valid_coord propR in |

1459 |
let ax_validC = valid_coord propC in |

1460 |
let ax_validX = valid_coord propX in |

1461 |
let ax_validY = valid_coord propY in |

1462 |
let ax_validV = if unary then is_unique propV nn else at_most_counter propV (pred nn) bnn in |

1463 | |

1464 |
let last = mk_and_lst [maxR; maxC; maxX; maxY] in |

1465 |
let ax_nosuc = f.l_imp last (l_box f.l_ff) in |

1466 |
let ax_suc = f.l_imp (f.l_not last) (l_dia f.l_tt) in |

1467 | |

1468 |
let count_up prop x max null = |

1469 |
if unary then |

1470 |
let fkt i = f.l_imp (prop i) (l_box (prop ((succ i) mod n))) in |

1471 |
const_bigOp f.l_and f.l_tt fkt n |

1472 |
else |

1473 |
let f1 = f.l_imp max (l_box null) in |

1474 |
let f2 = f.l_imp (f.l_not max) (mk_counter f a x bn) in |

1475 |
f.l_and f1 f2 |

1476 |
in |

1477 |
let stay_same prop = |

1478 |
let fkt i = |

1479 |
let f1 = f.l_imp (prop i) (l_box (prop i)) in |

1480 |
if unary then f1 |

1481 |
else |

1482 |
let f2 = f.l_imp (f.l_not (prop i)) (l_box (f.l_not (prop i))) in |

1483 |
f.l_and f1 f2 |

1484 |
in |

1485 |
const_bigOp f.l_and f.l_tt fkt (if unary then n else bn) |

1486 |
in |

1487 |
let cond_count_up maxCondL prop x max null = |

1488 |
let maxCond = mk_and_lst maxCondL in |

1489 |
let f1 = f.l_imp maxCond (count_up prop x max null) in |

1490 |
let f2 = f.l_imp (f.l_not maxCond) (stay_same prop) in |

1491 |
f.l_and f1 f2 |

1492 |
in |

1493 |
let ax_upR = count_up propR "r" maxR zeroR in |

1494 |
let ax_upC = cond_count_up [maxR] propC "c" maxC zeroC in |

1495 |
let ax_upX = cond_count_up [maxR; maxC] propX "x" maxX zeroX in |

1496 |
let ax_upY = cond_count_up [maxR; maxC; maxX] propY "y" maxY zeroY in |

1497 | |

1498 |
let no_doubles propA propB = |

1499 |
let fkt1 i = |

1500 |
let pAi = eq_coord propA i in |

1501 |
let fkt2 j = |

1502 |
let pBj = eq_coord propB j in |

1503 |
let fkt3 k = |

1504 |
let pVk = eq_value k in |

1505 |
let ante = mk_and_lst [pAi; pBj; pVk] in |

1506 |
let concl = l_box (l_aw (f.l_imp (f.l_and pAi pBj) (f.l_not pVk))) in |

1507 |
f.l_imp ante concl |

1508 |
in |

1509 |
const_bigOp f.l_and f.l_tt fkt3 nn |

1510 |
in |

1511 |
const_bigOp f.l_and f.l_tt fkt2 n |

1512 |
in |

1513 |
const_bigOp f.l_and f.l_tt fkt1 n |

1514 |
in |

1515 |
let ax_no_doubles_block = no_doubles propX propY in |

1516 |
let ax_no_doubles_row = no_doubles propX propR in |

1517 |
let ax_no_doubles_col = no_doubles propY propC in |

1518 | |

1519 |
let tbox = l_aw (mk_and_lst [ax_initV; |

1520 |
ax_validR; ax_validC; ax_validX; ax_validY; ax_validV; |

1521 |
ax_nosuc; ax_suc; |

1522 |
ax_upR; ax_upC; ax_upX; ax_upY; |

1523 |
ax_no_doubles_block; ax_no_doubles_row; ax_no_doubles_col]) |

1524 |
in |

1525 |
f.l_and init tbox |

1526 | |

1527 |
(** An instance of a Sudoku which was considered easy. |

1528 |
*) |

1529 |
let sudokuEasy = [(0,0,1,0,0);(0,0,0,1,2);(0,0,1,1,3);(0,0,2,2,5); |

1530 |
(0,1,0,0,4);(0,1,1,0,7);(0,1,0,1,8); |

1531 |
(0,2,2,0,0);(0,2,2,1,7);(0,2,1,2,6);(0,2,2,2,2); |

1532 |
(1,0,0,1,1);(1,0,1,1,7);(1,0,0,2,8);(1,0,2,2,4); |

1533 |
(1,1,1,0,3);(1,1,2,0,8);(1,1,0,1,4);(1,1,2,1,0);(1,1,0,2,2);(1,1,1,2,1); |

1534 |
(1,2,0,0,6);(1,2,2,0,2);(1,2,1,1,5);(1,2,2,1,3); |

1535 |
(2,0,0,0,1);(2,0,1,0,6);(2,0,0,1,4);(2,0,0,2,7); |

1536 |
(2,1,2,1,5);(2,1,1,2,4);(2,1,2,2,6); |

1537 |
(2,2,0,0,5);(2,2,1,1,8);(2,2,2,1,2);(2,2,1,2,3)] |

1538 | |

1539 |
(** An instance of a Sudoku which was considered tough. |

1540 |
*) |

1541 |
let sudokuTough = [(0,0,1,0,5); |

1542 |
(0,1,1,0,6);(0,1,1,1,8);(0,1,0,2,7);(0,1,2,2,3); |

1543 |
(0,2,1,0,4);(0,2,1,2,1);(0,2,2,2,6); |

1544 |
(1,0,1,1,0);(1,0,0,2,4);(1,0,2,2,1); |

1545 |
(1,2,0,0,5);(1,2,2,0,8);(1,2,1,1,7); |

1546 |
(2,0,0,0,6);(2,0,1,0,3);(2,0,1,2,8); |

1547 |
(2,1,0,0,5);(2,1,2,0,4);(2,1,1,1,7);(2,1,1,2,6); |

1548 |
(2,2,1,2,2)] |

1549 | |

1550 | |

1551 |
(** Generates a satisfiable formula a la Goranko. |

1552 |
@param f All the logical operations needed. |

1553 |
@param n The size of the formulae. |

1554 |
@return The formula "F p0 & ... & F pn-1" |

1555 |
*) |

1556 |
let mk_eFormula f n = |

1557 |
let a = f.l_aa "a" 0 in |

1558 |
let fkt i = f.l_ev [a] (f.l_ap "p" i) in |

1559 |
const_bigOp f.l_and f.l_tt fkt n |

1560 | |

1561 |
(** Generates a satisfiable formula a la Goranko. |

1562 |
@param f All the logical operations needed. |

1563 |
@param n The size of the formulae. |

1564 |
@return The formula "G p0 & ... & G pn-1" |

1565 |
*) |

1566 |
let mk_sFormula f n = |

1567 |
let a = f.l_aa "a" 0 in |

1568 |
let fkt i = f.l_aw [a] (f.l_ap "p" i) in |

1569 |
const_bigOp f.l_and f.l_tt fkt n |

1570 | |

1571 |
(** Generates a satisfiable formula a la Goranko. |

1572 |
@param f All the logical operations needed. |

1573 |
@param n The size of the formulae. |

1574 |
@return The formula "(((p0 U p2) U p3) U ...) U pn-1" |

1575 |
*) |

1576 |
let rec mk_ulFormula f n = |

1577 |
let n = pred n in |

1578 |
if n <= 0 then f.l_ap "p" 0 |

1579 |
else |

1580 |
let rest = mk_ulFormula f n in |

1581 |
f.l_until rest (f.l_ap "p" n) |

1582 | |

1583 |
(** Generates a satisfiable formula a la Goranko. |

1584 |
@param f All the logical operations needed. |

1585 |
@param n The size of the formulae. |

1586 |
@return The formula "p0 U (p1 U (... U pn-1))" |

1587 |
*) |

1588 |
let rec mk_urFormula f n = |

1589 |
const_bigOp f.l_until f.l_tt (fun i -> f.l_ap "p" i) n |

1590 | |

1591 |
(** Generates a satisfiable formula a la Goranko. |

1592 |
@param f All the logical operations needed. |

1593 |
@param n The size of the formulae. |

1594 |
@return The formula "A F p_1 | ... | A F p_n" |

1595 |
*) |

1596 |
let mk_c1Formula f n = |

1597 |
let a = f.l_aa "a" 0 in |

1598 |
let fkt i = f.l_aw [a] (f.l_ev [a] (f.l_ap "p" i)) in |

1599 |
const_bigOp f.l_or f.l_ff fkt n |

1600 | |

1601 |
(** Generates a satisfiable formula a la Goranko. |

1602 |
@param f All the logical operations needed. |

1603 |
@param n The size of the formulae. |

1604 |
@return The formula "A F p_1 & ... & A F p_n" |

1605 |
*) |

1606 |
let mk_c2Formula f n = |

1607 |
let a = f.l_aa "a" 0 in |

1608 |
let fkt i = f.l_aw [a] (f.l_ev [a] (f.l_ap "p" i)) in |

1609 |
const_bigOp f.l_and f.l_tt fkt n |

1610 | |

1611 |
(** Generates a formula which ensures seriality. |

1612 |
@param f All the logical operations needed. |

1613 |
@param al A list [a_0;...;a_n] of agents. |

1614 |
@return The formula "AW (<a_0>True & ... & <a_n>True)" |

1615 |
*) |

1616 |
let mk_serial f al = |

1617 |
let exl = List.map (fun a -> f.l_dia a f.l_tt) al in |

1618 |
let conj = const_bigOpL f.l_and f.l_tt exl in |

1619 |
f.l_aw al conj |

1620 | |

1621 |
(** Generates a satisfiable formula a la Montali. |

1622 |
@param f All the logical operations needed. |

1623 |
@param n The number of propositional variables. |

1624 |
@param d The nesting depth. |

1625 |
@return A formula "F (p0 & AX F (p0 & AX F (... & AX F p0))) & |

1626 |
G ((p0 => AX F p1) & ... & (pn-2 => AX F pn-1))" |

1627 |
*) |

1628 |
let mk_montaliSat f n d = |

1629 |
let a = f.l_aa "a" 0 in |

1630 |
let n = max 1 n in |

1631 |
let d = max 0 d in |

1632 |
let rec fktD i = |

1633 |
let p0 = f.l_ap "p" 0 in |

1634 |
if i = d then p0 |

1635 |
else |

1636 |
let f2 = fktD (succ i) in |

1637 |
f.l_and p0 (f.l_box a (f.l_ev [a] f2)) |

1638 |
in |

1639 |
let f1 = f.l_ev [a] (fktD 0) in |

1640 |
if n = 1 then f1 |

1641 |
else |

1642 |
let fktN i = |

1643 |
let pi = f.l_ap "p" i in |

1644 |
let pip = f.l_ap "p" (succ i) in |

1645 |
f.l_imp pi (f.l_box a (f.l_ev [a] pip)) |

1646 |
in |

1647 |
let f2 = const_bigOp f.l_and f.l_tt fktN (pred n) in |

1648 |
f.l_and f1 (f.l_aw [a] f2) |

1649 | |

1650 |
(** Generates an unsatisfiable formula a la Montali. |

1651 |
NOTE for CTL: formula is only unsatisfiable if AG/AU is taken for G/U. |

1652 |
@param f All the logical operations needed. |

1653 |
@param n The number of propositional variables. |

1654 |
@param d The nesting depth. |

1655 |
@return A formula "F (p0 & AX F (p0 & X F (... & X F p0))) & |

1656 |
G ((p0 => AX (~p0 U p1)) & ... & (pn-2 => AX (~pn-2 U pn-1))) & |

1657 |
~(F (pn-1 & AX F (pn-1 & AX F (... & AX F pn-1))))" |

1658 |
*) |

1659 |
let mk_montaliUnsat f n d = |

1660 |
let a = f.l_aa "a" 0 in |

1661 |
let n = max 1 n in |

1662 |
let d = max 0 d in |

1663 |
let p0 = f.l_ap "p" 0 in |

1664 |
let rec fktD1 i = |

1665 |
if i = d then p0 |

1666 |
else |

1667 |
let f2 = fktD1 (succ i) in |

1668 |
f.l_and p0 (f.l_box a (f.l_ev [a] f2)) |

1669 |
in |

1670 |
let f1 = f.l_ev [a] (fktD1 0) in |

1671 |
let pnm = f.l_ap "p" (pred n) in |

1672 |
let rec fktD2 i = |

1673 |
if i = d then pnm |

1674 |
else |

1675 |
let f2 = fktD2 (succ i) in |

1676 |
f.l_and pnm (f.l_box a (f.l_ev [a] f2)) |

1677 |
in |

1678 |
let f3 = f.l_not (f.l_ev [a] (fktD2 0)) in |

1679 |
if n = 1 then f.l_and f1 f3 |

1680 |
else |

1681 |
let fktN i = |

1682 |
let pi = f.l_ap "p" i in |

1683 |
let pip = f.l_ap "p" (succ i) in |

1684 |
f.l_imp pi (f.l_box a (f.l_until (f.l_not pi) pip)) |

1685 |
in |

1686 |
let f2 = const_bigOp f.l_and f.l_tt fktN (pred n) in |

1687 |
f.l_and f1 (f.l_and (f.l_aw [a] f2) f3) |

1688 | |

1689 |
(** Generates an unsatisfiable formula a la Marrero. |

1690 |
NOTE for CTL: formula is only unsatisfiable if AG/AF is taken for G/F. |

1691 |
@param f All the logical operations needed. |

1692 |
@param n The number of propositional variables. |

1693 |
@return A formula "~(p0 & G (AND[0,n-1][pi => AX p(i+1modn)]) => G F p0)" |

1694 |
*) |

1695 |
let mk_induction f n = |

1696 |
assert (n > 0); |

1697 |
let a = f.l_aa "a" 0 in |

1698 |
let f1 = |

1699 |
let fkt i = f.l_aw [a] (f.l_imp (f.l_ap "p" i) (f.l_box a (f.l_ap "p" ((succ i) mod n)))) in |

1700 |
const_bigOp f.l_and f.l_tt fkt n |

1701 |
in |

1702 |
let p0 = f.l_ap "p" 0 in |

1703 |
let f2 = f.l_and p0 f1 in |

1704 |
let f3 = f.l_aw [a] (f.l_ev [a] p0) in |

1705 |
f.l_not (f.l_imp f2 f3) |

1706 | |

1707 |
(** Generates an unsatisfiable formula a la Marrero. |

1708 |
NOTE for CTL: formula is only unsatisfiable if AG/AF is taken for G/F. |

1709 |
@param f All the logical operations needed. |

1710 |
@param n The number of propositional variables. |

1711 |
@return A formula "~(F pn & AND[0,n][~pi] & G (AND[0,n-1][~pi => AX ~pi+1]) => F p0)" |

1712 |
*) |

1713 |
let mk_precede f n = |

1714 |
assert (n > 0); |

1715 |
let a = f.l_aa "a" 0 in |

1716 |
let mkNF i = f.l_not (f.l_ap "p" i) in |

1717 |
let f1 = const_bigOp f.l_and f.l_tt mkNF (n+1) in |

1718 |
let f2 = |

1719 |
let fkt i = f.l_aw [a] (f.l_imp (mkNF i) (f.l_box a (mkNF (succ i)))) in |

1720 |
const_bigOp f.l_and f.l_tt fkt n |

1721 |
in |

1722 |
let f2 = f.l_and (f.l_ev [a] (f.l_ap "p" n)) (f.l_and f1 f2) in |

1723 |
let f3 = f.l_ev [a] (f.l_ap "p" 0) in |

1724 |
f.l_not (f.l_imp f2 f3) |

1725 | |

1726 |
(** Generates an unsatisfiable formula a la Marrero. |

1727 |
NOTE for CTL: formula is only unsatisfiable if AG/AF is taken for G/F. |

1728 |
@param f All the logical operations needed. |

1729 |
@param n The number of propositional variables. |

1730 |
@return A formula "~(G (F p0 & AND[0,n-1][pi => AX F p(i+1modn)]) => G F pn-1)" |

1731 |
*) |

1732 |
let mk_fair f n = |

1733 |
assert (n > 0); |

1734 |
let a = f.l_aa "a" 0 in |

1735 |
let f1 = |

1736 |
let fkt i = f.l_aw [a] (f.l_imp (f.l_ap "p" i) (f.l_box a (f.l_ev [a] (f.l_ap "p" ((succ i) mod n))))) in |

1737 |
const_bigOp f.l_and f.l_tt fkt n |

1738 |
in |

1739 |
let f2 = f.l_and (f.l_aw [a] (f.l_ev [a] (f.l_ap "p" 0))) f1 in |

1740 |
let f3 = f.l_aw [a] (f.l_ev [a] (f.l_ap "p" (pred n))) in |

1741 |
f.l_not (f.l_imp f2 f3) |

1742 | |

1743 |
(** Generates a satisfiable formula a la Marrero. |

1744 |
NOTE for CTL: formula is only unsatisfiable if AG/AF is taken for G/F. |

1745 |
@param f All the logical operations needed. |

1746 |
@param n The number of propositional variables. |

1747 |
@return A formula "~(G (AND[0,n-1][pi => AX p(i+1modn)]) => G F p0)" |

1748 |
*) |

1749 |
let mk_nobase f n = |

1750 |
assert (n > 0); |

1751 |
let a = f.l_aa "a" 0 in |

1752 |
let f1 = |

1753 |
let fkt i = f.l_aw [a] (f.l_imp (f.l_ap "p" i) (f.l_box a (f.l_ap "p" ((succ i) mod n)))) in |

1754 |
const_bigOp f.l_and f.l_tt fkt n |

1755 |
in |

1756 |
let f2 = f.l_aw [a] (f.l_ev [a] (f.l_ap "p" 0)) in |

1757 |
f.l_not (f.l_imp f1 f2) |

1758 | |

1759 |
(** Generates a formula a la Hustadt. |

1760 |
@param f All the logical operations needed. |

1761 |
@param k The number of "literals" in the clauses. |

1762 |
@param l The number of clauses. |

1763 |
@param n The number of propositional variables. |

1764 |
@return A randomly generated formula as described in |

1765 |
Hustadt and Konev: TRP++: A temporal resolution prover. |

1766 |
*) |

1767 |
let gen_Cran1 f k l n = |

1768 |
let a = f.l_aa "a" 0 in |

1769 |
let lits = genLiterals (fun i -> f.l_ap "p" (int_of_string i)) "" n in |

1770 |
let fktk (pi, _) = |

1771 |
let li = if Random.bool () then pi else f.l_not pi in |

1772 |
f.l_box a li |

1773 |
in |

1774 |
let fktl _ = |

1775 |
let pls = chooseK k lits in |

1776 |
let lls = List.map fktk pls in |

1777 |
let cli = const_bigOpL f.l_or f.l_ff lls in |

1778 |
f.l_aw [a] cli |

1779 |
in |

1780 |
let f1 = const_bigOp f.l_and f.l_tt fktl l in |

1781 |
let fktp i = |

1782 |
let npi = f.l_not (fst (List.nth lits i)) in |

1783 |
let evip = f.l_ev [a] (fst (List.nth lits ((succ i) mod n))) in |

1784 |
f.l_aw [a] (f.l_or npi evip) |

1785 |
in |

1786 |
let f2 = const_bigOp f.l_and f.l_tt fktp n in |

1787 |
f.l_and f1 f2 |

1788 | |

1789 |
(** Generates a formula a la Hustadt. |

1790 |
@param f All the logical operations needed. |

1791 |
@param k The number of "literals" in the clauses. |

1792 |
@param l The number of clauses. |

1793 |
@param n The number of propositional variables. |

1794 |
@return A randomly generated formula as described in |

1795 |
Hustadt and Konev: TRP++: A temporal resolution prover. |

1796 |
*) |

1797 |
let gen_Cran2 f k l n = |

1798 |
let a = f.l_aa "a" 0 in |

1799 |
let lits = genLiterals (fun i -> f.l_ap "p" (int_of_string i)) "" n in |

1800 |
let fktk (pi, _) = if Random.bool () then pi else f.l_not pi in |

1801 |
let r0 = f.l_ap "r" 0 in |

1802 |
let fktl _ = |

1803 |
let pls = chooseK k lits in |

1804 |
let lls = List.map fktk pls in |

1805 |
const_bigOpL f.l_or f.l_ff (r0 :: lls) |

1806 |
in |

1807 |
let f1 = const_bigOp f.l_and f.l_tt fktl l in |

1808 |
let fkt1 i = |

1809 |
let l1 = f.l_not (f.l_ap "r" (n-1-i)) in |

1810 |
let l2 = f.l_box a (f.l_ap "r" ((n-i) mod n)) in |

1811 |
f.l_aw [a] (f.l_or l1 l2) |

1812 |
in |

1813 |
let f2 = const_bigOp f.l_and f.l_tt fkt1 n in |

1814 |
let nqnm1 = f.l_not (f.l_ap "q" (n-1)) in |

1815 |
let fkt2 i = |

1816 |
let l1 = f.l_not (f.l_ap "r" (n-1-i)) in |

1817 |
f.l_aw [a] (f.l_or l1 (f.l_box a nqnm1)) |

1818 |
in |

1819 |
let f3 = const_bigOp f.l_and f.l_tt fkt2 n in |

1820 |
let f4 = f.l_and (f.l_or (f.l_not r0) (f.l_ap "q" 0)) (f.l_or (f.l_not r0) nqnm1) in |

1821 |
let fkt3 i = |

1822 |
let g1 = f.l_or (f.l_not (f.l_ap "q" i)) (f.l_ev [a] (f.l_ap "s" (i+1))) in |

1823 |
let h1 = f.l_or (f.l_not (f.l_ap "s" (i+1))) (f.l_ap "q" (i+1)) in |

1824 |
let g2 = |

1825 |
if i = n - 2 then h1 |

1826 |
else |

1827 |
let fkt4 i = f.l_box a (f.l_ap "q" (n-1-i)) in |

1828 |
let h2 = const_bigOp f.l_or f.l_ff fkt4 (n-2-i) in |

1829 |
f.l_or h1 h2 |

1830 |
in |

1831 |
f.l_and (f.l_aw [a] g1) (f.l_aw [a] g2) |

1832 |
in |

1833 |
let f5 = const_bigOp f.l_and f.l_tt fkt3 (n-1) in |

1834 |
const_bigOpL f.l_and f.l_tt [f1; f2; f3; f4; f5] |