Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ 7b21fbae

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
let rec propSat setStates setCores setCnstr = function
37
  | [] -> ()
38
  | propElem::tl ->
39
      let tl1 =
40
        match propElem with
41
        | UState (state, _) ->
42
            if setMemState setStates state then
43
              let cnstrs = stateGetConstraints state in
44
              let isStillOpen = cssExists (fun c -> propSatFindSucc setCnstr c) cnstrs in
45
              if isStillOpen then () else setRemoveState setStates state
46
            else ();
47
            tl
48
        | UCore (core, _) ->
49
            if setMemCore setCores core then
50
              let cnstrs = coreGetConstraints core in
51
              let isStillOpen = cssExists (fun c -> propSatFindSucc setCnstr c) cnstrs in
52
              if isStillOpen then tl else begin
53
                setRemoveCore setCores core;
54
                let cnstrPar = coreGetConstraintParents core in
55
                List.fold_left (fun acc cset -> (UCnstr cset)::acc) tl cnstrPar
56
              end
57
            else tl
58
        | UCnstr cset ->
59
            if setMemCnstr setCnstr cset then begin
60
              setRemoveCnstr setCnstr cset;
61
              match graphFindCnstr cset with
62
              | Some (OpenC nodes) ->
63
                  let prop acc node =
64
                    match node with
65
                    | Core core -> (UCore (core, true))::acc
66
                    | State state -> (UState (state, None))::acc
67
                  in
68
                  List.fold_left prop tl nodes
69
              | _ -> assert false
70
            end else tl
71
      in
72
      propSat setStates setCores setCnstr tl1
73

    
74
let propagateSat () =
75
  let setStates = setEmptyState () in
76
  let setCores = setEmptyCore () in
77
  let setCnstr = setEmptyCnstr () in
78
  let fktS1 state =
79
    match stateGetStatus state with
80
    | Expandable
81
    | Open -> setAddState setStates state
82
    | Unsat
83
    | Sat -> ()
84
  in
85
  graphIterStates fktS1;
86
  let fktC1 core =
87
    match coreGetStatus core with
88
    | Expandable
89
    | Open -> setAddCore setCores core
90
    | Unsat
91
    | Sat -> ()
92
  in
93
  graphIterCores fktC1;
94
  let cfkt1 cset cnstr =
95
    if csetHasDot cset then ()
96
    else
97
      match cnstr with
98
      | OpenC _ -> setAddCnstr setCnstr cset
99
      | UnsatC
100
      | SatC
101
      | UnexpandedC _ -> ()
102
  in
103
  graphIterCnstrs cfkt1;
104
  graphIterStates (fun state -> propSat setStates setCores setCnstr [UState (state, None)]);
105
  graphIterCores (fun core -> propSat setStates setCores setCnstr [UCore (core, false)]);
106
  setIterState (fun state -> stateSetStatus state Sat) setStates;
107
  let setCoreSat core =
108
    coreSetStatus core Sat;
109
    if core == graphGetRoot () then raise (CoAlg_finished true) else ()
110
  in
111
  setIterCore setCoreSat setCores;
112
  setIterCnstr (fun cset -> graphReplaceCnstr cset SatC) setCnstr
113

    
114

    
115
(*****************************************************************************)
116
(*                     Propagation of Unsatisfiability                       *)
117
(*****************************************************************************)
118

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

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

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

    
135

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

    
261

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

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

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

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

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

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

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

    
398

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    
632

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

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

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

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

    
674

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

    
705

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

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

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

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

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

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

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

    
782

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

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