Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgMisc.ml @ 5956a56d

History | View | Annotate | Download (46 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 * 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
    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
  | MultiModalKD
82
  | CoalitionLogic
83
  | GML
84
  | PML
85
  | Constant of string list
86
  | Identity
87
  | DefaultImplication
88
  | Choice
89
  | Fusion
90

    
91
(* functors whose constructor takes additional parameters *)
92
type parametricFunctorName =
93
  | NameConstant
94

    
95
(* this type should only be used in the following few helper functions *)
96
type functorName =
97
  | NPa of functors (* No Parameters = functor without parameters *)
98
  | Pa  of parametricFunctorName (* Parameters = functor with parameters *)
99

    
100
let unaryfunctor2name : (functorName*string) list =
101
  [ (NPa MultiModalK , "MultiModalK")
102
  ; (NPa MultiModalKD , "MultiModalKD")
103
  ; (NPa GML ,           "GML")
104
  ; (NPa PML ,           "PML")
105
  ; (NPa CoalitionLogic , "CoalitionLogic")
106
  ; (NPa MultiModalK , "K")
107
  ; (NPa MultiModalKD , "KD")
108
  ; (NPa CoalitionLogic , "CL")
109
  ; (Pa  NameConstant , "Const")
110
  ; (Pa  NameConstant , "Constant")
111
  ; (NPa Identity, "Id")
112
  ; (NPa Identity, "Identity")
113
  ]
114

    
115
let functor2name : (functorName*string) list =
116
  L.append unaryfunctor2name
117
  [ (NPa Choice , "Choice")
118
  ; (NPa Fusion , "Fusion")
119
  ]
120

    
121
let functor_apply_parameters (func : parametricFunctorName) (params: string list) : functors option =
122
    (* apply parameter list to the constructor, denoted by the functor name func *)
123
    (* return None, if the parameters somehow don't match the required parameters *)
124
    match func with
125
    | NameConstant -> Some (Constant params)
126

    
127

    
128
let functor_of_string str params : functors option =
129
    let fst (a,b) = a in
130
    try
131
        let functorName = fst (List.find (fun (f,name) -> name = str) functor2name) in
132
        match functorName with
133
        | NPa x -> Some x
134
        | Pa f -> functor_apply_parameters f params
135
    with Not_found -> None
136

    
137
let unaryfunctor_of_string str params =
138
    match (functor_of_string str params) with
139
    | Some Choice -> None
140
    | Some Fusion -> None
141
    | x -> x
142

    
143
let string_of_functor (f: functors) : string =
144
    (* replace f orrectly with possibly some Pa wrapper *)
145
    (* also put the parameters into some suffix which will be appended later *)
146
    let f,suffix = match f with
147
            | Constant params -> Pa NameConstant, " "^(String.concat " " params)
148
            | _ -> NPa f, ""
149
    in
150
    let snd (a,b) = b in
151
    try
152
        let name = snd (List.find (fun (f2,name) -> f = f2) functor2name) in
153
        name ^ suffix
154
    with Not_found -> assert false
155

    
156
(* This type may be extended for additional logics. *)
157
type formulaType =
158
  | Other
159
  | TrueFalseF (* constant true or false *)
160
  | AndF
161
  | OrF
162
  | AtF
163
  | NomF
164
  | ExF  (* Existential / diamond *)
165
  | AxF  (* Universal / box *)
166
  | EnforcesF (* diamond of CL *)
167
  | AllowsF   (* box of CL *)
168
  | MoreThanF (* more than n successors = diamond in gml *)
169
  | MaxExceptF(* at most n exceptions = box in gml *)
170
  | AtLeastProbF (* for PML *)
171
  | LessProbFailF (* box for PML *)
172
  | ConstF (* constant functor *)
173
  | ConstnF (* constant functor *)
174
  | IdF (* Identity functor *)
175
  | NormF (* Default Implication *)
176
  | NormnF (* negation normal form of default implication *)
177
  | ChcF (* Choice *)
178
  | FusF (* Fusion *)
179
  | MuF
180
  | NuF
181

    
182
type localFormula = int
183
type bset = S.bitset
184

    
185
type atFormula = int
186
type cset = S.bitset
187
type csetSet = BsSet.t
188

    
189
type lht = localFormula LHt.t
190
type fht = Minisat.lit FHt.t
191
type nht = bset NHt.t
192

    
193
type state = { sortS : sort;
194
               mutable bsS : bset; (* a set of formulas who are either literals or
195
                                      modalities (TODO: also @-formulas?).
196
                                      the state is satisfiable if /\bsS is satisfiable.
197
                                    *)
198
               mutable deferralS : bset; (* which formulas still have deferrals *)
199
               mutable statusS : nodeStatus;
200
               mutable parentsS : core list; mutable childrenS : (dependencies * core list) list;
201
               mutable constraintsS : csetSet; expandFkt : stateExpander;
202
               idx: int }
203

    
204
and core = { (* for details, see documentation of newCore *)
205
             sortC : sort;
206
             mutable bsC : bset; (* a set of arbitrary formulas.
207
                                    the present core is satisfiable if /\ bsC is satisfiable *)
208
             mutable deferralC : bset; (* which formulas still have deferrals *)
209
             mutable statusC : nodeStatus;
210
             mutable parentsC : (state * int) list;
211
             mutable childrenC : state list;
212
             mutable constraintsC : csetSet;
213
             solver : Minisat.solver; (* a solver to find satisfying assignemnts for bsC.
214
                                         the solver returns "satisfiable" iff
215
                                         there is a satisfying assignment of
216
                                         bsC which is not represented by some state from the
217
                                         childrenC yet.
218
                                       *)
219
             fht : fht; (* mapping of boolean subformulas of bsC to their corresponding literals
220
                           of the Minisat solver
221
                         *)
222
             mutable constraintParents : cset list;
223
             idx : int }
224

    
225
and setState = state GHt.t array
226

    
227
and setCore = core GHt.t array
228

    
229
and setCnstr = unit GHtS.t
230

    
231

    
232
(*****************************************************************************)
233
(*                Types that are hard coded into the algorithm               *)
234
(*****************************************************************************)
235

    
236
and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *)
237
                  | Conjunctive of 'a (*specifies that all of the 'a need  to be satifsfied *)
238

    
239
and stateExpander = rule lazylist
240

    
241
and sort = C.sort
242

    
243
and nodeStatus =
244
  | Expandable
245
  | Open
246
  | Sat
247
  | Unsat
248

    
249
(* In K, given the singleton list [bs] returns the list of all Ax'es
250
   responsible for the individual members of bs being part of the core
251
   as well as the Ex.
252

    
253
   So given the state { <>φ , []ψ , []η } and the core { φ , ψ , η },
254
   dependency would map { η } to { <>φ , []η } and { ψ } to { <>φ , []ψ }
255
*)
256
and dependencies = bset list -> bset
257

    
258
(* Note: sort * bset * bset is to be read as sort * formulas_in_core * deferrals_in_core *)
259
and rule = (dependencies * (sort * bset * bset) lazylist)
260

    
261
and 'a lazyliststep =
262
  | MultipleElements of 'a list
263
  | SingleElement    of 'a
264
  | NoMoreElements
265

    
266
and 'a lazylist = unit -> 'a lazyliststep
267

    
268
and ruleEnumeration = rule lazyliststep
269

    
270
let nodeStatusToString : nodeStatus -> string = function
271
  | Expandable -> "Expandable"
272
  | Open -> "Open"
273
  | Sat -> "Sat"
274
  | Unsat -> "Unsat"
275

    
276
let lazylistFromList a_list =
277
    let list_state = ref (Some a_list) in
278
    fun () -> begin match !list_state with
279
              | Some (a_list) -> begin
280
                    list_state := None;
281
                    MultipleElements a_list
282
                end
283
              | None -> NoMoreElements
284
              end
285

    
286
let rec listFromLazylist evalfunc =
287
    let step = evalfunc () in
288
    match step with
289
    | NoMoreElements -> []
290
    | SingleElement x -> x::(listFromLazylist evalfunc)
291
    | MultipleElements xs -> List.append xs (listFromLazylist evalfunc)
292

    
293
type nominal = sort * localFormula
294

    
295
type node =
296
  | State of state
297
  | Core of core
298

    
299
type constrnt =
300
  | UnsatC
301
  | SatC
302
  | OpenC of node list
303
  | UnexpandedC of node list
304

    
305
type propagateElement =
306
  | UState of state * int option
307
  | UCore of core * bool
308
  | UCnstr of cset
309

    
310
type queueElement =
311
  | QState of state
312
  | QCore of core
313
  | QCnstr of cset
314
  | QEmpty
315

    
316
type sortTable = (functors * int list) array
317

    
318
exception CoAlg_finished of bool
319

    
320

    
321
let sortTable = ref (Array.make 0 (MultiModalK, [1]))
322

    
323
let junctionEvalBool : (bool list junction) -> bool = function
324
    | Disjunctive l -> List.fold_right (||) l false
325
    | Conjunctive l -> List.fold_right (&&) l true
326

    
327
let junctionEval (f: 'a -> bool) : 'a list junction -> bool = function
328
    | Disjunctive l -> List.fold_right (fun x y -> (f x) || y) l false
329
    | Conjunctive l -> List.fold_right (fun x y -> (f x) && y) l true
330

    
331
let optionalizeOperator (f: 'a -> 'b -> 'c) (x: 'a option) (y: 'b option) : 'c option =
332
    match x with
333
    | None -> None
334
    | Some x -> (match y with
335
                 | None -> None
336
                 | Some y -> Some (f x y))
337

    
338
let junctionEvalBoolOption : bool option list junction -> bool option =
339
    let f extreme op x y = (* ensure that: (Some True) || None = Some True *)
340
        if x = extreme || y = extreme
341
        then extreme
342
        else optionalizeOperator op x y
343
    in function
344
    | Disjunctive l ->
345
        List.fold_right (f (Some true)  (||)) l (Some false)
346
    | Conjunctive l ->
347
        List.fold_right (f (Some false) (&&)) l (Some true)
348

    
349
let junctionExtract : 'a junction -> ('a * ('b -> 'b junction)) = function
350
    | Disjunctive l -> (l, fun x -> Disjunctive x)
351
    | Conjunctive l -> (l, fun x -> Conjunctive x)
352

    
353
(*****************************************************************************)
354
(*      "Module type" and a specific implementation of the main queue        *)
355
(*****************************************************************************)
356

    
357
let queueStates = ref ([] : state list)
358
let queueCores1 = ref ([] : core list)
359
let queueCores2 = ref ([] : core list)
360
let queueCnstrs = ref ([] : cset list)
361
let doPropagation = ref false
362

    
363
let queueInit () =
364
  queueStates := [];
365
  queueCores1 := [];
366
  queueCores2 := [];
367
  queueCnstrs := [];
368
  doPropagation := false
369

    
370
let queueIsEmpty () =
371
  !queueStates = [] && !queueCores1 = [] && !queueCores2 = [] && !queueCnstrs = []
372

    
373
let queueInsertState state = queueStates := state::!queueStates
374

    
375
(* original version: breadth-first *)
376
let queueInsertCore core = queueCores2 := core::!queueCores2
377

    
378
(* experiment: depth first
379
let queueInsertCore core = queueCores1 := core::!queueCores1
380
*)
381

    
382
let queueInsertCnstr cset = queueCnstrs := cset::!queueCnstrs
383

    
384
let queueGetElement () =
385
  if !queueCnstrs <> [] then
386
    let res = List.hd !queueCnstrs in
387
    queueCnstrs := List.tl !queueCnstrs;
388
    QCnstr res
389
  else if !queueStates <> [] then
390
    let res = List.hd !queueStates in
391
    queueStates := List.tl !queueStates;
392
    QState res
393
  else if !queueCores1 <> [] then
394
    let res = List.hd !queueCores1 in
395
    queueCores1 := List.tl !queueCores1;
396
    QCore res
397
  else if !queueCores2 = [] then QEmpty
398
  else
399
    let res = List.hd !queueCores2 in
400
    doPropagation := true;
401
    queueCores1 := List.tl !queueCores2;
402
    queueCores2 := [];
403
    QCore res
404

    
405
let doNominalPropagation () = !doPropagation
406

    
407
let doSatPropagation () =
408
  let res = !doPropagation in
409
  doPropagation := false;
410
  res
411

    
412
(*****************************************************************************)
413
(*        "Module type" and a specific implementation of the graph           *)
414
(*****************************************************************************)
415

    
416
let graphStates = ref (Array.make 0 (GHt.create 0 : state GHt.t))
417
let graphCores = ref (Array.make 0 (GHt.create 0 : core GHt.t))
418
let graphCnstrs = ref (GHtS.create 0 : constrnt GHtS.t)
419
let graphRoot = ref (None : core option)
420

    
421
let graphInit () =
422
  let size = Array.length !sortTable in
423
  graphStates := Array.init size (fun _ -> GHt.create 128);
424
  graphCores := Array.init size (fun _ -> GHt.create 128);
425
  graphCnstrs := GHtS.create 128;
426
  graphRoot := None
427

    
428
let graphIterStates fkt =
429
  Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphStates
430

    
431
let graphIterCores fkt =
432
  Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphCores
433

    
434
let graphIterCnstrs fkt = GHtS.iter fkt !graphCnstrs
435

    
436
let graphClearCnstr () =
437
  let newGraph = GHtS.create (GHtS.length !graphCnstrs) in
438
  let copyCnstr cset cnstr =
439
    match cnstr with
440
    | UnsatC
441
    | SatC -> GHtS.add newGraph cset cnstr
442
    | OpenC _ -> GHtS.add newGraph cset (OpenC [])
443
    | UnexpandedC _ -> GHtS.add newGraph cset (UnexpandedC [])
444
  in
445
  GHtS.iter copyCnstr !graphCnstrs;
446
  graphCnstrs := newGraph
447

    
448
let graphFindState sort bs =
449
  try
450
    Some (GHt.find !graphStates.(sort) bs)
451
  with Not_found -> None
452

    
453
let graphFindCore sort bs =
454
  try
455
    Some (GHt.find !graphCores.(sort) bs)
456
  with Not_found -> None
457

    
458
let graphFindCnstr cset =
459
  try
460
    Some (GHtS.find !graphCnstrs cset)
461
  with Not_found -> None
462

    
463
let graphInsertState sort bs state =
464
  assert (not (GHt.mem !graphStates.(sort) bs));
465
  GHt.add !graphStates.(sort) bs state
466

    
467
let graphInsertCore sort bs core =
468
  assert (not (GHt.mem !graphCores.(sort) bs));
469
  GHt.add !graphCores.(sort) bs core
470

    
471
let graphInsertCnstr cset cnstr =
472
  assert (not (GHtS.mem !graphCnstrs cset));
473
  GHtS.add !graphCnstrs cset cnstr
474

    
475
let graphReplaceCnstr cset cnstr =
476
  GHtS.replace !graphCnstrs cset cnstr
477

    
478
let graphSizeState () =
479
  Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphStates
480
let graphSizeCore () =
481
  Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphCores
482
let graphSizeCnstr () = GHtS.length !graphCnstrs
483

    
484
let graphAddRoot core =
485
  if !graphRoot = None then graphRoot := Some core
486
  else raise (C.CoAlgException "Root of graph is already set.")
487

    
488
let graphGetRoot () =
489
  match !graphRoot with
490
  | None -> raise (C.CoAlgException "Root of graph is not set.")
491
  | Some core -> core
492

    
493

    
494
(*****************************************************************************)
495
(*     "Module type" and a specific implementation of sets of constraints    *)
496
(*****************************************************************************)
497

    
498
let cssEmpty = BsSet.empty
499
let cssExists fkt css = BsSet.exists fkt css
500
let cssForall fkt css = BsSet.for_all fkt css
501
let cssUnion css1 css2 = BsSet.union css1 css2
502
let cssAdd cset css = BsSet.add cset css
503
let cssFold fkt css init = BsSet.fold fkt css init
504
let cssSingleton cset = BsSet.singleton cset
505
let cssEqual css1 css2 = BsSet.equal css1 css2
506
let cssIter (action: cset -> unit) css =
507
    BsSet.iter action css
508

    
509

    
510
(*****************************************************************************)
511
(*      "Module type" and a specific implementation of state nodes           *)
512
(*****************************************************************************)
513
let nodeCounter = ref 0
514
let nextNodeIdx () : int =
515
    let oldVal = !nodeCounter in
516
    nodeCounter := oldVal + 1;
517
    oldVal
518

    
519
let stateMake sort bs defer exp =
520
  { sortS = sort; bsS = bs; deferralS = defer; statusS = Expandable; parentsS = []; childrenS = [];
521
    constraintsS = cssEmpty; expandFkt = exp;
522
    idx = nextNodeIdx()
523
  }
524
let stateGetSort state = state.sortS
525
let stateGetBs state = state.bsS
526
let stateSetBs state bs = state.bsS <- bs
527
let stateGetDeferral state = state.deferralS
528
let stateSetDeferral state bs = state.deferralS <- bs
529
let stateGetStatus state = state.statusS
530
let stateSetStatus state status = state.statusS <- status
531
let stateGetParents state = state.parentsS
532
let stateAddParent state parent = state.parentsS <- parent::state.parentsS
533
let stateGetRule state idx = List.nth state.childrenS (List.length state.childrenS - idx)
534
let stateGetRules state = state.childrenS
535
let stateAddRule state dep children =
536
  state.childrenS <- (dep, children)::state.childrenS;
537
  List.length state.childrenS
538
let stateGetConstraints state = state.constraintsS
539
let stateSetConstraints state csets = state.constraintsS <- csets
540
let stateNextRule state = state.expandFkt ()
541
let stateGetIdx (state:state) = state.idx
542

    
543

    
544
(*****************************************************************************)
545
(*      "Module type" and a specific implementation of core nodes            *)
546
(*****************************************************************************)
547

    
548
let coreMake sort bs defer solver fht =
549
  { sortC = sort; bsC = bs; deferralC = defer; statusC = Expandable; parentsC = []; childrenC = [];
550
    constraintsC = cssEmpty; solver = solver; fht = fht; constraintParents = [];
551
    idx = nextNodeIdx()
552
  }
553
let coreGetSort core = core.sortC
554
let coreGetBs core = core.bsC
555
let coreSetBs core bs = core.bsC <- bs
556
let coreGetDeferral core = core.deferralC
557
let coreSetDeferral core bs = core.deferralC <- bs
558
let coreGetStatus core = core.statusC
559
let coreSetStatus core status = core.statusC <- status
560
let coreGetParents core = core.parentsC
561
let coreAddParent core parent idx = core.parentsC <- (parent, idx)::core.parentsC
562
let coreGetChildren core = core.childrenC
563
let coreAddChild core child = core.childrenC <- child::core.childrenC
564
let coreGetConstraints core = core.constraintsC
565
let coreSetConstraints core csets = core.constraintsC <- csets
566
let coreGetSolver core = core.solver
567
let coreGetFht core = core.fht
568
let coreGetIdx (core:core) = core.idx
569
let coreGetConstraintParents core = core.constraintParents
570
let coreAddConstraintParent core cset =
571
  core.constraintParents <- cset::core.constraintParents
572

    
573

    
574
(*****************************************************************************)
575
(*      "Module type" and a specific implementation of sets of               *)
576
(*      states, cores, and constraints for the sat propagation               *)
577
(*****************************************************************************)
578

    
579
let setEmptyState () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
580
let setEmptyCore () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
581
let setCopyState set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx))
582
let setCopyCore set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx))
583
let setEmptyCnstr () = GHtS.create 128
584
let setAddState set state =
585
  GHt.add set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state)) state
586
let setAddCore set core =
587
  GHt.add set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core)) core
588
let setAddCnstr set cset = GHtS.add set cset ()
589
let setMemState set state =
590
  GHt.mem set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
591
let setMemCore set core =
592
  GHt.mem set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
593
let setMemCnstr set cset = GHtS.mem set cset
594
let setRemoveState set state =
595
  GHt.remove set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
596
let setRemoveCore set core =
597
  GHt.remove set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
598
let setRemoveCnstr set cset = GHtS.remove set cset
599
let setIterState fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
600
let setIterCore fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
601
let setIterCnstr fkt set = GHtS.iter (fun cset () -> fkt cset) set
602
let setLengthState seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta
603
let setLengthCore seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta
604

    
605

    
606
(*****************************************************************************)
607
(*        "Module type" and a specific implementation of the mapping         *)
608
(*        between (local) formulae and literals of the sat solver,           *)
609
(*        and of a mapping of nominals to sets of formulae                   *)
610
(*****************************************************************************)
611

    
612
let lhtInit () = LHt.create 16
613
let lhtAdd lht lit f = LHt.add lht lit f
614
let lhtFind lht lit =
615
  try
616
    Some (LHt.find lht lit)
617
  with Not_found -> None
618

    
619
let fhtInit () = FHt.create 16
620
let fhtAdd fht f lit = FHt.add fht f lit
621
let fhtFind fht f =
622
  try
623
    Some (FHt.find fht f)
624
  with Not_found -> None
625

    
626
let nhtInit () = NHt.create 8
627
let nhtAdd nht nom bs = NHt.add nht nom bs
628
let nhtFind nht nom =
629
  try
630
    Some (NHt.find nht nom)
631
  with Not_found -> None
632
let nhtFold fkt nht init = NHt.fold fkt nht init
633

    
634
(*****************************************************************************)
635
(*         "Module type" and a specific implementation of sets of            *)
636
(*         local formulae and @-formulae                                     *)
637
(*****************************************************************************)
638

    
639
let tboxTable = ref (Array.make 0 S.dummyBS)
640

    
641
let bsetMake () = S.makeBS ()
642
let bsetAdd bs lf = S.addBSNoChk bs lf
643
let bsetMem bs lf = S.memBS bs lf
644
let bsetRem bs lf = S.remBS bs lf
645
let bsetCompare bs1 bs2 = S.compareBS bs1 bs2
646
let bsetMakeRealEmpty () =
647
    let res = bsetMake () in
648
    bsetRem res !S.bstrue; (* remove bstrue which is initially in an empty bset *)
649
    res
650
let bsetCopy bs = S.copyBS bs
651
let bsetFold fkt bs init = S.foldBS fkt bs init
652
let bsetIter fkt bset = S.iterBS fkt bset
653
let bsetFilter (a: bset) (f: localFormula -> bool) : bset =
654
    let res = bsetMakeRealEmpty () in
655
    bsetIter (fun form -> if (f form) then bsetAdd res form else ()) a;
656
    res
657

    
658
let bsetAddTBox sort bs = S.unionBSNoChk bs !tboxTable.(sort)
659

    
660
let csetCompare cs1 cs2 = S.compareBS cs1 cs2
661
let csetMake () = S.makeBS ()
662
let csetAdd cs lf = S.addBSNoChk cs lf
663
let csetCopy cs = S.copyBS cs
664
let csetUnion cs1 cs2 = S.unionBSNoChk cs1 cs2
665
let csetHasDot cs = S.memBS cs !S.bsfalse
666
let csetAddDot cs = S.addBSNoChk cs !S.bsfalse
667
let csetRemDot cs = S.remBS cs !S.bsfalse
668
let csetAddTBox sort cs = S.unionBSNoChk cs !tboxTable.(sort)
669
let csetIter cs fkt =
670
  let fkt2 f = if not (f = !S.bstrue || f = !S.bsfalse) then fkt f else () in
671
  S.iterBS fkt2 cs
672

    
673

    
674
(*****************************************************************************)
675
(*            "Module type" and a specific implementation of                 *)
676
(*            local formulae and @-formulae                                  *)
677
(*****************************************************************************)
678

    
679
(** This table maps integers (representing formulae) to their corresponding formulae.
680
 *)
681
let arrayFormula = ref (Array.make 0 (Array.make 0 C.TRUE))
682

    
683
(** This table maps integers (representing formulae) to their corresponding type.
684
 *)
685
let arrayType = ref (Array.make 0 (Array.make 0 Other))
686

    
687
(** This lookup table maps formulae (represented as integers)
688
    to their negation (in negation normal form).
689
 *)
690
let arrayNeg = ref (Array.make 0 (Array.make 0 (-1)))
691

    
692
(** These lookup tables map formulae (represented as integers)
693
    to their decompositions (represented as integers).
694
    This is done according to the rules of the tableau procedure
695
    and depends on the type of the formulae.
696
 *)
697
 (*
698
    for PML: arrayDest1 = the subformula
699
             arrayNum  = the nominator of the probability
700
             arrayNum2 = the denominator of the probability
701
 *)
702
let arrayDest1 = ref (Array.make 0 (Array.make 0 (-1)))  (* first subformula *)
703
let arrayDest2 = ref (Array.make 0 (Array.make 0 (-1)))  (* second subformula *)
704
let arrayDest3 = ref (Array.make 0 (Array.make 0 (-1)))  (* a role *)
705
let arrayDeferral = ref (Array.make 0 (Array.make 0 (-1)))  (* deferral at point *)
706
let arrayDestNum = ref (Array.make 0 (Array.make 0 (-1)))  (* an integer *)
707
let arrayDestNum2 = ref (Array.make 0 (Array.make 0 (-1)))  (* another integer *)
708
let arrayDestAg = ref (Array.make 0 (Array.make 0 [|0|])) (* arrays of agents *)
709

    
710
(** This lookup table maps formulae (represented as integers)
711
    to their @-wrapper.
712
 *)
713
let arrayAt = ref (Array.make 0 (Array.make 0 (FHt.create 64)))
714

    
715
let lfGetType sort f = !arrayType.(sort).(f)
716
let lfGetDest1 sort f = !arrayDest1.(sort).(f)
717
let lfGetDest2 sort f = !arrayDest2.(sort).(f)
718
let lfGetDest3 sort f = !arrayDest3.(sort).(f)
719
let lfGetDeferral sort f = !arrayDeferral.(sort).(f)
720
let lfGetDestNum sort f = !arrayDestNum.(sort).(f)
721
let lfGetDestNum2 sort f = !arrayDestNum2.(sort).(f)
722
let lfGetDestAg sort f = !arrayDestAg.(sort).(f)
723
let lfGetNeg sort f =
724
  let nf = !arrayNeg.(sort).(f) in
725
  if nf >= 0 then Some nf else None
726
let lfGetAt (sort, nom) f =
727
  FHt.find !arrayAt.(sort).(f) nom
728
let lfToInt lf = lf
729
let lfFromInt num = num
730
let lfGetFormula sort f = !arrayFormula.(sort).(f)
731

    
732
let escapeHtml (input : string) : string =
733
  List.fold_right (fun (x, y) (str : string) -> Str.global_replace (Str.regexp x) y str)
734
    [("<", "&lt;") ; (">", "&gt;") ; ("&", "&amp;")]
735
    input
736

    
737
let bsetToString sort bset : string =
738
    let toFormula (lf:localFormula) (lst: string list) : string list =
739
        let formula: C.formula = lfGetFormula sort lf in
740
        (C.string_of_formula formula) :: lst
741
    in
742
    let formulaList = bsetFold toFormula bset [] in
743
    "{ "^(String.concat ", " formulaList)^" }"
744

    
745
let csetToString sort cset = bsetToString sort cset
746

    
747
let coreToString (core:core): string =
748
    let helper cset lst : string list =
749
        (csetToString core.sortC cset):: lst
750
    in
751
    let constraints = cssFold helper core.constraintsC [] in
752
    let children =
753
        List.map (fun (st:state) -> string_of_int st.idx) core.childrenC
754
    in
755
    let parents =
756
        List.map (fun (st,_:state*int) -> string_of_int st.idx) core.parentsC
757
    in
758
    "Core "^(string_of_int core.idx)^" {\n"^
759
    "  Status: " ^ (nodeStatusToString core.statusC) ^ "\n"^
760
    "  " ^ bsetToString core.sortC core.bsC ^ "\n" ^
761
    "  Deferrals: \n" ^
762
    "    " ^ bsetToString core.sortC core.deferralC ^ "\n" ^
763
    "  Constraints: { "^(String.concat
764
                         "\n                 " constraints)^" }\n"^
765
    "  Children: { "^(String.concat
766
                         ", " children)^" }\n"^
767
    "  Parents: { "^(String.concat ", " parents)^" }\n"^
768
    "}"
769

    
770
let stateToString (state:state): string =
771
    let helper cset lst : string list =
772
        (csetToString state.sortS cset):: lst
773
    in
774
    let constraints = cssFold helper state.constraintsS [] in
775
    let core2idx core = core.idx in
776
    let fst (a,b) = a in
777
    let conclusionList =
778
        List.map (fun (_,lst) ->
779
                  List.map (fun (core:core) -> string_of_int core.idx) lst
780
        ) state.childrenS
781
    in
782
    let conclusionList =
783
        List.map (fun x -> "{"^String.concat ", " x^"}") conclusionList
784
    in
785
    let parents =
786
        List.map (fun (co:core) -> string_of_int co.idx) state.parentsS
787
    in
788
    "State "^(string_of_int state.idx)^" {\n"^
789
    "  Status: " ^ (nodeStatusToString state.statusS) ^ "\n"^
790
    "  " ^ bsetToString state.sortS state.bsS ^ "\n" ^
791
    "  Deferrals: \n" ^
792
    "    " ^ bsetToString state.sortS state.deferralS ^ "\n" ^
793
    "  Constraints: { "^(String.concat
794
                         "\n                 " constraints)^" }\n"^
795
    "  Children: { "^(String.concat
796
                         "\n              " conclusionList)^" }\n"^
797
    "  Parents: { "^(String.concat ", " parents)^" }\n"^
798
    "}"
799

    
800
let stateToDot (state:state): string =
801
  let color = match state.statusS with
802
    | Sat -> "green"
803
    | Unsat -> "red"
804
    | Open -> "yellow"
805
    | Expandable -> "white"
806
  in
807
  let toFormula (lf:localFormula) (lst: string list) : string list =
808
    let formula: C.formula = lfGetFormula state.sortS lf in
809
    if (bsetMem state.deferralS lf)
810
    then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst
811
    else (escapeHtml (C.string_of_formula formula)) :: lst
812
  in
813
  let formulaList = bsetFold toFormula state.bsS [] in
814
  let ownidx = (string_of_int state.idx) in
815
  let parents =
816
    List.map (fun (co:core) ->
817
              "Node"^string_of_int co.idx^" -> Node"^ownidx^";")
818
             state.parentsS
819
  in
820
  "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
821
  ^ ",label=<State "  ^ ownidx
822
  ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
823
  ^ ">];\n"
824
  ^ (String.concat "\n" parents)
825

    
826

    
827
let coreToDot (core:core): string =
828
  let color = match core.statusC with
829
    | Sat -> "green"
830
    | Unsat -> "red"
831
    | Open -> "yellow"
832
    | Expandable -> "white"
833
  in
834
  let toFormula (lf:localFormula) (lst: string list) : string list =
835
    let formula: C.formula = lfGetFormula core.sortC lf in
836
    if (bsetMem core.deferralC lf)
837
    then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst
838
    else (escapeHtml (C.string_of_formula formula)) :: lst
839
  in
840
  let formulaList = bsetFold toFormula core.bsC [] in
841
  let ownidx = (string_of_int core.idx) in
842
  let parents =
843
    List.map (fun (st,_:state*int) ->
844
              "Node"^string_of_int st.idx^" -> Node"^ownidx^";")
845
             core.parentsC
846
  in
847
  "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
848
  ^ ",label=<Core "  ^ ownidx
849
  ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
850
  ^ ">];\n"
851
  ^ (String.concat "\n" parents)
852

    
853

    
854
let queuePrettyStatus () =
855
  let printList (sl : int list) : string =
856
    String.concat ", " (List.map string_of_int sl)
857
  in
858
  (* TODO: are atFormulas always look-up-able for sort 0? *)
859
  (Printf.sprintf "%d Constraints: " (List.length !queueCnstrs))
860
  ^(String.concat ", " (List.map (csetToString 0) !queueCnstrs))
861
  ^(Printf.sprintf "\n%d States: " (List.length !queueStates))
862
  ^(printList (List.map (fun (st:state) -> st.idx) !queueStates))
863
  ^(Printf.sprintf "\n%d Cores1: " (List.length !queueCores1))
864
  ^(printList (List.map (fun (co:core) -> co.idx) !queueCores1))
865
  ^(Printf.sprintf "\n%d Cores2: " (List.length !queueCores2))
866
  ^(printList (List.map (fun (co:core) -> co.idx) !queueCores2))
867
  ^"\n"
868

    
869

    
870

    
871

    
872
let atFormulaGetSubformula f = !arrayDest1.(0).(f)
873
let atFormulaGetNominal f =
874
  let s = !arrayDest3.(0).(f) in
875
  let n = !arrayDest2.(0).(f) in
876
  (s, n)
877

    
878
let lfToAt _ lf = lf
879

    
880
(* Calculate all possible formulae. This includes all subformulae and
881
   in the case of μ-Calculus the Fischer-Ladner closure.
882

    
883
   TODO: variable sort needs to match epected sort
884
 *)
885
let rec detClosure vars nomTbl hcF fset vset atset nomset s f =
886
  let newvars = List.filter (fun (x) -> C.hc_freeIn x f) vars in
887
  let detClosure_ = detClosure newvars in
888
  let deferral = if List.length newvars > 0
889
                 then (List.hd newvars)
890
                 else "ε" in
891
  if s < 0 || s >= Array.length fset then
892
    let sstr = string_of_int s in
893
    raise (C.CoAlgException ("Invalid sort (i.e. sort out of range): " ^ sstr))
894
  else ();
895
  if C.HcFHt.mem vset.(s) f &&
896
    (compare (C.HcFHt.find vset.(s) f) deferral = 0 ||
897
        compare deferral "ε" = 0)
898
  then ()
899
  else
900
    let () = C.HcFHt.add vset.(s) f deferral in
901
    let () = C.HcFHt.add fset.(s) f () in
902
    let (func, sortlst) = !sortTable.(s) in
903
    match f.HC.node with
904
    | C.HCTRUE
905
    | C.HCFALSE
906
    | C.HCVAR _ -> ()
907
    | C.HCAP name ->
908
        if C.isNominal name then begin
909
          Hashtbl.replace nomset name s;
910
          match nomTbl name with
911
          | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name))
912
          | Some sort ->
913
              if sort <> s then
914
                let str1 = "Nominal: " ^ name ^ " of sort " ^ (string_of_int sort) in
915
                let str2 = " is used in sort " ^ (string_of_int s) ^ "." in
916
                raise (C.CoAlgException (str1 ^ str2))
917
              else ()
918
        end else ()
919
    | C.HCNOT _ -> ()
920
    | C.HCAT (name, f1) ->
921
        C.HcFHt.replace atset f ();
922
        let s1 =
923
          match nomTbl name with
924
          | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name))
925
          | Some sort -> sort
926
        in
927
        let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
928
        detClosure_ nomTbl hcF fset vset atset nomset s1 hcnom;
929
        detClosure_ nomTbl hcF fset vset atset nomset s1 f1
930
    | C.HCOR (f1, f2)
931
    | C.HCAND (f1, f2) ->
932
        detClosure_ nomTbl hcF fset vset atset nomset s f1;
933
        detClosure_ nomTbl hcF fset vset atset nomset s f2
934
    | C.HCEX (_, f1)
935
    | C.HCAX (_, f1) ->
936
        if (func <> MultiModalK && func <> MultiModalKD)
937
            || List.length sortlst <> 1
938
        then raise (C.CoAlgException "Ex/Ax-formula is used in wrong sort.")
939
        else ();
940
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
941
    | C.HCENFORCES (_, f1)
942
    | C.HCALLOWS (_, f1) ->
943
        if func <> CoalitionLogic || List.length sortlst <> 1
944
        then raise (C.CoAlgException "[{Agents}]-formula is used in wrong sort.")
945
        else ();
946
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
947
    | C.HCMORETHAN (_,_,f1)
948
    | C.HCMAXEXCEPT (_,_,f1) ->
949
        if func <> GML || List.length sortlst <> 1
950
        then raise (C.CoAlgException "[{>=,<=}]-formula is used in wrong sort.")
951
        else ();
952
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
953
    | C.HCATLEASTPROB (_,f1)
954
    | C.HCLESSPROBFAIL (_,f1) ->
955
        if func <> PML || List.length sortlst <> 1
956
        then raise (C.CoAlgException "[{>=,<}]-formula with probability is used in wrong sort.")
957
        else ();
958
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1;
959
        (*
960
            TODO: add ¬ f1 to the closure!
961
        detClosure nomTbl hcF fset atset nomset (List.hd sortlst) (f1.HC.node.negNde)
962
        *)
963
    | C.HCCONST color
964
    | C.HCCONSTN color ->
965
      begin match func with
966
      | Constant params ->
967
            if not (List.exists ((=) color) params)
968
            then raise (C.CoAlgException ("=-formula mentions \""^color^"\" but the only"
969
                             ^" choices are: "^(String.concat ", " params)))
970
      | _ -> raise (C.CoAlgException "=-formula is used in wrong sort.")
971
      end;
972
      if List.length sortlst <> 1
973
        then raise (C.CoAlgException "=-formula is used in wrong sort.")
974
        else ();
975
      (* NB: =-formulae have no subformlae hence no closure *)
976
    | C.HCID f1 ->
977
        if func <> Identity || List.length sortlst <> 1
978
        then raise (C.CoAlgException "Identity operator applied to
979
          formula of wrong sort.")
980
        else ();
981
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1;
982
    | C.HCNORM (f1, f2)
983
    | C.HCNORMN(f1, f2) ->
984
      if func <> DefaultImplication || List.length sortlst <> 1 then
985
          raise (C.CoAlgException "Default Implication applied to
986
          formulae of wrong sort.")
987
        else ();
988
        detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 0) f1;
989
        detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 1) f2
990

    
991
    | C.HCCHC (f1, f2) ->
992
        if func <> Choice || List.length sortlst <> 2 then
993
          raise (C.CoAlgException "Choice formula is used in wrong sort.")
994
        else ();
995
        detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 0) f1;
996
        detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 1) f2
997
    | C.HCFUS (first, f1) ->
998
        if func <> Fusion || List.length sortlst <> 2 then
999
          raise (C.CoAlgException "Fusion formula is used in wrong sort.")
1000
        else ();
1001
        let s1 = List.nth sortlst (if first then 0 else 1) in
1002
        detClosure_ nomTbl hcF fset vset atset nomset s1 f1
1003
    (*
1004
       FL(μ X . φ) = {μ X . φ} ∪ FL(φ[X|->μ X . φ])
1005
     *)
1006
    | C.HCMU (name, f1) ->
1007
       let () = C.HcFHt.replace vset.(s) f name in
1008
       let unfold = C.hc_replace hcF name f f1 in
1009
       let appendvars = List.append newvars [name] in
1010
       detClosure appendvars nomTbl hcF fset vset atset nomset s unfold
1011
    | C.HCNU (name, f1) ->
1012
       let unfold = C.hc_replace hcF name f f1 in
1013
       detClosure_ nomTbl hcF fset vset atset nomset s unfold
1014

    
1015

    
1016
let detClosureAt hcF atset name f () =
1017
  match f.HC.node with
1018
  | C.HCTRUE
1019
  | C.HCFALSE
1020
  | C.HCOR _
1021
  | C.HCAND _
1022
  | C.HCAT _ -> ()
1023
  | _ ->
1024
      let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
1025
      C.HcFHt.replace atset at ()
1026

    
1027
(** Initialises the arrays for a formula and its integer representation.
1028
 *)
1029
let initTables nomTbl hcF htF htR vset s f n =
1030
  !arrayFormula.(s).(n) <- f.HC.fml;
1031
  !arrayDeferral.(s).(n) <- Hashtbl.hash (C.HcFHt.find vset.(s) f);
1032
  let fneg = f.HC.neg in
1033
  if C.HcFHt.mem htF.(s) fneg then !arrayNeg.(s).(n) <- C.HcFHt.find htF.(s) fneg;
1034
  let (_, sortlst) = !sortTable.(s) in
1035
  match f.HC.node with
1036
  | C.HCTRUE
1037
  | C.HCFALSE -> !arrayType.(s).(n) <- TrueFalseF
1038
  | C.HCAP name ->
1039
      if C.isNominal name then !arrayType.(s).(n) <- NomF
1040
      else !arrayType.(s).(n) <- Other
1041
  | C.HCNOT _ -> !arrayType.(s).(n) <- Other
1042
  | C.HCAT (name, f1) ->
1043
      !arrayType.(s).(n) <- AtF;
1044
      let s1 =
1045
        match nomTbl name with
1046
        | None -> assert false
1047
        | Some sort -> sort
1048
      in
1049
      let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
1050
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s1) f1;
1051
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s1) hcnom;
1052
      !arrayDest3.(s).(n) <- s1
1053
  | C.HCOR (f1, f2) ->
1054
      !arrayType.(s).(n) <- OrF;
1055
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) f1;
1056
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s) f2
1057
  | C.HCAND (f1, f2) ->
1058
      !arrayType.(s).(n) <- AndF;
1059
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) f1;
1060
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s) f2
1061
  | C.HCEX (role, f1) ->
1062
      !arrayType.(s).(n) <- ExF;
1063
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1064
      !arrayDest3.(s).(n) <-
1065
        if Hashtbl.mem htR role then Hashtbl.find htR role
1066
        else
1067
          let size = Hashtbl.length htR in
1068
          Hashtbl.add htR role size;
1069
          size
1070
  | C.HCAX (role, f1) ->
1071
      !arrayType.(s).(n) <- AxF;
1072
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1073
      !arrayDest3.(s).(n) <-
1074
        if Hashtbl.mem htR role then Hashtbl.find htR role
1075
        else
1076
          let size = Hashtbl.length htR in
1077
          Hashtbl.add htR role size;
1078
          size
1079
  | C.HCENFORCES (aglist, f1) ->  (* aglist = list of agents *)
1080
      !arrayType.(s).(n) <- EnforcesF;
1081
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1082
      !arrayDestAg.(s).(n) <- Array.of_list aglist
1083
  | C.HCALLOWS (aglist, f1) ->  (* aglist = list of agents *)
1084
      !arrayType.(s).(n) <- AllowsF;
1085
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1086
      !arrayDestAg.(s).(n) <- Array.of_list aglist
1087
  | C.HCMORETHAN (cnt,role,f1) ->
1088
      !arrayType.(s).(n) <- MoreThanF;
1089
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1090
      !arrayDestNum.(s).(n) <- cnt;
1091
      !arrayDest3.(s).(n) <-
1092
        if Hashtbl.mem htR role then Hashtbl.find htR role
1093
        else
1094
          let size = Hashtbl.length htR in
1095
          Hashtbl.add htR role size;
1096
          size
1097
  | C.HCMAXEXCEPT (cnt,role,f1) ->
1098
      !arrayType.(s).(n) <- MaxExceptF;
1099
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1100
      !arrayDestNum.(s).(n) <- cnt;
1101
      !arrayDest3.(s).(n) <-
1102
        if Hashtbl.mem htR role then Hashtbl.find htR role
1103
        else
1104
          let size = Hashtbl.length htR in
1105
          Hashtbl.add htR role size;
1106
          size
1107
  | C.HCATLEASTPROB (p,f1) ->
1108
      !arrayType.(s).(n) <- AtLeastProbF;
1109
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1110
      !arrayDestNum.(s).(n) <- p.C.nominator;
1111
      !arrayDestNum2.(s).(n) <- p.C.denominator
1112
  | C.HCLESSPROBFAIL (p,f1) ->
1113
      !arrayType.(s).(n) <- LessProbFailF;
1114
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1115
      !arrayDestNum.(s).(n) <- p.C.nominator;
1116
      !arrayDestNum2.(s).(n) <- p.C.denominator
1117
  | C.HCCONST str ->
1118
      !arrayType.(s).(n) <- ConstF; (* type of modality *)
1119
      (* Dest1 and Dest2 are the arguments, here: none *)
1120
      (* DestNum and DestNum2 are the numerators and denonimators of
1121
      fractions, here: none *)
1122
      !arrayDest3.(s).(n) <-
1123
        if Hashtbl.mem htR str then Hashtbl.find htR str
1124
        else
1125
          let size = Hashtbl.length htR in
1126
          Hashtbl.add htR str size;
1127
          size
1128
      (* Dest3 are the role names / identifiers for constant values *)
1129
      (* idea: hash identifier names *)
1130
  | C.HCCONSTN str ->
1131
      !arrayType.(s).(n) <- ConstnF; (* type of modality *)
1132
      (* Dest1 and Dest2 are the arguments, here: none *)
1133
      (* DestNum and DestNum2 are the numerators and denonimators of
1134
      fractions, here: none *)
1135
      !arrayDest3.(s).(n) <-
1136
        if Hashtbl.mem htR str then Hashtbl.find htR str
1137
        else
1138
          let size = Hashtbl.length htR in
1139
          Hashtbl.add htR str size;
1140
          size
1141
      (* Dest3 are the role names / identifiers for constant values *)
1142
      (* idea: hash identifier names *)
1143
  | C.HCID (f1) ->
1144
      !arrayType.(s).(n) <- IdF;
1145
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1
1146
  | C.HCNORM (f1, f2) ->
1147
      !arrayType.(s).(n) <- NormF;
1148
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
1149
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2
1150
  | C.HCNORMN (f1, f2) ->
1151
      !arrayType.(s).(n) <- NormnF;
1152
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
1153
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2
1154
  (* note that choice is self-dual *)
1155
  | C.HCCHC (f1, f2) ->
1156
      !arrayType.(s).(n) <- ChcF;
1157
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
1158
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2
1159
  | C.HCFUS (first, f1) ->
1160
      !arrayType.(s).(n) <- FusF;
1161
      let s1 = List.nth sortlst (if first then 0 else 1) in
1162
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s1) f1;
1163
      !arrayDest3.(s).(n) <- if first then 0 else 1
1164
  | C.HCMU (name, f1) ->
1165
     !arrayType.(s).(n) <- MuF;
1166
     let unfold = C.hc_replace hcF name f f1 in
1167
     !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold
1168
  | C.HCNU (name, f1) ->
1169
     !arrayType.(s).(n) <- NuF;
1170
     let unfold = C.hc_replace hcF name f f1 in
1171
     !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold
1172
  | C.HCVAR _ -> !arrayType.(s).(n) <- Other
1173

    
1174

    
1175
let initTablesAt hcF htF name sort =
1176
  let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
1177
  let nom = C.HcFHt.find htF.(sort) hcnom in
1178
  let addAt f n =
1179
    match f.HC.node with
1180
    | C.HCTRUE
1181
    | C.HCFALSE
1182
    | C.HCOR _
1183
    | C.HCAND _
1184
    | C.HCAT _ -> ()
1185
    | _ ->
1186
        let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
1187
        let atn = C.HcFHt.find htF.(0) at in
1188
        FHt.add !arrayAt.(sort).(n) nom atn
1189
  in
1190
  C.HcFHt.iter addAt htF.(sort)
1191

    
1192
let ppFormulae nomTbl tbox (s, f) =
1193
  let card = Array.length !sortTable in
1194
  if card <= 0 then
1195
    raise (C.CoAlgException "Number of sorts must be positive.")
1196
  else ();
1197
  let nnfAndSimplify f = C.simplify (C.nnf f) in
1198
  let  f1    = nnfAndSimplify f in
1199
  let nf1    = nnfAndSimplify (C.NOT f) in
1200
  let  tbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify f)) tbox in
1201
  let ntbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify (C.NOT f))) tbox in
1202

    
1203
  let hcF     =  C.HcFormula.create true in
1204
  let  hcf    = C.hc_formula hcF  f1 in
1205
  let nhcf    = C.hc_formula hcF nf1 in
1206
  let  hctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f))  tbox1 in
1207
  let nhctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f)) ntbox1 in
1208
  let hcfalse = C.hc_formula hcF C.FALSE in
1209
  let hctrue  = C.hc_formula hcF C.TRUE in
1210

    
1211
  let fset = Array.init card (fun _ -> C.HcFHt.create 128) in
1212
  let vset = Array.init card (fun _ -> C.HcFHt.create 128) in
1213
  let atset = C.HcFHt.create 64 in
1214
  let nomset = Hashtbl.create 16 in
1215
  for i = 0 to card-1 do
1216
    detClosure [] nomTbl hcF fset vset atset nomset i hcfalse;
1217
    detClosure [] nomTbl hcF fset vset atset nomset i hctrue;
1218
  done;
1219
  detClosure [] nomTbl hcF fset vset atset nomset s  hcf;
1220
  detClosure [] nomTbl hcF fset vset atset nomset s nhcf;
1221
  List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f)
1222
            hctbox;
1223
  List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f)
1224
            nhctbox;
1225
  Hashtbl.iter (fun n s -> C.HcFHt.iter (detClosureAt hcF atset n) fset.(s)) nomset;
1226

    
1227
  let htF = Array.init card (fun _ -> C.HcFHt.create 128) in
1228
  for i = 0 to card-1 do
1229
    C.HcFHt.add htF.(i) hcfalse 0;
1230
    C.HcFHt.add htF.(i) hctrue 1
1231
  done;
1232
  let addAts f () idx =
1233
    for i = 0 to card-1 do
1234
      C.HcFHt.add htF.(i) f idx
1235
    done;
1236
    idx + 1
1237
  in
1238
  let sizeAt = C.HcFHt.fold addAts atset 2 in
1239
  let addFml i f () idx =
1240
    if C.HcFHt.mem htF.(i) f then idx
1241
    else begin
1242
      C.HcFHt.add htF.(i) f idx;
1243
      idx+1
1244
    end
1245
  in
1246
  let size = ref 0 in
1247
  for i = 0 to card-1 do
1248
    let size2 = C.HcFHt.fold (addFml i) fset.(i) sizeAt in
1249
    if size2 > !size then size := size2 else ()
1250
  done;
1251

    
1252
  arrayFormula := Array.init card (fun _ -> Array.make !size C.TRUE);
1253
  arrayType := Array.init card (fun _ -> Array.make !size Other);
1254
  arrayDest1 := Array.init card (fun _ -> Array.make !size (-1));
1255
  arrayDest2 := Array.init card (fun _ -> Array.make !size (-1));
1256
  arrayDest3 := Array.init card (fun _ -> Array.make !size (-1));
1257
  arrayDeferral := Array.init card (fun _-> Array.make !size(-1));
1258
  arrayNeg := Array.init card (fun _ -> Array.make !size (-1));
1259
  arrayDestNum := Array.init card (fun _ -> Array.make !size (-1));
1260
  arrayDestNum2 := Array.init card (fun _ -> Array.make !size (-1));
1261
  arrayDestAg := Array.init card (fun _ -> Array.make !size (Array.make 0 (-1)));
1262
  let htR = Hashtbl.create 128 in
1263
  Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR vset s) ht) htF;
1264
  arrayAt := Array.init card (fun _ -> Array.init !size (fun _ -> FHt.create 8));
1265
  Hashtbl.iter (initTablesAt hcF htF) nomset;
1266

    
1267
  S.initMisc !size (C.HcFHt.find htF.(0) hcfalse) (C.HcFHt.find htF.(0) hctrue) (-1) (-1) (-1);
1268
  let initbs = bsetMake () in
1269
  bsetAdd initbs (C.HcFHt.find htF.(s) hcf);
1270
  let tboxTbl = Array.init card (fun _ -> bsetMake ()) in
1271
  List.iter (fun (s, f) -> bsetAdd tboxTbl.(s) (C.HcFHt.find htF.(s) f)) hctbox;
1272
  tboxTable := tboxTbl;
1273
  (tbox1, (s, f1), initbs)