Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgFormula.ml @ 7c4d2eb4

History | View | Annotate | Download (42.3 KB)

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

    
6

    
7
module HC = HashConsing
8
module A = AltGenlex
9
module L = List
10
module Str = String
11

    
12

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

    
19
(** Indicates the sort of a sorted formula
20
 *)
21
type sort = int
22

    
23
(** Defines (unsorted) coalgebraic formulae.
24
 *)
25
type formula =
26
  | TRUE
27
  | FALSE
28
  | AP of string
29
  | NOT of formula
30
  | AT of string * formula
31
  | OR of formula * formula
32
  | AND of formula * formula
33
  | EQU of formula * formula
34
  | IMP of formula * formula
35
  | EX of string * formula
36
  | AX of string * formula
37
  | ENFORCES of int list * formula
38
  | ALLOWS   of int list * formula
39
  | MIN of int * string * formula
40
  | MAX of int * string * formula
41
  | MORETHAN of int * string * formula (* diamond of GML *)
42
  | MAXEXCEPT of int * string * formula (* box of GML *)
43
  | CHC of formula * formula
44
  | CHCN of formula * formula
45
  | FUS of bool * formula
46

    
47
(** Defines sorted coalgebraic formulae.
48
 *)
49
type sortedFormula = sort * formula
50

    
51

    
52
(** Determines whether a name indicates a nominal.
53
    @param A string s.
54
    @return True iff s contains a prime character.
55
 *)
56
let isNominal s = String.contains s '\''
57

    
58

    
59
(** Determines the size of a formula.
60
    @param f A formula.
61
    @return The size of f.
62
 *)
63
let rec sizeFormula f =
64
  match f with
65
  | TRUE 
66
  | FALSE 
67
  | AP _ -> 1
68
  | NOT f1
69
  | AT (_, f1) -> succ (sizeFormula f1)
70
  | OR (f1, f2)  
71
  | AND (f1, f2)
72
  | EQU (f1, f2) 
73
  | IMP (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
74
  | EX (_, f1)
75
  | AX (_, f1)
76
  | ENFORCES (_, f1)
77
  | ALLOWS (_, f1) -> succ (sizeFormula f1)
78
  | MIN (_, _, f1)
79
  | MAX (_, _, f1)
80
  | MORETHAN (_, _, f1)
81
  | MAXEXCEPT (_, _, f1) -> succ (sizeFormula f1)
82
  | CHC (f1, f2)
83
  | CHCN (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
84
  | FUS (_, f1) -> succ (sizeFormula f1)
85

    
86
(** Determines the size of a sorted formula.
87
    @param f A sorted formula.
88
    @return The size of f.
89
 *)
90
let sizeSortedFormula f = sizeFormula (snd f)
91

    
92

    
93
(** Appends a string representation of a formula to a string buffer.
94
    Parentheses are ommited where possible
95
    where the preference rules are defined as usual.
96
    @param sb A string buffer.
97
    @param f A formula.
98
 *)
99
let rec exportFormula_buffer sb f =
100
  let negate = function
101
    | NOT f -> f
102
    | f -> NOT f
103
  in
104
  let prio n lf =
105
    let prionr = function
106
      | EQU _ -> 0
107
      | IMP _  -> 1 
108
      | OR _ -> 2
109
      | AND _ -> 3
110
      | _ -> 4
111
    in
112
    if prionr lf < n then begin
113
      Buffer.add_char sb '(';
114
      exportFormula_buffer sb lf;
115
      Buffer.add_char sb ')'
116
    end
117
    else exportFormula_buffer sb lf
118
  in
119
  match f with
120
  | TRUE -> Buffer.add_string sb "True"
121
  | FALSE -> Buffer.add_string sb "False"
122
  | AP s -> Buffer.add_string sb s
123
  | NOT f1 ->
124
      Buffer.add_string sb "~";
125
      prio 4 f1
126
  | AT (s, f1) ->
127
      Buffer.add_string sb "@ ";
128
      Buffer.add_string sb s;
129
      Buffer.add_string sb " ";
130
      prio 4 f1
131
  | OR (f1, f2) ->
132
      prio 2 f1;
133
      Buffer.add_string sb " | ";
134
      prio 2 f2
135
  | AND (f1, f2) ->
136
      prio 3 f1;
137
      Buffer.add_string sb " & ";
138
      prio 3 f2
139
  | EQU (f1, f2) ->
140
      prio 0 f1;
141
      Buffer.add_string sb " <=> ";
142
      prio 0 f2
143
  | IMP (f1, f2) ->
144
      prio 2 f1;
145
      Buffer.add_string sb " => ";
146
      prio 2 f2
147
  | EX (s, f1) ->
148
      Buffer.add_string sb "<";
149
      Buffer.add_string sb s;
150
      Buffer.add_string sb ">";
151
      prio 4 f1
152
  | AX (s, f1) ->
153
      Buffer.add_string sb "[";
154
      Buffer.add_string sb s;
155
      Buffer.add_string sb "]";
156
      prio 4 f1
157
  | ALLOWS (s, f1) ->
158
      Buffer.add_string sb "<{";
159
      Buffer.add_string sb (
160
          match s with
161
          | [] -> " "
162
          | _ ->(Str.concat " " (L.map string_of_int s))
163
      );
164
      Buffer.add_string sb "}>";
165
      prio 4 f1
166
  | ENFORCES (s, f1) ->
167
      Buffer.add_string sb "[{";
168
      Buffer.add_string sb (
169
          match s with
170
          | [] -> " "
171
          | _ ->(Str.concat " " (L.map string_of_int s))
172
      );
173
      Buffer.add_string sb "}]";
174
      prio 4 f1
175
  | MIN (n, s, f1) ->
176
      Buffer.add_string sb "{>=";
177
      Buffer.add_string sb (string_of_int n);
178
      Buffer.add_string sb " ";
179
      Buffer.add_string sb s;
180
      Buffer.add_string sb "}";
181
      prio 4 f1
182
  | MAX (n, s, f1) ->
183
      Buffer.add_string sb "{<=";
184
      Buffer.add_string sb (string_of_int n);
185
      Buffer.add_string sb " ";
186
      Buffer.add_string sb s;
187
      Buffer.add_string sb "}";
188
      prio 4 f1
189
  | MORETHAN (n, s, f1) ->
190
      Buffer.add_string sb "{>";
191
      Buffer.add_string sb (string_of_int n);
192
      Buffer.add_string sb " ";
193
      Buffer.add_string sb s;
194
      Buffer.add_string sb "}";
195
      prio 4 f1
196
  | MAXEXCEPT (n, s, f1) ->
197
      Buffer.add_string sb "{<=";
198
      Buffer.add_string sb (string_of_int n);
199
      Buffer.add_string sb " ~ ";
200
      Buffer.add_string sb s;
201
      Buffer.add_string sb "}";
202
      prio 4 f1 (* actually is prio of ~ and not of <= *)
203
  | CHC (f1, f2) ->
204
      Buffer.add_string sb "(";
205
      exportFormula_buffer sb f1;
206
      Buffer.add_string sb " + ";
207
      exportFormula_buffer sb f2;
208
      Buffer.add_string sb ")"
209
  | CHCN (f1, f2) ->
210
      Buffer.add_string sb "~(";
211
      exportFormula_buffer sb (negate f1);
212
      Buffer.add_string sb " + ";
213
      exportFormula_buffer sb (negate f2);
214
      Buffer.add_string sb ")"
215
  | FUS (first, f1) ->
216
      Buffer.add_string sb (if first then "[pi1]" else "[pi2]");
217
      prio 4 f1
218

    
219
(** Converts a formula into a string representation.
220
    Parentheses are ommited where possible
221
    where the preference rules are defined as usual.
222
    @param f A formula.
223
    @return A string representing f.
224
 *)
225
let exportFormula f =
226
  let sb = Buffer.create 128 in
227
  exportFormula_buffer sb f;
228
  Buffer.contents sb
229

    
230
(** export (CL)-formula suitable for tatl-inputs *)
231
let rec exportTatlFormula_buffer sb f =
232
  let negate = function
233
    | NOT f -> f
234
    | f -> NOT f
235
  in
236
  let prio n lf =
237
    let prionr = function
238
      | EQU _ -> 0
239
      | IMP _  -> 1 
240
      | OR _ -> 2
241
      | AND _ -> 3
242
      | _ -> 4
243
    in
244
    if prionr lf < n then begin
245
      Buffer.add_char sb '(';
246
      exportTatlFormula_buffer sb lf;
247
      Buffer.add_char sb ')'
248
    end
249
    else exportTatlFormula_buffer sb lf
250
  in
251
  match f with
252
  | TRUE -> Buffer.add_string sb "(p \\/ ~p)"
253
  | FALSE -> Buffer.add_string sb "(p /\\ ~p)"
254
  | AP s -> Buffer.add_string sb s
255
  | NOT f1 ->
256
      Buffer.add_string sb "~";
257
      prio 4 f1
258
  | OR (f1, f2) ->
259
      prio 2 f1;
260
      Buffer.add_string sb " \\/ ";
261
      prio 2 f2
262
  | AND (f1, f2) ->
263
      prio 3 f1;
264
      Buffer.add_string sb " /\\ ";
265
      prio 3 f2
266
  | EQU (f1, f2) ->
267
      prio 0 (AND (IMP (f1,f2), IMP (f2,f1)))
268
  | IMP (f1, f2) ->
269
      prio 2 f1;
270
      Buffer.add_string sb " -> ";
271
      prio 2 f2
272
  | ALLOWS (s, f1) ->
273
      Buffer.add_string sb "<<";
274
      Buffer.add_string sb (
275
          match s with
276
          | [] -> " "
277
          | _ ->(Str.concat "," (L.map string_of_int s))
278
      );
279
      Buffer.add_string sb ">>X ";
280
      prio 4 f1
281
  | ENFORCES (s, f1) ->
282
      Buffer.add_string sb "~<<";
283
      Buffer.add_string sb (
284
          match s with
285
          | [] -> " "
286
          | _ ->(Str.concat "," (L.map string_of_int s))
287
      );
288
      Buffer.add_string sb ">>X ~ ";
289
      prio 4 f1
290
  | EX _
291
  | AX _
292
  | MIN _
293
  | MAX _
294
  | MORETHAN _
295
  | MAXEXCEPT _
296
  | AT _
297
  | CHC _
298
  | CHCN _
299
  | FUS _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
300

    
301
let exportTatlFormula f =
302
  let sb = Buffer.create 128 in
303
  exportTatlFormula_buffer sb f;
304
  Buffer.contents sb
305

    
306
(** Appends a string representation of a sorted formula to a string buffer.
307
    Parentheses are ommited where possible
308
    where the preference rules are defined as usual.
309
    @param sb A string buffer.
310
    @param (s, f) A sorted formula.
311
 *)
312
let rec exportSortedFormula_buffer sb (s, f) =
313
  Buffer.add_string sb (string_of_int s);
314
  Buffer.add_string sb ": ";
315
  exportFormula_buffer sb f
316

    
317
(** Converts a sorted formula into a string representation.
318
    Parentheses are ommited where possible
319
    where the preference rules are defined as usual.
320
    @param f A sorted formula.
321
    @return A string representing f.
322
 *)
323
let exportSortedFormula f =
324
  let sb = Buffer.create 128 in
325
  exportSortedFormula_buffer sb f;
326
  Buffer.contents sb
327

    
328
(** Converts a (sorted) formula query into a string representation.
329
    @param tbox A list of sorted formulae representing a TBox.
330
    @param f A sorted formula.
331
    @return A string representing tbox |- f.
332
 *)
333
let exportQuery tbox f =
334
  let sb = Buffer.create 1000 in
335
  let rec expFl = function
336
    | [] -> ()
337
    | h::tl ->
338
        exportSortedFormula_buffer sb h;
339
        if tl <> [] then Buffer.add_string sb "; " else ();
340
        expFl tl
341
  in
342
  expFl tbox;
343
  Buffer.add_string sb "  |-  ";
344
  exportSortedFormula_buffer sb f;
345
  Buffer.contents sb
346

    
347
(** Converts a (sorted) formula query into a string representation. Such that
348
    coalg can read it again using importQuery
349
    @param tbox A list of sorted formulae representing a TBox.
350
    @param f A sorted formula.
351
    @return A string representing tbox |- f.
352
 *)
353
let exportQueryParsable tbox (_,f) =
354
  let sb = Buffer.create 1000 in
355
  let rec expFl = function
356
    | [] -> ()
357
    | (_,h)::tl ->
358
        exportFormula_buffer sb h;
359
        if tl <> [] then Buffer.add_string sb "; " else ();
360
        expFl tl
361
  in
362
  expFl tbox;
363
  Buffer.add_string sb "  |-  ";
364
  exportFormula_buffer sb f;
365
  Buffer.contents sb
366

    
367

    
368
let lexer = A.make_lexer 
369
    [":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]"
370
    ;"[{";"}]";"<{";"}>";","
371
    ] 
372

    
373
let mk_exn s = CoAlgException s
374

    
375
(** These functions parse a token stream to obtain a formula.
376
    It is a standard recursive descent procedure.
377
    @param ts A token stream.
378
    @return The resulting (sub-)formula.
379
    @raise CoAlgException if ts does not represent a formula.
380
 *)
381
let rec parse_formula ts =
382
  let f1 = parse_imp ts in
383
  match Stream.peek ts with
384
  | None -> f1
385
  | Some (A.Kwd "<=>") ->
386
      Stream.junk ts;
387
      let f2 = parse_formula ts in
388
      EQU (f1, f2)
389
  | _ -> f1
390

    
391
(** These functions parse a token stream to obtain a formula.
392
    It is a standard recursive descent procedure.
393
    @param ts A token stream.
394
    @return The resulting (sub-)formula.
395
    @raise CoAlgException if ts does not represent a formula.
396
 *)
397
and parse_imp ts =
398
  let f1 = parse_or ts in
399
  match Stream.peek ts with
400
  | None -> f1
401
  | Some (A.Kwd "=>") ->
402
      Stream.junk ts;
403
      let f2 = parse_imp ts in
404
      IMP (f1, f2)
405
  | _ -> f1
406

    
407
(** These functions parse a token stream to obtain a formula.
408
    It is a standard recursive descent procedure.
409
    @param ts A token stream.
410
    @return The resulting (sub-)formula.
411
    @raise CoAlgException if ts does not represent a formula.
412
 *)
413
and parse_or ts =
414
  let f1 = parse_and ts in
415
  match Stream.peek ts with
416
  | None -> f1
417
  | Some (A.Kwd "|") ->
418
      Stream.junk ts;
419
      let f2 = parse_or ts in
420
      OR (f1, f2)
421
  | _ -> f1
422

    
423
(** These functions parse a token stream to obtain a formula.
424
    It is a standard recursive descent procedure.
425
    @param ts A token stream.
426
    @return The resulting (sub-)formula.
427
    @raise CoAlgException if ts does not represent a formula.
428
 *)
429
and parse_and ts =
430
  let f1 = parse_rest ts in
431
  match Stream.peek ts with
432
  | None -> f1
433
  | Some (A.Kwd "&") ->
434
      Stream.junk ts;
435
      let f2 = parse_and ts in
436
      AND (f1, f2)
437
  | _ -> f1
438

    
439
(** These functions parse a token stream to obtain a formula.
440
    It is a standard recursive descent procedure.
441
    @param ts A token stream.
442
    @return The resulting (sub-)formula.
443
    @raise CoAlgException if ts does not represent a formula.
444
 *)
445
and parse_rest ts =
446
  let boxinternals noNo es =
447
    let n =
448
      if noNo then 0
449
      else
450
        match Stream.next ts with
451
        | A.Int n when n >= 0 -> n
452
        | t -> A.printError mk_exn ~t ~ts "<non-negative number> expected: "
453
    in
454
    let s =
455
      match Stream.peek ts with
456
      | Some (A.Ident s1) -> Stream.junk ts; s1
457
      | Some (A.Kwd c) when c = es -> ""
458
      | _ -> A.printError mk_exn ~ts ("role name or \"" ^ es ^ "\" expected: ")
459
    in
460
    let _ =
461
      match Stream.next ts with
462
      | A.Kwd c when c = es -> ()
463
      | t -> A.printError mk_exn ~t ~ts ("\"" ^ es ^ "\" expected: ")
464
    in
465
    (n, s)
466
  in
467
  let rec agentlist es =
468
    let allAgents = CoolUtils.cl_get_agents () in
469
    match Stream.next ts with
470
    | A.Int n -> if CoolUtils.TArray.elem n allAgents
471
                 then n::(agentlist es)
472
                 else A.printError mk_exn ~ts ("agent name \"" ^ (string_of_int n) ^ "\" unknonwn, see --agents: ")
473
    | A.Kwd c when c = es -> []
474
    | _ -> A.printError mk_exn ~ts ("agent name or " ^ es ^ "\" expected: ")
475
  in
476
  match Stream.next ts with
477
  | A.Kwd "True" -> TRUE
478
  | A.Kwd "False" -> FALSE
479
  | A.Ident s -> AP s
480
  | A.Kwd "~" ->
481
      let f = parse_rest ts in
482
      NOT f
483
  | A.Kwd "@" ->
484
      let s =
485
        match Stream.next ts with
486
        | A.Ident s when isNominal s -> s
487
        | t -> A.printError mk_exn ~t ~ts ("nominal expected: ")
488
      in
489
      let f = parse_rest ts in
490
      AT (s, f)
491
  | A.Kwd "<" -> 
492
      let (_, s) = boxinternals true ">" in
493
      let f1 = parse_rest ts in
494
      EX (s, f1) 
495
  | A.Kwd "[" -> 
496
      let (_, s) = boxinternals true "]" in
497
      let f1 = parse_rest ts in
498
      AX (s, f1)
499
  | A.Kwd "[{" -> 
500
      let ls = agentlist "}]" in
501
      let f1 = parse_rest ts in
502
      ENFORCES (ls, f1)
503
  | A.Kwd "<{" -> 
504
      let ls = agentlist "}>" in
505
      let f1 = parse_rest ts in
506
      ALLOWS (ls, f1)
507
  | A.Kwd "{>=" -> 
508
      let (n, s) = boxinternals false "}" in
509
      let f1 = parse_rest ts in
510
      MIN (n, s, f1)
511
  | A.Kwd "{<=" -> 
512
      let (n, s) = boxinternals false "}" in
513
      let f1 = parse_rest ts in
514
      MAX (n, s, f1)
515
  | A.Kwd "(" -> begin
516
      let f = parse_formula ts in
517
      match Stream.next ts with
518
      | A.Kwd ")" -> f
519
      | A.Kwd "+" -> begin
520
          let f2 = parse_formula ts in
521
          match Stream.next ts with
522
          | A.Kwd ")" -> CHC (f, f2)
523
          | t -> A.printError mk_exn ~t ~ts "\")\" expected: "
524
        end
525
      | t -> A.printError mk_exn ~t ~ts "\")\" or \"+\" expected: "
526
    end
527
  | A.Kwd "[pi1]" ->
528
      let f = parse_rest ts in
529
      FUS (true, f)
530
  | A.Kwd "[pi2]" ->
531
      let f = parse_rest ts in
532
      FUS (false, f)
533
  | t -> A.printError mk_exn ~t ~ts 
534
      "\"<\", \"[\", \"{>=\", \"{<=\", \"@\", \"~\", \"(\", \"True\", \"False\", or <ident> expected: "
535
        
536
(** Parses a sorted formula.
537
    @param ts A token stream.
538
    @return A sorted formula.
539
    @raise CoAlgException If ts does not represent a sorted formula.
540
 *)
541
let parse_sortedFormula ts =
542
  let nr = 
543
    match Stream.peek ts with
544
    | Some (A.Int n) ->
545
        if n >= 0 then begin
546
          Stream.junk ts;
547
          let () =
548
            match Stream.next ts with
549
            | A.Kwd ":" -> ()
550
            | t -> A.printError mk_exn ~t ~ts ("\":\" expected: ")
551
          in
552
          n
553
        end else
554
          A.printError mk_exn ~ts ("<non-negative number> expected: ")
555
    | _ -> 0 
556
  in
557
  let f = parse_formula ts in
558
  (nr, f)
559

    
560
(** Parses a list of sorted formulae separated by ";".
561
    @param ts A token stream.
562
    @param acc The list of sorted formulae parsed so far.
563
    @return The resulting list of sorted formula.
564
    @raise CoAlgException if ts does not represent a list of sorted formulae.
565
 *)
566
let rec parse_sortedFormulaList ts acc =
567
  let f1 = parse_sortedFormula ts in
568
  match Stream.peek ts with
569
  | Some (A.Kwd ";") ->
570
      Stream.junk ts;
571
      parse_sortedFormulaList ts (f1::acc)
572
  | _ -> List.rev (f1::acc)
573

    
574
(** A common wrapper for import functions.
575
    @param fkt An import function.
576
    @param s A string.
577
    @return The object imported from s using fkt.
578
    @raise CoAlgException If ts is not empty.
579
 *)
580
let importWrapper fkt s =
581
  let ts = lexer s in
582
  try
583
    let res = fkt ts in
584
    let _ =
585
      match Stream.peek ts with
586
      | None -> ()
587
      | Some _ -> A.printError mk_exn ~ts "EOS expected: "
588
    in
589
    res
590
  with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS"
591

    
592
(** Parses a string to obtain a formula.
593
    @param s A string representing a formula.
594
    @return The resulting formula.
595
    @raise CoAlgException if s does not represent a formula.
596
 *)
597
let importFormula s = importWrapper parse_formula s
598

    
599
(** Parses a string to obtain a sorted formula.
600
    @param s A string representing a sorted formula.
601
    @return The sorted formula.
602
    @raise CoAlgException If s does not represent a sorted formula.
603
 *)
604
let importSortedFormula s = importWrapper parse_sortedFormula s
605

    
606
(** Parses a string to obtain a (sorted) formula query.
607
    @param s A string representing a formula query.
608
    @return A pair (tbox, f) where
609
    tbox is a list of sorted formulae representing the TBox; and
610
    f is a sorted formula.
611
    @raise CoAlgException if s does not represent a formula query.
612
 *)
613
let importQuery s =
614
  let fkt ts =
615
    match Stream.peek ts with
616
    | Some (A.Kwd "|-") ->
617
        Stream.junk ts;
618
        let f = parse_sortedFormula ts in
619
        ([], f)
620
    | _ ->
621
        let fl = parse_sortedFormulaList ts [] in
622
        match Stream.peek ts with
623
        | Some (A.Kwd "|-") ->
624
            Stream.junk ts;
625
            let f = parse_sortedFormula ts in
626
            (fl, f)
627
        | _ -> 
628
            if List.length fl = 1 then ([], List.hd fl)
629
            else A.printError mk_exn ~ts "\"|-\" expected: "
630
  in
631
  importWrapper fkt s
632

    
633

    
634
(** Converts the negation of a formula to negation normal form
635
    by "pushing in" the negations "~".
636
    The symbols "<=>" and "=>" are substituted by their usual definitions.
637
    @param f A formula.
638
    @return A formula in negation normal form and not containing "<=>" or "=>"
639
    that is equivalent to ~f.
640
 *)
641
let rec nnfNeg f =
642
  match f with
643
  | TRUE -> FALSE
644
  | FALSE -> TRUE
645
  | AP _ -> NOT f
646
  | NOT f1 -> nnf f1
647
  | AT (s, f1) -> AT (s, nnfNeg f1)
648
  | OR (f1, f2) -> AND (nnfNeg f1, nnfNeg f2)
649
  | AND (f1, f2) -> OR (nnfNeg f1, nnfNeg f2)
650
  | EQU (f1, f2) -> OR (AND (nnf f1, nnfNeg f2), AND (nnf f2, nnfNeg f1))
651
  | IMP (f1, f2) -> AND (nnf f1, nnfNeg f2)
652
  | EX (s, f1) -> AX (s, nnfNeg f1)
653
  | AX (s, f1) -> EX (s, nnfNeg f1)
654
  | ENFORCES (s, f1) -> ALLOWS (s, nnfNeg f1)
655
  | ALLOWS (s, f1) -> ENFORCES (s, nnfNeg f1)
656
  | MIN (n, s, f1) -> if n = 0 then FALSE else MAXEXCEPT (n-1, s, nnfNeg f1)
657
  | MAX (n, s, f1) -> MORETHAN (n, s, nnf f1)
658
  | MORETHAN (n, s, f1) -> MAXEXCEPT (n, s, nnfNeg f1)
659
  | MAXEXCEPT (n, s, f1) -> MORETHAN (n, s, nnfNeg f1)
660
  | CHC (f1, f2) -> CHCN (nnfNeg f1, nnfNeg f2)  
661
  | CHCN (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)  
662
  | FUS (first, f1) -> FUS (first, nnfNeg f1)
663
      
664
(** Converts a formula to negation normal form
665
    by "pushing in" the negations "~".
666
    The symbols "<=>" and "=>" are substituted by their usual definitions.
667
    @param f A formula.
668
    @return A formula in negation normal form and not containing "<=>" or "=>"
669
    that is equivalent to f.
670
 *)
671
and nnf f =
672
  match f with
673
  | TRUE
674
  | FALSE
675
  | AP _
676
  | NOT (AP _) -> f
677
  | NOT f1 -> nnfNeg f1
678
  | AT (s, f1) ->
679
      let ft1 = nnf f1 in
680
      if ft1 == f1 then f else AT (s, ft1)
681
  | OR (f1, f2) ->
682
      let ft1 = nnf f1 in
683
      let ft2 = nnf f2 in
684
      if ft1 == f1 && ft2 == f2 then f else OR (ft1, ft2)
685
  | AND (f1, f2) ->
686
      let ft1 = nnf f1 in
687
      let ft2 = nnf f2 in
688
      if ft1 == f1 && ft2 == f2 then f else AND (ft1, ft2)
689
  | EQU (f1, f2) -> AND (OR (nnfNeg f1, nnf f2), OR (nnfNeg f2, nnf f1))
690
  | IMP (f1, f2) -> OR (nnfNeg f1, nnf f2)
691
  | EX (s, f1) -> 
692
      let ft = nnf f1 in
693
      if ft == f1 then f else EX (s, ft)
694
  | AX (s, f1) ->
695
      let ft = nnf f1 in
696
      if ft == f1 then f else AX (s, ft)
697
  | ENFORCES (s, f1) -> 
698
      let ft = nnf f1 in
699
      if ft == f1 then f else ENFORCES (s, ft)
700
  | ALLOWS (s, f1) ->
701
      let ft = nnf f1 in
702
      if ft == f1 then f else ALLOWS (s, ft)
703
  | MIN (n, s, f1) ->
704
      if n = 0 then TRUE
705
      else
706
        let ft = nnf f1 in
707
        MORETHAN (n-1,s,ft)
708
  | MAX (n, s, f1) ->
709
      let ft = nnfNeg f1 in
710
      MAXEXCEPT (n,s, ft)
711
  | MORETHAN (n,s,f1) ->
712
      let ft = nnf f1 in
713
      if ft = f1 then f else MORETHAN (n,s,ft)
714
  | MAXEXCEPT (n,s,f1) ->
715
      let ft = nnf f1 in
716
      if ft = f1 then f else MAXEXCEPT (n,s,ft)
717
  | CHC (f1, f2) ->
718
      let ft1 = nnf f1 in
719
      let ft2 = nnf f2 in
720
      if ft1 == f1 && ft2 == f2 then f else CHC (ft1, ft2)
721
  | CHCN (f1, f2) ->
722
      let ft1 = nnf f1 in
723
      let ft2 = nnf f2 in
724
      if ft1 == f1 && ft2 == f2 then f else CHCN (ft1, ft2)
725
  | FUS (first, f1) ->
726
      let ft = nnf f1 in
727
      if ft == f1 then f else FUS (first, ft)
728

    
729

    
730
(** Simplifies a formula.
731
    @param f A formula which must be in negation normal form.
732
    @return A formula in negation normal form that is equivalent to f.
733
    @raise CoAlgException if f is not in negation normal form.
734
 *)
735
let rec simplify f =
736
  match f with
737
  | TRUE
738
  | FALSE
739
  | AP _
740
  | NOT (AP _) -> f
741
  | AT (s, f1) ->
742
      let ft = simplify f1 in
743
      begin
744
        match ft with
745
        | FALSE -> FALSE
746
        | TRUE -> TRUE
747
        | AT _ -> ft
748
        | AP s1 when s = s1 -> TRUE
749
        | NOT (AP s1) when s = s1 -> FALSE
750
        | _ -> if ft == f1 then f else AT (s, ft)
751
      end
752
  | OR (f1, f2) ->
753
      let ft1 = simplify f1 in
754
      let ft2 = simplify f2 in
755
      begin
756
        match ft1, ft2 with
757
        | TRUE, _ -> TRUE
758
        | FALSE, _ -> ft2
759
        | _, TRUE -> TRUE
760
        | _, FALSE -> ft1
761
        | _, _ ->
762
            if (f1 == ft1) && (f2 == ft2) then f 
763
            else OR (ft1, ft2)
764
      end
765
  | AND (f1, f2) ->
766
      let ft1 = simplify f1 in
767
      let ft2 = simplify f2 in
768
      begin
769
        match ft1, ft2 with
770
        | TRUE, _ -> ft2
771
        | FALSE, _ -> FALSE
772
        | _, TRUE -> ft1
773
        | _, FALSE -> FALSE
774
        | _, _ ->
775
            if (f1 == ft1) && (f2 == ft2) then f 
776
            else AND (ft1, ft2)
777
      end
778
  | NOT _
779
  | EQU _
780
  | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.")
781
  | EX (s, f1) ->
782
      let ft = simplify f1 in
783
      begin
784
        match ft with
785
        | FALSE -> FALSE
786
        | _ -> if ft == f1 then f else EX (s, ft)
787
      end
788
  | AX (s, f1) ->
789
      let ft = simplify f1 in
790
      begin
791
        match ft with
792
        | TRUE -> TRUE
793
        | _ -> if ft == f1 then f else AX (s, ft)
794
      end
795
  | ENFORCES (s, f1) ->
796
      let ft = simplify f1 in
797
      begin
798
        match ft with
799
        (* Simplification rules are checked with dirks Generic.hs
800
        let enforce ls = M (C ls)
801
        let allow   ls = Neg . M (C ls) . Neg
802
        provable $ F <-> enforce [1,2] F
803
        *)
804
        | TRUE -> TRUE
805
        | FALSE -> FALSE
806
        | _ -> if ft == f1 then f else ENFORCES (s, ft)
807
      end
808
  | ALLOWS (s, f1) ->
809
      let ft = simplify f1 in
810
      begin
811
        match ft with
812
        (* Simplification rules are checked with dirks Generic.hs
813
        let enforce ls = M (C ls)
814
        let allow   ls = Neg . M (C ls) . Neg
815
        provable $ F <-> enforce [1,2] F
816
        *)
817
        | TRUE -> TRUE
818
        | FALSE -> FALSE
819
        | _ -> if ft == f1 then f else ALLOWS (s, ft)
820
      end
821
  | MIN (n, s, f1) ->
822
      if n = 0 then TRUE
823
      else
824
        let ft = simplify f1 in
825
        begin
826
          match ft with
827
          | FALSE -> FALSE
828
          | _ -> if ft == f1 then f else MIN (n, s, ft)
829
        end
830
  | MORETHAN (n,s,f1) ->
831
      let ft = simplify f1 in
832
      if ft == f1 then f else MORETHAN (n,s,ft)
833
  | MAXEXCEPT (n,s,f1) ->
834
      let ft = simplify f1 in
835
      if ft == f1 then f else MAXEXCEPT (n,s,ft)
836
  | MAX (n, s, f1) ->
837
      let ft = simplify f1 in
838
      begin
839
        match ft with
840
        | FALSE -> TRUE
841
        | _ -> if ft == f1 then f else MAX (n, s, ft)
842
      end
843
  | CHC (f1, f2) ->
844
      let ft1 = simplify f1 in
845
      let ft2 = simplify f2 in
846
      begin
847
        match ft1, ft2 with
848
        | TRUE, TRUE -> TRUE
849
        | FALSE, FALSE -> FALSE
850
        | _, _ ->
851
            if (f1 == ft1) && (f2 == ft2) then f 
852
            else CHC (ft1, ft2)
853
      end
854
  | CHCN (f1, f2) ->
855
      let ft1 = simplify f1 in
856
      let ft2 = simplify f2 in
857
      begin
858
        match ft1, ft2 with
859
        | TRUE, TRUE -> TRUE
860
        | FALSE, FALSE -> FALSE
861
        | _, _ ->
862
            if (f1 == ft1) && (f2 == ft2) then f 
863
            else CHCN (ft1, ft2)
864
      end
865
  | FUS (first, f1) ->
866
      let ft = simplify f1 in
867
      begin
868
        match ft with
869
        | FALSE -> FALSE
870
        | TRUE -> TRUE
871
        | _ -> if ft == f1 then f else FUS (first, ft)
872
      end
873

    
874

    
875
(** Destructs an atomic proposition.
876
    @param f An atomic proposition.
877
    @return The name of the atomic proposition.
878
    @raise CoAlgException if f is not an atomic proposition.
879
 *)
880
let dest_ap f =
881
  match f with
882
  | AP s when not (isNominal s) -> s
883
  | _ -> raise (CoAlgException "Formula is not an atomic proposition.")
884

    
885
(** Destructs a nominal.
886
    @param f A nominal.
887
    @return The name of the nominal
888
    @raise CoAlgException if f is not a nominal.
889
 *)
890
let dest_nom f =
891
  match f with
892
  | AP s when isNominal s -> s
893
  | _ -> raise (CoAlgException "Formula is not a nominal.")
894

    
895
(** Destructs a negation.
896
    @param f A negation.
897
    @return The immediate subformula of the negation.
898
    @raise CoAlgException if f is not a negation.
899
 *)
900
let dest_not f =
901
  match f with
902
  | NOT f1 -> f1
903
  | _ -> raise (CoAlgException "Formula is not a negation.")
904

    
905
(** Destructs an @-formula.
906
    @param f An @-formula.
907
    @return The name of the nominal and the immediate subformula of the @-formula.
908
    @raise CoAlgException if f is not an @-formula.
909
 *)
910
let dest_at f =
911
  match f with
912
  | AT (s, f1) -> (s, f1)
913
  | _ -> raise (CoAlgException "Formula is not an @-formula.")
914

    
915
(** Destructs an or-formula.
916
    @param f An or-formula.
917
    @return The two immediate subformulae of the or-formula.
918
    @raise CoAlgException if f is not an or-formula.
919
 *)
920
let dest_or f =
921
  match f with
922
  | OR (f1, f2) -> (f1, f2)
923
  | _ -> raise (CoAlgException "Formula is not an or-formula.")
924

    
925
(** Destructs an and-formula.
926
    @param f An and-formula.
927
    @return The two immediate subformulae of the and-formula.
928
    @raise CoAlgException if f is not an and-formula.
929
 *)
930
let dest_and f =
931
  match f with
932
  | AND (f1, f2) -> (f1, f2)
933
  | _ -> raise (CoAlgException "Formula is not an and-formula.")
934

    
935
(** Destructs an equivalence.
936
    @param f An equivalence.
937
    @return The two immediate subformulae of the equivalence.
938
    @raise CoAlgException if f is not an equivalence.
939
 *)
940
let dest_equ f =
941
  match f with
942
  | EQU (f1, f2) -> (f1, f2)
943
  | _ -> raise (CoAlgException "Formula is not an equivalence.")
944

    
945
(** Destructs an implication.
946
    @param f An implication.
947
    @return The two immediate subformulae of the implication.
948
    @raise CoAlgException if f is not an implication.
949
 *)
950
let dest_imp f =
951
  match f with
952
  | IMP (f1, f2) -> (f1, f2)
953
  | _ -> raise (CoAlgException "Formula is not an implication.")
954

    
955
(** Destructs an EX-formula.
956
    @param f An EX-formula.
957
    @return The role name and the immediate subformula of the EX-formula.
958
    @raise CoAlgException if f is not an EX-formula.
959
 *)
960
let dest_ex f =
961
  match f with
962
  | EX (s, f1) -> (s, f1)
963
  | _ -> raise (CoAlgException "Formula is not an EX-formula.")
964

    
965
(** Destructs an AX-formula.
966
    @param f An AX-formula.
967
    @return The role name and the immediate subformula of the AX-formula.
968
    @raise CoAlgException if f is not an AX-formula.
969
 *)
970
let dest_ax f =
971
  match f with
972
  | AX (s, f1) -> (s, f1)
973
  | _ -> raise (CoAlgException "Formula is not an AX-formula.")
974

    
975
(** Destructs a MIN-formula.
976
    @param f A MIN-formula.
977
    @return The number restriction, role name,
978
    and the immediate subformula of the MIN-formula.
979
    @raise CoAlgException if f is not a MIN-formula.
980
 *)
981
let dest_min f =
982
  match f with
983
  | MIN (n, s, f1) -> (n, s, f1)
984
  | _ -> raise (CoAlgException "Formula is not a MIN-formula.")
985

    
986
(** Destructs a MAX-formula.
987
    @param f A MAX-formula.
988
    @return The number restriction, role name,
989
    and the immediate subformula of the MAX-formula.
990
    @raise CoAlgException if f is not a MAX-formula.
991
 *)
992
let dest_max f =
993
  match f with
994
  | MAX (n, s, f1) -> (n, s, f1)
995
  | _ -> raise (CoAlgException "Formula is not a MAX-formula.")
996

    
997
(** Destructs a choice formula.
998
    @param f A choice formula.
999
    @return The two immediate subformulae of the choice formula.
1000
    @raise CoAlgException if f is not a choice formula.
1001
 *)
1002
let dest_choice f =
1003
  match f with
1004
  | CHC (f1, f2) -> (f1, f2)
1005
  | _ -> raise (CoAlgException "Formula is not a choice formula.")
1006

    
1007
(** Destructs a fusion formula.
1008
    @param f A fusion formula.
1009
    @return A pair (first, f1) where
1010
    first is true iff f is a first projection; and
1011
    f1 is the immediate subformulae of f.
1012
    @raise CoAlgException if f is not a fusion formula.
1013
 *)
1014
let dest_fusion f =
1015
  match f with
1016
  | FUS (first, f1) -> (first, f1)
1017
  | _ -> raise (CoAlgException "Formula is not a fusion formula.")
1018

    
1019

    
1020
(** Tests whether a formula is the constant True.
1021
    @param f A formula.
1022
    @return True iff f is the constant True.
1023
 *)
1024
let is_true f =
1025
  match f with
1026
  | TRUE -> true
1027
  | _ -> false
1028

    
1029
(** Tests whether a formula is the constant False.
1030
    @param f A formula.
1031
    @return True iff f is the constant False.
1032
 *)
1033
let is_false f =
1034
  match f with
1035
  | FALSE -> true
1036
  | _ -> false
1037

    
1038
(** Tests whether a formula is an atomic proposition.
1039
    @param f A formula.
1040
    @return True iff f is an atomic proposition.
1041
 *)
1042
let is_ap f =
1043
  match f with
1044
  | AP s when not (isNominal s) -> true
1045
  | _ -> false
1046

    
1047
(** Tests whether a formula is a nominal.
1048
    @param f A formula.
1049
    @return True iff f is a nominal.
1050
 *)
1051
let is_nom f =
1052
  match f with
1053
  | AP s when isNominal s -> true
1054
  | _ -> false
1055

    
1056
(** Tests whether a formula is a negation.
1057
    @param f A formula.
1058
    @return True iff f is a negation.
1059
 *)
1060
let is_not f =
1061
  match f with
1062
  | NOT _ -> true
1063
  | _ -> false
1064

    
1065
(** Tests whether a formula is an @-formula.
1066
    @param f A formula.
1067
    @return True iff f is an @-formula.
1068
 *)
1069
let is_at f =
1070
  match f with
1071
  | AT _ -> true
1072
  | _ -> false
1073

    
1074
(** Tests whether a formula is an or-formula.
1075
    @param f A formula.
1076
    @return True iff f is an or-formula.
1077
 *)
1078
let is_or f =
1079
  match f with
1080
  | OR _ -> true
1081
  | _ -> false
1082

    
1083
(** Tests whether a formula is an and-formula.
1084
    @param f A formula.
1085
    @return True iff f is an and-formula.
1086
 *)
1087
let is_and f =
1088
  match f with
1089
  | AND _ -> true
1090
  | _ -> false
1091

    
1092
(** Tests whether a formula is an equivalence.
1093
    @param f A formula.
1094
    @return True iff f is an equivalence.
1095
 *)
1096
let is_equ f =
1097
  match f with
1098
  | EQU _ -> true
1099
  | _ -> false
1100

    
1101
(** Tests whether a formula is an implication.
1102
    @param f A formula.
1103
    @return True iff f is an implication.
1104
 *)
1105
let is_imp f =
1106
  match f with
1107
  | IMP _ -> true
1108
  | _ -> false
1109

    
1110
(** Tests whether a formula is an EX-formula.
1111
    @param f A formula.
1112
    @return True iff f is an EX-formula.
1113
 *)
1114
let is_ex f =
1115
  match f with
1116
  | EX _ -> true
1117
  | _ -> false
1118

    
1119
(** Tests whether a formula is an AX-formula.
1120
    @param f A formula.
1121
    @return True iff f is an AX-formula.
1122
 *)
1123
let is_ax f =
1124
  match f with
1125
  | AX _ -> true
1126
  | _ -> false
1127

    
1128
(** Tests whether a formula is a MIN-formula.
1129
    @param f A formula.
1130
    @return True iff f is a MIN-formula.
1131
 *)
1132
let is_min f =
1133
  match f with
1134
  | MIN _ -> true
1135
  | _ -> false
1136

    
1137
(** Tests whether a formula is a MAX-formula.
1138
    @param f A formula.
1139
    @return True iff f is a MAX-formula.
1140
 *)
1141
let is_max f =
1142
  match f with
1143
  | MAX _ -> true
1144
  | _ -> false
1145

    
1146
(** Tests whether a formula is a choice formula.
1147
    @param f A formula.
1148
    @return True iff f is a choice formula.
1149
 *)
1150
let is_choice f =
1151
  match f with
1152
  | CHC _ -> true
1153
  | _ -> false
1154

    
1155
(** Tests whether a formula is a fusion formula.
1156
    @param f A formula.
1157
    @return True iff f is a fusion formula.
1158
 *)
1159
let is_fusion f =
1160
  match f with
1161
  | FUS _ -> true
1162
  | _ -> false
1163

    
1164
        
1165
(** The constant True.
1166
 *)
1167
let const_true = TRUE
1168

    
1169
(** The constant False.
1170
 *)
1171
let const_false = FALSE
1172
    
1173
(** Constructs an atomic proposition.
1174
    @param s The name of the atomic proposition.
1175
    @return The atomic proposition with name s.
1176
    @raise CoAlgException if s is a nominal name.
1177
 *)
1178
let const_ap s =
1179
  if isNominal s then raise (CoAlgException "The name indicates a nominal.")
1180
  else AP s
1181

    
1182
(** Constructs a nominal.
1183
    @param s The name of the nominal.
1184
    @return A nominal with name s.
1185
    @raise CoAlgException if s is not a nominal name.
1186
 *)
1187
let const_nom s =
1188
  if isNominal s then AP s
1189
  else raise (CoAlgException "The name does not indicate a nominal.")
1190

    
1191
(** Negates a formula.
1192
    @param f A formula.
1193
    @return The negation of f.
1194
 *)
1195
let const_not f = NOT f
1196
  
1197
(** Constructs an @-formula from a name and a formula.
1198
    @param s A nominal name.
1199
    @param f A formula.
1200
    @return The formula AT (s, f).
1201
 *)
1202
let const_at s f = AT (s, f)
1203

    
1204
(** Constructs an or-formula from two formulae.
1205
    @param f1 The first formula (LHS).
1206
    @param f2 The second formula (LHS).
1207
    @return The formula f1 | f2.
1208
 *)
1209
let const_or f1 f2 = OR (f1, f2)
1210

    
1211
(** Constructs an and-formula from two formulae.
1212
    @param f1 The first formula (LHS).
1213
    @param f2 The second formula (LHS).
1214
    @return The formula f1 & f2.
1215
 *)    
1216
let const_and f1 f2 = AND (f1, f2)
1217

    
1218
(** Constructs an equivalence from two formulae.
1219
    @param f1 The first formula (LHS).
1220
    @param f2 The second formula (LHS).
1221
    @return The equivalence f1 <=> f2.
1222
 *)
1223
let const_equ f1 f2 = EQU (f1, f2)
1224

    
1225
(** Constructs an implication from two formulae.
1226
    @param f1 The first formula (LHS).
1227
    @param f2 The second formula (LHS).
1228
    @return The implication f1 => f2.
1229
 *)
1230
let const_imp f1 f2 = IMP (f1, f2)
1231

    
1232
(** Constructs an EX-formula from a formula.
1233
    @param s A role name.
1234
    @param f A formula.
1235
    @return The formula EX (s, f).
1236
 *)
1237
let const_ex s f = EX (s, f)
1238

    
1239
(** Constructs an AX-formula from a formula.
1240
    @param s A role name.
1241
    @param f A formula.
1242
    @return The formula AX (s, f).
1243
 *)
1244
let const_ax s f = AX (s, f)
1245

    
1246
(** Constructs a MIN-formula from a formula.
1247
    @param n A non-negative integer.
1248
    @param s A role name.
1249
    @param f A formula.
1250
    @return The formula MIN f.
1251
    @raise CoAlgException Iff n is negative.
1252
 *)
1253
let const_min n s f =
1254
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
1255
  else MIN (n, s, f)
1256

    
1257
(** Constructs a MAX-formula from a formula.
1258
    @param n A non-negative integer.
1259
    @param s A role name.
1260
    @param f A formula.
1261
    @return The formula MAX f.
1262
    @raise CoAlgException Iff n is negative.
1263
 *)
1264
let const_max n s f =
1265
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
1266
  else MAX (n, s, f)
1267

    
1268
let const_enforces p f =
1269
    ENFORCES (p,f)
1270

    
1271
let const_allows p f =
1272
    ALLOWS (p,f)
1273

    
1274
(** Constructs a choice formula from two formulae.
1275
    @param f1 The first formula (LHS).
1276
    @param f2 The second formula (LHS).
1277
    @return The formula (f1 + f2).
1278
 *)
1279
let const_choice f1 f2 = CHC (f1, f2)
1280

    
1281
(** Constructs a fusion formula.
1282
    @param first True iff the result is a first projection.
1283
    @param f1 A formula.
1284
    @return The formula [pi1] f1 or [pi2] f1 (depending on first).
1285
 *)
1286
let const_fusion first f1 = FUS (first, f1)
1287

    
1288

    
1289
(** Hash-consed formulae, which are in negation normal form,
1290
    such that structural and physical equality coincide.
1291
 *)
1292
type hcFormula = (hcFormula_node, formula) HC.hash_consed
1293
and hcFormula_node =
1294
  | HCTRUE
1295
  | HCFALSE
1296
  | HCAP of string
1297
  | HCNOT of string
1298
  | HCAT of string * hcFormula
1299
  | HCOR of hcFormula * hcFormula
1300
  | HCAND of hcFormula * hcFormula
1301
  | HCEX of string * hcFormula
1302
  | HCAX of string * hcFormula
1303
  | HCENFORCES of int list * hcFormula
1304
  | HCALLOWS of int list * hcFormula
1305
  | HCMORETHAN of int * string * hcFormula (* GML Diamond *)
1306
  | HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
1307
  | HCCHC of hcFormula * hcFormula
1308
  | HCCHCN of hcFormula * hcFormula
1309
  | HCFUS of bool * hcFormula
1310

    
1311
(** Determines whether two formula nodes are structurally equal.
1312
    @param f1 The first formula node.
1313
    @param f2 The second formula node.
1314
    @return True iff f1 and f2 are structurally equal.
1315
 *)
1316
let equal_hcFormula_node f1 f2 =
1317
  match f1, f2 with
1318
  | HCTRUE, HCTRUE -> true
1319
  | HCFALSE, HCFALSE -> true
1320
  | HCAP s1, HCAP s2
1321
  | HCNOT s1, HCNOT s2 -> compare s1 s2 = 0
1322
  | HCAT (s1, f1), HCAT (s2, f2) -> compare s1 s2 = 0 && f1 == f2
1323
  | HCOR (f1a, f1b), HCOR (f2a, f2b)
1324
  | HCAND (f1a, f1b), HCAND (f2a, f2b) -> f1a == f2a && f1b == f2b
1325
  | HCEX (s1, f1), HCEX (s2, f2)
1326
  | HCAX (s1, f1), HCAX (s2, f2) -> compare s1 s2 = 0 && f1 == f2
1327
  | HCENFORCES (s1, f1), HCALLOWS (s2, f2)
1328
  | HCENFORCES (s1, f1), HCALLOWS (s2, f2) -> compare s1 s2 = 0 && f1 == f2
1329
  | HCMORETHAN (n1, s1, f1), HCMORETHAN (n2, s2, f2)
1330
  | HCMAXEXCEPT (n1, s1, f1), HCMAXEXCEPT (n2, s2, f2) ->
1331
      n1 = n2 && compare s1 s2 = 0 && f1 == f2 
1332
  | HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b
1333
  | HCCHCN (f1a, f1b), HCCHCN (f2a, f2b) -> f1a == f2a && f1b == f2b
1334
  | HCFUS (first1, f1), HCFUS (first2, f2) -> first1 = first2 && f1 == f2
1335
(* The rest could be shortened to | _ -> false,
1336
   but then the compiler would not warn if the formula type is extended
1337
   and this function is not updated accordingly.*)
1338
  | HCTRUE, _
1339
  | HCFALSE, _
1340
  | HCAP _, _
1341
  | HCNOT _, _
1342
  | HCAT _, _
1343
  | HCOR _, _
1344
  | HCAND _, _
1345
  | HCEX _, _
1346
  | HCAX _, _
1347
  | HCENFORCES _, _
1348
  | HCALLOWS   _, _
1349
  | HCMORETHAN _, _
1350
  | HCMAXEXCEPT _, _
1351
  | HCCHC _, _
1352
  | HCCHCN _, _
1353
  | HCFUS _, _ -> false
1354

    
1355
(** Computes the hash value of a formula node.
1356
    @param f A formula node.
1357
    @return The hash value of f.
1358
 *)
1359
let hash_hcFormula_node f =
1360
  match f with
1361
  | HCTRUE -> 0
1362
  | HCFALSE -> 1
1363
  | HCAP s
1364
  | HCNOT s -> 19 * Hashtbl.hash s + 1
1365
  | HCAT (s, f1) -> 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 2
1366
  | HCOR (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 5
1367
  | HCAND (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 6
1368
  | HCEX (s, f1) -> 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 3
1369
  | HCAX (s, f1) -> 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 4
1370
  | HCMORETHAN (n, s, f1) -> 19 * (19 * (19 * (Hashtbl.hash s) + n) + f1.HC.hkey) + 7
1371
  | HCMAXEXCEPT (n, s, f1) -> 19 * (19 * (19 * (Hashtbl.hash s) + n) + f1.HC.hkey) + 8
1372
  | HCCHC (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 9
1373
  | HCCHCN (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 10
1374
  | HCFUS (first, f1) -> 19 * (19 * (Hashtbl.hash first) + f1.HC.hkey) + 11
1375
  | HCENFORCES (s, f1) -> 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 12
1376
  | HCALLOWS   (s, f1) -> 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 13
1377

    
1378
(** Determines the "real" formula of a formula node.
1379
    @param f A formula node.
1380
    @return The formula (in negation normal form) which corresponds to f.
1381
 *)
1382
let toFml_hcFormula_node f =
1383
  match f with
1384
  | HCTRUE -> TRUE
1385
  | HCFALSE -> FALSE
1386
  | HCAP s -> AP s
1387
  | HCNOT s -> NOT (AP s)
1388
  | HCAT (s, f1) -> AT (s, f1.HC.fml)
1389
  | HCOR (f1, f2) -> OR (f1.HC.fml, f2.HC.fml)
1390
  | HCAND (f1, f2) -> AND (f1.HC.fml, f2.HC.fml)
1391
  | HCEX (s, f1) -> EX (s, f1.HC.fml)
1392
  | HCAX (s, f1) -> AX (s, f1.HC.fml)
1393
  | HCENFORCES (s, f1) -> ENFORCES (s, f1.HC.fml)
1394
  | HCALLOWS (s, f1) -> ALLOWS (s, f1.HC.fml)
1395
  | HCMORETHAN (n, s, f1) -> MORETHAN (n, s, f1.HC.fml)
1396
  | HCMAXEXCEPT (n, s, f1) -> MAXEXCEPT (n, s, f1.HC.fml)
1397
  | HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml)
1398
  | HCCHCN (f1, f2) -> CHCN (f1.HC.fml, f2.HC.fml)
1399
  | HCFUS (first, f1) -> FUS (first, f1.HC.fml)
1400

    
1401
(** Determines the negation (in negation normal form) of a formula node.
1402
    @param f A formula node.
1403
    @return The negation (in negation normal form) of f.
1404
 *)
1405
let negNde_hcFormula_node f =
1406
  match f with
1407
  | HCTRUE -> HCFALSE
1408
  | HCFALSE -> HCTRUE
1409
  | HCAP s -> HCNOT s
1410
  | HCNOT s -> HCAP s
1411
  | HCAT (s, f1) -> HCAT (s, f1.HC.neg)
1412
  | HCOR (f1, f2) -> HCAND (f1.HC.neg, f2.HC.neg)
1413
  | HCAND (f1, f2) -> HCOR (f1.HC.neg, f2.HC.neg)
1414
  | HCEX (s, f2) -> HCAX (s, f2.HC.neg)
1415
  | HCAX (s, f2) -> HCEX (s, f2.HC.neg)
1416
  | HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg)
1417
  | HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg)
1418
  | HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg)
1419
  | HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg)
1420
  | HCCHC (f1, f2) -> HCCHCN (f1.HC.neg, f2.HC.neg)
1421
  | HCCHCN (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg)
1422
  | HCFUS (first, f1) -> HCFUS (first, f1.HC.neg)
1423

    
1424
(** An instantiation of hash-consing for formulae.
1425
 *)
1426
module HcFormula = HC.Make(
1427
  struct
1428
    type nde = hcFormula_node
1429
    type fml = formula
1430
    let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2
1431
    let hash (n : nde) = hash_hcFormula_node n
1432
    let negNde (n : nde) = negNde_hcFormula_node n
1433
    let toFml (n : nde) = toFml_hcFormula_node n
1434
  end
1435
 )
1436

    
1437
(** Converts a formula into its hash-consed version.
1438
    @param hcF A hash-cons table for formulae.
1439
    @param f A formula in negation normal form.
1440
    @return The hash-consed version of f.
1441
    @raise CoAlgException if f is not in negation normal form.
1442
*)
1443
let rec hc_formula hcF f =
1444
  match f with
1445
  | TRUE -> HcFormula.hashcons hcF HCTRUE
1446
  | FALSE -> HcFormula.hashcons hcF HCFALSE
1447
  | AP s -> HcFormula.hashcons hcF (HCAP s)
1448
  | NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s)
1449
  | AT (s, f1) ->
1450
      let tf1 = hc_formula hcF f1 in
1451
      HcFormula.hashcons hcF (HCAT (s, tf1))
1452
  | OR (f1, f2) ->
1453
      let tf1 = hc_formula hcF f1 in
1454
      let tf2 = hc_formula hcF f2 in
1455
      HcFormula.hashcons hcF (HCOR (tf1, tf2))
1456
  | AND (f1, f2) ->
1457
      let tf1 = hc_formula hcF f1 in
1458
      let tf2 = hc_formula hcF f2 in
1459
      HcFormula.hashcons hcF (HCAND (tf1, tf2))
1460
  | NOT _
1461
  | EQU _
1462
  | MIN _
1463
  | MAX _
1464
  | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.")
1465
  | EX (s, f1) ->
1466
      let tf1 = hc_formula hcF f1 in
1467
      HcFormula.hashcons hcF (HCEX (s, tf1))
1468
  | AX (s, f1) ->
1469
      let tf1 = hc_formula hcF f1 in
1470
      HcFormula.hashcons hcF (HCAX (s, tf1))
1471
  | ENFORCES (s, f1) ->
1472
      let tf1 = hc_formula hcF f1 in
1473
      HcFormula.hashcons hcF (HCENFORCES (s, tf1))
1474
  | ALLOWS (s, f1) ->
1475
      let tf1 = hc_formula hcF f1 in
1476
      HcFormula.hashcons hcF (HCALLOWS (s, tf1))
1477
  | MORETHAN  (n, s, f1) ->
1478
      let tf1 = hc_formula hcF f1 in
1479
      HcFormula.hashcons hcF (HCMORETHAN (n, s, tf1))
1480
  | MAXEXCEPT  (n, s, f1) ->
1481
      let tf1 = hc_formula hcF f1 in
1482
      HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1))
1483
  | CHC (f1, f2) ->
1484
      let tf1 = hc_formula hcF f1 in
1485
      let tf2 = hc_formula hcF f2 in
1486
      HcFormula.hashcons hcF (HCCHC (tf1, tf2))
1487
  | CHCN (f1, f2) ->
1488
      let tf1 = hc_formula hcF f1 in
1489
      let tf2 = hc_formula hcF f2 in
1490
      HcFormula.hashcons hcF (HCCHCN (tf1, tf2))
1491
  | FUS (first, f1) ->
1492
      let tf1 = hc_formula hcF f1 in
1493
      HcFormula.hashcons hcF (HCFUS (first, tf1))
1494

    
1495

    
1496
(** An instantiation of a hash table (of the standard library)
1497
    for hash-consed formulae. The test for equality
1498
    and computing the hash value is done in constant time.
1499
 *)
1500
module HcFHt = Hashtbl.Make(
1501
  struct
1502
    type t = hcFormula
1503
    let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag
1504
    let hash (f : t) = f.HC.tag
1505
  end
1506
 )