## 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 |