Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / FuzzyALCABox.ml @ b75e5a66

History | View | Annotate | Download (15.6 KB)

1
(*
2
 * vim: ts=2 sw=2
3
 *)
4
(** This module implements fuzzy ALC formulae
5
    (e.g. parsing, printing, (de-)constructing, ...).
6
    @author Florian Widmann / Dominik Paulus
7
 *)
8

    
9
module HC = HashConsing
10
module A = AltGenlex
11
module L = List
12
module Str = String
13

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

    
20
(** Defines (unsorted) coalgebraic formulae.
21
 *)
22
type concept =
23
  | TRUE
24
  | FALSE
25
  | AP of string
26
  | NOT of concept
27
  | OR of concept * concept
28
  | AND of concept * concept
29
  | EXISTS of int * concept
30
  | FORALL of int * concept
31

    
32
type asst =
33
  | ROLE of int * int * int
34
  | CONCEPT of int * concept
35
type assertion = (asst list) * int * (asst list)
36

    
37
exception ConversionException of concept
38

    
39
let rec print_fuzzyDL concept =
40
  match concept with
41
  | TRUE -> "*top*"
42
  | FALSE -> "*bottom*"
43
  | AP(s) -> s
44
  | NOT(s) -> "(not " ^ print_fuzzyDL s ^ ")"
45
  | EXISTS(a, b) -> "(some R" ^ string_of_int a ^ " " ^ print_fuzzyDL b ^ ")"
46
  | FORALL(a, b) -> "(all R" ^ string_of_int a ^ " " ^ print_fuzzyDL b ^ ")"
47
  | AND(a, b) -> "(and " ^ print_fuzzyDL a ^ " " ^ print_fuzzyDL b ^ ")"
48
  | OR(a, b) -> "(or " ^ print_fuzzyDL a ^ " " ^ print_fuzzyDL b ^ ")"
49

    
50
let rec random_concept depth count atoms (weights : int list) =
51
  snd (random_concept_int depth count atoms weights)
52
(* Returns: (Number of operators used, concept) *)
53
and random_concept_int depth count atoms weights =
54
  let random_atomic a =
55
    match (Random.int a) with
56
      | 0 -> TRUE
57
      | 1 -> AP("A")
58
      | 2 -> AP("B")
59
      | 3 -> AP("C")
60
      | 4 -> AP("D")
61
      | 5 -> AP("E")
62
      | 6 -> AP("F")
63
      | 7 -> AP("G")
64
      | 8 -> AP("H")
65
      | 9 -> AP("I")
66
      | _ -> AP("J")
67
  in
68
  let sumweights = List.fold_left (+) 0 weights in
69
  (*
70
  let f (sum, ret) elem =
71
    (sum + elem, (sum+elem)::ret)
72
  in
73
  let summed = snd (List.fold_left f (0, []) weights) in
74
*)
75
  let rnd = Random.int sumweights in
76
  if (depth = 0 || count = 0 || (rnd < List.hd weights)) then
77
    (0, random_atomic atoms)
78
  else (
79
    let (u1, con1) = random_concept_int (depth - 1) (count-1) atoms weights in
80
    let l2 = List.tl weights in
81
    let s2 = List.hd weights in
82
    if rnd < (s2 + List.hd l2) then
83
      (u1+1, NOT(con1))
84
    else
85
      (* Two operands of our operator *)
86
      let l3 = List.tl l2 in
87
      let s3 = s2 + List.hd l2 in
88
      if rnd < (s3 + List.hd l3) then
89
        let (u2, con2) = random_concept_int (depth - 1) (count-1-u1) atoms weights in
90
        (u1+u2+1, AND(con1, con2))
91
      else
92
        (u1+1, EXISTS(Random.int 42, con1))
93
  )
94

    
95
let rec count_operators concept =
96
  match concept with
97
  | TRUE -> 0
98
  | AP(_) -> 0
99
  | NOT(x) -> 1 + count_operators x
100
  | AND(x, y) -> (count_operators x) + (count_operators y) + 1
101
  | EXISTS(_, y) -> 1 + (count_operators y)
102

    
103
let rec random_concept_opcount depth count atoms weights =
104
  let rec helper p =
105
    let con = random_concept depth count atoms weights in
106
    if (count_operators con) = count then con
107
    else helper p
108
  in
109
  helper 1
110

    
111
  (*
112
let rec random_ABox depth_left depth_right =
113
  let left =
114
    if depth_left <> 0 then
115
      [CONCEPT(0, random_concept (Random.int depth_left))]
116
    else
117
      []
118
  in
119
  let right =
120
    if depth_right <> 0 then
121
      [CONCEPT(0, random_concept (Random.int depth_right))]
122
    else
123
      []
124
  in
125
  (left, 0, right)
126
  *)
127

    
128
let lexer = A.make_lexer 
129
    [":";"(";")";"|";"&";"~";"True";"False";"[";"]";"<";">";"+";".";";";","]
130

    
131
let mk_exn s = CoAlgException s
132

    
133
(** These functions parse a token stream to obtain a formula.
134
    It is a standard recursive descent procedure.
135
    @param ts A token stream.
136
    @return The resulting (sub-)formula.
137
    @raise CoAlgException if ts does not represent a formula.
138
 *)
139
let rec parse_asst ts =
140
  let cur = match (Stream.next ts, Stream.next ts, Stream.peek ts) with
141
    (* Concept *)
142
    | (A.Int id, A.Kwd ":", _) ->
143
      CONCEPT(id, parse_or ts)
144
    (* Role *)
145
    | (A.Int i, A.Kwd ",", Some (A.Int j)) ->
146
      ((* Discard j *)
147
      Stream.junk ts;
148
      (* Discard ":", TODO: Check this *)
149
      Stream.junk ts;
150
      let (A.Int k) = Stream.next ts in
151
      ROLE(i, j, k))
152
    | _ -> A.printError mk_exn ~ts ("Invalid concept.")
153
  in
154
  match Stream.peek ts with
155
  | Some (A.Kwd "+") ->
156
      Stream.junk ts;
157
      cur :: (parse_asst ts)
158
  | _ -> [cur]
159

    
160
(** These functions parse a token stream to obtain a formula.
161
    It is a standard recursive descent procedure.
162
    @param ts A token stream.
163
    @return The resulting (sub-)formula.
164
    @raise CoAlgException if ts does not represent a formula.
165
 *)
166
and parse_or ts =
167
  let f1 = parse_and ts in
168
  match Stream.peek ts with
169
  | None -> f1
170
  | Some (A.Kwd "|") ->
171
      Stream.junk ts;
172
      let f2 = parse_or ts in
173
      OR (f1, f2)
174
  | _ -> f1
175

    
176
(** These functions parse a token stream to obtain a formula.
177
    It is a standard recursive descent procedure.
178
    @param ts A token stream.
179
    @return The resulting (sub-)formula.
180
    @raise CoAlgException if ts does not represent a formula.
181
 *)
182
and parse_and ts =
183
  let f1 = parse_rest ts in
184
  match Stream.peek ts with
185
  | None -> f1
186
  | Some (A.Kwd "&") ->
187
      Stream.junk ts;
188
      let f2 = parse_and ts in
189
      AND (f1, f2)
190
  | _ -> f1
191

    
192
(** These functions parse a token stream to obtain a formula.
193
    It is a standard recursive descent procedure.
194
    @param ts A token stream.
195
    @return The resulting (sub-)formula.
196
    @raise CoAlgException if ts does not represent a formula.
197
 *)
198
and parse_rest ts =
199
  match Stream.next ts with
200
  | A.Kwd "True" -> TRUE
201
  | A.Kwd "False" -> FALSE
202
  | A.Ident s -> AP s
203
  | A.Kwd "~" ->
204
      let f = parse_rest ts in
205
      NOT f
206
  | A.Kwd "<" -> 
207
      let name =
208
        match Stream.next ts with
209
        | A.Int sl -> sl
210
        | _ -> A.printError mk_exn ~ts ("role id expected")
211
      in
212
      let f1 = parse_or ts in
213
      let _ =
214
        match Stream.next ts with
215
        | A.Kwd c when c = ">" -> ""
216
        | _ -> A.printError mk_exn ~ts ("\">\" expected: ")
217
      in
218
      EXISTS (name, f1) 
219
  | A.Kwd "[" -> 
220
      let name =
221
        match Stream.next ts with
222
        | A.Int sl -> sl
223
        | _ -> A.printError mk_exn ~ts ("role id expected")
224
      in
225
      let f1 = parse_or ts in
226
      let _ =
227
        match Stream.next ts with
228
        | A.Kwd c when c = "]" -> ""
229
        | _ -> A.printError mk_exn ~ts ("\"]\" expected: ")
230
      in
231
      FORALL (name, f1) 
232
  | A.Kwd "(" -> begin
233
      let f = parse_or ts in
234
      match Stream.next ts with
235
      | A.Kwd ")" -> f
236
      | t -> A.printError mk_exn ~t ~ts "\")\" expected: "
237
    end
238
  | t -> A.printError mk_exn ~t ~ts 
239
      "\"<\", \"[\", \"{>=\", \"{<=\", \"@\", \"~\", \"(\", \"True\", \"False\", or <ident> expected: "
240

    
241
(** Parsees a assertion of the form "(role/concept assertions) >n (role/concept assertions)" *)
242
let rec parse_assertion ts =
243
  (* Left side *)
244
  let left =
245
    match Stream.peek ts with
246
    | Some (A.Kwd ">") -> []
247
    | _ -> parse_asst ts
248
  in
249
  (* Greater sign *)
250
  let gr =
251
    match (Stream.next ts, Stream.next ts) with
252
    | (A.Kwd ">", A.Int i) -> i
253
    | _ -> A.printError mk_exn ~ts ("Invalid assertion, \">(num)\" expected")
254
  in
255
  (* Right side *)
256
  let right =
257
    match Stream.peek ts with
258
    | None -> []
259
    | _ -> parse_asst ts
260
  in
261
  (left, gr, right)
262
        
263
(** Parses a sorted formula.
264
    @param ts A token stream.
265
    @return A sorted formula.
266
    @raise CoAlgException If ts does not represent a sorted formula.
267
 *)
268
let parse_sortedFormula ts =
269
  parse_assertion ts
270

    
271
(** Parses a list of sorted formulae separated by ";".
272
    @param ts A token stream.
273
    @param acc The list of sorted formulae parsed so far.
274
    @return The resulting list of sorted formula.
275
    @raise CoAlgException if ts does not represent a list of sorted formulae.
276
 *)
277
let rec parse_SortedFormulaList ts acc =
278
  let f1 = parse_sortedFormula ts in
279
  match Stream.peek ts with
280
  | Some (A.Kwd ";") ->
281
      Stream.junk ts;
282
      if (Stream.peek ts) == None then
283
        acc
284
      else
285
        parse_SortedFormulaList ts (f1::acc)
286
  | _ -> List.rev (f1::acc)
287

    
288
(** A common wrapper for import functions.
289
    @param fkt An import function.
290
    @param s A string.
291
    @return The object imported from s using fkt.
292
    @raise CoAlgException If ts is not empty.
293
 *)
294
let importWrapper fkt s =
295
  let ts = lexer s in
296
  try
297
    let res = fkt ts [] in
298
    let _ =
299
      match Stream.peek ts with
300
      | None -> ()
301
      | Some _ -> A.printError mk_exn ~ts "EOS expected: "
302
    in
303
    res
304
  with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS"
305

    
306
(** Parses a string to obtain a formula.
307
    @param s A string representing a formula.
308
    @return The resulting formula.
309
    @raise CoAlgException if s does not represent a formula.
310
 *)
311
(*let importFormula s = importWrapper parse_asst s*)
312

    
313
(** Parses a string to obtain a sorted formula.
314
    @param s A string representing a sorted formula.
315
    @return The sorted formula.
316
    @raise CoAlgException If s does not represent a sorted formula.
317
 *)
318
(*let importSortedFormula s = importWrapper parse_sortedFormula s*)
319

    
320
(** Parses a string to obtain a (sorted) formula query.
321
    @param s A string representing a formula query.
322
    @return A pair (tbox, f) where
323
    tbox is a list of sorted formulae representing the TBox; and
324
    f is a sorted formula.
325
    @raise CoAlgException if s does not represent a formula query.
326
 *)
327
let importQuery s =
328
  importWrapper parse_SortedFormulaList s
329

    
330
let rec printConcept x =
331
  match x with
332
  | AP(a) -> a
333
  | OR (a, b) -> "(" ^ printConcept a ^ " | " ^ printConcept b ^ ")"
334
  | AND (a, b) -> "(" ^ printConcept a ^ " & " ^ printConcept b ^ ")"
335
  | NOT (a) -> "~" ^ printConcept a
336
  | FORALL (a, b) -> "[" ^ (string_of_int a) ^ " " ^ printConcept b ^ "]"
337
  | EXISTS (a, b) -> "<" ^ (string_of_int a) ^ " " ^ printConcept b ^ ">"
338
  | TRUE -> "True"
339
  | FALSE -> "False"
340

    
341
let rec printAsst s =
342
  let convert ts =
343
    match ts with
344
    | CONCEPT(x, y) -> (string_of_int x) ^ ":(" ^ (printConcept y) ^ ")"
345
    | ROLE(a, b, c) -> (string_of_int a) ^ "," ^ (string_of_int b) ^ ":" ^ (string_of_int c)
346
  in
347
  match s with
348
  | [] -> ""
349
  | _ -> List.fold_left (fun acc ts -> acc ^ " + " ^ convert ts) (convert (List.hd s)) (List.tl s)
350

    
351
let rec printAssertion s =
352
  match s with
353
  | (left, gr, right) -> (printAsst left) ^ " >" ^ (string_of_int gr) ^ " " ^ (printAsst right)
354

    
355
let rec assertionMap a f =
356
  let g x =
357
    match x with
358
    | CONCEPT (a, b) -> CONCEPT (a, f b)
359
    | a -> a
360
  in
361
  match a with
362
  | (left, gr, right) -> (List.map g left, gr, List.map g right)
363

    
364
let rec replaceOrForall s =
365
  let rec g x =
366
    match x with
367
    | FORALL (a, b) -> NOT(EXISTS(a, NOT(g b)))
368
    | OR (a, b) -> NOT(AND(NOT a, NOT (g b)))
369
    (* We don't touch these *)
370
    | AP(a) -> AP(a)
371
    | AND(a, b) -> AND(g a, g b)
372
    | NOT(a) -> NOT(g a)
373
    | EXISTS(a, b) -> EXISTS(a, g b)
374
    | TRUE -> TRUE
375
    | FALSE -> FALSE
376
  in
377
  assertionMap s g
378

    
379
let rec collapseNeg s =
380
  let rec f x =
381
    match x with
382
    | NOT(NOT(a)) -> f a
383
    | NOT(a) -> NOT (f a)
384
    | AP(a) -> AP(a)
385
    | OR(a, b) -> OR(f a, f b)
386
    | AND(a, b) -> AND(f a, f b)
387
    | FORALL(a, b) -> FORALL(a, f b)
388
    | EXISTS(a, b) -> EXISTS(a, f b)
389
    | a -> a
390
  in
391
  assertionMap s f
392

    
393
(** Hash-consed formulae, which are in negation normal form,
394
    such that structural and physical equality coincide.
395
 *)
396
type hcConcept = (hcConcept_node, concept) HC.hash_consed
397
and hcConcept_node =
398
  | HCTRUE
399
  | HCFALSE
400
  | HCAP of string
401
  | HCNOT of hcConcept
402
  | HCOR of hcConcept * hcConcept
403
  | HCAND of hcConcept * hcConcept
404
  | HCEXISTS of int * hcConcept
405
  | HCFORALL of int * hcConcept
406

    
407
(** Determines whether two formula nodes are structurally equal.
408
    @param f1 The first formula node.
409
    @param f2 The second formula node.
410
    @return True iff f1 and f2 are structurally equal.
411
 *)
412
let equal_hcConcept_node f1 f2 =
413
  match f1, f2 with
414
  | HCTRUE, HCTRUE -> true
415
  | HCFALSE, HCFALSE -> true
416
  | HCAP s1, HCAP s2 -> compare s1 s2 = 0
417
  | HCNOT s1, HCNOT s2 -> compare s1 s2 = 0
418
  | HCOR (f1a, f1b), HCOR (f2a, f2b)
419
  | HCAND (f1a, f1b), HCAND (f2a, f2b) -> f1a == f2a && f1b == f2b
420
  | HCEXISTS (s1, f1), HCEXISTS (s2, f2)
421
  | HCFORALL (s1, f1), HCFORALL (s2, f2) -> compare s1 s2 = 0 && f1 == f2
422
(* The rest could be shortened to | _ -> false,
423
   but then the compiler would not warn if the formula type is extended
424
   and this function is not updated accordingly.*)
425
  | HCTRUE, _
426
  | HCFALSE, _
427
  | HCAP _, _
428
  | HCNOT _, _
429
  | HCOR _, _
430
  | HCAND _, _
431
  | HCEXISTS _, _
432
  | HCFORALL _, _ -> false
433

    
434
(** Computes the hash value of a formula node.
435
    @param f A formula node.
436
    @return The hash value of f.
437
 *)
438
let hash_hcConcept_node f =
439
  match f with
440
  | HCTRUE -> 0
441
  | HCFALSE -> 1
442
  | HCAP s -> 19 * Hashtbl.hash s + 0
443
  | HCNOT s -> 19 * Hashtbl.hash s + 1
444
  | HCOR (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 2
445
  | HCAND (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 3
446
  | HCEXISTS (s, f1) -> 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 4
447
  | HCFORALL (s, f1) -> 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 5
448

    
449
(** Determines the "real" formula of a formula node.
450
    @param f A formula node.
451
    @return The formula (in negation normal form) which corresponds to f.
452
 *)
453
let toFml_hcConcept_node f =
454
  match f with
455
  | HCTRUE -> TRUE
456
  | HCFALSE -> FALSE
457
  | HCAP s -> AP s
458
  | HCNOT s -> NOT s.HC.fml
459
  | HCOR (f1, f2) -> OR (f1.HC.fml, f2.HC.fml)
460
  | HCAND (f1, f2) -> AND (f1.HC.fml, f2.HC.fml)
461
  | HCEXISTS (s, f1) -> EXISTS (s, f1.HC.fml)
462
  | HCFORALL (s, f1) -> FORALL (s, f1.HC.fml)
463

    
464
(** An instantiation of hash-consing for formulae.
465
 *)
466
module HcFormula = HC.Make(
467
  struct
468
    type nde = hcConcept_node
469
    type fml = concept
470
    let equal (n1 : nde) n2 = equal_hcConcept_node n1 n2
471
    let hash (n : nde) = hash_hcConcept_node n
472
    let negNde (n : nde) = n (*negNde_hcConcept_node n*)
473
    let toFml (n : nde) = toFml_hcConcept_node n
474
  end
475
 )
476

    
477
(** Converts a formula into its hash-consed version.
478
    @param hcF A hash-cons table for formulae.
479
    @param f A formula in negation normal form.
480
    @return The hash-consed version of f.
481
    @raise CoAlgException if f is not in negation normal form.
482
*)
483
let rec hc_formula hcF f =
484
  match f with
485
  | TRUE -> HcFormula.hashcons hcF HCTRUE
486
  | FALSE -> HcFormula.hashcons hcF HCFALSE
487
  | AP s -> HcFormula.hashcons hcF (HCAP s)
488
  | NOT s -> HcFormula.hashcons hcF (HCNOT (hc_formula hcF s))
489
  | OR (f1, f2) ->
490
      let tf1 = hc_formula hcF f1 in
491
      let tf2 = hc_formula hcF f2 in
492
      HcFormula.hashcons hcF (HCOR (tf1, tf2))
493
  | AND (f1, f2) ->
494
      let tf1 = hc_formula hcF f1 in
495
      let tf2 = hc_formula hcF f2 in
496
      HcFormula.hashcons hcF (HCAND (tf1, tf2))
497
  | EXISTS (s, f1) ->
498
      let tf1 = hc_formula hcF f1 in
499
      HcFormula.hashcons hcF (HCEXISTS (s, tf1))
500
  | FORALL (s, f1) ->
501
      let tf1 = hc_formula hcF f1 in
502
      HcFormula.hashcons hcF (HCFORALL (s, tf1))
503

    
504

    
505
(** An instantiation of a hash table (of the standard library)
506
    for hash-consed formulae. The test for equality
507
    and computing the hash value is done in constant time.
508
 *)
509
module HcFHt = Hashtbl.Make(
510
  struct
511
    type t = hcConcept
512
    let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag
513
    let hash (f : t) = f.HC.tag
514
  end
515
 )
516

    
517
type hcAsst =
518
  | HCROLE of int * int * int
519
  | HCCONCEPT of int * hcConcept
520
type hcAssertion = (hcAsst list) * int * (hcAsst list)
521

    
522
let toAsst asst =
523
  match asst with
524
  | HCROLE(a, b, c) -> ROLE(a, b, c)
525
  | HCCONCEPT(a, hcFml) -> CONCEPT(a, hcFml.fml)
526

    
527
(*
528
let toAsst xs =
529
  let f (left, gr, right) =
530
    let g hcasst =
531
      match hcasst with
532
      | HCROLE(a, b, c) -> ROLE(a, b, c)
533
      | HCCONCEPT(a, hcFml) -> CONCEPT(a, hcFml.fml)
534
    in
535
    (List.map g left, gr, List.map g right)
536
  in
537
  List.map f xs
538
  *)
539

    
540
let toHcAsst hcF asst =
541
  match asst with
542
  | ROLE(a, b, c) -> HCROLE(a, b, c)
543
  | CONCEPT(a, c) -> HCCONCEPT(a, hc_formula hcF c)