Project

General

Profile

Statistics
| Branch: | Revision:

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

History | View | Annotate | Download (22.7 KB)

1
(** The "plug-in" functions for each individual logic.
2
    @author Florian Widmann
3
 *)
4

    
5

    
6
open CoAlgMisc
7
open CoolUtils
8
open CoAlgLogicUtils
9
open Gmlmip
10

    
11
module S = MiscSolver
12

    
13
(** directly return a list of rules **)
14
let mkRuleList_MultiModalK sort bs defer sl : rule list =
15
  (* arguments:
16
    sort: type of formulae in bs (needed to disambiguate hashing)
17
    sl: sorts functor arguments, e.g. type of argument formulae
18
    bs: tableau sequent  consisting of modal atoms
19
        (premiss, conjunctive set of formulae represented by hash values)
20
    result: set R of (propagation function, rule conclusion) pairs
21
        s.t. [ (premiss / conc) : (_, conc) \in R ] are all rules
22
        applicable to premiss.
23
        Propagation functions map unsatisfiable subsets of the
24
        (union of all?) conclusion(s) to unsatisfiable subsets of
25
        the premiss -- this is a hook for backjumping.
26
        NB: propagating the whole premiss is always safe.
27
  *)
28
  assert (List.length sl = 1);
29
  let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
30
  let dep f bsl =                 (* dependencies for formula f (f is a diamond) *)
31
    assert (List.length bsl = 1); (* -+                 *)
32
    let bs1 = List.hd bsl in      (* -+-> [bs1] := bsl  *)
33
    let res = bsetMake () in
34
    bsetAdd res f;
35
    let (role : int) = lfGetDest3 sort f in (* ♥R.? := f, ♥ ∈ {∃,∀} *)
36
    let filterFkt f1 =
37
      if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role
38
        && bsetMem bs1 (lfGetDest1 sort f1)
39
      then
40
        (* if f1 = ∀R.C and C ∈ bs1 then res = res ∪ {∀R.C} *)
41
        bsetAdd res f1
42
      else ()
43
    in
44
    bsetIter filterFkt bs;
45
    res
46
  in
47
  let getRules f acc =
48
    if lfGetType sort f = ExF then (* f = ∃R.C,i.e. a diamond *)
49
      let bs1 = bsetMake () in
50
      let defer1 = bsetMakeRealEmpty () in
51
      let nextf = (lfGetDest1 sort f) in
52
      bsetAdd bs1 nextf; (* bs1 := { C }          *)
53
      if (refocusing && (lfGetDeferral sort nextf) != (Hashtbl.hash "ε")) ||
54
           ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf))
55
      then
56
        bsetAdd defer1 nextf;
57
      let (role : int) = lfGetDest3 sort f in (* role := R *)
58
      let filterFkt f1 =
59
        if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role then
60
          (* if f1 = ∀R.D then bs1 = bs1 ∪ { D } *)
61
          let nextf1 = (lfGetDest1 sort f1) in
62
          bsetAdd bs1 nextf1;
63
          (if (refocusing && (lfGetDeferral sort nextf1) != (Hashtbl.hash "ε")) ||
64
              ((bsetMem defer f1) && (lfGetDeferral sort f1) = (lfGetDeferral sort nextf1)) then
65
             bsetAdd defer1 nextf1;)
66
        else ()
67
      in
68
      bsetIter filterFkt bs; (* bs1 := bs1 ∪ { D | some "∀R.D" ∈ bs } *)
69
      let s1 = List.hd sl in (* [s1] := sl *)
70
      let rle = (dep f, lazylistFromList [(s1, bs1, defer1)]) in
71
      rle::acc
72
    else acc
73
  in
74
  (* effectively:
75
        mkRule_MultiModalK sort bs [s1]
76
            = { ( λ[bs1]. { ∃R.C } ∪ { ∀R.D
77
                                     | ∀R.D ∈ bs, D ∈ bs1
78
                                     }
79
                , [(s1, {C}∪{D | "∀R.D" ∈ bs)]
80
                )
81
              | "∃R.C" ∈ bs
82
              }
83
  *)
84
  bsetFold getRules bs []
85

    
86
let mkRule_MultiModalK sort bs defer sl : stateExpander =
87
  let rules = mkRuleList_MultiModalK sort bs defer sl in
88
  lazylistFromList rules
89

    
90
(* TODO: test it with:
91
     make && ./coalg sat <<< $'<R> False \n [R] False \n [R] True'
92
*)
93
let mkRule_MultiModalKD sort bs defer sl : stateExpander =
94
  assert (List.length sl = 1); (* functor has just one argument *)
95
  let s1 = List.hd sl in (* [s1] = sl *)
96
  let roles = S.makeBS () in
97
  (* step 1: for each ∀R._ add R *)
98
  let addRoleIfBox formula =
99
    if lfGetType sort formula = AxF then
100
      ignore (S.addBSNoChk roles (lfGetDest3 sort formula))
101
    else ()
102
  in
103
  bsetIter (addRoleIfBox) bs;
104
  (* step 2: for each ∃R._ remove R again from roles (optimization) *)
105
  let rmRoleIfDiamond formula =
106
    if lfGetType sort formula = ExF then
107
      S.remBS roles (lfGetDest3 sort formula)
108
    else ()
109
  in
110
  bsetIter (rmRoleIfDiamond) bs;
111
  (* step 3: for each R in roles enforce one successor *)
112
  let getRules r acc = (* add the rule for a concrete R *)
113
    let dep r bsl =
114
      assert (List.length bsl = 1); (* -+                 *)
115
      let bs1 = List.hd bsl in      (* -+-> [bs1] := bsl  *)
116
      let res = bsetMake () in (* res := { ∀R.D ∈ bs | D ∈ bs1} *)
117
      let f formula =
118
        if lfGetType sort formula = AxF
119
           && lfGetDest3 sort formula = r
120
           && bsetMem bs1 (lfGetDest1 sort formula)
121
        then ignore (bsetAdd res formula)
122
        else ()
123
      in
124
      bsetIter f bs; (* fill res *)
125
      res
126
    in
127
    let succs = bsetMake () in (* succs := {D | ∀r.D ∈ bs *)
128
    let defer1 = bsetMakeRealEmpty () in (* TODO: actually track deferrals *)
129
    let f formula =
130
      if lfGetType sort formula = AxF
131
         && lfGetDest3 sort formula = r
132
      then
133
          let nextf1 = (lfGetDest1 sort formula) in
134
          bsetAdd succs nextf1;
135
          ignore (if (bsetMem defer formula) &&
136
                       (lfGetDeferral sort formula) = (lfGetDeferral sort nextf1)
137
                  then
138
                    bsetAdd defer1 nextf1;)
139
      else ()
140
    in
141
    bsetIter f bs;
142
    (dep r, lazylistFromList [(s1, succs, defer1)])::acc
143
  in
144
  (*
145
    mkRule_MultiModalKD sort bs [s1]
146
        = { (λ[bs1]. { ∀R.D ∈ bs | D ∈ bs1}
147
            , [(s1, {D | "∀R.D" ∈ bs)]
148
            )
149
          | R ∈ signature(bs) (or R ∈ roles)
150
          }
151
          ∪ mkRule_MultiModalK sort bs [s1]
152
  *)
153
  let rules = mkRuleList_MultiModalK sort bs defer sl in
154
  (* extend rules from K with enforcing of successors *)
155
  let rules = S.foldBS getRules roles rules in
156
  lazylistFromList rules
157

    
158

    
159
(** directly return a list of rules **)
160
let mkRuleList_Monotone sort bs defer sl : rule list =
161
  (* arguments:
162
    sort: type of formulae in bs (needed to disambiguate hashing)
163
    sl: sorts functor arguments, e.g. type of argument formulae
164
    bs: tableau sequent  consisting of modal atoms
165
        (premiss, conjunctive set of formulae represented by hash values)
166
    result: set R of (propagation function, rule conclusion) pairs
167
        s.t. [ (premiss / conc) : (_, conc) \in R ] are all rules
168
        applicable to premiss.
169
        Propagation functions map unsatisfiable subsets of the
170
        (union of all?) conclusion(s) to unsatisfiable subsets of
171
        the premiss -- this is a hook for backjumping.
172
        NB: propagating the whole premiss is always safe.
173
  *)
174
  assert (List.length sl = 1);
175
  let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
176
  let dep f bsl =                 (* dependencies for formula f (f is a diamond) *)
177
    assert (List.length bsl = 1); (* -+                 *)
178
    let bs1 = List.hd bsl in      (* -+-> [bs1] := bsl  *)
179
    let res = bsetMake () in
180
    bsetAdd res f;
181
    let (role : int) = lfGetDest3 sort f in (* ♥R.? := f, ♥ ∈ {∃,∀} *)
182
    let filterFkt f1 =
183
      if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role
184
        && bsetMem bs1 (lfGetDest1 sort f1)
185
      then
186
        (* if f1 = ∀R.C and C ∈ bs1 then res = res ∪ {∀R.C} *)
187
        bsetAdd res f1
188
      else ()
189
    in
190
    bsetIter filterFkt bs;
191
    res
192
  in
193
  let getRules f acc =
194
    if lfGetType sort f = ExF then (* f = ∃R.C,i.e. a diamond *)
195
      let bs1base = bsetMake () in
196
      let defer1base = bsetMakeRealEmpty () in
197
      let nextf = (lfGetDest1 sort f) in
198
      bsetAdd bs1base nextf; (* bs1 := { C }          *)
199
      if (refocusing && (lfGetDeferral sort nextf) != (Hashtbl.hash "ε")) ||
200
           ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf))
201
      then
202
        bsetAdd defer1base nextf
203
      else ();
204
      let (role : int) = lfGetDest3 sort f in (* role := R *)
205
      let filterFkt f1 acc =
206
        if lfGetType sort f1 = AxF && lfGetDest3 sort f1 = role then
207
          let bs1 = bsetCopy bs1base in
208
          let defer1 = bsetCopy defer1base in
209
          (* if f1 = ∀R.D then bs1 = bs1 ∪ { D } *)
210
          let nextf1 = (lfGetDest1 sort f1) in
211
          bsetAdd bs1 nextf1;
212
          if (refocusing && (lfGetDeferral sort nextf1) != (Hashtbl.hash "ε")) ||
213
               ((bsetMem defer f1) && (lfGetDeferral sort f1) = (lfGetDeferral sort nextf1))
214
          then
215
            bsetAdd defer1 nextf1
216
          else ();
217
          let s1 = List.hd sl in (* [s1] := sl *)
218
          let rle1 = (dep f, lazylistFromList [(s1, bs1, defer1)]) in
219
          rle1::acc
220
        else acc
221
      in
222
      let s1 = List.hd sl in (* [s1] := sl *)
223
      let rle = (dep f, lazylistFromList [(s1, bs1base, defer1base)]) in
224
      let fold = bsetFold filterFkt bs acc in (* bs1 := bs1 ∪ { D | some "∀R.D" ∈ bs } *)
225
      rle::fold
226
    else if lfGetType sort f = AxF then
227
      let bs1 = bsetMake () in
228
      let defer1 = bsetMakeRealEmpty () in
229
      (* if f1 = ∀R.D then bs1 = bs1 ∪ { D } *)
230
      let nextf1 = (lfGetDest1 sort f) in
231
      bsetAdd bs1 nextf1;
232
      if (refocusing && (lfGetDeferral sort nextf1) != (Hashtbl.hash "ε")) ||
233
           ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf1))
234
      then
235
        bsetAdd defer1 nextf1
236
      else ();
237
      let s1 = List.hd sl in (* [s1] := sl *)
238
      let rle1 = (dep f, lazylistFromList [(s1, bs1, defer1)]) in
239
      rle1::acc
240
    else acc
241
  in
242
  (* effectively:
243
        mkRule_MultiModalK sort bs [s1]
244
            = { ( λ[bs1]. { ∃R.C } ∪ { ∀R.D
245
                                     | ∀R.D ∈ bs, D ∈ bs1
246
                                                    , [(s1, {C}∪{D | "∀R.D" ∈ bs)]
247
                )
248
              | "∃R.C" ∈ bs
249
              }
250
  *)
251
  bsetFold getRules bs []
252

    
253
let mkRule_Monotone sort bs defer sl : stateExpander =
254
  let rules = mkRuleList_Monotone sort bs defer sl in
255
  lazylistFromList rules
256

    
257

    
258

    
259
(* CoalitionLogic: helper functions *)
260
(*val subset : bitset -> bitset -> bool*)
261
let bsetlen (a: bset) : int =
262
    let res = ref (0) in
263
    bsetIter (fun _ -> res := !res + 1) a;
264
    !res
265

    
266
let subset (a: bset) (b: bset) : bool =
267
    let res = ref (true) in
268
    let f formula =
269
        if bsetMem b formula
270
        then ()
271
        else res := false
272
    in
273
    bsetIter f a;
274
    !res && (bsetlen a < bsetlen b)
275

    
276
let bsetForall (a: bset) (f: CoAlgMisc.localFormula -> bool) : bool =
277
    let res = ref (true) in
278
    let helper formula =
279
        if (f formula) then () else res := false
280
    in
281
    bsetIter helper a;
282
    !res
283

    
284
let bsetExists (a: bset) (f: CoAlgMisc.localFormula -> bool) : bool =
285
    not (bsetForall a (fun x -> not (f x)))
286

    
287
let compatible sort (a: bset) formula1 =
288
    let res = ref (true) in
289
    let f formula2 =
290
        if not (disjointAgents sort formula1 formula2)
291
        then res := false
292
        else ()
293
    in
294
    bsetIter f a;
295
    !res
296

    
297
(*
298
    CoalitionLogic: tableau rules for satisfiability
299

    
300
    Rule 1:
301

    
302
     /\  n
303
    /  \i=1 [C_i] a_i       n ≥ 0,
304
  ——————————————————————    C_i pairwise disjoint
305
     /\  n
306
    /  \i=1  a_i
307

    
308
    Rule 2:
309

    
310
     /\ n                         /\ m
311
    /  \i=1 [C_i] a_i  /\ <D> b  /  \j=1 <N> c_j    n,m ≥ 0
312
  ————————————————————————————————————————————————  C_i pairwise disjoint
313
     /\ n                         /\ m              all C_i ⊆ D
314
    /  \i=1 a_i        /\    b   /  \j=1 c_j
315
*)
316

    
317
(* Not yet implemented: backjumping hooks.
318

    
319
  E.g. in Rule 1, if a subset I of {a_1, ..., a_n} is unsat, then {[C_i] a_i : i \in I} is
320
  already unsat.
321
*)
322

    
323
let mkRule_CL sort bs defer sl : stateExpander =
324
  assert (List.length sl = 1); (* TODO: Why? *)
325
  let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
326
  let deferral_tracking f nextf =
327
    (refocusing && (lfGetDeferral sort nextf) != (Hashtbl.hash "ε")) ||
328
      ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf))
329
  in
330
  let s1 = List.hd sl in (* [s1] = List.hd sl *)
331
  let boxes = bsetFilter bs (fun f -> lfGetType sort f = EnforcesF) in
332
  let diamonds = bsetFilter bs (fun f -> lfGetType sort f = AllowsF) in
333
  let disjoints = maxDisjoints sort boxes in
334
  (*print_endline ("disjoints: "^(string_of_coalition_list sort disjoints)); *)
335
  let nCands = bsetMakeRealEmpty () in (* all N-diamonds *)
336
  let hasFullAgentList formula =
337
    let aglist = lfGetDestAg sort formula in
338
    let value = TArray.all (fun x -> TArray.elem x aglist) (cl_get_agents ()) in
339
    if (value) then bsetAdd nCands formula else () ;
340
    value
341
  in
342
  (* Candidates for D in Rule 2 *)
343
  let dCands = bsetFilter diamonds (fun f -> not (hasFullAgentList f)) in
344
  let c_j : (localFormula * bool) list =
345
    bsetFold (fun f a ->
346
              let nextf = lfGetDest1 sort f in
347
              (nextf, (deferral_tracking f nextf))::a)
348
             nCands []
349
  in
350
  let getRule2 diamDb acc = (* diamDb = <D> b *)
351
    (* print_endline "Rule2" ; *)
352
    let d = lfGetDestAg sort diamDb in (* the agent list *)
353
    let b = lfGetDest1 sort diamDb in
354
    let hasAppropriateAglist f =
355
        let aglist = lfGetDestAg sort f in
356
        TArray.included aglist d
357
    in
358
    let maxdisj = maxDisjoints sort (bsetFilter boxes hasAppropriateAglist) in
359
    let createSingleRule acc coalitions =
360
        let a_i : (localFormula * bool) list =
361
          bsetFold (fun f a ->
362
                    let nextf = lfGetDest1 sort f in
363
                    (nextf, (deferral_tracking f nextf))::a)
364
                   coalitions []
365
        in
366
        (* now do rule 2:
367
            coalitions  /\ <d> b /\ nCands
368
           ————————————————————————————————
369
              a_i       /\     b /\ c_j
370
        *)
371
        let children = bsetMakeRealEmpty () in
372
        let defer1 = bsetMakeRealEmpty () in
373
        bsetAdd children b;
374
        if deferral_tracking diamDb b
375
        then bsetAdd defer1 b;
376
        List.iter (fun (f, isdefer) ->
377
                   bsetAdd children f;
378
                   if isdefer then bsetAdd defer1 f)
379
                  c_j ;
380
        List.iter (fun (f, isdefer) ->
381
                   bsetAdd children f;
382
                   if isdefer then bsetAdd defer1 f)
383
                  a_i ;
384
        ((fun bs1 -> bs), lazylistFromList [(s1, children, defer1)])::acc
385
    in
386
    List.fold_left createSingleRule acc maxdisj
387
  in
388
  let rules = bsetFold getRule2 dCands [] in
389
  let getRule1 acc coalitions =
390
    (* print_endline "Rule1" ; *)
391
    (* do rule 1:
392
        coalitions
393
       ————————————
394
           a_i
395
    *)
396
    let a_i : bset = bsetMakeRealEmpty () in
397
    let defer1 : bset = bsetMakeRealEmpty () in
398
    bsetIter (fun f ->
399
              let nextf = lfGetDest1 sort f in
400
              bsetAdd a_i nextf;
401
              if deferral_tracking f nextf
402
              then bsetAdd defer1 nextf)
403
             coalitions ;
404
    ((fun bs1 -> bs), lazylistFromList [(s1, a_i, defer1)])::acc
405
  in
406
  let rules = List.fold_left getRule1 rules disjoints in
407
  (*
408
    mkRule_CL sort bs [s1]
409
    = { (λ[bs1]. bs, [(s1, { a_i | i∈I })])
410
        | {[C_i]a_i | i∈I} ⊆ bs,
411
          C_i pairwise disjoint and I maximal
412
        }
413
  *)
414
  lazylistFromList rules
415

    
416
let mkRule_GML sort bs defer sl : stateExpander =
417
  assert (List.length sl = 1);
418
  let defer1 = bsetMake () in (* TODO: track deferrals *)
419
  let s1 = List.hd sl in (* [s1] = List.hd sl *)
420
  let diamonds = bsetFilter bs (fun f -> lfGetType sort f = MoreThanF) in
421
  let boxes = bsetFilter bs (fun f -> lfGetType sort f = MaxExceptF) in
422
  let roles = S.makeBS () in
423
  (* step 1: for each diamond/box add R *)
424
  let addRole formula =
425
      ignore (S.addBSNoChk roles (lfGetDest3 sort formula))
426
  in
427
  bsetIter addRole boxes;
428
  bsetIter addRole diamonds;
429
  let addRule role acc =
430
      let premise: (bool*int*int) list =
431
        let modality isDiamond m acc =
432
            if lfGetDest3 sort m = role
433
            then (isDiamond,lfGetDestNum sort m,lfToInt (lfGetDest1 sort m))::acc
434
            else acc
435
        in
436
        List.append
437
            (bsetFold (modality true) diamonds [])
438
            (bsetFold (modality false) boxes [])
439
      in
440
      let conclusion = gml_rules premise in
441
      (* conclusion is a set of rules, *each* of the form \/ /\ lit *)
442
      let handleRuleConcl rc acc =
443
        let handleConjunction conj =
444
            let res = bsetMake () in
445
            List.iter (fun (f,positive) ->
446
                        let f = lfFromInt f in
447
                        let f = if positive then f else
448
                                    match lfGetNeg sort f with
449
                                    | Some nf -> nf
450
                                    | None -> raise (CoAlgFormula.CoAlgException ("Negation of formula missing"))
451
                                    in
452
                        bsetAdd res f)
453
                      conj;
454
            (s1,res, defer1)
455
        in
456
        let rc = List.map handleConjunction rc in
457
        ((fun bs1 -> bs),lazylistFromList rc)::acc
458
      in List.fold_right handleRuleConcl conclusion acc
459
  in
460
  let rules = S.foldBS addRule roles [] in
461
  lazylistFromList rules
462

    
463
let mkRule_PML sort bs defer sl : stateExpander =
464
  assert (List.length sl = 1);
465
  let defer1 = bsetMake () in (* TODO: track deferrals *)
466
  let s1 = List.hd sl in (* [s1] = List.hd sl *)
467
  let diamonds = bsetFilter bs (fun f -> lfGetType sort f = AtLeastProbF) in
468
  let boxes = bsetFilter bs (fun f -> lfGetType sort f = LessProbFailF) in
469
  let premise: (bool*int*int*int) list =
470
    let modality isDiamond m acc =
471
        let nominator   = lfGetDestNum sort m in
472
        let denominator = lfGetDestNum2 sort m in
473
        let nestedFormula = lfToInt (lfGetDest1 sort m) in
474
        (*print_endline ("putting formula "^(string_of_int nestedFormula)); *)
475
        (isDiamond,nominator,denominator,nestedFormula)::acc
476
    in
477
    List.append
478
        (bsetFold (modality true) diamonds [])
479
        (bsetFold (modality false) boxes [])
480
  in
481
  let conclusion = pml_rules premise in
482
  let error message = raise (CoAlgFormula.CoAlgException message) in
483
  (* conclusion is a set of rules, *each* of the form \/ /\ lit *)
484
  let handleRuleConcl rc acc =
485
    let handleConjunction conj =
486
        let res = bsetMake () in
487
        let handleLiteral = fun (f_int,positive) -> begin
488
                    let f = lfFromInt f_int in
489
                    let f = if positive
490
                            then f
491
                            else begin
492
                                (*print_endline ("getting "^(string_of_int f_int)); *)
493
                                match lfGetNeg sort f with
494
                                 | Some nf -> nf
495
                                 | None -> error ("Negation of formula missing")
496
                            end
497
                            in
498
                    bsetAdd res f
499
                    end
500
        in
501
        List.iter handleLiteral conj;
502
        (s1,res, defer1)
503
    in
504
    let rc = List.map handleConjunction rc in
505
    ((fun bs1 -> bs),lazylistFromList rc)::acc
506
  in
507
  let rules = List.fold_right handleRuleConcl conclusion [] in
508
  lazylistFromList rules
509

    
510
(* constant functor *)
511
let mkRule_Const colors sort bs defer sl : stateExpander =
512
  assert (List.length sl = 1);    (* just one (formal) argument *)
513
  let helper (f:localFormula)  (pos, neg) =
514
    let col = lfGetDest3 sort f in
515
    match (lfGetType sort f) with
516
      |  ConstnF -> (pos, (col::neg))
517
      |  ConstF  -> ((col::pos), neg)
518
      |  _       -> (pos, neg)
519
  in
520
  let (pos, neg) = bsetFold helper bs ([], []) in (* pos/neg literals *)
521
  let clash = List.exists (fun l -> List.mem l pos) neg in (* =a /\ ~ = a *)
522
  let allneg = List.length colors = List.length neg in
523
  let twopos = List.length pos > 1 in
524
  let rules = if (clash || allneg || twopos)
525
              then [((fun x -> bs), lazylistFromList [])]  (* no backjumping *)
526
              else []
527
  in
528
  lazylistFromList rules
529

    
530
let mkRule_Identity sort bs defer sl : stateExpander =
531
  let defer1 = bsetMake () in (* TODO: track deferrals *)
532
  assert (List.length sl = 1); (* Identity has one argument *)
533
  let s1 = List.hd sl in
534
  let dep bsl = (* return arguments prefixed with identity operator *)
535
    assert (List.length bsl = 1);
536
    let bs1 = List.hd bsl in
537
    let res = bsetMake () in
538
    let filterFkt f =
539
      if lfGetType sort f = IdF &&
540
        bsetMem bs1 (lfGetDest1 sort f)
541
      then bsetAdd res f
542
      else ()
543
    in
544
    bsetIter filterFkt bs;
545
    res
546
  in
547
  let bs1 = bsetMake () in
548
  let getRule f =
549
    if lfGetType sort f = IdF
550
    then bsetAdd bs1 (lfGetDest1 sort f)
551
    else ()
552
  in
553
  bsetIter getRule bs;
554
  lazylistFromList [(dep, lazylistFromList [(s1, bs1, defer1)])]
555

    
556

    
557
let mkRule_DefaultImplication sort bs defer sl : stateExpander =
558
  raise (CoAlgFormula.CoAlgException ("Default Implication Not yet implemented."))
559

    
560
let mkRule_Choice sort bs defer sl : stateExpander =
561
  assert (List.length sl = 2);
562
  let defer1 = bsetMake () in (* TODO: track deferrals *)
563
  let dep bsl =
564
    assert (List.length bsl = 2);
565
    let bs1 = List.nth bsl 0 in
566
    let bs2 = List.nth bsl 1 in
567
    let res = bsetMake () in
568
    let filterFkt f =
569
      if lfGetType sort f = ChcF &&
570
        (bsetMem bs1 (lfGetDest1 sort f) || bsetMem bs2 (lfGetDest2 sort f))
571
      then bsetAdd res f
572
      else ()
573
    in
574
    bsetIter filterFkt bs;
575
    res
576
  in
577
  let bs1 = bsetMake () in
578
  let bs2 = bsetMake () in
579
  let getRule f =
580
    if lfGetType sort f = ChcF then begin
581
      bsetAdd bs1 (lfGetDest1 sort f);
582
      bsetAdd bs2 (lfGetDest2 sort f)
583
    end else ()
584
  in
585
  bsetIter getRule bs;
586
  let s1 = List.nth sl 0 in
587
  let s2 = List.nth sl 1 in
588
  lazylistFromList [(dep, lazylistFromList [(s1, bs1, defer1); (s2, bs2, defer1)])]
589

    
590

    
591
let mkRule_Fusion sort bs defer sl : stateExpander =
592
  assert (List.length sl = 2);
593
  let defer1 = bsetMake () in (* TODO: track deferrals *)
594
  let dep proj bsl =
595
    assert (List.length bsl = 1);
596
    let bs1 = List.hd bsl in
597
    let res = bsetMake () in
598
    let filterFkt f =
599
      if lfGetType sort f = FusF && lfGetDest3 sort f = proj &&
600
        bsetMem bs1 (lfGetDest1 sort f)
601
      then bsetAdd res f
602
      else ()
603
    in
604
    bsetIter filterFkt bs;
605
    res
606
  in
607
  let bs1 = bsetMake () in
608
  let bs2 = bsetMake () in
609
  let getRule f =
610
    if lfGetType sort f = FusF then
611
      if lfGetDest3 sort f = 0 then bsetAdd bs1 (lfGetDest1 sort f)
612
      else bsetAdd bs2 (lfGetDest1 sort f)
613
    else ()
614
  in
615
  bsetIter getRule bs;
616
  let s1 = List.nth sl 0 in
617
  let s2 = List.nth sl 1 in
618
  lazylistFromList [(dep 0, lazylistFromList [(s1, bs1, defer1)]); (dep 1, lazylistFromList [(s2, bs2, defer1)])]
619

    
620

    
621
(* Maps a logic represented by the type "functors" to the corresponding
622
   "plug-in" function.
623
 *)
624
let getExpandingFunctionProducer = function
625
  | MultiModalK -> mkRule_MultiModalK
626
  | MultiModalKD -> mkRule_MultiModalKD
627
  | Monotone -> mkRule_Monotone
628
  | CoalitionLogic -> mkRule_CL
629
  | GML -> mkRule_GML
630
  | PML -> mkRule_PML
631
  | Constant colors -> mkRule_Const colors
632
  | Identity -> mkRule_Identity
633
  | DefaultImplication -> mkRule_DefaultImplication
634
  | Choice -> mkRule_Choice
635
  | Fusion -> mkRule_Fusion