Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ 1d36cd07

History | View | Annotate | Download (40 KB)

1 4fd28192 Thorsten Wißmann
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
2
    @author Florian Widmann
3
 *)
4
5
6
open CoAlgMisc
7
8
module M = Minisat
9
10 c2cc0c2e Thorsten Wißmann
module CU = CoolUtils
11
12 4fd28192 Thorsten Wißmann
type sortTable = CoAlgMisc.sortTable
13
14 c78c1ce0 Thorsten Wißmann
type nomTable = string -> CoAlgFormula.sort option
15
16
type assumptions = CoAlgFormula.sortedFormula list
17
18
type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula
19
20 f335015f Thorsten Wißmann
exception ReasonerError of string
21 4fd28192 Thorsten Wißmann
22
(*****************************************************************************)
23
(*                     Propagation of Satisfiability                         *)
24
(*****************************************************************************)
25
26
let propSatFindSucc setCnstr cset =
27
  if csetHasDot cset then false
28
  else
29
    match graphFindCnstr cset with
30 6d64bc5a Christoph Egger
    | None -> raise (ReasonerError "?")
31
    | Some SatC -> true
32
    | Some (OpenC _) -> setMemCnstr setCnstr cset
33
    | Some (UnexpandedC _)
34
    | Some UnsatC -> false
35
36 4fd28192 Thorsten Wißmann
37
let rec propSat setStates setCores setCnstr = function
38
  | [] -> ()
39
  | propElem::tl ->
40
      let tl1 =
41
        match propElem with
42
        | UState (state, _) ->
43
            if setMemState setStates state then
44
              let cnstrs = stateGetConstraints state in
45
              let isStillOpen = cssExists (fun c -> propSatFindSucc setCnstr c) cnstrs in
46
              if isStillOpen then () else setRemoveState setStates state
47
            else ();
48
            tl
49
        | UCore (core, _) ->
50
            if setMemCore setCores core then
51
              let cnstrs = coreGetConstraints core in
52
              let isStillOpen = cssExists (fun c -> propSatFindSucc setCnstr c) cnstrs in
53
              if isStillOpen then tl else begin
54
                setRemoveCore setCores core;
55
                let cnstrPar = coreGetConstraintParents core in
56
                List.fold_left (fun acc cset -> (UCnstr cset)::acc) tl cnstrPar
57
              end
58
            else tl
59
        | UCnstr cset ->
60
            if setMemCnstr setCnstr cset then begin
61
              setRemoveCnstr setCnstr cset;
62
              match graphFindCnstr cset with
63
              | Some (OpenC nodes) ->
64
                  let prop acc node =
65
                    match node with
66
                    | Core core -> (UCore (core, true))::acc
67
                    | State state -> (UState (state, None))::acc
68
                  in
69
                  List.fold_left prop tl nodes
70
              | _ -> assert false
71
            end else tl
72
      in
73
      propSat setStates setCores setCnstr tl1
74
75
let propagateSat () =
76
  let setStates = setEmptyState () in
77
  let setCores = setEmptyCore () in
78
  let setCnstr = setEmptyCnstr () in
79
  let fktS1 state =
80
    match stateGetStatus state with
81
    | Expandable
82
    | Open -> setAddState setStates state
83
    | Unsat
84
    | Sat -> ()
85
  in
86
  graphIterStates fktS1;
87
  let fktC1 core =
88
    match coreGetStatus core with
89
    | Expandable
90
    | Open -> setAddCore setCores core
91
    | Unsat
92
    | Sat -> ()
93
  in
94
  graphIterCores fktC1;
95
  let cfkt1 cset cnstr =
96
    if csetHasDot cset then ()
97
    else
98
      match cnstr with
99
      | OpenC _ -> setAddCnstr setCnstr cset
100
      | UnsatC
101
      | SatC
102
      | UnexpandedC _ -> ()
103
  in
104
  graphIterCnstrs cfkt1;
105
  graphIterStates (fun state -> propSat setStates setCores setCnstr [UState (state, None)]);
106
  graphIterCores (fun core -> propSat setStates setCores setCnstr [UCore (core, false)]);
107
  setIterState (fun state -> stateSetStatus state Sat) setStates;
108
  let setCoreSat core =
109
    coreSetStatus core Sat;
110
    if core == graphGetRoot () then raise (CoAlg_finished true) else ()
111
  in
112
  setIterCore setCoreSat setCores;
113
  setIterCnstr (fun cset -> graphReplaceCnstr cset SatC) setCnstr
114
115
116 6bbde09c Christoph Egger
let propagateSatMu () =
117
  let setFinishingStates = setEmptyState () in
118
  let setFinishingCores = setEmptyCore () in
119
  let setStates = setEmptyState () in
120
  let setCores = setEmptyCore () in
121
  let emptySet = bsetMakeRealEmpty () in
122 dce4e4aa Christoph Egger
  let openstates = ref 0 in
123 6bbde09c Christoph Egger
124 2f126161 Christoph Egger
  (* Collect two sets of nodes. All nodes that may be satisfiable
125
   * after this iteration are collected into setStates/setCores.
126
   *
127
   * As every cycle containing a node with empty focus or an
128
   * satisfiable node should be considered satisfiable, collect these
129
   * decisive nodes into setFinishingStates/setFinishingCores
130
   *
131
   * This also marks in trivial cases nodes as satisfiable.
132
   *)
133 6bbde09c Christoph Egger
  let stateCollector state =
134
    match stateGetStatus state with
135 07a36b24 Christoph Egger
    | Unsat -> ()
136
    | Sat ->
137 3c05e89f Christoph Egger
       setAddState setStates state;
138 3a374ca4 Hans-Peter Deifel
       setAddState setFinishingStates state
139 1e781c93 Christoph Egger
    | Expandable -> ()
140 6bbde09c Christoph Egger
    | Open ->
141 dce4e4aa Christoph Egger
       openstates := !openstates + 1;
142 012c092c Christoph Egger
       if List.length (stateGetRules state) == 0 || (* States with no rules are satisfiable *)
143 2f126161 Christoph Egger
         bsetCompare (bsetMake ()) (stateGetBs state) == 0 (* KD generates nodes with just True as formula *)
144 6bbde09c Christoph Egger
       then begin
145 3f073372 Christoph Egger
         setAddState setFinishingStates state;
146 46cd6856 Christoph Egger
         stateSetStatus state Sat
147
       end else begin
148
         setAddState setStates state;
149
         if bsetCompare (stateGetDeferral state) emptySet == 0
150
         then begin
151 6bbde09c Christoph Egger
           setAddState setFinishingStates state
152
         end
153 46cd6856 Christoph Egger
         else ()
154
       end
155 2f126161 Christoph Egger
156
  (* As it is enough for a core to have one successfull child, we can
157
   * also handle (some) expandable cores.
158
   *)
159
  and coreCollector core =
160 6bbde09c Christoph Egger
    match coreGetStatus core with
161 07a36b24 Christoph Egger
    | Unsat -> ()
162
    | Sat ->
163 3c05e89f Christoph Egger
       setAddCore setCores core;
164 3f073372 Christoph Egger
       setAddCore setFinishingCores core
165 080482ac Christoph Egger
    | Expandable
166 6bbde09c Christoph Egger
    | Open ->
167
       setAddCore setCores core;
168 3a374ca4 Hans-Peter Deifel
       if bsetCompare (coreGetDeferral core) emptySet == 0
169
       then begin
170
         setAddCore setFinishingCores core
171
       end
172
       else ()
173 6bbde09c Christoph Egger
  in
174
  graphIterStates stateCollector;
175
  graphIterCores coreCollector;
176
177 dce4e4aa Christoph Egger
  setPropagationCounter !openstates;
178 55dc0a64 Christoph Egger
179 2f126161 Christoph Egger
  (* In a fixpoint the set called setStates / setCores is narrowed
180
   * down.
181
   *
182
   * In each step only those states and cores are retained in setStates
183
   * / setCores which reach one of setFinishing{States,Cores} in
184
   * finitely many steps. This new set of States / Cores is collected
185
   * as allowed{States,Cores} during each fixpoint iteration.
186
   *
187
   * Only those finishing nodes are retained that have allowed or
188
   * Successfull Children.
189
   *)
190 6bbde09c Christoph Egger
  let rec fixpointstep setStates setCores =
191 67b07e54 Christoph Egger
    let allowedStates = setEmptyState () in
192
    let allowedCores = setEmptyCore () in
193 6bbde09c Christoph Egger
194
    let rec visitParentStates (core : core) : unit =
195 9fb4b019 Christoph Egger
      if not (setMemCore allowedCores core)
196
      then begin
197
        setAddCore allowedCores core;
198
        let verifyParent (state,_) =
199
          let rules = stateGetRules state in
200
          let ruleiter (dependencies, corelist) =
201 0debe698 Christoph Egger
            List.exists (fun (core : core) -> setMemCore allowedCores core ||
202
                                                coreGetStatus core == Sat)
203 9fb4b019 Christoph Egger
              corelist
204
          in
205
          if List.for_all ruleiter rules
206
          then visitParentCores state
207 67b07e54 Christoph Egger
        in
208 9fb4b019 Christoph Egger
        List.iter verifyParent (coreGetParents core)
209 6bbde09c Christoph Egger
      end
210
211
    and visitParentCores (state : state) : unit =
212 9fb4b019 Christoph Egger
      if not (setMemState allowedStates state)
213
      then begin
214
        setAddState allowedStates state;
215
        let verifyParent core =
216
          let acceptable =
217 0debe698 Christoph Egger
            List.exists (fun (state : state) -> setMemState allowedStates state ||
218
                                                  stateGetStatus state == Sat)
219 9fb4b019 Christoph Egger
              (coreGetChildren core)
220
          in
221
          if acceptable
222
          then visitParentStates core
223 6bbde09c Christoph Egger
        in
224 9fb4b019 Christoph Egger
        List.iter verifyParent (stateGetParents state)
225 6bbde09c Christoph Egger
      end
226
    in
227
228 07a36b24 Christoph Egger
    (* All rule applications need to still be potentially Sat for a
229
     * finishing State to be a valid startingpoint for this fixpoint.
230
     *)
231
    let checkFinishingState (state : state) =
232
      let ruleiter (dependencies, corelist) : bool =
233 0debe698 Christoph Egger
        List.for_all (fun (core : core) -> coreGetStatus core == Unsat ||
234
                                             coreGetStatus core == Expandable ||
235
                                               not (setMemCore setCores core)) corelist
236 07a36b24 Christoph Egger
      in
237
      if not (List.exists ruleiter (stateGetRules state)) then begin
238
        visitParentCores state
239
      end
240
241
    (* There needs to be a State still potentially Sat for this core
242
     * to be considered for the fixpoint
243
     *)
244
    and checkFinishingCore (core : core) =
245 0debe698 Christoph Egger
      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat ||
246
                                                     stateGetStatus state == Expandable ||
247
                                                       not (setMemState setStates state))
248 07a36b24 Christoph Egger
                           (coreGetChildren core))
249
      then begin
250
        visitParentStates core
251
      end
252
    in
253
    setIterState checkFinishingState setFinishingStates;
254
    setIterCore checkFinishingCore setFinishingCores;
255
256 6bbde09c Christoph Egger
257
    if (setLengthState setStates) = (setLengthState allowedStates) &&
258 07a36b24 Christoph Egger
         (setLengthCore setCores) = (setLengthCore allowedCores)
259 6bbde09c Christoph Egger
    then begin
260 07a36b24 Christoph Egger
        setIterState (fun state -> stateSetStatus state Sat) setStates;
261 0debe698 Christoph Egger
        setIterCore (fun core -> coreSetStatus core Sat; if core == graphGetRoot ()
262
                                                         then raise (CoAlg_finished true)
263
                                                         else ()) setCores;
264 07a36b24 Christoph Egger
      end else
265 6bbde09c Christoph Egger
      fixpointstep allowedStates allowedCores
266
  in
267
  fixpointstep setStates setCores
268
269
270 4fd28192 Thorsten Wißmann
(*****************************************************************************)
271
(*                     Propagation of Unsatisfiability                       *)
272
(*****************************************************************************)
273
274
let isConstraintUnsat cset =
275
  match graphFindCnstr cset with
276
  | None -> assert false
277
  | Some UnsatC -> true
278
  | _ -> false
279
280 433c8a2e Thorsten Wißmann
let fhtMustFind fht f =
281 4fd28192 Thorsten Wißmann
  match fhtFind fht f with
282
  | Some l -> l
283
  | None -> assert false
284
285 433c8a2e Thorsten Wißmann
let lhtMustFind lht l =
286
  match lhtFind lht l with
287 4fd28192 Thorsten Wißmann
  | Some f -> f
288
  | None -> assert false
289 01bf25db Thorsten Wißmann
290 7b21fbae Christoph Egger
291
(* Gets a list of Things we know are unsatisfiable and propagates this
292
   information backwards *)
293 433c8a2e Thorsten Wißmann
let rec propagateUnsat = function
294 4fd28192 Thorsten Wißmann
  | [] -> ()
295
  | propElem::tl ->
296
      let tl1 =
297
        match propElem with
298
        | UState (state, idxopt) -> begin
299
            match stateGetStatus state with
300
            | Unsat -> tl
301 73762b19 Thorsten Wißmann
            | Sat -> raise (ReasonerError ("Propagation tells state "
302
                                           ^(string_of_int (stateGetIdx state))
303
                                           ^" would be unsat, but it is already sat"))
304 4fd28192 Thorsten Wißmann
            | Open
305
            | Expandable ->
306
                let mbs =
307
                  match idxopt with
308
                  | None -> stateGetBs state
309
                  | Some idx ->
310
                      let (dep, children) = stateGetRule state idx in
311
                      let getBs core =
312
                        assert (coreGetStatus core = Unsat);
313
                        coreGetBs core
314
                      in
315
                      dep (List.map getBs children)
316
                in
317
                stateSetBs state mbs;
318
                stateSetStatus state Unsat;
319
                let prop acc core =
320
                  let turnsUnsat =
321
                    match coreGetStatus core with
322 0debe698 Christoph Egger
                    | Open -> List.for_all (fun s -> stateGetStatus s = Unsat)
323
                                           (coreGetChildren core)
324 4fd28192 Thorsten Wißmann
                    | Expandable
325
                    | Unsat
326
                    | Sat -> false
327
                  in
328
                  if turnsUnsat then (UCore (core, false))::acc else acc
329
                in
330
                List.fold_left prop tl (stateGetParents state)
331
          end
332
        | UCore (core, comesFromCnstr) -> begin
333
            match coreGetStatus core with
334
            | Unsat -> tl
335 73762b19 Thorsten Wißmann
            | Sat -> raise (ReasonerError ("Propagation tells core "
336
                                           ^(string_of_int (coreGetIdx core))
337
                                           ^" would be unsat, but it is already sat"))
338 4fd28192 Thorsten Wißmann
            | Open
339
            | Expandable ->
340
                let mbs =
341
                  if comesFromCnstr then coreGetBs core
342
                  else
343
                    let bs = coreGetBs core in
344 e0e6eb62 Hans-Peter Deifel
                    let solver = coreGetSolver core in
345 4fd28192 Thorsten Wißmann
                    let fht = coreGetFht core in
346
                    let lht = lhtInit () in
347
                    let addLits f acc =
348
                      let lit = fhtMustFind fht f in
349
                      lhtAdd lht lit f;
350
                      lit::acc
351
                    in
352
                    let litset = bsetFold addLits bs [] in
353
                    let addClauses state =
354
                      let cbs = stateGetBs state in
355
                      let clause = bsetFold (fun f acc -> (M.neg_lit (fhtMustFind fht f))::acc) cbs [] in
356
                      let okay = M.add_clause solver clause in
357
                      assert okay
358
                    in
359
                    List.iter addClauses (coreGetChildren core);
360
                    let isSat = M.invoke_solver solver litset in
361
                    assert (not isSat);
362
                    let res = bsetMake () in
363
                    let confls = M.get_conflict solver in
364
                    List.iter (fun l -> bsetAdd res (lhtMustFind lht l)) confls;
365
                    res
366
                in
367
                coreSetBs core mbs;
368
                coreSetStatus core Unsat;
369 6aa0e444 Christoph Egger
                coreDeallocateSolver core;
370 4fd28192 Thorsten Wißmann
                if core == graphGetRoot () then raise (CoAlg_finished false) else ();
371
                let prop acc (state, idx) =
372
                  let turnsUnsat =
373
                    match stateGetStatus state with
374
                    | Open
375
                    | Expandable ->
376
                        List.for_all (fun c -> coreGetStatus c = Unsat) (snd (stateGetRule state idx))
377
                    | Unsat
378
                    | Sat -> false
379
                  in
380
                  if turnsUnsat then (UState (state, Some idx))::acc else acc
381
                in
382
                let tl2 = List.fold_left prop tl (coreGetParents core) in
383
                List.fold_left (fun acc cset -> (UCnstr cset)::acc) tl2 (coreGetConstraintParents core)
384
          end
385
        | UCnstr cset ->
386
            match graphFindCnstr cset with
387
            | None
388
            | Some SatC -> assert false
389
            | Some UnsatC -> tl
390
            | Some (UnexpandedC nodes)
391
            | Some (OpenC nodes) ->
392
                graphReplaceCnstr cset UnsatC;
393
                let prop acc node =
394
                  match node with
395
                  | State state ->
396 3eb8fabd Christoph Egger
                      let turnsUnsat =
397 4fd28192 Thorsten Wißmann
                        match stateGetStatus state with
398
                        | Expandable
399
                        | Open -> cssForall isConstraintUnsat (stateGetConstraints state)
400
                        | Unsat
401
                        | Sat -> false
402
                      in
403
                      if turnsUnsat then (UState (state, None))::acc else acc
404
                  | Core core ->
405
                      let turnsUnsat =
406
                        match coreGetStatus core with
407
                        | Expandable
408
                        | Open -> cssForall isConstraintUnsat (coreGetConstraints core)
409
                        | Unsat
410
                        | Sat -> false
411
                      in
412
                      if turnsUnsat then (UCore (core, true))::acc else acc
413
                in
414
                List.fold_left prop tl nodes
415
      in
416
      propagateUnsat tl1
417
418 8ab82480 Christoph Egger
let propagateUnsatMu () =
419 5956a56d Christoph Egger
  let setFinishingStates = setEmptyState () in
420
  let setFinishingCores = setEmptyCore () in
421
  let setStates = setEmptyState () in
422
  let setCores = setEmptyCore () in
423
  let emptySet = bsetMakeRealEmpty () in
424
425
  (* Collect two sets of nodes. All nodes that may be unsatisfiable
426
   * after this iteration are collected into setStates/setCores.
427
   *
428
   * Nodes reaching Points with empty focus as well as Expandable nodes
429
   * (if not Unsat) can not be declared Unsat so we collect these into
430
   * setFinishingStates/setFinishingCores.
431
   *)
432
  let stateCollector state =
433
    match stateGetStatus state with
434
    | Unsat -> ()
435
    | Sat
436
    | Expandable ->
437
       setAddState setStates state;
438
      setAddState setFinishingStates state
439
    | Open ->
440
       setAddState setStates state;
441 c126d689 Christoph Egger
      if [] = (stateGetRules state)
442
      then begin
443
        stateSetStatus state Sat;
444
        setAddState setFinishingStates state
445
      end
446
      else ();
447 5956a56d Christoph Egger
      if bsetCompare (stateGetDeferral state) emptySet == 0
448
      then begin
449
        setAddState setFinishingStates state
450
      end
451
      else ()
452
453
  and coreCollector core =
454
    match coreGetStatus core with
455
    | Unsat -> ()
456
    | Expandable
457
    | Sat ->
458
       setAddCore setCores core;
459
      setAddCore setFinishingCores core
460
    | Open ->
461
       setAddCore setCores core;
462
      if bsetCompare (coreGetDeferral core) emptySet == 0
463
      then begin
464
        setAddCore setFinishingCores core
465
      end
466
      else ()
467
  in
468
  graphIterStates stateCollector;
469
  graphIterCores coreCollector;
470
471
  (* In a fixpoint the set called setFinishingStates/setFinishingCores
472
   * is narrowed down
473
   *
474
   * In each iteration we start with all Nodes and remove all that can
475
   * reach a finishing Node. We then remove all finishing Nodes from the
476
   * respective set which are becoming Unsat and start with the next
477
   * iteration until the fixpoint is reached
478
   *
479
   *
480
   *)
481
  let rec fixpointstep setPrevUnsatStates setPrevUnsatCores =
482
    let setUnsatStates = setCopyState setStates in
483
    let setUnsatCores = setCopyCore setCores in
484
485
    let rec visitParentStates (core : core) : unit =
486
      if setMemCore setUnsatCores core
487
      then begin
488
        setRemoveCore setUnsatCores core;
489
        let verifyParent (state,_) =
490
          let rules = stateGetRules state in
491
          let ruleiter (dependencies, corelist) =
492 0debe698 Christoph Egger
            List.exists (fun (core : core) -> not (setMemCore setUnsatCores core) ||
493
                                                coreGetStatus core == Sat)
494 5956a56d Christoph Egger
              corelist
495
          in
496
          if List.for_all ruleiter rules
497
          then visitParentCores state
498
        in
499
        List.iter verifyParent (coreGetParents core)
500
      end
501
502
    and visitParentCores (state : state) : unit =
503
      if setMemState setUnsatStates state
504
      then begin
505
        setRemoveState setUnsatStates state;
506
        let verifyParent core =
507
          let acceptable =
508 0debe698 Christoph Egger
            List.exists (fun (state : state) -> not (setMemState setUnsatStates state) ||
509
                                                  stateGetStatus state == Sat)
510 5956a56d Christoph Egger
              (coreGetChildren core)
511
          in
512
          if acceptable
513
          then visitParentStates core
514
        in
515
        List.iter verifyParent (stateGetParents state)
516
      end
517
    in
518
519
    (* All rule applications need to still be potentially Sat for a
520
     * finishing State to be a valid startingpoint for this fixpoint.
521
     *)
522
    let checkFinishingState (state : state) =
523
      let ruleiter (dependencies, corelist) : bool =
524 0debe698 Christoph Egger
        List.for_all (fun (core : core) -> coreGetStatus core == Unsat ||
525
                                             setMemCore setPrevUnsatCores core) corelist
526 5956a56d Christoph Egger
      in
527 0debe698 Christoph Egger
      if not (List.exists ruleiter (stateGetRules state)) ||
528
           stateGetStatus state == Expandable then begin
529 5956a56d Christoph Egger
        visitParentCores state
530
      end
531
532
    (* There needs to be a State still potentially Sat for this core
533
     * to be considered for the fixpoint
534
     *)
535
    and checkFinishingCore (core : core) =
536 0debe698 Christoph Egger
      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat ||
537
                                                     setMemState setPrevUnsatStates state)
538 e1489b0d Christoph Egger
                (coreGetChildren core)) ||
539
        coreGetStatus core == Expandable
540 5956a56d Christoph Egger
      then begin
541
        visitParentStates core
542
      end
543
    in
544
    setIterState checkFinishingState setFinishingStates;
545
    setIterCore checkFinishingCore setFinishingCores;
546
547
    if (setLengthState setPrevUnsatStates) = (setLengthState setUnsatStates) &&
548
      (setLengthCore setPrevUnsatCores) = (setLengthCore setUnsatCores)
549
    then begin
550
        setIterState (fun state -> stateSetStatus state Unsat) setUnsatStates;
551 6aa0e444 Christoph Egger
        setIterCore (fun core -> propagateUnsat [UCore (core, false)]) setUnsatCores;
552 5956a56d Christoph Egger
      end else
553
      fixpointstep setUnsatStates setUnsatCores
554
  in
555
  fixpointstep (setEmptyState ()) (setEmptyCore ())
556
557 4fd28192 Thorsten Wißmann
558
(*****************************************************************************)
559
(*                   Propagation of Nominal Constraints                      *)
560
(*****************************************************************************)
561
562 433c8a2e Thorsten Wißmann
let extractAts sort bs =
563 4fd28192 Thorsten Wißmann
  let ats = csetMake () in
564
  let procNom nom f =
565
    match lfGetType sort f with
566
    | AndF
567
    | OrF -> ()
568 3b055ae8 dirk
    | TrueFalseF
569 4fd28192 Thorsten Wißmann
    | AtF -> ()
570
    | _ -> csetAdd ats (lfGetAt (sort, nom) f)
571
  in
572
  let getAts f =
573
    match lfGetType sort f with
574
    | AtF -> csetAdd ats (lfToAt sort f)
575
    | NomF -> bsetIter (fun f1 -> procNom f f1) bs
576
    | _ -> ()
577
  in
578
  bsetIter getAts bs;
579
  ats
580
581 433c8a2e Thorsten Wißmann
let detConstraintsState state =
582 4fd28192 Thorsten Wißmann
  let procRule accR (_, chldrn) =
583
    let procChldrn accC core =
584
      if coreGetStatus core = Unsat then accC
585
      else cssUnion accC (coreGetConstraints core)
586
    in
587
    let orset = List.fold_left procChldrn cssEmpty chldrn in
588
    let procOrset csetO accO =
589
      let mkUnion csetU accU =
590
        let cset = csetUnion csetO csetU in
591
        cssAdd cset accU
592
      in
593
      cssFold mkUnion accR accO
594
    in
595
    cssFold procOrset orset cssEmpty
596
  in
597
  let sort = stateGetSort state in
598
  let bs = stateGetBs state in
599
  let ats = extractAts sort bs in
600
  if stateGetStatus state = Expandable then csetAddDot ats else ();
601
  List.fold_left procRule (cssSingleton ats) (stateGetRules state)
602
603 433c8a2e Thorsten Wißmann
let detConstraintsCore core =
604 4fd28192 Thorsten Wißmann
  let sort = coreGetSort core in
605
  let bs = coreGetBs core in
606
  let ats = extractAts sort bs in
607
  let addCnstr acc state =
608
    if stateGetStatus state = Unsat then acc
609
    else
610
      let csets = stateGetConstraints state in
611
      (* cssFold (fun c a -> cssAdd (csetUnion c ats) a) csets acc *)
612
      cssUnion csets acc
613
  in
614
  let initInner =
615
    if coreGetStatus core = Expandable then
616
      (* let cset = csetCopy ats in *)
617
      let cset = ats in
618
      csetAddDot cset;
619
      cssSingleton cset
620
    else cssEmpty
621
  in
622
  List.fold_left addCnstr initInner (coreGetChildren core)
623
624 433c8a2e Thorsten Wißmann
let rec propNom = function
625 4fd28192 Thorsten Wißmann
  | [] -> ()
626
  | node::tl ->
627
      let tl1 =
628
        match node with
629
        | State state ->
630
            if stateGetStatus state = Unsat then tl
631
            else
632
              let csets = detConstraintsState state in
633
              let oldcsets = stateGetConstraints state in
634
              if cssEqual csets oldcsets then tl
635
              else begin
636
                stateSetConstraints state csets;
637
                List.fold_left (fun acc c -> (Core c)::acc) tl (stateGetParents state)
638
              end
639
        | Core core ->
640
            if coreGetStatus core = Unsat then tl
641
            else
642
              let csets = detConstraintsCore core in
643
              let oldcsets = coreGetConstraints core in
644
              if cssEqual csets oldcsets then tl
645
              else begin
646
                coreSetConstraints core csets;
647
                List.fold_left (fun acc (s, _) -> (State s)::acc) tl (coreGetParents core)
648
              end
649
      in
650
      propNom tl1
651
652
let updateConstraints node elemU csets =
653
  let update cset acc =
654
    let cnstr =
655
      match graphFindCnstr cset with
656
      | Some cn -> cn
657
      | None ->
658
          let cn = UnexpandedC [] in
659
          graphInsertCnstr cset cn;
660
          queueInsertCnstr cset;
661
          cn
662
    in
663
    match cnstr with
664
    | UnsatC -> acc
665
    | UnexpandedC parents ->
666
        graphReplaceCnstr cset (UnexpandedC (node::parents));
667
        false
668
    | OpenC parents ->
669
        graphReplaceCnstr cset (OpenC (node::parents));
670
        false
671
    | SatC -> false
672
  in
673
  let isUnsat = cssFold update csets true in
674
  if isUnsat then propagateUnsat [elemU] else ()
675
676 433c8a2e Thorsten Wißmann
let propagateNominals () =
677 4fd28192 Thorsten Wißmann
  let init = cssSingleton (csetMake ()) in
678
  graphIterStates (fun s -> if stateGetStatus s = Unsat then () else stateSetConstraints s init);
679
  graphIterCores (fun c -> if coreGetStatus c = Unsat then () else coreSetConstraints c init);
680
  graphIterStates (fun s -> propNom [State s]);
681
  graphIterCores (fun c -> propNom [Core c]);
682
  graphClearCnstr ();
683
  let fktS state =
684
    if stateGetStatus state = Unsat then ()
685
    else updateConstraints (State state) (UState (state, None)) (stateGetConstraints state)
686
  in
687
  graphIterStates fktS;
688
  let fktC core =
689
    if coreGetStatus core = Unsat then ()
690
    else updateConstraints (Core core) (UCore (core, true)) (coreGetConstraints core)
691
  in
692
  graphIterCores fktC
693
694
695
(*****************************************************************************)
696
(*                           Node Expansions                                 *)
697
(*****************************************************************************)
698
699 433c8a2e Thorsten Wißmann
let getLit sort fht solver f =
700 4fd28192 Thorsten Wißmann
  match fhtFind fht f with
701
  | Some lit -> lit
702
  | None ->
703
      let var = M.new_variable solver in
704
      let lit = M.var_to_lit var true in
705
      fhtAdd fht f lit;
706
      let () =
707
        match lfGetNeg sort f with
708
        | None -> ()
709
        | Some nf ->
710
            let nlit = M.neg_lit lit in
711
            fhtAdd fht nf nlit;
712
      in
713
      lit
714
715 16af388e Christoph Egger
let newCore sort bs defer =
716 e0f19999 Thorsten Wißmann
  (* when creating a now core from a set of formulas bs
717
        bs = { x_1, ...., x_n }
718
           = "x_1 /\ .... /\ x_n"
719
     Then we do this by:
720
721
        1. creating a new literal in the sat solver for each
722
           "boolean subformula" from the x_i. "boolean subformula" means that
723
           this subformula is not hidden under modalities but only under
724
           boolean connectives (/\, \/).
725
        2. encoding the relation between a formula and its intermediate boolean
726
           subformulas by a clause:
727
  *)
728 4fd28192 Thorsten Wißmann
  let fht = fhtInit () in
729
  let solver = M.new_solver () in
730 433c8a2e Thorsten Wißmann
  let rec addClauses f =
731 e0f19999 Thorsten Wißmann
    (* step 1: create a literal in the satsolver representing the formula f *)
732 433c8a2e Thorsten Wißmann
    let lf = getLit sort fht solver f in
733 e0f19999 Thorsten Wißmann
    (* step 2: encode relation to possible subformulas *)
734 4fd28192 Thorsten Wißmann
    match lfGetType sort f with
735
    | OrF ->
736 e0f19999 Thorsten Wißmann
        (*
737
           case 2.(a)   f =  f1 \/ f2
738
                   fill fht such that it says:
739
740
                        f  |---> lf
741
                        f1 |---> lf1
742
                        f2 |---> lf2
743
        *)
744 4fd28192 Thorsten Wißmann
        let f1 = lfGetDest1 sort f in
745
        let f2 = lfGetDest2 sort f in
746
        addClauses f1;
747
        addClauses f2;
748
        let lf1 = fhtMustFind fht f1 in
749
        let lf2 = fhtMustFind fht f2 in
750 e0f19999 Thorsten Wißmann
        (*
751
            encode the structure of f by adding the clause (lf -> lf1 \/ lf2)
752
        *)
753 4fd28192 Thorsten Wißmann
        let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in
754
        assert (okay)
755
    | AndF ->
756 e0f19999 Thorsten Wißmann
        (*
757
           case 2.(b)   f =  f1 /\ f2
758
                   fill fht such that it says:
759
760
                        f  |---> lf
761
                        f1 |---> lf1
762
                        f2 |---> lf2
763
        *)
764 4fd28192 Thorsten Wißmann
        let f1 = lfGetDest1 sort f in
765
        let f2 = lfGetDest2 sort f in
766
        addClauses f1;
767
        addClauses f2;
768
        let lf1 = fhtMustFind fht f1 in
769
        let lf2 = fhtMustFind fht f2 in
770 e0f19999 Thorsten Wißmann
        (*
771
            encode the structure of f by adding the clauses
772
                    (lf -> lf1) /\ (lf -> lf2)
773
        *)
774 4fd28192 Thorsten Wißmann
        let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
775
        assert (okay1);
776
        let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in
777
        assert (okay2)
778 3eb8fabd Christoph Egger
    | MuF
779
    | NuF ->
780
       (*
781 9b6bdd74 Christoph Egger
          Dest of a fixpoint is it's unfolded version. This adds just
782
          an simple forward implication that could be optimised out
783
          though not without nontrivial transformation of code
784
785
            f = μ X . φ   |---> lf
786
            φ[X |-> f]    |---> lf1
787
788
          Then adding lf -> lf1 to minisat
789 3eb8fabd Christoph Egger
        *)
790
       let f1 = lfGetDest1 sort f in
791
       addClauses f1;
792
       let lf1 = fhtMustFind fht f1 in
793
       let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
794 9b6bdd74 Christoph Egger
       assert (okay1);
795 4fd28192 Thorsten Wißmann
    | _ -> ()
796 e0f19999 Thorsten Wißmann
        (* case 2.(c)
797
            We don't need to do anything except adding f to the fht
798
        *)
799 4fd28192 Thorsten Wißmann
  in
800
  bsetIter addClauses bs;
801 9f1263ec Christoph Egger
  coreMake sort bs defer (Some solver) fht
802 4fd28192 Thorsten Wißmann
803 433c8a2e Thorsten Wißmann
let getNextState core =
804 e0f19999 Thorsten Wißmann
  (* Create a new state, which is obtained by a satisfying assignment of the
805
     literals of the minisat solver.
806
     In addition to that, feed the negation of the satisfying assignment back
807
     to the minisat solver in order to obtain different solutions on successive
808
     minisat calls.
809
  *)
810 4fd28192 Thorsten Wißmann
  let bs = coreGetBs core in
811 16af388e Christoph Egger
  let refocusing = bsetCompare (bsetMakeRealEmpty ()) (coreGetDeferral core) = 0 in
812
  let deferralS =
813
    if refocusing then
814
      bsetCopy bs
815
    else
816
      coreGetDeferral core
817
  in
818 4fd28192 Thorsten Wißmann
  let fht = coreGetFht core in
819
  let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
820 e0e6eb62 Hans-Peter Deifel
  let solver = coreGetSolver core in
821 4fd28192 Thorsten Wißmann
  let isSat = M.invoke_solver solver litset in
822 e0f19999 Thorsten Wißmann
  (* Clearly, if the current core is unsatisfiable, no further child state can
823
     be created *)
824 4fd28192 Thorsten Wißmann
  if not isSat then None
825
  else
826
    let sort = coreGetSort core in
827 e0f19999 Thorsten Wißmann
    (* create a new set of formulas newbs with the property:
828
       if the conjunction of newbs is satisfiable, then the present core is
829
       satisfiable.
830
    *)
831 4fd28192 Thorsten Wißmann
    let newbs = bsetMake () in
832 16af388e Christoph Egger
    let newdefer = bsetMakeRealEmpty () in
833 e0f19999 Thorsten Wißmann
    (* if newbs = { l_1, .... l_n }, i.e.
834
835
            newbs = l_1 /\ ... /\ l_n
836
837
       then we can get essentially different satisfying assignments of bs by
838
       adding another clause
839
840
            clause = ¬ newbs = ¬l_1 \/ ... \/ ¬l_n
841
842
       By mkExclClause, newbs is filled, and clause is built in the accumulator acc.
843
    *)
844 b395c870 Christoph Egger
    let rec mkExclClause deferral f acc =
845 e0f19999 Thorsten Wißmann
      (* f is a formula that is true in the current satisfying assignment *)
846 4fd28192 Thorsten Wißmann
      match lfGetType sort f with
847 433c8a2e Thorsten Wißmann
      | OrF ->
848 e0f19999 Thorsten Wißmann
          (* if f is true and a disjunction, then one of its disjuncts is true *)
849 4fd28192 Thorsten Wißmann
          let f1 = lfGetDest1 sort f in
850 433c8a2e Thorsten Wißmann
          let lf1 = fhtMustFind fht f1 in
851 e0f19999 Thorsten Wißmann
          (* if the first disjunct f1 is true, then we need to add subformulas
852
             of f1 to newbs&clause *)
853 b395c870 Christoph Egger
          if M.literal_status solver lf1 = M.LTRUE then mkExclClause deferral f1 acc
854 4fd28192 Thorsten Wißmann
          else
855 e0f19999 Thorsten Wißmann
            (* otherwise f2 must be true *)
856 4fd28192 Thorsten Wißmann
            let f2 = lfGetDest2 sort f in
857
            let lf2 = fhtMustFind fht f2 in
858
            assert (M.literal_status solver lf2 = M.LTRUE);
859 b395c870 Christoph Egger
            mkExclClause deferral f2 acc
860 4fd28192 Thorsten Wißmann
      | AndF ->
861 e0f19999 Thorsten Wißmann
          (* if the true f is a conjuction, then both conjunctions must be true *)
862 4fd28192 Thorsten Wißmann
          let f1 = lfGetDest1 sort f in
863
          let lf1 = fhtMustFind fht f1 in
864
          assert (M.literal_status solver lf1 = M.LTRUE);
865 b395c870 Christoph Egger
          let acc1 = mkExclClause deferral f1 acc in
866 4fd28192 Thorsten Wißmann
          let f2 = lfGetDest2 sort f in
867
          let lf2 = fhtMustFind fht f2 in
868
          assert (M.literal_status solver lf2 = M.LTRUE);
869 b395c870 Christoph Egger
          mkExclClause deferral f2 acc1
870 3eb8fabd Christoph Egger
      | MuF
871
      | NuF ->
872
         let f1 = lfGetDest1 sort f in
873 b395c870 Christoph Egger
         mkExclClause deferral f1 acc
874 4fd28192 Thorsten Wißmann
      | _ ->
875 b395c870 Christoph Egger
         (* if f is a trivial formula or modality, then add it ... *)
876
         (* ... to newbs *)
877
         bsetAdd newbs f;
878
         let defercandidate = lfGetDeferral sort f in
879 16af388e Christoph Egger
         (if (defercandidate != (Hashtbl.hash "ε") &&
880
                (refocusing || deferral = defercandidate)) then
881 b395c870 Christoph Egger
            bsetAdd newdefer f);
882
         (* ... and to the new clause *)
883
         (M.neg_lit (fhtMustFind fht f))::acc
884 4fd28192 Thorsten Wißmann
    in
885 b395c870 Christoph Egger
    let init_clause f acc =
886
      let deferral =
887 07c71f1c Christoph Egger
        (* for each deferral determine which variable it belongs to *)
888 16af388e Christoph Egger
        if bsetMem deferralS f then (
889
          lfGetDeferral sort f)
890 b395c870 Christoph Egger
        else
891
          (Hashtbl.hash "ε")
892
      in
893
      mkExclClause deferral f acc
894
    in
895
    let clause = bsetFold init_clause bs [] in
896 433c8a2e Thorsten Wißmann
    let okay = M.add_clause solver clause in
897 4fd28192 Thorsten Wißmann
    assert (okay);
898 b395c870 Christoph Egger
    Some (sort, newbs, newdefer)
899 4fd28192 Thorsten Wißmann
900 b395c870 Christoph Egger
let newState sort bs defer =
901 4fd28192 Thorsten Wißmann
  let (func, sl) = !sortTable.(sort) in
902
  let producer = CoAlgLogics.getExpandingFunctionProducer func in
903 16af388e Christoph Egger
  let exp = producer sort bs defer sl in
904 b395c870 Christoph Egger
  stateMake sort bs defer exp
905 4fd28192 Thorsten Wißmann
906 b395c870 Christoph Egger
let insertState parent sort bs defer =
907 4fd28192 Thorsten Wißmann
  let child =
908 16af388e Christoph Egger
    match graphFindState sort (bs, defer) with
909 4fd28192 Thorsten Wißmann
    | None ->
910 b395c870 Christoph Egger
        let s = newState sort bs defer in
911 16af388e Christoph Egger
        graphInsertState sort (bs, defer) s;
912 4fd28192 Thorsten Wißmann
        queueInsertState s;
913
        s
914
    | Some s -> s
915
  in
916
  coreAddChild parent child;
917
  stateAddParent child parent
918
919
let expandCore core =
920
  match getNextState core with
921 b395c870 Christoph Egger
  | Some (sort, bs, defer) ->
922
      insertState core sort bs defer;
923 4fd28192 Thorsten Wißmann
      queueInsertCore core
924
  | None ->
925
      let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in
926 6aa0e444 Christoph Egger
      if isUnsat
927
      then
928
          propagateUnsat [UCore (core, false)]
929
      else
930
          coreSetStatus core Open
931 4fd28192 Thorsten Wißmann
932
933 16af388e Christoph Egger
let insertCore sort bs defer =
934
  match graphFindCore sort (bs, defer) with
935 4fd28192 Thorsten Wißmann
  | None ->
936 16af388e Christoph Egger
     let c = newCore sort bs defer in
937
     graphInsertCore sort (bs, defer) c;
938
     queueInsertCore c;
939
     c
940 4fd28192 Thorsten Wißmann
  | Some c -> c
941
942 e7aaefa9 Hans-Peter Deifel
(** Insert cores for the children generated by a modal rule application.
943
  *
944
  * @return true if all new cores are already unsatisfiable, false otherwise
945
  *)
946 433c8a2e Thorsten Wißmann
let insertRule state dep chldrn =
947
  let chldrn = listFromLazylist chldrn in
948 93ef4736 Hans-Peter Deifel
  let mkCores (sort, bs, defer) =
949 4fd28192 Thorsten Wißmann
    let bs1 = bsetAddTBox sort bs in
950 b6653b96 Hans-Peter Deifel
    (* For the aconjunctive fragment, instead of adding a core annotated with
951 93ef4736 Hans-Peter Deifel
     * all deferrals, we add a core for each formula in the deferral set. *)
952 e7aaefa9 Hans-Peter Deifel
    let deferSingletons =
953 b6653b96 Hans-Peter Deifel
      if getFragment () = AconjunctiveAltFree
954
         && bsetCompare defer (bsetMakeRealEmpty ()) <> 0 then
955
        bsetFold (fun f list -> bsetSingleton f::list) defer []
956 e7aaefa9 Hans-Peter Deifel
      else
957 b6653b96 Hans-Peter Deifel
        [defer] in
958 93ef4736 Hans-Peter Deifel
    List.map (insertCore sort (bsetCopy bs1)) deferSingletons
959 4fd28192 Thorsten Wißmann
  in
960 93ef4736 Hans-Peter Deifel
  (* A list of cores for each child: [[child1a;child1b]; [child2a;child2b]] *)
961
  let coresPerChild = List.map mkCores chldrn in
962
  (* All combinations that take a core from each child:
963
   * [[ch1a;ch2a]; [ch1a;ch2b]; [ch1b;ch2a]; [ch1b;ch2b]]
964
   * Neccesary because stateAddRule expects each child to have only one core. *)
965
  let coresPerRule = CU.TList.combinations coresPerChild in
966
  let addRule cores =
967
    let idx = stateAddRule state dep cores in
968
    List.iter (fun c -> coreAddParent c state idx) cores;
969
    if List.for_all (fun core -> coreGetStatus core = Unsat) cores then begin
970
      propagateUnsat [UState (state, Some idx)];
971
      true
972
    end else 
973
      false
974
  in
975
  List.mem true (List.map (fun r -> addRule r) coresPerRule)
976
  
977 433c8a2e Thorsten Wißmann
978 e7aaefa9 Hans-Peter Deifel
(** Call insertRule on all rules
979
  * @return true if any rule application generated only unsat cores
980
  *)
981
let rec insertAllRules state rules =
982 93ef4736 Hans-Peter Deifel
  List.mem true (List.map (fun (dep, children) -> insertRule state dep children) rules)
983 4fd28192 Thorsten Wißmann
984
let expandState state =
985 433c8a2e Thorsten Wißmann
  match stateNextRule state with
986 69243f7f Thorsten Wißmann
  | MultipleElements rules ->
987 e7aaefa9 Hans-Peter Deifel
      let unsat = insertAllRules state rules in
988
      if not unsat then stateSetStatus state Open
989 69243f7f Thorsten Wißmann
  | SingleElement (dep, chldrn) ->
990 e7aaefa9 Hans-Peter Deifel
      let unsat = insertRule state dep chldrn in
991
      if not unsat then queueInsertState state else ()
992 69243f7f Thorsten Wißmann
  | NoMoreElements -> stateSetStatus state Open
993 4fd28192 Thorsten Wißmann
994
995
let expandCnstr cset =
996
  let nht = nhtInit () in
997
  let mkCores f =
998
    let (sort, lf) as nom = atFormulaGetNominal f in
999
    let nomset =
1000
      match nhtFind nht nom with
1001
      | Some ns -> ns
1002
      | None ->
1003
          let cset1 = csetCopy cset in
1004
          csetRemDot cset1;
1005
          let bs = csetAddTBox sort cset1 in
1006
          bsetAdd bs lf;
1007
          nhtAdd nht nom bs;
1008
          bs
1009
    in
1010
    bsetAdd nomset (atFormulaGetSubformula f)
1011
  in
1012
  csetIter cset mkCores;
1013
  let inCores (sort, _) bs (isUns, acc) =
1014 16af388e Christoph Egger
    let core = insertCore sort bs bs in (* TODO: think of deferral / μ stuff here *)
1015 4fd28192 Thorsten Wißmann
    coreAddConstraintParent core cset;
1016
    (coreGetStatus core = Unsat || isUns, core::acc)
1017
  in
1018
  let (isUnsat, children) = nhtFold inCores nht (false, []) in
1019
  if isUnsat then propagateUnsat [UCnstr cset]
1020
  else
1021
    match graphFindCnstr cset with
1022
    | Some (UnexpandedC parents) -> graphReplaceCnstr cset (OpenC parents)
1023
    | _ -> assert false
1024
1025
1026
(*****************************************************************************)
1027
(*                           The Main Loop                                   *)
1028
(*****************************************************************************)
1029
1030 2679ab63 Thorsten Wißmann
let expandNodesLoop (recursiveAction: unit -> unit) =
1031 4fd28192 Thorsten Wißmann
  match queueGetElement () with
1032
  | QState state ->
1033
      if stateGetStatus state = Expandable then begin
1034
        expandState state;
1035
        if doNominalPropagation () then begin
1036 1c26e356 Christoph Egger
          (* propagateNominals (); *)
1037 31229254 Christoph Egger
          if doSatPropagation () then (propagateUnsatMu (); propagateSatMu ())
1038 4fd28192 Thorsten Wißmann
        end else ()
1039
      end else ();
1040 2679ab63 Thorsten Wißmann
      recursiveAction ()
1041 4fd28192 Thorsten Wißmann
  | QCore core ->
1042
      if coreGetStatus core = Expandable then begin
1043
        expandCore core;
1044
        if doNominalPropagation () then begin
1045 1c26e356 Christoph Egger
          (* propagateNominals (); *)
1046 31229254 Christoph Egger
          if doSatPropagation () then (propagateUnsatMu (); propagateSatMu ())
1047 4fd28192 Thorsten Wißmann
        end else ()
1048
      end else ();
1049 2679ab63 Thorsten Wißmann
      recursiveAction ()
1050 4fd28192 Thorsten Wißmann
  | QCnstr cset ->
1051
      expandCnstr cset;
1052 2679ab63 Thorsten Wißmann
      recursiveAction ()
1053 4fd28192 Thorsten Wißmann
  | QEmpty -> ()
1054
1055 c2cc0c2e Thorsten Wißmann
let runReasonerStep () =
1056 2679ab63 Thorsten Wißmann
  let void () = () in
1057
  expandNodesLoop void; (* expand at most one node *)
1058 371cb823 Hans-Peter Deifel
  propagateUnsatMu ();
1059 2679ab63 Thorsten Wißmann
  (* if this emptied the queue *)
1060
  if queueIsEmpty () then begin
1061
    (* then check whether the nominals would add further queue elements *)
1062 1c26e356 Christoph Egger
    (* print_endline "Propagating nominals..."; *)
1063
    (* propagateNominals () *)
1064 2679ab63 Thorsten Wißmann
  end else () (* else: the next step would be to expand another node *)
1065 c2cc0c2e Thorsten Wißmann
1066
let rec buildGraphLoop () =
1067 2679ab63 Thorsten Wißmann
  let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in
1068
  expandNodesFurther (); (* expand as many queue elements as possible *)
1069 1c26e356 Christoph Egger
  (* propagateNominals (); *)
1070 2679ab63 Thorsten Wißmann
  (* if propagating nominals added some more queue members, do all again.. *)
1071 4fd28192 Thorsten Wißmann
  if queueIsEmpty () then () else buildGraphLoop ()
1072 c2cc0c2e Thorsten Wißmann
1073 f24367c4 Hans-Peter Deifel
let initReasoner fragSpec sorts nomTable tbox sf =
1074 c2cc0c2e Thorsten Wißmann
  sortTable := Array.copy sorts;
1075 f24367c4 Hans-Peter Deifel
  let (tbox1, sf1, bs) = ppFormulae fragSpec nomTable tbox sf in
1076 c2cc0c2e Thorsten Wißmann
  let sort = fst sf in
1077
  let bs1 = bsetAddTBox sort bs in
1078 16af388e Christoph Egger
  let deferrals = bsetMakeRealEmpty() in
1079
  let markDeferral f =
1080
    if (Hashtbl.hash "ε") != (lfGetDeferral sort f) then (
1081
      bsetAdd deferrals f;)
1082
  in
1083
  bsetIter markDeferral bs;
1084 c2cc0c2e Thorsten Wißmann
  graphInit ();
1085
  queueInit ();
1086 16af388e Christoph Egger
  let root = insertCore sort bs1 deferrals in
1087 c2cc0c2e Thorsten Wißmann
  graphAddRoot root
1088
1089
let isRootSat () =
1090
  match coreGetStatus (graphGetRoot ()) with
1091
  | Expandable -> None
1092
  | Unsat -> Some false
1093 c4142480 Christoph Egger
  | Sat -> Some true
1094 86948fae Christoph Egger
  | Open -> if (queueIsEmpty()) then Some true else None
1095 c2cc0c2e Thorsten Wißmann
1096
let reasonerFinished () =
1097
  match coreGetStatus (graphGetRoot ()) with
1098
  | Expandable -> false
1099
  | Unsat
1100
  | Sat  -> true
1101
  | Open -> queueIsEmpty ()
1102 3eb8fabd Christoph Egger
1103 c2cc0c2e Thorsten Wißmann
1104 4fd28192 Thorsten Wißmann
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
1105
    @param verbose An optional switch which determines
1106
    whether the procedure shall print some information on the standard output.
1107
    The default is false.
1108
    @param sorts An array mapping each sort (represented as an integer)
1109
    to a functor and a list of sorts which are the arguments of the functor.
1110
    @param nomTable A partial function mapping nominals (represented as strings)
1111
    to their sorts.
1112
    @param tbox A list of sorted formulae.
1113
    @param sf A sorted formula.
1114
    @return True if sf is satisfiable wrt tbox, false otherwise.
1115
 *)
1116 c2cc0c2e Thorsten Wißmann
1117 f24367c4 Hans-Peter Deifel
let isSat ?(verbose = false) fragSpec sorts nomTable tbox sf =
1118 4fd28192 Thorsten Wißmann
  let start = if verbose then Unix.gettimeofday () else 0. in
1119 f24367c4 Hans-Peter Deifel
  initReasoner fragSpec sorts nomTable tbox sf;
1120 4fd28192 Thorsten Wißmann
  let sat =
1121
    try
1122
      buildGraphLoop ();
1123 e4faff97 Christoph Egger
      propagateUnsatMu ();
1124 c2cc0c2e Thorsten Wißmann
      (* get whether the root is satisfiable *)
1125
      (* we know that the reasoner finished, so the value is there, *)
1126
      (* i.e. isRootSat() will give a "Some x" and not "None" *)
1127
      CU.fromSome (isRootSat())
1128 4fd28192 Thorsten Wißmann
    with CoAlg_finished res -> res
1129
  in
1130 c2cc0c2e Thorsten Wißmann
  (* print some statistics *)
1131 4fd28192 Thorsten Wißmann
  if verbose then
1132
    let stop = Unix.gettimeofday () in
1133
    let addup lst = List.fold_left (fun acc sf -> acc + (CoAlgFormula.sizeSortedFormula sf)) 0 lst in
1134
    print_newline ();
1135
    print_endline ("Query: " ^ (CoAlgFormula.exportQuery tbox sf));
1136
    let size = (CoAlgFormula.sizeSortedFormula sf) + (addup tbox) in
1137
    print_endline ("Added Size: " ^ (string_of_int size));
1138 c2cc0c2e Thorsten Wißmann
    (*
1139 4fd28192 Thorsten Wißmann
    print_endline ("Negation Normal Form: " ^ (CoAlgFormula.exportQuery tbox1 sf1));
1140
    let nsize = (CoAlgFormula.sizeSortedFormula sf1) + (addup tbox1) in
1141
    print_endline ("Added Size: " ^ (string_of_int nsize));
1142 c2cc0c2e Thorsten Wißmann
    *)
1143 4fd28192 Thorsten Wißmann
    print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable.");
1144
    print_endline ("Time: " ^ (string_of_float (stop -. start)));
1145
    print_endline ("Generated states: " ^ (string_of_int (graphSizeState ())));
1146
    print_endline ("Generated cores: " ^ (string_of_int (graphSizeCore ())));
1147
    print_endline ("Generated constraints: " ^ (string_of_int (graphSizeCnstr ())));
1148
    print_newline ()
1149
  else ();
1150
  sat
1151 a57eb439 Hans-Peter Deifel
1152
(* vim: set et sw=2 sts=2 ts=8 : *)