Project

General

Profile

Statistics
| Branch: | Revision:

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

History | View | Annotate | Download (26.8 KB)

1 4fd28192 Thorsten Wißmann
(** Common types, functions, and data structures for the CoAlgebraic reasoner.
2
    @author Florian Widmann
3
 *)
4
5
6
module S = MiscSolver
7 f1fa9ad5 Thorsten Wißmann
module L = List
8 4fd28192 Thorsten Wißmann
module C = CoAlgFormula
9
module HC = HashConsing
10
11
12
(** An instantiation of a set (of the standard library) for bitsets.
13
 *)
14
module BsSet = Set.Make(
15
  struct
16
    type t = S.bitset
17
    let (compare : t -> t -> int) = S.compareBS
18
  end
19
 )
20
21
(** An instantiation of a hash table (of the standard library) for bitsets.
22
 *)
23
module GHt = Hashtbl.Make(
24
  struct
25
    type t = S.bitset
26
    let equal (bs1 : t) bs2 = S.compareBS bs1 bs2 = 0
27
    let hash (bs : t) = S.hashBS bs
28
  end
29
 )
30
31
(** An instantiation of a hash table (of the standard library) for literals.
32
 *)
33
module LHt = Hashtbl.Make(
34
  struct
35
    type t = Minisat.lit
36
    let equal (l1 : t) l2 = l1 = l2
37
    let hash (l : t) = (l :> int)
38
  end
39
 )
40
41
(** An instantiation of a hash table (of the standard library) for formulae.
42
 *)
43
module FHt = Hashtbl.Make(
44
  struct
45
    type t = int
46
    let equal (f1 : t) f2 = f1 = f2
47
    let hash (f : t) = f
48
  end
49
 )
50
51
(** An instantiation of a hash table (of the standard library) for nominals.
52
 *)
53
module NHt = Hashtbl.Make(
54
  struct
55
    type t = int * int
56
    let equal ((s1, f1) : t) (s2, f2) = (s1 = s2) && (f1 = f2)
57
    let hash ((s, f) : t) = (((s+f)*(s+f+1)) / 2) + f
58
  end
59
)
60
61
62
(*****************************************************************************)
63
(*     Types that can be modified rather easily                              *)
64
(*     (of course you then have to modify the implementations below too)     *)
65
(*****************************************************************************)
66
67
(* This type must be extended for additional logics. *)
68
type functors =
69
  | MultiModalK
70 a87192e8 Thorsten Wißmann
  | MultiModalKD
71 f1fa9ad5 Thorsten Wißmann
  | CoalitionLogic
72 29b2e3f3 Thorsten Wißmann
  | GML
73 4fd28192 Thorsten Wißmann
  | Choice
74
  | Fusion
75
76
(* This type may be extended for additional logics. *)
77
type formulaType =
78
  | Other
79
  | ConstF
80
  | AndF
81
  | OrF
82
  | AtF
83
  | NomF
84 559819d7 Thorsten Wißmann
  | ExF  (* Existential / diamond *)
85
  | AxF  (* Universal / box *)
86 29b2e3f3 Thorsten Wißmann
  | EnforcesF (* diamond of CL *)
87
  | AllowsF   (* box of CL *)
88 af276a36 Thorsten Wißmann
  | MoreThanF (* more than n successors = diamond in gml *)
89
  | MaxExceptF(* at most n exceptions = box in gml *)
90 559819d7 Thorsten Wißmann
  | ChcF (* Choice *)
91
  | FusF (* Fusion *)
92 4fd28192 Thorsten Wißmann
93
type localFormula = int
94
type bset = S.bitset
95
96
type atFormula = int
97
type cset = S.bitset
98
type csetSet = BsSet.t
99
100
type lht = localFormula LHt.t
101
type fht = Minisat.lit FHt.t
102
type nht = bset NHt.t
103
104
type state = { sortS : sort; mutable bsS : bset; mutable statusS : nodeStatus;
105
               mutable parentsS : core list; mutable childrenS : (dependencies * core list) list;
106
               mutable constraintsS : csetSet; expandFkt : stateExpander }
107
108
and core = { sortC : sort; mutable bsC : bset; mutable statusC : nodeStatus;
109
             mutable parentsC : (state * int) list; mutable childrenC : state list;
110
             mutable constraintsC : csetSet; solver : Minisat.solver; fht : fht;
111
             mutable constraintParents : cset list }
112
113
and setState = state GHt.t
114
115
and setCore = core GHt.t
116
117
and setCnstr = unit GHt.t
118
119
120
(*****************************************************************************)
121
(*                Types that are hard coded into the algorithm               *)
122
(*****************************************************************************)
123
124
and stateExpander = unit -> ruleEnumeration
125
126
and sort = C.sort
127
128
and nodeStatus =
129
  | Expandable
130
  | Open
131
  | Sat
132
  | Unsat
133
134
and dependencies = bset list -> bset
135
and ruleEnumeration =
136
  | AllInOne of (dependencies * (sort * bset) list) list
137
  | NextRule of dependencies * (sort * bset) list
138
  | NoMoreRules
139
140
type nominal = sort * localFormula
141
142
type node =
143
  | State of state
144
  | Core of core
145
146
type constrnt =
147
  | UnsatC
148
  | SatC
149
  | OpenC of node list
150
  | UnexpandedC of node list
151
152
type propagateElement =
153
  | UState of state * int option
154
  | UCore of core * bool
155
  | UCnstr of cset
156
157
type queueElement =
158
  | QState of state
159
  | QCore of core
160
  | QCnstr of cset
161
  | QEmpty
162
163
type sortTable = (functors * int list) array
164
165
exception CoAlg_finished of bool
166
167
168
let sortTable = ref (Array.make 0 (MultiModalK, [1]))
169
170
171
(*****************************************************************************)
172
(*      "Module type" and a specific implementation of the main queue        *)
173
(*****************************************************************************)
174
175
let queueStates = ref ([] : state list)
176
let queueCores1 = ref ([] : core list)
177
let queueCores2 = ref ([] : core list)
178
let queueCnstrs = ref ([] : cset list)
179
let doPropagation = ref false
180
181
let queueInit () =
182
  queueStates := [];
183
  queueCores1 := [];
184
  queueCores2 := [];
185
  queueCnstrs := [];
186
  doPropagation := false
187
188
let queueIsEmpty () =
189
  !queueStates = [] && !queueCores1 = [] && !queueCores2 = [] && !queueCnstrs = []
190
191
let queueInsertState state = queueStates := state::!queueStates
192
193
let queueInsertCore core = queueCores2 := core::!queueCores2
194
195
let queueInsertCnstr cset = queueCnstrs := cset::!queueCnstrs
196
197
let queueGetElement () =
198
  if !queueCnstrs <> [] then
199
    let res = List.hd !queueCnstrs in
200
    queueCnstrs := List.tl !queueCnstrs;
201
    QCnstr res
202
  else if !queueStates <> [] then
203
    let res = List.hd !queueStates in
204
    queueStates := List.tl !queueStates;
205
    QState res
206
  else if !queueCores1 <> [] then
207
    let res = List.hd !queueCores1 in
208
    queueCores1 := List.tl !queueCores1;
209
    QCore res
210
  else if !queueCores2 = [] then QEmpty
211
  else
212
    let res = List.hd !queueCores2 in
213
    doPropagation := true;
214
    queueCores1 := List.tl !queueCores2;
215
    queueCores2 := [];
216
    QCore res
217
218
let doNominalPropagation () = !doPropagation
219
220
let doSatPropagation () =
221
  let res = !doPropagation in
222
  doPropagation := false;
223
  res
224
225
226
(*****************************************************************************)
227
(*        "Module type" and a specific implementation of the graph           *)
228
(*****************************************************************************)
229
230
let graphStates = ref (Array.make 0 (GHt.create 0 : state GHt.t))
231
let graphCores = ref (Array.make 0 (GHt.create 0 : core GHt.t))
232
let graphCnstrs = ref (GHt.create 0 : constrnt GHt.t)
233
let graphRoot = ref (None : core option)
234
235
let graphInit () =
236
  let size = Array.length !sortTable in
237
  graphStates := Array.init size (fun _ -> GHt.create 128);
238
  graphCores := Array.init size (fun _ -> GHt.create 128);
239
  graphCnstrs := GHt.create 128;
240
  graphRoot := None
241
242
let graphIterStates fkt =
243
  Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphStates
244
245
let graphIterCores fkt =
246
  Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphCores
247
248
let graphIterCnstrs fkt = GHt.iter fkt !graphCnstrs
249
250
let graphClearCnstr () =
251
  let newGraph = GHt.create (GHt.length !graphCnstrs) in
252
  let copyCnstr cset cnstr =
253
    match cnstr with
254
    | UnsatC
255
    | SatC -> GHt.add newGraph cset cnstr
256
    | OpenC _ -> GHt.add newGraph cset (OpenC [])
257
    | UnexpandedC _ -> GHt.add newGraph cset (UnexpandedC [])
258
  in
259
  GHt.iter copyCnstr !graphCnstrs;
260
  graphCnstrs := newGraph
261
262
let graphFindState sort bs =
263
  try
264
    Some (GHt.find !graphStates.(sort) bs)
265
  with Not_found -> None
266
267
let graphFindCore sort bs =
268
  try
269
    Some (GHt.find !graphCores.(sort) bs)
270
  with Not_found -> None
271
272
let graphFindCnstr cset =
273
  try
274
    Some (GHt.find !graphCnstrs cset)
275
  with Not_found -> None
276
277
let graphInsertState sort bs state =
278
  assert (not (GHt.mem !graphStates.(sort) bs));
279
  GHt.add !graphStates.(sort) bs state
280
281
let graphInsertCore sort bs core =
282
  assert (not (GHt.mem !graphCores.(sort) bs));
283
  GHt.add !graphCores.(sort) bs core
284
285
let graphInsertCnstr cset cnstr =
286
  assert (not (GHt.mem !graphCnstrs cset));
287
  GHt.add !graphCnstrs cset cnstr
288
289
let graphReplaceCnstr cset cnstr =
290
  GHt.replace !graphCnstrs cset cnstr
291
292
let graphSizeState () =
293
  Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphStates
294
let graphSizeCore () =
295
  Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphCores
296
let graphSizeCnstr () = GHt.length !graphCnstrs
297
298
let graphAddRoot core =
299
  if !graphRoot = None then graphRoot := Some core
300
  else raise (C.CoAlgException "Root of graph is already set.")
301
302
let graphGetRoot () =
303
  match !graphRoot with
304
  | None -> raise (C.CoAlgException "Root of graph is not set.")
305
  | Some core -> core
306
307
308
(*****************************************************************************)
309
(*     "Module type" and a specific implementation of sets of constraints    *)
310
(*****************************************************************************)
311
312
let cssEmpty = BsSet.empty
313
let cssExists fkt css = BsSet.exists fkt css
314
let cssForall fkt css = BsSet.for_all fkt css
315
let cssUnion css1 css2 = BsSet.union css1 css2
316
let cssAdd cset css = BsSet.add cset css
317
let cssFold fkt css init = BsSet.fold fkt css init
318
let cssSingleton cset = BsSet.singleton cset
319
let cssEqual css1 css2 = BsSet.equal css1 css2
320
321
322
(*****************************************************************************)
323
(*      "Module type" and a specific implementation of state nodes           *)
324
(*****************************************************************************)
325
326
let stateMake sort bs exp =
327
  { sortS = sort; bsS = bs; statusS = Expandable; parentsS = []; childrenS = [];
328
    constraintsS = cssEmpty; expandFkt = exp }
329
let stateGetSort state = state.sortS
330
let stateGetBs state = state.bsS
331
let stateSetBs state bs = state.bsS <- bs
332
let stateGetStatus state = state.statusS
333
let stateSetStatus state status = state.statusS <- status
334
let stateGetParents state = state.parentsS
335
let stateAddParent state parent = state.parentsS <- parent::state.parentsS
336
let stateGetRule state idx = List.nth state.childrenS (List.length state.childrenS - idx)
337
let stateGetRules state = state.childrenS
338
let stateAddRule state dep children =
339
  state.childrenS <- (dep, children)::state.childrenS;
340
  List.length state.childrenS
341
let stateGetConstraints state = state.constraintsS
342
let stateSetConstraints state csets = state.constraintsS <- csets
343
let stateNextRule state = state.expandFkt ()
344
345
346
(*****************************************************************************)
347
(*      "Module type" and a specific implementation of core nodes            *)
348
(*****************************************************************************)
349
350
let coreMake sort bs solver fht =
351
  { sortC = sort; bsC = bs; statusC = Expandable; parentsC = []; childrenC = [];
352
    constraintsC = cssEmpty; solver = solver; fht = fht; constraintParents = [] }
353
let coreGetSort core = core.sortC
354
let coreGetBs core = core.bsC
355
let coreSetBs core bs = core.bsC <- bs
356
let coreGetStatus core = core.statusC
357
let coreSetStatus core status = core.statusC <- status
358
let coreGetParents core = core.parentsC
359
let coreAddParent core parent idx = core.parentsC <- (parent, idx)::core.parentsC
360
let coreGetChildren core = core.childrenC
361
let coreAddChild core child = core.childrenC <- child::core.childrenC
362
let coreGetConstraints core = core.constraintsC
363
let coreSetConstraints core csets = core.constraintsC <- csets
364
let coreGetSolver core = core.solver
365
let coreGetFht core = core.fht
366
let coreGetConstraintParents core = core.constraintParents
367
let coreAddConstraintParent core cset =
368
  core.constraintParents <- cset::core.constraintParents
369
370
371
(*****************************************************************************)
372
(*      "Module type" and a specific implementation of sets of               *)
373
(*      states, cores, and constraints for the sat propagation               *)
374
(*****************************************************************************)
375
376
let setEmptyState () = GHt.create 16
377
let setEmptyCore () = GHt.create 16
378
let setEmptyCnstr () = GHt.create 16
379
let setAddState set state = GHt.add set (stateGetBs state) state
380
let setAddCore set core = GHt.add set (coreGetBs core) core
381
let setAddCnstr set cset = GHt.add set cset ()
382
let setMemState set state = GHt.mem set (stateGetBs state)
383
let setMemCore set core = GHt.mem set (coreGetBs core)
384
let setMemCnstr set cset = GHt.mem set cset
385
let setRemoveState set state = GHt.remove set (stateGetBs state)
386
let setRemoveCore set core = GHt.remove set (coreGetBs core)
387
let setRemoveCnstr set cset = GHt.remove set cset
388
let setIterState fkt set = GHt.iter (fun _ state -> fkt state) set
389
let setIterCore fkt set = GHt.iter (fun _ core -> fkt core) set
390
let setIterCnstr fkt set = GHt.iter (fun cset () -> fkt cset) set
391
392
393
(*****************************************************************************)
394
(*        "Module type" and a specific implementation of the mapping         *)
395
(*        between (local) formulae and literals of the sat solver,           *)
396
(*        and of a mapping of nominals to sets of formulae                   *)
397
(*****************************************************************************)
398
399
let lhtInit () = LHt.create 16
400
let lhtAdd lht lit f = LHt.add lht lit f
401
let lhtFind lht lit =
402
  try
403
    Some (LHt.find lht lit)
404
  with Not_found -> None
405
406
let fhtInit () = FHt.create 16
407
let fhtAdd fht f lit = FHt.add fht f lit
408
let fhtFind fht f =
409
  try
410
    Some (FHt.find fht f)
411
  with Not_found -> None
412
413
let nhtInit () = NHt.create 8
414
let nhtAdd nht nom bs = NHt.add nht nom bs
415
let nhtFind nht nom =
416
  try
417
    Some (NHt.find nht nom)
418
  with Not_found -> None
419
let nhtFold fkt nht init = NHt.fold fkt nht init
420
421
(*****************************************************************************)
422
(*         "Module type" and a specific implementation of sets of            *)
423
(*         local formulae and @-formulae                                     *)
424
(*****************************************************************************)
425
426
let tboxTable = ref (Array.make 0 S.dummyBS)
427
428
let bsetMake () = S.makeBS ()
429
let bsetAdd bs lf = S.addBSNoChk bs lf
430
let bsetMem bs lf = S.memBS bs lf
431 b7445f7e Thorsten Wißmann
let bsetRem bs lf = S.remBS bs lf
432 45d554b0 Thorsten Wißmann
let bsetMakeRealEmpty () =
433
    let res = bsetMake () in
434
    bsetRem res !S.bstrue; (* remove bstrue which is initially in an empty bset *)
435
    res
436 b7c3a47e Thorsten Wißmann
let bsetCopy bs = S.copyBS bs
437 4fd28192 Thorsten Wißmann
let bsetFold fkt bs init = S.foldBS fkt bs init
438
let bsetIter fkt bset = S.iterBS fkt bset
439 e4cd869a Thorsten Wißmann
let bsetFilter (a: bset) (f: localFormula -> bool) : bset =
440 45d554b0 Thorsten Wißmann
    let res = bsetMakeRealEmpty () in
441 e4cd869a Thorsten Wißmann
    bsetIter (fun form -> if (f form) then bsetAdd res form else ()) a;
442
    res
443
444 4fd28192 Thorsten Wißmann
let bsetAddTBox sort bs = S.unionBSNoChk bs !tboxTable.(sort)
445
446
let csetCompare cs1 cs2 = S.compareBS cs1 cs2
447
let csetMake () = S.makeBS ()
448
let csetAdd cs lf = S.addBSNoChk cs lf
449
let csetCopy cs = S.copyBS cs
450
let csetUnion cs1 cs2 = S.unionBSNoChk cs1 cs2
451
let csetHasDot cs = S.memBS cs !S.bsfalse
452
let csetAddDot cs = S.addBSNoChk cs !S.bsfalse
453
let csetRemDot cs = S.remBS cs !S.bsfalse
454
let csetAddTBox sort cs = S.unionBSNoChk cs !tboxTable.(sort)
455
let csetIter cs fkt =
456
  let fkt2 f = if not (f = !S.bstrue || f = !S.bsfalse) then fkt f else () in
457
  S.iterBS fkt2 cs
458
459
460
(*****************************************************************************)
461
(*            "Module type" and a specific implementation of                 *)
462
(*            local formulae and @-formulae                                  *)
463
(*****************************************************************************)
464
465
(** This table maps integers (representing formulae) to their corresponding formulae.
466
 *)
467
let arrayFormula = ref (Array.make 0 (Array.make 0 C.TRUE))
468
469
(** This table maps integers (representing formulae) to their corresponding type.
470
 *)
471
let arrayType = ref (Array.make 0 (Array.make 0 Other))
472
473
(** This lookup table maps formulae (represented as integers)
474
    to their negation (in negation normal form).
475
 *)
476
let arrayNeg = ref (Array.make 0 (Array.make 0 (-1)))
477
478
(** These lookup tables map formulae (represented as integers)
479
    to their decompositions (represented as integers).
480
    This is done according to the rules of the tableau procedure
481
    and depends on the type of the formulae.
482
 *)
483 f1fa9ad5 Thorsten Wißmann
let arrayDest1 = ref (Array.make 0 (Array.make 0 (-1)))  (* first subformula *)
484
let arrayDest2 = ref (Array.make 0 (Array.make 0 (-1)))  (* second subformula *)
485
let arrayDest3 = ref (Array.make 0 (Array.make 0 (-1)))  (* a role *)
486 29b2e3f3 Thorsten Wißmann
let arrayDestNum = ref (Array.make 0 (Array.make 0 (-1)))  (* an integer *)
487 f1fa9ad5 Thorsten Wißmann
let arrayDestAg = ref (Array.make 0 (Array.make 0 [|0|])) (* arrays of agents *)
488 4fd28192 Thorsten Wißmann
489
(** This lookup table maps formulae (represented as integers)
490
    to their @-wrapper.
491
 *)
492
let arrayAt = ref (Array.make 0 (Array.make 0 (FHt.create 64)))
493
494
let lfGetType sort f = !arrayType.(sort).(f)
495
let lfGetDest1 sort f = !arrayDest1.(sort).(f)
496
let lfGetDest2 sort f = !arrayDest2.(sort).(f)
497
let lfGetDest3 sort f = !arrayDest3.(sort).(f)
498 29b2e3f3 Thorsten Wißmann
let lfGetDestNum sort f = !arrayDestNum.(sort).(f)
499 f1fa9ad5 Thorsten Wißmann
let lfGetDestAg sort f = !arrayDestAg.(sort).(f)
500 4fd28192 Thorsten Wißmann
let lfGetNeg sort f =
501
  let nf = !arrayNeg.(sort).(f) in
502
  if nf >= 0 then Some nf else None
503
let lfGetAt (sort, nom) f =
504
  FHt.find !arrayAt.(sort).(f) nom
505 a0cffef0 Thorsten Wißmann
let lfToInt lf = lf
506
let lfFromInt num = num
507 4fd28192 Thorsten Wißmann
508
let atFormulaGetSubformula f = !arrayDest1.(0).(f)
509
let atFormulaGetNominal f =
510
  let s = !arrayDest3.(0).(f) in
511
  let n = !arrayDest2.(0).(f) in
512
  (s, n)
513
514
let lfToAt _ lf = lf
515
516
517
let rec detClosure nomTbl hcF fset atset nomset s f =
518
  if s < 0 || s >= Array.length fset then
519
    let sstr = string_of_int s in
520
    raise (C.CoAlgException ("Invalid sort (i.e. sort out of range): " ^ sstr))
521
  else ();
522
  if C.HcFHt.mem fset.(s) f then ()
523
  else
524
    let () = C.HcFHt.add fset.(s) f () in
525
    let (func, sortlst) = !sortTable.(s) in
526
    match f.HC.node with
527
    | C.HCTRUE
528
    | C.HCFALSE -> ()
529
    | C.HCAP name ->
530
        if C.isNominal name then begin
531
          Hashtbl.replace nomset name s;
532
          match nomTbl name with
533
          | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name))
534
          | Some sort ->
535
              if sort <> s then
536
                let str1 = "Nominal: " ^ name ^ " of sort " ^ (string_of_int sort) in
537
                let str2 = " is used in sort " ^ (string_of_int s) ^ "." in
538
                raise (C.CoAlgException (str1 ^ str2))
539
              else ()
540
        end else ()
541
    | C.HCNOT _ -> ()
542
    | C.HCAT (name, f1) ->
543
        C.HcFHt.replace atset f ();
544
        let s1 =
545
          match nomTbl name with
546
          | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name))
547
          | Some sort -> sort
548
        in
549
        let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
550
        detClosure nomTbl hcF fset atset nomset s1 hcnom;
551
        detClosure nomTbl hcF fset atset nomset s1 f1
552
    | C.HCOR (f1, f2)
553
    | C.HCAND (f1, f2) ->
554
        detClosure nomTbl hcF fset atset nomset s f1;
555
        detClosure nomTbl hcF fset atset nomset s f2
556
    | C.HCEX (_, f1)
557
    | C.HCAX (_, f1) ->
558 2a84977e Thorsten Wißmann
        if (func <> MultiModalK && func <> MultiModalKD)
559
            || List.length sortlst <> 1
560
        then raise (C.CoAlgException "Ex/Ax-formula is used in wrong sort.")
561 4fd28192 Thorsten Wißmann
        else ();
562
        detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1
563 f1fa9ad5 Thorsten Wißmann
    | C.HCENFORCES (_, f1)
564
    | C.HCALLOWS (_, f1) ->
565
        if func <> CoalitionLogic || List.length sortlst <> 1
566
        then raise (C.CoAlgException "[{Agents}]-formula is used in wrong sort.")
567
        else ();
568
        detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1
569 af276a36 Thorsten Wißmann
    | C.HCMORETHAN (_,_,f1)
570
    | C.HCMAXEXCEPT (_,_,f1) ->
571 29b2e3f3 Thorsten Wißmann
        if func <> GML || List.length sortlst <> 1
572
        then raise (C.CoAlgException "[{>=,<=}]-formula is used in wrong sort.")
573
        else ();
574
        detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1
575 4fd28192 Thorsten Wißmann
    | C.HCCHC (f1, f2)
576
    | C.HCCHCN (f1, f2) ->
577
        if func <> Choice || List.length sortlst <> 2 then
578
          raise (C.CoAlgException "Choice formula is used in wrong sort.")
579
        else ();
580
        detClosure nomTbl hcF fset atset nomset (List.nth sortlst 0) f1;
581
        detClosure nomTbl hcF fset atset nomset (List.nth sortlst 1) f2
582
    | C.HCFUS (first, f1) ->
583
        if func <> Fusion || List.length sortlst <> 2 then
584
          raise (C.CoAlgException "Fusion formula is used in wrong sort.")
585
        else ();
586
        let s1 = List.nth sortlst (if first then 0 else 1) in
587
        detClosure nomTbl hcF fset atset nomset s1 f1
588
589
let detClosureAt hcF atset name f () =
590
  match f.HC.node with
591
  | C.HCTRUE
592
  | C.HCFALSE
593
  | C.HCOR _
594
  | C.HCAND _
595
  | C.HCAT _ -> ()
596
  | _ ->
597
      let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in 
598
      C.HcFHt.replace atset at ()
599
600
(** Initialises the arrays for a formula and its integer representation.
601
 *)
602
let initTables nomTbl hcF htF htR s f n =
603
  !arrayFormula.(s).(n) <- f.HC.fml;
604
  let fneg = f.HC.neg in
605
  if C.HcFHt.mem htF.(s) fneg then !arrayNeg.(s).(n) <- C.HcFHt.find htF.(s) fneg;
606
  let (_, sortlst) = !sortTable.(s) in
607
  match f.HC.node with
608
  | C.HCTRUE
609
  | C.HCFALSE -> !arrayType.(s).(n) <- ConstF
610
  | C.HCAP name ->
611
      if C.isNominal name then !arrayType.(s).(n) <- NomF
612
      else !arrayType.(s).(n) <- Other
613
  | C.HCNOT _ -> !arrayType.(s).(n) <- Other
614
  | C.HCAT (name, f1) ->
615
      !arrayType.(s).(n) <- AtF;
616
      let s1 =
617
        match nomTbl name with
618
        | None -> assert false
619
        | Some sort -> sort
620
      in
621
      let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
622
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s1) f1;
623
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s1) hcnom;
624
      !arrayDest3.(s).(n) <- s1
625
  | C.HCOR (f1, f2) ->
626
      !arrayType.(s).(n) <- OrF;
627
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) f1;
628
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s) f2
629
  | C.HCAND (f1, f2) ->
630
      !arrayType.(s).(n) <- AndF;
631
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) f1;
632
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s) f2
633
  | C.HCEX (role, f1) -> 
634
      !arrayType.(s).(n) <- ExF;
635
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
636
      !arrayDest3.(s).(n) <- 
637
        if Hashtbl.mem htR role then Hashtbl.find htR role
638
        else
639
          let size = Hashtbl.length htR in
640
          Hashtbl.add htR role size;
641
          size
642
  | C.HCAX (role, f1) ->
643
      !arrayType.(s).(n) <- AxF;
644
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
645
      !arrayDest3.(s).(n) <-
646
        if Hashtbl.mem htR role then Hashtbl.find htR role
647
        else
648
          let size = Hashtbl.length htR in
649
          Hashtbl.add htR role size;
650
          size
651 f1fa9ad5 Thorsten Wißmann
  | C.HCENFORCES (aglist, f1) ->  (* aglist = list of agents *)
652
      !arrayType.(s).(n) <- EnforcesF;
653
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
654
      !arrayDestAg.(s).(n) <- Array.of_list aglist
655
  | C.HCALLOWS (aglist, f1) ->  (* aglist = list of agents *)
656
      !arrayType.(s).(n) <- AllowsF;
657
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
658
      !arrayDestAg.(s).(n) <- Array.of_list aglist
659 af276a36 Thorsten Wißmann
  | C.HCMORETHAN (cnt,role,f1) ->
660
      !arrayType.(s).(n) <- MoreThanF;
661 29b2e3f3 Thorsten Wißmann
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
662
      !arrayDestNum.(s).(n) <- cnt;
663
      !arrayDest3.(s).(n) <-
664
        if Hashtbl.mem htR role then Hashtbl.find htR role
665
        else
666
          let size = Hashtbl.length htR in
667
          Hashtbl.add htR role size;
668
          size
669 af276a36 Thorsten Wißmann
  | C.HCMAXEXCEPT (cnt,role,f1) ->
670
      !arrayType.(s).(n) <- MaxExceptF;
671 29b2e3f3 Thorsten Wißmann
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
672
      !arrayDestNum.(s).(n) <- cnt;
673
      !arrayDest3.(s).(n) <-
674
        if Hashtbl.mem htR role then Hashtbl.find htR role
675
        else
676
          let size = Hashtbl.length htR in
677
          Hashtbl.add htR role size;
678
          size
679 4fd28192 Thorsten Wißmann
  | C.HCCHC (f1, f2)
680
  | C.HCCHCN (f1, f2) ->
681
      !arrayType.(s).(n) <- ChcF;
682
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
683
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2
684
  | C.HCFUS (first, f1) ->
685
      !arrayType.(s).(n) <- FusF;
686
      let s1 = List.nth sortlst (if first then 0 else 1) in
687
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s1) f1;
688
      !arrayDest3.(s).(n) <- if first then 0 else 1
689
690
let initTablesAt hcF htF name sort =
691
  let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
692
  let nom = C.HcFHt.find htF.(sort) hcnom in
693
  let addAt f n =
694
    match f.HC.node with
695
    | C.HCTRUE
696
    | C.HCFALSE
697
    | C.HCOR _
698
    | C.HCAND _
699
    | C.HCAT _ -> ()
700
    | _ ->
701
        let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in 
702
        let atn = C.HcFHt.find htF.(0) at in
703
        FHt.add !arrayAt.(sort).(n) nom atn
704
  in
705
  C.HcFHt.iter addAt htF.(sort)
706
707
let ppFormulae nomTbl tbox (s, f) =
708
  let card = Array.length !sortTable in
709
  if card <= 0 then
710
    raise (C.CoAlgException "Number of sorts must be positive.")
711
  else ();
712
  let nnfAndSimplify f = C.simplify (C.nnf f) in
713 f828ad2f Thorsten Wißmann
  let  f1    = nnfAndSimplify f in
714
  let nf1    = nnfAndSimplify (C.NOT f) in
715
  let  tbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify f)) tbox in
716
  let ntbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify (C.NOT f))) tbox in
717
718
  let hcF     =  C.HcFormula.create true in
719
  let  hcf    = C.hc_formula hcF  f1 in
720
  let nhcf    = C.hc_formula hcF nf1 in
721
  let  hctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f))  tbox1 in
722
  let nhctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f)) ntbox1 in
723 4fd28192 Thorsten Wißmann
  let hcfalse = C.hc_formula hcF C.FALSE in
724 f828ad2f Thorsten Wißmann
  let hctrue  = C.hc_formula hcF C.TRUE in
725 4fd28192 Thorsten Wißmann
726
  let fset = Array.init card (fun _ -> C.HcFHt.create 128) in
727
  let atset = C.HcFHt.create 64 in
728
  let nomset = Hashtbl.create 16 in
729
  for i = 0 to card-1 do
730
    detClosure nomTbl hcF fset atset nomset i hcfalse;
731
    detClosure nomTbl hcF fset atset nomset i hctrue;
732
  done;
733 f828ad2f Thorsten Wißmann
  detClosure nomTbl hcF fset atset nomset s  hcf;
734
  detClosure nomTbl hcF fset atset nomset s nhcf;
735
  List.iter (fun (s, f) -> detClosure nomTbl hcF fset atset nomset s f)  hctbox;
736
  List.iter (fun (s, f) -> detClosure nomTbl hcF fset atset nomset s f) nhctbox;
737 4fd28192 Thorsten Wißmann
  Hashtbl.iter (fun n s -> C.HcFHt.iter (detClosureAt hcF atset n) fset.(s)) nomset;
738
739
  let htF = Array.init card (fun _ -> C.HcFHt.create 128) in
740
  for i = 0 to card-1 do
741
    C.HcFHt.add htF.(i) hcfalse 0;
742
    C.HcFHt.add htF.(i) hctrue 1
743
  done;
744
  let addAts f () idx =
745
    for i = 0 to card-1 do
746
      C.HcFHt.add htF.(i) f idx
747
    done;
748
    idx + 1
749
  in
750
  let sizeAt = C.HcFHt.fold addAts atset 2 in
751
  let addFml i f () idx =
752
    if C.HcFHt.mem htF.(i) f then idx
753
    else begin
754
      C.HcFHt.add htF.(i) f idx;
755
      idx+1
756
    end
757
  in
758
  let size = ref 0 in
759
  for i = 0 to card-1 do
760
    let size2 = C.HcFHt.fold (addFml i) fset.(i) sizeAt in
761
    if size2 > !size then size := size2 else ()
762
  done;
763
764
  arrayFormula := Array.init card (fun _ -> Array.make !size C.TRUE);
765
  arrayType := Array.init card (fun _ -> Array.make !size Other);
766
  arrayDest1 := Array.init card (fun _ -> Array.make !size (-1));
767
  arrayDest2 := Array.init card (fun _ -> Array.make !size (-1));
768
  arrayDest3 := Array.init card (fun _ -> Array.make !size (-1));
769
  arrayNeg := Array.init card (fun _ -> Array.make !size (-1));
770 29b2e3f3 Thorsten Wißmann
  arrayDestNum := Array.init card (fun _ -> Array.make !size (-1));
771 98af95fb Thorsten Wißmann
  arrayDestAg := Array.init card (fun _ -> Array.make !size (Array.make 0 (-1)));
772 4fd28192 Thorsten Wißmann
  let htR = Hashtbl.create 128 in
773
  Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR s) ht) htF;
774
  arrayAt := Array.init card (fun _ -> Array.init !size (fun _ -> FHt.create 8));
775
  Hashtbl.iter (initTablesAt hcF htF) nomset;
776
777
  S.initMisc !size (C.HcFHt.find htF.(0) hcfalse) (C.HcFHt.find htF.(0) hctrue) (-1) (-1) (-1);
778
  let initbs = bsetMake () in
779
  bsetAdd initbs (C.HcFHt.find htF.(s) hcf);
780
  let tboxTbl = Array.init card (fun _ -> bsetMake ()) in
781
  List.iter (fun (s, f) -> bsetAdd tboxTbl.(s) (C.HcFHt.find htF.(s) f)) hctbox;
782
  tboxTable := tboxTbl;
783
  (tbox1, (s, f1), initbs)