Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ 6d64bc5a

History | View | Annotate | Download (28.4 KB)

1
(** 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
module CU = CoolUtils
11

    
12
type sortTable = CoAlgMisc.sortTable
13

    
14
type nomTable = string -> CoAlgFormula.sort option
15

    
16
type assumptions = CoAlgFormula.sortedFormula list
17

    
18
type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula
19

    
20
exception ReasonerError of string
21

    
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
    | None -> raise (ReasonerError "?")
31
    | Some SatC -> true
32
    | Some (OpenC _) -> setMemCnstr setCnstr cset
33
    | Some (UnexpandedC _)
34
    | Some UnsatC -> false
35

    
36

    
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
(*****************************************************************************)
117
(*                     Propagation of Unsatisfiability                       *)
118
(*****************************************************************************)
119

    
120
let isConstraintUnsat cset =
121
  match graphFindCnstr cset with
122
  | None -> assert false
123
  | Some UnsatC -> true
124
  | _ -> false
125

    
126
let fhtMustFind fht f =
127
  match fhtFind fht f with
128
  | Some l -> l
129
  | None -> assert false
130

    
131
let lhtMustFind lht l =
132
  match lhtFind lht l with
133
  | Some f -> f
134
  | None -> assert false
135

    
136

    
137
(* Gets a list of Things we know are unsatisfiable and propagates this
138
   information backwards *)
139
let rec propagateUnsat = function
140
  | [] -> ()
141
  | propElem::tl ->
142
      let tl1 =
143
        match propElem with
144
        | UState (state, idxopt) -> begin
145
            match stateGetStatus state with
146
            | Unsat -> tl
147
            | Sat -> raise (ReasonerError ("Propagation tells state "
148
                                           ^(string_of_int (stateGetIdx state))
149
                                           ^" would be unsat, but it is already sat"))
150
            | Open
151
            | Expandable ->
152
                let mbs =
153
                  match idxopt with
154
                  | None -> stateGetBs state
155
                  | Some idx ->
156
                      let (dep, children) = stateGetRule state idx in
157
                      let getBs core =
158
                        assert (coreGetStatus core = Unsat);
159
                        coreGetBs core
160
                      in
161
                      dep (List.map getBs children)
162
                in
163
                stateSetBs state mbs;
164
                stateSetStatus state Unsat;
165
                let prop acc core =
166
                  let turnsUnsat =
167
                    match coreGetStatus core with
168
                    | Open -> List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core)
169
                    | Expandable
170
                    | Unsat
171
                    | Sat -> false
172
                  in
173
                  if turnsUnsat then (UCore (core, false))::acc else acc
174
                in
175
                List.fold_left prop tl (stateGetParents state)
176
          end
177
        | UCore (core, comesFromCnstr) -> begin
178
            match coreGetStatus core with
179
            | Unsat -> tl
180
            | Sat -> raise (ReasonerError ("Propagation tells core "
181
                                           ^(string_of_int (coreGetIdx core))
182
                                           ^" would be unsat, but it is already sat"))
183
            | Open
184
            | Expandable ->
185
                let mbs =
186
                  if comesFromCnstr then coreGetBs core
187
                  else
188
                    let bs = coreGetBs core in
189
                    let solver = coreGetSolver core in
190
                    let fht = coreGetFht core in
191
                    let lht = lhtInit () in
192
                    let addLits f acc =
193
                      let lit = fhtMustFind fht f in
194
                      lhtAdd lht lit f;
195
                      lit::acc
196
                    in
197
                    let litset = bsetFold addLits bs [] in
198
                    let addClauses state =
199
                      let cbs = stateGetBs state in
200
                      let clause = bsetFold (fun f acc -> (M.neg_lit (fhtMustFind fht f))::acc) cbs [] in
201
                      let okay = M.add_clause solver clause in
202
                      assert okay
203
                    in
204
                    List.iter addClauses (coreGetChildren core);
205
                    let isSat = M.invoke_solver solver litset in
206
                    assert (not isSat);
207
                    let res = bsetMake () in
208
                    let confls = M.get_conflict solver in
209
                    List.iter (fun l -> bsetAdd res (lhtMustFind lht l)) confls;
210
                    res
211
                in
212
                coreSetBs core mbs;
213
                coreSetStatus core Unsat;
214
                if core == graphGetRoot () then raise (CoAlg_finished false) else ();
215
                let prop acc (state, idx) =
216
                  let turnsUnsat =
217
                    match stateGetStatus state with
218
                    | Open
219
                    | Expandable ->
220
                        List.for_all (fun c -> coreGetStatus c = Unsat) (snd (stateGetRule state idx))
221
                    | Unsat
222
                    | Sat -> false
223
                  in
224
                  if turnsUnsat then (UState (state, Some idx))::acc else acc
225
                in
226
                let tl2 = List.fold_left prop tl (coreGetParents core) in
227
                List.fold_left (fun acc cset -> (UCnstr cset)::acc) tl2 (coreGetConstraintParents core)
228
          end
229
        | UCnstr cset ->
230
            match graphFindCnstr cset with
231
            | None
232
            | Some SatC -> assert false
233
            | Some UnsatC -> tl
234
            | Some (UnexpandedC nodes)
235
            | Some (OpenC nodes) ->
236
                graphReplaceCnstr cset UnsatC;
237
                let prop acc node =
238
                  match node with
239
                  | State state ->
240
                      let turnsUnsat =
241
                        match stateGetStatus state with
242
                        | Expandable
243
                        | Open -> cssForall isConstraintUnsat (stateGetConstraints state)
244
                        | Unsat
245
                        | Sat -> false
246
                      in
247
                      if turnsUnsat then (UState (state, None))::acc else acc
248
                  | Core core ->
249
                      let turnsUnsat =
250
                        match coreGetStatus core with
251
                        | Expandable
252
                        | Open -> cssForall isConstraintUnsat (coreGetConstraints core)
253
                        | Unsat
254
                        | Sat -> false
255
                      in
256
                      if turnsUnsat then (UCore (core, true))::acc else acc
257
                in
258
                List.fold_left prop tl nodes
259
      in
260
      propagateUnsat tl1
261

    
262

    
263
(*****************************************************************************)
264
(*                   Propagation of Nominal Constraints                      *)
265
(*****************************************************************************)
266

    
267
let extractAts sort bs =
268
  let ats = csetMake () in
269
  let procNom nom f =
270
    match lfGetType sort f with
271
    | AndF
272
    | OrF -> ()
273
    | TrueFalseF
274
    | AtF -> ()
275
    | _ -> csetAdd ats (lfGetAt (sort, nom) f)
276
  in
277
  let getAts f =
278
    match lfGetType sort f with
279
    | AtF -> csetAdd ats (lfToAt sort f)
280
    | NomF -> bsetIter (fun f1 -> procNom f f1) bs
281
    | _ -> ()
282
  in
283
  bsetIter getAts bs;
284
  ats
285

    
286
let detConstraintsState state =
287
  let procRule accR (_, chldrn) =
288
    let procChldrn accC core =
289
      if coreGetStatus core = Unsat then accC
290
      else cssUnion accC (coreGetConstraints core)
291
    in
292
    let orset = List.fold_left procChldrn cssEmpty chldrn in
293
    let procOrset csetO accO =
294
      let mkUnion csetU accU =
295
        let cset = csetUnion csetO csetU in
296
        cssAdd cset accU
297
      in
298
      cssFold mkUnion accR accO
299
    in
300
    cssFold procOrset orset cssEmpty
301
  in
302
  let sort = stateGetSort state in
303
  let bs = stateGetBs state in
304
  let ats = extractAts sort bs in
305
  if stateGetStatus state = Expandable then csetAddDot ats else ();
306
  List.fold_left procRule (cssSingleton ats) (stateGetRules state)
307

    
308
let detConstraintsCore core =
309
  let sort = coreGetSort core in
310
  let bs = coreGetBs core in
311
  let ats = extractAts sort bs in
312
  let addCnstr acc state =
313
    if stateGetStatus state = Unsat then acc
314
    else
315
      let csets = stateGetConstraints state in
316
      (* cssFold (fun c a -> cssAdd (csetUnion c ats) a) csets acc *)
317
      cssUnion csets acc
318
  in
319
  let initInner =
320
    if coreGetStatus core = Expandable then
321
      (* let cset = csetCopy ats in *)
322
      let cset = ats in
323
      csetAddDot cset;
324
      cssSingleton cset
325
    else cssEmpty
326
  in
327
  List.fold_left addCnstr initInner (coreGetChildren core)
328

    
329
let rec propNom = function
330
  | [] -> ()
331
  | node::tl ->
332
      let tl1 =
333
        match node with
334
        | State state ->
335
            if stateGetStatus state = Unsat then tl
336
            else
337
              let csets = detConstraintsState state in
338
              let oldcsets = stateGetConstraints state in
339
              if cssEqual csets oldcsets then tl
340
              else begin
341
                stateSetConstraints state csets;
342
                List.fold_left (fun acc c -> (Core c)::acc) tl (stateGetParents state)
343
              end
344
        | Core core ->
345
            if coreGetStatus core = Unsat then tl
346
            else
347
              let csets = detConstraintsCore core in
348
              let oldcsets = coreGetConstraints core in
349
              if cssEqual csets oldcsets then tl
350
              else begin
351
                coreSetConstraints core csets;
352
                List.fold_left (fun acc (s, _) -> (State s)::acc) tl (coreGetParents core)
353
              end
354
      in
355
      propNom tl1
356

    
357
let updateConstraints node elemU csets =
358
  let update cset acc =
359
    let cnstr =
360
      match graphFindCnstr cset with
361
      | Some cn -> cn
362
      | None ->
363
          let cn = UnexpandedC [] in
364
          graphInsertCnstr cset cn;
365
          queueInsertCnstr cset;
366
          cn
367
    in
368
    match cnstr with
369
    | UnsatC -> acc
370
    | UnexpandedC parents ->
371
        graphReplaceCnstr cset (UnexpandedC (node::parents));
372
        false
373
    | OpenC parents ->
374
        graphReplaceCnstr cset (OpenC (node::parents));
375
        false
376
    | SatC -> false
377
  in
378
  let isUnsat = cssFold update csets true in
379
  if isUnsat then propagateUnsat [elemU] else ()
380

    
381
let propagateNominals () =
382
  let init = cssSingleton (csetMake ()) in
383
  graphIterStates (fun s -> if stateGetStatus s = Unsat then () else stateSetConstraints s init);
384
  graphIterCores (fun c -> if coreGetStatus c = Unsat then () else coreSetConstraints c init);
385
  graphIterStates (fun s -> propNom [State s]);
386
  graphIterCores (fun c -> propNom [Core c]);
387
  graphClearCnstr ();
388
  let fktS state =
389
    if stateGetStatus state = Unsat then ()
390
    else updateConstraints (State state) (UState (state, None)) (stateGetConstraints state)
391
  in
392
  graphIterStates fktS;
393
  let fktC core =
394
    if coreGetStatus core = Unsat then ()
395
    else updateConstraints (Core core) (UCore (core, true)) (coreGetConstraints core)
396
  in
397
  graphIterCores fktC
398

    
399

    
400
(*****************************************************************************)
401
(*                           Node Expansions                                 *)
402
(*****************************************************************************)
403

    
404
let getLit sort fht solver f =
405
  match fhtFind fht f with
406
  | Some lit -> lit
407
  | None ->
408
      let var = M.new_variable solver in
409
      let lit = M.var_to_lit var true in
410
      fhtAdd fht f lit;
411
      let () =
412
        match lfGetNeg sort f with
413
        | None -> ()
414
        | Some nf ->
415
            let nlit = M.neg_lit lit in
416
            fhtAdd fht nf nlit;
417
      in
418
      lit
419

    
420
let newCore sort bs defer =
421
  (* when creating a now core from a set of formulas bs
422
        bs = { x_1, ...., x_n }
423
           = "x_1 /\ .... /\ x_n"
424
     Then we do this by:
425

    
426
        1. creating a new literal in the sat solver for each
427
           "boolean subformula" from the x_i. "boolean subformula" means that
428
           this subformula is not hidden under modalities but only under
429
           boolean connectives (/\, \/).
430
        2. encoding the relation between a formula and its intermediate boolean
431
           subformulas by a clause:
432
  *)
433
  let fht = fhtInit () in
434
  let solver = M.new_solver () in
435
  let rec addClauses f =
436
    (* step 1: create a literal in the satsolver representing the formula f *)
437
    let lf = getLit sort fht solver f in
438
    (* step 2: encode relation to possible subformulas *)
439
    match lfGetType sort f with
440
    | OrF ->
441
        (*
442
           case 2.(a)   f =  f1 \/ f2
443
                   fill fht such that it says:
444

    
445
                        f  |---> lf
446
                        f1 |---> lf1
447
                        f2 |---> lf2
448
        *)
449
        let f1 = lfGetDest1 sort f in
450
        let f2 = lfGetDest2 sort f in
451
        addClauses f1;
452
        addClauses f2;
453
        let lf1 = fhtMustFind fht f1 in
454
        let lf2 = fhtMustFind fht f2 in
455
        (*
456
            encode the structure of f by adding the clause (lf -> lf1 \/ lf2)
457
        *)
458
        let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in
459
        assert (okay)
460
    | AndF ->
461
        (*
462
           case 2.(b)   f =  f1 /\ f2
463
                   fill fht such that it says:
464

    
465
                        f  |---> lf
466
                        f1 |---> lf1
467
                        f2 |---> lf2
468
        *)
469
        let f1 = lfGetDest1 sort f in
470
        let f2 = lfGetDest2 sort f in
471
        addClauses f1;
472
        addClauses f2;
473
        let lf1 = fhtMustFind fht f1 in
474
        let lf2 = fhtMustFind fht f2 in
475
        (*
476
            encode the structure of f by adding the clauses
477
                    (lf -> lf1) /\ (lf -> lf2)
478
        *)
479
        let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
480
        assert (okay1);
481
        let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in
482
        assert (okay2)
483
    | MuF
484
    | NuF ->
485
       (*
486
          Dest of a fixpoint is it's unfolded version. This adds just
487
          an simple forward implication that could be optimised out
488
          though not without nontrivial transformation of code
489

    
490
            f = μ X . φ   |---> lf
491
            φ[X |-> f]    |---> lf1
492

    
493
          Then adding lf -> lf1 to minisat
494
        *)
495
       let f1 = lfGetDest1 sort f in
496
       addClauses f1;
497
       let lf1 = fhtMustFind fht f1 in
498
       let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
499
       assert (okay1);
500
    | _ -> ()
501
        (* case 2.(c)
502
            We don't need to do anything except adding f to the fht
503
        *)
504
  in
505
  bsetIter addClauses bs;
506
  coreMake sort bs defer solver fht
507

    
508
let getNextState core =
509
  (* Create a new state, which is obtained by a satisfying assignment of the
510
     literals of the minisat solver.
511
     In addition to that, feed the negation of the satisfying assignment back
512
     to the minisat solver in order to obtain different solutions on successive
513
     minisat calls.
514
  *)
515
  let bs = coreGetBs core in
516
  let refocusing = bsetCompare (bsetMakeRealEmpty ()) (coreGetDeferral core) = 0 in
517
  let deferralS =
518
    if refocusing then
519
      bsetCopy bs
520
    else
521
      coreGetDeferral core
522
  in
523
  let fht = coreGetFht core in
524
  let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
525
  let solver = coreGetSolver core in
526
  let isSat = M.invoke_solver solver litset in
527
  (* Clearly, if the current core is unsatisfiable, no further child state can
528
     be created *)
529
  if not isSat then None
530
  else
531
    let sort = coreGetSort core in
532
    (* create a new set of formulas newbs with the property:
533
       if the conjunction of newbs is satisfiable, then the present core is
534
       satisfiable.
535
    *)
536
    let newbs = bsetMake () in
537
    let newdefer = bsetMakeRealEmpty () in
538
    (* if newbs = { l_1, .... l_n }, i.e.
539

    
540
            newbs = l_1 /\ ... /\ l_n
541

    
542
       then we can get essentially different satisfying assignments of bs by
543
       adding another clause
544

    
545
            clause = ¬ newbs = ¬l_1 \/ ... \/ ¬l_n
546

    
547
       By mkExclClause, newbs is filled, and clause is built in the accumulator acc.
548
    *)
549
    let rec mkExclClause deferral f acc =
550
      (* f is a formula that is true in the current satisfying assignment *)
551
      match lfGetType sort f with
552
      | OrF ->
553
          (* if f is true and a disjunction, then one of its disjuncts is true *)
554
          let f1 = lfGetDest1 sort f in
555
          let lf1 = fhtMustFind fht f1 in
556
          (* if the first disjunct f1 is true, then we need to add subformulas
557
             of f1 to newbs&clause *)
558
          if M.literal_status solver lf1 = M.LTRUE then mkExclClause deferral f1 acc
559
          else
560
            (* otherwise f2 must be true *)
561
            let f2 = lfGetDest2 sort f in
562
            let lf2 = fhtMustFind fht f2 in
563
            assert (M.literal_status solver lf2 = M.LTRUE);
564
            mkExclClause deferral f2 acc
565
      | AndF ->
566
          (* if the true f is a conjuction, then both conjunctions must be true *)
567
          let f1 = lfGetDest1 sort f in
568
          let lf1 = fhtMustFind fht f1 in
569
          assert (M.literal_status solver lf1 = M.LTRUE);
570
          let acc1 = mkExclClause deferral f1 acc in
571
          let f2 = lfGetDest2 sort f in
572
          let lf2 = fhtMustFind fht f2 in
573
          assert (M.literal_status solver lf2 = M.LTRUE);
574
          mkExclClause deferral f2 acc1
575
      | MuF
576
      | NuF ->
577
         let f1 = lfGetDest1 sort f in
578
         mkExclClause deferral f1 acc
579
      | _ ->
580
         (* if f is a trivial formula or modality, then add it ... *)
581
         (* ... to newbs *)
582
         bsetAdd newbs f;
583
         let defercandidate = lfGetDeferral sort f in
584
         (if (defercandidate != (Hashtbl.hash "ε") &&
585
                (refocusing || deferral = defercandidate)) then
586
            bsetAdd newdefer f);
587
         (* ... and to the new clause *)
588
         (M.neg_lit (fhtMustFind fht f))::acc
589
    in
590
    let init_clause f acc =
591
      let deferral =
592
        if bsetMem deferralS f then (
593
          lfGetDeferral sort f)
594
        else
595
          (Hashtbl.hash "ε")
596
      in
597
      mkExclClause deferral f acc
598
    in
599
    let clause = bsetFold init_clause bs [] in
600
    let okay = M.add_clause solver clause in
601
    assert (okay);
602
    Some (sort, newbs, newdefer)
603

    
604
let newState sort bs defer =
605
  let (func, sl) = !sortTable.(sort) in
606
  let producer = CoAlgLogics.getExpandingFunctionProducer func in
607
  let exp = producer sort bs defer sl in
608
  stateMake sort bs defer exp
609

    
610
let insertState parent sort bs defer =
611
  let child =
612
    match graphFindState sort (bs, defer) with
613
    | None ->
614
        let s = newState sort bs defer in
615
        graphInsertState sort (bs, defer) s;
616
        queueInsertState s;
617
        s
618
    | Some s -> s
619
  in
620
  coreAddChild parent child;
621
  stateAddParent child parent
622

    
623
let expandCore core =
624
  match getNextState core with
625
  | Some (sort, bs, defer) ->
626
      insertState core sort bs defer;
627
      queueInsertCore core
628
  | None ->
629
      let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in
630
      if isUnsat then propagateUnsat [UCore (core, false)]
631
      else coreSetStatus core Open
632

    
633

    
634
let insertCore sort bs defer =
635
  match graphFindCore sort (bs, defer) with
636
  | None ->
637
     let c = newCore sort bs defer in
638
     graphInsertCore sort (bs, defer) c;
639
     queueInsertCore c;
640
     c
641
  | Some c -> c
642

    
643
let insertRule state dep chldrn =
644
  let chldrn = listFromLazylist chldrn in
645
  let insert (isUns, acc) (sort, bs, defer) =
646
    let bs1 = bsetAddTBox sort bs in
647
    let core = insertCore sort bs1 defer in
648
    let isUns1 = if coreGetStatus core = Unsat then isUns else false in
649
    (isUns1, core::acc)
650
  in
651
  let (isUnsat, children) = List.fold_left insert (true, []) chldrn in
652
  let idx = stateAddRule state dep (List.rev children) in
653
  List.iter (fun c -> coreAddParent c state idx) children;
654
  if isUnsat then begin
655
    propagateUnsat [UState (state, Some idx)];
656
    false
657
  end else true
658

    
659
let rec insertAllRules state = function
660
  | [] -> true
661
  | (dep, chldrn)::tl ->
662
      let notUnsat = insertRule state dep chldrn in
663
      if notUnsat then insertAllRules state tl else false
664

    
665
let expandState state =
666
  match stateNextRule state with
667
  | MultipleElements rules ->
668
      let notUnsat = insertAllRules state rules in
669
      if notUnsat then stateSetStatus state Open
670
  | SingleElement (dep, chldrn) ->
671
      let notUnsat = insertRule state dep chldrn in
672
      if notUnsat then queueInsertState state else ()
673
  | NoMoreElements -> stateSetStatus state Open
674

    
675

    
676
let expandCnstr cset =
677
  let nht = nhtInit () in
678
  let mkCores f =
679
    let (sort, lf) as nom = atFormulaGetNominal f in
680
    let nomset =
681
      match nhtFind nht nom with
682
      | Some ns -> ns
683
      | None ->
684
          let cset1 = csetCopy cset in
685
          csetRemDot cset1;
686
          let bs = csetAddTBox sort cset1 in
687
          bsetAdd bs lf;
688
          nhtAdd nht nom bs;
689
          bs
690
    in
691
    bsetAdd nomset (atFormulaGetSubformula f)
692
  in
693
  csetIter cset mkCores;
694
  let inCores (sort, _) bs (isUns, acc) =
695
    let core = insertCore sort bs bs in (* TODO: think of deferral / μ stuff here *)
696
    coreAddConstraintParent core cset;
697
    (coreGetStatus core = Unsat || isUns, core::acc)
698
  in
699
  let (isUnsat, children) = nhtFold inCores nht (false, []) in
700
  if isUnsat then propagateUnsat [UCnstr cset]
701
  else
702
    match graphFindCnstr cset with
703
    | Some (UnexpandedC parents) -> graphReplaceCnstr cset (OpenC parents)
704
    | _ -> assert false
705

    
706

    
707
(*****************************************************************************)
708
(*                           The Main Loop                                   *)
709
(*****************************************************************************)
710

    
711
let expandNodesLoop (recursiveAction: unit -> unit) =
712
  match queueGetElement () with
713
  | QState state ->
714
      if stateGetStatus state = Expandable then begin
715
        expandState state;
716
        if doNominalPropagation () then begin
717
          propagateNominals ();
718
          if doSatPropagation () then propagateSat ()
719
        end else ()
720
      end else ();
721
      recursiveAction ()
722
  | QCore core ->
723
      if coreGetStatus core = Expandable then begin
724
        expandCore core;
725
        if doNominalPropagation () then begin
726
          propagateNominals ();
727
          if doSatPropagation () then propagateSat ()
728
        end else ()
729
      end else ();
730
      recursiveAction ()
731
  | QCnstr cset ->
732
      expandCnstr cset;
733
      recursiveAction ()
734
  | QEmpty -> ()
735

    
736
let runReasonerStep () =
737
  let void () = () in
738
  expandNodesLoop void; (* expand at most one node *)
739
  (* if this emptied the queue *)
740
  if queueIsEmpty () then begin
741
    (* then check whether the nominals would add further queue elements *)
742
    print_endline "Propagating nominals...";
743
    propagateNominals ()
744
  end else () (* else: the next step would be to expand another node *)
745

    
746
let rec buildGraphLoop () =
747
  let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in
748
  expandNodesFurther (); (* expand as many queue elements as possible *)
749
  propagateNominals ();
750
  (* if propagating nominals added some more queue members, do all again.. *)
751
  if queueIsEmpty () then () else buildGraphLoop ()
752

    
753
let initReasoner sorts nomTable tbox sf =
754
  sortTable := Array.copy sorts;
755
  let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in
756
  let sort = fst sf in
757
  let bs1 = bsetAddTBox sort bs in
758
  let deferrals = bsetMakeRealEmpty() in
759
  let markDeferral f =
760
    if (Hashtbl.hash "ε") != (lfGetDeferral sort f) then (
761
      bsetAdd deferrals f;)
762
  in
763
  bsetIter markDeferral bs;
764
  graphInit ();
765
  queueInit ();
766
  let root = insertCore sort bs1 deferrals in
767
  graphAddRoot root
768

    
769
let isRootSat () =
770
  match coreGetStatus (graphGetRoot ()) with
771
  | Expandable -> None
772
  | Unsat -> Some false
773
  | Sat
774
  | Open -> if (queueIsEmpty()) then Some true else None
775

    
776
let reasonerFinished () =
777
  match coreGetStatus (graphGetRoot ()) with
778
  | Expandable -> false
779
  | Unsat
780
  | Sat  -> true
781
  | Open -> queueIsEmpty ()
782

    
783

    
784
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
785
    @param verbose An optional switch which determines
786
    whether the procedure shall print some information on the standard output.
787
    The default is false.
788
    @param sorts An array mapping each sort (represented as an integer)
789
    to a functor and a list of sorts which are the arguments of the functor.
790
    @param nomTable A partial function mapping nominals (represented as strings)
791
    to their sorts.
792
    @param tbox A list of sorted formulae.
793
    @param sf A sorted formula.
794
    @return True if sf is satisfiable wrt tbox, false otherwise.
795
 *)
796

    
797
let isSat ?(verbose = false) sorts nomTable tbox sf =
798
  let start = if verbose then Unix.gettimeofday () else 0. in
799
  initReasoner sorts nomTable tbox sf;
800
  let sat =
801
    try
802
      buildGraphLoop ();
803
      (* get whether the root is satisfiable *)
804
      (* we know that the reasoner finished, so the value is there, *)
805
      (* i.e. isRootSat() will give a "Some x" and not "None" *)
806
      CU.fromSome (isRootSat())
807
    with CoAlg_finished res -> res
808
  in
809
  (* print some statistics *)
810
  if verbose then
811
    let stop = Unix.gettimeofday () in
812
    let addup lst = List.fold_left (fun acc sf -> acc + (CoAlgFormula.sizeSortedFormula sf)) 0 lst in
813
    print_newline ();
814
    print_endline ("Query: " ^ (CoAlgFormula.exportQuery tbox sf));
815
    let size = (CoAlgFormula.sizeSortedFormula sf) + (addup tbox) in
816
    print_endline ("Added Size: " ^ (string_of_int size));
817
    (*
818
    print_endline ("Negation Normal Form: " ^ (CoAlgFormula.exportQuery tbox1 sf1));
819
    let nsize = (CoAlgFormula.sizeSortedFormula sf1) + (addup tbox1) in
820
    print_endline ("Added Size: " ^ (string_of_int nsize));
821
    *)
822
    print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable.");
823
    print_endline ("Time: " ^ (string_of_float (stop -. start)));
824
    print_endline ("Generated states: " ^ (string_of_int (graphSizeState ())));
825
    print_endline ("Generated cores: " ^ (string_of_int (graphSizeCore ())));
826
    print_endline ("Generated constraints: " ^ (string_of_int (graphSizeCnstr ())));
827
    print_newline ()
828
  else ();
829
  sat