Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgMisc.ml @ 50df1dc2

History | View | Annotate | Download (45.1 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 setEmptyCnstr () = GHtS.create 128
582
let setAddState set state =
583
  GHt.add set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state)) state
584
let setAddCore set core =
585
  GHt.add set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core)) core
586
let setAddCnstr set cset = GHtS.add set cset ()
587
let setMemState set state =
588
  GHt.mem set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
589
let setMemCore set core =
590
  GHt.mem set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
591
let setMemCnstr set cset = GHtS.mem set cset
592
let setRemoveState set state =
593
  GHt.remove set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
594
let setRemoveCore set core =
595
  GHt.remove set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
596
let setRemoveCnstr set cset = GHtS.remove set cset
597
let setIterState fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
598
let setIterCore fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
599
let setIterCnstr fkt set = GHtS.iter (fun cset () -> fkt cset) set
600
let setLengthState seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta
601
let setLengthCore seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta
602

    
603

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

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

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

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

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

    
637
let tboxTable = ref (Array.make 0 S.dummyBS)
638

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

    
656
let bsetAddTBox sort bs = S.unionBSNoChk bs !tboxTable.(sort)
657

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

    
671

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

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

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

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

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

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

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

    
730
let bsetToString sort bset : string =
731
    let toFormula (lf:localFormula) (lst: string list) : string list =
732
        let formula: C.formula = lfGetFormula sort lf in
733
        (C.string_of_formula formula) :: lst
734
    in
735
    let formulaList = bsetFold toFormula bset [] in
736
    "{ "^(String.concat ", " formulaList)^" }"
737

    
738
let csetToString sort cset = bsetToString sort cset
739

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

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

    
793
let stateToDot (state:state): string =
794
  let color = match state.statusS with
795
    | Sat -> "green"
796
    | Unsat -> "red"
797
    | Open -> "yellow"
798
    | Expandable -> "white"
799
  in
800
  let ownidx = (string_of_int state.idx) in
801
  let parents =
802
    List.map (fun (co:core) ->
803
              "Node"^string_of_int co.idx^" -> Node"^ownidx^";")
804
             state.parentsS
805
  in
806
  "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
807
  ^ ",label=\"State "  ^ ownidx
808
  ^ "\\n" ^ (Str.global_replace (Str.regexp ", ") "\\n"
809
                                (bsetToString state.sortS state.bsS))
810
  ^ "\"];\n"
811
  ^ (String.concat "\n" parents)
812

    
813

    
814
let coreToDot (core:core): string =
815
  let color = match core.statusC with
816
    | Sat -> "green"
817
    | Unsat -> "red"
818
    | Open -> "yellow"
819
    | Expandable -> "white"
820
  in
821
  let ownidx = (string_of_int core.idx) in
822
  let parents =
823
    List.map (fun (st,_:state*int) ->
824
              "Node"^string_of_int st.idx^" -> Node"^ownidx^";")
825
             core.parentsC
826
  in
827
  "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
828
  ^ ",label=\"Core "  ^ ownidx
829
  ^ "\\n" ^ (Str.global_replace (Str.regexp ", ") "\\n"
830
                                (bsetToString core.sortC core.bsC))
831
  ^ "\"];\n"
832
  ^ (String.concat "\n" parents)
833

    
834

    
835
let queuePrettyStatus () =
836
  let printList (sl : int list) : string =
837
    String.concat ", " (List.map string_of_int sl)
838
  in
839
  (* TODO: are atFormulas always look-up-able for sort 0? *)
840
  (Printf.sprintf "%d Constraints: " (List.length !queueCnstrs))
841
  ^(String.concat ", " (List.map (csetToString 0) !queueCnstrs))
842
  ^(Printf.sprintf "\n%d States: " (List.length !queueStates))
843
  ^(printList (List.map (fun (st:state) -> st.idx) !queueStates))
844
  ^(Printf.sprintf "\n%d Cores1: " (List.length !queueCores1))
845
  ^(printList (List.map (fun (co:core) -> co.idx) !queueCores1))
846
  ^(Printf.sprintf "\n%d Cores2: " (List.length !queueCores2))
847
  ^(printList (List.map (fun (co:core) -> co.idx) !queueCores2))
848
  ^"\n"
849

    
850

    
851

    
852

    
853
let atFormulaGetSubformula f = !arrayDest1.(0).(f)
854
let atFormulaGetNominal f =
855
  let s = !arrayDest3.(0).(f) in
856
  let n = !arrayDest2.(0).(f) in
857
  (s, n)
858

    
859
let lfToAt _ lf = lf
860

    
861
(* Calculate all possible formulae. This includes all subformulae and
862
   in the case of μ-Calculus the Fischer-Ladner closure.
863

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

    
970
    | C.HCCHC (f1, f2) ->
971
        if func <> Choice || List.length sortlst <> 2 then
972
          raise (C.CoAlgException "Choice formula is used in wrong sort.")
973
        else ();
974
        detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 0) f1;
975
        detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 1) f2
976
    | C.HCFUS (first, f1) ->
977
        if func <> Fusion || List.length sortlst <> 2 then
978
          raise (C.CoAlgException "Fusion formula is used in wrong sort.")
979
        else ();
980
        let s1 = List.nth sortlst (if first then 0 else 1) in
981
        detClosure_ nomTbl hcF fset vset atset nomset s1 f1
982
    (*
983
       FL(μ X . φ) = {μ X . φ} ∪ FL(φ[X|->μ X . φ])
984
     *)
985
    | C.HCMU (name, f1) ->
986
       let () = C.HcFHt.replace vset.(s) f name in
987
       let unfold = C.hc_replace hcF name f f1 in
988
       let appendvars = List.append newvars [name] in
989
       detClosure appendvars nomTbl hcF fset vset atset nomset s unfold
990
    | C.HCNU (name, f1) ->
991
       let unfold = C.hc_replace hcF name f f1 in
992
       detClosure_ nomTbl hcF fset vset atset nomset s unfold
993

    
994

    
995
let detClosureAt hcF atset name f () =
996
  match f.HC.node with
997
  | C.HCTRUE
998
  | C.HCFALSE
999
  | C.HCOR _
1000
  | C.HCAND _
1001
  | C.HCAT _ -> ()
1002
  | _ ->
1003
      let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
1004
      C.HcFHt.replace atset at ()
1005

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

    
1153

    
1154
let initTablesAt hcF htF name sort =
1155
  let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
1156
  let nom = C.HcFHt.find htF.(sort) hcnom in
1157
  let addAt f n =
1158
    match f.HC.node with
1159
    | C.HCTRUE
1160
    | C.HCFALSE
1161
    | C.HCOR _
1162
    | C.HCAND _
1163
    | C.HCAT _ -> ()
1164
    | _ ->
1165
        let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
1166
        let atn = C.HcFHt.find htF.(0) at in
1167
        FHt.add !arrayAt.(sort).(n) nom atn
1168
  in
1169
  C.HcFHt.iter addAt htF.(sort)
1170

    
1171
let ppFormulae nomTbl tbox (s, f) =
1172
  let card = Array.length !sortTable in
1173
  if card <= 0 then
1174
    raise (C.CoAlgException "Number of sorts must be positive.")
1175
  else ();
1176
  let nnfAndSimplify f = C.simplify (C.nnf f) in
1177
  let  f1    = nnfAndSimplify f in
1178
  let nf1    = nnfAndSimplify (C.NOT f) in
1179
  let  tbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify f)) tbox in
1180
  let ntbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify (C.NOT f))) tbox in
1181

    
1182
  let hcF     =  C.HcFormula.create true in
1183
  let  hcf    = C.hc_formula hcF  f1 in
1184
  let nhcf    = C.hc_formula hcF nf1 in
1185
  let  hctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f))  tbox1 in
1186
  let nhctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f)) ntbox1 in
1187
  let hcfalse = C.hc_formula hcF C.FALSE in
1188
  let hctrue  = C.hc_formula hcF C.TRUE in
1189

    
1190
  let fset = Array.init card (fun _ -> C.HcFHt.create 128) in
1191
  let vset = Array.init card (fun _ -> C.HcFHt.create 128) in
1192
  let atset = C.HcFHt.create 64 in
1193
  let nomset = Hashtbl.create 16 in
1194
  for i = 0 to card-1 do
1195
    detClosure [] nomTbl hcF fset vset atset nomset i hcfalse;
1196
    detClosure [] nomTbl hcF fset vset atset nomset i hctrue;
1197
  done;
1198
  detClosure [] nomTbl hcF fset vset atset nomset s  hcf;
1199
  detClosure [] nomTbl hcF fset vset atset nomset s nhcf;
1200
  List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f)
1201
            hctbox;
1202
  List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f)
1203
            nhctbox;
1204
  Hashtbl.iter (fun n s -> C.HcFHt.iter (detClosureAt hcF atset n) fset.(s)) nomset;
1205

    
1206
  let htF = Array.init card (fun _ -> C.HcFHt.create 128) in
1207
  for i = 0 to card-1 do
1208
    C.HcFHt.add htF.(i) hcfalse 0;
1209
    C.HcFHt.add htF.(i) hctrue 1
1210
  done;
1211
  let addAts f () idx =
1212
    for i = 0 to card-1 do
1213
      C.HcFHt.add htF.(i) f idx
1214
    done;
1215
    idx + 1
1216
  in
1217
  let sizeAt = C.HcFHt.fold addAts atset 2 in
1218
  let addFml i f () idx =
1219
    if C.HcFHt.mem htF.(i) f then idx
1220
    else begin
1221
      C.HcFHt.add htF.(i) f idx;
1222
      idx+1
1223
    end
1224
  in
1225
  let size = ref 0 in
1226
  for i = 0 to card-1 do
1227
    let size2 = C.HcFHt.fold (addFml i) fset.(i) sizeAt in
1228
    if size2 > !size then size := size2 else ()
1229
  done;
1230

    
1231
  arrayFormula := Array.init card (fun _ -> Array.make !size C.TRUE);
1232
  arrayType := Array.init card (fun _ -> Array.make !size Other);
1233
  arrayDest1 := Array.init card (fun _ -> Array.make !size (-1));
1234
  arrayDest2 := Array.init card (fun _ -> Array.make !size (-1));
1235
  arrayDest3 := Array.init card (fun _ -> Array.make !size (-1));
1236
  arrayDeferral := Array.init card (fun _-> Array.make !size(-1));
1237
  arrayNeg := Array.init card (fun _ -> Array.make !size (-1));
1238
  arrayDestNum := Array.init card (fun _ -> Array.make !size (-1));
1239
  arrayDestNum2 := Array.init card (fun _ -> Array.make !size (-1));
1240
  arrayDestAg := Array.init card (fun _ -> Array.make !size (Array.make 0 (-1)));
1241
  let htR = Hashtbl.create 128 in
1242
  Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR vset s) ht) htF;
1243
  arrayAt := Array.init card (fun _ -> Array.init !size (fun _ -> FHt.create 8));
1244
  Hashtbl.iter (initTablesAt hcF htF) nomset;
1245

    
1246
  S.initMisc !size (C.HcFHt.find htF.(0) hcfalse) (C.HcFHt.find htF.(0) hctrue) (-1) (-1) (-1);
1247
  let initbs = bsetMake () in
1248
  bsetAdd initbs (C.HcFHt.find htF.(s) hcf);
1249
  let tboxTbl = Array.init card (fun _ -> bsetMake ()) in
1250
  List.iter (fun (s, f) -> bsetAdd tboxTbl.(s) (C.HcFHt.find htF.(s) f)) hctbox;
1251
  tboxTable := tboxTbl;
1252
  (tbox1, (s, f1), initbs)