## cool / src / lib / FuzzyALCReasoner.ml @ b75e5a66

History | View | Annotate | Download (24.8 KB)

1 |
(* |
---|---|

2 |
* vim: ts=2 sw=2 |

3 |
*) |

4 | |

5 |
(* |

6 |
* This module implements the Lukasiewicz Fuzzy |

7 |
* ALC reasoner described in |

8 |
* http://ijcai.org/papers13/Papers/IJCAI13-147.pdf |

9 |
*) |

10 | |

11 |
open FuzzyALCABox |

12 |
open Hashtbl |

13 |
open Glpk |

14 |
open HashConsing |

15 |
module HC = HashConsing |

16 | |

17 |
(* |

18 |
* XXX - global state kept by the solver. |

19 |
* For performance (and some other) reasons, |

20 |
* we keep parts of the state in this global |

21 |
* hash table. This avoids copying it with |

22 |
* each recursion step. |

23 |
*) |

24 |
let maxrole = ref (0) |

25 |
let freshIndividual m = |

26 |
incr m; |

27 |
(*outputDebug 5 ("Generated new individual, id " ^ string_of_int !m);*) |

28 |
!m |

29 |
module AsstSet = Map.Make( |

30 |
struct |

31 |
type t = hcAsst |

32 |
let compare a b = |

33 |
match (a, b) with |

34 |
| (HCCONCEPT(a, x), HCCONCEPT(b, y)) -> |

35 |
if a != b then a - b |

36 |
else if x != y then Pervasives.compare x.HC.tag y.HC.tag |

37 |
else 0 |

38 |
| ((HCROLE(a, b, c) as x), (HCROLE(d, e, f) as y)) -> |

39 |
Pervasives.compare x y |

40 |
| (HCCONCEPT(_, _), HCROLE(_, _, _)) -> -1 |

41 |
| (HCROLE(_, _, _), HCCONCEPT(_, _)) -> 1 |

42 |
end |

43 |
) |

44 |
let expandedLeft = ref AsstSet.empty |

45 |
let getLeftExpansion hcAsst = |

46 |
if AsstSet.mem hcAsst !expandedLeft then |

47 |
AsstSet.find hcAsst !expandedLeft |

48 |
else |

49 |
( |

50 |
let r = freshIndividual maxrole in |

51 |
expandedLeft := AsstSet.add hcAsst r !expandedLeft; |

52 |
r |

53 |
) |

54 |
let branchMemo = ref AsstSet.empty |

55 | |

56 |
(* Debugging options *) |

57 |
let recursionDepth = ref 0 |

58 | |

59 |
let debuglevel = 0 |

60 |
let outputDepth = 4 |

61 |
let printBussProof = false |

62 | |

63 |
let print_proof s = |

64 |
if printBussProof then |

65 |
print_endline s |

66 |
else |

67 |
() |

68 | |

69 |
let outputDebug l s = |

70 |
if debuglevel >= l then |

71 |
( |

72 |
if !recursionDepth < 6 then ( |

73 |
print_string (" " ^ (string_of_int !recursionDepth) ^ " "); |

74 |
for i = 0 to !recursionDepth do |

75 |
print_string "\t" |

76 |
done; |

77 |
print_endline s ) |

78 |
) |

79 |
else |

80 |
() |

81 | |

82 |
(* |

83 |
* We use two different forms for storing inequalities in this |

84 |
* module: First, the basic |

85 |
* (asst List) * int * (asst List) |

86 |
* where both sides are multisets of inequalities, represented as |

87 |
* lists, and second, during the solving process, |

88 |
* the ABox is saved in a map mapping |

89 |
* (AsstMultiSet.t * int * AsstMultiSet.t) to int |

90 |
* where the value is an integer that signals different flags relevant |

91 |
* to the solver routine and the key is the actual inequality, |

92 |
* using the AsstMultiSet documented below. |

93 |
*) |

94 | |

95 |
(* |

96 |
* Maps assertion to coefficient. Used as building block |

97 |
* to implement a multiset. |

98 |
*) |

99 |
module AsstMap = Map.Make( |

100 |
struct |

101 |
type t = hcAsst |

102 |
(* If hash-consing works, then... *) |

103 |
let equal l r = |

104 |
match (l, r) with |

105 |
| (HCROLE(a1, b1, c1), HCROLE(a2, b2, c2)) -> |

106 |
a1 = a2 && b1 = b2 && c1 = c2 |

107 |
| (HCCONCEPT(a1, c1), HCCONCEPT(a2, c2)) -> |

108 |
a1 = a2 && c1 == c2 |

109 |
| (_, _) -> false |

110 |
let compare l r = |

111 |
match (l, r) with |

112 |
| (HCROLE(a1, b1, c1), HCROLE(a2, b2, c2)) -> |

113 |
if a1 != a2 then a1 - a2 |

114 |
else if b1 != b2 then b1 - b2 |

115 |
else if c1 != c2 then c1 - c2 |

116 |
else 0 |

117 |
| (HCCONCEPT(a1, c1), HCCONCEPT(a2, c2)) -> |

118 |
if a1 != a2 then a1 - a2 |

119 |
else if c1 != c2 then Pervasives.compare c1.HC.tag c2.HC.tag |

120 |
else 0 |

121 |
| (HCROLE(_, _, _), _) -> -1 |

122 |
| (HCCONCEPT(_, _), _) -> +1 |

123 |
end |

124 |
) |

125 | |

126 |
(* |

127 |
* Implements a multiset of assertions. Provides a subset |

128 |
* of the normal set operations, with changed semantics: |

129 |
* Each element might exist multiple times in the multiset. |

130 |
* Iterating over a multiset might call the iterator function |

131 |
* multiple times for the same element, if it exists more than |

132 |
* once in the set. |

133 |
*) |

134 |
module AsstMultiSet = |

135 |
struct |

136 |
type t = int AsstMap.t |

137 |
let empty = AsstMap.empty |

138 |
let compare a b = |

139 |
AsstMap.compare (fun x y -> x - y) a b |

140 |
let equal a b = |

141 |
AsstMap.equal (fun x y -> x = y) a b |

142 | |

143 |
let add value t = |

144 |
if not (AsstMap.mem value t) then |

145 |
AsstMap.add value 1 t |

146 |
else |

147 |
AsstMap.add value ((AsstMap.find value t) + 1) t |

148 | |

149 |
let remove value t = |

150 |
let old = AsstMap.find value t in |

151 |
if old = 1 then |

152 |
AsstMap.remove value t |

153 |
else |

154 |
AsstMap.add value (old - 1) t |

155 | |

156 |
let iter f t = |

157 |
let iter_f key value = |

158 |
for i = 1 to value do |

159 |
f key |

160 |
done |

161 |
in |

162 |
AsstMap.iter iter_f t |

163 | |

164 |
let for_all f t = |

165 |
AsstMap.for_all (fun key value -> f key) t |

166 | |

167 |
let cardinal t v = |

168 |
AsstMap.find v t |

169 | |

170 |
(* |

171 |
* This iterates over the underlying map, calling the given iterator function |

172 |
* as often as the element is contained in the set. It does not behave |

173 |
* like the iteration on the map would ;-) |

174 |
*) |

175 |
let fold f t b = |

176 |
let foldN key value bb = |

177 |
if value = 0 then bb |

178 |
else ( |

179 |
let ret = ref bb in |

180 |
for i = 1 to value do |

181 |
ret := f key !ret |

182 |
done; |

183 |
!ret |

184 |
) |

185 |
in |

186 |
AsstMap.fold foldN t b |

187 | |

188 |
(* This wraps the fold of the underlying map *) |

189 |
let fold_raw f t b = |

190 |
AsstMap.fold f t b |

191 |
end |

192 | |

193 |
type inequality = AsstMultiSet.t * int * AsstMultiSet.t |

194 |
(* |

195 |
* Flags associated with the inequalities while they are |

196 |
* being mangled by the solver. These will be expanded in |

197 |
* the future. Currently, the only flag signals whether |

198 |
* the (\exists L) rule has already be applied to this |

199 |
* inequality. |

200 |
*) |

201 |
let emptyFlags = 0 |

202 |
let addDeleted i = i lor 1 |

203 |
let checkDeleted i = (i land 1) > 0 |

204 |
(* |

205 |
* A map used for storing the ABoxes in memory. |

206 |
* Maps the inequalities in the set to their flags |

207 |
* (ABoxes are _sets_ of inequalities) |

208 |
*) |

209 |
module InequalitySet = Map.Make( |

210 |
struct |

211 |
type t = inequality |

212 |
(*let compare = compare*) |

213 |
let compare (l1, g1, r1) (l2, g2, r2) = |

214 |
if g1 != g2 then g1 - g2 |

215 |
else if not (AsstMultiSet.equal l1 l2) then AsstMultiSet.compare l1 l2 |

216 |
else if not (AsstMultiSet.equal r1 r2) then AsstMultiSet.compare r1 r2 |

217 |
else 0 |

218 |
let equal (l1, g1, r1) (l2, g2, r2) = |

219 |
g1 = g2 && |

220 |
AsstMultiSet.equal l1 l2 && |

221 |
AsstMultiSet.equal r1 r2 |

222 |
end |

223 |
) |

224 |
let iterInequalitySet f s = |

225 |
let g elem flags = |

226 |
if not (checkDeleted flags) then |

227 |
f elem flags |

228 |
else |

229 |
() |

230 |
in |

231 |
InequalitySet.iter g s |

232 |
let removeInequality ineq r = |

233 |
r := InequalitySet.add ineq (addDeleted emptyFlags) (!r) |

234 | |

235 |
(* |

236 |
* Converts from AsstMultiSet to list representation |

237 |
*) |

238 |
let toAssertion ((lefts : AsstMultiSet.t), (gr : int), (rights : AsstMultiSet.t)) = |

239 |
let left = ref [] in |

240 |
let right = ref [] in |

241 |
let iter ret asst = |

242 |
ret := (toAsst asst)::(!ret) |

243 |
in |

244 |
AsstMultiSet.iter (iter left) lefts; |

245 |
AsstMultiSet.iter (iter right) rights; |

246 |
(!left, gr, !right) |

247 | |

248 |
(* |

249 |
* For debug reasons: Prints ABox to stdout |

250 |
*) |

251 |
let printABox hcInput = |

252 |
outputDebug 4 "-------------"; |

253 |
iterInequalitySet (fun k flags -> (outputDebug 4 ((string_of_int flags) ^ " -> " ^ (printAssertion (toAssertion k))))) !hcInput; |

254 |
outputDebug 4 "-------------"; |

255 |
() |

256 | |

257 |
(* |

258 |
* Checks whether an inequality consists of atomic assertions only. |

259 |
* |

260 |
* We also consider inequalities atomic that have (TODO: explain \exist R-problems) |

261 |
*) |

262 |
let nodeAtomic (left, gr, right) = |

263 |
let asstAtomic s ignoreExists = |

264 |
let f x = |

265 |
match x with |

266 |
| HCCONCEPT (_, y) -> |

267 |
(match y.fml with |

268 |
| AP(_) -> true |

269 |
| TRUE -> true |

270 |
| FALSE -> true |

271 |
| EXISTS(_, _) when ignoreExists -> true |

272 |
| _ -> false) |

273 |
| HCROLE (_, _, _) -> true |

274 |
in |

275 |
AsstMultiSet.for_all f s |

276 |
in |

277 |
asstAtomic left false && asstAtomic right true |

278 | |

279 |
let max (a : int) (b : int) = |

280 |
if a > b then a else b |

281 | |

282 |
exception InternalReasonerError of string |

283 | |

284 |
(* |

285 |
* Solve linear programming problem consisting of an arbitrary number |

286 |
* of assertions with exactly n variables. |

287 |
*) |

288 |
let lpSolve assertions n = |

289 |
(* Coefficients of function being optimized. As we |

290 |
* only care for satisfiability of the LP problem, not |

291 |
* for an optimum, set them to 0. *) |

292 |
let coeff = Array.make n 0. in |

293 |
let matrix = Array.make_matrix (List.length assertions) n 0. in |

294 |
(* Auxiliary variables, i.e. row variables. |

295 |
* All rows will be of the form a + b - c - d + X > 0 *) |

296 |
let auxbound = Array.make (List.length assertions) (0., infinity) in |

297 |
(* Original variables, i.e. column variables *) |

298 |
let origbound = Array.make n (0., 1.) in |

299 |
(* Iterate over all rows and fill linear problem *) |

300 |
let f i (gr, left, right) = |

301 |
Array.set auxbound i (0.001 -. (float_of_int gr), infinity); |

302 |
(* Iterate over this row *) |

303 |
let g fac asstID = |

304 |
(*outputDebug ("Setting asstID " ^ string_of_int(asstID));*) |

305 |
let currow = Array.get matrix i in |

306 |
let newval = (Array.get currow asstID) +. fac in |

307 |
Array.set currow asstID newval |

308 |
in |

309 |
(*outputDebug (string_of_int i);*) |

310 |
List.iter (g 1.) left; |

311 |
List.iter (g ~-.1.) right; |

312 |
i+1; |

313 |
in |

314 |
if n == 0 then ( |

315 |
outputDebug 2 ("LP problem with no variables given, number of assertions: " ^ (string_of_int (List.length assertions))); |

316 |
(* If we have no variables, we either might have no inequalities, too |

317 |
* (-> In this case, the problem is trivially satisfiable), or |

318 |
* n >= 1 inequalities with no variables, in this case, all inequalities |

319 |
* are 0 + X > 0. In this case, check whether there is an unsatisfiable |

320 |
* assertion *) |

321 |
let check cur (gr, left, right) = |

322 |
cur && (gr > 0) |

323 |
in |

324 |
List.fold_left check true assertions |

325 |
) else ( |

326 |
outputDebug 2 ("Building LP problem for " ^ string_of_int (List.length assertions) ^ " ABox inequalities" ^ " and " ^ string_of_int n ^ " variables."); |

327 |
List.fold_left f 0 assertions; |

328 |
(*outputDebug "Solving!";*) |

329 |
let lp = make_problem Maximize coeff matrix auxbound origbound in |

330 |
simplex lp; |

331 |
if get_status lp then ( |

332 |
outputDebug 1 "Satisfiable ABox!"; |

333 |
) else ( |

334 |
outputDebug 1 "Unsatisfiable ABox!"; |

335 |
(*print_proof "\AxiomC{}";*) |

336 |
); |

337 |
get_status lp |

338 |
) |

339 | |

340 |
let rec ruleClash hcF input = |

341 |
let foobar = ref input in |

342 |
printABox foobar; |

343 |
(* |

344 |
* Construct LP problem from ABox. Use all atomic ABox inequalities |

345 |
* and map them to an linear inequality. |

346 |
*) |

347 |
let conceptIdTable = Hashtbl.create 3 in |

348 |
let roleIdTable = Hashtbl.create 3 in |

349 |
let counter = ref 0 in |

350 |
(* |

351 |
* Variables in the LP problem correspond to atomic concept assertions, i.e. |

352 |
* assertions of the form (individual ID):(atomic concept), or atomic role |

353 |
* assertions. |

354 |
* |

355 |
* Give each of these assertions a unique ID. getConceptId and getRoleId |

356 |
* get the mapping, counter holds the number of currently found concepts. |

357 |
*) |

358 |
let getConceptId i s = |

359 |
outputDebug 5 ("Finding ID for concept: " ^ (string_of_int i) ^ ", " ^ s); |

360 |
try Hashtbl.find conceptIdTable (i, s) |

361 |
with Not_found -> |

362 |
let x = !counter in |

363 |
incr counter; |

364 |
Hashtbl.add conceptIdTable (i, s) x; |

365 |
x; |

366 |
in |

367 |
let getRoleId i1 i2 s = |

368 |
outputDebug 5 ("Finding ID for role: " ^ string_of_int(i1) ^ ", " ^ string_of_int(i2) ^ ", " ^ string_of_int(s)); |

369 |
try Hashtbl.find roleIdTable (i1, i2, s) |

370 |
with Not_found -> |

371 |
let x = !counter in |

372 |
incr counter; |

373 |
Hashtbl.add roleIdTable (i1, i2, s) x; |

374 |
x; |

375 |
in |

376 |
let getAssts x ret = |

377 |
match x with |

378 |
| HCROLE(i1, i2, s) -> (getRoleId i1 i2 s)::ret |

379 |
| HCCONCEPT(i, {fml = AP(s)}) -> (getConceptId i s)::ret |

380 |
(* |

381 |
* On the right-hand side of the assertion, existential quantifiers |

382 |
* might occur, we can ignore them. |

383 |
*) |

384 |
| HCCONCEPT(i, {fml = EXISTS(_, _)}) -> ret |

385 |
(* |

386 |
* Top and bottom might always accour and are handled |

387 |
* in countTop |

388 |
*) |

389 |
| HCCONCEPT(i, {fml = TRUE}) -> ret |

390 |
| HCCONCEPT(i, {fml = FALSE}) -> ret |

391 |
| _ -> raise (InternalReasonerError "Invalid assertion given to getAssts") |

392 |
in |

393 |
let countTop assts = |

394 |
let f asst ret = |

395 |
match asst with |

396 |
| HCCONCEPT(i, {fml = TRUE}) -> ret + 1 |

397 |
| HCCONCEPT(i, {fml = FALSE}) -> ret - 1 |

398 |
| _ -> ret |

399 |
in |

400 |
AsstMultiSet.fold f assts 0 |

401 |
in |

402 |
let f ((left, gr, right) as ineq) value ret = |

403 |
outputDebug 5 ("Processing inequality " ^ (printAssertion (toAssertion ineq))); |

404 |
(gr + (countTop left) - (countTop right), |

405 |
AsstMultiSet.fold getAssts left [], AsstMultiSet.fold getAssts right [])::ret |

406 |
in |

407 |
(* Filter out atomic assertions in this ABox and map them to linear inequalities *) |

408 |
let atomics = InequalitySet.filter (fun key value -> nodeAtomic key) input in |

409 |
lpSolve (InequalitySet.fold f atomics []) !counter |

410 | |

411 | |

412 |
let inconsistent_marker = (AsstMultiSet.empty, -1, AsstMultiSet.empty) |

413 | |

414 |
(* |

415 |
* Adds an inequality to the set. Returns true if successful, false |

416 |
* if the ABox gets obviously inconsistent after the addition. |

417 |
* (Note that a positive return value does not imply consistency |

418 |
* of the resulting ABox!) |

419 |
*) |

420 |
let addInequality ref changed ((left, gr, right) as ineq) flags = |

421 |
if not (InequalitySet.mem ineq !ref) then |

422 |
( |

423 |
let count (s : AsstMultiSet.t) = |

424 |
let iter k a r = |

425 |
r + a |

426 |
in |

427 |
AsstMultiSet.fold_raw iter s 0 |

428 |
in |

429 |
(* If all left variables are set to true, but the left side is still below 0, the |

430 |
* inequality obviously causes a clash. *) |

431 |
let ok = ((count left) + gr) > 0 in |

432 |
if ok then ( |

433 |
outputDebug 2 (" --> Adding inequality " ^ (printAssertion (toAssertion ineq))); |

434 |
ref := InequalitySet.add ineq flags !ref; |

435 |
changed := true; |

436 |
) else ( |

437 |
outputDebug 2 (" --> Inequality " ^ (printAssertion (toAssertion ineq)) ^ " causes clash. Not adding!"); |

438 |
(* Add a magic inequality to the set, to mark it inconsistent. *) |

439 |
ref := InequalitySet.add inconsistent_marker emptyFlags !ref; |

440 |
) |

441 |
) |

442 | |

443 |
(************************************************************ |

444 |
* non-branching rules. We can always apply them |

445 |
************************************************************) |

446 | |

447 |
(* |

448 |
* Applies negation elimination to both sides of the |

449 |
* inequality, left and right |

450 |
*) |

451 |
let rec ruleNeg hcF ret changed = |

452 |
let iter ((left, gr, right) as ineq) flags = |

453 |
let iter_asst_left hcasst = |

454 |
match hcasst with |

455 |
| HCCONCEPT(a, {fml = NOT(y); _}) -> |

456 |
removeInequality ineq ret; |

457 |
addInequality ret changed (AsstMultiSet.remove hcasst left, gr+1, AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, y))) right) emptyFlags; |

458 |
() |

459 |
| _ -> () |

460 |
in |

461 |
let iter_asst_right hcasst = |

462 |
match hcasst with |

463 |
| HCCONCEPT(a, {fml = NOT(y); _}) -> |

464 |
removeInequality ineq ret; |

465 |
addInequality ret changed (AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, y))) left, gr-1, AsstMultiSet.remove hcasst right) emptyFlags; |

466 |
() |

467 |
| _ -> () |

468 |
in |

469 |
AsstMultiSet.iter iter_asst_left left; |

470 |
AsstMultiSet.iter iter_asst_right right; |

471 |
in |

472 |
iterInequalitySet iter !ret |

473 | |

474 |
let rec ruleAndRight hcF ret changed = |

475 |
let iter ((left, gr, right) as ineq) flags = |

476 |
let f elem = |

477 |
match elem with |

478 |
| HCCONCEPT(a, {fml = AND(x, y); _}) -> |

479 |
let nr = AsstMultiSet.remove elem right in |

480 |
removeInequality ineq ret; |

481 |
addInequality ret changed (left, gr, nr) emptyFlags; |

482 |
addInequality ret changed (left, gr+1, AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, x))) (AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, y))) nr)) emptyFlags; |

483 |
() |

484 |
| _ -> (); |

485 |
in |

486 |
AsstMultiSet.iter f right; |

487 |
in |

488 |
iterInequalitySet iter !ret |

489 | |

490 |
let rec ruleExistsRight hcF ret changed = |

491 |
(* |

492 |
* We have to find pairs of inequalities. Iterate over all inequalities |

493 |
* two times (quadratic). First, find an inequality with a assertion |

494 |
* a:\exists R.C on the right side, then an inequality with a matching |

495 |
* role assertion on the left side. |

496 |
*) |

497 |
(* This function looks for (a,b):R on the left side and returns a list of |

498 |
* matching individuals b *) |

499 |
let fold1 na ((left, gr, right) as ineq) flags l1 = |

500 |
let f elem l2 = |

501 |
match elem with |

502 |
| HCROLE(a, b, c) when a = na -> |

503 |
b :: l2 |

504 |
| _ -> l2 |

505 |
in |

506 |
AsstMultiSet.fold f left l1 |

507 |
in |

508 |
(* This function looks for a:\exists R.C on the right side *) |

509 |
let iter1 ((left, gr, right) as ineq) flags = |

510 |
(* Find pairs of inequalities *) |

511 |
let f elem = |

512 |
match elem with |

513 |
(* Candidate for first inequality *) |

514 |
| HCCONCEPT(a, {fml = EXISTS(x, c)}) as r -> |

515 |
(* Get list of candidates for b *) |

516 |
let bs = InequalitySet.fold (fold1 a) !ret [] in |

517 |
if List.length bs != 0 then ( |

518 |
addInequality ret changed (left, gr, AsstMultiSet.remove r right) emptyFlags; |

519 |
let addf () b = |

520 |
addInequality ret changed (left, gr+1, AsstMultiSet.add (toHcAsst hcF (CONCEPT(b, c))) (AsstMultiSet.add (toHcAsst hcF (ROLE(a, b, x))) (AsstMultiSet.remove r right))) emptyFlags; |

521 |
() |

522 |
in |

523 |
List.fold_left addf () bs; |

524 |
) else |

525 |
(); |

526 |
| _ -> (); |

527 |
in |

528 |
AsstMultiSet.iter f right; |

529 |
in |

530 |
iterInequalitySet iter1 !ret |

531 | |

532 |
(************************************************************* |

533 |
* Solver loop and branching rules (mutually recursive |

534 |
* with main solver routine) |

535 |
*************************************************************) |

536 | |

537 |
let branchCount = ref 0 |

538 |
let startTime = ref 0. |

539 |
let maxRuntime = ref (-1.) |

540 | |

541 |
exception BranchCountExhausted |

542 | |

543 |
let checkTime x = |

544 |
if !maxRuntime <> -1. then |

545 |
( |

546 |
if (Sys.time() -. !startTime) > !maxRuntime then |

547 |
raise BranchCountExhausted |

548 |
else |

549 |
() |

550 |
) |

551 |
else |

552 |
() |

553 | |

554 |
let rec internalSolve hcF input = |

555 |
checkTime 0; |

556 |
let r = ref input in |

557 |
(* |

558 |
incr branchCount; |

559 |
(*print_endline (string_of_int !branchCount);*) |

560 |
(if !branchCount > 100000 then |

561 |
raise BranchCountExhausted |

562 |
else |

563 |
() |

564 |
) |

565 |
; |

566 |
*) |

567 |
outputDebug 5 "Starting on ABox:"; |

568 |
printABox r; |

569 |
if InequalitySet.mem inconsistent_marker input then |

570 |
( |

571 |
outputDebug 2 "Trivially clashing ABox given to internalSolve, returning false"; |

572 |
false |

573 |
) |

574 |
else if not (true (*ruleClash hcF input*)) then |

575 |
( |

576 |
outputDebug 2 "Nontrivially clashing ABox given to internalSolve, returning false"; |

577 |
false |

578 |
) |

579 |
else internalSolve2 hcF input |

580 |
and solveWrapper hcF changed abox newineq remineq = |

581 |
let newabox = ref abox in |

582 |
addInequality newabox changed newineq emptyFlags; |

583 |
removeInequality remineq newabox; |

584 |
internalSolve hcF !newabox |

585 |
and internalSolve2 hcF input = |

586 |
let hcInput = ref input in |

587 |
let changed = ref true in |

588 |
outputDebug 2 "GREP Starting new branch with ABox:"; |

589 |
printABox hcInput; |

590 |
while !changed do |

591 |
changed := false; |

592 |
ruleNeg hcF hcInput changed; |

593 |
ruleAndRight hcF hcInput changed; |

594 |
checkTime 0; |

595 |
(*printABox hcInput*) |

596 |
(*outputDebug("Non-branching rules applied. Number of inequalities in result: " ^ string_of_int (InequalitySet.cardinal !hcInput))*) |

597 |
done; |

598 |
changed := true; |

599 |
let existsRightDone = ref false in |

600 |
while !changed do |

601 |
changed := false; |

602 |
ruleExistsRight hcF hcInput changed; |

603 |
checkTime 0; |

604 |
existsRightDone := !existsRightDone || !changed; |

605 |
done; |

606 |
if !existsRightDone then |

607 |
internalSolve hcF !hcInput |

608 |
else ( |

609 |
(*outputDebug "No further linear expansion possible. Checking for branches.";*) |

610 |
(* XXX *) |

611 |
let ok = ref false in |

612 |
changed := false; |

613 |
ok := ruleExistsLeft hcF hcInput changed; |

614 |
if !changed then !ok else ( |

615 |
ok := ruleAndLeft hcF hcInput changed; |

616 |
if !changed then !ok else ( |

617 |
(*outputDebug("No branches possible. Checking if ABox clashes.");*) |

618 |
(*printABox hcInput;*) |

619 |
checkTime 0; |

620 |
ruleClash hcF !hcInput |

621 |
) |

622 |
) |

623 |
) |

624 |
(************************************************************* |

625 |
* Branching rules |

626 |
* (They call the "internalSolve" function recursively) |

627 |
*************************************************************) |

628 |
and branchWrapper hcF changed ret newineq1 newineq2 remineq reason = |

629 |
(* |

630 |
* Performs a branch on the assertion "reason". If a branch |

631 |
* on this exact assertion has already been performed in the |

632 |
* current path of the tableau, take the same direction as |

633 |
* previously. If not, record the branch direction in |

634 |
* the global hash table |

635 |
*) |

636 |
if AsstSet.mem reason !branchMemo then ( |

637 |
if AsstSet.find reason !branchMemo = 0 then |

638 |
solveWrapper hcF changed ret newineq1 remineq |

639 |
else |

640 |
solveWrapper hcF changed ret newineq2 remineq |

641 |
) else ( |

642 |
let retval = ref false in |

643 |
branchMemo := AsstSet.add reason 0 !branchMemo; |

644 |
retval := !retval || solveWrapper hcF changed ret newineq1 remineq; |

645 |
branchMemo := AsstSet.add reason 1 !branchMemo; |

646 |
retval := !retval || solveWrapper hcF changed ret newineq2 remineq; |

647 |
branchMemo := AsstSet.remove reason !branchMemo; |

648 |
!retval |

649 |
) |

650 |
and ruleExistsLeft hcF ret changed = |

651 |
let ok = ref false in |

652 |
let iter ((left, gr, right) as ineq) flags = |

653 |
let f elem = |

654 |
match elem with |

655 |
(* |

656 |
* This rule may only be applied once to a single assertion (i.e. a single |

657 |
* existential quantifier - generating more individuals wouldn't make any |

658 |
* sense from a logic/model-building point of view). We keep a set of all |

659 |
* assertions we've already applied this rule to. |

660 |
*) |

661 |
| (HCCONCEPT(a, {fml = EXISTS(x, y); _}) as asst) as reason -> |

662 |
(*outputDebug ("GREP Branching on (exists left) " ^ (printAssertion (toAssertion (left, gr, right))));*) |

663 |
(*print_endline ("Generating new individual for assertion " ^ (string_of_int a) ^ ":\exists " ^ (string_of_int x) ^ "." ^ (printConcept y));*) |

664 |
let nl = AsstMultiSet.remove elem left in |

665 |
let branch1 = (nl, gr, right) in |

666 |
let indiv = getLeftExpansion asst in |

667 |
let branch2 = (AsstMultiSet.add (toHcAsst hcF (ROLE(a, indiv, x))) (AsstMultiSet.add (toHcAsst hcF (CONCEPT(indiv, y))) nl), gr-1, right) in |

668 |
if (not (InequalitySet.mem branch1 !ret)) && (not (InequalitySet.mem branch2 !ret)) then |

669 |
( |

670 |
changed := true; |

671 |
recursionDepth := !recursionDepth + 1; |

672 |
ok := !ok || branchWrapper hcF changed !ret branch1 branch2 ineq reason; |

673 |
recursionDepth := !recursionDepth - 1; |

674 |
) |

675 |
else |

676 |
() |

677 |
| _ -> (); |

678 |
in |

679 |
AsstMultiSet.iter f left; |

680 |
in |

681 |
iterInequalitySet iter !ret; |

682 |
!ok |

683 |
and ruleAndLeft hcF ret changed = |

684 |
let ok = ref false in |

685 |
let iter ((left, gr, right) as ineq) flags = |

686 |
let f elem = |

687 |
match elem with |

688 |
| HCCONCEPT(a, {fml = AND(x, y); _}) as reason -> |

689 |
let nl = AsstMultiSet.remove elem left in |

690 |
let branch1 = (nl, gr, right) in |

691 |
let branch2 = (AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, x))) (AsstMultiSet.add (toHcAsst hcF (CONCEPT(a, y))) (AsstMultiSet.remove elem left)), gr-1, right) in |

692 |
if (not (InequalitySet.mem branch1 !ret)) && (not (InequalitySet.mem branch2 !ret)) then |

693 |
( |

694 |
(*outputDebug ("GREP Branching on (and left) " ^ (printAssertion (toAssertion (left, gr, right))) ^ ", branch is: " ^ (printConcept (AND(x, y)))); |

695 |
outputDebug ("GREP Adding " ^ (printAssertion (toAssertion branch1)) ^ " or " ^ (printAssertion (toAssertion branch2)));*) |

696 |
changed := true; |

697 |
recursionDepth := !recursionDepth + 1; |

698 |
ok := !ok || branchWrapper hcF changed !ret branch1 branch2 ineq reason; |

699 |
recursionDepth := !recursionDepth - 1; |

700 |
) |

701 |
else |

702 |
() |

703 |
| _ -> (); |

704 |
in |

705 |
AsstMultiSet.iter f left; |

706 |
in |

707 |
iterInequalitySet iter !ret; |

708 |
!ok |

709 | |

710 |
let rec simplify_concept (f:concept) : concept = |

711 |
match f with |

712 |
| NOT(NOT(a)) -> simplify_concept a |

713 |
| AND(x, y) -> |

714 |
let xx = simplify_concept x in |

715 |
let yy = simplify_concept y in |

716 |
if xx = TRUE then yy |

717 |
else (if yy = TRUE then xx |

718 |
else (if (xx = FALSE) || (yy = FALSE) then FALSE |

719 |
else AND(xx, yy))) |

720 |
| OR(x, y) -> |

721 |
let xx = simplify_concept x in |

722 |
let yy = simplify_concept y in |

723 |
if xx = FALSE then yy |

724 |
else (if yy = FALSE then xx |

725 |
else (if (xx = TRUE) || (yy = TRUE) then TRUE |

726 |
else OR(xx, yy))) |

727 |
| EXISTS(r, c) -> |

728 |
let cc = simplify_concept c in |

729 |
if cc = FALSE then FALSE |

730 |
else (if cc = TRUE then TRUE |

731 |
else EXISTS(r, cc)) |

732 |
| x -> x |

733 | |

734 |
let funConcat f1 f2 x = f1 (f2 x) (* XXX can't this be done better? *) |

735 | |

736 |
let rec setMaxRuntime m = |

737 |
maxRuntime := m |

738 | |

739 |
let rec fuzzyALCsat input_orig = |

740 |
(* Create new HashCons table. Formulas don't have negation forms. *) |

741 |
let hcF = HcFormula.create false in |

742 |
(* Remove universal quantifiers from input *) |

743 |
let input = List.map (funConcat FuzzyALCABox.replaceOrForall FuzzyALCABox.collapseNeg) input_orig in |

744 |
(* Convert input formulae to hash-consed representation *) |

745 |
maxrole := (-1); |

746 |
expandedLeft := AsstSet.empty; |

747 |
let f ss (left, gr, right) = |

748 |
let g s asst = |

749 |
match asst with |

750 |
| ROLE(a, b, c) -> |

751 |
maxrole := max !maxrole (max a b); |

752 |
AsstMultiSet.add (HCROLE(a, b, c)) s |

753 |
| CONCEPT(a, c) -> |

754 |
maxrole := max !maxrole a; |

755 |
AsstMultiSet.add (HCCONCEPT(a, hc_formula hcF (simplify_concept c))) s |

756 |
in |

757 |
InequalitySet.add (List.fold_left g AsstMultiSet.empty left, gr, List.fold_left g AsstMultiSet.empty right) emptyFlags ss |

758 |
in |

759 |
branchCount := 0; |

760 |
let ret = internalSolve hcF (List.fold_left f InequalitySet.empty input) in |

761 |
ret |

762 | |

763 |
let fuzzyALCsat_time input maxtime = |

764 |
setMaxRuntime maxtime; |

765 |
startTime := Sys.time(); |

766 |
try |

767 |
let sat = fuzzyALCsat input in |

768 |
setMaxRuntime (-1.); |

769 |
(Sys.time() -. (!startTime), sat) |

770 |
with |

771 |
BranchCountExhausted -> |

772 |
setMaxRuntime (-1.); |

773 |
(-1., false) |