Project

General

Profile

Statistics
| Branch: | Revision:

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

History | View | Annotate | Download (31.5 KB)

1
(** Common functions and data structures
2
    which are shared by the decision procedures for ALC-satisfiability.
3
    @author Florian Widmann
4
 *)
5

    
6

    
7
module A = ALCFormula
8
module HC = HashConsing
9

    
10

    
11
open MiscSolver
12

    
13

    
14
(** This exception is thrown when the status of the root node in the graph
15
    becomes (un)satisfiable and the procedure can stop.
16
 *)
17
exception ALC_finished of bool
18

    
19

    
20
(** This table maps integers (representing formulae) to their corresponding formulae.
21
 *)
22
let arrayFormula = ref (Array.make 0 A.TRUE)
23

    
24
(** This lookup table maps EX/AX-formulae to their inverse concept.
25
 *)
26
let arrayInv = ref (Array.make 0 (-1))
27

    
28
(** This table maps integers (representing formulae) to their corresponding definitions.
29
 *)
30
let arrayDef = ref (Array.make 0 (-1))
31

    
32

    
33
(** The lowest integer representing an OR-formula.
34
 *)
35
let lposOR = ref (-1)
36

    
37
(** The greatest integer representing an OR-formula.
38
 *)
39
let hposOR = ref (-1)
40

    
41

    
42
(** A dependency is defined between two nodes: a node n and one of its children c.
43
    It maps some formulae f of c to the formulae of n that caused the creation of f.
44
    If n is an or-node, formulae of c that are not mapped are implicitly assumed
45
    to map to themselves (and are hence in n and c).
46
    If n is a state, formulae of c that are not mapped do not derive from 
47
    formulae in c but are inserted because of the TBox.
48
    If n is a state the value -1 (which is not a formula) is mapped to the
49
    <>-formula in n that caused the creation of c.
50
 *)
51
type dependency = (int list) FMap.t
52

    
53
(** An empty dependency map.
54
 *)
55
let (emptyDep : dependency) = FMap.empty
56

    
57
(** Returns the dependencies of a formula.
58
    @param dep A dependency map.
59
    @param f A formula.
60
    @return The list of formulae assigned to f in dep.
61
    @raise Not_found If nothing is assigned to f in dep.
62
 *)
63
let findDep (dep : dependency) f = FMap.find f dep
64

    
65
(** Adds new dependencies for a formula to a dependency map.
66
    Old dependencies for the formula are overridden.
67
    @param dep A dependency map.
68
    @param f The formula that gets new dependencies.
69
    @param fl A list of formulae that is assigned to f in dep.
70
    @return A dependency map that assigns fl to f
71
    and behaves like dep otherwise.
72
 *)
73
let addDep (dep : dependency) f fl = FMap.add f fl dep
74

    
75
(** Converts a dependency map into a string representation.
76
    @param expF A function which converts the formula in integer
77
    representations into a readable string.
78
    @param dep A dependency map.
79
    @return A string representing dep.
80
 *)
81
let exportDep expF dep =
82
  let expFl fl = List.map expF fl in
83
  let fld k e acc =
84
    let kstr = if k = (-1) then "-1" else expF k in
85
    let estr = exportAsSet "" expFl e in
86
    (kstr ^ " --> " ^ estr)::acc
87
  in
88
  let expD d = FMap.fold fld d [] in
89
  exportAsSet "" expD dep
90

    
91

    
92
(** Tests whether a formula is an element of a set of formulae.
93
    The function takes into account that and-formulae are split automatically.
94
    An or-formula is considered to be in the set
95
    if one of its subformulae is in the set (this applies recursively).
96
    Atomic concepts that are defined in the definitional TBox
97
    are expanded automatically.
98
    @param fs A bitset of formulae.
99
    @param f The integer representation of a formula.
100
    @return True iff f is an element of fs.
101
 *)
102
let rec containsFormula fs f = 
103
  match !arrayType.(f) with
104
  | 5 ->
105
      containsFormula fs !arrayDest1.(f) &&
106
      containsFormula fs !arrayDest2.(f)
107
  | 4 ->
108
      (memBS fs f ||
109
      containsFormula fs !arrayDest1.(f) ||
110
      containsFormula fs !arrayDest2.(f))
111
  | 2 ->
112
      if memBS fs f then true
113
      else
114
        let fdef = !arrayDef.(f) in
115
        if fdef >= 0 && !arrayDef.(!arrayNeg.(f)) >= 0 then
116
          containsFormula fs fdef
117
        else false
118
  | 3 ->
119
      if memBS fs f then true
120
      else
121
        let fdef = !arrayDef.(f) in
122
        if fdef >= 0 then containsFormula fs fdef else false
123
  | _ -> memBS fs f
124

    
125
let containsFormulaChk fs f = f >= 0 && containsFormula fs f
126

    
127
(** Tests whether a formula is an element of a set of formulae.
128
    The function takes into account that and-formulae are split automatically.
129
    An or-formula is considered to be in the set
130
    if one of its subformulae is in the set (this applies recursively).
131
    Atomic concepts that are defined in the definitional TBox
132
    are expanded automatically.
133
    @param fs A bitset of formulae.
134
    @param f The integer representation of a formula.
135
    @return None iff f is not an element of fs;
136
    Some l iff f is an element of fs
137
    where l is a list of formula in fs that "make up" f.
138
 *)
139
let rec containsFormulaDep fs f = 
140
  match !arrayType.(f) with
141
  | 5 -> begin
142
      let res1 = containsFormulaDep fs !arrayDest1.(f) in
143
      match res1 with
144
      | Some l1 -> begin
145
          let res2 = containsFormulaDep fs !arrayDest2.(f) in
146
          match res2 with
147
          | Some l2 -> Some (l1 @ l2)
148
          | None -> None
149
      end
150
      | None -> None
151
  end
152
  | 4 -> 
153
      if memBS fs f then Some [f]
154
      else begin
155
        let res1 = containsFormulaDep fs !arrayDest1.(f) in
156
        match res1 with
157
        | Some _ -> res1
158
        | None -> containsFormulaDep fs !arrayDest2.(f)
159
      end
160
  | 2 ->
161
      if memBS fs f then Some [f]
162
      else
163
        let fdef = !arrayDef.(f) in
164
        if fdef >= 0 && !arrayDef.(!arrayNeg.(f)) >= 0 then
165
          containsFormulaDep fs fdef
166
        else None
167
  | 3 ->
168
      if memBS fs f then Some [f]
169
      else
170
        let fdef = !arrayDef.(f) in
171
        if fdef >= 0 then containsFormulaDep fs fdef else None
172
  | _ -> if memBS fs f then Some [f] else None
173

    
174
let containsFormulaDepChk fs f = 
175
  if f >= 0 then containsFormulaDep fs f else None
176

    
177

    
178
(** Adds a formula to a set of formulae.
179
    And-formulae are split, i.e. both their direct subformulae are inserted
180
    (and maybe split themselves recursively).
181
    Atomic concepts that are defined in the definitional TBox
182
    are expanded automatically.
183
    If a contradiction is found, the state of fs is undefined.
184
    @param fs A bitset of formulae.
185
    @param f The integer representation of a formula that is to be added to bs.
186
    @return True iff inserting f into fs causes a contradiction.
187
 *)
188
let rec insertFormula fs f =
189
  match !arrayType.(f) with
190
  | 5 ->
191
      let notf = !arrayNeg.(f) in
192
      ((notf >= 0 && memBS fs notf) ||
193
      insertFormula fs !arrayDest1.(f) ||
194
      insertFormula fs !arrayDest2.(f))
195
  | 4 ->
196
      addBSNoChk fs f;
197
      containsFormulaChk fs !arrayNeg.(f)
198
  | 2
199
  | 3 ->
200
      let fdef = !arrayDef.(f) in
201
      if fdef >= 0 then addBS fs f || insertFormula fs fdef
202
      else addBS fs f
203
  | _ -> addBS fs f
204

    
205
(** Adds a formula to a set of formulae.
206
    And-formulae are split, i.e. both their direct subformulae are inserted
207
    (and maybe split themselves recursively).
208
    Atomic concepts that are defined in the definitional TBox
209
    are expanded automatically.
210
    If a contradiction is found, the state of fs is undefined.
211
    @param fs A bitset of formulae.
212
    @param f The integer representation of a formula that is to be added to bs.
213
    @param dep The dependency map of fs.
214
    @param fDepl A list of formula that f depends on.
215
    @return A pair (ndep, cntr) where
216
    ndep is the new dependency map of fs 
217
    (that is it extends dep such that all formula
218
    that are actually inserted into fs have fDepl as their dependencies); and
219
    cntr is None iff inserting f into fs did not cause a contradiction,
220
    and Some cfs otherwise where cfs is a "minimal subset" of fs
221
    that already contains the contradiction.
222
 *)
223
let rec insertFormulaDep fs f dep fDepl =
224
  match !arrayType.(f) with
225
  | 5 -> begin
226
      let (dep1, cntr1) as res1 = insertFormulaDep fs !arrayDest1.(f) dep fDepl in
227
      match cntr1 with
228
      | None -> begin
229
          let (dep2, cntr2) as res2 = insertFormulaDep fs !arrayDest2.(f) dep1 fDepl in
230
          match cntr2 with
231
          | None -> 
232
              let notf = !arrayNeg.(f) in
233
              if notf >= 0 && memBS fs notf then
234
                let dep3 = addDep dep2 f fDepl in
235
                let cfs = makeBS () in
236
                addBSNoChk cfs f;
237
                addBSNoChk cfs notf;
238
                (dep3, Some cfs)
239
              else res2
240
          | Some _ -> res2
241
      end
242
      | Some _ -> res1
243
  end
244
  | 4 -> begin
245
      let dep1 = if memBS fs f then dep else addDep dep f fDepl in
246
      addBSNoChk fs f;
247
      let iscont = containsFormulaDepChk fs !arrayNeg.(f) in
248
      match iscont with
249
      | None -> (dep1, None)
250
      | Some notfl ->
251
          let cfs = makeBS () in
252
          addBSNoChk cfs f;
253
          List.iter (addBSNoChk cfs) notfl;
254
          (dep1, Some cfs)
255
  end
256
  | 2
257
  | 3 ->
258
      let dep1 = if memBS fs f then dep else addDep dep f fDepl in
259
      if addBS fs f then
260
        let cfs = makeBS () in
261
        addBSNoChk cfs f;
262
        if f <> !bsfalse then addBSNoChk cfs !arrayNeg.(f) else ();
263
        (dep1, Some cfs)
264
      else
265
        let fdef = !arrayDef.(f) in
266
        if fdef >= 0 then insertFormulaDep fs fdef dep1 fDepl
267
        else (dep1, None)
268
  | _ ->
269
      let dep1 = if memBS fs f then dep else addDep dep f fDepl in
270
      if addBS fs f then
271
        let cfs = makeBS () in
272
        addBSNoChk cfs f;
273
        if f <> !bsfalse then addBSNoChk cfs !arrayNeg.(f) else ();
274
        (dep1, Some cfs)
275
      else (dep1, None)
276

    
277

    
278
(** Removes or-formulae from a set
279
    if one of its direct subformulae are already in the set,
280
    or replaces them by one of its direct subformulae
281
    if the negation of the other direct subformula is in the set.
282
    @param fs A set of formulae.
283
    @return True if a contradiction is detected in fs.
284
 *)
285
let rec subsume fs =
286
  let rec chkOr bnd acc i =
287
    if i <= bnd then
288
      if memBS fs i then
289
        let f1 = !arrayDest1.(i) in
290
        let f2 = !arrayDest2.(i) in
291
        if containsFormula fs f1 || containsFormula fs f2 then begin
292
          remBS fs i;
293
          chkOr bnd acc (succ i)
294
        end
295
        else
296
          let iscont1 = containsFormulaChk fs !arrayNeg.(f1) in
297
          if iscont1 then begin
298
            remBS fs i;
299
            if insertFormula fs f2 then 1 else chkOr bnd 2 (succ i)
300
          end
301
          else
302
            let iscont2 = containsFormulaChk fs !arrayNeg.(f2) in
303
            if iscont2 then begin
304
              remBS fs i;
305
              if insertFormula fs f1 then 1 else chkOr bnd 2 (succ i)
306
            end
307
            else chkOr bnd acc (succ i)
308
      else chkOr bnd acc (succ i)
309
    else acc
310
  in
311
  match chkOr !hposOR 0 !lposOR with
312
  | 0 -> false
313
  | 1 -> true
314
  | _ -> subsume fs
315

    
316
(** Removes or-formulae from a set
317
    if one of its direct subformulae are already in the set,
318
    or replaces them by one of its direct subformulae
319
    if the negation of the other direct subformula is in the set.
320
    @param isor True iff the node that is responsible
321
    for invoking this function is an or-node (otherwise it is a state).
322
    @param dep The dependency map of fs.
323
    @param fs A set of formulae.
324
    @return A pair (ndep, cntr) where
325
    ndep is the new dependency map of fs; and
326
    cntr is None iff the subsumption did not cause a contradiction,
327
    and Some cfs otherwise where cfs is a "minimal subset" of fs
328
    that already contains the contradiction.
329
 *)
330
let rec subsumeDep isor dep fs =
331
  let subsumeFold dep acc f =
332
    try
333
      let dl = findDep dep f in
334
      dl @ acc
335
    with Not_found -> if isor then f::acc else acc
336
  in
337
  let rec chkOr bnd acc i dep =
338
    if i <= bnd then
339
      if memBS fs i then
340
        let f1 = !arrayDest1.(i) in
341
        let f2 = !arrayDest2.(i) in
342
        if containsFormula fs f1 || containsFormula fs f2 then begin
343
          remBS fs i;
344
          chkOr bnd acc (succ i) dep
345
        end
346
        else
347
          let iscont1 = containsFormulaDepChk fs !arrayNeg.(f1) in
348
          match iscont1 with
349
          | Some negf1l -> begin
350
              remBS fs i;
351
              let f2Depl = List.fold_left (subsumeFold dep) [] (i::negf1l) in
352
              let (dep1, cntr1) as res1 = insertFormulaDep fs f2 dep f2Depl in
353
              match cntr1 with
354
              | None -> chkOr bnd true (succ i) dep1
355
              | Some _ -> (true, res1)
356
          end
357
          | None ->
358
              let iscont2 = containsFormulaDepChk fs !arrayNeg.(f2) in
359
                match iscont2 with
360
                | Some negf2l -> begin
361
                    remBS fs i;
362
                    let f1Depl = List.fold_left (subsumeFold dep) [] (i::negf2l) in
363
                    let (dep2, cntr2) as res2 = insertFormulaDep fs f1 dep f1Depl in
364
                    match cntr2 with
365
                    | None -> chkOr bnd true (succ i) dep2
366
                    | Some _ -> (false, res2)
367
                end
368
                | None -> chkOr bnd acc (succ i) dep
369
      else chkOr bnd acc (succ i) dep
370
    else (acc, (dep, None))
371
  in
372
  let (modified, ((dep3, contr3) as res3)) = chkOr !hposOR false !lposOR dep in
373
  match contr3 with
374
  | None -> if modified then subsumeDep isor dep3 fs else res3
375
  | Some _ -> res3
376

    
377
(** Invokes subsume on a set unless it already contains a contradiction.
378
    @param isor True iff the node that is responsible
379
    for invoking this function is an or-node (otherwise it is a state).
380
    @param fs A set of formulae.
381
    @param dep The dependency map of fs.
382
    @param cntr None iff fs does not contain a contradiction.
383
    @return If cntr is not None then (dep, cntr),
384
    otherwise a pair (ndep, ncntr) where
385
    ndep is the new dependency map of fs; and
386
    cntr is None iff the subsumption did not cause a contradiction,
387
    and Some cfs otherwise where cfs is a "minimal subset" of fs
388
    that already contains the contradiction.
389
*)
390
let testSubsume isor fs ((dep, cntr) as res) =
391
  match cntr with
392
  | None -> subsumeDep isor dep fs
393
  | Some _ -> res
394

    
395

    
396
(** Creates a "minimal" contradictory set for a node
397
    according to a "minimal" contradictory set of a child
398
    and a corresponding dependency map.
399
    @param isor True iff the node that is responsible
400
    for invoking this function is an or-node (otherwise it is a state).
401
    @param ocfs The "minimal" contradictory set of a child.
402
    @param dep The corresponding dependency map.
403
    @param ncfs The resulting "minimal" contradictory set of a child.
404
    It does not have to be empty (e.g. for or-formula
405
    this function is invoked twice).
406
 *)
407
let makeCSDep isor ocfs dep ncfs =
408
  for i = 0 to pred !nrFormulae do
409
    if memBS ocfs i then
410
      try
411
        let dl = findDep dep i in
412
        List.iter (addBSNoChk ncfs) dl
413
      with Not_found -> if isor then addBSNoChk ncfs i else ()
414
    else ()
415
  done
416

    
417

    
418
(** Adds all [a]-formulae of a set, where a is a given program,
419
    to another set after stripping the outermost [a].
420
    If a contradiction is found the result may not contain
421
    all stripped [a]-formulae.
422
    @param bs The bitset of formulae containing the [a]-formulae.
423
    @param ap The integer representation of an atomic program.
424
    @param nbs The bitset to which the stripped [a]-formulae are added.
425
    @param bnd The greatest integer representing a [a]-formula.
426
    @param i The current index of the array.
427
    @return True iff adding the formulae to nbs caused a contradiction.
428
 *)
429
let rec intern_mkDelta bs ap nbs bnd i =
430
  if i <= bnd then
431
    if memBS bs i && ap = !arrayDest2.(i) then
432
      if insertFormula nbs !arrayDest1.(i) then true
433
      else intern_mkDelta bs ap nbs bnd (succ i)
434
    else intern_mkDelta bs ap nbs bnd (succ i)
435
  else false
436

    
437
let mkDelta bs ap nbs = intern_mkDelta bs ap nbs !hposAX !lposAX
438

    
439
(** Adds all [a]-formulae of a set, where a is a given atomic program,
440
    to another set after stripping the outermost [a].
441
    If a contradiction is found the result may not contain
442
    all stripped [a]-formulae.
443
    @param bs The bitset of formulae containing the [a]-formulae.
444
    @param ap The integer representation of an atomic program.
445
    @param dep The dependency map of bs.
446
    @param nbs The bitset to which the stripped [a]-formulae are added.
447
    @param bnd The greatest integer representing a [a]-formula.
448
    @param i The current index of the array.
449
    @return A pair (ndep, cntr) where
450
    ndep is the new dependency map of bs; and
451
    cntr is None iff inserting the formulae did not cause a contradiction,
452
    and Some cfs otherwise where cfs is a "minimal subset" of bs
453
    that already contains the contradiction.
454
 *)
455
let rec intern_mkDeltaDep bs ap dep nbs bnd i =
456
  if i <= bnd then
457
    if memBS bs i && ap = !arrayDest2.(i) then
458
      let (dep1, cntr1) as res1 = insertFormulaDep nbs !arrayDest1.(i) dep [i] in
459
      match cntr1 with
460
      | None -> intern_mkDeltaDep bs ap dep1 nbs bnd (succ i)
461
      | Some _ -> res1
462
    else intern_mkDeltaDep bs ap dep nbs bnd (succ i)
463
  else (dep, None)
464

    
465
(** For a principal formula <a>A,
466
    this function adds A and all [a]-formulae of a set
467
    to another set (which may already contain formulae of a TBox)
468
    after stripping the outermost [a].
469
    If a contradiction is found the result may not contain
470
    all stripped [a]-formulae.
471
    @param bs The bitset of formulae containing the [a]-formulae.
472
    @param pf The principal formula.
473
    @param nbs The bitset to which the formulae are added.
474
    @return A pair (ndep, cntr) where
475
    ndep is the new dependency map of bs; and
476
    cntr is None iff inserting the formulae did not cause a contradiction,
477
    and Some cfs otherwise where cfs is a "minimal subset" of bs
478
    that already contains the contradiction.
479
 *)
480
let mkDeltaDep bs pf nbs =
481
  let f = !arrayDest1.(pf) in
482
  let (dep, cntr) as res = insertFormulaDep nbs f emptyDep [pf] in
483
  match cntr with
484
  | None ->
485
      let ap = !arrayDest2.(pf) in
486
      intern_mkDeltaDep bs ap dep nbs !hposAX !lposAX
487
  | Some _ -> res
488

    
489

    
490
(** Extends a pair by a third element and adds the result to a list.
491
    @param c The element that is added to (a, b).
492
    @param lst A list of triples.
493
    @param (a, b) A pair.
494
    @return (a, b, c)::lst
495
 *)
496
let addTuple c lst (a, b) = (a, b, c)::lst
497

    
498

    
499
(** Test whether all AX-formulae of a set of formulae
500
    stripped of their outermost [r]
501
    are contained in another set of formulae.
502
    @param bs1 The bitset of formulae containing the AX-formulae.
503
    @param bs2 The other bitset.
504
    @param ap The integer representation of a role.
505
    @param bnd The greatest integer representing a [a]-formula.
506
    @param i The current index of the array.
507
    @return True iff all formula (as described above) are contained in bs2.
508
 *)
509
let rec intern_isConsistent bs1 bs2 ap bnd i =
510
  if i <= bnd then
511
    if memBS bs1 i && ap = !arrayDest2.(i) then
512
      if containsFormula bs2 !arrayDest1.(i) then
513
        intern_isConsistent bs1 bs2 ap bnd (succ i)
514
      else false
515
    else intern_isConsistent bs1 bs2 ap bnd (succ i)
516
  else true
517

    
518
let isConsistent bs1 bs2 ap = intern_isConsistent bs1 bs2 ap !hposAX !lposAX
519

    
520

    
521
(** Initialises the arrays for a formula and its integer representation.
522
    @param htF A hashtable that maps formulae to their integer representation.
523
    @param htR A hashtable that maps role names to their integer representation.
524
    @param tboxD A list of definitions
525
    representing the definitional part of a TBox.
526
    The definitions must not be cyclic
527
    and each concept must not be defined more than once.
528
    @param f A formula.
529
    @param n The integer representation of f.
530
    @raise ACLException if f is not in negation normal form.
531
 *)
532
let initTables htF htR tboxD f n = 
533
  let rec getDef isneg cn = function
534
    | [] -> None
535
    | h::tl ->
536
        match h with
537
        | A.PRIMITIVE (s, f) ->
538
            if cn = s then
539
              if not isneg then Some f else None
540
            else getDef isneg cn tl
541
        | A.NECANDSUFF (s, f) ->
542
            if cn = s then Some f
543
            else getDef isneg cn tl
544
  in
545
  !arrayFormula.(n) <- f;
546
  let fneg = A.nnfNeg f in
547
  if Hashtbl.mem htF fneg then !arrayNeg.(n) <- Hashtbl.find htF fneg else ();
548
  match f with
549
  | A.TRUE -> !arrayType.(n) <- 0
550
  | A.FALSE -> !arrayType.(n) <- 1
551
  | A.AP s -> begin
552
      !arrayType.(n) <- 2;
553
      let defopt = getDef false s tboxD in
554
      match defopt with
555
      | None -> ()
556
      | Some fdef -> !arrayDef.(n) <- Hashtbl.find htF fdef
557
  end
558
  | A.NOT (A.AP s) -> begin
559
      !arrayType.(n) <- 3;
560
      let defopt = getDef true s tboxD in
561
      match defopt with
562
      | None -> ()
563
      | Some nfdef ->
564
          let fdef = A.nnfNeg nfdef in
565
          !arrayDef.(n) <- Hashtbl.find htF fdef
566
  end
567
  | A.OR (f1, f2) ->
568
      !arrayType.(n) <- 4;
569
      !arrayDest1.(n) <- Hashtbl.find htF f1;
570
      !arrayDest2.(n) <- Hashtbl.find htF f2
571
  | A.AND (f1, f2) ->
572
      !arrayType.(n) <- 5;
573
      !arrayDest1.(n) <- Hashtbl.find htF f1;
574
      !arrayDest2.(n) <- Hashtbl.find htF f2
575
  | A.EX (s, inv, f1) -> 
576
      !arrayType.(n) <- 6;
577
      !arrayDest1.(n) <- Hashtbl.find htF f1;
578
      !arrayDest2.(n) <- 
579
        if Hashtbl.mem htR (s, inv) then Hashtbl.find htR (s, inv)
580
        else begin
581
          let size = Hashtbl.length htR in
582
          Hashtbl.add htR (s, inv) size;
583
          size
584
        end;
585
      !arrayInv.(n) <- 
586
        let ninv = not inv in
587
        if Hashtbl.mem htR (s, ninv) then Hashtbl.find htR (s, ninv)
588
        else
589
          let size = Hashtbl.length htR in
590
          Hashtbl.add htR (s, ninv) size;
591
          size
592
  | A.AX (s, inv, f1) ->
593
      !arrayType.(n) <- 7;
594
      !arrayDest1.(n) <- Hashtbl.find htF f1;
595
      !arrayDest2.(n) <-
596
        if Hashtbl.mem htR (s, inv) then Hashtbl.find htR (s, inv)
597
        else begin
598
          let size = Hashtbl.length htR in
599
          Hashtbl.add htR (s, inv) size;
600
          size
601
        end;
602
      !arrayInv.(n) <- 
603
        let ninv = not inv in
604
        if Hashtbl.mem htR (s, ninv) then Hashtbl.find htR (s, ninv)
605
        else
606
          let size = Hashtbl.length htR in
607
          Hashtbl.add htR (s, ninv) size;
608
          size
609
  | _ -> raise (A.ALCException "Formula is not in negation normal form.")
610

    
611
(** Initialises the arrays for a formula and its integer representation.
612
    @param hcF A hash-cons table.
613
    @param htF A hashtable that maps formulae to their integer representation.
614
    @param htR A hashtable that maps role names to their integer representation.
615
    @param tboxD A list of definitions
616
    representing the definitional part of a TBox.
617
    The definitions must not be cyclic
618
    and each concept must not be defined more than once.
619
    @param f A hash-consed formula (in negation normal form).
620
    @param n The integer representation of f.
621
 *)
622
let initTablesHc hcF htF htR tboxD f n =
623
  let rec getDef isneg cn = function
624
    | [] -> None
625
    | (true, s, f)::tl ->
626
        if cn = s then
627
          if not isneg then Some f else None
628
        else getDef isneg cn tl
629
    | (false, s, f)::tl ->
630
        if cn = s then Some f
631
        else getDef isneg cn tl
632
  in
633
  !arrayFormula.(n) <- f.HC.fml;
634
  let fneg = f.HC.neg in
635
  if A.HcFHt.mem htF fneg then
636
    !arrayNeg.(n) <- A.HcFHt.find htF fneg;
637
  match f.HC.node with
638
  | A.HCTRUE -> !arrayType.(n) <- 0
639
  | A.HCFALSE -> !arrayType.(n) <- 1
640
  | A.HCAP s -> begin
641
      !arrayType.(n) <- 2;
642
      let defopt = getDef false s tboxD in
643
      match defopt with
644
      | None -> ()
645
      | Some fdef -> !arrayDef.(n) <- A.HcFHt.find htF fdef
646
    end
647
  | A.HCNOT s -> begin
648
      !arrayType.(n) <- 3;
649
      let defopt = getDef true s tboxD in
650
      match defopt with
651
      | None -> ()
652
      | Some nfdef ->
653
          let fdef = nfdef.HC.neg in
654
          !arrayDef.(n) <- A.HcFHt.find htF fdef
655
  end
656
  | A.HCOR (f1, f2) ->
657
      !arrayType.(n) <- 4;
658
      !arrayDest1.(n) <- A.HcFHt.find htF f1;
659
      !arrayDest2.(n) <- A.HcFHt.find htF f2
660
  | A.HCAND (f1, f2) ->
661
      !arrayType.(n) <- 5;
662
      !arrayDest1.(n) <- A.HcFHt.find htF f1;
663
      !arrayDest2.(n) <- A.HcFHt.find htF f2
664
  | A.HCEX (s, inv, f1) -> 
665
      !arrayType.(n) <- 6;
666
      !arrayDest1.(n) <- A.HcFHt.find htF f1;
667
      !arrayDest2.(n) <- 
668
        if Hashtbl.mem htR (s, inv) then Hashtbl.find htR (s, inv)
669
        else begin
670
          let size = Hashtbl.length htR in
671
          Hashtbl.add htR (s, inv) size;
672
          size
673
        end;
674
      !arrayInv.(n) <- 
675
        let ninv = not inv in
676
        if Hashtbl.mem htR (s, ninv) then Hashtbl.find htR (s, ninv)
677
        else
678
          let size = Hashtbl.length htR in
679
          Hashtbl.add htR (s, ninv) size;
680
          size
681
  | A.HCAX (s, inv, f1) ->
682
      !arrayType.(n) <- 7;
683
      !arrayDest1.(n) <- A.HcFHt.find htF f1;
684
      !arrayDest2.(n) <-
685
        if Hashtbl.mem htR (s, inv) then Hashtbl.find htR (s, inv)
686
        else begin
687
          let size = Hashtbl.length htR in
688
          Hashtbl.add htR (s, inv) size;
689
          size
690
        end;
691
      !arrayInv.(n) <- 
692
        let ninv = not inv in
693
        if Hashtbl.mem htR (s, ninv) then Hashtbl.find htR (s, ninv)
694
        else
695
          let size = Hashtbl.length htR in
696
          Hashtbl.add htR (s, ninv) size;
697
          size
698

    
699
(** Converts the formula in the given lists in negation normal form
700
    and simplifies them.
701
    Initialises the internal tables of this module.
702
    @param fl The list of initial formulae that are to be tested for satisfiability.
703
    @param tboxND A list of formulae representing
704
    the non-definitional part of a TBox.
705
    @param tboxD A list of definitions
706
    representing the definitional part of a TBox.
707
    The definitions must not be cyclic
708
    and each concept must not be defined more than once.
709
    @param rankingF A complete ranking of the different types of formulae.
710
    @param noty The number of types in rankingF,
711
    starting from the beginning of the list,
712
    whose formulae are stored in the bitsets explicitly.
713
    @param allowIR Indicates whether inverse roles are allowed.
714
    @return A tuple (nfl, ntbND, ntbD, initset, tbox, cntr) where:
715
    nfl is the result of converting all formulae in fl in negation normal form
716
    and simplifying them;
717
    ntboxl is the result of converting all formulae in tboxND in negation normal form
718
    and simplifying them;
719
    ntboxD is the result of converting all formulae in tboxD in negation normal form
720
    and simplifying them;
721
    initset is a bitset containing the formulae in nfl and ntbND (in integer representation);
722
    tbox is a bitset containing the formulae in ntboxl (in integer representation);
723
    cntr is smaller than 0 iff initset contains a contradiction.
724
    @raise A.ALCException If fl is the empty list.
725
 *)
726
let ppFormulae fl tboxND tboxD rankingF noty allowIR =
727
  let testD = function
728
    | A.PRIMITIVE (_, f)
729
    | A.NECANDSUFF (_, f) -> A.containsInverse f
730
  in
731
  if (not allowIR) &&
732
    (List.exists A.containsInverse fl || List.exists A.containsInverse tboxND || List.exists testD tboxD)
733
  then raise (A.ALCException "Query contains inverse roles.") else ();
734
  if fl = [] then raise (A.ALCException "Initial formula list is empty.") else ();
735
  let mapD g = function
736
    | A.PRIMITIVE (s, f) -> A.PRIMITIVE (s, g f)
737
    | A.NECANDSUFF (s, f) -> A.NECANDSUFF (s, g f)
738
  in
739
  let nfl = List.map A.nnf fl in
740
  let ntboxND = List.map A.nnf tboxND in
741
  let ntboxD = List.map (mapD A.nnf) tboxD in
742
  let nfl = List.map A.simplifyFormula nfl in
743
  let ntboxND = List.map A.simplifyFormula ntboxND in
744
  let ntboxD = List.map (mapD A.simplifyFormula) ntboxD in
745
(*
746
  let compF = A.generateCompare A.aRanking in
747
  let module FSet = Set.Make(
748
    struct
749
      type t = A.formula
750
      let (compare : t -> t -> int) = compF
751
    end
752
   )
753
  in
754
  let fld acc = function
755
    | A.PRIMITIVE (s, f) ->
756
        let c = A.AP s in
757
        let notc = A.NOT c in
758
        c::f::notc::acc
759
    | A.NECANDSUFF (s, f) ->
760
        let c = A.AP s in
761
        let notc = A.NOT c in
762
        let notf = A.nnfNeg f in
763
        c::f::notc::notf::acc
764
  in
765
  let ntboxDFl = List.fold_left fld [] ntboxD in
766
  let allf = List.rev_append ntboxDFl (List.rev_append nfl ntboxND) in
767
  let ppF acc f =
768
    let fl = A.detClosure compF f in
769
    List.fold_left (fun a f -> FSet.add f a) acc fl
770
  in
771
  let getFml f = f in
772
  let module Ht = Hashtbl in
773
 *)
774

    
775
  let module FSet = Set.Make(
776
    struct
777
      type t = A.hcFormula
778
      let compare (f1 : t) f2 = compare f1.HC.tag  f2.HC.tag
779
    end
780
  )
781
  in
782
  let hcF = A.HcFormula.create ~size:100 true in
783
  let hcnfl = List.map (A.hc_formula hcF) nfl in
784
  let hcntboxND = List.map (A.hc_formula hcF) ntboxND in
785
  let mapD = function
786
    | A.PRIMITIVE (s, f) -> (true, s, A.hc_formula hcF f)
787
    | A.NECANDSUFF (s, f) -> (false, s, A.hc_formula hcF f)
788
  in
789
  let hcntboxD = List.map mapD ntboxD in
790
  let fld acc = function
791
    | (true, s, f) ->
792
        let c = A.HcFormula.hashcons hcF (A.HCAP s) in
793
        let notc = c.HC.neg in
794
        c::f::notc::acc
795
    | (false, s, f) ->
796
        let c = A.HcFormula.hashcons hcF (A.HCAP s) in
797
        let notc = c.HC.neg in
798
        let notf = f.HC.neg in
799
        c::f::notc::notf::acc
800
  in
801
  let hcntboxDFl = List.fold_left fld [] hcntboxD in
802
  let allf = List.rev_append hcntboxDFl (List.rev_append hcnfl hcntboxND) in
803
  let ppF acc f =
804
    let fl = A.detClosureHc hcF f in
805
    List.fold_left (fun a f -> FSet.add f a) acc fl
806
  in
807
  let getFml f = f.HC.fml in
808
  let module Ht = A.HcFHt in
809

    
810
  let fset = List.fold_left ppF FSet.empty allf in
811
  let noF = Array.make A.numberOfTypes 0 in
812
  let liter f =
813
    let ty = A.getTypeFormula (getFml f) in
814
    noF.(ty) <- succ noF.(ty)
815
  in
816
  FSet.iter liter fset;
817
  let idxF = Array.make A.numberOfTypes 0 in
818
  let len = List.fold_left (fun idx ty -> idxF.(ty) <- idx; idx + noF.(ty)) 0 rankingF in
819
  let countSize (size, idx) ty =
820
    let nsize = if idx > 0 then size + noF.(ty) else size in
821
    (nsize, pred idx)
822
  in
823
  let (size, _) = List.fold_left countSize (0, noty) rankingF in
824
  let tyEX = A.getTypeFormula (A.EX ("", false, A.TRUE)) in
825
  let idxEX = idxF.(tyEX) in
826
  let noEX = noF.(tyEX) in
827
  let tyAX = A.getTypeFormula (A.AX ("", false, A.TRUE)) in
828
  let noAX = noF.(tyAX) in
829
  let tyOR = A.getTypeFormula (A.OR (A.TRUE, A.TRUE)) in
830
  lposOR := idxF.(tyOR);
831
  hposOR := !lposOR + noF.(tyOR) - 1;
832
  arrayFormula := Array.make len A.TRUE;
833
  arrayType := Array.make len (-1);
834
  arrayDest1 := Array.make len (-1);
835
  arrayDest2 := Array.make len (-1);
836
  arrayNeg := Array.make len (-1);
837
  arrayInv := Array.make len (-1);
838
  arrayDef := Array.make len (-1);
839
  let htF = Ht.create (2 * size) in
840
  let htR = Hashtbl.create size in
841
  let fillHt f =
842
    let ty = A.getTypeFormula (getFml f) in
843
    Ht.add htF f idxF.(ty);
844
    idxF.(ty) <- succ idxF.(ty)
845
  in
846
  FSet.iter fillHt fset;
847
(*
848
  let ff = A.FALSE in
849
  let tt = A.TRUE in
850
  let nflFl = nfl in
851
  let ntboxNDFl = ntboxND in
852
  let initTbl = initTables htF htR ntboxD in
853
 *)
854

    
855
  let ff = A.HcFormula.hashcons hcF A.HCFALSE in
856
  let tt = A.HcFormula.hashcons hcF A.HCTRUE in
857
  let nflFl = hcnfl in
858
  let ntboxNDFl = hcntboxND in
859
  let initTbl = initTablesHc hcF htF htR hcntboxD in
860

    
861
  Ht.iter initTbl htF;
862
  initMisc size (Ht.find htF ff) (Ht.find htF tt) idxEX noEX noAX;
863
  let toSet bs acc f = acc || insertFormula bs (Ht.find htF f) in
864
  let tbox = makeBS () in
865
  let cntr = List.fold_left (toSet tbox) false ntboxNDFl in
866
  let initset = copyBS tbox in
867
  let cntr = List.fold_left (toSet initset) cntr nflFl in
868
  (nfl, ntboxND, ntboxD, initset, tbox, cntr)
869

    
870

    
871
(** Converts a formula into a string.
872
    @param f A formula in integer representation.
873
    @return A string representing f.
874
 *)
875
let exportF f = A.exportFormula !arrayFormula.(f)
876

    
877

    
878
(** A ranking of formulae where the and-like formulae,
879
    with the exception of [*]-formulae,
880
    are not stored in the bitsets explicitly.
881
 *)
882
let rankingNoAnd = [ A.getTypeFormula (A.OR (A.TRUE, A.TRUE));
883
                     A.getTypeFormula (A.EX ("", false, A.TRUE));
884
                     A.getTypeFormula (A.AX ("", false, A.TRUE));
885
                     A.getTypeFormula A.TRUE;
886
                     A.getTypeFormula A.FALSE;
887
                     A.getTypeFormula (A.AP "");
888
                     A.getTypeFormula (A.NOT A.TRUE);
889
                     A.getTypeFormula (A.AND (A.TRUE, A.TRUE));
890
                     A.getTypeFormula (A.EQU (A.TRUE, A.TRUE));
891
                     A.getTypeFormula (A.IMP (A.TRUE, A.TRUE)) ]
892

    
893
(** The number of types in rankingFNoAnd,
894
    starting from the beginning of the list,
895
    whose formulae are stored in the bitsets explicitly.
896
 *)
897
let notyNoAnd = 7