Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / ALCFormula.ml @ 40a714df

History | View | Annotate | Download (54.2 KB)

1
(** This module implements ALC formulae
2
    including inverse roles
3
    (e.g. parsing, printing, (de-)constructing, ...).
4
    @author Florian Widmann
5
 *)
6

    
7

    
8
module HC = HashConsing
9
module A = AltGenlex
10

    
11

    
12
(** A general exception for all kinds of errors
13
    that can happen in the tableau procedure.
14
    More specific information is given in the argument. 
15
 *)
16
exception ALCException of string
17

    
18

    
19
(** Defines ALC formulae.
20
 *)
21
type formula =
22
  | TRUE
23
  | FALSE
24
  | AP of string
25
  | NOT of formula
26
  | EX of string * bool * formula
27
  | AX of string * bool * formula
28
  | MIN of int * string * bool * formula
29
  | MAX of int * string * bool * formula
30
  | EQU of formula * formula
31
  | IMP of formula * formula
32
  | OR of formula * formula
33
  | AND of formula * formula
34

    
35
(** Defines TBox definitions.
36
    It can either be a primitive definition
37
    of the form cn <= f,
38
    or a necessary and sufficient definition
39
    of the form cn = f
40
    (where cn is a concept name and f a concept).
41
 *)
42
type definition =
43
  | PRIMITIVE of string * formula
44
  | NECANDSUFF of string * formula
45

    
46
(** The number of constructors of type formula.
47
 *)
48
let numberOfTypes = 12
49

    
50
(** Maps a formula to an integer representing its type (e.g. or-formula).
51
    The assignment of integers to types is arbitrary,
52
    but it is guaranteed that different types 
53
    map to different integers
54
    and that the codomain of this function is [0..numberOfTypes-1].
55
    @param f A formula.
56
    @return An integer that represents the type of f.
57
 *)
58
let getTypeFormula f = 
59
  match f with
60
  | TRUE -> 0
61
  | FALSE -> 1
62
  | AP _ -> 2
63
  | NOT _ -> 3
64
  | EX _ -> 4
65
  | AX _ -> 5
66
  | EQU _ -> 6
67
  | IMP _ -> 7
68
  | OR _ -> 8
69
  | AND _ -> 9
70
  | MIN _ -> 10
71
  | MAX _ -> 11
72

    
73
(** Generates a function comp that compares two formula.
74
    The order that is defined by comp is lexicograhic.
75
    It depends on the given ranking of types of formulae.
76
    @param order A list containing exactly the numbers 0 to numberOfTypes-1.
77
    Each number represents a type
78
    and the list therefore induces a ranking on the types
79
    with the smallest type being the first in the list.
80
    @return A function comp that compares two formula.
81
    comp f1 f2 returns 0 iff f1 is equal to f2, 
82
    -1 if f1 is smaller than f2, and
83
    1 if f1 is greater than f2.
84
    @raise Failure if order is not of the required form.
85
 *)
86
let generateCompare order =
87
  let rec listOK = function
88
    | 0 -> true
89
    | n ->
90
        let nn = pred n in
91
        if List.mem nn order then listOK nn
92
        else false
93
  in
94
  let _ = 
95
    if (List.length order <> numberOfTypes) || not (listOK numberOfTypes) then
96
      raise (Failure "generateCompare: argument is not in the correct form")
97
  in
98
  let arrayOrder = Array.make numberOfTypes 0 in
99
  let _ = 
100
    for i = 0 to (numberOfTypes - 1) do
101
      let ty = List.nth order i in
102
      arrayOrder.(ty) <- i
103
    done
104
  in
105
  let rec comp f1 f2 =
106
    match f1, f2 with
107
    | TRUE, TRUE
108
    | FALSE, FALSE -> 0
109
    | AP s1, AP s2 -> compare s1 s2
110
    | NOT f1a, NOT f2a -> comp f1a f2a
111
    | EX (s1, i1, f1a), EX (s2, i2, f2a)
112
    | AX (s1, i1, f1a), AX (s2, i2, f2a) ->
113
        let res1 = compare s1 s2 in
114
        if res1 <> 0 then res1
115
        else
116
          let res2 = compare i1 i2 in
117
          if res2 <> 0 then res2
118
          else comp f1a f2a
119
    | MIN (n1, s1, i1, f1a), MIN (n2, s2, i2, f2a)
120
    | MAX (n1, s1, i1, f1a), MAX (n2, s2, i2, f2a) ->
121
        let res0 = compare n1 n2 in
122
        if res0 <> 0 then res0
123
        else
124
          let res1 = compare s1 s2 in
125
          if res1 <> 0 then res1
126
          else
127
            let res2 = compare i1 i2 in
128
            if res2 <> 0 then res2
129
            else comp f1a f2a
130
    | OR (f1a, f1b), OR (f2a, f2b)
131
    | AND (f1a, f1b), AND (f2a, f2b)
132
    | EQU (f1a, f1b), EQU (f2a, f2b)
133
    | IMP (f1a, f1b), IMP (f2a, f2b) ->
134
        let res1 = comp f1a f2a in
135
        if res1 <> 0 then res1
136
        else comp f1b f2b
137
    | _ ->
138
        let t1 = getTypeFormula f1 in
139
        let r1 = arrayOrder.(t1) in
140
        let t2 = getTypeFormula f2 in
141
        let r2 = arrayOrder.(t2) in
142
        if r1 < r2 then (-1) else 1
143
  in
144
  comp
145

    
146
(** Defines a ranking of the different types of formulae
147
    such that the ranking of the types corresponds
148
    to the ranking of the tableau rules.
149
 *)
150
let aRanking = [ getTypeFormula (OR (TRUE, TRUE));
151
                 getTypeFormula (EX ("", false, TRUE));
152
                 getTypeFormula (AX ("", false, TRUE));
153
                 getTypeFormula TRUE;
154
                 getTypeFormula FALSE;
155
                 getTypeFormula (AP "");
156
                 getTypeFormula (NOT TRUE);
157
                 getTypeFormula (AND (TRUE, TRUE));
158
                 getTypeFormula (EQU (TRUE, TRUE));
159
                 getTypeFormula (IMP (TRUE, TRUE));
160
                 getTypeFormula (MIN (0, "", false, TRUE));
161
                 getTypeFormula (MAX (0, "", false, TRUE)) ]
162

    
163

    
164
(** Determines the size of a formula.
165
    Basically, it counts the symbols (without parentheses) of a formula, 
166
    where <r> _ etc. is treated as one symbol.
167
    @param f A formula.
168
    @return The size of f.
169
 *)
170
let rec sizeFormula f =
171
  match f with
172
  | TRUE 
173
  | FALSE 
174
  | AP _ -> 1
175
  | NOT f1
176
  | EX (_, _, f1)
177
  | AX (_, _, f1)
178
  | MIN (_, _, _, f1)
179
  | MAX (_, _, _, f1) -> succ (sizeFormula f1)
180
  | EQU (f1, f2) 
181
  | IMP (f1, f2)
182
  | OR (f1, f2)  
183
  | AND (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
184

    
185

    
186
(** Appends a string representation of a formula to a string buffer.
187
    Parentheses are ommited where possible
188
    where the preference rules are defined as usual.
189
    @param sb A string buffer.
190
    @param f A formula.
191
 *)
192
let rec exportFormula_buffer sb f =
193
  let prio n lf =
194
    let prionr = function
195
      | EQU _ -> 0
196
      | IMP _  -> 1 
197
      | OR _ -> 2
198
      | AND _ -> 3
199
      | _ -> 4
200
    in
201
    if prionr lf < n then begin
202
      Buffer.add_char sb '(';
203
      exportFormula_buffer sb lf;
204
      Buffer.add_char sb ')'
205
    end
206
    else exportFormula_buffer sb lf
207
  in
208
  match f with
209
  | TRUE -> Buffer.add_string sb "True"
210
  | FALSE -> Buffer.add_string sb "False"
211
  | AP s -> Buffer.add_string sb s
212
  | NOT f1 ->
213
      Buffer.add_string sb "~";
214
      prio 4 f1
215
  | EX (s, i1, f1) ->
216
      Buffer.add_string sb "<";
217
      Buffer.add_string sb s;
218
      if i1 then Buffer.add_string sb "-" else ();
219
      Buffer.add_string sb ">";
220
      prio 4 f1
221
  | AX (s, i1, f1) ->
222
      Buffer.add_string sb "[";
223
      Buffer.add_string sb s;
224
      if i1 then Buffer.add_string sb "-" else ();
225
      Buffer.add_string sb "]";
226
      prio 4 f1
227
  | MIN (n, s, i1, f1) ->
228
      Buffer.add_string sb "{>=";
229
      Buffer.add_string sb (string_of_int n);
230
      Buffer.add_string sb " ";
231
      Buffer.add_string sb s;
232
      if i1 then Buffer.add_string sb "-" else ();
233
      Buffer.add_string sb "}";
234
      prio 4 f1
235
  | MAX (n, s, i1, f1) ->
236
      Buffer.add_string sb "{<=";
237
      Buffer.add_string sb (string_of_int n);
238
      Buffer.add_string sb " ";
239
      Buffer.add_string sb s;
240
      if i1 then Buffer.add_string sb "-" else ();
241
      Buffer.add_string sb "}";
242
      prio 4 f1
243
  | EQU (f1, f2) ->
244
      prio 0 f1;
245
      Buffer.add_string sb " <=> ";
246
      prio 0 f2
247
  | IMP (f1, f2) ->
248
      prio 2 f1;
249
      Buffer.add_string sb " => ";
250
      prio 2 f2
251
  | OR (f1, f2) ->
252
      prio 2 f1;
253
      Buffer.add_string sb " | ";
254
      prio 2 f2
255
  | AND (f1, f2) ->
256
      prio 3 f1;
257
      Buffer.add_string sb " & ";
258
      prio 3 f2
259

    
260
(** Converts a formula into a string representation.
261
    Parentheses are ommited where possible
262
    where the preference rules are defined as usual.
263
    @param f A formula.
264
    @return A string representing f.
265
 *)
266
let exportFormula f =
267
  let size = sizeFormula f in
268
  let sb = Buffer.create (2 * size) in
269
  exportFormula_buffer sb f;
270
  Buffer.contents sb
271

    
272
(** Converts a formula query into a string representation.
273
    @param fl A list of formulae representing the initial input.
274
    @param tboxND A list of formulae representing
275
    the non-definitional part of a TBox.
276
    @param tboxD A list of definitions
277
    representing the definitional part of a TBox.
278
    @return A string representing tboxND; tboxD |- fl.
279
    @raise ALCException Iff one of the defined formulae in tboxD
280
    is not a concept.
281
 *)
282
let exportQuery fl tboxND tboxD =
283
  let sb = Buffer.create 1000 in
284
  let exportDef = function
285
    | PRIMITIVE (s, f) ->
286
        Buffer.add_string sb s;
287
        Buffer.add_string sb " # ";
288
        exportFormula_buffer sb f
289
    | NECANDSUFF (s, f) ->
290
        Buffer.add_string sb s;
291
        Buffer.add_string sb " = ";
292
        exportFormula_buffer sb f
293
  in
294
  let rec expFl fkt = function
295
    | [] -> ()
296
    | h::tl -> 
297
        fkt h;
298
        if tl <> [] then Buffer.add_string sb "; " else ();
299
        expFl fkt tl
300
  in
301
  expFl (exportFormula_buffer sb) tboxND;
302
  if tboxND <> [] && tboxD <> [] then Buffer.add_string sb "; " else ();
303
  expFl exportDef tboxD;
304
  Buffer.add_string sb "  |-  ";
305
  expFl (exportFormula_buffer sb) fl;
306
  Buffer.contents sb
307

    
308

    
309
let lexer = A.make_lexer 
310
    ["#";"=";"|-";";";"(";")";"=>";"<=>";"|";"&";"~";"True";"False";"<";">";"[";"]";"-";"{<=";"{>=";"}"] 
311

    
312
let mk_exn s = ALCException s
313

    
314
(** These functions parse a token stream to obtain a formula.
315
    It is a standard recursive descent procedure.
316
    @param ts A token stream.
317
    @return The resulting (sub-)formula.
318
    @raise ALCException if ts does not represent a formula.
319
 *)
320
let rec parse_equ ts =
321
  let f1 = parse_imp ts in
322
  match Stream.peek ts with
323
  | None -> f1
324
  | Some (A.Kwd "<=>") ->
325
      Stream.junk ts;
326
      let f2 = parse_equ ts in
327
      EQU (f1, f2)
328
  | _ -> f1
329

    
330
(** These functions parse a token stream to obtain a formula.
331
    It is a standard recursive descent procedure.
332
    @param ts A token stream.
333
    @return The resulting (sub-)formula.
334
    @raise ALCException if ts does not represent a formula.
335
 *)
336
and parse_imp ts =
337
  let f1 = parse_or ts in
338
  match Stream.peek ts with
339
  | None -> f1
340
  | Some (A.Kwd "=>") ->
341
      Stream.junk ts;
342
      let f2 = parse_imp ts in
343
      IMP (f1, f2)
344
  | _ -> f1
345

    
346
(** These functions parse a token stream to obtain a formula.
347
    It is a standard recursive descent procedure.
348
    @param ts A token stream.
349
    @return The resulting (sub-)formula.
350
    @raise ALCException if ts does not represent a formula.
351
 *)
352
and parse_or ts =
353
  let f1 = parse_and ts in
354
  match Stream.peek ts with
355
  | None -> f1
356
  | Some (A.Kwd "|") ->
357
      Stream.junk ts;
358
      let f2 = parse_or ts in
359
      OR (f1, f2)
360
  | _ -> f1
361

    
362
(** These functions parse a token stream to obtain a formula.
363
    It is a standard recursive descent procedure.
364
    @param ts A token stream.
365
    @return The resulting (sub-)formula.
366
    @raise ALCException if ts does not represent a formula.
367
 *)
368
and parse_and ts =
369
  let f1 = parse_rest ts in
370
  match Stream.peek ts with
371
  | None -> f1
372
  | Some (A.Kwd "&") ->
373
      Stream.junk ts;
374
      let f2 = parse_and ts in
375
      AND (f1, f2)
376
  | _ -> f1
377

    
378
(** These functions parse a token stream to obtain a formula.
379
    It is a standard recursive descent procedure.
380
    @param ts A token stream.
381
    @return The resulting (sub-)formula.
382
    @raise ALCException if ts does not represent a formula.
383
 *)
384
and parse_rest ts =
385
  let boxinternals noNo es =
386
    let n =
387
      if noNo then 0
388
      else
389
        match Stream.next ts with
390
        | A.Int n when n >= 0 -> n
391
        | t -> A.printError mk_exn ~t ~ts "<non-negative number> expected: "
392
    in
393
    let s =
394
      match Stream.peek ts with
395
      | Some (A.Ident s1) -> Stream.junk ts; s1
396
      | Some (A.Kwd c) when c = es -> ""
397
      | Some (A.Kwd "-") -> ""
398
      | Some t -> A.printError mk_exn ~ts ("role name, \"-\", or \"" ^ es ^ "\" expected: ")
399
      | None -> A.printError mk_exn ~ts ("role name, \"-\", or \"" ^ es ^ "\" expected: ")
400
    in
401
    let isInv =
402
      match Stream.next ts with
403
      | A.Kwd c when c = es -> false
404
      | A.Kwd "-" -> begin
405
          match Stream.next ts with
406
          | A.Kwd c when c = es -> true
407
          | t -> A.printError mk_exn ~t ~ts ("\"" ^ es ^ "\" expected: ")
408
        end
409
      | t -> A.printError mk_exn ~t ~ts ("\"-\" or \"" ^ es ^ "\" expected: ")
410
    in
411
    (n, s, isInv)
412
  in
413
  match Stream.next ts with
414
  | A.Kwd "<" -> 
415
      let (_, s, isInv) = boxinternals true ">" in
416
      let f1 = parse_rest ts in
417
      EX (s, isInv, f1) 
418
  | A.Kwd "[" -> 
419
      let (_, s, isInv) = boxinternals true "]" in
420
      let f1 = parse_rest ts in
421
      AX (s, isInv, f1)
422
  | A.Kwd "{>=" -> 
423
      let (n, s, isInv) = boxinternals false "}" in
424
      let f1 = parse_rest ts in
425
      MIN (n, s, isInv, f1)
426
  | A.Kwd "{<=" -> 
427
      let (n, s, isInv) = boxinternals false "}" in
428
      let f1 = parse_rest ts in
429
      MAX (n, s, isInv, f1)
430
  | A.Kwd "(" -> 
431
      let f = parse_equ ts in
432
      let _ =
433
        match Stream.next ts with
434
        | A.Kwd ")" -> ()
435
        | t -> A.printError mk_exn ~t ~ts "\")\" expected: "
436
      in
437
      f
438
  | A.Kwd "~" ->
439
      let f = parse_rest ts in
440
      NOT f
441
  | A.Kwd "True" -> TRUE
442
  | A.Kwd "False" -> FALSE
443
  | A.Ident s -> AP s
444
  | t -> A.printError mk_exn ~t ~ts 
445
        "\"<\", \"[\", \"~\", \"(\", \"True\", \"False\", or <ident> expected: "
446
        
447
(** Parses a string to obtain a formula.
448
    @param s A string representing a formula.
449
    @return The resulting formula.
450
    @raise ALCException if s does not represent a formula.
451
 *)
452
let importFormula s =
453
  let ts = lexer s in
454
  try
455
    begin
456
      let f = parse_equ ts in
457
      let _ =
458
        match Stream.peek ts with
459
        | None -> ()
460
        | Some _ -> A.printError mk_exn ~ts "EOS expected: "
461
      in
462
      f
463
    end
464
  with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS"
465

    
466

    
467
(** Parses a list of formulae separated by ";".
468
    @param wDef Iff set to true then definitions are allowed.
469
    @param ts A token stream.
470
    @param accF The list of formulae parsed so far.
471
    @param accD The list of definitions parsed so far.
472
    @return The resulting lists of formulae and definitions.
473
    @raise ALCException if ts does not represent a list of formulae
474
    and definitions (if allowed).
475
 *)
476
let rec parse_formulaeDefList wDef ts (accF, accD) =
477
  let defopt =
478
    if not wDef then None
479
    else
480
      let p2 = Stream.npeek 2 ts in
481
      if List.length p2 < 2 then None
482
      else
483
        match List.hd p2 with
484
        | A.Ident s1 -> begin
485
            match List.nth p2 1 with
486
            | A.Kwd "=" ->
487
                Stream.junk ts;
488
                Stream.junk ts;
489
                let f1 = parse_equ ts in
490
                Some (NECANDSUFF (s1, f1))
491
            | A.Kwd "#" ->
492
                Stream.junk ts;
493
                Stream.junk ts;
494
                let f1 = parse_equ ts in
495
                Some (PRIMITIVE (s1, f1))
496
            | _ -> None
497
        end
498
        | _ -> None
499
  in
500
  let (accF1, accD1) as acc1 =
501
    match defopt with
502
    | None ->
503
        let f1 = parse_equ ts in
504
        (f1::accF, accD)
505
    | Some def -> (accF, def::accD)
506
  in
507
  match Stream.peek ts with
508
  | Some (A.Kwd ";") ->
509
      Stream.junk ts;
510
      parse_formulaeDefList wDef ts acc1
511
  | _ -> (List.rev accF1, List.rev accD1)
512

    
513
(** Parses a string to obtain a formula query.
514
    @param s A string representing a formula query.
515
    @return A triple (fl, tboxND, tboxD) where
516
    fl is a list of formula representing the initial input;
517
    tboxND is a list of formulae representing
518
    the non-definitional part of a TBox; and
519
    tboxD is a list of definitions
520
    representing the definitional part of a TBox.
521
    @raise ALCException if s does not represent a formula query.
522
 *)
523
let importQuery s =
524
  let ts = lexer s in
525
  try
526
    begin
527
      let res =
528
        match Stream.peek ts with
529
        | Some (A.Kwd "|-") ->
530
            Stream.junk ts;
531
            let (fl1, _) = parse_formulaeDefList false ts ([], []) in
532
            (fl1, [], [])
533
        | _ ->
534
            begin
535
              let (fl1, dl1) = parse_formulaeDefList true ts ([], []) in
536
              match Stream.peek ts with
537
              | Some (A.Kwd "|-") ->
538
                  Stream.junk ts;
539
                  let (fl2, _) = parse_formulaeDefList false ts ([], []) in
540
                  (fl2, fl1, dl1)
541
              | _ -> 
542
                  if dl1 = [] then (fl1, [], [])
543
                  else A.printError mk_exn ~ts "\"|-\" expected: "
544
            end
545
      in
546
      let _ =
547
        match Stream.peek ts with
548
        | None -> ()
549
        | Some _ -> A.printError mk_exn ~ts "EOS expected: "
550
      in
551
      res
552
    end
553
  with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS"
554

    
555

    
556
(** Substitutes some propositional variables in a formula.
557
    @param subl A list of pairs (s, fp) 
558
    where s is the name of a propositional variable and fp is a formula.
559
    @param f A formula.
560
    @return A formula f' where each propositional variable p
561
    such that (p, fp) is contained in subl is replaced by fp.
562
 *)
563
let rec substFormula subl f =
564
  match f with
565
  | TRUE
566
  | FALSE -> f
567
  | AP s -> if List.mem_assoc s subl then List.assoc s subl else f
568
  | NOT f1 ->
569
      let ft = substFormula subl f1 in
570
      if ft == f1 then f else NOT ft
571
  | EX (s, i, f1) ->
572
      let ft = substFormula subl f1 in
573
      if ft == f1 then f else EX (s, i, ft)
574
  | AX (s, i, f1) ->
575
      let ft = substFormula subl f1 in
576
      if ft == f1 then f else AX (s, i, ft)
577
  | MIN (n, s, i, f1) ->
578
      let ft = substFormula subl f1 in
579
      if ft == f1 then f else MIN (n, s, i, ft)
580
  | MAX (n, s, i, f1) ->
581
      let ft = substFormula subl f1 in
582
      if ft == f1 then f else MAX (n, s, i, ft)
583
  | EQU (f1, f2) ->
584
      let ft1 = substFormula subl f1 in
585
      let ft2 = substFormula subl f2 in
586
      if (f1 == ft1) && (f2 == ft2) then f 
587
      else EQU (ft1, ft2)
588
  | IMP (f1, f2) ->
589
      let ft1 = substFormula subl f1 in
590
      let ft2 = substFormula subl f2 in
591
      if (f1 == ft1) && (f2 == ft2) then f 
592
      else IMP (ft1, ft2)
593
  | OR (f1, f2) ->
594
      let ft1 = substFormula subl f1 in
595
      let ft2 = substFormula subl f2 in
596
      if (f1 == ft1) && (f2 == ft2) then f 
597
      else OR (ft1, ft2)
598
  | AND (f1, f2) ->
599
      let ft1 = substFormula subl f1 in
600
      let ft2 = substFormula subl f2 in
601
      if (f1 == ft1) && (f2 == ft2) then f 
602
      else AND (ft1, ft2)
603

    
604

    
605
(** Converts the negation of a formula to negation normal form
606
    by "pushing in" the negations "~".
607
    The symbols "<=>" and "=>" are substituted by their usual definitions.
608
    @param f A formula.
609
    @return A formula in negation normal form and not containing "<=>" or "=>"
610
    that is equivalent to ~f.
611
 *)
612
let rec nnfNeg f =
613
  match f with
614
  | TRUE -> FALSE
615
  | FALSE -> TRUE
616
  | AP _ -> NOT f
617
  | NOT f1 -> nnf f1
618
  | EX (s, i, f1) -> AX (s, i, nnfNeg f1)
619
  | AX (s, i, f1) -> EX (s, i, nnfNeg f1)
620
  | MIN (n, s, i, f1) ->
621
      if n = 0 then FALSE else MAX (n-1, s, i, nnf f1)
622
  | MAX (n, s, i, f1) -> MIN (n+1, s, i, nnf f1)
623
  | EQU (f1, f2) -> OR (AND (nnf f1, nnfNeg f2), AND (nnf f2, nnfNeg f1))
624
  | IMP (f1, f2) -> AND (nnf f1, nnfNeg f2)
625
  | OR (f1, f2) -> AND (nnfNeg f1, nnfNeg f2)
626
  | AND (f1, f2) -> OR (nnfNeg f1, nnfNeg f2)
627
        
628
(** Converts a formula to negation normal form
629
    by "pushing in" the negations "~".
630
    The symbols "<=>" and "=>" are substituted by their usual definitions.
631
    @param f A formula.
632
    @return A formula in negation normal form and not containing "<=>" or "=>"
633
    that is equivalent to f.
634
 *)
635
and nnf f =
636
  match f with
637
  | TRUE
638
  | FALSE
639
  | AP _
640
  | NOT (AP _) -> f
641
  | NOT f1 -> nnfNeg f1
642
  | EX (s, i, f1) -> 
643
      let ft = nnf f1 in
644
      if ft == f1 then f else EX (s, i, ft)
645
  | AX (s, i, f1) ->
646
      let ft = nnf f1 in
647
      if ft == f1 then f else AX (s, i, ft)
648
  | MIN (n, s, i, f1) ->
649
      let ft = nnf f1 in
650
      if ft == f1 then f else MIN (n, s, i, ft)
651
  | MAX (n, s, i, f1) ->
652
      let ft = nnf f1 in
653
      if ft == f1 then f else MAX (n, s, i, ft)
654
  | EQU (f1, f2) -> AND (OR (nnfNeg f1, nnf f2), OR (nnfNeg f2, nnf f1))
655
  | IMP (f1, f2) -> OR (nnfNeg f1, nnf f2)
656
  | OR (f1, f2) ->
657
      let ft1 = nnf f1 in
658
      let ft2 = nnf f2 in
659
      if ft1 == f1 && ft2 == f2 then f else OR (ft1, ft2)
660
  | AND (f1, f2) ->
661
      let ft1 = nnf f1 in
662
      let ft2 = nnf f2 in
663
      if ft1 == f1 && ft2 == f2 then f else AND (ft1, ft2)
664

    
665

    
666
(** Checks whether a formula contains inverse roles.
667
    @param f A formula.
668
    @return True iff f contains some inverse roles.
669
 *)
670
let rec containsInverse f =
671
  match f with
672
  | TRUE
673
  | FALSE
674
  | AP _ -> false
675
  | NOT f1 -> containsInverse f1
676
  | EX (_, i, f1)
677
  | AX (_, i, f1)
678
  | MIN (_, _, i, f1)
679
  | MAX (_, _, i, f1) -> i || containsInverse f1
680
  | EQU (f1, f2)
681
  | IMP (f1, f2)
682
  | OR (f1, f2)
683
  | AND (f1, f2) -> containsInverse f1 || containsInverse f2
684

    
685

    
686
(** Simplifies a formula that is in negation normal form.
687
    @param f A formula in negation normal form.
688
    @return A formula in negation normal form that is equivalent to f.
689
    @raise ALCException if f is not in negation normal form.
690
 *)
691
let rec simplifyFormula f =
692
  match f with
693
  | TRUE
694
  | FALSE
695
  | AP _
696
  | NOT (AP _) -> f
697
  | EX (s, i, f1) ->
698
      let ft = simplifyFormula f1 in
699
      begin
700
        match ft with
701
        | FALSE -> FALSE
702
        | _ -> if ft == f1 then f else EX (s, i, ft)
703
      end
704
  | AX (s, i, f1) ->
705
      let ft = simplifyFormula f1 in
706
      begin
707
        match ft with
708
        | TRUE -> TRUE
709
        | _ -> if ft == f1 then f else AX (s, i, ft)
710
      end
711
  | MIN (n, s, i, f1) ->
712
      if n = 0 then TRUE
713
      else
714
        let ft = simplifyFormula f1 in
715
        begin
716
          match ft with
717
          | FALSE -> FALSE
718
          | _ -> if ft == f1 then f else MIN (n, s, i, ft)
719
        end
720
  | MAX (n, s, i, f1) ->
721
      let ft = simplifyFormula f1 in
722
      begin
723
        match ft with
724
        | FALSE -> TRUE
725
        | _ -> if ft == f1 then f else MAX (n, s, i, ft)
726
      end
727
  | OR (f1, f2) ->
728
      let ft1 = simplifyFormula f1 in
729
      let ft2 = simplifyFormula f2 in
730
      begin
731
        match ft1, ft2 with
732
        | TRUE, _ -> TRUE
733
        | FALSE, _ -> ft2
734
        | _, TRUE -> TRUE
735
        | _, FALSE -> ft1
736
        | _, _ ->
737
            if (f1 == ft1) && (f2 == ft2) then f 
738
            else OR (ft1, ft2)
739
      end
740
  | AND (f1, f2) ->
741
      let ft1 = simplifyFormula f1 in
742
      let ft2 = simplifyFormula f2 in
743
      begin
744
        match ft1, ft2 with
745
        | TRUE, _ -> ft2
746
        | FALSE, _ -> FALSE
747
        | _, TRUE -> ft1
748
        | _, FALSE -> FALSE
749
        | _, _ ->
750
            if (f1 == ft1) && (f2 == ft2) then f 
751
            else AND (ft1, ft2)
752
      end
753
  | _ -> raise (ALCException "Formula is not in negation normal form.")
754

    
755

    
756
(** Destructs an atomic proposition.
757
    @param f An atomic proposition.
758
    @return The name of the atomic proposition.
759
    @raise ALCException if f is not an atomic proposition.
760
 *)
761
let dest_ap f =
762
  match f with
763
  | AP s -> s
764
  | _ -> raise (ALCException "Formula is not an atomic proposition.")
765

    
766
(** Destructs a negation.
767
    @param f A negation.
768
    @return The immediate subformula of the negation.
769
    @raise ALCException if f is not a negation.
770
 *)
771
let dest_not f =
772
  match f with
773
  | NOT f1 -> f1
774
  | _ -> raise (ALCException "Formula is not a negation.")
775

    
776
(** Destructs an EX-formula.
777
    @param f An EX-formula.
778
    @return The role name, whether it is an inverse role,
779
    and the immediate subformula of the EX-formula.
780
    @raise ALCException if f is not an EX-formula.
781
 *)
782
let dest_ex f =
783
  match f with
784
  | EX (s, i, f1) -> (s, i, f1)
785
  | _ -> raise (ALCException "Formula is not an EX-formula.")
786

    
787
(** Destructs an AX-formula.
788
    @param f An AX-formula.
789
    @return The role name, whether it is an inverse role,
790
    and the immediate subformula of the AX-formula.
791
    @raise ALCException if f is not an AX-formula.
792
 *)
793
let dest_ax f =
794
  match f with
795
  | AX (s, i, f1) -> (s, i, f1)
796
  | _ -> raise (ALCException "Formula is not an AX-formula.")
797

    
798
(** Destructs a MIN-formula.
799
    @param f A MIN-formula.
800
    @return The number restriction, role name, whether it is an inverse role,
801
    and the immediate subformula of the MIN-formula.
802
    @raise ALCException if f is not a MIN-formula.
803
 *)
804
let dest_min f =
805
  match f with
806
  | MIN (n, s, i, f1) -> (n, s, i, f1)
807
  | _ -> raise (ALCException "Formula is not a MIN-formula.")
808

    
809
(** Destructs a MAX-formula.
810
    @param f A MAX-formula.
811
    @return The number restriction, role name, whether it is an inverse role,
812
    and the immediate subformula of the MAX-formula.
813
    @raise ALCException if f is not a MAX-formula.
814
 *)
815
let dest_max f =
816
  match f with
817
  | MAX (n, s, i, f1) -> (n, s, i, f1)
818
  | _ -> raise (ALCException "Formula is not a MAX-formula.")
819

    
820
(** Destructs an equivalence.
821
    @param f An equivalence.
822
    @return The two immediate subformulae of the equivalence.
823
    @raise ALCException if f is not an equivalence.
824
 *)
825
let dest_equ f =
826
  match f with
827
  | EQU (f1, f2) -> (f1, f2)
828
  | _ -> raise (ALCException "Formula is not an equivalence.")
829

    
830
(** Destructs an implication.
831
    @param f An implication.
832
    @return The two immediate subformulae of the implication.
833
    @raise ALCException if f is not an implication.
834
 *)
835
let dest_imp f =
836
  match f with
837
  | IMP (f1, f2) -> (f1, f2)
838
  | _ -> raise (ALCException "Formula is not an implication.")
839

    
840
(** Destructs an or-formula.
841
    @param f An or-formula.
842
    @return The two immediate subformulae of the or-formula.
843
    @raise ALCException if f is not an or-formula.
844
 *)
845
let dest_or f =
846
  match f with
847
  | OR (f1, f2) -> (f1, f2)
848
  | _ -> raise (ALCException "Formula is not an or-formula.")
849

    
850
(** Destructs an and-formula.
851
    @param f An and-formula.
852
    @return The two immediate subformulae of the and-formula.
853
    @raise ALCException if f is not an and-formula.
854
 *)
855
let dest_and f =
856
  match f with
857
  | AND (f1, f2) -> (f1, f2)
858
  | _ -> raise (ALCException "Formula is not an and-formula.")
859

    
860

    
861
(** Tests whether a formula is the constant True.
862
    @param f A formula.
863
    @return True iff f is the constant True.
864
 *)
865
let is_true f =
866
  match f with
867
  | TRUE -> true
868
  | _ -> false
869

    
870
(** Tests whether a formula is the constant False.
871
    @param f A formula.
872
    @return True iff f is the constant False.
873
 *)
874
let is_false f =
875
  match f with
876
  | FALSE -> true
877
  | _ -> false
878

    
879
(** Tests whether a formula is an atomic proposition.
880
    @param f A formula.
881
    @return True iff f is an atomic proposition.
882
 *)
883
let is_ap f =
884
  match f with
885
  | AP _ -> true
886
  | _ -> false
887

    
888
(** Tests whether a formula is a negation.
889
    @param f A formula.
890
    @return True iff f is a negation.
891
 *)
892
let is_not f =
893
  match f with
894
  | NOT _ -> true
895
  | _ -> false
896

    
897
(** Tests whether a formula is an EX-formula.
898
    @param f A formula.
899
    @return True iff f is an EX-formula.
900
 *)
901
let is_ex f =
902
  match f with
903
  | EX _ -> true
904
  | _ -> false
905

    
906
(** Tests whether a formula is an AX-formula.
907
    @param f A formula.
908
    @return True iff f is an AX-formula.
909
 *)
910
let is_ax f =
911
  match f with
912
  | AX _ -> true
913
  | _ -> false
914

    
915
(** Tests whether a formula is a MIN-formula.
916
    @param f A formula.
917
    @return True iff f is a MIN-formula.
918
 *)
919
let is_min f =
920
  match f with
921
  | MIN _ -> true
922
  | _ -> false
923

    
924
(** Tests whether a formula is a MAX-formula.
925
    @param f A formula.
926
    @return True iff f is a MAX-formula.
927
 *)
928
let is_max f =
929
  match f with
930
  | MAX _ -> true
931
  | _ -> false
932

    
933
(** Tests whether a formula is an equivalence.
934
    @param f A formula.
935
    @return True iff f is an equivalence.
936
 *)
937
let is_equ f =
938
  match f with
939
  | EQU _ -> true
940
  | _ -> false
941

    
942
(** Tests whether a formula is an implication.
943
    @param f A formula.
944
    @return True iff f is an implication.
945
 *)
946
let is_imp f =
947
  match f with
948
  | IMP _ -> true
949
  | _ -> false
950

    
951
(** Tests whether a formula is an or-formula.
952
    @param f A formula.
953
    @return True iff f is an or-formula.
954
 *)
955
let is_or f =
956
  match f with
957
  | OR _ -> true
958
  | _ -> false
959

    
960
(** Tests whether a formula is an and-formula.
961
    @param f A formula.
962
    @return True iff f is an and-formula.
963
 *)
964
let is_and f =
965
  match f with
966
  | AND _ -> true
967
  | _ -> false
968

    
969
        
970
(** The constant True.
971
 *)
972
let const_true = TRUE
973

    
974
(** The constant False.
975
 *)
976
let const_false = FALSE
977
    
978
(** Constructs an atomic proposition.
979
    @param s The name of the atomic proposition.
980
    @return The atomic proposition with name s.
981
 *)
982
let const_ap s = AP s
983

    
984
(** Negates a formula.
985
    @param f A formula.
986
    @return The negation of f.
987
 *)
988
let const_not f = NOT f
989

    
990
(** Constructs an EX-formula from a formula.
991
    @param s A role name.
992
    @param i True if it is an inverse role, false otherwise.
993
    @param f A formula.
994
    @return The formula EX f.
995
 *)
996
let const_ex s i f = EX (s, i, f)
997

    
998
(** Constructs an AX-formula from a formula.
999
    @param s A role name.
1000
    @param i True if it is an inverse role, false otherwise.
1001
    @param f A formula.
1002
    @return The formula AX f.
1003
 *)
1004
let const_ax s i f = AX (s, i, f)
1005

    
1006
(** Constructs a MIN-formula from a formula.
1007
    @param n A non-negative integer.
1008
    @param s A role name.
1009
    @param i True if it is an inverse role, false otherwise.
1010
    @param f A formula.
1011
    @return The formula MIN f.
1012
    @raise ALCException Iff n is negative.
1013
 *)
1014
let const_min n s i f =
1015
  if n < 0 then raise (ALCException "Negative cardinality constraint.")
1016
  else MIN (n, s, i, f)
1017

    
1018
(** Constructs a MAX-formula from a formula.
1019
    @param n A non-negative integer.
1020
    @param s A role name.
1021
    @param i True if it is an inverse role, false otherwise.
1022
    @param f A formula.
1023
    @return The formula MAX f.
1024
    @raise ALCException Iff n is negative.
1025
 *)
1026
let const_max n s i f =
1027
  if n < 0 then raise (ALCException "Negative cardinality constraint.")
1028
  else MAX (n, s, i, f)
1029

    
1030
(** Constructs an equivalence from two formulae.
1031
    @param f1 The first formula (LHS).
1032
    @param f2 The second formula (LHS).
1033
    @return The equivalence f1 <=> f2.
1034
 *)
1035
let const_equ f1 f2 = EQU (f1, f2)
1036

    
1037
(** Constructs an implication from two formulae.
1038
    @param f1 The first formula (LHS).
1039
    @param f2 The second formula (LHS).
1040
    @return The implication f1 => f2.
1041
 *)
1042
let const_imp f1 f2 = IMP (f1, f2)
1043

    
1044
(** Constructs an or-formula from two formulae.
1045
    @param f1 The first formula (LHS).
1046
    @param f2 The second formula (LHS).
1047
    @return The formula f1 | f2.
1048
 *)
1049
let const_or f1 f2 = OR (f1, f2)
1050

    
1051
(** Constructs an and-formula from two formulae.
1052
    @param f1 The first formula (LHS).
1053
    @param f2 The second formula (LHS).
1054
    @return The formula f1 & f2.
1055
 *)    
1056
let const_and f1 f2 = AND (f1, f2)
1057

    
1058

    
1059
(** Calculates all formulae
1060
    that may be created in the tableau procedure (i.e. a kind of Fischer-Ladner closure).
1061
    @param compF A function that compares formulae.
1062
    @param f The initial formula of the tableau procedure
1063
    which must be in negation normal form.
1064
    @return A list containing all formulae of the closure in increasing order.
1065
    @raise ALCException if f is not in negation normal form.
1066
 *)
1067
let detClosure compF f =
1068
  let module TSet = Set.Make(
1069
    struct
1070
      type t = formula
1071
      let (compare : t -> t -> int) = compF
1072
    end
1073
   )
1074
  in
1075
  let rec detC fs f =
1076
    if TSet.mem f fs then fs
1077
    else
1078
      let nfs = TSet.add f fs in
1079
      match f with
1080
      | TRUE
1081
      | FALSE -> nfs
1082
      | AP _ -> TSet.add (NOT f) nfs
1083
      | NOT (AP s) -> TSet.add (AP s) nfs
1084
      | EX (_, _, f1)
1085
      | AX (_, _, f1) -> detC nfs f1
1086
      | OR (f1, f2)
1087
      | AND (f1, f2) ->
1088
          let nfs = detC nfs f1 in
1089
          detC nfs f2
1090
      | _ -> raise (ALCException "Formula is not in negation normal form.")
1091
  in
1092
  let tset = TSet.empty in
1093
  let tset = TSet.add TRUE tset in
1094
  let tset = TSet.add FALSE tset in
1095
  let rset = detC tset f in
1096
  TSet.elements rset
1097

    
1098

    
1099
(** Hash-consed formulae, which are in negation normal form,
1100
    such that structural and physical equality coincide.
1101
 *)
1102
type hcFormula = (hcFormula_node, formula) HC.hash_consed
1103
and hcFormula_node =
1104
  | HCTRUE
1105
  | HCFALSE
1106
  | HCAP of string
1107
  | HCNOT of string
1108
  | HCEX of string * bool * hcFormula
1109
  | HCAX of string * bool * hcFormula
1110
  | HCOR of hcFormula * hcFormula
1111
  | HCAND of hcFormula * hcFormula
1112

    
1113
(** Determines whether two formula nodes are structurally equal.
1114
    @param f1 The first formula node.
1115
    @param f2 The second formula node.
1116
    @return True iff f1 and f2 are structurally equal.
1117
 *)
1118
let equal_hcFormula_node f1 f2 =
1119
  match f1, f2 with
1120
  | HCTRUE, HCTRUE -> true
1121
  | HCFALSE, HCFALSE -> true
1122
  | HCAP s1, HCAP s2
1123
  | HCNOT s1, HCNOT s2 -> compare s1 s2 = 0
1124
  | HCEX (s1, i1, f1), HCEX (s2, i2, f2)
1125
  | HCAX (s1, i1, f1), HCAX (s2, i2, f2) -> compare s1 s2 = 0 && i1 = i2 && f1 == f2
1126
  | HCOR (f1a, f1b), HCOR (f2a, f2b)
1127
  | HCAND (f1a, f1b), HCAND (f2a, f2b) -> f1a == f2a && f1b == f2b
1128
  | _ -> false
1129

    
1130
(** Computes the hash value of a formula node.
1131
    @param f A formula node.
1132
    @return The hash value of f.
1133
 *)
1134
let hash_hcFormula_node f =
1135
  match f with
1136
  | HCTRUE -> 0
1137
  | HCFALSE -> 1
1138
  | HCAP s -> Hashtbl.hash s
1139
  | HCNOT s -> Hashtbl.hash s + 1
1140
  | HCEX (s, i, f1) -> 19 * (19 * (Hashtbl.hash s) + (if i then 1 else 0) + f1.HC.hkey) + 3
1141
  | HCAX (s, i, f1) -> 19 * (19 * (Hashtbl.hash s) + (if i then 1 else 0) + f1.HC.hkey) + 4
1142
  | HCOR (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 5
1143
  | HCAND (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 6
1144

    
1145
(** Determines the "real" formula of a formula node.
1146
    @param f A formula node.
1147
    @return The formula (in negation normal form) which corresponds to f.
1148
 *)
1149
let toFml_hcFormula_node f =
1150
  match f with
1151
  | HCTRUE -> TRUE
1152
  | HCFALSE -> FALSE
1153
  | HCAP s -> AP s
1154
  | HCNOT s -> NOT (AP s)
1155
  | HCEX (s, i, f1) -> EX (s, i, f1.HC.fml)
1156
  | HCAX (s, i, f1) -> AX (s, i, f1.HC.fml)
1157
  | HCOR (f1, f2) ->
1158
      let fml1 = f1.HC.fml in
1159
      let fml2 = f2.HC.fml in
1160
      OR (fml1, fml2)
1161
  | HCAND (f1, f2) ->
1162
      let fml1 = f1.HC.fml in
1163
      let fml2 = f2.HC.fml in
1164
      AND (fml1, fml2)
1165

    
1166
(** Determines the negation (in negation normal form) of a formula node.
1167
    @param f A formula node.
1168
    @return The negation (in negation normal form) of f.
1169
 *)
1170
let negNde_hcFormula_node f =
1171
  match f with
1172
  | HCTRUE -> HCFALSE
1173
  | HCFALSE -> HCTRUE
1174
  | HCAP s -> HCNOT s
1175
  | HCNOT s -> HCAP s
1176
  | HCEX (s, i, f2) -> HCAX (s, i, f2.HC.neg)
1177
  | HCAX (s, i, f2) -> HCEX (s, i, f2.HC.neg)
1178
  | HCOR (f1, f2) ->
1179
      let notf1 = f1.HC.neg in
1180
      let notf2 = f2.HC.neg in
1181
      HCAND (notf1, notf2)
1182
  | HCAND (f1, f2) ->
1183
      let notf1 = f1.HC.neg in
1184
      let notf2 = f2.HC.neg in
1185
      HCOR (notf1, notf2)
1186

    
1187
(** An instantiation of hash-consing for formulae.
1188
 *)
1189
module HcFormula = HC.Make(
1190
  struct
1191
    type nde = hcFormula_node
1192
    type fml = formula
1193
    let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2
1194
    let hash (n : nde) = hash_hcFormula_node n
1195
    let negNde (n : nde) = negNde_hcFormula_node n
1196
    let toFml (n : nde) = toFml_hcFormula_node n
1197
  end
1198
 )
1199

    
1200

    
1201
(** An instantiation of a hash table (of the standard library)
1202
    for hash-consed formulae. The test for equality
1203
    and computing the hash value is done in constant time.
1204
 *)
1205
module HcFHt = Hashtbl.Make(
1206
  struct
1207
    type t = hcFormula
1208
    let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag
1209
    let hash (f : t) = f.HC.tag
1210
  end
1211
 )
1212

    
1213

    
1214
(** Converts a formula into its hash-consed version.
1215
    @param hcF A hash-cons table for formulae.
1216
    @param f A formula in negation normal form.
1217
    @return The hash-consed version of f.
1218
    @raise ALCException if f is not in negation normal form.
1219
*)
1220
let rec hc_formula hcF f =
1221
  match f with
1222
  | TRUE -> HcFormula.hashcons hcF HCTRUE
1223
  | FALSE -> HcFormula.hashcons hcF HCFALSE
1224
  | AP s -> HcFormula.hashcons hcF (HCAP s)
1225
  | NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s)
1226
  | EX (s, i, f1) ->
1227
      let tf1 = hc_formula hcF f1 in
1228
      HcFormula.hashcons hcF (HCEX (s, i, tf1))
1229
  | AX (s, i, f1) ->
1230
      let tf1 = hc_formula hcF f1 in
1231
      HcFormula.hashcons hcF (HCAX (s, i, tf1))
1232
  | OR (f1, f2) ->
1233
      let tf1 = hc_formula hcF f1 in
1234
      let tf2 = hc_formula hcF f2 in
1235
      HcFormula.hashcons hcF (HCOR (tf1, tf2))
1236
  | AND (f1, f2) ->
1237
      let tf1 = hc_formula hcF f1 in
1238
      let tf2 = hc_formula hcF f2 in
1239
      HcFormula.hashcons hcF (HCAND (tf1, tf2))
1240
  | _ -> raise (ALCException "Formula is not in negation normal form.")
1241

    
1242

    
1243
(** Calculates all formulae
1244
    which may be created in the tableau procedure (i.e. a kind of Fischer-Ladner closure).
1245
    @param hcF A hash-cons table for formulae.
1246
    @param hcnnf The initial formula of the tableau procedure as hash-consed version.
1247
    (which is in negation normal form).
1248
    @return A list containing all hash-consed formulae of the closure (in arbitrary order).
1249
    @raise ALCException if nnf is not in negation normal form.
1250
 *)
1251
let detClosureHc hcF hcnnf =
1252
  let hcFht = HcFHt.create 100 in
1253
  HcFHt.add hcFht (HcFormula.hashcons hcF HCTRUE) ();
1254
  HcFHt.add hcFht (HcFormula.hashcons hcF HCFALSE) ();
1255
  let rec detC f =
1256
    if HcFHt.mem hcFht f then ()
1257
    else begin
1258
      HcFHt.add hcFht f ();
1259
      match f.HC.node with
1260
      | HCTRUE
1261
      | HCFALSE
1262
      | HCAP _
1263
      | HCNOT _ -> ()
1264
      | HCOR (f1, f2)
1265
      | HCAND (f1, f2) ->
1266
          detC f1;
1267
          detC f2
1268
      | HCEX (_, _, f1)
1269
      | HCAX (_, _, f1) -> detC f1
1270
    end
1271
  in
1272
  detC hcnnf;
1273
  let flist = HcFHt.fold (fun f () acc -> f::acc) hcFht [] in
1274
  flist
1275

    
1276

    
1277
(** Converts a formula into a string representation for alc-tableau.
1278
    @param f A formula with no inverse roles.
1279
    @return A string representing f for alc-tableau.
1280
    @raise ALCException If f contains number restrictions or inverse roles, or
1281
    if the name of an atomic program
1282
    or a propositional variable in f is "tt" or "ff".
1283
 *)
1284
let exportFormulaAlcTableau f =
1285
  let size = sizeFormula f in
1286
  let sb = Buffer.create (2 * size) in
1287
  let rec expF = function
1288
    | TRUE -> Buffer.add_string sb "tt"
1289
    | FALSE -> Buffer.add_string sb "ff"
1290
    | AP s -> 
1291
        if s <> "tt" && s <> "ff" then Buffer.add_string sb s
1292
        else raise (ALCException "Formula contains \"tt\" or \"ff\".")
1293
    | NOT f1 ->
1294
        Buffer.add_string sb "not(";
1295
        expF f1;
1296
        Buffer.add_string sb ")"
1297
    | EX (s1, i1, f1) ->
1298
        if i1 then raise (ALCException "Formula contains inverse roles.")
1299
        else begin
1300
          Buffer.add_string sb "some(";
1301
          Buffer.add_string sb s1;
1302
          Buffer.add_string sb ",";
1303
          expF f1;
1304
          Buffer.add_string sb ")"
1305
        end
1306
    | AX (s1, i1, f1) ->
1307
        if i1 then raise (ALCException "Formula contains inverse roles.")
1308
        else begin
1309
          Buffer.add_string sb "all(";
1310
          Buffer.add_string sb s1;
1311
          Buffer.add_string sb ",";
1312
          expF f1;
1313
          Buffer.add_string sb ")"
1314
        end
1315
    | MIN _
1316
    | MAX _ -> raise (ALCException "Formula contains number restrictions.")
1317
    | EQU (f1, f2) ->
1318
        Buffer.add_string sb "equiv(";
1319
        expF f1;
1320
        Buffer.add_string sb ",";
1321
        expF f2;
1322
        Buffer.add_string sb ")"
1323
    | IMP (f1, f2) ->
1324
        Buffer.add_string sb "implies(";
1325
        expF f1;
1326
        Buffer.add_string sb ",";
1327
        expF f2;
1328
        Buffer.add_string sb ")"
1329
    | OR (f1, f2) ->
1330
        Buffer.add_string sb "disj(";
1331
        expF f1;
1332
        Buffer.add_string sb ",";
1333
        expF f2;
1334
        Buffer.add_string sb ")"
1335
    | AND (f1, f2) ->
1336
        Buffer.add_string sb "conj(";
1337
        expF f1;
1338
        Buffer.add_string sb ",";
1339
        expF f2;
1340
        Buffer.add_string sb ")"
1341
  in
1342
  expF f;
1343
  Buffer.contents sb
1344

    
1345

    
1346
(** Creates a file representing a TBox in FaCT++ format.
1347
    The satisfiability query is the definition
1348
    of the special concept name "SAT".
1349
    @param The name of the output file.
1350
    @param fl A list of formulae which are to be tested for joint satisfiability.
1351
    @param tboxND A list of formulae representing
1352
    the non-definitional part of a TBox.
1353
    @param tboxD A list of definitions
1354
    representing the definitional part of a TBox.
1355
    The definitions must not be cyclic
1356
    and each concept must not be defined more than once.
1357
 *)
1358
let createFactTBox filename fl tboxND tboxD =
1359
  assert (fl <> []);
1360
  let file = open_out filename in
1361
  let ps s = output_string file s in
1362
  let rec printFormula = function
1363
    | TRUE -> ps "*TOP*"
1364
    | FALSE -> ps "*BOTTOM*"
1365
    | AP s -> ps s
1366
    | NOT f1 -> 
1367
        ps "(not ";
1368
        printFormula f1;
1369
        ps ")"
1370
    | EX (s, i1, f1) ->
1371
        ps ("(some " ^ (if i1 then "(inv r" ^ s ^ ") " else "r" ^ s ^ " "));
1372
        printFormula f1;
1373
        ps ")"
1374
    | AX (s, i1, f1) ->
1375
        ps ("(all " ^ (if i1 then "(inv r" ^ s ^ ") " else "r" ^ s ^ " "));
1376
        printFormula f1;
1377
        ps ")"
1378
    | MIN (n, s, i1, f1) ->
1379
        ps ("(min " ^ (string_of_int n) ^ (if i1 then " (inv r" ^ s ^ ") " else " r" ^ s ^ " "));
1380
        printFormula f1;
1381
        ps ")"
1382
    | MAX (n, s, i1, f1) ->
1383
        ps ("(max " ^ (string_of_int n) ^ (if i1 then " (inv r" ^ s ^ ") " else " r" ^ s ^ " "));
1384
        printFormula f1;
1385
        ps ")"
1386
    | EQU (f1, f2) -> printFormula (AND (OR (NOT f1, f2), OR (NOT f2, f1)))
1387
    | IMP (f1, f2) -> printFormula (OR (NOT f1, f2))
1388
    | OR (f1, f2) ->
1389
        ps "(or ";
1390
        printFormula f1;
1391
        ps " ";
1392
        printFormula f2;
1393
        ps ")"
1394
    | AND (f1, f2) ->
1395
        ps "(and ";
1396
        printFormula f1;
1397
        ps " ";
1398
        printFormula f2;
1399
        ps ")"
1400
  in
1401
  let printTBoxD = function
1402
    | PRIMITIVE (s, f) ->
1403
        ps ("(implies_c " ^ s ^ " ");
1404
        printFormula f;
1405
        ps ")\n"
1406
    | NECANDSUFF (s, f) ->
1407
        ps ("(equal_c " ^ s ^ " ");
1408
        printFormula f;
1409
        ps ")\n"
1410
  in
1411
  let f = List.fold_left (fun res f -> AND (res, f)) (List.hd fl) (List.tl fl) in
1412
  let printTBoxND f =
1413
    ps "(implies_c *TOP* ";
1414
    printFormula f;
1415
    ps ")\n"
1416
  in
1417
  List.iter printTBoxD tboxD;
1418
  List.iter printTBoxND tboxND;
1419
  ps "(equal_c SAT ";
1420
  printFormula f;
1421
  ps ")\n";
1422
  close_out file
1423

    
1424
(** Determines all propositional variables and roles
1425
    occurring in a list of formulae.
1426
    @param fl A list of formulae.
1427
    @return A list containing all propositional variables in fl
1428
    and a list containing all roles occurring in fl.
1429
 *)
1430
let detVars fl =
1431
  let module PSet = Set.Make(String) in
1432
  let rec detPR ((ps, rs) as pr) = function
1433
    | TRUE
1434
    | FALSE -> pr
1435
    | AP s ->  (PSet.add s ps, rs)
1436
    | NOT f1 -> detPR pr f1
1437
    | EX (s, _, f1)
1438
    | AX (s, _, f1)
1439
    | MIN (_, s, _, f1)
1440
    | MAX (_, s, _, f1) -> detPR (ps, PSet.add s rs) f1
1441
    | EQU (f1, f2)
1442
    | IMP (f1, f2)
1443
    | OR (f1, f2)
1444
    | AND (f1, f2) ->
1445
        let npr = detPR pr f1 in
1446
        detPR npr f2
1447
  in
1448
  let (pset, rset) = List.fold_left (fun acc f -> detPR acc f) (PSet.empty, PSet.empty) fl in
1449
  (PSet.elements pset, PSet.elements rset)
1450

    
1451
(** Creates a file representing a formula for Will's prover.
1452
    @param The name of the output file.
1453
    @param f A formula which must not contain inverse roles and
1454
    must not contain more than one role.
1455
    @raise ALCException If f contains inverse roles or more than one role.
1456
 *)
1457
let createWill filename f =
1458
  if containsInverse f then raise (ALCException "Formula contains inverse roles.") else ();
1459
  let (_, pl) = detVars [f] in
1460
  if List.length pl > 1 then raise (ALCException "Formula contains more than one role.") else ();
1461
  let file = open_out filename in
1462
  let ps s = output_string file s in
1463
  let isProperName s =
1464
    let len = String.length s in
1465
    let rec isNumber i =
1466
      if i <= 0 then true
1467
      else
1468
        let c = Char.code s.[i] in
1469
        c >= Char.code '0' && c <= Char.code '9' && isNumber (i-1)
1470
    in
1471
    len >= 2 && s.[0] = 'p' && isNumber (len-1)
1472
  in
1473
  let rec printFormula = function
1474
    | TRUE -> printFormula (NOT FALSE)
1475
    | FALSE ->
1476
        (* prerr_endline "Will's prover does not support constants true/false natively"; *)
1477
        printFormula (AND (AP "p0", NOT (AP "p0")))
1478
    | AP s ->
1479
        if isProperName s then ps s
1480
        else raise (ALCException "Propositional variables have to be of the form p0, p1, etc.")
1481
    | NOT f1 -> 
1482
        ps "(~ ";
1483
        printFormula f1;
1484
        ps ")"
1485
    | EX (_, _, f1) ->
1486
        ps ("(<0> ");
1487
        printFormula f1;
1488
        ps ")"
1489
    | AX (s, i1, f1) -> printFormula (NOT (EX (s, i1, NOT f1)))
1490
    | MIN (n, _, _, f1) ->
1491
        if n = 0 then printFormula TRUE
1492
        else begin
1493
          ps ("(<" ^ (string_of_int (n-1)) ^ "> ");
1494
          printFormula f1;
1495
          ps ")"
1496
        end
1497
    | MAX (n, s, i1, f1) -> printFormula (NOT (MIN (n+1, s, i1, f1)))
1498
    | EQU (f1, f2) -> printFormula (AND (OR (NOT f1, f2), OR (NOT f2, f1)))
1499
    | IMP (f1, f2) -> printFormula (OR (NOT f1, f2))
1500
    | OR (f1, f2) ->
1501
        ps "(";
1502
        printFormula f1;
1503
        ps " v ";
1504
        printFormula f2;
1505
        ps ")"
1506
    | AND (f1, f2) ->
1507
        ps "(";
1508
        printFormula f1;
1509
        ps " & ";
1510
        printFormula f2;
1511
        ps ")"
1512
  in
1513
  ps "Logic: GML\n";
1514
  printFormula f;
1515
  close_out file
1516

    
1517
(** Creates a file representing a TBox in OWL format.
1518
    The satisfiability query is added as an anonymous assertion (ABox constraint).
1519
    @param The name of the output file.
1520
    @param fl A list of formulae which are to be tested for joint satisfiability.
1521
    @param tboxND A list of formulae representing
1522
    the non-definitional part of a TBox.
1523
    @param tboxD A list of definitions
1524
    representing the definitional part of a TBox.
1525
    The definitions must not be cyclic
1526
    and each concept must not be defined more than once.
1527
 *)
1528
let createOWL filename fl tboxND tboxD =
1529
  assert (fl <> []);
1530
  let file = open_out filename in
1531
  let addTBoxD acc = function
1532
    | PRIMITIVE (s, f)
1533
    | NECANDSUFF (s, f) -> (AP s)::(f::acc)
1534
  in
1535
  let f = List.fold_left (fun res f -> AND (res, f)) (List.hd fl) (List.tl fl) in
1536
  let tfl = List.fold_left addTBoxD (f :: tboxND) tboxD in
1537
  let (pl,rl) = detVars tfl in
1538
  let ps n s =
1539
    for i = 1 to n do
1540
      output_string file " "
1541
    done;
1542
    output_string file s
1543
  in
1544
  let rec exall n c s i f popt =
1545
    ps n "<owl:Restriction>\n";
1546
    ps (n+1) "<owl:onProperty>\n";
1547
    if i then begin
1548
      ps (n+2) "<rdf:Description>\n";
1549
      ps (n+3) ("<owl:inverseOf rdf:resource=\"#r" ^ s ^ "\"/>\n");
1550
      ps (n+2) "</rdf:Description>\n"
1551
    end 
1552
    else ps (n+2) ("<rdf:Description rdf:about=\"#r" ^ s ^ "\"/>\n");
1553
    ps (n+1) "</owl:onProperty>\n";
1554
    let _ =
1555
      match popt with
1556
      | None -> ()
1557
      | Some (c2, no) ->
1558
          ps (n+1) ("<" ^ c2 ^ " rdf:datatype=\"&xsd;nonNegativeInteger\">\n");
1559
          ps (n+2) ((string_of_int no) ^ "\n");
1560
          ps (n+1) ("</" ^ c2 ^ ">\n")
1561
    in
1562
    ps (n+1) ("<" ^ c ^ ">\n");
1563
    printFormula (n+2) f;
1564
    ps (n+1) ("</" ^ c ^ ">\n");
1565
    ps n "</owl:Restriction>\n";
1566
  and andor n c f1 f2 =
1567
    ps n "<owl:Class>\n";
1568
    ps (n+1) ("<" ^ c ^ " rdf:parseType=\"Collection\">\n");
1569
    printFormula (n+2) f1;
1570
    printFormula (n+2) f2;
1571
    ps (n+1) ("</" ^ c ^ ">\n");
1572
    ps n "</owl:Class>\n";
1573
  and printFormula n f =
1574
    match f with
1575
    | TRUE -> ps n "<rdf:Description rdf:about=\"&owl;Thing\"/>\n";
1576
    | FALSE -> ps n "<rdf:Description rdf:about=\"&owl;Nothing\"/>\n";
1577
    | AP s -> ps n ("<rdf:Description rdf:about=\"#p" ^ s ^ "\"/>\n");
1578
    | NOT f1 -> 
1579
        ps n "<owl:Class>\n";
1580
        ps (n+1) "<owl:complementOf>\n";
1581
        printFormula (n+2) f1;
1582
        ps (n+1) "</owl:complementOf>\n";
1583
        ps n "</owl:Class>\n";
1584
    | EQU (f1, f2) -> printFormula n (AND (OR (NOT f1, f2), OR (NOT f2, f1)))
1585
    | IMP (f1, f2) -> printFormula n (OR (NOT f1, f2))
1586
    | EX (s, i1, f1) -> exall n "owl:someValuesFrom" s i1 f1 None
1587
    | AX (s, i1, f1) -> exall n "owl:allValuesFrom" s i1 f1 None
1588
    | MIN (card, s, i1, f1) ->
1589
        exall n "owl:onClass" s i1 f1 (Some ("owl:minQualifiedCardinality", card))
1590
    | MAX (card, s, i1, f1) ->
1591
        exall n "owl:onClass" s i1 f1 (Some ("owl:maxQualifiedCardinality", card))
1592
    | OR (f1, f2) -> andor n "owl:unionOf" f1 f2
1593
    | AND (f1, f2) -> andor n "owl:intersectionOf" f1 f2
1594
  in
1595
  let printAxiom c1 c2 s f =
1596
    ps 2 ("<rdf:Description " ^ c1 ^ "=\"" ^ s ^ "\">\n");
1597
    ps 3 ("<" ^ c2 ^ ">\n");
1598
    printFormula 4 f;
1599
    ps 3 ("</" ^ c2 ^ ">\n");
1600
    ps 2 "</rdf:Description>\n\n";
1601
  in
1602
  let printTBoxD = function
1603
    | PRIMITIVE (s, f) -> printAxiom "rdf:about" "rdfs:subClassOf" ("#p" ^ s) f
1604
    | NECANDSUFF (s, f) -> printAxiom "rdf:about" "owl:equivalentClass" ("#p" ^ s) f
1605
  in
1606
  let printTBoxND f = printAxiom "rdf:about" "rdfs:subClassOf" "&owl;Thing" f in
1607
  ps 0 "<?xml version=\"1.0\"?>\n\n";
1608
  ps 0 "<!DOCTYPE rdf:RDF [\n";
1609
  ps 5 "<!ENTITY owl \"http://www.w3.org/2002/07/owl#\" >\n";
1610
  ps 5 "<!ENTITY xsd \"http://www.w3.org/2001/XMLSchema#\" >\n";
1611
  (* ps 5 "<!ENTITY rdfs \"http://www.w3.org/2000/01/rdf-schema#\" >\n"; *)
1612
  ps 0 "]>\n\n";
1613
  ps 0 "<rdf:RDF xml:base=\"http://example.com/tmp\"\n";
1614
  ps 1 "xmlns=\"http://example.com/tmp\"\n";
1615
  ps 1 "xmlns:rdf=\"http://www.w3.org/1999/02/22-rdf-syntax-ns#\"\n";
1616
  ps 1 "xmlns:rdfs=\"http://www.w3.org/2000/01/rdf-schema#\"\n";
1617
  ps 1 "xmlns:owl=\"http://www.w3.org/2002/07/owl#\"\n";
1618
  ps 1 "xmlns:xsd=\"http://www.w3.org/2001/XMLSchema#\">\n\n";
1619
  ps 2 "<owl:Ontology rdf:about=\"\"/>\n\n";
1620
  List.iter (fun s -> ps 2 ("<owl:Class rdf:about=\"#p" ^ s ^ "\"/>\n")) pl;
1621
  List.iter (fun s -> ps 2 ("<owl:ObjectProperty rdf:about=\"#r" ^ s ^ "\"/>\n")) rl;
1622
  ps 0 "\n";
1623
  List.iter printTBoxD tboxD;
1624
  List.iter printTBoxND tboxND;
1625
  ps 0 "\n";
1626
  printAxiom "rdf:nodeID" "rdf:type" "_:a" f;
1627
  ps 0 "</rdf:RDF>\n";
1628
  close_out file
1629

    
1630

    
1631
let lexerf = A.make_lexer_file ~comment:"%"
1632
    ["(";")";".";",";"inputformula";"hypothesis";"axiom";"conjecture";
1633
     "-";"~";"&";"|";"=>";"pos";"box";":";"true";"false"] 
1634

    
1635
(** These functions parse a TANCS token stream to obtain a formula.
1636
    It is a standard recursive descent procedure.
1637
    @param ts A token stream.
1638
    @return The resulting (sub-)formula.
1639
    @raise ALCException if ts does not represent a formula.
1640
 *)
1641
let rec parseTancs_equ ts =
1642
  let f1 = parseTancs_imp ts in
1643
  match Stream.peek ts with
1644
  | None -> f1
1645
  | Some (A.Kwd "<=>") ->
1646
      Stream.junk ts;
1647
      let f2 = parseTancs_equ ts in
1648
      EQU (f1, f2)
1649
  | _ -> f1
1650

    
1651
(** These functions parse a TANCS token stream to obtain a formula.
1652
    It is a standard recursive descent procedure.
1653
    @param ts A token stream.
1654
    @return The resulting (sub-)formula.
1655
    @raise ALCException if ts does not represent a formula.
1656
 *)
1657
and parseTancs_imp ts =
1658
  let f1 = parseTancs_or ts in
1659
  match Stream.peek ts with
1660
  | None -> f1
1661
  | Some (A.Kwd "=>") ->
1662
      Stream.junk ts;
1663
      let f2 = parseTancs_imp ts in
1664
      IMP (f1, f2)
1665
  | _ -> f1
1666

    
1667
(** These functions parse a TANCS token stream to obtain a formula.
1668
    It is a standard recursive descent procedure.
1669
    @param ts A token stream.
1670
    @return The resulting (sub-)formula.
1671
    @raise ALCException if ts does not represent a formula.
1672
 *)
1673
and parseTancs_or ts =
1674
  let f1 = parseTancs_and ts in
1675
  match Stream.peek ts with
1676
  | None -> f1
1677
  | Some (A.Kwd "|") ->
1678
      Stream.junk ts;
1679
      let f2 = parseTancs_or ts in
1680
      OR (f1, f2)
1681
  | _ -> f1
1682

    
1683
(** These functions parse a TANCS token stream to obtain a formula.
1684
    It is a standard recursive descent procedure.
1685
    @param ts A token stream.
1686
    @return The resulting (sub-)formula.
1687
    @raise ALCException if ts does not represent a formula.
1688
 *)
1689
and parseTancs_and ts =
1690
  let f1 = parseTancs_rest ts in
1691
  match Stream.peek ts with
1692
  | None -> f1
1693
  | Some (A.Kwd "&") ->
1694
      Stream.junk ts;
1695
      let f2 = parseTancs_and ts in
1696
      AND (f1, f2)
1697
  | _ -> f1
1698

    
1699
(** These functions parse a TANCS token stream to obtain a formula.
1700
    It is a standard recursive descent procedure.
1701
    @param ts A token stream.
1702
    @return The resulting (sub-)formula.
1703
    @raise ALCException if ts does not represent a formula.
1704
 *)
1705
and parseTancs_rest ts =
1706
  let token = Stream.next ts in
1707
  match token with
1708
  | A.Kwd "pos"
1709
  | A.Kwd "box" -> begin
1710
      let s =
1711
        match Stream.peek ts with
1712
        | Some (A.Ident s1) -> Stream.junk ts; s1
1713
        | Some (A.Kwd ":") -> ""
1714
        | Some (A.Kwd "-") -> ""
1715
        | Some t -> A.printError mk_exn ~t ~ts "role name, \"-\", or \":\" expected: "
1716
        | None -> A.printError mk_exn ~ts "role name, \"-\", or \":\" expected: "
1717
      in
1718
      let isInv =
1719
        match Stream.next ts with
1720
        | A.Kwd ":" -> false
1721
        | A.Kwd "-" -> begin
1722
            match Stream.next ts with
1723
            | A.Kwd ":" -> true
1724
            | t -> A.printError mk_exn ~t ~ts "\":\" expected: "
1725
        end
1726
        | t -> A.printError mk_exn ~t ~ts "\":\" or \"-\" expected: "
1727
      in
1728
      let f1 = parseTancs_rest ts in
1729
      match token with
1730
      | A.Kwd "pos" -> EX (s, isInv, f1)
1731
      | _ -> AX (s, isInv, f1)
1732
    end
1733
  | A.Kwd "(" -> 
1734
      let f = parseTancs_equ ts in
1735
      let _ =
1736
        match Stream.next ts with
1737
        | A.Kwd ")" -> ()
1738
        | t -> A.printError mk_exn ~t ~ts "\")\" expected: "
1739
      in
1740
      f
1741
  | A.Kwd "~" ->
1742
      let f = parseTancs_rest ts in
1743
      NOT f
1744
  | A.Kwd "true" -> TRUE
1745
  | A.Kwd "false" -> FALSE
1746
  | A.Ident s -> AP s
1747
  | t -> A.printError mk_exn ~t ~ts 
1748
        "\"pos\", \"box\", \"~\", \"(\", \"true\", \"false\", or <ident> expected: "
1749

    
1750
(** These functions parse a TANCS token stream to obtain a set of clauses.
1751
    It is a standard recursive descent procedure.
1752
    @param ts A token stream.
1753
    @param axl The axioms parsed so far.
1754
    @param hypl The hyptheses parsed so far.
1755
    @param conl The conjectures parsed so far.
1756
    @return A triple (axl, hypl, conl) where
1757
    axl is a list of formula representing axioms;
1758
    hypl is a list of formula representing hypotheses;
1759
    conl is a list of formula representing conjectures;
1760
    @raise ALCException if s does not represent a set of clauses.
1761
 *)
1762
let rec parseTancs_clauses ts axl hypl conl =
1763
  match Stream.peek ts with
1764
  | Some (A.Kwd "inputformula") -> begin
1765
      Stream.junk ts;
1766
      A.getKws mk_exn ts ["("];
1767
      let _ =
1768
        match Stream.next ts with
1769
        | A.Ident s -> s
1770
        | t -> A.printError mk_exn ~t "clause name expected: "
1771
      in
1772
      A.getKws mk_exn ts [","];
1773
      let ty =
1774
        match Stream.next ts with
1775
        | A.Kwd "axiom" -> 1
1776
        | A.Kwd "hypothesis" -> 2
1777
        | A.Kwd "conjecture" -> 3
1778
        | t -> A.printError mk_exn ~t
1779
            "clause type (i.e. \"hypothesis\", \"axiom\", or \"conjecture\") expected: "
1780
      in
1781
      A.getKws mk_exn ts [","];
1782
      let cl = parseTancs_equ ts in
1783
      A.getKws mk_exn ts [")";"."];
1784
      match ty with
1785
      | 1 -> parseTancs_clauses ts (cl::axl) hypl conl
1786
      | 2 -> parseTancs_clauses ts axl (cl::hypl) conl
1787
      | _ -> parseTancs_clauses ts axl hypl (cl::conl) 
1788
    end
1789
  | _ -> (axl, hypl, conl)
1790

    
1791
(** Imports queries in TAMCS2000 style.
1792
    @param filename The name of the input file.
1793
    @return A triple (fl, tboxND, tboxD) where
1794
    fl is a list of formula representing the initial input;
1795
    tboxND is a list of formulae representing
1796
    the non-definitional part of a TBox; and
1797
    tboxD is a list of definitions
1798
    representing the definitional part of a TBox.
1799
    @raise ALCException if s does not represent a formula query.
1800
 *)
1801
let importTancs2000 filename =
1802
  let file = open_in filename in
1803
  let ts = lexerf file in
1804
  try
1805
    begin
1806
      let (axl, hypl, conl) = parseTancs_clauses ts [] [] [] in
1807
      let _ =
1808
        match Stream.peek ts with
1809
        | None -> ()
1810
        | Some _ -> A.printError mk_exn ~ts "EOS expected: "
1811
      in
1812
      assert (conl <> []);
1813
      let conc =
1814
        List.fold_left (fun res f -> OR (res, NOT f)) (NOT (List.hd conl)) (List.tl conl)
1815
      in
1816
      close_in file;
1817
      (conc::hypl, axl, [])
1818
    end
1819
  with Stream.Failure ->
1820
    close_in file;
1821
    A.printError mk_exn ~ts "unexpected EOS"