Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgLogics.ml @ edfbcc2b

History | View | Annotate | Download (26 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 nCandsEmpty = ref (true) in
336
  let nCands = bsetMakeRealEmpty () in (* all N-diamonds *)
337
  let dCandsEmpty = ref (true) in
338
  let hasFullAgentList formula =
339
    let aglist = lfGetDestAg sort formula in
340
    let value = TArray.all (fun x -> TArray.elem x aglist) (cl_get_agents ()) in
341
    if (value) then
342
    begin
343
        bsetAdd nCands formula;
344
        nCandsEmpty := false
345
    end
346
    else dCandsEmpty := false;
347
    value
348
  in
349
  (* Candidates for D in Rule 2 *)
350
  (* implicitly fill nCands *)
351
  let dCands = bsetFilter diamonds (fun f -> not (hasFullAgentList f)) in
352
  (*
353
  print_endline ("For set " ^(CoAlgMisc.bsetToString sort bs));
354
  print_endline ("N-Cands: " ^(CoAlgMisc.bsetToString sort nCands));
355
  print_endline ("D-Cands: " ^(CoAlgMisc.bsetToString sort dCands));
356
  *)
357
  let c_j : (localFormula * bool) list =
358
    bsetFold (fun f a -> let nextf = lfGetDest1 sort f in
359
                         (nextf, (deferral_tracking f nextf))::a)
360
      nCands []
361
  in
362
  (* rule 2 for diamaonds where D is a proper subset of the agent set N *)
363
  let getRule2 diamDb acc = (* diamDb = <D> b *)
364
    (* print_endline "Rule2" ; *)
365
    let d = lfGetDestAg sort diamDb in (* the agent list *)
366
    let b = lfGetDest1 sort diamDb in
367
    let hasAppropriateAglist f =
368
        let aglist = lfGetDestAg sort f in
369
        TArray.included aglist d
370
    in
371
    let maxdisj = maxDisjoints sort (bsetFilter boxes hasAppropriateAglist) in
372
    let createSingleRule acc coalitions =
373
        let a_i : (localFormula * bool) list =
374
          bsetFold (fun f a ->
375
                    let nextf = lfGetDest1 sort f in
376
                    (nextf, (deferral_tracking f nextf))::a)
377
                   coalitions []
378
        in
379
        (* now do rule 2:
380
            coalitions  /\ <d> b /\ nCands
381
           ————————————————————————————————
382
              a_i       /\     b /\ c_j
383
        *)
384
        let children = bsetMakeRealEmpty () in
385
        let defer1 = bsetMakeRealEmpty () in
386
        bsetAdd children b;
387
        if deferral_tracking diamDb b
388
        then bsetAdd defer1 b;
389
        List.iter (fun (f, isdefer) ->
390
                   bsetAdd children f;
391
                   if isdefer then bsetAdd defer1 f)
392
                  c_j ;
393
        List.iter (fun (f, isdefer) ->
394
                   bsetAdd children f;
395
                   if isdefer then bsetAdd defer1 f)
396
                  a_i ;
397
        ((fun bs1 -> bs), lazylistFromList [(s1, children, defer1)])::acc
398
    in
399
    List.fold_left createSingleRule acc maxdisj
400
  in
401
  let rules = bsetFold getRule2 dCands [] in
402
  let getRule2ForFullAgents acc =
403
    (* So far, we only applied rule 2 for D a proper subset of N.
404
       We still need rule 2 for D=N and b=c_j for some j. (Or equivalently we
405
       apply rule2 without the <d> b).
406
       If there are not N formulas, we don't need to do this because the
407
       created rule 2 applications are just the rule 1 applications.
408
    *)
409
    if not !nCandsEmpty then begin
410
        (* create rule 2 once for all the diamonds with a full agent set *)
411
        let maxdisj = maxDisjoints sort boxes in
412
        let createSingleRule acc coalitions =
413
            let a_i : (localFormula * bool) list =
414
              bsetFold (fun f a -> let nextf = lfGetDest1 sort f in
415
                                   (nextf, (deferral_tracking f nextf))::a)
416
                coalitions []
417
            in
418
            (* now do rule 2:
419
                coalitions  /\ nCands
420
               ———————————————————————
421
                  a_i       /\ c_j
422
            *)
423
            let children = bsetMakeRealEmpty () in
424
            let defer1 = bsetMakeRealEmpty () in
425
            List.iter (fun (f, isdefer) ->
426
              bsetAdd children f;
427
              if isdefer then bsetAdd defer1 f)
428
              c_j ;
429
            List.iter (fun (f, isdefer) ->
430
              bsetAdd children f;
431
              if isdefer then bsetAdd defer1 f)
432
              a_i ;
433
            ((fun bs1 -> bs), lazylistFromList [(s1, children, defer1)])::acc
434
        in
435
        List.fold_left createSingleRule acc maxdisj
436
    end else acc
437
  in
438
  let rules = getRule2ForFullAgents rules in
439
  let getRule1 acc coalitions =
440
    (* print_endline "Rule1" ; *)
441
    (* do rule 1:
442
        coalitions
443
       ————————————
444
           a_i
445
    *)
446
    let a_i : bset = bsetMakeRealEmpty () in
447
    let defer1 : bset = bsetMakeRealEmpty () in
448
    bsetIter (fun f ->
449
              let nextf = lfGetDest1 sort f in
450
              bsetAdd a_i nextf;
451
              if deferral_tracking f nextf
452
              then bsetAdd defer1 nextf)
453
             coalitions ;
454
    ((fun bs1 -> bs), lazylistFromList [(s1, a_i, defer1)])::acc
455
  in
456
  let rules = List.fold_left getRule1 rules disjoints in
457
  (*
458
    mkRule_CL sort bs [s1]
459
    = { (λ[bs1]. bs, [(s1, { a_i | i∈I })])
460
        | {[C_i]a_i | i∈I} ⊆ bs,
461
          C_i pairwise disjoint and I maximal
462
        }
463
  *)
464
  lazylistFromList rules
465

    
466
let mkRule_GML sort bs defer sl : stateExpander =
467
  assert (List.length sl = 1);
468
  let defer1 = bsetMake () in (* TODO: track deferrals *)
469
  let s1 = List.hd sl in (* [s1] = List.hd sl *)
470
  let diamonds = bsetFilter bs (fun f -> lfGetType sort f = MoreThanF) in
471
  let boxes = bsetFilter bs (fun f -> lfGetType sort f = MaxExceptF) in
472
  let roles = S.makeBS () in
473
  (* step 1: for each diamond/box add R *)
474
  let addRole formula =
475
      ignore (S.addBSNoChk roles (lfGetDest3 sort formula))
476
  in
477
  bsetIter addRole boxes;
478
  bsetIter addRole diamonds;
479
  let addRule role acc =
480
      let premise: (bool*int*int) list =
481
        let modality isDiamond m acc =
482
            if lfGetDest3 sort m = role
483
            then (isDiamond,lfGetDestNum sort m,lfToInt (lfGetDest1 sort m))::acc
484
            else acc
485
        in
486
        List.append
487
            (bsetFold (modality true) diamonds [])
488
            (bsetFold (modality false) boxes [])
489
      in
490
      let conclusion = gml_rules premise in
491
      (* conclusion is a set of rules, *each* of the form \/ /\ lit *)
492
      let handleRuleConcl rc acc =
493
        let handleConjunction conj =
494
            let res = bsetMake () in
495
            List.iter (fun (f,positive) ->
496
                        let f = lfFromInt f in
497
                        let f = if positive then f else
498
                                    match lfGetNeg sort f with
499
                                    | Some nf -> nf
500
                                    | None -> raise (CoAlgFormula.CoAlgException ("Negation of formula missing"))
501
                                    in
502
                        bsetAdd res f)
503
                      conj;
504
            (s1,res, defer1)
505
        in
506
        let rc = List.map handleConjunction rc in
507
        ((fun bs1 -> bs),lazylistFromList rc)::acc
508
      in List.fold_right handleRuleConcl conclusion acc
509
  in
510
  let rules = S.foldBS addRule roles [] in
511
  lazylistFromList rules
512

    
513
let mkRule_PML sort bs defer sl : stateExpander =
514
  assert (List.length sl = 1);
515
  let defer1 = bsetMake () in (* TODO: track deferrals *)
516
  let s1 = List.hd sl in (* [s1] = List.hd sl *)
517
  let diamonds = bsetFilter bs (fun f -> lfGetType sort f = AtLeastProbF) in
518
  let boxes = bsetFilter bs (fun f -> lfGetType sort f = LessProbFailF) in
519
  let premise: (bool*int*int*int) list =
520
    let modality isDiamond m acc =
521
        let nominator   = lfGetDestNum sort m in
522
        let denominator = lfGetDestNum2 sort m in
523
        let nestedFormula = lfToInt (lfGetDest1 sort m) in
524
        (*print_endline ("putting formula "^(string_of_int nestedFormula)); *)
525
        (isDiamond,nominator,denominator,nestedFormula)::acc
526
    in
527
    List.append
528
        (bsetFold (modality true) diamonds [])
529
        (bsetFold (modality false) boxes [])
530
  in
531
  let conclusion = pml_rules premise in
532
  let error message = raise (CoAlgFormula.CoAlgException message) in
533
  (* conclusion is a set of rules, *each* of the form \/ /\ lit *)
534
  let handleRuleConcl rc acc =
535
    let handleConjunction conj =
536
        let res = bsetMake () in
537
        let handleLiteral = fun (f_int,positive) -> begin
538
                    let f = lfFromInt f_int in
539
                    let f = if positive
540
                            then f
541
                            else begin
542
                                (*print_endline ("getting "^(string_of_int f_int)); *)
543
                                match lfGetNeg sort f with
544
                                 | Some nf -> nf
545
                                 | None -> error ("Negation of formula missing")
546
                            end
547
                            in
548
                    bsetAdd res f
549
                    end
550
        in
551
        List.iter handleLiteral conj;
552
        (s1,res, defer1)
553
    in
554
    let rc = List.map handleConjunction rc in
555
    ((fun bs1 -> bs),lazylistFromList rc)::acc
556
  in
557
  let rules = List.fold_right handleRuleConcl conclusion [] in
558
  lazylistFromList rules
559

    
560
(* constant functor *)
561
let mkRule_Const colors sort bs defer sl : stateExpander =
562
  assert (List.length sl = 1);    (* just one (formal) argument *)
563
  let helper (f:localFormula)  (pos, neg) =
564
    let col = lfGetDest3 sort f in
565
    match (lfGetType sort f) with
566
      |  ConstnF -> (pos, (col::neg))
567
      |  ConstF  -> ((col::pos), neg)
568
      |  _       -> (pos, neg)
569
  in
570
  let (pos, neg) = bsetFold helper bs ([], []) in (* pos/neg literals *)
571
  let clash = List.exists (fun l -> List.mem l pos) neg in (* =a /\ ~ = a *)
572
  let allneg = List.length colors = List.length neg in
573
  let twopos = List.length pos > 1 in
574
  let rules = if (clash || allneg || twopos)
575
              then [((fun x -> bs), lazylistFromList [])]  (* no backjumping *)
576
              else []
577
  in
578
  lazylistFromList rules
579

    
580
let mkRule_Identity sort bs defer sl : stateExpander =
581
  assert (List.length sl = 1); (* Identity has one argument *)
582
  let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
583
  let deferral_tracking defer f nextf =
584
    if (refocusing && (lfGetDeferral sort nextf) != (Hashtbl.hash "ε")) ||
585
         ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf))
586
    then bsetAdd defer nextf
587
  in
588
  let s1 = List.hd sl in
589
  let dep bsl = (* return arguments prefixed with identity operator *)
590
    assert (List.length bsl = 1);
591
    let bs1 = List.hd bsl in
592
    let res = bsetMake () in
593
    let filterFkt f =
594
      if lfGetType sort f = IdF &&
595
        bsetMem bs1 (lfGetDest1 sort f)
596
      then bsetAdd res f
597
      else ()
598
    in
599
    bsetIter filterFkt bs;
600
    res
601
  in
602
  let bs1 = bsetMake () in
603
  let defer1 = bsetMakeRealEmpty () in
604
  let getRule f =
605
    if lfGetType sort f = IdF
606
    then
607
      begin
608
        deferral_tracking defer1 f (lfGetDest1 sort f);
609
        bsetAdd bs1 (lfGetDest1 sort f)
610
      end
611
    else ()
612
  in
613
  bsetIter getRule bs;
614
  lazylistFromList [(dep, lazylistFromList [(s1, bs1, defer1)])]
615

    
616

    
617
let mkRule_DefaultImplication sort bs defer sl : stateExpander =
618
  raise (CoAlgFormula.CoAlgException ("Default Implication Not yet implemented."))
619

    
620
let mkRule_Choice sort bs defer sl : stateExpander =
621
  assert (List.length sl = 2);
622
  let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
623
  let deferral_tracking defer f nextf =
624
    if (refocusing && (lfGetDeferral sort nextf) != (Hashtbl.hash "ε")) ||
625
         ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf))
626
    then bsetAdd defer nextf
627
  in
628
  let dep bsl =
629
    assert (List.length bsl = 2);
630
    let bs1 = List.nth bsl 0 in
631
    let bs2 = List.nth bsl 1 in
632
    let res = bsetMake () in
633
    let filterFkt f =
634
      if lfGetType sort f = ChcF &&
635
        (bsetMem bs1 (lfGetDest1 sort f) || bsetMem bs2 (lfGetDest2 sort f))
636
      then bsetAdd res f
637
      else ()
638
    in
639
    bsetIter filterFkt bs;
640
    res
641
  in
642
  let bs1 = bsetMake () in
643
  let defer1 = bsetMakeRealEmpty () in
644
  let bs2 = bsetMake () in
645
  let defer2 = bsetMakeRealEmpty () in
646
  let getRule f =
647
    if lfGetType sort f = ChcF then
648
      begin
649
        bsetAdd bs1 (lfGetDest1 sort f);
650
        deferral_tracking defer1 f (lfGetDest1 sort f);
651
        bsetAdd bs2 (lfGetDest2 sort f);
652
        deferral_tracking defer2 f (lfGetDest2 sort f)
653
      end else ()
654
  in
655
  bsetIter getRule bs;
656
  let s1 = List.nth sl 0 in
657
  let s2 = List.nth sl 1 in
658
  lazylistFromList [(dep, lazylistFromList [(s1, bs1, defer1); (s2, bs2, defer2)])]
659

    
660

    
661
let mkRule_Fusion sort bs defer sl : stateExpander =
662
  assert (List.length sl = 2);
663
  let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
664
  let deferral_tracking defer f nextf =
665
    if (refocusing && (lfGetDeferral sort nextf) != (Hashtbl.hash "ε")) ||
666
         ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf))
667
    then bsetAdd defer nextf
668
  in
669
  let dep proj bsl =
670
    assert (List.length bsl = 1);
671
    let bs1 = List.hd bsl in
672
    let res = bsetMake () in
673
    let filterFkt f =
674
      if lfGetType sort f = FusF && lfGetDest3 sort f = proj &&
675
        bsetMem bs1 (lfGetDest1 sort f)
676
      then bsetAdd res f
677
      else ()
678
    in
679
    bsetIter filterFkt bs;
680
    res
681
  in
682
  let bs1 = bsetMake () in
683
  let defer1 = bsetMakeRealEmpty () in
684
  let bs2 = bsetMake () in
685
  let defer2 = bsetMakeRealEmpty () in
686
  let getRule f =
687
    if lfGetType sort f = FusF then
688
      if lfGetDest3 sort f = 0 then
689
        begin
690
          deferral_tracking defer1 f (lfGetDest1 sort f);
691
          bsetAdd bs1 (lfGetDest1 sort f)
692
        end
693
      else
694
        begin
695
          deferral_tracking defer2 f (lfGetDest1 sort f);
696
          bsetAdd bs2 (lfGetDest1 sort f)
697
        end
698
    else ()
699
  in
700
  bsetIter getRule bs;
701
  let s1 = List.nth sl 0 in
702
  let s2 = List.nth sl 1 in
703
  lazylistFromList [(dep 0, lazylistFromList [(s1, bs1, defer1)]);
704
                    (dep 1, lazylistFromList [(s2, bs2, defer2)])]
705

    
706

    
707
(* Maps a logic represented by the type "functors" to the corresponding
708
   "plug-in" function.
709
 *)
710
let getExpandingFunctionProducer = function
711
  | MultiModalK -> mkRule_MultiModalK
712
  | MultiModalKD -> mkRule_MultiModalKD
713
  | Monotone -> mkRule_Monotone
714
  | CoalitionLogic -> mkRule_CL
715
  | GML -> mkRule_GML
716
  | PML -> mkRule_PML
717
  | Constant colors -> mkRule_Const colors
718
  | Identity -> mkRule_Identity
719
  | DefaultImplication -> mkRule_DefaultImplication
720
  | Choice -> mkRule_Choice
721
  | Fusion -> mkRule_Fusion