Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgMisc.ml @ 40a714df

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

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

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

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

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

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

    
129

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

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

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

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

    
184
type localFormula = int
185
type bset = S.bitset
186

    
187
type atFormula = int
188
type cset = S.bitset
189
type csetSet = BsSet.t
190

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

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

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

    
227
and setState = state GHt.t array
228

    
229
and setCore = core GHt.t array
230

    
231
and setCnstr = unit GHtS.t
232

    
233

    
234
(*****************************************************************************)
235
(*                Types that are hard coded into the algorithm               *)
236
(*****************************************************************************)
237

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

    
241
and stateExpander = rule lazylist
242

    
243
and sort = C.sort
244

    
245
and nodeStatus =
246
  | Expandable
247
  | Open
248
  | Sat
249
  | Unsat
250

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

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

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

    
263
and 'a lazyliststep =
264
  | MultipleElements of 'a list
265
  | SingleElement    of 'a
266
  | NoMoreElements
267

    
268
and 'a lazylist = unit -> 'a lazyliststep
269

    
270
and ruleEnumeration = rule lazyliststep
271

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

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

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

    
295
type nominal = sort * localFormula
296

    
297
type node =
298
  | State of state
299
  | Core of core
300

    
301
type constrnt =
302
  | UnsatC
303
  | SatC
304
  | OpenC of node list
305
  | UnexpandedC of node list
306

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

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

    
318
type sortTable = (functors * int list) array
319

    
320
exception CoAlg_finished of bool
321

    
322

    
323
let sortTable = ref (Array.make 0 (MultiModalK, [1]))
324

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

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

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

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

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

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

    
359
let queueStates = ref ([] : state list)
360
let queueCores1 = ref ([] : core list)
361
let queueCores2 = ref ([] : core list)
362
let queueCnstrs = ref ([] : cset list)
363
let doPropagation = ref false
364
let doPropagationCounter = ref 0
365

    
366
let queueInit () =
367
  queueStates := [];
368
  queueCores1 := [];
369
  queueCores2 := [];
370
  queueCnstrs := [];
371
  doPropagation := false
372

    
373
let queueIsEmpty () =
374
  !queueStates = [] && !queueCores1 = [] && !queueCores2 = [] && !queueCnstrs = []
375

    
376
let queueInsertState state = queueStates := state::!queueStates
377

    
378
(* original version: breadth-first *)
379
let queueInsertCore core = queueCores2 := core::!queueCores2
380

    
381
(* experiment: depth first
382
let queueInsertCore core = queueCores1 := core::!queueCores1
383
*)
384

    
385
let queueInsertCnstr cset = queueCnstrs := cset::!queueCnstrs
386

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

    
408
let doNominalPropagation () = !doPropagation
409

    
410
let setPropagationCounter count =
411
  doPropagationCounter := count
412

    
413
let doSatPropagation () =
414
  if !doPropagationCounter == 0
415
  then true
416
  else begin
417
      doPropagationCounter := !doPropagationCounter - 1;
418
      false
419
    end
420
  (* let res = !doPropagation in *)
421
  (* doPropagation := false; *)
422
  (* res *)
423

    
424
(*****************************************************************************)
425
(*        "Module type" and a specific implementation of the graph           *)
426
(*****************************************************************************)
427

    
428
let graphStates = ref (Array.make 0 (GHt.create 0 : state GHt.t))
429
let graphCores = ref (Array.make 0 (GHt.create 0 : core GHt.t))
430
let graphCnstrs = ref (GHtS.create 0 : constrnt GHtS.t)
431
let graphRoot = ref (None : core option)
432

    
433
let graphInit () =
434
  let size = Array.length !sortTable in
435
  graphStates := Array.init size (fun _ -> GHt.create 128);
436
  graphCores := Array.init size (fun _ -> GHt.create 128);
437
  graphCnstrs := GHtS.create 128;
438
  graphRoot := None
439

    
440
let graphIterStates fkt =
441
  Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphStates
442

    
443
let graphIterCores fkt =
444
  Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphCores
445

    
446
let graphIterCnstrs fkt = GHtS.iter fkt !graphCnstrs
447

    
448
let graphClearCnstr () =
449
  let newGraph = GHtS.create (GHtS.length !graphCnstrs) in
450
  let copyCnstr cset cnstr =
451
    match cnstr with
452
    | UnsatC
453
    | SatC -> GHtS.add newGraph cset cnstr
454
    | OpenC _ -> GHtS.add newGraph cset (OpenC [])
455
    | UnexpandedC _ -> GHtS.add newGraph cset (UnexpandedC [])
456
  in
457
  GHtS.iter copyCnstr !graphCnstrs;
458
  graphCnstrs := newGraph
459

    
460
let graphFindState sort bs =
461
  try
462
    Some (GHt.find !graphStates.(sort) bs)
463
  with Not_found -> None
464

    
465
let graphFindCore sort bs =
466
  try
467
    Some (GHt.find !graphCores.(sort) bs)
468
  with Not_found -> None
469

    
470
let graphFindCnstr cset =
471
  try
472
    Some (GHtS.find !graphCnstrs cset)
473
  with Not_found -> None
474

    
475
let graphInsertState sort bs state =
476
  assert (not (GHt.mem !graphStates.(sort) bs));
477
  GHt.add !graphStates.(sort) bs state
478

    
479
let graphInsertCore sort bs core =
480
  assert (not (GHt.mem !graphCores.(sort) bs));
481
  GHt.add !graphCores.(sort) bs core
482

    
483
let graphInsertCnstr cset cnstr =
484
  assert (not (GHtS.mem !graphCnstrs cset));
485
  GHtS.add !graphCnstrs cset cnstr
486

    
487
let graphReplaceCnstr cset cnstr =
488
  GHtS.replace !graphCnstrs cset cnstr
489

    
490
let graphSizeState () =
491
  Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphStates
492
let graphSizeCore () =
493
  Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphCores
494
let graphSizeCnstr () = GHtS.length !graphCnstrs
495

    
496
let graphAddRoot core =
497
  if !graphRoot = None then graphRoot := Some core
498
  else raise (C.CoAlgException "Root of graph is already set.")
499

    
500
let graphGetRoot () =
501
  match !graphRoot with
502
  | None -> raise (C.CoAlgException "Root of graph is not set.")
503
  | Some core -> core
504

    
505

    
506
(*****************************************************************************)
507
(*     "Module type" and a specific implementation of sets of constraints    *)
508
(*****************************************************************************)
509

    
510
let cssEmpty = BsSet.empty
511
let cssExists fkt css = BsSet.exists fkt css
512
let cssForall fkt css = BsSet.for_all fkt css
513
let cssUnion css1 css2 = BsSet.union css1 css2
514
let cssAdd cset css = BsSet.add cset css
515
let cssFold fkt css init = BsSet.fold fkt css init
516
let cssSingleton cset = BsSet.singleton cset
517
let cssEqual css1 css2 = BsSet.equal css1 css2
518
let cssIter (action: cset -> unit) css =
519
    BsSet.iter action css
520

    
521

    
522
(*****************************************************************************)
523
(*      "Module type" and a specific implementation of state nodes           *)
524
(*****************************************************************************)
525
let nodeCounter = ref 0
526
let nextNodeIdx () : int =
527
    let oldVal = !nodeCounter in
528
    nodeCounter := oldVal + 1;
529
    oldVal
530

    
531
let stateMake sort bs defer exp =
532
  { sortS = sort; bsS = bs; deferralS = defer; statusS = Expandable; parentsS = []; childrenS = [];
533
    constraintsS = cssEmpty; expandFkt = exp;
534
    idx = nextNodeIdx()
535
  }
536
let stateGetSort state = state.sortS
537
let stateGetBs state = state.bsS
538
let stateSetBs state bs = state.bsS <- bs
539
let stateGetDeferral state = state.deferralS
540
let stateSetDeferral state bs = state.deferralS <- bs
541
let stateGetStatus state = state.statusS
542
let stateSetStatus state status = state.statusS <- status
543
let stateGetParents state = state.parentsS
544
let stateAddParent state parent = state.parentsS <- parent::state.parentsS
545
let stateGetRule state idx = List.nth state.childrenS (List.length state.childrenS - idx)
546
let stateGetRules state = state.childrenS
547
let stateAddRule state dep children =
548
  state.childrenS <- (dep, children)::state.childrenS;
549
  List.length state.childrenS
550
let stateGetConstraints state = state.constraintsS
551
let stateSetConstraints state csets = state.constraintsS <- csets
552
let stateNextRule state = state.expandFkt ()
553
let stateGetIdx (state:state) = state.idx
554

    
555

    
556
(*****************************************************************************)
557
(*      "Module type" and a specific implementation of core nodes            *)
558
(*****************************************************************************)
559

    
560
let coreMake sort bs defer solver fht =
561
  { sortC = sort; bsC = bs; deferralC = defer; statusC = Expandable; parentsC = []; childrenC = [];
562
    constraintsC = cssEmpty; solver = solver; fht = fht; constraintParents = [];
563
    idx = nextNodeIdx()
564
  }
565
let coreGetSort core = core.sortC
566
let coreGetBs core = core.bsC
567
let coreSetBs core bs = core.bsC <- bs
568
let coreGetDeferral core = core.deferralC
569
let coreSetDeferral core bs = core.deferralC <- bs
570
let coreGetStatus core = core.statusC
571
let coreSetStatus core status = core.statusC <- status
572
let coreGetParents core = core.parentsC
573
let coreAddParent core parent idx = core.parentsC <- (parent, idx)::core.parentsC
574
let coreGetChildren core = core.childrenC
575
let coreAddChild core child = core.childrenC <- child::core.childrenC
576
let coreGetConstraints core = core.constraintsC
577
let coreSetConstraints core csets = core.constraintsC <- csets
578
let coreGetSolver core = core.solver
579
let coreDeallocateSolver core = core.solver <- None; FHt.reset core.fht
580
let coreGetFht core = core.fht
581
let coreGetIdx (core:core) = core.idx
582
let coreGetConstraintParents core = core.constraintParents
583
let coreAddConstraintParent core cset =
584
  core.constraintParents <- cset::core.constraintParents
585

    
586

    
587
(*****************************************************************************)
588
(*      "Module type" and a specific implementation of sets of               *)
589
(*      states, cores, and constraints for the sat propagation               *)
590
(*****************************************************************************)
591

    
592
let setEmptyState () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
593
let setEmptyCore () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
594
let setCopyState set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx))
595
let setCopyCore set = Array.init (Array.length !sortTable) (fun idx -> GHt.copy set.(idx))
596
let setEmptyCnstr () = GHtS.create 128
597
let setAddState set state =
598
  GHt.add set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state)) state
599
let setAddCore set core =
600
  GHt.add set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core)) core
601
let setAddCnstr set cset = GHtS.add set cset ()
602
let setMemState set state =
603
  GHt.mem set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
604
let setMemCore set core =
605
  GHt.mem set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
606
let setMemCnstr set cset = GHtS.mem set cset
607
let setRemoveState set state =
608
  GHt.remove set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
609
let setRemoveCore set core =
610
  GHt.remove set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
611
let setRemoveCnstr set cset = GHtS.remove set cset
612
let setIterState fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
613
let setIterCore fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
614
let setIterCnstr fkt set = GHtS.iter (fun cset () -> fkt cset) set
615
let setLengthState seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta
616
let setLengthCore seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta
617

    
618

    
619
(*****************************************************************************)
620
(*        "Module type" and a specific implementation of the mapping         *)
621
(*        between (local) formulae and literals of the sat solver,           *)
622
(*        and of a mapping of nominals to sets of formulae                   *)
623
(*****************************************************************************)
624

    
625
let lhtInit () = LHt.create 16
626
let lhtAdd lht lit f = LHt.add lht lit f
627
let lhtFind lht lit =
628
  try
629
    Some (LHt.find lht lit)
630
  with Not_found -> None
631

    
632
let fhtInit () = FHt.create 16
633
let fhtAdd fht f lit = FHt.add fht f lit
634
let fhtFind fht f =
635
  try
636
    Some (FHt.find fht f)
637
  with Not_found -> None
638

    
639
let nhtInit () = NHt.create 8
640
let nhtAdd nht nom bs = NHt.add nht nom bs
641
let nhtFind nht nom =
642
  try
643
    Some (NHt.find nht nom)
644
  with Not_found -> None
645
let nhtFold fkt nht init = NHt.fold fkt nht init
646

    
647
(*****************************************************************************)
648
(*         "Module type" and a specific implementation of sets of            *)
649
(*         local formulae and @-formulae                                     *)
650
(*****************************************************************************)
651

    
652
let tboxTable = ref (Array.make 0 S.dummyBS)
653

    
654
let bsetMake () = S.makeBS ()
655
let bsetAdd bs lf = S.addBSNoChk bs lf
656
let bsetMem bs lf = S.memBS bs lf
657
let bsetRem bs lf = S.remBS bs lf
658
let bsetCompare bs1 bs2 = S.compareBS bs1 bs2
659
let bsetMakeRealEmpty () =
660
    let res = bsetMake () in
661
    bsetRem res !S.bstrue; (* remove bstrue which is initially in an empty bset *)
662
    res
663
let bsetCopy bs = S.copyBS bs
664
let bsetFold fkt bs init = S.foldBS fkt bs init
665
let bsetIter fkt bset = S.iterBS fkt bset
666
let bsetFilter (a: bset) (f: localFormula -> bool) : bset =
667
    let res = bsetMakeRealEmpty () in
668
    bsetIter (fun form -> if (f form) then bsetAdd res form else ()) a;
669
    res
670

    
671
let bsetAddTBox sort bs = S.unionBSNoChk bs !tboxTable.(sort)
672

    
673
let csetCompare cs1 cs2 = S.compareBS cs1 cs2
674
let csetMake () = S.makeBS ()
675
let csetAdd cs lf = S.addBSNoChk cs lf
676
let csetCopy cs = S.copyBS cs
677
let csetUnion cs1 cs2 = S.unionBSNoChk cs1 cs2
678
let csetHasDot cs = S.memBS cs !S.bsfalse
679
let csetAddDot cs = S.addBSNoChk cs !S.bsfalse
680
let csetRemDot cs = S.remBS cs !S.bsfalse
681
let csetAddTBox sort cs = S.unionBSNoChk cs !tboxTable.(sort)
682
let csetIter cs fkt =
683
  let fkt2 f = if not (f = !S.bstrue || f = !S.bsfalse) then fkt f else () in
684
  S.iterBS fkt2 cs
685

    
686

    
687
(*****************************************************************************)
688
(*            "Module type" and a specific implementation of                 *)
689
(*            local formulae and @-formulae                                  *)
690
(*****************************************************************************)
691

    
692
(** This table maps integers (representing formulae) to their corresponding formulae.
693
 *)
694
let arrayFormula = ref (Array.make 0 (Array.make 0 C.TRUE))
695

    
696
(** This table maps integers (representing formulae) to their corresponding type.
697
 *)
698
let arrayType = ref (Array.make 0 (Array.make 0 Other))
699

    
700
(** This lookup table maps formulae (represented as integers)
701
    to their negation (in negation normal form).
702
 *)
703
let arrayNeg = ref (Array.make 0 (Array.make 0 (-1)))
704

    
705
(** These lookup tables map formulae (represented as integers)
706
    to their decompositions (represented as integers).
707
    This is done according to the rules of the tableau procedure
708
    and depends on the type of the formulae.
709
 *)
710
 (*
711
    for PML: arrayDest1 = the subformula
712
             arrayNum  = the nominator of the probability
713
             arrayNum2 = the denominator of the probability
714
 *)
715
let arrayDest1 = ref (Array.make 0 (Array.make 0 (-1)))  (* first subformula *)
716
let arrayDest2 = ref (Array.make 0 (Array.make 0 (-1)))  (* second subformula *)
717
let arrayDest3 = ref (Array.make 0 (Array.make 0 (-1)))  (* a role *)
718
let arrayDeferral = ref (Array.make 0 (Array.make 0 (-1)))  (* deferral at point *)
719
let arrayDestNum = ref (Array.make 0 (Array.make 0 (-1)))  (* an integer *)
720
let arrayDestNum2 = ref (Array.make 0 (Array.make 0 (-1)))  (* another integer *)
721
let arrayDestAg = ref (Array.make 0 (Array.make 0 [|0|])) (* arrays of agents *)
722

    
723
(** This lookup table maps formulae (represented as integers)
724
    to their @-wrapper.
725
 *)
726
let arrayAt = ref (Array.make 0 (Array.make 0 (FHt.create 64)))
727

    
728
let lfGetType sort f = !arrayType.(sort).(f)
729
let lfGetDest1 sort f = !arrayDest1.(sort).(f)
730
let lfGetDest2 sort f = !arrayDest2.(sort).(f)
731
let lfGetDest3 sort f = !arrayDest3.(sort).(f)
732
let lfGetDeferral sort f = !arrayDeferral.(sort).(f)
733
let lfGetDestNum sort f = !arrayDestNum.(sort).(f)
734
let lfGetDestNum2 sort f = !arrayDestNum2.(sort).(f)
735
let lfGetDestAg sort f = !arrayDestAg.(sort).(f)
736
let lfGetNeg sort f =
737
  let nf = !arrayNeg.(sort).(f) in
738
  if nf >= 0 then Some nf else None
739
let lfGetAt (sort, nom) f =
740
  FHt.find !arrayAt.(sort).(f) nom
741
let lfToInt lf = lf
742
let lfFromInt num = num
743
let lfGetFormula sort f = !arrayFormula.(sort).(f)
744

    
745
let escapeHtml (input : string) : string =
746
  List.fold_right (fun (x, y) (str : string) -> Str.global_replace (Str.regexp x) y str)
747
    [("<", "&lt;") ; (">", "&gt;") ; ("&", "&amp;")]
748
    input
749

    
750
let bsetToString sort bset : string =
751
    let toFormula (lf:localFormula) (lst: string list) : string list =
752
        let formula: C.formula = lfGetFormula sort lf in
753
        (C.string_of_formula formula) :: lst
754
    in
755
    let formulaList = bsetFold toFormula bset [] in
756
    "{ "^(String.concat ", " formulaList)^" }"
757

    
758
let csetToString sort cset = bsetToString sort cset
759

    
760
let coreToString (core:core): string =
761
    let helper cset lst : string list =
762
        (csetToString core.sortC cset):: lst
763
    in
764
    let constraints = cssFold helper core.constraintsC [] in
765
    let children =
766
        List.map (fun (st:state) -> string_of_int st.idx) core.childrenC
767
    in
768
    let parents =
769
        List.map (fun (st,_:state*int) -> string_of_int st.idx) core.parentsC
770
    in
771
    "Core "^(string_of_int core.idx)^" {\n"^
772
    "  Status: " ^ (nodeStatusToString core.statusC) ^ "\n"^
773
    "  " ^ bsetToString core.sortC core.bsC ^ "\n" ^
774
    "  Deferrals: \n" ^
775
    "    " ^ bsetToString core.sortC core.deferralC ^ "\n" ^
776
    "  Constraints: { "^(String.concat
777
                         "\n                 " constraints)^" }\n"^
778
    "  Children: { "^(String.concat
779
                         ", " children)^" }\n"^
780
    "  Parents: { "^(String.concat ", " parents)^" }\n"^
781
    "}"
782

    
783
let stateToString (state:state): string =
784
    let helper cset lst : string list =
785
        (csetToString state.sortS cset):: lst
786
    in
787
    let constraints = cssFold helper state.constraintsS [] in
788
    let core2idx core = core.idx in
789
    let fst (a,b) = a in
790
    let conclusionList =
791
        List.map (fun (_,lst) ->
792
                  List.map (fun (core:core) -> string_of_int core.idx) lst
793
        ) state.childrenS
794
    in
795
    let conclusionList =
796
        List.map (fun x -> "{"^String.concat ", " x^"}") conclusionList
797
    in
798
    let parents =
799
        List.map (fun (co:core) -> string_of_int co.idx) state.parentsS
800
    in
801
    "State "^(string_of_int state.idx)^" {\n"^
802
    "  Status: " ^ (nodeStatusToString state.statusS) ^ "\n"^
803
    "  " ^ bsetToString state.sortS state.bsS ^ "\n" ^
804
    "  Deferrals: \n" ^
805
    "    " ^ bsetToString state.sortS state.deferralS ^ "\n" ^
806
    "  Constraints: { "^(String.concat
807
                         "\n                 " constraints)^" }\n"^
808
    "  Children: { "^(String.concat
809
                         "\n              " conclusionList)^" }\n"^
810
    "  Parents: { "^(String.concat ", " parents)^" }\n"^
811
    "}"
812

    
813
let stateToDot (state:state): string =
814
  let color = match state.statusS with
815
    | Sat -> "green"
816
    | Unsat -> "red"
817
    | Open -> "yellow"
818
    | Expandable -> "white"
819
  in
820
  let toFormula (lf:localFormula) (lst: string list) : string list =
821
    let formula: C.formula = lfGetFormula state.sortS lf in
822
    if (bsetMem state.deferralS lf)
823
    then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst
824
    else (escapeHtml (C.string_of_formula formula)) :: lst
825
  in
826
  let formulaList = bsetFold toFormula state.bsS [] in
827
  let ownidx = (string_of_int state.idx) in
828
  let parents =
829
    List.map (fun (co:core) ->
830
              "Node"^string_of_int co.idx^" -> Node"^ownidx^";")
831
             state.parentsS
832
  in
833
  "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
834
  ^ ",label=<State "  ^ ownidx
835
  ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
836
  ^ ">];\n"
837
  ^ (String.concat "\n" parents)
838

    
839

    
840
let coreToDot (core:core): string =
841
  let color = match core.statusC with
842
    | Sat -> "green"
843
    | Unsat -> "red"
844
    | Open -> "yellow"
845
    | Expandable -> "white"
846
  in
847
  let toFormula (lf:localFormula) (lst: string list) : string list =
848
    let formula: C.formula = lfGetFormula core.sortC lf in
849
    if (bsetMem core.deferralC lf)
850
    then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst
851
    else (escapeHtml (C.string_of_formula formula)) :: lst
852
  in
853
  let formulaList = bsetFold toFormula core.bsC [] in
854
  let ownidx = (string_of_int core.idx) in
855
  let parents =
856
    List.map (fun (st,_:state*int) ->
857
              "Node"^string_of_int st.idx^" -> Node"^ownidx^";")
858
             core.parentsC
859
  in
860
  "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
861
  ^ ",label=<Core "  ^ ownidx
862
  ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
863
  ^ ">];\n"
864
  ^ (String.concat "\n" parents)
865

    
866

    
867
let queuePrettyStatus () =
868
  let printList (sl : int list) : string =
869
    String.concat ", " (List.map string_of_int sl)
870
  in
871
  (* TODO: are atFormulas always look-up-able for sort 0? *)
872
  (Printf.sprintf "%d Constraints: " (List.length !queueCnstrs))
873
  ^(String.concat ", " (List.map (csetToString 0) !queueCnstrs))
874
  ^(Printf.sprintf "\n%d States: " (List.length !queueStates))
875
  ^(printList (List.map (fun (st:state) -> st.idx) !queueStates))
876
  ^(Printf.sprintf "\n%d Cores1: " (List.length !queueCores1))
877
  ^(printList (List.map (fun (co:core) -> co.idx) !queueCores1))
878
  ^(Printf.sprintf "\n%d Cores2: " (List.length !queueCores2))
879
  ^(printList (List.map (fun (co:core) -> co.idx) !queueCores2))
880
  ^"\n"
881

    
882

    
883

    
884

    
885
let atFormulaGetSubformula f = !arrayDest1.(0).(f)
886
let atFormulaGetNominal f =
887
  let s = !arrayDest3.(0).(f) in
888
  let n = !arrayDest2.(0).(f) in
889
  (s, n)
890

    
891
let lfToAt _ lf = lf
892

    
893
(* Calculate all possible formulae. This includes all subformulae and
894
   in the case of μ-Calculus the Fischer-Ladner closure.
895

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

    
1004
    | C.HCCHC (f1, f2) ->
1005
        if func <> Choice || List.length sortlst <> 2 then
1006
          raise (C.CoAlgException "Choice formula is used in wrong sort.")
1007
        else ();
1008
        detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 0) f1;
1009
        detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 1) f2
1010
    | C.HCFUS (first, f1) ->
1011
        if func <> Fusion || List.length sortlst <> 2 then
1012
          raise (C.CoAlgException "Fusion formula is used in wrong sort.")
1013
        else ();
1014
        let s1 = List.nth sortlst (if first then 0 else 1) in
1015
        detClosure_ nomTbl hcF fset vset atset nomset s1 f1
1016
    (*
1017
       FL(μ X . φ) = {μ X . φ} ∪ FL(φ[X|->μ X . φ])
1018
     *)
1019
    | C.HCMU (name, f1) ->
1020
       let () = C.HcFHt.replace vset.(s) f name in
1021
       let unfold = C.hc_replace hcF name f f1 in
1022
       let appendvars = List.append newvars [name] in
1023
       detClosure appendvars nomTbl hcF fset vset atset nomset s unfold
1024
    | C.HCNU (name, f1) ->
1025
       let unfold = C.hc_replace hcF name f f1 in
1026
       detClosure_ nomTbl hcF fset vset atset nomset s unfold
1027

    
1028

    
1029
let detClosureAt hcF atset name f () =
1030
  match f.HC.node with
1031
  | C.HCTRUE
1032
  | C.HCFALSE
1033
  | C.HCOR _
1034
  | C.HCAND _
1035
  | C.HCAT _ -> ()
1036
  | _ ->
1037
      let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
1038
      C.HcFHt.replace atset at ()
1039

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

    
1187

    
1188
let initTablesAt hcF htF name sort =
1189
  let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
1190
  let nom = C.HcFHt.find htF.(sort) hcnom in
1191
  let addAt f n =
1192
    match f.HC.node with
1193
    | C.HCTRUE
1194
    | C.HCFALSE
1195
    | C.HCOR _
1196
    | C.HCAND _
1197
    | C.HCAT _ -> ()
1198
    | _ ->
1199
        let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
1200
        let atn = C.HcFHt.find htF.(0) at in
1201
        FHt.add !arrayAt.(sort).(n) nom atn
1202
  in
1203
  C.HcFHt.iter addAt htF.(sort)
1204

    
1205
let ppFormulae nomTbl tbox (s, f) =
1206
  let card = Array.length !sortTable in
1207
  if card <= 0 then
1208
    raise (C.CoAlgException "Number of sorts must be positive.")
1209
  else ();
1210
  let nnfAndSimplify f = C.simplify (C.nnf f) in
1211
  let  f1    = nnfAndSimplify f in
1212
  let nf1    = nnfAndSimplify (C.NOT f) in
1213
  let  tbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify f)) tbox in
1214
  let ntbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify (C.NOT f))) tbox in
1215

    
1216
  let hcF     =  C.HcFormula.create true in
1217
  let  hcf    = C.hc_formula hcF  f1 in
1218
  let nhcf    = C.hc_formula hcF nf1 in
1219
  let  hctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f))  tbox1 in
1220
  let nhctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f)) ntbox1 in
1221
  let hcfalse = C.hc_formula hcF C.FALSE in
1222
  let hctrue  = C.hc_formula hcF C.TRUE in
1223

    
1224
  let fset = Array.init card (fun _ -> C.HcFHt.create 128) in
1225
  let vset = Array.init card (fun _ -> C.HcFHt.create 128) in
1226
  let atset = C.HcFHt.create 64 in
1227
  let nomset = Hashtbl.create 16 in
1228
  for i = 0 to card-1 do
1229
    detClosure [] nomTbl hcF fset vset atset nomset i hcfalse;
1230
    detClosure [] nomTbl hcF fset vset atset nomset i hctrue;
1231
  done;
1232
  detClosure [] nomTbl hcF fset vset atset nomset s  hcf;
1233
  detClosure [] nomTbl hcF fset vset atset nomset s nhcf;
1234
  List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f)
1235
            hctbox;
1236
  List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f)
1237
            nhctbox;
1238
  Hashtbl.iter (fun n s -> C.HcFHt.iter (detClosureAt hcF atset n) fset.(s)) nomset;
1239

    
1240
  let htF = Array.init card (fun _ -> C.HcFHt.create 128) in
1241
  for i = 0 to card-1 do
1242
    C.HcFHt.add htF.(i) hcfalse 0;
1243
    C.HcFHt.add htF.(i) hctrue 1
1244
  done;
1245
  let addAts f () idx =
1246
    for i = 0 to card-1 do
1247
      C.HcFHt.add htF.(i) f idx
1248
    done;
1249
    idx + 1
1250
  in
1251
  let sizeAt = C.HcFHt.fold addAts atset 2 in
1252
  let addFml i f () idx =
1253
    if C.HcFHt.mem htF.(i) f then idx
1254
    else begin
1255
      C.HcFHt.add htF.(i) f idx;
1256
      idx+1
1257
    end
1258
  in
1259
  let size = ref 0 in
1260
  for i = 0 to card-1 do
1261
    let size2 = C.HcFHt.fold (addFml i) fset.(i) sizeAt in
1262
    if size2 > !size then size := size2 else ()
1263
  done;
1264

    
1265
  arrayFormula := Array.init card (fun _ -> Array.make !size C.TRUE);
1266
  arrayType := Array.init card (fun _ -> Array.make !size Other);
1267
  arrayDest1 := Array.init card (fun _ -> Array.make !size (-1));
1268
  arrayDest2 := Array.init card (fun _ -> Array.make !size (-1));
1269
  arrayDest3 := Array.init card (fun _ -> Array.make !size (-1));
1270
  arrayDeferral := Array.init card (fun _-> Array.make !size(-1));
1271
  arrayNeg := Array.init card (fun _ -> Array.make !size (-1));
1272
  arrayDestNum := Array.init card (fun _ -> Array.make !size (-1));
1273
  arrayDestNum2 := Array.init card (fun _ -> Array.make !size (-1));
1274
  arrayDestAg := Array.init card (fun _ -> Array.make !size (Array.make 0 (-1)));
1275
  let htR = Hashtbl.create 128 in
1276
  Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR vset s) ht) htF;
1277
  arrayAt := Array.init card (fun _ -> Array.init !size (fun _ -> FHt.create 8));
1278
  Hashtbl.iter (initTablesAt hcF htF) nomset;
1279

    
1280
  S.initMisc !size (C.HcFHt.find htF.(0) hcfalse) (C.HcFHt.find htF.(0) hctrue) (-1) (-1) (-1);
1281
  let initbs = bsetMake () in
1282
  bsetAdd initbs (C.HcFHt.find htF.(s) hcf);
1283
  let tboxTbl = Array.init card (fun _ -> bsetMake ()) in
1284
  List.iter (fun (s, f) -> bsetAdd tboxTbl.(s) (C.HcFHt.find htF.(s) f)) hctbox;
1285
  tboxTable := tboxTbl;
1286
  (tbox1, (s, f1), initbs)