Project

General

Profile

Statistics
| Branch: | Revision:

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

History | View | Annotate | Download (26.8 KB)

1
(** Common types, functions, and data structures for the CoAlgebraic reasoner.
2
    @author Florian Widmann
3
 *)
4

    
5

    
6
module S = MiscSolver
7
module L = List
8
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
  | MultiModalKD
71
  | CoalitionLogic
72
  | GML
73
  | 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
  | ExF  (* Existential / diamond *)
85
  | AxF  (* Universal / box *)
86
  | EnforcesF (* diamond of CL *)
87
  | AllowsF   (* box of CL *)
88
  | MoreThanF (* more than n successors = diamond in gml *)
89
  | MaxExceptF(* at most n exceptions = box in gml *)
90
  | ChcF (* Choice *)
91
  | FusF (* Fusion *)
92

    
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
let bsetRem bs lf = S.remBS bs lf
432
let bsetMakeRealEmpty () =
433
    let res = bsetMake () in
434
    bsetRem res !S.bstrue; (* remove bstrue which is initially in an empty bset *)
435
    res
436
let bsetCopy bs = S.copyBS bs
437
let bsetFold fkt bs init = S.foldBS fkt bs init
438
let bsetIter fkt bset = S.iterBS fkt bset
439
let bsetFilter (a: bset) (f: localFormula -> bool) : bset =
440
    let res = bsetMakeRealEmpty () in
441
    bsetIter (fun form -> if (f form) then bsetAdd res form else ()) a;
442
    res
443

    
444
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
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
let arrayDestNum = ref (Array.make 0 (Array.make 0 (-1)))  (* an integer *)
487
let arrayDestAg = ref (Array.make 0 (Array.make 0 [|0|])) (* arrays of agents *)
488

    
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
let lfGetDestNum sort f = !arrayDestNum.(sort).(f)
499
let lfGetDestAg sort f = !arrayDestAg.(sort).(f)
500
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
let lfToInt lf = lf
506
let lfFromInt num = num
507

    
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
        if (func <> MultiModalK && func <> MultiModalKD)
559
            || List.length sortlst <> 1
560
        then raise (C.CoAlgException "Ex/Ax-formula is used in wrong sort.")
561
        else ();
562
        detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1
563
    | 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
    | C.HCMORETHAN (_,_,f1)
570
    | C.HCMAXEXCEPT (_,_,f1) ->
571
        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
    | 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
  | 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
  | C.HCMORETHAN (cnt,role,f1) ->
660
      !arrayType.(s).(n) <- MoreThanF;
661
      !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
  | C.HCMAXEXCEPT (cnt,role,f1) ->
670
      !arrayType.(s).(n) <- MaxExceptF;
671
      !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
  | 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
  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
  let hcfalse = C.hc_formula hcF C.FALSE in
724
  let hctrue  = C.hc_formula hcF C.TRUE in
725

    
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
  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
  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
  arrayDestNum := Array.init card (fun _ -> Array.make !size (-1));
771
  arrayDestAg := Array.init card (fun _ -> Array.make !size (Array.make 0 (-1)));
772
  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)