Project

General

Profile

Statistics
| Branch: | Revision:

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]