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 tatlinputs *) 
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 "<nonnegative 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 ("<nonnegative 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 (n1, 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 (n1,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 orformula. 
916 
@param f An orformula. 
917 
@return The two immediate subformulae of the orformula. 
918 
@raise CoAlgException if f is not an orformula. 
919 
*) 
920 
let dest_or f = 
921 
match f with 
922 
 OR (f1, f2) > (f1, f2) 
923 
 _ > raise (CoAlgException "Formula is not an orformula.") 
924  
925 
(** Destructs an andformula. 
926 
@param f An andformula. 
927 
@return The two immediate subformulae of the andformula. 
928 
@raise CoAlgException if f is not an andformula. 
929 
*) 
930 
let dest_and f = 
931 
match f with 
932 
 AND (f1, f2) > (f1, f2) 
933 
 _ > raise (CoAlgException "Formula is not an andformula.") 
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 EXformula. 
956 
@param f An EXformula. 
957 
@return The role name and the immediate subformula of the EXformula. 
958 
@raise CoAlgException if f is not an EXformula. 
959 
*) 
960 
let dest_ex f = 
961 
match f with 
962 
 EX (s, f1) > (s, f1) 
963 
 _ > raise (CoAlgException "Formula is not an EXformula.") 
964  
965 
(** Destructs an AXformula. 
966 
@param f An AXformula. 
967 
@return The role name and the immediate subformula of the AXformula. 
968 
@raise CoAlgException if f is not an AXformula. 
969 
*) 
970 
let dest_ax f = 
971 
match f with 
972 
 AX (s, f1) > (s, f1) 
973 
 _ > raise (CoAlgException "Formula is not an AXformula.") 
974  
975 
(** Destructs a MINformula. 
976 
@param f A MINformula. 
977 
@return The number restriction, role name, 
978 
and the immediate subformula of the MINformula. 
979 
@raise CoAlgException if f is not a MINformula. 
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 MINformula.") 
985  
986 
(** Destructs a MAXformula. 
987 
@param f A MAXformula. 
988 
@return The number restriction, role name, 
989 
and the immediate subformula of the MAXformula. 
990 
@raise CoAlgException if f is not a MAXformula. 
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 MAXformula.") 
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 orformula. 
1075 
@param f A formula. 
1076 
@return True iff f is an orformula. 
1077 
*) 
1078 
let is_or f = 
1079 
match f with 
1080 
 OR _ > true 
1081 
 _ > false 
1082  
1083 
(** Tests whether a formula is an andformula. 
1084 
@param f A formula. 
1085 
@return True iff f is an andformula. 
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 EXformula. 
1111 
@param f A formula. 
1112 
@return True iff f is an EXformula. 
1113 
*) 
1114 
let is_ex f = 
1115 
match f with 
1116 
 EX _ > true 
1117 
 _ > false 
1118  
1119 
(** Tests whether a formula is an AXformula. 
1120 
@param f A formula. 
1121 
@return True iff f is an AXformula. 
1122 
*) 
1123 
let is_ax f = 
1124 
match f with 
1125 
 AX _ > true 
1126 
 _ > false 
1127  
1128 
(** Tests whether a formula is a MINformula. 
1129 
@param f A formula. 
1130 
@return True iff f is a MINformula. 
1131 
*) 
1132 
let is_min f = 
1133 
match f with 
1134 
 MIN _ > true 
1135 
 _ > false 
1136  
1137 
(** Tests whether a formula is a MAXformula. 
1138 
@param f A formula. 
1139 
@return True iff f is a MAXformula. 
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 orformula 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 andformula 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 EXformula 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 AXformula 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 MINformula from a formula. 
1247 
@param n A nonnegative 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 MAXformula from a formula. 
1258 
@param n A nonnegative 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 
(** Hashconsed 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 hashconsing 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 hashconsed version. 
1438 
@param hcF A hashcons table for formulae. 
1439 
@param f A formula in negation normal form. 
1440 
@return The hashconsed 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 hashconsed 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 
) 