Project

General

Profile

Statistics
| Branch: | Revision:

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)