Project

General

Profile

Statistics
| Branch: | Revision:

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

History | View | Annotate | Download (46.4 KB)

1 4fd28192 Thorsten Wißmann
(** Common types, functions, and data structures for the CoAlgebraic reasoner.
2
    @author Florian Widmann
3
 *)
4
5
6
module S = MiscSolver
7 f1fa9ad5 Thorsten Wißmann
module L = List
8 4fd28192 Thorsten Wißmann
module C = CoAlgFormula
9
module HC = HashConsing
10
11
12
(** An instantiation of a set (of the standard library) for bitsets.
13
 *)
14
module BsSet = Set.Make(
15
  struct
16
    type t = S.bitset
17
    let (compare : t -> t -> int) = S.compareBS
18
  end
19
 )
20
21
(** An instantiation of a hash table (of the standard library) for bitsets.
22
 *)
23
module GHt = Hashtbl.Make(
24
  struct
25 16af388e Christoph Egger
    type t = S.bitset * S.bitset
26
    let equal ((bs1l, bs1r) : t) (bs2l, bs2r) =
27
      (S.compareBS bs1l bs2l = 0) && (S.compareBS bs1r bs2r = 0)
28
    let hash ((bsl, bsr) : t) = (S.hashBS bsl) lxor (S.hashBS bsr)
29
  end
30
 )
31
32
(** An instantiation of a hash table (of the standard library) for bitsets.
33
 *)
34
module GHtS = Hashtbl.Make(
35
  struct
36 4fd28192 Thorsten Wißmann
    type t = S.bitset
37
    let equal (bs1 : t) bs2 = S.compareBS bs1 bs2 = 0
38
    let hash (bs : t) = S.hashBS bs
39
  end
40
 )
41
42
(** An instantiation of a hash table (of the standard library) for literals.
43
 *)
44
module LHt = Hashtbl.Make(
45
  struct
46
    type t = Minisat.lit
47
    let equal (l1 : t) l2 = l1 = l2
48
    let hash (l : t) = (l :> int)
49
  end
50
 )
51
52
(** An instantiation of a hash table (of the standard library) for formulae.
53
 *)
54
module FHt = Hashtbl.Make(
55
  struct
56
    type t = int
57
    let equal (f1 : t) f2 = f1 = f2
58
    let hash (f : t) = f
59
  end
60
 )
61
62
(** An instantiation of a hash table (of the standard library) for nominals.
63
 *)
64
module NHt = Hashtbl.Make(
65
  struct
66
    type t = int * int
67
    let equal ((s1, f1) : t) (s2, f2) = (s1 = s2) && (f1 = f2)
68
    let hash ((s, f) : t) = (((s+f)*(s+f+1)) / 2) + f
69
  end
70
)
71
72
73
(*****************************************************************************)
74
(*     Types that can be modified rather easily                              *)
75
(*     (of course you then have to modify the implementations below too)     *)
76
(*****************************************************************************)
77
78
(* This type must be extended for additional logics. *)
79
type functors =
80
  | MultiModalK
81 a87192e8 Thorsten Wißmann
  | MultiModalKD
82 f4e43751 Christoph Egger
  | Monotone
83 f1fa9ad5 Thorsten Wißmann
  | CoalitionLogic
84 29b2e3f3 Thorsten Wißmann
  | GML
85 86b07be8 Thorsten Wißmann
  | PML
86 5e0983fe Thorsten Wißmann
  | Constant of string list
87 19f5dad0 Dirk Pattinson
  | Identity
88
  | DefaultImplication
89 4fd28192 Thorsten Wißmann
  | Choice
90
  | Fusion
91
92 5e0983fe Thorsten Wißmann
(* functors whose constructor takes additional parameters *)
93
type parametricFunctorName =
94
  | NameConstant
95
96
(* this type should only be used in the following few helper functions *)
97
type functorName =
98
  | NPa of functors (* No Parameters = functor without parameters *)
99
  | Pa  of parametricFunctorName (* Parameters = functor with parameters *)
100
101
let unaryfunctor2name : (functorName*string) list =
102
  [ (NPa MultiModalK , "MultiModalK")
103
  ; (NPa MultiModalKD , "MultiModalKD")
104 f4e43751 Christoph Egger
  ; (NPa Monotone , "Monotone")
105 5e0983fe Thorsten Wißmann
  ; (NPa GML ,           "GML")
106
  ; (NPa PML ,           "PML")
107
  ; (NPa CoalitionLogic , "CoalitionLogic")
108
  ; (NPa MultiModalK , "K")
109
  ; (NPa MultiModalKD , "KD")
110
  ; (NPa CoalitionLogic , "CL")
111
  ; (Pa  NameConstant , "Const")
112
  ; (Pa  NameConstant , "Constant")
113 19f5dad0 Dirk Pattinson
  ; (NPa Identity, "Id")
114
  ; (NPa Identity, "Identity")
115 db23edf7 Thorsten Wißmann
  ]
116
117 5e0983fe Thorsten Wißmann
let functor2name : (functorName*string) list =
118 db23edf7 Thorsten Wißmann
  L.append unaryfunctor2name
119 5e0983fe Thorsten Wißmann
  [ (NPa Choice , "Choice")
120
  ; (NPa Fusion , "Fusion")
121 db23edf7 Thorsten Wißmann
  ]
122
123 5e0983fe Thorsten Wißmann
let functor_apply_parameters (func : parametricFunctorName) (params: string list) : functors option =
124
    (* apply parameter list to the constructor, denoted by the functor name func *)
125
    (* return None, if the parameters somehow don't match the required parameters *)
126
    match func with
127
    | NameConstant -> Some (Constant params)
128
129
130
let functor_of_string str params : functors option =
131 db23edf7 Thorsten Wißmann
    let fst (a,b) = a in
132
    try
133 5e0983fe Thorsten Wißmann
        let functorName = fst (List.find (fun (f,name) -> name = str) functor2name) in
134
        match functorName with
135
        | NPa x -> Some x
136
        | Pa f -> functor_apply_parameters f params
137 db23edf7 Thorsten Wißmann
    with Not_found -> None
138
139 5e0983fe Thorsten Wißmann
let unaryfunctor_of_string str params =
140
    match (functor_of_string str params) with
141 db23edf7 Thorsten Wißmann
    | Some Choice -> None
142
    | Some Fusion -> None
143
    | x -> x
144
145
let string_of_functor (f: functors) : string =
146 5e0983fe Thorsten Wißmann
    (* replace f orrectly with possibly some Pa wrapper *)
147
    (* also put the parameters into some suffix which will be appended later *)
148
    let f,suffix = match f with
149
            | Constant params -> Pa NameConstant, " "^(String.concat " " params)
150
            | _ -> NPa f, ""
151
    in
152 db23edf7 Thorsten Wißmann
    let snd (a,b) = b in
153
    try
154 5e0983fe Thorsten Wißmann
        let name = snd (List.find (fun (f2,name) -> f = f2) functor2name) in
155
        name ^ suffix
156 db23edf7 Thorsten Wißmann
    with Not_found -> assert false
157
158 4fd28192 Thorsten Wißmann
(* This type may be extended for additional logics. *)
159
type formulaType =
160
  | Other
161 3b055ae8 dirk
  | TrueFalseF (* constant true or false *)
162 4fd28192 Thorsten Wißmann
  | AndF
163
  | OrF
164
  | AtF
165
  | NomF
166 559819d7 Thorsten Wißmann
  | ExF  (* Existential / diamond *)
167
  | AxF  (* Universal / box *)
168 29b2e3f3 Thorsten Wißmann
  | EnforcesF (* diamond of CL *)
169
  | AllowsF   (* box of CL *)
170 af276a36 Thorsten Wißmann
  | MoreThanF (* more than n successors = diamond in gml *)
171
  | MaxExceptF(* at most n exceptions = box in gml *)
172 86b07be8 Thorsten Wißmann
  | AtLeastProbF (* for PML *)
173 9bae2c4f Thorsten Wißmann
  | LessProbFailF (* box for PML *)
174 c49eea11 Thorsten Wißmann
  | ConstF (* constant functor *)
175
  | ConstnF (* constant functor *)
176 19f5dad0 Dirk Pattinson
  | IdF (* Identity functor *)
177
  | NormF (* Default Implication *)
178
  | NormnF (* negation normal form of default implication *)
179 559819d7 Thorsten Wißmann
  | ChcF (* Choice *)
180
  | FusF (* Fusion *)
181 3b407438 Christoph Egger
  | MuF
182
  | NuF
183 4fd28192 Thorsten Wißmann
184
type localFormula = int
185
type bset = S.bitset
186
187
type atFormula = int
188
type cset = S.bitset
189
type csetSet = BsSet.t
190
191
type lht = localFormula LHt.t
192
type fht = Minisat.lit FHt.t
193
type nht = bset NHt.t
194
195 e0f19999 Thorsten Wißmann
type state = { sortS : sort;
196
               mutable bsS : bset; (* a set of formulas who are either literals or
197
                                      modalities (TODO: also @-formulas?).
198
                                      the state is satisfiable if /\bsS is satisfiable.
199
                                    *)
200 3285ac30 Christoph Egger
               mutable deferralS : bset; (* which formulas still have deferrals *)
201 e0f19999 Thorsten Wißmann
               mutable statusS : nodeStatus;
202 4fd28192 Thorsten Wißmann
               mutable parentsS : core list; mutable childrenS : (dependencies * core list) list;
203 73762b19 Thorsten Wißmann
               mutable constraintsS : csetSet; expandFkt : stateExpander;
204
               idx: int }
205 4fd28192 Thorsten Wißmann
206 e0f19999 Thorsten Wißmann
and core = { (* for details, see documentation of newCore *)
207
             sortC : sort;
208
             mutable bsC : bset; (* a set of arbitrary formulas.
209
                                    the present core is satisfiable if /\ bsC is satisfiable *)
210 3285ac30 Christoph Egger
             mutable deferralC : bset; (* which formulas still have deferrals *)
211 e0f19999 Thorsten Wißmann
             mutable statusC : nodeStatus;
212
             mutable parentsC : (state * int) list;
213
             mutable childrenC : state list;
214
             mutable constraintsC : csetSet;
215 9f1263ec Christoph Egger
             mutable solver : Minisat.solver option; (* a solver to find satisfying assignemnts for bsC.
216 e0f19999 Thorsten Wißmann
                                         the solver returns "satisfiable" iff
217
                                         there is a satisfying assignment of
218
                                         bsC which is not represented by some state from the
219
                                         childrenC yet.
220
                                       *)
221
             fht : fht; (* mapping of boolean subformulas of bsC to their corresponding literals
222
                           of the Minisat solver
223
                         *)
224 73762b19 Thorsten Wißmann
             mutable constraintParents : cset list;
225
             idx : int }
226 4fd28192 Thorsten Wißmann
227 d283bf7a Thorsten Wißmann
and setState = state GHt.t array
228 4fd28192 Thorsten Wißmann
229 d283bf7a Thorsten Wißmann
and setCore = core GHt.t array
230 4fd28192 Thorsten Wißmann
231 16af388e Christoph Egger
and setCnstr = unit GHtS.t
232 4fd28192 Thorsten Wißmann
233
234
(*****************************************************************************)
235
(*                Types that are hard coded into the algorithm               *)
236
(*****************************************************************************)
237
238 269d93e5 Thorsten Wißmann
and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *)
239
                  | Conjunctive of 'a (*specifies that all of the 'a need  to be satifsfied *)
240
241 a9949a25 Thorsten Wißmann
and stateExpander = rule lazylist
242 4fd28192 Thorsten Wißmann
243
and sort = C.sort
244
245
and nodeStatus =
246
  | Expandable
247
  | Open
248
  | Sat
249
  | Unsat
250
251 f4498ed1 Christoph Egger
(* In K, given the singleton list [bs] returns the list of all Ax'es
252
   responsible for the individual members of bs being part of the core
253
   as well as the Ex.
254
255
   So given the state { <>φ , []ψ , []η } and the core { φ , ψ , η },
256
   dependency would map { η } to { <>φ , []η } and { ψ } to { <>φ , []ψ }
257
*)
258 4fd28192 Thorsten Wißmann
and dependencies = bset list -> bset
259 269d93e5 Thorsten Wißmann
260 f4498ed1 Christoph Egger
(* Note: sort * bset * bset is to be read as sort * formulas_in_core * deferrals_in_core *)
261 16af388e Christoph Egger
and rule = (dependencies * (sort * bset * bset) lazylist)
262 269d93e5 Thorsten Wißmann
263 a9949a25 Thorsten Wißmann
and 'a lazyliststep =
264 69243f7f Thorsten Wißmann
  | MultipleElements of 'a list
265
  | SingleElement    of 'a
266
  | NoMoreElements
267
268 a9949a25 Thorsten Wißmann
and 'a lazylist = unit -> 'a lazyliststep
269
270
and ruleEnumeration = rule lazyliststep
271
272 f335015f Thorsten Wißmann
let nodeStatusToString : nodeStatus -> string = function
273
  | Expandable -> "Expandable"
274
  | Open -> "Open"
275
  | Sat -> "Sat"
276
  | Unsat -> "Unsat"
277
278 a9949a25 Thorsten Wißmann
let lazylistFromList a_list =
279
    let list_state = ref (Some a_list) in
280
    fun () -> begin match !list_state with
281
              | Some (a_list) -> begin
282
                    list_state := None;
283
                    MultipleElements a_list
284
                end
285
              | None -> NoMoreElements
286
              end
287 4fd28192 Thorsten Wißmann
288 672429b4 Thorsten Wißmann
let rec listFromLazylist evalfunc =
289
    let step = evalfunc () in
290
    match step with
291
    | NoMoreElements -> []
292
    | SingleElement x -> x::(listFromLazylist evalfunc)
293
    | MultipleElements xs -> List.append xs (listFromLazylist evalfunc)
294
295 4fd28192 Thorsten Wißmann
type nominal = sort * localFormula
296
297
type node =
298
  | State of state
299
  | Core of core
300
301
type constrnt =
302
  | UnsatC
303
  | SatC
304
  | OpenC of node list
305
  | UnexpandedC of node list
306
307
type propagateElement =
308
  | UState of state * int option
309
  | UCore of core * bool
310
  | UCnstr of cset
311
312
type queueElement =
313
  | QState of state
314
  | QCore of core
315
  | QCnstr of cset
316
  | QEmpty
317
318
type sortTable = (functors * int list) array
319
320
exception CoAlg_finished of bool
321
322
323
let sortTable = ref (Array.make 0 (MultiModalK, [1]))
324
325 269d93e5 Thorsten Wißmann
let junctionEvalBool : (bool list junction) -> bool = function
326
    | Disjunctive l -> List.fold_right (||) l false
327
    | Conjunctive l -> List.fold_right (&&) l true
328
329
let junctionEval (f: 'a -> bool) : 'a list junction -> bool = function
330
    | Disjunctive l -> List.fold_right (fun x y -> (f x) || y) l false
331
    | Conjunctive l -> List.fold_right (fun x y -> (f x) && y) l true
332
333
let optionalizeOperator (f: 'a -> 'b -> 'c) (x: 'a option) (y: 'b option) : 'c option =
334
    match x with
335
    | None -> None
336
    | Some x -> (match y with
337
                 | None -> None
338
                 | Some y -> Some (f x y))
339
340
let junctionEvalBoolOption : bool option list junction -> bool option =
341
    let f extreme op x y = (* ensure that: (Some True) || None = Some True *)
342
        if x = extreme || y = extreme
343
        then extreme
344
        else optionalizeOperator op x y
345
    in function
346
    | Disjunctive l ->
347
        List.fold_right (f (Some true)  (||)) l (Some false)
348
    | Conjunctive l ->
349
        List.fold_right (f (Some false) (&&)) l (Some true)
350
351
let junctionExtract : 'a junction -> ('a * ('b -> 'b junction)) = function
352
    | Disjunctive l -> (l, fun x -> Disjunctive x)
353
    | Conjunctive l -> (l, fun x -> Conjunctive x)
354 4fd28192 Thorsten Wißmann
355
(*****************************************************************************)
356
(*      "Module type" and a specific implementation of the main queue        *)
357
(*****************************************************************************)
358
359
let queueStates = ref ([] : state list)
360
let queueCores1 = ref ([] : core list)
361
let queueCores2 = ref ([] : core list)
362
let queueCnstrs = ref ([] : cset list)
363
let doPropagation = ref false
364 61c5af02 Christoph Egger
let doPropagationCounter = ref 0
365 4fd28192 Thorsten Wißmann
366
let queueInit () =
367
  queueStates := [];
368
  queueCores1 := [];
369
  queueCores2 := [];
370
  queueCnstrs := [];
371
  doPropagation := false
372
373
let queueIsEmpty () =
374
  !queueStates = [] && !queueCores1 = [] && !queueCores2 = [] && !queueCnstrs = []
375
376
let queueInsertState state = queueStates := state::!queueStates
377
378 d58bba0f Dirk Pattinson
(* original version: breadth-first *)
379 4fd28192 Thorsten Wißmann
let queueInsertCore core = queueCores2 := core::!queueCores2
380
381 034a8dea Christoph Egger
(* experiment: depth first
382 d58bba0f Dirk Pattinson
let queueInsertCore core = queueCores1 := core::!queueCores1
383
*)
384
385 4fd28192 Thorsten Wißmann
let queueInsertCnstr cset = queueCnstrs := cset::!queueCnstrs
386
387
let queueGetElement () =
388
  if !queueCnstrs <> [] then
389
    let res = List.hd !queueCnstrs in
390
    queueCnstrs := List.tl !queueCnstrs;
391
    QCnstr res
392
  else if !queueStates <> [] then
393
    let res = List.hd !queueStates in
394
    queueStates := List.tl !queueStates;
395
    QState res
396
  else if !queueCores1 <> [] then
397
    let res = List.hd !queueCores1 in
398
    queueCores1 := List.tl !queueCores1;
399
    QCore res
400
  else if !queueCores2 = [] then QEmpty
401
  else
402
    let res = List.hd !queueCores2 in
403
    doPropagation := true;
404
    queueCores1 := List.tl !queueCores2;
405
    queueCores2 := [];
406
    QCore res
407
408
let doNominalPropagation () = !doPropagation
409
410 55dc0a64 Christoph Egger
let setPropagationCounter count =
411
  doPropagationCounter := count
412
413 4fd28192 Thorsten Wißmann
let doSatPropagation () =
414 61c5af02 Christoph Egger
  if !doPropagationCounter == 0
415 55dc0a64 Christoph Egger
  then true
416 61c5af02 Christoph Egger
  else begin
417
      doPropagationCounter := !doPropagationCounter - 1;
418
      false
419
    end
420
  (* let res = !doPropagation in *)
421
  (* doPropagation := false; *)
422
  (* res *)
423 4fd28192 Thorsten Wißmann
424
(*****************************************************************************)
425
(*        "Module type" and a specific implementation of the graph           *)
426
(*****************************************************************************)
427
428
let graphStates = ref (Array.make 0 (GHt.create 0 : state GHt.t))
429
let graphCores = ref (Array.make 0 (GHt.create 0 : core GHt.t))
430 16af388e Christoph Egger
let graphCnstrs = ref (GHtS.create 0 : constrnt GHtS.t)
431 4fd28192 Thorsten Wißmann
let graphRoot = ref (None : core option)
432
433
let graphInit () =
434
  let size = Array.length !sortTable in
435
  graphStates := Array.init size (fun _ -> GHt.create 128);
436
  graphCores := Array.init size (fun _ -> GHt.create 128);
437 16af388e Christoph Egger
  graphCnstrs := GHtS.create 128;
438 4fd28192 Thorsten Wißmann
  graphRoot := None
439
440
let graphIterStates fkt =
441
  Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphStates
442
443
let graphIterCores fkt =
444
  Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphCores
445
446 16af388e Christoph Egger
let graphIterCnstrs fkt = GHtS.iter fkt !graphCnstrs
447 4fd28192 Thorsten Wißmann
448
let graphClearCnstr () =
449 16af388e Christoph Egger
  let newGraph = GHtS.create (GHtS.length !graphCnstrs) in
450 4fd28192 Thorsten Wißmann
  let copyCnstr cset cnstr =
451
    match cnstr with
452
    | UnsatC
453 16af388e Christoph Egger
    | SatC -> GHtS.add newGraph cset cnstr
454
    | OpenC _ -> GHtS.add newGraph cset (OpenC [])
455
    | UnexpandedC _ -> GHtS.add newGraph cset (UnexpandedC [])
456 4fd28192 Thorsten Wißmann
  in
457 16af388e Christoph Egger
  GHtS.iter copyCnstr !graphCnstrs;
458 4fd28192 Thorsten Wißmann
  graphCnstrs := newGraph
459
460
let graphFindState sort bs =
461
  try
462
    Some (GHt.find !graphStates.(sort) bs)
463
  with Not_found -> None
464
465
let graphFindCore sort bs =
466
  try
467
    Some (GHt.find !graphCores.(sort) bs)
468
  with Not_found -> None
469
470
let graphFindCnstr cset =
471
  try
472 16af388e Christoph Egger
    Some (GHtS.find !graphCnstrs cset)
473 4fd28192 Thorsten Wißmann
  with Not_found -> None
474
475
let graphInsertState sort bs state =
476
  assert (not (GHt.mem !graphStates.(sort) bs));
477
  GHt.add !graphStates.(sort) bs state
478
479
let graphInsertCore sort bs core =
480
  assert (not (GHt.mem !graphCores.(sort) bs));
481
  GHt.add !graphCores.(sort) bs core
482
483
let graphInsertCnstr cset cnstr =
484 16af388e Christoph Egger
  assert (not (GHtS.mem !graphCnstrs cset));
485
  GHtS.add !graphCnstrs cset cnstr
486 4fd28192 Thorsten Wißmann
487
let graphReplaceCnstr cset cnstr =
488 16af388e Christoph Egger
  GHtS.replace !graphCnstrs cset cnstr
489 4fd28192 Thorsten Wißmann
490
let graphSizeState () =
491
  Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphStates
492
let graphSizeCore () =
493
  Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphCores
494 16af388e Christoph Egger
let graphSizeCnstr () = GHtS.length !graphCnstrs
495 4fd28192 Thorsten Wißmann
496
let graphAddRoot core =
497
  if !graphRoot = None then graphRoot := Some core
498
  else raise (C.CoAlgException "Root of graph is already set.")
499
500
let graphGetRoot () =
501
  match !graphRoot with
502
  | None -> raise (C.CoAlgException "Root of graph is not set.")
503
  | Some core -> core
504
505
506
(*****************************************************************************)
507
(*     "Module type" and a specific implementation of sets of constraints    *)
508
(*****************************************************************************)
509
510
let cssEmpty = BsSet.empty
511
let cssExists fkt css = BsSet.exists fkt css
512
let cssForall fkt css = BsSet.for_all fkt css
513
let cssUnion css1 css2 = BsSet.union css1 css2
514
let cssAdd cset css = BsSet.add cset css
515
let cssFold fkt css init = BsSet.fold fkt css init
516
let cssSingleton cset = BsSet.singleton cset
517
let cssEqual css1 css2 = BsSet.equal css1 css2
518 f335015f Thorsten Wißmann
let cssIter (action: cset -> unit) css =
519
    BsSet.iter action css
520 4fd28192 Thorsten Wißmann
521
522
(*****************************************************************************)
523
(*      "Module type" and a specific implementation of state nodes           *)
524
(*****************************************************************************)
525 73762b19 Thorsten Wißmann
let nodeCounter = ref 0
526
let nextNodeIdx () : int =
527
    let oldVal = !nodeCounter in
528
    nodeCounter := oldVal + 1;
529
    oldVal
530
531 3285ac30 Christoph Egger
let stateMake sort bs defer exp =
532
  { sortS = sort; bsS = bs; deferralS = defer; statusS = Expandable; parentsS = []; childrenS = [];
533 73762b19 Thorsten Wißmann
    constraintsS = cssEmpty; expandFkt = exp;
534
    idx = nextNodeIdx()
535
  }
536 4fd28192 Thorsten Wißmann
let stateGetSort state = state.sortS
537
let stateGetBs state = state.bsS
538
let stateSetBs state bs = state.bsS <- bs
539 3285ac30 Christoph Egger
let stateGetDeferral state = state.deferralS
540
let stateSetDeferral state bs = state.deferralS <- bs
541 4fd28192 Thorsten Wißmann
let stateGetStatus state = state.statusS
542
let stateSetStatus state status = state.statusS <- status
543
let stateGetParents state = state.parentsS
544
let stateAddParent state parent = state.parentsS <- parent::state.parentsS
545
let stateGetRule state idx = List.nth state.childrenS (List.length state.childrenS - idx)
546
let stateGetRules state = state.childrenS
547
let stateAddRule state dep children =
548
  state.childrenS <- (dep, children)::state.childrenS;
549
  List.length state.childrenS
550
let stateGetConstraints state = state.constraintsS
551
let stateSetConstraints state csets = state.constraintsS <- csets
552
let stateNextRule state = state.expandFkt ()
553 73762b19 Thorsten Wißmann
let stateGetIdx (state:state) = state.idx
554 4fd28192 Thorsten Wißmann
555
556
(*****************************************************************************)
557
(*      "Module type" and a specific implementation of core nodes            *)
558
(*****************************************************************************)
559
560 3285ac30 Christoph Egger
let coreMake sort bs defer solver fht =
561
  { sortC = sort; bsC = bs; deferralC = defer; statusC = Expandable; parentsC = []; childrenC = [];
562 73762b19 Thorsten Wißmann
    constraintsC = cssEmpty; solver = solver; fht = fht; constraintParents = [];
563
    idx = nextNodeIdx()
564
  }
565 4fd28192 Thorsten Wißmann
let coreGetSort core = core.sortC
566
let coreGetBs core = core.bsC
567
let coreSetBs core bs = core.bsC <- bs
568 3285ac30 Christoph Egger
let coreGetDeferral core = core.deferralC
569
let coreSetDeferral core bs = core.deferralC <- bs
570 4fd28192 Thorsten Wißmann
let coreGetStatus core = core.statusC
571
let coreSetStatus core status = core.statusC <- status
572
let coreGetParents core = core.parentsC
573
let coreAddParent core parent idx = core.parentsC <- (parent, idx)::core.parentsC
574
let coreGetChildren core = core.childrenC
575
let coreAddChild core child = core.childrenC <- child::core.childrenC
576
let coreGetConstraints core = core.constraintsC
577
let coreSetConstraints core csets = core.constraintsC <- csets
578
let coreGetSolver core = core.solver
579 9f1263ec Christoph Egger
let coreDeallocateSolver core = core.solver <- None; FHt.reset core.fht
580 4fd28192 Thorsten Wißmann
let coreGetFht core = core.fht
581 73762b19 Thorsten Wißmann
let coreGetIdx (core:core) = core.idx
582 4fd28192 Thorsten Wißmann
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 d283bf7a Thorsten Wißmann
let setEmptyState () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
593
let setEmptyCore () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
594 5956a56d Christoph Egger
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 16af388e Christoph Egger
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 d283bf7a Thorsten Wißmann
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 16af388e Christoph Egger
let setIterCnstr fkt set = GHtS.iter (fun cset () -> fkt cset) set
615 50df1dc2 Christoph Egger
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 4fd28192 Thorsten Wißmann
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 b7445f7e Thorsten Wißmann
let bsetRem bs lf = S.remBS bs lf
658 16af388e Christoph Egger
let bsetCompare bs1 bs2 = S.compareBS bs1 bs2
659 45d554b0 Thorsten Wißmann
let bsetMakeRealEmpty () =
660
    let res = bsetMake () in
661
    bsetRem res !S.bstrue; (* remove bstrue which is initially in an empty bset *)
662
    res
663 b7c3a47e Thorsten Wißmann
let bsetCopy bs = S.copyBS bs
664 4fd28192 Thorsten Wißmann
let bsetFold fkt bs init = S.foldBS fkt bs init
665
let bsetIter fkt bset = S.iterBS fkt bset
666 e4cd869a Thorsten Wißmann
let bsetFilter (a: bset) (f: localFormula -> bool) : bset =
667 45d554b0 Thorsten Wißmann
    let res = bsetMakeRealEmpty () in
668 e4cd869a Thorsten Wißmann
    bsetIter (fun form -> if (f form) then bsetAdd res form else ()) a;
669
    res
670
671 4fd28192 Thorsten Wißmann
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 86b07be8 Thorsten Wißmann
 (*
711
    for PML: arrayDest1 = the subformula
712 eda515b6 Thorsten Wißmann
             arrayNum  = the nominator of the probability
713
             arrayNum2 = the denominator of the probability
714 86b07be8 Thorsten Wißmann
 *)
715 f1fa9ad5 Thorsten Wißmann
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 d9f4e4af Christoph Egger
let arrayDeferral = ref (Array.make 0 (Array.make 0 (-1)))  (* deferral at point *)
719 29b2e3f3 Thorsten Wißmann
let arrayDestNum = ref (Array.make 0 (Array.make 0 (-1)))  (* an integer *)
720 eda515b6 Thorsten Wißmann
let arrayDestNum2 = ref (Array.make 0 (Array.make 0 (-1)))  (* another integer *)
721 f1fa9ad5 Thorsten Wißmann
let arrayDestAg = ref (Array.make 0 (Array.make 0 [|0|])) (* arrays of agents *)
722 4fd28192 Thorsten Wißmann
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 c67aca42 Christoph Egger
let lfGetDeferral sort f = !arrayDeferral.(sort).(f)
733 29b2e3f3 Thorsten Wißmann
let lfGetDestNum sort f = !arrayDestNum.(sort).(f)
734 eda515b6 Thorsten Wißmann
let lfGetDestNum2 sort f = !arrayDestNum2.(sort).(f)
735 f1fa9ad5 Thorsten Wißmann
let lfGetDestAg sort f = !arrayDestAg.(sort).(f)
736 4fd28192 Thorsten Wißmann
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 a0cffef0 Thorsten Wißmann
let lfToInt lf = lf
742
let lfFromInt num = num
743 f335015f Thorsten Wißmann
let lfGetFormula sort f = !arrayFormula.(sort).(f)
744
745 de84f40d Christoph Egger
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 f335015f Thorsten Wißmann
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 8d6bf016 Christoph Egger
let coreToString (core:core): string =
761 f335015f Thorsten Wißmann
    let helper cset lst : string list =
762
        (csetToString core.sortC cset):: lst
763
    in
764
    let constraints = cssFold helper core.constraintsC [] in
765 488cea0f Thorsten Wißmann
    let children =
766
        List.map (fun (st:state) -> string_of_int st.idx) core.childrenC
767
    in
768 4164c8e1 Thorsten Wißmann
    let parents =
769
        List.map (fun (st,_:state*int) -> string_of_int st.idx) core.parentsC
770
    in
771 73762b19 Thorsten Wißmann
    "Core "^(string_of_int core.idx)^" {\n"^
772 f335015f Thorsten Wißmann
    "  Status: " ^ (nodeStatusToString core.statusC) ^ "\n"^
773
    "  " ^ bsetToString core.sortC core.bsC ^ "\n" ^
774 16af388e Christoph Egger
    "  Deferrals: \n" ^
775
    "    " ^ bsetToString core.sortC core.deferralC ^ "\n" ^
776 73762b19 Thorsten Wißmann
    "  Constraints: { "^(String.concat
777
                         "\n                 " constraints)^" }\n"^
778 488cea0f Thorsten Wißmann
    "  Children: { "^(String.concat
779
                         ", " children)^" }\n"^
780 4164c8e1 Thorsten Wißmann
    "  Parents: { "^(String.concat ", " parents)^" }\n"^
781 f335015f Thorsten Wißmann
    "}"
782 73762b19 Thorsten Wißmann
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 4164c8e1 Thorsten Wißmann
    let parents =
799
        List.map (fun (co:core) -> string_of_int co.idx) state.parentsS
800
    in
801 73762b19 Thorsten Wißmann
    "State "^(string_of_int state.idx)^" {\n"^
802
    "  Status: " ^ (nodeStatusToString state.statusS) ^ "\n"^
803
    "  " ^ bsetToString state.sortS state.bsS ^ "\n" ^
804 16af388e Christoph Egger
    "  Deferrals: \n" ^
805
    "    " ^ bsetToString state.sortS state.deferralS ^ "\n" ^
806 73762b19 Thorsten Wißmann
    "  Constraints: { "^(String.concat
807
                         "\n                 " constraints)^" }\n"^
808
    "  Children: { "^(String.concat
809
                         "\n              " conclusionList)^" }\n"^
810 4164c8e1 Thorsten Wißmann
    "  Parents: { "^(String.concat ", " parents)^" }\n"^
811 73762b19 Thorsten Wißmann
    "}"
812
813 8d6bf016 Christoph Egger
let stateToDot (state:state): string =
814 c13029a3 Christoph Egger
  let color = match state.statusS with
815
    | Sat -> "green"
816
    | Unsat -> "red"
817
    | Open -> "yellow"
818
    | Expandable -> "white"
819
  in
820 de84f40d Christoph Egger
  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 8d6bf016 Christoph Egger
  let ownidx = (string_of_int state.idx) in
828
  let parents =
829 c13029a3 Christoph Egger
    List.map (fun (co:core) ->
830
              "Node"^string_of_int co.idx^" -> Node"^ownidx^";")
831 8d6bf016 Christoph Egger
             state.parentsS
832
  in
833 c13029a3 Christoph Egger
  "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
834 de84f40d Christoph Egger
  ^ ",label=<State "  ^ ownidx
835
  ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
836
  ^ ">];\n"
837 8d6bf016 Christoph Egger
  ^ (String.concat "\n" parents)
838
839
840
let coreToDot (core:core): string =
841 c13029a3 Christoph Egger
  let color = match core.statusC with
842
    | Sat -> "green"
843
    | Unsat -> "red"
844
    | Open -> "yellow"
845
    | Expandable -> "white"
846
  in
847 de84f40d Christoph Egger
  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 8d6bf016 Christoph Egger
  let ownidx = (string_of_int core.idx) in
855
  let parents =
856 c13029a3 Christoph Egger
    List.map (fun (st,_:state*int) ->
857
              "Node"^string_of_int st.idx^" -> Node"^ownidx^";")
858 8d6bf016 Christoph Egger
             core.parentsC
859
  in
860 c13029a3 Christoph Egger
  "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
861 de84f40d Christoph Egger
  ^ ",label=<Core "  ^ ownidx
862
  ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
863
  ^ ">];\n"
864 8d6bf016 Christoph Egger
  ^ (String.concat "\n" parents)
865
866
867 488cea0f Thorsten Wißmann
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 73762b19 Thorsten Wißmann
883
884 4fd28192 Thorsten Wißmann
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 4b0d0388 Christoph Egger
(* Calculate all possible formulae. This includes all subformulae and
894
   in the case of μ-Calculus the Fischer-Ladner closure.
895 4fd28192 Thorsten Wißmann
896 4b0d0388 Christoph Egger
   TODO: variable sort needs to match epected sort
897
 *)
898 cb12f8a5 Christoph Egger
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 4fd28192 Thorsten Wißmann
  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 653eaa4b Christoph Egger
  if C.HcFHt.mem vset.(s) f &&
909 066ed7b8 Christoph Egger
    (compare (C.HcFHt.find vset.(s) f) deferral = 0 ||
910
        compare deferral "ε" = 0)
911 1b17ef3c Christoph Egger
  then ()
912 4fd28192 Thorsten Wißmann
  else
913 cb12f8a5 Christoph Egger
    let () = C.HcFHt.add vset.(s) f deferral in
914 4fd28192 Thorsten Wißmann
    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 43194ed2 Christoph Egger
    | C.HCFALSE
919
    | C.HCVAR _ -> ()
920 4fd28192 Thorsten Wißmann
    | 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 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset s1 hcnom;
942
        detClosure_ nomTbl hcF fset vset atset nomset s1 f1
943 4fd28192 Thorsten Wißmann
    | C.HCOR (f1, f2)
944
    | C.HCAND (f1, f2) ->
945 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset s f1;
946
        detClosure_ nomTbl hcF fset vset atset nomset s f2
947 4fd28192 Thorsten Wißmann
    | C.HCEX (_, f1)
948
    | C.HCAX (_, f1) ->
949 f4e43751 Christoph Egger
        if (func <> MultiModalK && func <> MultiModalKD && func <> Monotone)
950 2a84977e Thorsten Wißmann
            || List.length sortlst <> 1
951
        then raise (C.CoAlgException "Ex/Ax-formula is used in wrong sort.")
952 4fd28192 Thorsten Wißmann
        else ();
953 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
954 f1fa9ad5 Thorsten Wißmann
    | 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 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
960 af276a36 Thorsten Wißmann
    | C.HCMORETHAN (_,_,f1)
961
    | C.HCMAXEXCEPT (_,_,f1) ->
962 29b2e3f3 Thorsten Wißmann
        if func <> GML || List.length sortlst <> 1
963
        then raise (C.CoAlgException "[{>=,<=}]-formula is used in wrong sort.")
964
        else ();
965 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
966 86b07be8 Thorsten Wißmann
    | C.HCATLEASTPROB (_,f1)
967 9bae2c4f Thorsten Wißmann
    | C.HCLESSPROBFAIL (_,f1) ->
968 86b07be8 Thorsten Wißmann
        if func <> PML || List.length sortlst <> 1
969 c855ba91 Thorsten Wißmann
        then raise (C.CoAlgException "[{>=,<}]-formula with probability is used in wrong sort.")
970 86b07be8 Thorsten Wißmann
        else ();
971 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1;
972 9bae2c4f Thorsten Wißmann
        (*
973
            TODO: add ¬ f1 to the closure!
974
        detClosure nomTbl hcF fset atset nomset (List.hd sortlst) (f1.HC.node.negNde)
975
        *)
976 5e0983fe Thorsten Wißmann
    | 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 c49eea11 Thorsten Wißmann
        then raise (C.CoAlgException "=-formula is used in wrong sort.")
987
        else ();
988
      (* NB: =-formulae have no subformlae hence no closure *)
989 19f5dad0 Dirk Pattinson
    | 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 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1;
995 19f5dad0 Dirk Pattinson
    | 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 cb12f8a5 Christoph Egger
        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 19f5dad0 Dirk Pattinson
1004 d58bba0f Dirk Pattinson
    | C.HCCHC (f1, f2) ->
1005 4fd28192 Thorsten Wißmann
        if func <> Choice || List.length sortlst <> 2 then
1006
          raise (C.CoAlgException "Choice formula is used in wrong sort.")
1007
        else ();
1008 cb12f8a5 Christoph Egger
        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 4fd28192 Thorsten Wißmann
    | 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 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset s1 f1
1016 034a8dea Christoph Egger
    (*
1017 6553983f Christoph Egger
       FL(μ X . φ) = {μ X . φ} ∪ FL(φ[X|->μ X . φ])
1018 034a8dea Christoph Egger
     *)
1019
    | C.HCMU (name, f1) ->
1020 cb12f8a5 Christoph Egger
       let () = C.HcFHt.replace vset.(s) f name in
1021 034a8dea Christoph Egger
       let unfold = C.hc_replace hcF name f f1 in
1022 cb12f8a5 Christoph Egger
       let appendvars = List.append newvars [name] in
1023
       detClosure appendvars nomTbl hcF fset vset atset nomset s unfold
1024 034a8dea Christoph Egger
    | C.HCNU (name, f1) ->
1025
       let unfold = C.hc_replace hcF name f f1 in
1026 cb12f8a5 Christoph Egger
       detClosure_ nomTbl hcF fset vset atset nomset s unfold
1027 6553983f Christoph Egger
1028 4fd28192 Thorsten Wißmann
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 034a8dea Christoph Egger
      let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
1038 4fd28192 Thorsten Wißmann
      C.HcFHt.replace atset at ()
1039
1040
(** Initialises the arrays for a formula and its integer representation.
1041
 *)
1042 d9f4e4af Christoph Egger
let initTables nomTbl hcF htF htR vset s f n =
1043 4fd28192 Thorsten Wißmann
  !arrayFormula.(s).(n) <- f.HC.fml;
1044 d9f4e4af Christoph Egger
  !arrayDeferral.(s).(n) <- Hashtbl.hash (C.HcFHt.find vset.(s) f);
1045 4fd28192 Thorsten Wißmann
  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 3b055ae8 dirk
  | C.HCFALSE -> !arrayType.(s).(n) <- TrueFalseF
1051 4fd28192 Thorsten Wißmann
  | 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 034a8dea Christoph Egger
  | C.HCEX (role, f1) ->
1075 4fd28192 Thorsten Wißmann
      !arrayType.(s).(n) <- ExF;
1076
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1077 034a8dea Christoph Egger
      !arrayDest3.(s).(n) <-
1078 4fd28192 Thorsten Wißmann
        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 f1fa9ad5 Thorsten Wißmann
  | 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 af276a36 Thorsten Wißmann
  | C.HCMORETHAN (cnt,role,f1) ->
1101
      !arrayType.(s).(n) <- MoreThanF;
1102 29b2e3f3 Thorsten Wißmann
      !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 af276a36 Thorsten Wißmann
  | C.HCMAXEXCEPT (cnt,role,f1) ->
1111
      !arrayType.(s).(n) <- MaxExceptF;
1112 29b2e3f3 Thorsten Wißmann
      !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 86b07be8 Thorsten Wißmann
  | C.HCATLEASTPROB (p,f1) ->
1121
      !arrayType.(s).(n) <- AtLeastProbF;
1122
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1123 eda515b6 Thorsten Wißmann
      !arrayDestNum.(s).(n) <- p.C.nominator;
1124
      !arrayDestNum2.(s).(n) <- p.C.denominator
1125 9bae2c4f Thorsten Wißmann
  | C.HCLESSPROBFAIL (p,f1) ->
1126
      !arrayType.(s).(n) <- LessProbFailF;
1127 86b07be8 Thorsten Wißmann
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1128 eda515b6 Thorsten Wißmann
      !arrayDestNum.(s).(n) <- p.C.nominator;
1129
      !arrayDestNum2.(s).(n) <- p.C.denominator
1130 c49eea11 Thorsten Wißmann
  | 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 19f5dad0 Dirk Pattinson
  | C.HCID (f1) ->
1157
      !arrayType.(s).(n) <- IdF;
1158 d58bba0f Dirk Pattinson
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1
1159 034a8dea Christoph Egger
  | C.HCNORM (f1, f2) ->
1160 19f5dad0 Dirk Pattinson
      !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 034a8dea Christoph Egger
  | C.HCNORMN (f1, f2) ->
1164 19f5dad0 Dirk Pattinson
      !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 d58bba0f Dirk Pattinson
  | C.HCCHC (f1, f2) ->
1169 4fd28192 Thorsten Wißmann
      !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 5ec97220 Christoph Egger
  | C.HCMU (name, f1) ->
1178
     !arrayType.(s).(n) <- MuF;
1179 034a8dea Christoph Egger
     let unfold = C.hc_replace hcF name f f1 in
1180
     !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold
1181 5ec97220 Christoph Egger
  | C.HCNU (name, f1) ->
1182 034a8dea Christoph Egger
     !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 5ec97220 Christoph Egger
  | C.HCVAR _ -> !arrayType.(s).(n) <- Other
1186
1187 4fd28192 Thorsten Wißmann
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 034a8dea Christoph Egger
        let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
1200 4fd28192 Thorsten Wißmann
        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 f828ad2f Thorsten Wißmann
  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 4fd28192 Thorsten Wißmann
  let hcfalse = C.hc_formula hcF C.FALSE in
1222 f828ad2f Thorsten Wißmann
  let hctrue  = C.hc_formula hcF C.TRUE in
1223 4fd28192 Thorsten Wißmann
1224
  let fset = Array.init card (fun _ -> C.HcFHt.create 128) in
1225 cb12f8a5 Christoph Egger
  let vset = Array.init card (fun _ -> C.HcFHt.create 128) in
1226 4fd28192 Thorsten Wißmann
  let atset = C.HcFHt.create 64 in
1227
  let nomset = Hashtbl.create 16 in
1228
  for i = 0 to card-1 do
1229 cb12f8a5 Christoph Egger
    detClosure [] nomTbl hcF fset vset atset nomset i hcfalse;
1230
    detClosure [] nomTbl hcF fset vset atset nomset i hctrue;
1231 4fd28192 Thorsten Wißmann
  done;
1232 cb12f8a5 Christoph Egger
  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 4fd28192 Thorsten Wißmann
  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 d9f4e4af Christoph Egger
  arrayDeferral := Array.init card (fun _-> Array.make !size(-1));
1271 4fd28192 Thorsten Wißmann
  arrayNeg := Array.init card (fun _ -> Array.make !size (-1));
1272 29b2e3f3 Thorsten Wißmann
  arrayDestNum := Array.init card (fun _ -> Array.make !size (-1));
1273 eda515b6 Thorsten Wißmann
  arrayDestNum2 := Array.init card (fun _ -> Array.make !size (-1));
1274 98af95fb Thorsten Wißmann
  arrayDestAg := Array.init card (fun _ -> Array.make !size (Array.make 0 (-1)));
1275 4fd28192 Thorsten Wißmann
  let htR = Hashtbl.create 128 in
1276 d9f4e4af Christoph Egger
  Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR vset s) ht) htF;
1277 4fd28192 Thorsten Wißmann
  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)