Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgMisc.ml @ de84f40d

History | View | Annotate | Download (45.8 KB)

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

    
5

    
6
module S = MiscSolver
7
module L = List
8
module C = CoAlgFormula
9
module HC = HashConsing
10

    
11

    
12
(** An instantiation of a set (of the standard library) for bitsets.
13
 *)
14
module BsSet = Set.Make(
15
  struct
16
    type t = S.bitset
17
    let (compare : t -> t -> int) = S.compareBS
18
  end
19
 )
20

    
21
(** An instantiation of a hash table (of the standard library) for bitsets.
22
 *)
23
module GHt = Hashtbl.Make(
24
  struct
25
    type t = S.bitset * 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 escapeHtml (input : string) : string =
731
  List.fold_right (fun (x, y) (str : string) -> Str.global_replace (Str.regexp x) y str)
732
    [("<", "&lt;") ; (">", "&gt;") ; ("&", "&amp;")]
733
    input
734

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

    
743
let csetToString sort cset = bsetToString sort cset
744

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

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

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

    
824

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

    
851

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

    
867

    
868

    
869

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

    
876
let lfToAt _ lf = lf
877

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

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

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

    
1011

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

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

    
1170

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

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

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

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

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

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

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