Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgMisc.ml @ de84f40d

History | View | Annotate | Download (45.8 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 f1fa9ad5 Thorsten Wißmann
  | CoalitionLogic
83 29b2e3f3 Thorsten Wißmann
  | GML
84 86b07be8 Thorsten Wißmann
  | PML
85 5e0983fe Thorsten Wißmann
  | Constant of string list
86 19f5dad0 Dirk Pattinson
  | Identity
87
  | DefaultImplication
88 4fd28192 Thorsten Wißmann
  | Choice
89
  | Fusion
90
91 5e0983fe Thorsten Wißmann
(* functors whose constructor takes additional parameters *)
92
type parametricFunctorName =
93
  | NameConstant
94
95
(* this type should only be used in the following few helper functions *)
96
type functorName =
97
  | NPa of functors (* No Parameters = functor without parameters *)
98
  | Pa  of parametricFunctorName (* Parameters = functor with parameters *)
99
100
let unaryfunctor2name : (functorName*string) list =
101
  [ (NPa MultiModalK , "MultiModalK")
102
  ; (NPa MultiModalKD , "MultiModalKD")
103
  ; (NPa GML ,           "GML")
104
  ; (NPa PML ,           "PML")
105
  ; (NPa CoalitionLogic , "CoalitionLogic")
106
  ; (NPa MultiModalK , "K")
107
  ; (NPa MultiModalKD , "KD")
108
  ; (NPa CoalitionLogic , "CL")
109
  ; (Pa  NameConstant , "Const")
110
  ; (Pa  NameConstant , "Constant")
111 19f5dad0 Dirk Pattinson
  ; (NPa Identity, "Id")
112
  ; (NPa Identity, "Identity")
113 db23edf7 Thorsten Wißmann
  ]
114
115 5e0983fe Thorsten Wißmann
let functor2name : (functorName*string) list =
116 db23edf7 Thorsten Wißmann
  L.append unaryfunctor2name
117 5e0983fe Thorsten Wißmann
  [ (NPa Choice , "Choice")
118
  ; (NPa Fusion , "Fusion")
119 db23edf7 Thorsten Wißmann
  ]
120
121 5e0983fe Thorsten Wißmann
let functor_apply_parameters (func : parametricFunctorName) (params: string list) : functors option =
122
    (* apply parameter list to the constructor, denoted by the functor name func *)
123
    (* return None, if the parameters somehow don't match the required parameters *)
124
    match func with
125
    | NameConstant -> Some (Constant params)
126
127
128
let functor_of_string str params : functors option =
129 db23edf7 Thorsten Wißmann
    let fst (a,b) = a in
130
    try
131 5e0983fe Thorsten Wißmann
        let functorName = fst (List.find (fun (f,name) -> name = str) functor2name) in
132
        match functorName with
133
        | NPa x -> Some x
134
        | Pa f -> functor_apply_parameters f params
135 db23edf7 Thorsten Wißmann
    with Not_found -> None
136
137 5e0983fe Thorsten Wißmann
let unaryfunctor_of_string str params =
138
    match (functor_of_string str params) with
139 db23edf7 Thorsten Wißmann
    | Some Choice -> None
140
    | Some Fusion -> None
141
    | x -> x
142
143
let string_of_functor (f: functors) : string =
144 5e0983fe Thorsten Wißmann
    (* replace f orrectly with possibly some Pa wrapper *)
145
    (* also put the parameters into some suffix which will be appended later *)
146
    let f,suffix = match f with
147
            | Constant params -> Pa NameConstant, " "^(String.concat " " params)
148
            | _ -> NPa f, ""
149
    in
150 db23edf7 Thorsten Wißmann
    let snd (a,b) = b in
151
    try
152 5e0983fe Thorsten Wißmann
        let name = snd (List.find (fun (f2,name) -> f = f2) functor2name) in
153
        name ^ suffix
154 db23edf7 Thorsten Wißmann
    with Not_found -> assert false
155
156 4fd28192 Thorsten Wißmann
(* This type may be extended for additional logics. *)
157
type formulaType =
158
  | Other
159 3b055ae8 dirk
  | TrueFalseF (* constant true or false *)
160 4fd28192 Thorsten Wißmann
  | AndF
161
  | OrF
162
  | AtF
163
  | NomF
164 559819d7 Thorsten Wißmann
  | ExF  (* Existential / diamond *)
165
  | AxF  (* Universal / box *)
166 29b2e3f3 Thorsten Wißmann
  | EnforcesF (* diamond of CL *)
167
  | AllowsF   (* box of CL *)
168 af276a36 Thorsten Wißmann
  | MoreThanF (* more than n successors = diamond in gml *)
169
  | MaxExceptF(* at most n exceptions = box in gml *)
170 86b07be8 Thorsten Wißmann
  | AtLeastProbF (* for PML *)
171 9bae2c4f Thorsten Wißmann
  | LessProbFailF (* box for PML *)
172 c49eea11 Thorsten Wißmann
  | ConstF (* constant functor *)
173
  | ConstnF (* constant functor *)
174 19f5dad0 Dirk Pattinson
  | IdF (* Identity functor *)
175
  | NormF (* Default Implication *)
176
  | NormnF (* negation normal form of default implication *)
177 559819d7 Thorsten Wißmann
  | ChcF (* Choice *)
178
  | FusF (* Fusion *)
179 3b407438 Christoph Egger
  | MuF
180
  | NuF
181 4fd28192 Thorsten Wißmann
182
type localFormula = int
183
type bset = S.bitset
184
185
type atFormula = int
186
type cset = S.bitset
187
type csetSet = BsSet.t
188
189
type lht = localFormula LHt.t
190
type fht = Minisat.lit FHt.t
191
type nht = bset NHt.t
192
193 e0f19999 Thorsten Wißmann
type state = { sortS : sort;
194
               mutable bsS : bset; (* a set of formulas who are either literals or
195
                                      modalities (TODO: also @-formulas?).
196
                                      the state is satisfiable if /\bsS is satisfiable.
197
                                    *)
198 3285ac30 Christoph Egger
               mutable deferralS : bset; (* which formulas still have deferrals *)
199 e0f19999 Thorsten Wißmann
               mutable statusS : nodeStatus;
200 4fd28192 Thorsten Wißmann
               mutable parentsS : core list; mutable childrenS : (dependencies * core list) list;
201 73762b19 Thorsten Wißmann
               mutable constraintsS : csetSet; expandFkt : stateExpander;
202
               idx: int }
203 4fd28192 Thorsten Wißmann
204 e0f19999 Thorsten Wißmann
and core = { (* for details, see documentation of newCore *)
205
             sortC : sort;
206
             mutable bsC : bset; (* a set of arbitrary formulas.
207
                                    the present core is satisfiable if /\ bsC is satisfiable *)
208 3285ac30 Christoph Egger
             mutable deferralC : bset; (* which formulas still have deferrals *)
209 e0f19999 Thorsten Wißmann
             mutable statusC : nodeStatus;
210
             mutable parentsC : (state * int) list;
211
             mutable childrenC : state list;
212
             mutable constraintsC : csetSet;
213
             solver : Minisat.solver; (* a solver to find satisfying assignemnts for bsC.
214
                                         the solver returns "satisfiable" iff
215
                                         there is a satisfying assignment of
216
                                         bsC which is not represented by some state from the
217
                                         childrenC yet.
218
                                       *)
219
             fht : fht; (* mapping of boolean subformulas of bsC to their corresponding literals
220
                           of the Minisat solver
221
                         *)
222 73762b19 Thorsten Wißmann
             mutable constraintParents : cset list;
223
             idx : int }
224 4fd28192 Thorsten Wißmann
225 d283bf7a Thorsten Wißmann
and setState = state GHt.t array
226 4fd28192 Thorsten Wißmann
227 d283bf7a Thorsten Wißmann
and setCore = core GHt.t array
228 4fd28192 Thorsten Wißmann
229 16af388e Christoph Egger
and setCnstr = unit GHtS.t
230 4fd28192 Thorsten Wißmann
231
232
(*****************************************************************************)
233
(*                Types that are hard coded into the algorithm               *)
234
(*****************************************************************************)
235
236 269d93e5 Thorsten Wißmann
and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *)
237
                  | Conjunctive of 'a (*specifies that all of the 'a need  to be satifsfied *)
238
239 a9949a25 Thorsten Wißmann
and stateExpander = rule lazylist
240 4fd28192 Thorsten Wißmann
241
and sort = C.sort
242
243
and nodeStatus =
244
  | Expandable
245
  | Open
246
  | Sat
247
  | Unsat
248
249 f4498ed1 Christoph Egger
(* In K, given the singleton list [bs] returns the list of all Ax'es
250
   responsible for the individual members of bs being part of the core
251
   as well as the Ex.
252
253
   So given the state { <>φ , []ψ , []η } and the core { φ , ψ , η },
254
   dependency would map { η } to { <>φ , []η } and { ψ } to { <>φ , []ψ }
255
*)
256 4fd28192 Thorsten Wißmann
and dependencies = bset list -> bset
257 269d93e5 Thorsten Wißmann
258 f4498ed1 Christoph Egger
(* Note: sort * bset * bset is to be read as sort * formulas_in_core * deferrals_in_core *)
259 16af388e Christoph Egger
and rule = (dependencies * (sort * bset * bset) lazylist)
260 269d93e5 Thorsten Wißmann
261 a9949a25 Thorsten Wißmann
and 'a lazyliststep =
262 69243f7f Thorsten Wißmann
  | MultipleElements of 'a list
263
  | SingleElement    of 'a
264
  | NoMoreElements
265
266 a9949a25 Thorsten Wißmann
and 'a lazylist = unit -> 'a lazyliststep
267
268
and ruleEnumeration = rule lazyliststep
269
270 f335015f Thorsten Wißmann
let nodeStatusToString : nodeStatus -> string = function
271
  | Expandable -> "Expandable"
272
  | Open -> "Open"
273
  | Sat -> "Sat"
274
  | Unsat -> "Unsat"
275
276 a9949a25 Thorsten Wißmann
let lazylistFromList a_list =
277
    let list_state = ref (Some a_list) in
278
    fun () -> begin match !list_state with
279
              | Some (a_list) -> begin
280
                    list_state := None;
281
                    MultipleElements a_list
282
                end
283
              | None -> NoMoreElements
284
              end
285 4fd28192 Thorsten Wißmann
286 672429b4 Thorsten Wißmann
let rec listFromLazylist evalfunc =
287
    let step = evalfunc () in
288
    match step with
289
    | NoMoreElements -> []
290
    | SingleElement x -> x::(listFromLazylist evalfunc)
291
    | MultipleElements xs -> List.append xs (listFromLazylist evalfunc)
292
293 4fd28192 Thorsten Wißmann
type nominal = sort * localFormula
294
295
type node =
296
  | State of state
297
  | Core of core
298
299
type constrnt =
300
  | UnsatC
301
  | SatC
302
  | OpenC of node list
303
  | UnexpandedC of node list
304
305
type propagateElement =
306
  | UState of state * int option
307
  | UCore of core * bool
308
  | UCnstr of cset
309
310
type queueElement =
311
  | QState of state
312
  | QCore of core
313
  | QCnstr of cset
314
  | QEmpty
315
316
type sortTable = (functors * int list) array
317
318
exception CoAlg_finished of bool
319
320
321
let sortTable = ref (Array.make 0 (MultiModalK, [1]))
322
323 269d93e5 Thorsten Wißmann
let junctionEvalBool : (bool list junction) -> bool = function
324
    | Disjunctive l -> List.fold_right (||) l false
325
    | Conjunctive l -> List.fold_right (&&) l true
326
327
let junctionEval (f: 'a -> bool) : 'a list junction -> bool = function
328
    | Disjunctive l -> List.fold_right (fun x y -> (f x) || y) l false
329
    | Conjunctive l -> List.fold_right (fun x y -> (f x) && y) l true
330
331
let optionalizeOperator (f: 'a -> 'b -> 'c) (x: 'a option) (y: 'b option) : 'c option =
332
    match x with
333
    | None -> None
334
    | Some x -> (match y with
335
                 | None -> None
336
                 | Some y -> Some (f x y))
337
338
let junctionEvalBoolOption : bool option list junction -> bool option =
339
    let f extreme op x y = (* ensure that: (Some True) || None = Some True *)
340
        if x = extreme || y = extreme
341
        then extreme
342
        else optionalizeOperator op x y
343
    in function
344
    | Disjunctive l ->
345
        List.fold_right (f (Some true)  (||)) l (Some false)
346
    | Conjunctive l ->
347
        List.fold_right (f (Some false) (&&)) l (Some true)
348
349
let junctionExtract : 'a junction -> ('a * ('b -> 'b junction)) = function
350
    | Disjunctive l -> (l, fun x -> Disjunctive x)
351
    | Conjunctive l -> (l, fun x -> Conjunctive x)
352 4fd28192 Thorsten Wißmann
353
(*****************************************************************************)
354
(*      "Module type" and a specific implementation of the main queue        *)
355
(*****************************************************************************)
356
357
let queueStates = ref ([] : state list)
358
let queueCores1 = ref ([] : core list)
359
let queueCores2 = ref ([] : core list)
360
let queueCnstrs = ref ([] : cset list)
361
let doPropagation = ref false
362
363
let queueInit () =
364
  queueStates := [];
365
  queueCores1 := [];
366
  queueCores2 := [];
367
  queueCnstrs := [];
368
  doPropagation := false
369
370
let queueIsEmpty () =
371
  !queueStates = [] && !queueCores1 = [] && !queueCores2 = [] && !queueCnstrs = []
372
373
let queueInsertState state = queueStates := state::!queueStates
374
375 d58bba0f Dirk Pattinson
(* original version: breadth-first *)
376 4fd28192 Thorsten Wißmann
let queueInsertCore core = queueCores2 := core::!queueCores2
377
378 034a8dea Christoph Egger
(* experiment: depth first
379 d58bba0f Dirk Pattinson
let queueInsertCore core = queueCores1 := core::!queueCores1
380
*)
381
382 4fd28192 Thorsten Wißmann
let queueInsertCnstr cset = queueCnstrs := cset::!queueCnstrs
383
384
let queueGetElement () =
385
  if !queueCnstrs <> [] then
386
    let res = List.hd !queueCnstrs in
387
    queueCnstrs := List.tl !queueCnstrs;
388
    QCnstr res
389
  else if !queueStates <> [] then
390
    let res = List.hd !queueStates in
391
    queueStates := List.tl !queueStates;
392
    QState res
393
  else if !queueCores1 <> [] then
394
    let res = List.hd !queueCores1 in
395
    queueCores1 := List.tl !queueCores1;
396
    QCore res
397
  else if !queueCores2 = [] then QEmpty
398
  else
399
    let res = List.hd !queueCores2 in
400
    doPropagation := true;
401
    queueCores1 := List.tl !queueCores2;
402
    queueCores2 := [];
403
    QCore res
404
405
let doNominalPropagation () = !doPropagation
406
407
let doSatPropagation () =
408
  let res = !doPropagation in
409
  doPropagation := false;
410
  res
411
412
(*****************************************************************************)
413
(*        "Module type" and a specific implementation of the graph           *)
414
(*****************************************************************************)
415
416
let graphStates = ref (Array.make 0 (GHt.create 0 : state GHt.t))
417
let graphCores = ref (Array.make 0 (GHt.create 0 : core GHt.t))
418 16af388e Christoph Egger
let graphCnstrs = ref (GHtS.create 0 : constrnt GHtS.t)
419 4fd28192 Thorsten Wißmann
let graphRoot = ref (None : core option)
420
421
let graphInit () =
422
  let size = Array.length !sortTable in
423
  graphStates := Array.init size (fun _ -> GHt.create 128);
424
  graphCores := Array.init size (fun _ -> GHt.create 128);
425 16af388e Christoph Egger
  graphCnstrs := GHtS.create 128;
426 4fd28192 Thorsten Wißmann
  graphRoot := None
427
428
let graphIterStates fkt =
429
  Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphStates
430
431
let graphIterCores fkt =
432
  Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) !graphCores
433
434 16af388e Christoph Egger
let graphIterCnstrs fkt = GHtS.iter fkt !graphCnstrs
435 4fd28192 Thorsten Wißmann
436
let graphClearCnstr () =
437 16af388e Christoph Egger
  let newGraph = GHtS.create (GHtS.length !graphCnstrs) in
438 4fd28192 Thorsten Wißmann
  let copyCnstr cset cnstr =
439
    match cnstr with
440
    | UnsatC
441 16af388e Christoph Egger
    | SatC -> GHtS.add newGraph cset cnstr
442
    | OpenC _ -> GHtS.add newGraph cset (OpenC [])
443
    | UnexpandedC _ -> GHtS.add newGraph cset (UnexpandedC [])
444 4fd28192 Thorsten Wißmann
  in
445 16af388e Christoph Egger
  GHtS.iter copyCnstr !graphCnstrs;
446 4fd28192 Thorsten Wißmann
  graphCnstrs := newGraph
447
448
let graphFindState sort bs =
449
  try
450
    Some (GHt.find !graphStates.(sort) bs)
451
  with Not_found -> None
452
453
let graphFindCore sort bs =
454
  try
455
    Some (GHt.find !graphCores.(sort) bs)
456
  with Not_found -> None
457
458
let graphFindCnstr cset =
459
  try
460 16af388e Christoph Egger
    Some (GHtS.find !graphCnstrs cset)
461 4fd28192 Thorsten Wißmann
  with Not_found -> None
462
463
let graphInsertState sort bs state =
464
  assert (not (GHt.mem !graphStates.(sort) bs));
465
  GHt.add !graphStates.(sort) bs state
466
467
let graphInsertCore sort bs core =
468
  assert (not (GHt.mem !graphCores.(sort) bs));
469
  GHt.add !graphCores.(sort) bs core
470
471
let graphInsertCnstr cset cnstr =
472 16af388e Christoph Egger
  assert (not (GHtS.mem !graphCnstrs cset));
473
  GHtS.add !graphCnstrs cset cnstr
474 4fd28192 Thorsten Wißmann
475
let graphReplaceCnstr cset cnstr =
476 16af388e Christoph Egger
  GHtS.replace !graphCnstrs cset cnstr
477 4fd28192 Thorsten Wißmann
478
let graphSizeState () =
479
  Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphStates
480
let graphSizeCore () =
481
  Array.fold_left (fun acc ht -> acc + GHt.length ht) 0 !graphCores
482 16af388e Christoph Egger
let graphSizeCnstr () = GHtS.length !graphCnstrs
483 4fd28192 Thorsten Wißmann
484
let graphAddRoot core =
485
  if !graphRoot = None then graphRoot := Some core
486
  else raise (C.CoAlgException "Root of graph is already set.")
487
488
let graphGetRoot () =
489
  match !graphRoot with
490
  | None -> raise (C.CoAlgException "Root of graph is not set.")
491
  | Some core -> core
492
493
494
(*****************************************************************************)
495
(*     "Module type" and a specific implementation of sets of constraints    *)
496
(*****************************************************************************)
497
498
let cssEmpty = BsSet.empty
499
let cssExists fkt css = BsSet.exists fkt css
500
let cssForall fkt css = BsSet.for_all fkt css
501
let cssUnion css1 css2 = BsSet.union css1 css2
502
let cssAdd cset css = BsSet.add cset css
503
let cssFold fkt css init = BsSet.fold fkt css init
504
let cssSingleton cset = BsSet.singleton cset
505
let cssEqual css1 css2 = BsSet.equal css1 css2
506 f335015f Thorsten Wißmann
let cssIter (action: cset -> unit) css =
507
    BsSet.iter action css
508 4fd28192 Thorsten Wißmann
509
510
(*****************************************************************************)
511
(*      "Module type" and a specific implementation of state nodes           *)
512
(*****************************************************************************)
513 73762b19 Thorsten Wißmann
let nodeCounter = ref 0
514
let nextNodeIdx () : int =
515
    let oldVal = !nodeCounter in
516
    nodeCounter := oldVal + 1;
517
    oldVal
518
519 3285ac30 Christoph Egger
let stateMake sort bs defer exp =
520
  { sortS = sort; bsS = bs; deferralS = defer; statusS = Expandable; parentsS = []; childrenS = [];
521 73762b19 Thorsten Wißmann
    constraintsS = cssEmpty; expandFkt = exp;
522
    idx = nextNodeIdx()
523
  }
524 4fd28192 Thorsten Wißmann
let stateGetSort state = state.sortS
525
let stateGetBs state = state.bsS
526
let stateSetBs state bs = state.bsS <- bs
527 3285ac30 Christoph Egger
let stateGetDeferral state = state.deferralS
528
let stateSetDeferral state bs = state.deferralS <- bs
529 4fd28192 Thorsten Wißmann
let stateGetStatus state = state.statusS
530
let stateSetStatus state status = state.statusS <- status
531
let stateGetParents state = state.parentsS
532
let stateAddParent state parent = state.parentsS <- parent::state.parentsS
533
let stateGetRule state idx = List.nth state.childrenS (List.length state.childrenS - idx)
534
let stateGetRules state = state.childrenS
535
let stateAddRule state dep children =
536
  state.childrenS <- (dep, children)::state.childrenS;
537
  List.length state.childrenS
538
let stateGetConstraints state = state.constraintsS
539
let stateSetConstraints state csets = state.constraintsS <- csets
540
let stateNextRule state = state.expandFkt ()
541 73762b19 Thorsten Wißmann
let stateGetIdx (state:state) = state.idx
542 4fd28192 Thorsten Wißmann
543
544
(*****************************************************************************)
545
(*      "Module type" and a specific implementation of core nodes            *)
546
(*****************************************************************************)
547
548 3285ac30 Christoph Egger
let coreMake sort bs defer solver fht =
549
  { sortC = sort; bsC = bs; deferralC = defer; statusC = Expandable; parentsC = []; childrenC = [];
550 73762b19 Thorsten Wißmann
    constraintsC = cssEmpty; solver = solver; fht = fht; constraintParents = [];
551
    idx = nextNodeIdx()
552
  }
553 4fd28192 Thorsten Wißmann
let coreGetSort core = core.sortC
554
let coreGetBs core = core.bsC
555
let coreSetBs core bs = core.bsC <- bs
556 3285ac30 Christoph Egger
let coreGetDeferral core = core.deferralC
557
let coreSetDeferral core bs = core.deferralC <- bs
558 4fd28192 Thorsten Wißmann
let coreGetStatus core = core.statusC
559
let coreSetStatus core status = core.statusC <- status
560
let coreGetParents core = core.parentsC
561
let coreAddParent core parent idx = core.parentsC <- (parent, idx)::core.parentsC
562
let coreGetChildren core = core.childrenC
563
let coreAddChild core child = core.childrenC <- child::core.childrenC
564
let coreGetConstraints core = core.constraintsC
565
let coreSetConstraints core csets = core.constraintsC <- csets
566
let coreGetSolver core = core.solver
567
let coreGetFht core = core.fht
568 73762b19 Thorsten Wißmann
let coreGetIdx (core:core) = core.idx
569 4fd28192 Thorsten Wißmann
let coreGetConstraintParents core = core.constraintParents
570
let coreAddConstraintParent core cset =
571
  core.constraintParents <- cset::core.constraintParents
572
573
574
(*****************************************************************************)
575
(*      "Module type" and a specific implementation of sets of               *)
576
(*      states, cores, and constraints for the sat propagation               *)
577
(*****************************************************************************)
578
579 d283bf7a Thorsten Wißmann
let setEmptyState () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
580
let setEmptyCore () = Array.init (Array.length !sortTable) (fun _ -> GHt.create 128)
581 16af388e Christoph Egger
let setEmptyCnstr () = GHtS.create 128
582
let setAddState set state =
583
  GHt.add set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state)) state
584
let setAddCore set core =
585
  GHt.add set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core)) core
586
let setAddCnstr set cset = GHtS.add set cset ()
587
let setMemState set state =
588
  GHt.mem set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
589
let setMemCore set core =
590
  GHt.mem set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
591
let setMemCnstr set cset = GHtS.mem set cset
592
let setRemoveState set state =
593
  GHt.remove set.(stateGetSort state) ((stateGetBs state), (stateGetDeferral state))
594
let setRemoveCore set core =
595
  GHt.remove set.(coreGetSort core) ((coreGetBs core), (coreGetDeferral core))
596
let setRemoveCnstr set cset = GHtS.remove set cset
597 d283bf7a Thorsten Wißmann
let setIterState fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
598
let setIterCore fkt set = Array.iter (fun ht -> GHt.iter (fun _ x -> fkt x) ht) set
599 16af388e Christoph Egger
let setIterCnstr fkt set = GHtS.iter (fun cset () -> fkt cset) set
600 50df1dc2 Christoph Egger
let setLengthState seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta
601
let setLengthCore seta = Array.fold_left (fun acc set -> acc + GHt.length set) 0 seta
602 4fd28192 Thorsten Wißmann
603
604
(*****************************************************************************)
605
(*        "Module type" and a specific implementation of the mapping         *)
606
(*        between (local) formulae and literals of the sat solver,           *)
607
(*        and of a mapping of nominals to sets of formulae                   *)
608
(*****************************************************************************)
609
610
let lhtInit () = LHt.create 16
611
let lhtAdd lht lit f = LHt.add lht lit f
612
let lhtFind lht lit =
613
  try
614
    Some (LHt.find lht lit)
615
  with Not_found -> None
616
617
let fhtInit () = FHt.create 16
618
let fhtAdd fht f lit = FHt.add fht f lit
619
let fhtFind fht f =
620
  try
621
    Some (FHt.find fht f)
622
  with Not_found -> None
623
624
let nhtInit () = NHt.create 8
625
let nhtAdd nht nom bs = NHt.add nht nom bs
626
let nhtFind nht nom =
627
  try
628
    Some (NHt.find nht nom)
629
  with Not_found -> None
630
let nhtFold fkt nht init = NHt.fold fkt nht init
631
632
(*****************************************************************************)
633
(*         "Module type" and a specific implementation of sets of            *)
634
(*         local formulae and @-formulae                                     *)
635
(*****************************************************************************)
636
637
let tboxTable = ref (Array.make 0 S.dummyBS)
638
639
let bsetMake () = S.makeBS ()
640
let bsetAdd bs lf = S.addBSNoChk bs lf
641
let bsetMem bs lf = S.memBS bs lf
642 b7445f7e Thorsten Wißmann
let bsetRem bs lf = S.remBS bs lf
643 16af388e Christoph Egger
let bsetCompare bs1 bs2 = S.compareBS bs1 bs2
644 45d554b0 Thorsten Wißmann
let bsetMakeRealEmpty () =
645
    let res = bsetMake () in
646
    bsetRem res !S.bstrue; (* remove bstrue which is initially in an empty bset *)
647
    res
648 b7c3a47e Thorsten Wißmann
let bsetCopy bs = S.copyBS bs
649 4fd28192 Thorsten Wißmann
let bsetFold fkt bs init = S.foldBS fkt bs init
650
let bsetIter fkt bset = S.iterBS fkt bset
651 e4cd869a Thorsten Wißmann
let bsetFilter (a: bset) (f: localFormula -> bool) : bset =
652 45d554b0 Thorsten Wißmann
    let res = bsetMakeRealEmpty () in
653 e4cd869a Thorsten Wißmann
    bsetIter (fun form -> if (f form) then bsetAdd res form else ()) a;
654
    res
655
656 4fd28192 Thorsten Wißmann
let bsetAddTBox sort bs = S.unionBSNoChk bs !tboxTable.(sort)
657
658
let csetCompare cs1 cs2 = S.compareBS cs1 cs2
659
let csetMake () = S.makeBS ()
660
let csetAdd cs lf = S.addBSNoChk cs lf
661
let csetCopy cs = S.copyBS cs
662
let csetUnion cs1 cs2 = S.unionBSNoChk cs1 cs2
663
let csetHasDot cs = S.memBS cs !S.bsfalse
664
let csetAddDot cs = S.addBSNoChk cs !S.bsfalse
665
let csetRemDot cs = S.remBS cs !S.bsfalse
666
let csetAddTBox sort cs = S.unionBSNoChk cs !tboxTable.(sort)
667
let csetIter cs fkt =
668
  let fkt2 f = if not (f = !S.bstrue || f = !S.bsfalse) then fkt f else () in
669
  S.iterBS fkt2 cs
670
671
672
(*****************************************************************************)
673
(*            "Module type" and a specific implementation of                 *)
674
(*            local formulae and @-formulae                                  *)
675
(*****************************************************************************)
676
677
(** This table maps integers (representing formulae) to their corresponding formulae.
678
 *)
679
let arrayFormula = ref (Array.make 0 (Array.make 0 C.TRUE))
680
681
(** This table maps integers (representing formulae) to their corresponding type.
682
 *)
683
let arrayType = ref (Array.make 0 (Array.make 0 Other))
684
685
(** This lookup table maps formulae (represented as integers)
686
    to their negation (in negation normal form).
687
 *)
688
let arrayNeg = ref (Array.make 0 (Array.make 0 (-1)))
689
690
(** These lookup tables map formulae (represented as integers)
691
    to their decompositions (represented as integers).
692
    This is done according to the rules of the tableau procedure
693
    and depends on the type of the formulae.
694
 *)
695 86b07be8 Thorsten Wißmann
 (*
696
    for PML: arrayDest1 = the subformula
697 eda515b6 Thorsten Wißmann
             arrayNum  = the nominator of the probability
698
             arrayNum2 = the denominator of the probability
699 86b07be8 Thorsten Wißmann
 *)
700 f1fa9ad5 Thorsten Wißmann
let arrayDest1 = ref (Array.make 0 (Array.make 0 (-1)))  (* first subformula *)
701
let arrayDest2 = ref (Array.make 0 (Array.make 0 (-1)))  (* second subformula *)
702
let arrayDest3 = ref (Array.make 0 (Array.make 0 (-1)))  (* a role *)
703 d9f4e4af Christoph Egger
let arrayDeferral = ref (Array.make 0 (Array.make 0 (-1)))  (* deferral at point *)
704 29b2e3f3 Thorsten Wißmann
let arrayDestNum = ref (Array.make 0 (Array.make 0 (-1)))  (* an integer *)
705 eda515b6 Thorsten Wißmann
let arrayDestNum2 = ref (Array.make 0 (Array.make 0 (-1)))  (* another integer *)
706 f1fa9ad5 Thorsten Wißmann
let arrayDestAg = ref (Array.make 0 (Array.make 0 [|0|])) (* arrays of agents *)
707 4fd28192 Thorsten Wißmann
708
(** This lookup table maps formulae (represented as integers)
709
    to their @-wrapper.
710
 *)
711
let arrayAt = ref (Array.make 0 (Array.make 0 (FHt.create 64)))
712
713
let lfGetType sort f = !arrayType.(sort).(f)
714
let lfGetDest1 sort f = !arrayDest1.(sort).(f)
715
let lfGetDest2 sort f = !arrayDest2.(sort).(f)
716
let lfGetDest3 sort f = !arrayDest3.(sort).(f)
717 c67aca42 Christoph Egger
let lfGetDeferral sort f = !arrayDeferral.(sort).(f)
718 29b2e3f3 Thorsten Wißmann
let lfGetDestNum sort f = !arrayDestNum.(sort).(f)
719 eda515b6 Thorsten Wißmann
let lfGetDestNum2 sort f = !arrayDestNum2.(sort).(f)
720 f1fa9ad5 Thorsten Wißmann
let lfGetDestAg sort f = !arrayDestAg.(sort).(f)
721 4fd28192 Thorsten Wißmann
let lfGetNeg sort f =
722
  let nf = !arrayNeg.(sort).(f) in
723
  if nf >= 0 then Some nf else None
724
let lfGetAt (sort, nom) f =
725
  FHt.find !arrayAt.(sort).(f) nom
726 a0cffef0 Thorsten Wißmann
let lfToInt lf = lf
727
let lfFromInt num = num
728 f335015f Thorsten Wißmann
let lfGetFormula sort f = !arrayFormula.(sort).(f)
729
730 de84f40d Christoph Egger
let escapeHtml (input : string) : string =
731
  List.fold_right (fun (x, y) (str : string) -> Str.global_replace (Str.regexp x) y str)
732
    [("<", "&lt;") ; (">", "&gt;") ; ("&", "&amp;")]
733
    input
734
735 f335015f Thorsten Wißmann
let bsetToString sort bset : string =
736
    let toFormula (lf:localFormula) (lst: string list) : string list =
737
        let formula: C.formula = lfGetFormula sort lf in
738
        (C.string_of_formula formula) :: lst
739
    in
740
    let formulaList = bsetFold toFormula bset [] in
741
    "{ "^(String.concat ", " formulaList)^" }"
742
743
let csetToString sort cset = bsetToString sort cset
744
745 8d6bf016 Christoph Egger
let coreToString (core:core): string =
746 f335015f Thorsten Wißmann
    let helper cset lst : string list =
747
        (csetToString core.sortC cset):: lst
748
    in
749
    let constraints = cssFold helper core.constraintsC [] in
750 488cea0f Thorsten Wißmann
    let children =
751
        List.map (fun (st:state) -> string_of_int st.idx) core.childrenC
752
    in
753 4164c8e1 Thorsten Wißmann
    let parents =
754
        List.map (fun (st,_:state*int) -> string_of_int st.idx) core.parentsC
755
    in
756 73762b19 Thorsten Wißmann
    "Core "^(string_of_int core.idx)^" {\n"^
757 f335015f Thorsten Wißmann
    "  Status: " ^ (nodeStatusToString core.statusC) ^ "\n"^
758
    "  " ^ bsetToString core.sortC core.bsC ^ "\n" ^
759 16af388e Christoph Egger
    "  Deferrals: \n" ^
760
    "    " ^ bsetToString core.sortC core.deferralC ^ "\n" ^
761 73762b19 Thorsten Wißmann
    "  Constraints: { "^(String.concat
762
                         "\n                 " constraints)^" }\n"^
763 488cea0f Thorsten Wißmann
    "  Children: { "^(String.concat
764
                         ", " children)^" }\n"^
765 4164c8e1 Thorsten Wißmann
    "  Parents: { "^(String.concat ", " parents)^" }\n"^
766 f335015f Thorsten Wißmann
    "}"
767 73762b19 Thorsten Wißmann
768
let stateToString (state:state): string =
769
    let helper cset lst : string list =
770
        (csetToString state.sortS cset):: lst
771
    in
772
    let constraints = cssFold helper state.constraintsS [] in
773
    let core2idx core = core.idx in
774
    let fst (a,b) = a in
775
    let conclusionList =
776
        List.map (fun (_,lst) ->
777
                  List.map (fun (core:core) -> string_of_int core.idx) lst
778
        ) state.childrenS
779
    in
780
    let conclusionList =
781
        List.map (fun x -> "{"^String.concat ", " x^"}") conclusionList
782
    in
783 4164c8e1 Thorsten Wißmann
    let parents =
784
        List.map (fun (co:core) -> string_of_int co.idx) state.parentsS
785
    in
786 73762b19 Thorsten Wißmann
    "State "^(string_of_int state.idx)^" {\n"^
787
    "  Status: " ^ (nodeStatusToString state.statusS) ^ "\n"^
788
    "  " ^ bsetToString state.sortS state.bsS ^ "\n" ^
789 16af388e Christoph Egger
    "  Deferrals: \n" ^
790
    "    " ^ bsetToString state.sortS state.deferralS ^ "\n" ^
791 73762b19 Thorsten Wißmann
    "  Constraints: { "^(String.concat
792
                         "\n                 " constraints)^" }\n"^
793
    "  Children: { "^(String.concat
794
                         "\n              " conclusionList)^" }\n"^
795 4164c8e1 Thorsten Wißmann
    "  Parents: { "^(String.concat ", " parents)^" }\n"^
796 73762b19 Thorsten Wißmann
    "}"
797
798 8d6bf016 Christoph Egger
let stateToDot (state:state): string =
799 c13029a3 Christoph Egger
  let color = match state.statusS with
800
    | Sat -> "green"
801
    | Unsat -> "red"
802
    | Open -> "yellow"
803
    | Expandable -> "white"
804
  in
805 de84f40d Christoph Egger
  let toFormula (lf:localFormula) (lst: string list) : string list =
806
    let formula: C.formula = lfGetFormula state.sortS lf in
807
    if (bsetMem state.deferralS lf)
808
    then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst
809
    else (escapeHtml (C.string_of_formula formula)) :: lst
810
  in
811
  let formulaList = bsetFold toFormula state.bsS [] in
812 8d6bf016 Christoph Egger
  let ownidx = (string_of_int state.idx) in
813
  let parents =
814 c13029a3 Christoph Egger
    List.map (fun (co:core) ->
815
              "Node"^string_of_int co.idx^" -> Node"^ownidx^";")
816 8d6bf016 Christoph Egger
             state.parentsS
817
  in
818 c13029a3 Christoph Egger
  "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
819 de84f40d Christoph Egger
  ^ ",label=<State "  ^ ownidx
820
  ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
821
  ^ ">];\n"
822 8d6bf016 Christoph Egger
  ^ (String.concat "\n" parents)
823
824
825
let coreToDot (core:core): string =
826 c13029a3 Christoph Egger
  let color = match core.statusC with
827
    | Sat -> "green"
828
    | Unsat -> "red"
829
    | Open -> "yellow"
830
    | Expandable -> "white"
831
  in
832 de84f40d Christoph Egger
  let toFormula (lf:localFormula) (lst: string list) : string list =
833
    let formula: C.formula = lfGetFormula core.sortC lf in
834
    if (bsetMem core.deferralC lf)
835
    then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst
836
    else (escapeHtml (C.string_of_formula formula)) :: lst
837
  in
838
  let formulaList = bsetFold toFormula core.bsC [] in
839 8d6bf016 Christoph Egger
  let ownidx = (string_of_int core.idx) in
840
  let parents =
841 c13029a3 Christoph Egger
    List.map (fun (st,_:state*int) ->
842
              "Node"^string_of_int st.idx^" -> Node"^ownidx^";")
843 8d6bf016 Christoph Egger
             core.parentsC
844
  in
845 c13029a3 Christoph Egger
  "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
846 de84f40d Christoph Egger
  ^ ",label=<Core "  ^ ownidx
847
  ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
848
  ^ ">];\n"
849 8d6bf016 Christoph Egger
  ^ (String.concat "\n" parents)
850
851
852 488cea0f Thorsten Wißmann
let queuePrettyStatus () =
853
  let printList (sl : int list) : string =
854
    String.concat ", " (List.map string_of_int sl)
855
  in
856
  (* TODO: are atFormulas always look-up-able for sort 0? *)
857
  (Printf.sprintf "%d Constraints: " (List.length !queueCnstrs))
858
  ^(String.concat ", " (List.map (csetToString 0) !queueCnstrs))
859
  ^(Printf.sprintf "\n%d States: " (List.length !queueStates))
860
  ^(printList (List.map (fun (st:state) -> st.idx) !queueStates))
861
  ^(Printf.sprintf "\n%d Cores1: " (List.length !queueCores1))
862
  ^(printList (List.map (fun (co:core) -> co.idx) !queueCores1))
863
  ^(Printf.sprintf "\n%d Cores2: " (List.length !queueCores2))
864
  ^(printList (List.map (fun (co:core) -> co.idx) !queueCores2))
865
  ^"\n"
866
867 73762b19 Thorsten Wißmann
868
869 4fd28192 Thorsten Wißmann
870
let atFormulaGetSubformula f = !arrayDest1.(0).(f)
871
let atFormulaGetNominal f =
872
  let s = !arrayDest3.(0).(f) in
873
  let n = !arrayDest2.(0).(f) in
874
  (s, n)
875
876
let lfToAt _ lf = lf
877
878 4b0d0388 Christoph Egger
(* Calculate all possible formulae. This includes all subformulae and
879
   in the case of μ-Calculus the Fischer-Ladner closure.
880 4fd28192 Thorsten Wißmann
881 4b0d0388 Christoph Egger
   TODO: variable sort needs to match epected sort
882
 *)
883 cb12f8a5 Christoph Egger
let rec detClosure vars nomTbl hcF fset vset atset nomset s f =
884
  let newvars = List.filter (fun (x) -> C.hc_freeIn x f) vars in
885
  let detClosure_ = detClosure newvars in
886
  let deferral = if List.length newvars > 0
887
                 then (List.hd newvars)
888
                 else "ε" in
889 4fd28192 Thorsten Wißmann
  if s < 0 || s >= Array.length fset then
890
    let sstr = string_of_int s in
891
    raise (C.CoAlgException ("Invalid sort (i.e. sort out of range): " ^ sstr))
892
  else ();
893 653eaa4b Christoph Egger
  if C.HcFHt.mem vset.(s) f &&
894
       compare (C.HcFHt.find vset.(s) f) deferral = 0 then ()
895 4fd28192 Thorsten Wißmann
  else
896 cb12f8a5 Christoph Egger
    let () = C.HcFHt.add vset.(s) f deferral in
897 4fd28192 Thorsten Wißmann
    let () = C.HcFHt.add fset.(s) f () in
898
    let (func, sortlst) = !sortTable.(s) in
899
    match f.HC.node with
900
    | C.HCTRUE
901 43194ed2 Christoph Egger
    | C.HCFALSE
902
    | C.HCVAR _ -> ()
903 4fd28192 Thorsten Wißmann
    | C.HCAP name ->
904
        if C.isNominal name then begin
905
          Hashtbl.replace nomset name s;
906
          match nomTbl name with
907
          | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name))
908
          | Some sort ->
909
              if sort <> s then
910
                let str1 = "Nominal: " ^ name ^ " of sort " ^ (string_of_int sort) in
911
                let str2 = " is used in sort " ^ (string_of_int s) ^ "." in
912
                raise (C.CoAlgException (str1 ^ str2))
913
              else ()
914
        end else ()
915
    | C.HCNOT _ -> ()
916
    | C.HCAT (name, f1) ->
917
        C.HcFHt.replace atset f ();
918
        let s1 =
919
          match nomTbl name with
920
          | None -> raise (C.CoAlgException ("Unknown nominal: " ^ name))
921
          | Some sort -> sort
922
        in
923
        let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
924 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset s1 hcnom;
925
        detClosure_ nomTbl hcF fset vset atset nomset s1 f1
926 4fd28192 Thorsten Wißmann
    | C.HCOR (f1, f2)
927
    | C.HCAND (f1, f2) ->
928 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset s f1;
929
        detClosure_ nomTbl hcF fset vset atset nomset s f2
930 4fd28192 Thorsten Wißmann
    | C.HCEX (_, f1)
931
    | C.HCAX (_, f1) ->
932 2a84977e Thorsten Wißmann
        if (func <> MultiModalK && func <> MultiModalKD)
933
            || List.length sortlst <> 1
934
        then raise (C.CoAlgException "Ex/Ax-formula is used in wrong sort.")
935 4fd28192 Thorsten Wißmann
        else ();
936 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
937 f1fa9ad5 Thorsten Wißmann
    | C.HCENFORCES (_, f1)
938
    | C.HCALLOWS (_, f1) ->
939
        if func <> CoalitionLogic || List.length sortlst <> 1
940
        then raise (C.CoAlgException "[{Agents}]-formula is used in wrong sort.")
941
        else ();
942 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
943 af276a36 Thorsten Wißmann
    | C.HCMORETHAN (_,_,f1)
944
    | C.HCMAXEXCEPT (_,_,f1) ->
945 29b2e3f3 Thorsten Wißmann
        if func <> GML || List.length sortlst <> 1
946
        then raise (C.CoAlgException "[{>=,<=}]-formula is used in wrong sort.")
947
        else ();
948 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1
949 86b07be8 Thorsten Wißmann
    | C.HCATLEASTPROB (_,f1)
950 9bae2c4f Thorsten Wißmann
    | C.HCLESSPROBFAIL (_,f1) ->
951 86b07be8 Thorsten Wißmann
        if func <> PML || List.length sortlst <> 1
952 c855ba91 Thorsten Wißmann
        then raise (C.CoAlgException "[{>=,<}]-formula with probability is used in wrong sort.")
953 86b07be8 Thorsten Wißmann
        else ();
954 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1;
955 9bae2c4f Thorsten Wißmann
        (*
956
            TODO: add ¬ f1 to the closure!
957
        detClosure nomTbl hcF fset atset nomset (List.hd sortlst) (f1.HC.node.negNde)
958
        *)
959 5e0983fe Thorsten Wißmann
    | C.HCCONST color
960
    | C.HCCONSTN color ->
961
      begin match func with
962
      | Constant params ->
963
            if not (List.exists ((=) color) params)
964
            then raise (C.CoAlgException ("=-formula mentions \""^color^"\" but the only"
965
                             ^" choices are: "^(String.concat ", " params)))
966
      | _ -> raise (C.CoAlgException "=-formula is used in wrong sort.")
967
      end;
968
      if List.length sortlst <> 1
969 c49eea11 Thorsten Wißmann
        then raise (C.CoAlgException "=-formula is used in wrong sort.")
970
        else ();
971
      (* NB: =-formulae have no subformlae hence no closure *)
972 19f5dad0 Dirk Pattinson
    | C.HCID f1 ->
973
        if func <> Identity || List.length sortlst <> 1
974
        then raise (C.CoAlgException "Identity operator applied to
975
          formula of wrong sort.")
976
        else ();
977 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.hd sortlst) f1;
978 19f5dad0 Dirk Pattinson
    | C.HCNORM (f1, f2)
979
    | C.HCNORMN(f1, f2) ->
980
      if func <> DefaultImplication || List.length sortlst <> 1 then
981
          raise (C.CoAlgException "Default Implication applied to
982
          formulae of wrong sort.")
983
        else ();
984 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 0) f1;
985
        detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 1) f2
986 19f5dad0 Dirk Pattinson
987 d58bba0f Dirk Pattinson
    | C.HCCHC (f1, f2) ->
988 4fd28192 Thorsten Wißmann
        if func <> Choice || List.length sortlst <> 2 then
989
          raise (C.CoAlgException "Choice formula is used in wrong sort.")
990
        else ();
991 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 0) f1;
992
        detClosure_ nomTbl hcF fset vset atset nomset (List.nth sortlst 1) f2
993 4fd28192 Thorsten Wißmann
    | C.HCFUS (first, f1) ->
994
        if func <> Fusion || List.length sortlst <> 2 then
995
          raise (C.CoAlgException "Fusion formula is used in wrong sort.")
996
        else ();
997
        let s1 = List.nth sortlst (if first then 0 else 1) in
998 cb12f8a5 Christoph Egger
        detClosure_ nomTbl hcF fset vset atset nomset s1 f1
999 034a8dea Christoph Egger
    (*
1000 6553983f Christoph Egger
       FL(μ X . φ) = {μ X . φ} ∪ FL(φ[X|->μ X . φ])
1001 034a8dea Christoph Egger
     *)
1002
    | C.HCMU (name, f1) ->
1003 cb12f8a5 Christoph Egger
       let () = C.HcFHt.replace vset.(s) f name in
1004 034a8dea Christoph Egger
       let unfold = C.hc_replace hcF name f f1 in
1005 cb12f8a5 Christoph Egger
       let appendvars = List.append newvars [name] in
1006
       detClosure appendvars nomTbl hcF fset vset atset nomset s unfold
1007 034a8dea Christoph Egger
    | C.HCNU (name, f1) ->
1008
       let unfold = C.hc_replace hcF name f f1 in
1009 cb12f8a5 Christoph Egger
       detClosure_ nomTbl hcF fset vset atset nomset s unfold
1010 6553983f Christoph Egger
1011 4fd28192 Thorsten Wißmann
1012
let detClosureAt hcF atset name f () =
1013
  match f.HC.node with
1014
  | C.HCTRUE
1015
  | C.HCFALSE
1016
  | C.HCOR _
1017
  | C.HCAND _
1018
  | C.HCAT _ -> ()
1019
  | _ ->
1020 034a8dea Christoph Egger
      let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
1021 4fd28192 Thorsten Wißmann
      C.HcFHt.replace atset at ()
1022
1023
(** Initialises the arrays for a formula and its integer representation.
1024
 *)
1025 d9f4e4af Christoph Egger
let initTables nomTbl hcF htF htR vset s f n =
1026 4fd28192 Thorsten Wißmann
  !arrayFormula.(s).(n) <- f.HC.fml;
1027 d9f4e4af Christoph Egger
  !arrayDeferral.(s).(n) <- Hashtbl.hash (C.HcFHt.find vset.(s) f);
1028 4fd28192 Thorsten Wißmann
  let fneg = f.HC.neg in
1029
  if C.HcFHt.mem htF.(s) fneg then !arrayNeg.(s).(n) <- C.HcFHt.find htF.(s) fneg;
1030
  let (_, sortlst) = !sortTable.(s) in
1031
  match f.HC.node with
1032
  | C.HCTRUE
1033 3b055ae8 dirk
  | C.HCFALSE -> !arrayType.(s).(n) <- TrueFalseF
1034 4fd28192 Thorsten Wißmann
  | C.HCAP name ->
1035
      if C.isNominal name then !arrayType.(s).(n) <- NomF
1036
      else !arrayType.(s).(n) <- Other
1037
  | C.HCNOT _ -> !arrayType.(s).(n) <- Other
1038
  | C.HCAT (name, f1) ->
1039
      !arrayType.(s).(n) <- AtF;
1040
      let s1 =
1041
        match nomTbl name with
1042
        | None -> assert false
1043
        | Some sort -> sort
1044
      in
1045
      let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
1046
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s1) f1;
1047
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s1) hcnom;
1048
      !arrayDest3.(s).(n) <- s1
1049
  | C.HCOR (f1, f2) ->
1050
      !arrayType.(s).(n) <- OrF;
1051
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) f1;
1052
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s) f2
1053
  | C.HCAND (f1, f2) ->
1054
      !arrayType.(s).(n) <- AndF;
1055
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) f1;
1056
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s) f2
1057 034a8dea Christoph Egger
  | C.HCEX (role, f1) ->
1058 4fd28192 Thorsten Wißmann
      !arrayType.(s).(n) <- ExF;
1059
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1060 034a8dea Christoph Egger
      !arrayDest3.(s).(n) <-
1061 4fd28192 Thorsten Wißmann
        if Hashtbl.mem htR role then Hashtbl.find htR role
1062
        else
1063
          let size = Hashtbl.length htR in
1064
          Hashtbl.add htR role size;
1065
          size
1066
  | C.HCAX (role, f1) ->
1067
      !arrayType.(s).(n) <- AxF;
1068
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1069
      !arrayDest3.(s).(n) <-
1070
        if Hashtbl.mem htR role then Hashtbl.find htR role
1071
        else
1072
          let size = Hashtbl.length htR in
1073
          Hashtbl.add htR role size;
1074
          size
1075 f1fa9ad5 Thorsten Wißmann
  | C.HCENFORCES (aglist, f1) ->  (* aglist = list of agents *)
1076
      !arrayType.(s).(n) <- EnforcesF;
1077
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1078
      !arrayDestAg.(s).(n) <- Array.of_list aglist
1079
  | C.HCALLOWS (aglist, f1) ->  (* aglist = list of agents *)
1080
      !arrayType.(s).(n) <- AllowsF;
1081
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1082
      !arrayDestAg.(s).(n) <- Array.of_list aglist
1083 af276a36 Thorsten Wißmann
  | C.HCMORETHAN (cnt,role,f1) ->
1084
      !arrayType.(s).(n) <- MoreThanF;
1085 29b2e3f3 Thorsten Wißmann
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1086
      !arrayDestNum.(s).(n) <- cnt;
1087
      !arrayDest3.(s).(n) <-
1088
        if Hashtbl.mem htR role then Hashtbl.find htR role
1089
        else
1090
          let size = Hashtbl.length htR in
1091
          Hashtbl.add htR role size;
1092
          size
1093 af276a36 Thorsten Wißmann
  | C.HCMAXEXCEPT (cnt,role,f1) ->
1094
      !arrayType.(s).(n) <- MaxExceptF;
1095 29b2e3f3 Thorsten Wißmann
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1096
      !arrayDestNum.(s).(n) <- cnt;
1097
      !arrayDest3.(s).(n) <-
1098
        if Hashtbl.mem htR role then Hashtbl.find htR role
1099
        else
1100
          let size = Hashtbl.length htR in
1101
          Hashtbl.add htR role size;
1102
          size
1103 86b07be8 Thorsten Wißmann
  | C.HCATLEASTPROB (p,f1) ->
1104
      !arrayType.(s).(n) <- AtLeastProbF;
1105
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1106 eda515b6 Thorsten Wißmann
      !arrayDestNum.(s).(n) <- p.C.nominator;
1107
      !arrayDestNum2.(s).(n) <- p.C.denominator
1108 9bae2c4f Thorsten Wißmann
  | C.HCLESSPROBFAIL (p,f1) ->
1109
      !arrayType.(s).(n) <- LessProbFailF;
1110 86b07be8 Thorsten Wißmann
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
1111 eda515b6 Thorsten Wißmann
      !arrayDestNum.(s).(n) <- p.C.nominator;
1112
      !arrayDestNum2.(s).(n) <- p.C.denominator
1113 c49eea11 Thorsten Wißmann
  | C.HCCONST str ->
1114
      !arrayType.(s).(n) <- ConstF; (* type of modality *)
1115
      (* Dest1 and Dest2 are the arguments, here: none *)
1116
      (* DestNum and DestNum2 are the numerators and denonimators of
1117
      fractions, here: none *)
1118
      !arrayDest3.(s).(n) <-
1119
        if Hashtbl.mem htR str then Hashtbl.find htR str
1120
        else
1121
          let size = Hashtbl.length htR in
1122
          Hashtbl.add htR str size;
1123
          size
1124
      (* Dest3 are the role names / identifiers for constant values *)
1125
      (* idea: hash identifier names *)
1126
  | C.HCCONSTN str ->
1127
      !arrayType.(s).(n) <- ConstnF; (* type of modality *)
1128
      (* Dest1 and Dest2 are the arguments, here: none *)
1129
      (* DestNum and DestNum2 are the numerators and denonimators of
1130
      fractions, here: none *)
1131
      !arrayDest3.(s).(n) <-
1132
        if Hashtbl.mem htR str then Hashtbl.find htR str
1133
        else
1134
          let size = Hashtbl.length htR in
1135
          Hashtbl.add htR str size;
1136
          size
1137
      (* Dest3 are the role names / identifiers for constant values *)
1138
      (* idea: hash identifier names *)
1139 19f5dad0 Dirk Pattinson
  | C.HCID (f1) ->
1140
      !arrayType.(s).(n) <- IdF;
1141 d58bba0f Dirk Pattinson
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1
1142 034a8dea Christoph Egger
  | C.HCNORM (f1, f2) ->
1143 19f5dad0 Dirk Pattinson
      !arrayType.(s).(n) <- NormF;
1144
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
1145
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2
1146 034a8dea Christoph Egger
  | C.HCNORMN (f1, f2) ->
1147 19f5dad0 Dirk Pattinson
      !arrayType.(s).(n) <- NormnF;
1148
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
1149
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2
1150
  (* note that choice is self-dual *)
1151 d58bba0f Dirk Pattinson
  | C.HCCHC (f1, f2) ->
1152 4fd28192 Thorsten Wißmann
      !arrayType.(s).(n) <- ChcF;
1153
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
1154
      !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2
1155
  | C.HCFUS (first, f1) ->
1156
      !arrayType.(s).(n) <- FusF;
1157
      let s1 = List.nth sortlst (if first then 0 else 1) in
1158
      !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s1) f1;
1159
      !arrayDest3.(s).(n) <- if first then 0 else 1
1160 5ec97220 Christoph Egger
  | C.HCMU (name, f1) ->
1161
     !arrayType.(s).(n) <- MuF;
1162 034a8dea Christoph Egger
     let unfold = C.hc_replace hcF name f f1 in
1163
     !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold
1164 5ec97220 Christoph Egger
  | C.HCNU (name, f1) ->
1165 034a8dea Christoph Egger
     !arrayType.(s).(n) <- NuF;
1166
     let unfold = C.hc_replace hcF name f f1 in
1167
     !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold
1168 5ec97220 Christoph Egger
  | C.HCVAR _ -> !arrayType.(s).(n) <- Other
1169
1170 4fd28192 Thorsten Wißmann
1171
let initTablesAt hcF htF name sort =
1172
  let hcnom = C.HcFormula.hashcons hcF (C.HCAP name) in
1173
  let nom = C.HcFHt.find htF.(sort) hcnom in
1174
  let addAt f n =
1175
    match f.HC.node with
1176
    | C.HCTRUE
1177
    | C.HCFALSE
1178
    | C.HCOR _
1179
    | C.HCAND _
1180
    | C.HCAT _ -> ()
1181
    | _ ->
1182 034a8dea Christoph Egger
        let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
1183 4fd28192 Thorsten Wißmann
        let atn = C.HcFHt.find htF.(0) at in
1184
        FHt.add !arrayAt.(sort).(n) nom atn
1185
  in
1186
  C.HcFHt.iter addAt htF.(sort)
1187
1188
let ppFormulae nomTbl tbox (s, f) =
1189
  let card = Array.length !sortTable in
1190
  if card <= 0 then
1191
    raise (C.CoAlgException "Number of sorts must be positive.")
1192
  else ();
1193
  let nnfAndSimplify f = C.simplify (C.nnf f) in
1194 f828ad2f Thorsten Wißmann
  let  f1    = nnfAndSimplify f in
1195
  let nf1    = nnfAndSimplify (C.NOT f) in
1196
  let  tbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify f)) tbox in
1197
  let ntbox1 = List.map (fun (s, f) -> (s, nnfAndSimplify (C.NOT f))) tbox in
1198
1199
  let hcF     =  C.HcFormula.create true in
1200
  let  hcf    = C.hc_formula hcF  f1 in
1201
  let nhcf    = C.hc_formula hcF nf1 in
1202
  let  hctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f))  tbox1 in
1203
  let nhctbox = List.map (fun (s, f) -> (s, C.hc_formula hcF f)) ntbox1 in
1204 4fd28192 Thorsten Wißmann
  let hcfalse = C.hc_formula hcF C.FALSE in
1205 f828ad2f Thorsten Wißmann
  let hctrue  = C.hc_formula hcF C.TRUE in
1206 4fd28192 Thorsten Wißmann
1207
  let fset = Array.init card (fun _ -> C.HcFHt.create 128) in
1208 cb12f8a5 Christoph Egger
  let vset = Array.init card (fun _ -> C.HcFHt.create 128) in
1209 4fd28192 Thorsten Wißmann
  let atset = C.HcFHt.create 64 in
1210
  let nomset = Hashtbl.create 16 in
1211
  for i = 0 to card-1 do
1212 cb12f8a5 Christoph Egger
    detClosure [] nomTbl hcF fset vset atset nomset i hcfalse;
1213
    detClosure [] nomTbl hcF fset vset atset nomset i hctrue;
1214 4fd28192 Thorsten Wißmann
  done;
1215 cb12f8a5 Christoph Egger
  detClosure [] nomTbl hcF fset vset atset nomset s  hcf;
1216
  detClosure [] nomTbl hcF fset vset atset nomset s nhcf;
1217
  List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f)
1218
            hctbox;
1219
  List.iter (fun (s, f) -> detClosure [] nomTbl hcF fset vset atset nomset s f)
1220
            nhctbox;
1221 4fd28192 Thorsten Wißmann
  Hashtbl.iter (fun n s -> C.HcFHt.iter (detClosureAt hcF atset n) fset.(s)) nomset;
1222
1223
  let htF = Array.init card (fun _ -> C.HcFHt.create 128) in
1224
  for i = 0 to card-1 do
1225
    C.HcFHt.add htF.(i) hcfalse 0;
1226
    C.HcFHt.add htF.(i) hctrue 1
1227
  done;
1228
  let addAts f () idx =
1229
    for i = 0 to card-1 do
1230
      C.HcFHt.add htF.(i) f idx
1231
    done;
1232
    idx + 1
1233
  in
1234
  let sizeAt = C.HcFHt.fold addAts atset 2 in
1235
  let addFml i f () idx =
1236
    if C.HcFHt.mem htF.(i) f then idx
1237
    else begin
1238
      C.HcFHt.add htF.(i) f idx;
1239
      idx+1
1240
    end
1241
  in
1242
  let size = ref 0 in
1243
  for i = 0 to card-1 do
1244
    let size2 = C.HcFHt.fold (addFml i) fset.(i) sizeAt in
1245
    if size2 > !size then size := size2 else ()
1246
  done;
1247
1248
  arrayFormula := Array.init card (fun _ -> Array.make !size C.TRUE);
1249
  arrayType := Array.init card (fun _ -> Array.make !size Other);
1250
  arrayDest1 := Array.init card (fun _ -> Array.make !size (-1));
1251
  arrayDest2 := Array.init card (fun _ -> Array.make !size (-1));
1252
  arrayDest3 := Array.init card (fun _ -> Array.make !size (-1));
1253 d9f4e4af Christoph Egger
  arrayDeferral := Array.init card (fun _-> Array.make !size(-1));
1254 4fd28192 Thorsten Wißmann
  arrayNeg := Array.init card (fun _ -> Array.make !size (-1));
1255 29b2e3f3 Thorsten Wißmann
  arrayDestNum := Array.init card (fun _ -> Array.make !size (-1));
1256 eda515b6 Thorsten Wißmann
  arrayDestNum2 := Array.init card (fun _ -> Array.make !size (-1));
1257 98af95fb Thorsten Wißmann
  arrayDestAg := Array.init card (fun _ -> Array.make !size (Array.make 0 (-1)));
1258 4fd28192 Thorsten Wißmann
  let htR = Hashtbl.create 128 in
1259 d9f4e4af Christoph Egger
  Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR vset s) ht) htF;
1260 4fd28192 Thorsten Wißmann
  arrayAt := Array.init card (fun _ -> Array.init !size (fun _ -> FHt.create 8));
1261
  Hashtbl.iter (initTablesAt hcF htF) nomset;
1262
1263
  S.initMisc !size (C.HcFHt.find htF.(0) hcfalse) (C.HcFHt.find htF.(0) hctrue) (-1) (-1) (-1);
1264
  let initbs = bsetMake () in
1265
  bsetAdd initbs (C.HcFHt.find htF.(s) hcf);
1266
  let tboxTbl = Array.init card (fun _ -> bsetMake ()) in
1267
  List.iter (fun (s, f) -> bsetAdd tboxTbl.(s) (C.HcFHt.find htF.(s) f)) hctbox;
1268
  tboxTable := tboxTbl;
1269
  (tbox1, (s, f1), initbs)