Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgMisc.ml @ def3763d

History | View | Annotate | Download (48.1 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 16af388e Christoph Egger
    type t = S.bitset * S.bitset
26
    let equal ((bs1l, bs1r) : t) (bs2l, bs2r) =
27
      (S.compareBS bs1l bs2l = 0) && (S.compareBS bs1r bs2r = 0)
28
    let hash ((bsl, bsr) : t) = (S.hashBS bsl) lxor (S.hashBS bsr)
29
  end
30
 )
31
32
(** An instantiation of a hash table (of the standard library) for bitsets.
33
 *)
34
module GHtS = Hashtbl.Make(
35
  struct
36 4fd28192 Thorsten Wißmann
    type t = S.bitset
37
    let equal (bs1 : t) bs2 = S.compareBS bs1 bs2 = 0
38
    let hash (bs : t) = S.hashBS bs
39
  end
40
 )
41
42
(** An instantiation of a hash table (of the standard library) for literals.
43
 *)
44
module LHt = Hashtbl.Make(
45
  struct
46
    type t = Minisat.lit
47
    let equal (l1 : t) l2 = l1 = l2
48
    let hash (l : t) = (l :> int)
49
  end
50
 )
51
52
(** An instantiation of a hash table (of the standard library) for formulae.
53
 *)
54
module FHt = Hashtbl.Make(
55
  struct
56
    type t = int
57
    let equal (f1 : t) f2 = f1 = f2
58
    let hash (f : t) = f
59
  end
60
 )
61
62
(** An instantiation of a hash table (of the standard library) for nominals.
63
 *)
64
module NHt = Hashtbl.Make(
65
  struct
66
    type t = int * int
67
    let equal ((s1, f1) : t) (s2, f2) = (s1 = s2) && (f1 = f2)
68
    let hash ((s, f) : t) = (((s+f)*(s+f+1)) / 2) + f
69
  end
70
)
71
72
73
(*****************************************************************************)
74
(*     Types that can be modified rather easily                              *)
75
(*     (of course you then have to modify the implementations below too)     *)
76
(*****************************************************************************)
77
78
(* This type must be extended for additional logics. *)
79
type functors =
80
  | MultiModalK
81 a87192e8 Thorsten Wißmann
  | MultiModalKD
82 f4e43751 Christoph Egger
  | Monotone
83 f1fa9ad5 Thorsten Wißmann
  | CoalitionLogic
84 29b2e3f3 Thorsten Wißmann
  | GML
85 86b07be8 Thorsten Wißmann
  | PML
86 5e0983fe Thorsten Wißmann
  | Constant of string list
87 19f5dad0 Dirk Pattinson
  | Identity
88
  | DefaultImplication
89 4fd28192 Thorsten Wißmann
  | Choice
90
  | Fusion
91
92 5e0983fe Thorsten Wißmann
(* functors whose constructor takes additional parameters *)
93
type parametricFunctorName =
94
  | NameConstant
95
96
(* this type should only be used in the following few helper functions *)
97
type functorName =
98
  | NPa of functors (* No Parameters = functor without parameters *)
99
  | Pa  of parametricFunctorName (* Parameters = functor with parameters *)
100
101
let unaryfunctor2name : (functorName*string) list =
102
  [ (NPa MultiModalK , "MultiModalK")
103
  ; (NPa MultiModalKD , "MultiModalKD")
104 f4e43751 Christoph Egger
  ; (NPa Monotone , "Monotone")
105 5e0983fe Thorsten Wißmann
  ; (NPa GML ,           "GML")
106
  ; (NPa PML ,           "PML")
107
  ; (NPa CoalitionLogic , "CoalitionLogic")
108
  ; (NPa MultiModalK , "K")
109
  ; (NPa MultiModalKD , "KD")
110
  ; (NPa CoalitionLogic , "CL")
111
  ; (Pa  NameConstant , "Const")
112
  ; (Pa  NameConstant , "Constant")
113 19f5dad0 Dirk Pattinson
  ; (NPa Identity, "Id")
114
  ; (NPa Identity, "Identity")
115 db23edf7 Thorsten Wißmann
  ]
116
117 5e0983fe Thorsten Wißmann
let functor2name : (functorName*string) list =
118 db23edf7 Thorsten Wißmann
  L.append unaryfunctor2name
119 5e0983fe Thorsten Wißmann
  [ (NPa Choice , "Choice")
120
  ; (NPa Fusion , "Fusion")
121 db23edf7 Thorsten Wißmann
  ]
122
123 5e0983fe Thorsten Wißmann
let functor_apply_parameters (func : parametricFunctorName) (params: string list) : functors option =
124
    (* apply parameter list to the constructor, denoted by the functor name func *)
125
    (* return None, if the parameters somehow don't match the required parameters *)
126
    match func with
127
    | NameConstant -> Some (Constant params)
128
129
130
let functor_of_string str params : functors option =
131 db23edf7 Thorsten Wißmann
    let fst (a,b) = a in
132
    try
133 5e0983fe Thorsten Wißmann
        let functorName = fst (List.find (fun (f,name) -> name = str) functor2name) in
134
        match functorName with
135
        | NPa x -> Some x
136
        | Pa f -> functor_apply_parameters f params
137 db23edf7 Thorsten Wißmann
    with Not_found -> None
138
139 5e0983fe Thorsten Wißmann
let unaryfunctor_of_string str params =
140
    match (functor_of_string str params) with
141 db23edf7 Thorsten Wißmann
    | Some Choice -> None
142
    | Some Fusion -> None
143
    | x -> x
144
145
let string_of_functor (f: functors) : string =
146 5e0983fe Thorsten Wißmann
    (* replace f orrectly with possibly some Pa wrapper *)
147
    (* also put the parameters into some suffix which will be appended later *)
148
    let f,suffix = match f with
149
            | Constant params -> Pa NameConstant, " "^(String.concat " " params)
150
            | _ -> NPa f, ""
151
    in
152 db23edf7 Thorsten Wißmann
    let snd (a,b) = b in
153
    try
154 5e0983fe Thorsten Wißmann
        let name = snd (List.find (fun (f2,name) -> f = f2) functor2name) in
155
        name ^ suffix
156 db23edf7 Thorsten Wißmann
    with Not_found -> assert false
157
158 4fd28192 Thorsten Wißmann
(* This type may be extended for additional logics. *)
159
type formulaType =
160
  | Other
161 3b055ae8 dirk
  | TrueFalseF (* constant true or false *)
162 4fd28192 Thorsten Wißmann
  | AndF
163
  | OrF
164
  | AtF
165
  | NomF
166 559819d7 Thorsten Wißmann
  | ExF  (* Existential / diamond *)
167
  | AxF  (* Universal / box *)
168 29b2e3f3 Thorsten Wißmann
  | EnforcesF (* diamond of CL *)
169
  | AllowsF   (* box of CL *)
170 af276a36 Thorsten Wißmann
  | MoreThanF (* more than n successors = diamond in gml *)
171
  | MaxExceptF(* at most n exceptions = box in gml *)
172 86b07be8 Thorsten Wißmann
  | AtLeastProbF (* for PML *)
173 9bae2c4f Thorsten Wißmann
  | LessProbFailF (* box for PML *)
174 c49eea11 Thorsten Wißmann
  | ConstF (* constant functor *)
175
  | ConstnF (* constant functor *)
176 19f5dad0 Dirk Pattinson
  | IdF (* Identity functor *)
177
  | NormF (* Default Implication *)
178
  | NormnF (* negation normal form of default implication *)
179 559819d7 Thorsten Wißmann
  | ChcF (* Choice *)
180
  | FusF (* Fusion *)
181 3b407438 Christoph Egger
  | MuF
182
  | NuF
183 4fd28192 Thorsten Wißmann
184
type localFormula = int
185
type bset = S.bitset
186
187
type atFormula = int
188
type cset = S.bitset
189
type csetSet = BsSet.t
190
191
type lht = localFormula LHt.t
192
type fht = Minisat.lit FHt.t
193
type nht = bset NHt.t
194
195 e0f19999 Thorsten Wißmann
type state = { sortS : sort;
196
               mutable bsS : bset; (* a set of formulas who are either literals or
197
                                      modalities (TODO: also @-formulas?).
198
                                      the state is satisfiable if /\bsS is satisfiable.
199
                                    *)
200 3285ac30 Christoph Egger
               mutable deferralS : bset; (* which formulas still have deferrals *)
201 e0f19999 Thorsten Wißmann
               mutable statusS : nodeStatus;
202 4fd28192 Thorsten Wißmann
               mutable parentsS : core list; mutable childrenS : (dependencies * core list) list;
203 73762b19 Thorsten Wißmann
               mutable constraintsS : csetSet; expandFkt : stateExpander;
204 7eb41195 Hans-Peter Deifel
               idxS: int }
205 4fd28192 Thorsten Wißmann
206 e0f19999 Thorsten Wißmann
and core = { (* for details, see documentation of newCore *)
207
             sortC : sort;
208
             mutable bsC : bset; (* a set of arbitrary formulas.
209
                                    the present core is satisfiable if /\ bsC is satisfiable *)
210 3285ac30 Christoph Egger
             mutable deferralC : bset; (* which formulas still have deferrals *)
211 e0f19999 Thorsten Wißmann
             mutable statusC : nodeStatus;
212
             mutable parentsC : (state * int) list;
213
             mutable childrenC : state list;
214
             mutable constraintsC : csetSet;
215 9f1263ec Christoph Egger
             mutable solver : Minisat.solver option; (* a solver to find satisfying assignemnts for bsC.
216 e0f19999 Thorsten Wißmann
                                         the solver returns "satisfiable" iff
217
                                         there is a satisfying assignment of
218
                                         bsC which is not represented by some state from the
219
                                         childrenC yet.
220
                                       *)
221
             fht : fht; (* mapping of boolean subformulas of bsC to their corresponding literals
222
                           of the Minisat solver
223
                         *)
224 73762b19 Thorsten Wißmann
             mutable constraintParents : cset list;
225 7eb41195 Hans-Peter Deifel
             idxC : int }
226 4fd28192 Thorsten Wißmann
227 d283bf7a Thorsten Wißmann
and setState = state GHt.t array
228 4fd28192 Thorsten Wißmann
229 d283bf7a Thorsten Wißmann
and setCore = core GHt.t array
230 4fd28192 Thorsten Wißmann
231 16af388e Christoph Egger
and setCnstr = unit GHtS.t
232 4fd28192 Thorsten Wißmann
233
234
(*****************************************************************************)
235
(*                Types that are hard coded into the algorithm               *)
236
(*****************************************************************************)
237
238 269d93e5 Thorsten Wißmann
and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *)
239
                  | Conjunctive of 'a (*specifies that all of the 'a need  to be satifsfied *)
240
241 a9949a25 Thorsten Wißmann
and stateExpander = rule lazylist
242 4fd28192 Thorsten Wißmann
243
and sort = C.sort
244
245
and nodeStatus =
246
  | Expandable
247
  | Open
248
  | Sat
249
  | Unsat
250
251 f4498ed1 Christoph Egger
(* In K, given the singleton list [bs] returns the list of all Ax'es
252
   responsible for the individual members of bs being part of the core
253
   as well as the Ex.
254
255
   So given the state { <>φ , []ψ , []η } and the core { φ , ψ , η },
256
   dependency would map { η } to { <>φ , []η } and { ψ } to { <>φ , []ψ }
257
*)
258 4fd28192 Thorsten Wißmann
and dependencies = bset list -> bset
259 269d93e5 Thorsten Wißmann
260 f4498ed1 Christoph Egger
(* Note: sort * bset * bset is to be read as sort * formulas_in_core * deferrals_in_core *)
261 16af388e Christoph Egger
and rule = (dependencies * (sort * bset * bset) lazylist)
262 269d93e5 Thorsten Wißmann
263 a9949a25 Thorsten Wißmann
and 'a lazyliststep =
264 69243f7f Thorsten Wißmann
  | MultipleElements of 'a list
265
  | SingleElement    of 'a
266
  | NoMoreElements
267
268 a9949a25 Thorsten Wißmann
and 'a lazylist = unit -> 'a lazyliststep
269
270
and ruleEnumeration = rule lazyliststep
271
272 f335015f Thorsten Wißmann
let nodeStatusToString : nodeStatus -> string = function
273
  | Expandable -> "Expandable"
274
  | Open -> "Open"
275
  | Sat -> "Sat"
276
  | Unsat -> "Unsat"
277
278 a9949a25 Thorsten Wißmann
let lazylistFromList a_list =
279
    let list_state = ref (Some a_list) in
280
    fun () -> begin match !list_state with
281
              | Some (a_list) -> begin
282
                    list_state := None;
283
                    MultipleElements a_list
284
                end
285
              | None -> NoMoreElements
286
              end
287 4fd28192 Thorsten Wißmann
288 672429b4 Thorsten Wißmann
let rec listFromLazylist evalfunc =
289
    let step = evalfunc () in
290
    match step with
291
    | NoMoreElements -> []
292
    | SingleElement x -> x::(listFromLazylist evalfunc)
293
    | MultipleElements xs -> List.append xs (listFromLazylist evalfunc)
294
295 4fd28192 Thorsten Wißmann
type nominal = sort * localFormula
296
297
type node =
298
  | State of state
299
  | Core of core
300
301
type constrnt =
302
  | UnsatC
303
  | SatC
304
  | OpenC of node list
305
  | UnexpandedC of node list
306
307
type propagateElement =
308
  | UState of state * int option
309
  | UCore of core * bool
310
  | UCnstr of cset
311
312
type queueElement =
313
  | QState of state
314
  | QCore of core
315
  | QCnstr of cset
316
  | QEmpty
317
318
type sortTable = (functors * int list) array
319
320
exception CoAlg_finished of bool
321
322
323
let sortTable = ref (Array.make 0 (MultiModalK, [1]))
324
325 269d93e5 Thorsten Wißmann
let junctionEvalBool : (bool list junction) -> bool = function
326
    | Disjunctive l -> List.fold_right (||) l false
327
    | Conjunctive l -> List.fold_right (&&) l true
328
329
let junctionEval (f: 'a -> bool) : 'a list junction -> bool = function
330
    | Disjunctive l -> List.fold_right (fun x y -> (f x) || y) l false
331
    | Conjunctive l -> List.fold_right (fun x y -> (f x) && y) l true
332
333
let optionalizeOperator (f: 'a -> 'b -> 'c) (x: 'a option) (y: 'b option) : 'c option =
334
    match x with
335
    | None -> None
336
    | Some x -> (match y with
337
                 | None -> None
338
                 | Some y -> Some (f x y))
339
340
let junctionEvalBoolOption : bool option list junction -> bool option =
341
    let f extreme op x y = (* ensure that: (Some True) || None = Some True *)
342
        if x = extreme || y = extreme
343
        then extreme
344
        else optionalizeOperator op x y
345
    in function
346
    | Disjunctive l ->
347
        List.fold_right (f (Some true)  (||)) l (Some false)
348
    | Conjunctive l ->
349
        List.fold_right (f (Some false) (&&)) l (Some true)
350
351
let junctionExtract : 'a junction -> ('a * ('b -> 'b junction)) = function
352
    | Disjunctive l -> (l, fun x -> Disjunctive x)
353
    | Conjunctive l -> (l, fun x -> Conjunctive x)
354 4fd28192 Thorsten Wißmann
355
(*****************************************************************************)
356
(*      "Module type" and a specific implementation of the main queue        *)
357
(*****************************************************************************)
358
359
let queueStates = ref ([] : state list)
360
let queueCores1 = ref ([] : core list)
361
let queueCores2 = ref ([] : core list)
362
let queueCnstrs = ref ([] : cset list)
363
let doPropagation = ref false
364 61c5af02 Christoph Egger
let doPropagationCounter = ref 0
365 4fd28192 Thorsten Wißmann
366
let queueInit () =
367
  queueStates := [];
368
  queueCores1 := [];
369
  queueCores2 := [];
370
  queueCnstrs := [];
371
  doPropagation := false
372
373
let queueIsEmpty () =
374
  !queueStates = [] && !queueCores1 = [] && !queueCores2 = [] && !queueCnstrs = []
375
376
let queueInsertState state = queueStates := state::!queueStates
377
378 d58bba0f Dirk Pattinson
(* original version: breadth-first *)
379 4fd28192 Thorsten Wißmann
let queueInsertCore core = queueCores2 := core::!queueCores2
380
381 034a8dea Christoph Egger
(* experiment: depth first
382 d58bba0f Dirk Pattinson
let queueInsertCore core = queueCores1 := core::!queueCores1
383
*)
384
385 4fd28192 Thorsten Wißmann
let queueInsertCnstr cset = queueCnstrs := cset::!queueCnstrs
386
387
let queueGetElement () =
388
  if !queueCnstrs <> [] then
389
    let res = List.hd !queueCnstrs in
390
    queueCnstrs := List.tl !queueCnstrs;
391
    QCnstr res
392
  else if !queueStates <> [] then
393
    let res = List.hd !queueStates in
394
    queueStates := List.tl !queueStates;
395
    QState res
396
  else if !queueCores1 <> [] then
397
    let res = List.hd !queueCores1 in
398
    queueCores1 := List.tl !queueCores1;
399
    QCore res
400
  else if !queueCores2 = [] then QEmpty
401
  else
402
    let res = List.hd !queueCores2 in
403
    doPropagation := true;
404
    queueCores1 := List.tl !queueCores2;
405
    queueCores2 := [];
406
    QCore res
407
408
let doNominalPropagation () = !doPropagation
409
410 55dc0a64 Christoph Egger
let setPropagationCounter count =
411
  doPropagationCounter := count
412
413 4fd28192 Thorsten Wißmann
let doSatPropagation () =
414 61c5af02 Christoph Egger
  if !doPropagationCounter == 0
415 55dc0a64 Christoph Egger
  then true
416 61c5af02 Christoph Egger
  else begin
417
      doPropagationCounter := !doPropagationCounter - 1;
418
      false
419
    end
420
  (* let res = !doPropagation in *)
421
  (* doPropagation := false; *)
422
  (* res *)
423 4fd28192 Thorsten Wißmann
424
(*****************************************************************************)
425
(*        "Module type" and a specific implementation of the graph           *)
426
(*****************************************************************************)
427
428
let graphStates = ref (Array.make 0 (GHt.create 0 : state GHt.t))
429
let graphCores = ref (Array.make 0 (GHt.create 0 : core GHt.t))
430 16af388e Christoph Egger
let graphCnstrs = ref (GHtS.create 0 : constrnt GHtS.t)
431 4fd28192 Thorsten Wißmann
let graphRoot = ref (None : core option)
432
433
let graphInit () =
434
  let size = Array.length !sortTable in
435
  graphStates := Array.init size (fun _ -> GHt.create 128);
436
  graphCores := Array.init size (fun _ -> GHt.create 128);
437 16af388e Christoph Egger
  graphCnstrs := GHtS.create 128;
438 4fd28192 Thorsten Wißmann
  graphRoot := None
439
440
let graphIterStates fkt =
441
  Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphStates
442
443
let graphIterCores fkt =
444
  Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphCores
445
446 16af388e Christoph Egger
let graphIterCnstrs fkt = GHtS.iter fkt !graphCnstrs
447 4fd28192 Thorsten Wißmann
448
let graphClearCnstr () =
449 16af388e Christoph Egger
  let newGraph = GHtS.create (GHtS.length !graphCnstrs) in
450 4fd28192 Thorsten Wißmann
  let copyCnstr cset cnstr =
451
    match cnstr with
452
    | UnsatC
453 16af388e Christoph Egger
    | SatC -> GHtS.add newGraph cset cnstr
454
    | OpenC _ -> GHtS.add newGraph cset (OpenC [])
455
    | UnexpandedC _ -> GHtS.add newGraph cset (UnexpandedC [])
456 4fd28192 Thorsten Wißmann
  in
457 16af388e Christoph Egger
  GHtS.iter copyCnstr !graphCnstrs;
458 4fd28192 Thorsten Wißmann
  graphCnstrs := newGraph
459
460
let graphFindState sort bs =
461
  try
462
    Some (GHt.find !graphStates.(sort) bs)
463
  with Not_found -> None
464
465
let graphFindCore sort bs =
466
  try
467
    Some (GHt.find !graphCores.(sort) bs)
468
  with Not_found -> None
469
470
let graphFindCnstr cset =
471
  try
472 16af388e Christoph Egger
    Some (GHtS.find !graphCnstrs cset)
473 4fd28192 Thorsten Wißmann
  with Not_found -> None
474
475
let graphInsertState sort bs state =
476
  assert (not (GHt.mem !graphStates.(sort) bs));
477
  GHt.add !graphStates.(sort) bs state
478
479
let graphInsertCore sort bs core =
480
  assert (not (GHt.mem !graphCores.(sort) bs));
481
  GHt.add !graphCores.(sort) bs core
482
483
let graphInsertCnstr cset cnstr =
484 16af388e Christoph Egger
  assert (not (GHtS.mem !graphCnstrs cset));
485
  GHtS.add !graphCnstrs cset cnstr
486 4fd28192 Thorsten Wißmann
487
let graphReplaceCnstr cset cnstr =
488 16af388e Christoph Egger
  GHtS.replace !graphCnstrs cset cnstr
489 4fd28192 Thorsten Wißmann
490
let graphSizeState () =
491
  Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphStates
492
let graphSizeCore () =
493
  Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphCores
494 16af388e Christoph Egger
let graphSizeCnstr () = GHtS.length !graphCnstrs
495 4fd28192 Thorsten Wißmann
496
let graphAddRoot core =
497
  if !graphRoot = None then graphRoot := Some core
498
  else raise (C.CoAlgException "Root of graph is already set.")
499
500
let graphGetRoot () =
501
  match !graphRoot with
502
  | None -> raise (C.CoAlgException "Root of graph is not set.")
503
  | Some core -> core
504
505
506
(*****************************************************************************)
507
(*     "Module type" and a specific implementation of sets of constraints    *)
508
(*****************************************************************************)
509
510
let cssEmpty = BsSet.empty
511
let cssExists fkt css = BsSet.exists fkt css
512
let cssForall fkt css = BsSet.for_all fkt css
513
let cssUnion css1 css2 = BsSet.union css1 css2
514
let cssAdd cset css = BsSet.add cset css
515
let cssFold fkt css init = BsSet.fold fkt css init
516
let cssSingleton cset = BsSet.singleton cset
517
let cssEqual css1 css2 = BsSet.equal css1 css2
518 f335015f Thorsten Wißmann
let cssIter (action: cset -> unit) css =
519
    BsSet.iter action css
520 4fd28192 Thorsten Wißmann
521
522
(*****************************************************************************)
523
(*      "Module type" and a specific implementation of state nodes           *)
524
(*****************************************************************************)
525 73762b19 Thorsten Wißmann
let nodeCounter = ref 0
526
let nextNodeIdx () : int =
527
    let oldVal = !nodeCounter in
528
    nodeCounter := oldVal + 1;
529
    oldVal
530
531 3285ac30 Christoph Egger
let stateMake sort bs defer exp =
532
  { sortS = sort; bsS = bs; deferralS = defer; statusS = Expandable; parentsS = []; childrenS = [];
533 73762b19 Thorsten Wißmann
    constraintsS = cssEmpty; expandFkt = exp;
534 7eb41195 Hans-Peter Deifel
    idxS = nextNodeIdx()
535 73762b19 Thorsten Wißmann
  }
536 4fd28192 Thorsten Wißmann
let stateGetSort state = state.sortS
537
let stateGetBs state = state.bsS
538
let stateSetBs state bs = state.bsS <- bs
539 3285ac30 Christoph Egger
let stateGetDeferral state = state.deferralS
540
let stateSetDeferral state bs = state.deferralS <- bs
541 4fd28192 Thorsten Wißmann
let stateGetStatus state = state.statusS
542
let stateSetStatus state status = state.statusS <- status
543
let stateGetParents state = state.parentsS
544
let stateAddParent state parent = state.parentsS <- parent::state.parentsS
545
let stateGetRule state idx = List.nth state.childrenS (List.length state.childrenS - idx)
546
let stateGetRules state = state.childrenS
547
let stateAddRule state dep children =
548
  state.childrenS <- (dep, children)::state.childrenS;
549
  List.length state.childrenS
550
let stateGetConstraints state = state.constraintsS
551
let stateSetConstraints state csets = state.constraintsS <- csets
552
let stateNextRule state = state.expandFkt ()
553 7eb41195 Hans-Peter Deifel
let stateGetIdx (state:state) = state.idxS
554 4fd28192 Thorsten Wißmann
555
556
(*****************************************************************************)
557
(*      "Module type" and a specific implementation of core nodes            *)
558
(*****************************************************************************)
559
560 3285ac30 Christoph Egger
let coreMake sort bs defer solver fht =
561
  { sortC = sort; bsC = bs; deferralC = defer; statusC = Expandable; parentsC = []; childrenC = [];
562 73762b19 Thorsten Wißmann
    constraintsC = cssEmpty; solver = solver; fht = fht; constraintParents = [];
563 7eb41195 Hans-Peter Deifel
    idxC = nextNodeIdx()
564 73762b19 Thorsten Wißmann
  }
565 4fd28192 Thorsten Wißmann
let coreGetSort core = core.sortC
566
let coreGetBs core = core.bsC
567
let coreSetBs core bs = core.bsC <- bs
568 3285ac30 Christoph Egger
let coreGetDeferral core = core.deferralC
569
let coreSetDeferral core bs = core.deferralC <- bs
570 4fd28192 Thorsten Wißmann
let coreGetStatus core = core.statusC
571
let coreSetStatus core status = core.statusC <- status
572
let coreGetParents core = core.parentsC
573
let coreAddParent core parent idx = core.parentsC <- (parent, idx)::core.parentsC
574
let coreGetChildren core = core.childrenC
575
let coreAddChild core child = core.childrenC <- child::core.childrenC
576
let coreGetConstraints core = core.constraintsC
577
let coreSetConstraints core csets = core.constraintsC <- csets
578 e0e6eb62 Hans-Peter Deifel
let coreGetSolver core =
579
  match core.solver with
580
  | Some solver -> solver
581
  | None -> raise (Failure "Sat solver not allocated")
582 9f1263ec Christoph Egger
let coreDeallocateSolver core = core.solver <- None; FHt.reset core.fht
583 4fd28192 Thorsten Wißmann
let coreGetFht core = core.fht
584 7eb41195 Hans-Peter Deifel
let coreGetIdx (core:core) = core.idxC
585 4fd28192 Thorsten Wißmann
let coreGetConstraintParents core = core.constraintParents
586
let coreAddConstraintParent core cset =
587
  core.constraintParents <- cset::core.constraintParents
588
589
590
(*****************************************************************************)
591
(*      "Module type" and a specific implementation of sets of               *)
592
(*      states, cores, and constraints for the sat propagation               *)
593
(*****************************************************************************)
594
595 d283bf7a Thorsten Wißmann
let setEmptyState () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
596
let setEmptyCore () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
597 5956a56d Christoph Egger
let setCopyState set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx))
598
let setCopyCore set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx))
599 16af388e Christoph Egger
let setEmptyCnstr () = GHtS.create 128
600
let setAddState set state =
601
  GHt.add set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state)) state
602
let setAddCore set core =
603
  GHt.add set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core)) core
604
let setAddCnstr set cset = GHtS.add set cset ()
605
let setMemState set state =
606
  GHt.mem set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
607
let setMemCore set core =
608
  GHt.mem set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
609
let setMemCnstr set cset = GHtS.mem set cset
610
let setRemoveState set state =
611
  GHt.remove set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
612
let setRemoveCore set core =
613
  GHt.remove set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
614
let setRemoveCnstr set cset = GHtS.remove set cset
615 d283bf7a Thorsten Wißmann
let setIterState fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
616
let setIterCore fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
617 16af388e Christoph Egger
let setIterCnstr fkt set = GHtS.iter (fun cset () -> fkt cset) set
618 50df1dc2 Christoph Egger
let setLengthState seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta
619
let setLengthCore seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta
620 4fd28192 Thorsten Wißmann
621
622
(*****************************************************************************)
623
(*        "Module type" and a specific implementation of the mapping         *)
624
(*        between (local) formulae and literals of the sat solver,           *)
625
(*        and of a mapping of nominals to sets of formulae                   *)
626
(*****************************************************************************)
627
628
let lhtInit () = LHt.create 16
629
let lhtAdd lht lit f = LHt.add lht lit f
630
let lhtFind lht lit =
631
  try
632
    Some (LHt.find lht lit)
633
  with Not_found -> None
634
635
let fhtInit () = FHt.create 16
636
let fhtAdd fht f lit = FHt.add fht f lit
637
let fhtFind fht f =
638
  try
639
    Some (FHt.find fht f)
640
  with Not_found -> None
641
642
let nhtInit () = NHt.create 8
643
let nhtAdd nht nom bs = NHt.add nht nom bs
644
let nhtFind nht nom =
645
  try
646
    Some (NHt.find nht nom)
647
  with Not_found -> None
648
let nhtFold fkt nht init = NHt.fold fkt nht init
649
650
(*****************************************************************************)
651
(*         "Module type" and a specific implementation of sets of            *)
652
(*         local formulae and @-formulae                                     *)
653
(*****************************************************************************)
654
655
let tboxTable = ref (Array.make 0 S.dummyBS)
656
657
let bsetMake () = S.makeBS ()
658
let bsetAdd bs lf = S.addBSNoChk bs lf
659
let bsetMem bs lf = S.memBS bs lf
660 b7445f7e Thorsten Wißmann
let bsetRem bs lf = S.remBS bs lf
661 16af388e Christoph Egger
let bsetCompare bs1 bs2 = S.compareBS bs1 bs2
662 45d554b0 Thorsten Wißmann
let bsetMakeRealEmpty () =
663
    let res = bsetMake () in
664
    bsetRem res !S.bstrue; (* remove bstrue which is initially in an empty bset *)
665
    res
666 e7aaefa9 Hans-Peter Deifel
let bsetSingleton lf =
667
  let res = bsetMakeRealEmpty () in
668
  bsetAdd res lf;
669
  res
670 b7c3a47e Thorsten Wißmann
let bsetCopy bs = S.copyBS bs
671 4fd28192 Thorsten Wißmann
let bsetFold fkt bs init = S.foldBS fkt bs init
672
let bsetIter fkt bset = S.iterBS fkt bset
673 e4cd869a Thorsten Wißmann
let bsetFilter (a: bset) (f: localFormula -> bool) : bset =
674 45d554b0 Thorsten Wißmann
    let res = bsetMakeRealEmpty () in
675 e4cd869a Thorsten Wißmann
    bsetIter (fun form -> if (f form) then bsetAdd res form else ()) a;
676
    res
677
678 4fd28192 Thorsten Wißmann
let bsetAddTBox sort bs = S.unionBSNoChk bs !tboxTable.(sort)
679
680
let csetCompare cs1 cs2 = S.compareBS cs1 cs2
681
let csetMake () = S.makeBS ()
682
let csetAdd cs lf = S.addBSNoChk cs lf
683
let csetCopy cs = S.copyBS cs
684
let csetUnion cs1 cs2 = S.unionBSNoChk cs1 cs2
685
let csetHasDot cs = S.memBS cs !S.bsfalse
686
let csetAddDot cs = S.addBSNoChk cs !S.bsfalse
687
let csetRemDot cs = S.remBS cs !S.bsfalse
688
let csetAddTBox sort cs = S.unionBSNoChk cs !tboxTable.(sort)
689
let csetIter cs fkt =
690
  let fkt2 f = if not (f = !S.bstrue || f = !S.bsfalse) then fkt f else () in
691
  S.iterBS fkt2 cs
692
693
694
(*****************************************************************************)
695
(*            "Module type" and a specific implementation of                 *)
696
(*            local formulae and @-formulae                                  *)
697
(*****************************************************************************)
698
699
(** This table maps integers (representing formulae) to their corresponding formulae.
700
 *)
701
let arrayFormula = ref (Array.make 0 (Array.make 0 C.TRUE))
702
703
(** This table maps integers (representing formulae) to their corresponding type.
704
 *)
705
let arrayType = ref (Array.make 0 (Array.make 0 Other))
706
707
(** This lookup table maps formulae (represented as integers)
708
    to their negation (in negation normal form).
709
 *)
710
let arrayNeg = ref (Array.make 0 (Array.make 0 (-1)))
711
712
(** These lookup tables map formulae (represented as integers)
713
    to their decompositions (represented as integers).
714
    This is done according to the rules of the tableau procedure
715
    and depends on the type of the formulae.
716
 *)
717 86b07be8 Thorsten Wißmann
 (*
718
    for PML: arrayDest1 = the subformula
719 eda515b6 Thorsten Wißmann
             arrayNum  = the nominator of the probability
720
             arrayNum2 = the denominator of the probability
721 86b07be8 Thorsten Wißmann
 *)
722 f1fa9ad5 Thorsten Wißmann
let arrayDest1 = ref (Array.make 0 (Array.make 0 (-1)))  (* first subformula *)
723
let arrayDest2 = ref (Array.make 0 (Array.make 0 (-1)))  (* second subformula *)
724
let arrayDest3 = ref (Array.make 0 (Array.make 0 (-1)))  (* a role *)
725 d9f4e4af Christoph Egger
let arrayDeferral = ref (Array.make 0 (Array.make 0 (-1)))  (* deferral at point *)
726 29b2e3f3 Thorsten Wißmann
let arrayDestNum = ref (Array.make 0 (Array.make 0 (-1)))  (* an integer *)
727 eda515b6 Thorsten Wißmann
let arrayDestNum2 = ref (Array.make 0 (Array.make 0 (-1)))  (* another integer *)
728 f1fa9ad5 Thorsten Wißmann
let arrayDestAg = ref (Array.make 0 (Array.make 0 [|0|])) (* arrays of agents *)
729 4fd28192 Thorsten Wißmann
730
(** This lookup table maps formulae (represented as integers)
731
    to their @-wrapper.
732
 *)
733
let arrayAt = ref (Array.make 0 (Array.make 0 (FHt.create 64)))
734
735
let lfGetType sort f = !arrayType.(sort).(f)
736
let lfGetDest1 sort f = !arrayDest1.(sort).(f)
737
let lfGetDest2 sort f = !arrayDest2.(sort).(f)
738
let lfGetDest3 sort f = !arrayDest3.(sort).(f)
739 c67aca42 Christoph Egger
let lfGetDeferral sort f = !arrayDeferral.(sort).(f)
740 29b2e3f3 Thorsten Wißmann
let lfGetDestNum sort f = !arrayDestNum.(sort).(f)
741 eda515b6 Thorsten Wißmann
let lfGetDestNum2 sort f = !arrayDestNum2.(sort).(f)
742 f1fa9ad5 Thorsten Wißmann
let lfGetDestAg sort f = !arrayDestAg.(sort).(f)
743 4fd28192 Thorsten Wißmann
let lfGetNeg sort f =
744
  let nf = !arrayNeg.(sort).(f) in
745
  if nf >= 0 then Some nf else None
746
let lfGetAt (sort, nom) f =
747
  FHt.find !arrayAt.(sort).(f) nom
748 a0cffef0 Thorsten Wißmann
let lfToInt lf = lf
749
let lfFromInt num = num
750 f335015f Thorsten Wißmann
let lfGetFormula sort f = !arrayFormula.(sort).(f)
751
752 de84f40d Christoph Egger
let escapeHtml (input : string) : string =
753
  List.fold_right (fun (x, y) (str : string) -> Str.global_replace (Str.regexp x) y str)
754
    [("<", "&lt;") ; (">", "&gt;") ; ("&", "&amp;")]
755
    input
756
757 f335015f Thorsten Wißmann
let bsetToString sort bset : string =
758
    let toFormula (lf:localFormula) (lst: string list) : string list =
759
        let formula: C.formula = lfGetFormula sort lf in
760
        (C.string_of_formula formula) :: lst
761
    in
762
    let formulaList = bsetFold toFormula bset [] in
763
    "{ "^(String.concat ", " formulaList)^" }"
764
765
let csetToString sort cset = bsetToString sort cset
766
767 8d6bf016 Christoph Egger
let coreToString (core:core): string =
768 f335015f Thorsten Wißmann
    let helper cset lst : string list =
769
        (csetToString core.sortC cset):: lst
770
    in
771
    let constraints = cssFold helper core.constraintsC [] in
772 488cea0f Thorsten Wißmann
    let children =
773 7eb41195 Hans-Peter Deifel
        List.map (fun (st:state) -> string_of_int st.idxS) core.childrenC
774 488cea0f Thorsten Wißmann
    in
775 4164c8e1 Thorsten Wißmann
    let parents =
776 7eb41195 Hans-Peter Deifel
        List.map (fun (st,_:state*int) -> string_of_int st.idxS) core.parentsC
777 4164c8e1 Thorsten Wißmann
    in
778 7eb41195 Hans-Peter Deifel
    "Core "^(string_of_int core.idxC)^" {\n"^
779 f335015f Thorsten Wißmann
    "  Status: " ^ (nodeStatusToString core.statusC) ^ "\n"^
780
    "  " ^ bsetToString core.sortC core.bsC ^ "\n" ^
781 16af388e Christoph Egger
    "  Deferrals: \n" ^
782
    "    " ^ bsetToString core.sortC core.deferralC ^ "\n" ^
783 73762b19 Thorsten Wißmann
    "  Constraints: { "^(String.concat
784
                         "\n                 " constraints)^" }\n"^
785 488cea0f Thorsten Wißmann
    "  Children: { "^(String.concat
786
                         ", " children)^" }\n"^
787 4164c8e1 Thorsten Wißmann
    "  Parents: { "^(String.concat ", " parents)^" }\n"^
788 f335015f Thorsten Wißmann
    "}"
789 73762b19 Thorsten Wißmann
790
let stateToString (state:state): string =
791
    let helper cset lst : string list =
792
        (csetToString state.sortS cset):: lst
793
    in
794
    let constraints = cssFold helper state.constraintsS [] in
795
    let conclusionList =
796
        List.map (fun (_,lst) ->
797 7eb41195 Hans-Peter Deifel
                  List.map (fun (core:core) -> string_of_int core.idxC) lst
798 73762b19 Thorsten Wißmann
        ) state.childrenS
799
    in
800
    let conclusionList =
801
        List.map (fun x -> "{"^String.concat ", " x^"}") conclusionList
802
    in
803 4164c8e1 Thorsten Wißmann
    let parents =
804 7eb41195 Hans-Peter Deifel
        List.map (fun (co:core) -> string_of_int co.idxC) state.parentsS
805 4164c8e1 Thorsten Wißmann
    in
806 7eb41195 Hans-Peter Deifel
    "State "^(string_of_int state.idxS)^" {\n"^
807 73762b19 Thorsten Wißmann
    "  Status: " ^ (nodeStatusToString state.statusS) ^ "\n"^
808
    "  " ^ bsetToString state.sortS state.bsS ^ "\n" ^
809 16af388e Christoph Egger
    "  Deferrals: \n" ^
810
    "    " ^ bsetToString state.sortS state.deferralS ^ "\n" ^
811 73762b19 Thorsten Wißmann
    "  Constraints: { "^(String.concat
812
                         "\n                 " constraints)^" }\n"^
813
    "  Children: { "^(String.concat
814
                         "\n              " conclusionList)^" }\n"^
815 4164c8e1 Thorsten Wißmann
    "  Parents: { "^(String.concat ", " parents)^" }\n"^
816 73762b19 Thorsten Wißmann
    "}"
817
818 86c2c2ee Hans-Peter Deifel
let nodeToDot idx typ sort formulas deferrals status parentIdxs : string =
819
  let color = match status with
820
    | Sat -> "#8ae234"
821
    | Unsat -> "#ef2929"
822
    | Open -> "#729fcf"
823 c13029a3 Christoph Egger
    | Expandable -> "white"
824
  in
825 de84f40d Christoph Egger
  let toFormula (lf:localFormula) (lst: string list) : string list =
826 86c2c2ee Hans-Peter Deifel
    let formula: C.formula = lfGetFormula sort lf in
827
    if (bsetMem deferrals lf)
828
    then ("<U>"^(escapeHtml (C.string_of_formula formula))^"</U>") :: lst
829 de84f40d Christoph Egger
    else (escapeHtml (C.string_of_formula formula)) :: lst
830
  in
831 86c2c2ee Hans-Peter Deifel
  let formulaList = bsetFold toFormula formulas [] in
832
  let ownidx = (string_of_int idx) in
833 8d6bf016 Christoph Egger
  let parents =
834 86c2c2ee Hans-Peter Deifel
    List.map (fun (parentIdx) ->
835
              "Node"^string_of_int parentIdx^" -> Node"^ownidx^";")
836
             parentIdxs
837 8d6bf016 Christoph Egger
  in
838 86c2c2ee Hans-Peter Deifel
  let style = if typ = "Core" then "filled,rounded" else "filled" in
839
  "Node" ^ ownidx ^ " [shape=box,style=\"" ^ style
840
  ^ "\",fillcolor=\"" ^ color ^ "\""
841
  ^ ",label=<<B>" ^ typ ^ " "  ^ ownidx ^ "</B>"
842
  ^ "<BR/><BR/>" ^ (String.concat "<BR/>" formulaList)
843 de84f40d Christoph Egger
  ^ ">];\n"
844 8d6bf016 Christoph Egger
  ^ (String.concat "\n" parents)
845
846 86c2c2ee Hans-Peter Deifel
let stateToDot (state:state): string =
847
  nodeToDot state.idxS "State" state.sortS state.bsS state.deferralS
848
            state.statusS (List.map (fun c -> c.idxC) state.parentsS)
849 8d6bf016 Christoph Egger
850
let coreToDot (core:core): string =
851 86c2c2ee Hans-Peter Deifel
  nodeToDot core.idxC "Core" core.sortC core.bsC core.deferralC
852
            core.statusC (List.map (fun (s,_) -> s.idxS) core.parentsC)
853
854
let graphToDot () : string =
855
  let lines = ref ["digraph reasonerstate {"] in
856
  graphIterCores (fun core -> lines := (coreToDot core)::!lines);
857
  graphIterStates (fun state -> lines := (stateToDot state)::!lines);
858
859
  let legend =
860
    "subgraph legend {\n"
861
    ^ "key [label=<<TABLE CELLBORDER=\"0\" BGCOLOR=\"#d3d7cf\">\n"
862
    ^ "<TR><TD>Color:</TD><TD BGCOLOR=\"#8ae234\">sat</TD><TD BGCOLOR=\"#ef2929\">unsat</TD><TD BGCOLOR=\"#729fcf\">open</TD><TD BGCOLOR=\"white\">expandable</TD></TR>"
863
    ^ "<TR><TD>Rounded:</TD><TD>cores</TD></TR>"
864
    ^ "<TR><TD>Boxed:</TD><TD>states</TD></TR>"
865
    ^ "<TR><TD>Underlined:</TD><TD>focus</TD></TR>"
866
    ^ "</TABLE>>, shape=none];}" in
867
868
  lines := "}"::legend::!lines;
869
  String.concat "\n" (List.rev !lines)
870 8d6bf016 Christoph Egger
871 488cea0f Thorsten Wißmann
let queuePrettyStatus () =
872
  let printList (sl : int list) : string =
873
    String.concat ", " (List.map string_of_int sl)
874
  in
875
  (* TODO: are atFormulas always look-up-able for sort 0? *)
876
  (Printf.sprintf "%d Constraints: " (List.length !queueCnstrs))
877
  ^(String.concat ", " (List.map (csetToString 0) !queueCnstrs))
878
  ^(Printf.sprintf "\n%d States: " (List.length !queueStates))
879 7eb41195 Hans-Peter Deifel
  ^(printList (List.map (fun (st:state) -> st.idxS) !queueStates))
880 488cea0f Thorsten Wißmann
  ^(Printf.sprintf "\n%d Cores1: " (List.length !queueCores1))
881 7eb41195 Hans-Peter Deifel
  ^(printList (List.map (fun (co:core) -> co.idxC) !queueCores1))
882 488cea0f Thorsten Wißmann
  ^(Printf.sprintf "\n%d Cores2: " (List.length !queueCores2))
883 7eb41195 Hans-Peter Deifel
  ^(printList (List.map (fun (co:core) -> co.idxC) !queueCores2))
884 488cea0f Thorsten Wißmann
  ^"\n"
885
886 73762b19 Thorsten Wißmann
887
888 4fd28192 Thorsten Wißmann
889
let atFormulaGetSubformula f = !arrayDest1.(0).(f)
890
let atFormulaGetNominal f =
891
  let s = !arrayDest3.(0).(f) in
892
  let n = !arrayDest2.(0).(f) in
893
  (s, n)
894
895
let lfToAt _ lf = lf
896
897 b6653b96 Hans-Peter Deifel
898
type fragment = AlternationFree | AconjunctiveAltFree
899 f24367c4 Hans-Peter Deifel
type fragment_spec = Auto | Fragment of fragment
900 b6653b96 Hans-Peter Deifel
let fragment = ref AlternationFree
901
let getFragment () = !fragment
902
903
904 4b0d0388 Christoph Egger
(* Calculate all possible formulae. This includes all subformulae and
905
   in the case of μ-Calculus the Fischer-Ladner closure.
906 4fd28192 Thorsten Wißmann
907 4b0d0388 Christoph Egger
   TODO: variable sort needs to match epected sort
908
 *)
909 cb12f8a5 Christoph Egger
let rec detClosure vars nomTbl hcF fset vset atset nomset s f =
910
  let newvars = List.filter (fun (x) -> C.hc_freeIn x f) vars in
911
  let detClosure_ = detClosure newvars in
912
  let deferral = if List.length newvars > 0
913
                 then (List.hd newvars)
914
                 else "ε" in
915 4fd28192 Thorsten Wißmann
  if s < 0 || s >= Array.length fset then
916
    let sstr = string_of_int s in
917
    raise (C.CoAlgException ("Invalid sort (i.e. sort out of range): " ^ sstr))
918
  else ();
919 653eaa4b Christoph Egger
  if C.HcFHt.mem vset.(s) f &&
920 066ed7b8 Christoph Egger
    (compare (C.HcFHt.find vset.(s) f) deferral = 0 ||
921
        compare deferral "ε" = 0)
922 1b17ef3c Christoph Egger
  then ()
923 4fd28192 Thorsten Wißmann
  else
924 cb12f8a5 Christoph Egger
    let () = C.HcFHt.add vset.(s) f deferral in
925 4fd28192 Thorsten Wißmann
    let () = C.HcFHt.add fset.(s) f () in
926
    let (func, sortlst) = !sortTable.(s) in
927
    match f.HC.node with
928
    | C.HCTRUE
929 43194ed2 Christoph Egger
    | C.HCFALSE
930
    | C.HCVAR _ -> ()
931 4fd28192 Thorsten Wißmann
    | C.HCAP name ->
932
        if C.isNominal name then begin
933
          Hashtbl.replace nomset name s;
934
          match nomTbl name with
935
          | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name))
936
          | Some sort ->
937
              if sort <> s then
938
                let str1 = "Nominal: " ^ name ^ " of sort " ^ (string_of_int sort) in
939
                let str2 = " is used in sort " ^ (string_of_int s) ^ "." in
940
                raise (C.CoAlgException (str1 ^ str2))
941
              else ()
942
        end else ()
943
    | C.HCNOT _ -> ()
944
    | C.HCAT (name, f1) ->
945
        C.HcFHt.replace atset f ();
946
        let s1 =
947
          match nomTbl name with
948
          | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name))
949
          | Some sort -> sort
950
        in
951
        let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
952 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset s1 hcnom;
953
        detClosure_ nomTbl hcF fset vset atset nomset s1 f1
954 4fd28192 Thorsten Wißmann
    | C.HCOR (f1, f2)
955
    | C.HCAND (f1, f2) ->
956 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset s f1;
957
        detClosure_ nomTbl hcF fset vset atset nomset s f2
958 4fd28192 Thorsten Wißmann
    | C.HCEX (_, f1)
959
    | C.HCAX (_, f1) ->
960 f4e43751 Christoph Egger
        if (func <> MultiModalK && func <> MultiModalKD && func <> Monotone)
961 2a84977e Thorsten Wißmann
            || List.length sortlst <> 1
962
        then raise (C.CoAlgException "Ex/Ax-formula is used in wrong sort.")
963 4fd28192 Thorsten Wißmann
        else ();
964 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
965 f1fa9ad5 Thorsten Wißmann
    | C.HCENFORCES (_, f1)
966
    | C.HCALLOWS (_, f1) ->
967
        if func <> CoalitionLogic || List.length sortlst <> 1
968
        then raise (C.CoAlgException "[{Agents}]-formula is used in wrong sort.")
969
        else ();
970 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
971 af276a36 Thorsten Wißmann
    | C.HCMORETHAN (_,_,f1)
972
    | C.HCMAXEXCEPT (_,_,f1) ->
973 29b2e3f3 Thorsten Wißmann
        if func <> GML || List.length sortlst <> 1
974
        then raise (C.CoAlgException "[{>=,<=}]-formula is used in wrong sort.")
975
        else ();
976 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
977 86b07be8 Thorsten Wißmann
    | C.HCATLEASTPROB (_,f1)
978 9bae2c4f Thorsten Wißmann
    | C.HCLESSPROBFAIL (_,f1) ->
979 86b07be8 Thorsten Wißmann
        if func <> PML || List.length sortlst <> 1
980 c855ba91 Thorsten Wißmann
        then raise (C.CoAlgException "[{>=,<}]-formula with probability is used in wrong sort.")
981 86b07be8 Thorsten Wißmann
        else ();
982 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1;
983 9bae2c4f Thorsten Wißmann
        (*
984
            TODO: add ¬ f1 to the closure!
985
        detClosure nomTbl hcF fset atset nomset (List.hd sortlst) (f1.HC.node.negNde)
986
        *)
987 5e0983fe Thorsten Wißmann
    | C.HCCONST color
988
    | C.HCCONSTN color ->
989
      begin match func with
990
      | Constant params ->
991
            if not (List.exists ((=) color) params)
992
            then raise (C.CoAlgException ("=-formula mentions \""^color^"\" but the only"
993
                             ^" choices are: "^(String.concat ", " params)))
994
      | _ -> raise (C.CoAlgException "=-formula is used in wrong sort.")
995
      end;
996
      if List.length sortlst <> 1
997 c49eea11 Thorsten Wißmann
        then raise (C.CoAlgException "=-formula is used in wrong sort.")
998
        else ();
999
      (* NB: =-formulae have no subformlae hence no closure *)
1000 19f5dad0 Dirk Pattinson
    | C.HCID f1 ->
1001
        if func <> Identity || List.length sortlst <> 1
1002
        then raise (C.CoAlgException "Identity operator applied to
1003
          formula of wrong sort.")
1004
        else ();
1005 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1;
1006 19f5dad0 Dirk Pattinson
    | C.HCNORM (f1, f2)
1007
    | C.HCNORMN(f1, f2) ->
1008
      if func <> DefaultImplication || List.length sortlst <> 1 then
1009
          raise (C.CoAlgException "Default Implication applied to
1010
          formulae of wrong sort.")
1011
        else ();
1012 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 0) f1;
1013
        detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 1) f2
1014 19f5dad0 Dirk Pattinson
1015 d58bba0f Dirk Pattinson
    | C.HCCHC (f1, f2) ->
1016 4fd28192 Thorsten Wißmann
        if func <> Choice || List.length sortlst <> 2 then
1017
          raise (C.CoAlgException "Choice formula is used in wrong sort.")
1018
        else ();
1019 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 0) f1;
1020
        detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 1) f2
1021 4fd28192 Thorsten Wißmann
    | C.HCFUS (first, f1) ->
1022
        if func <> Fusion || List.length sortlst <> 2 then
1023
          raise (C.CoAlgException "Fusion formula is used in wrong sort.")
1024
        else ();
1025
        let s1 = List.nth sortlst (if first then 0 else 1) in
1026 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset s1 f1
1027 034a8dea Christoph Egger
    (*
1028 6553983f Christoph Egger
       FL(μ X . φ) = {μ X . φ} ∪ FL(φ[X|->μ X . φ])
1029 034a8dea Christoph Egger
     *)
1030
    | C.HCMU (name, f1) ->
1031 e08cd8a9 Christoph Egger
       begin
1032
         if C.hc_freeIn name f1
1033
         then
1034
           C.HcFHt.replace vset.(s) f name
1035
         else ();
1036
         let unfold = C.hc_replace hcF name f f1 in
1037
         let appendvars = List.append newvars [name] in
1038
         detClosure appendvars nomTbl hcF fset vset atset nomset s unfold
1039
       end
1040 034a8dea Christoph Egger
    | C.HCNU (name, f1) ->
1041
       let unfold = C.hc_replace hcF name f f1 in
1042 cb12f8a5 Christoph Egger
       detClosure_ nomTbl hcF fset vset atset nomset s unfold
1043 6553983f Christoph Egger
1044 4fd28192 Thorsten Wißmann
1045
let detClosureAt hcF atset name f () =
1046
  match f.HC.node with
1047
  | C.HCTRUE
1048
  | C.HCFALSE
1049
  | C.HCOR _
1050
  | C.HCAND _
1051
  | C.HCAT _ -> ()
1052
  | _ ->
1053 034a8dea Christoph Egger
      let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
1054 4fd28192 Thorsten Wißmann
      C.HcFHt.replace atset at ()
1055
1056
(** Initialises the arrays for a formula and its integer representation.
1057
 *)
1058 d9f4e4af Christoph Egger
let initTables nomTbl hcF htF htR vset s f n =
1059 4fd28192 Thorsten Wißmann
  !arrayFormula.(s).(n) <- f.HC.fml;
1060 d9f4e4af Christoph Egger
  !arrayDeferral.(s).(n) <- Hashtbl.hash (C.HcFHt.find vset.(s) f);
1061 4fd28192 Thorsten Wißmann
  let fneg = f.HC.neg in
1062
  if C.HcFHt.mem htF.(s) fneg then !arrayNeg.(s).(n) <- C.HcFHt.find htF.(s) fneg;
1063
  let (_, sortlst) = !sortTable.(s) in
1064
  match f.HC.node with
1065
  | C.HCTRUE
1066 3b055ae8 dirk
  | C.HCFALSE -> !arrayType.(s).(n) <- TrueFalseF
1067 4fd28192 Thorsten Wißmann
  | C.HCAP name ->
1068
      if C.isNominal name then !arrayType.(s).(n) <- NomF
1069
      else !arrayType.(s).(n) <- Other
1070
  | C.HCNOT _ -> !arrayType.(s).(n) <- Other
1071
  | C.HCAT (name, f1) ->
1072
      !arrayType.(s).(n) <- AtF;
1073
      let s1 =
1074
        match nomTbl name with
1075
        | None -> assert false
1076
        | Some sort -> sort
1077
      in
1078
      let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
1079
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s1) f1;
1080
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s1) hcnom;
1081
      !arrayDest3.(s).(n) <- s1
1082
  | C.HCOR (f1, f2) ->
1083
      !arrayType.(s).(n) <- OrF;
1084
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) f1;
1085
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s) f2
1086
  | C.HCAND (f1, f2) ->
1087
      !arrayType.(s).(n) <- AndF;
1088
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) f1;
1089
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s) f2
1090 034a8dea Christoph Egger
  | C.HCEX (role, f1) ->
1091 4fd28192 Thorsten Wißmann
      !arrayType.(s).(n) <- ExF;
1092
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1093 034a8dea Christoph Egger
      !arrayDest3.(s).(n) <-
1094 4fd28192 Thorsten Wißmann
        if Hashtbl.mem htR role then Hashtbl.find htR role
1095
        else
1096
          let size = Hashtbl.length htR in
1097
          Hashtbl.add htR role size;
1098
          size
1099
  | C.HCAX (role, f1) ->
1100
      !arrayType.(s).(n) <- AxF;
1101
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1102
      !arrayDest3.(s).(n) <-
1103
        if Hashtbl.mem htR role then Hashtbl.find htR role
1104
        else
1105
          let size = Hashtbl.length htR in
1106
          Hashtbl.add htR role size;
1107
          size
1108 f1fa9ad5 Thorsten Wißmann
  | C.HCENFORCES (aglist, f1) ->  (* aglist = list of agents *)
1109
      !arrayType.(s).(n) <- EnforcesF;
1110
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1111
      !arrayDestAg.(s).(n) <- Array.of_list aglist
1112
  | C.HCALLOWS (aglist, f1) ->  (* aglist = list of agents *)
1113
      !arrayType.(s).(n) <- AllowsF;
1114
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1115
      !arrayDestAg.(s).(n) <- Array.of_list aglist
1116 af276a36 Thorsten Wißmann
  | C.HCMORETHAN (cnt,role,f1) ->
1117
      !arrayType.(s).(n) <- MoreThanF;
1118 29b2e3f3 Thorsten Wißmann
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1119
      !arrayDestNum.(s).(n) <- cnt;
1120
      !arrayDest3.(s).(n) <-
1121
        if Hashtbl.mem htR role then Hashtbl.find htR role
1122
        else
1123
          let size = Hashtbl.length htR in
1124
          Hashtbl.add htR role size;
1125
          size
1126 af276a36 Thorsten Wißmann
  | C.HCMAXEXCEPT (cnt,role,f1) ->
1127
      !arrayType.(s).(n) <- MaxExceptF;
1128 29b2e3f3 Thorsten Wißmann
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1129
      !arrayDestNum.(s).(n) <- cnt;
1130
      !arrayDest3.(s).(n) <-
1131
        if Hashtbl.mem htR role then Hashtbl.find htR role
1132
        else
1133
          let size = Hashtbl.length htR in
1134
          Hashtbl.add htR role size;
1135
          size
1136 86b07be8 Thorsten Wißmann
  | C.HCATLEASTPROB (p,f1) ->
1137
      !arrayType.(s).(n) <- AtLeastProbF;
1138
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1139 eda515b6 Thorsten Wißmann
      !arrayDestNum.(s).(n) <- p.C.nominator;
1140
      !arrayDestNum2.(s).(n) <- p.C.denominator
1141 9bae2c4f Thorsten Wißmann
  | C.HCLESSPROBFAIL (p,f1) ->
1142
      !arrayType.(s).(n) <- LessProbFailF;
1143 86b07be8 Thorsten Wißmann
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1144 eda515b6 Thorsten Wißmann
      !arrayDestNum.(s).(n) <- p.C.nominator;
1145
      !arrayDestNum2.(s).(n) <- p.C.denominator
1146 c49eea11 Thorsten Wißmann
  | C.HCCONST str ->
1147
      !arrayType.(s).(n) <- ConstF; (* type of modality *)
1148
      (* Dest1 and Dest2 are the arguments, here: none *)
1149
      (* DestNum and DestNum2 are the numerators and denonimators of
1150
      fractions, here: none *)
1151
      !arrayDest3.(s).(n) <-
1152
        if Hashtbl.mem htR str then Hashtbl.find htR str
1153
        else
1154
          let size = Hashtbl.length htR in
1155
          Hashtbl.add htR str size;
1156
          size
1157
      (* Dest3 are the role names / identifiers for constant values *)
1158
      (* idea: hash identifier names *)
1159
  | C.HCCONSTN str ->
1160
      !arrayType.(s).(n) <- ConstnF; (* type of modality *)
1161
      (* Dest1 and Dest2 are the arguments, here: none *)
1162
      (* DestNum and DestNum2 are the numerators and denonimators of
1163
      fractions, here: none *)
1164
      !arrayDest3.(s).(n) <-
1165
        if Hashtbl.mem htR str then Hashtbl.find htR str
1166
        else
1167
          let size = Hashtbl.length htR in
1168
          Hashtbl.add htR str size;
1169
          size
1170
      (* Dest3 are the role names / identifiers for constant values *)
1171
      (* idea: hash identifier names *)
1172 19f5dad0 Dirk Pattinson
  | C.HCID (f1) ->
1173
      !arrayType.(s).(n) <- IdF;
1174 d58bba0f Dirk Pattinson
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1
1175 034a8dea Christoph Egger
  | C.HCNORM (f1, f2) ->
1176 19f5dad0 Dirk Pattinson
      !arrayType.(s).(n) <- NormF;
1177
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
1178
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2
1179 034a8dea Christoph Egger
  | C.HCNORMN (f1, f2) ->
1180 19f5dad0 Dirk Pattinson
      !arrayType.(s).(n) <- NormnF;
1181
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
1182
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2
1183
  (* note that choice is self-dual *)
1184 d58bba0f Dirk Pattinson
  | C.HCCHC (f1, f2) ->
1185 4fd28192 Thorsten Wißmann
      !arrayType.(s).(n) <- ChcF;
1186
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
1187
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2
1188
  | C.HCFUS (first, f1) ->
1189
      !arrayType.(s).(n) <- FusF;
1190
      let s1 = List.nth sortlst (if first then 0 else 1) in
1191
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s1) f1;
1192
      !arrayDest3.(s).(n) <- if first then 0 else 1
1193 5ec97220 Christoph Egger
  | C.HCMU (name, f1) ->
1194
     !arrayType.(s).(n) <- MuF;
1195 034a8dea Christoph Egger
     let unfold = C.hc_replace hcF name f f1 in
1196
     !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold
1197 5ec97220 Christoph Egger
  | C.HCNU (name, f1) ->
1198 034a8dea Christoph Egger
     !arrayType.(s).(n) <- NuF;
1199
     let unfold = C.hc_replace hcF name f f1 in
1200
     !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold
1201 5ec97220 Christoph Egger
  | C.HCVAR _ -> !arrayType.(s).(n) <- Other
1202
1203 4fd28192 Thorsten Wißmann
1204
let initTablesAt hcF htF name sort =
1205
  let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
1206
  let nom = C.HcFHt.find htF.(sort) hcnom in
1207
  let addAt f n =
1208
    match f.HC.node with
1209
    | C.HCTRUE
1210
    | C.HCFALSE
1211
    | C.HCOR _
1212
    | C.HCAND _
1213
    | C.HCAT _ -> ()
1214
    | _ ->
1215 034a8dea Christoph Egger
        let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
1216 4fd28192 Thorsten Wißmann
        let atn = C.HcFHt.find htF.(0) at in
1217
        FHt.add !arrayAt.(sort).(n) nom atn
1218
  in
1219
  C.HcFHt.iter addAt htF.(sort)
1220
1221 f24367c4 Hans-Peter Deifel
let ppFormulae fragSpec nomTbl tbox (s, f) =
1222 4fd28192 Thorsten Wißmann
  let card = Array.length !sortTable in
1223
  if card <= 0 then
1224
    raise (C.CoAlgException "Number of sorts must be positive.")
1225
  else ();
1226 bc8db289 Christoph Egger
  C.verifyFormula f;
1227 4fd28192 Thorsten Wißmann
  let nnfAndSimplify f = C.simplify (C.nnf f) in
1228 f828ad2f Thorsten Wißmann
  let  f1    = nnfAndSimplify f in
1229
  let nf1    = nnfAndSimplify (C.NOT f) in
1230
  let  tbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify f)) tbox in
1231
  let ntbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify (C.NOT f))) tbox in
1232
1233
  let hcF     =  C.HcFormula.create true in
1234
  let  hcf    = C.hc_formula hcF  f1 in
1235
  let nhcf    = C.hc_formula hcF nf1 in
1236
  let  hctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f))  tbox1 in
1237
  let nhctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f)) ntbox1 in
1238 4fd28192 Thorsten Wißmann
  let hcfalse = C.hc_formula hcF C.FALSE in
1239 f828ad2f Thorsten Wißmann
  let hctrue  = C.hc_formula hcF C.TRUE in
1240 4fd28192 Thorsten Wißmann
1241
  let fset = Array.init card (fun _ -> C.HcFHt.create 128) in
1242 cb12f8a5 Christoph Egger
  let vset = Array.init card (fun _ -> C.HcFHt.create 128) in
1243 4fd28192 Thorsten Wißmann
  let atset = C.HcFHt.create 64 in
1244
  let nomset = Hashtbl.create 16 in
1245
  for i = 0 to card-1 do
1246 cb12f8a5 Christoph Egger
    detClosure [] nomTbl hcF fset vset atset nomset i hcfalse;
1247
    detClosure [] nomTbl hcF fset vset atset nomset i hctrue;
1248 4fd28192 Thorsten Wißmann
  done;
1249 cb12f8a5 Christoph Egger
  detClosure [] nomTbl hcF fset vset atset nomset s  hcf;
1250
  detClosure [] nomTbl hcF fset vset atset nomset s nhcf;
1251
  List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f)
1252
            hctbox;
1253
  List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f)
1254
            nhctbox;
1255 4fd28192 Thorsten Wißmann
  Hashtbl.iter (fun n s -> C.HcFHt.iter (detClosureAt hcF atset n) fset.(s)) nomset;
1256
1257
  let htF = Array.init card (fun _ -> C.HcFHt.create 128) in
1258
  for i = 0 to card-1 do
1259
    C.HcFHt.add htF.(i) hcfalse 0;
1260
    C.HcFHt.add htF.(i) hctrue 1
1261
  done;
1262
  let addAts f () idx =
1263
    for i = 0 to card-1 do
1264
      C.HcFHt.add htF.(i) f idx
1265
    done;
1266
    idx + 1
1267
  in
1268
  let sizeAt = C.HcFHt.fold addAts atset 2 in
1269
  let addFml i f () idx =
1270
    if C.HcFHt.mem htF.(i) f then idx
1271
    else begin
1272
      C.HcFHt.add htF.(i) f idx;
1273
      idx+1
1274
    end
1275
  in
1276
  let size = ref 0 in
1277
  for i = 0 to card-1 do
1278
    let size2 = C.HcFHt.fold (addFml i) fset.(i) sizeAt in
1279
    if size2 > !size then size := size2 else ()
1280
  done;
1281
1282 f24367c4 Hans-Peter Deifel
  begin match fragSpec with
1283
  | Auto -> if C.isMuAconjunctive f then
1284
              fragment := AconjunctiveAltFree
1285
            else
1286
              fragment := AlternationFree
1287
  | Fragment AconjunctiveAltFree ->
1288
     if not (C.isMuAconjunctive f) then
1289
       raise (CoAlgFormula.CoAlgException "Formula not in required fragment")
1290
     else fragment := AconjunctiveAltFree
1291
  | Fragment AlternationFree ->
1292
     if C.isMuAconjunctive f then
1293
       raise (CoAlgFormula.CoAlgException "Formula not in required fragment")
1294
     else fragment := AlternationFree
1295
  end;
1296
1297
  (* if (fragSpec = Auto || fragSpec = Fragment AconjunctiveAltFree) && C.isMuAconjunctive f then *)
1298
  (*   fragment := AconjunctiveAltFree; *)
1299
  (* else if (fragSpec = Auto || fragSpec = Fragment AlternationFree) && (not (C.isMuAconjunctive f)) *)
1300
  (*   fragment := AlternationFree; *)
1301
  (* else *)
1302
  (*   raise (CoAlgFormula.CoAlgException "Formula not in required fragment"); *)
1303 b6653b96 Hans-Peter Deifel
1304 4fd28192 Thorsten Wißmann
  arrayFormula := Array.init card (fun _ -> Array.make !size C.TRUE);
1305
  arrayType := Array.init card (fun _ -> Array.make !size Other);
1306
  arrayDest1 := Array.init card (fun _ -> Array.make !size (-1));
1307
  arrayDest2 := Array.init card (fun _ -> Array.make !size (-1));
1308
  arrayDest3 := Array.init card (fun _ -> Array.make !size (-1));
1309 d9f4e4af Christoph Egger
  arrayDeferral := Array.init card (fun _-> Array.make !size(-1));
1310 4fd28192 Thorsten Wißmann
  arrayNeg := Array.init card (fun _ -> Array.make !size (-1));
1311 29b2e3f3 Thorsten Wißmann
  arrayDestNum := Array.init card (fun _ -> Array.make !size (-1));
1312 eda515b6 Thorsten Wißmann
  arrayDestNum2 := Array.init card (fun _ -> Array.make !size (-1));
1313 98af95fb Thorsten Wißmann
  arrayDestAg := Array.init card (fun _ -> Array.make !size (Array.make 0 (-1)));
1314 4fd28192 Thorsten Wißmann
  let htR = Hashtbl.create 128 in
1315 d9f4e4af Christoph Egger
  Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR vset s) ht) htF;
1316 4fd28192 Thorsten Wißmann
  arrayAt := Array.init card (fun _ -> Array.init !size (fun _ -> FHt.create 8));
1317
  Hashtbl.iter (initTablesAt hcF htF) nomset;
1318
1319
  S.initMisc !size (C.HcFHt.find htF.(0) hcfalse) (C.HcFHt.find htF.(0) hctrue) (-1) (-1) (-1);
1320
  let initbs = bsetMake () in
1321
  bsetAdd initbs (C.HcFHt.find htF.(s) hcf);
1322
  let tboxTbl = Array.init card (fun _ -> bsetMake ()) in
1323
  List.iter (fun (s, f) -> bsetAdd tboxTbl.(s) (C.HcFHt.find htF.(s) f)) hctbox;
1324
  tboxTable := tboxTbl;
1325
  (tbox1, (s, f1), initbs)
1326 a57eb439 Hans-Peter Deifel
1327
(* vim: set et sw=2 sts=2 ts=8 : *)