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