Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ 67b07e54

History | View | Annotate | Download (32.6 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
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

    
123
  let stateCollector state =
124
    match stateGetStatus state with
125
    | Unsat
126
    | Sat -> ()
127
    | Expandable
128
    | Open ->
129
       setAddState setStates state;
130
       if bsetCompare (stateGetDeferral state) emptySet == 0
131
       then begin
132
           print_endline (stateToString state);
133
           setAddState setFinishingStates state
134
         end
135
       else ()
136
  in
137
  let coreCollector core =
138
    match coreGetStatus core with
139
    | Unsat
140
    | Sat -> ()
141
    | Expandable
142
    | Open ->
143
       setAddCore setCores core;
144
       if bsetCompare (coreGetDeferral core) emptySet == 0
145
       then begin
146
           print_endline (coreToString core);
147
           setAddCore setFinishingCores core
148
         end
149
       else ()
150
  in
151
  graphIterStates stateCollector;
152
  graphIterCores coreCollector;
153

    
154
  (*
155
    In a fixpoint the set called setStates / setCores is narrowed down.
156

    
157
    In each step only those states and cores are retained in setStates
158
    / setCores which reach one of setFinishing{States,Cores} in
159
    finitely many steps. This new set of States / Cores is collected
160
    as allowed{States,Cores} during each fixpoint iteration.
161

    
162
    Only those finishing nodes are retained that have allowed or
163
    Successfull Children.
164
  *)
165

    
166
  let rec fixpointstep setStates setCores =
167
    let allowedStates = setEmptyState () in
168
    let allowedCores = setEmptyCore () in
169
    let initialStates = setEmptyState () in
170
    let initialCores = setEmptyCore () in
171

    
172
    let checkFinishingState (state : state) =
173
      let ruleiter (dependencies, corelist) : bool =
174
        List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable) corelist
175
      in
176
      if not (List.exists ruleiter (stateGetRules state)) then begin
177
        setAddState allowedStates state;
178
        setAddState initialStates state
179
      end
180
    in
181
    let checkFinishingCore (core : core) =
182
      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable)
183
                (coreGetChildren core)) then begin
184
        setAddCore allowedCores core;
185
        setAddCore initialCores core
186
      end
187
    in
188
    setIterState checkFinishingState setFinishingStates;
189
    setIterCore checkFinishingCore setFinishingCores;
190

    
191
    let rec visitParentStates (core : core) : unit =
192
      if not (setMemCore setCores core) then ()
193
      else begin
194
        let children = coreGetChildren core in
195
        let acceptable =
196
          List.exists (fun (state : state) -> setMemState allowedStates state || stateGetStatus state == Sat)
197
            children
198
        in
199
        if acceptable then begin
200
          print_endline ("Considering Core " ^ (string_of_int (coreGetIdx core)) ^ " as allowed");
201
          setAddCore allowedCores core;
202
          List.iter (fun (state, _) -> visitParentCores state)
203
            (coreGetParents core)
204
        end
205
      end
206

    
207
    and visitParentCores (state : state) : unit =
208
      if not (setMemState setStates state) then ()
209
      else begin
210
        let rules = stateGetRules state in
211
        let ruleiter (dependencies, corelist) =
212
          List.exists (fun (core : core) -> setMemCore allowedCores core || coreGetStatus core == Sat)
213
            corelist
214
        in
215
        let acceptable = List.for_all ruleiter rules in
216
        if acceptable then begin
217
          print_endline ("Considering State " ^ (string_of_int (stateGetIdx state)) ^ " as allowed");
218
          setAddState allowedStates state;
219
          List.iter (fun core -> if not (setMemCore allowedCores core) then visitParentStates core)
220
            (stateGetParents state)
221
        end
222
      end
223
    in
224

    
225
    setIterState visitParentCores initialStates;
226
    setIterCore visitParentStates initialCores;
227

    
228
    if (setLengthState setStates) = (setLengthState allowedStates) &&
229
      (setLengthCore setCores) = (setLengthCore allowedCores)
230
    then begin
231
      setIterState (fun state -> stateSetStatus state Sat) setStates;
232
      setIterCore (fun core -> coreSetStatus core Sat) setCores;
233
    end else
234
      fixpointstep allowedStates allowedCores
235
  in
236
  fixpointstep setStates setCores
237

    
238

    
239
(*****************************************************************************)
240
(*                     Propagation of Unsatisfiability                       *)
241
(*****************************************************************************)
242

    
243
let isConstraintUnsat cset =
244
  match graphFindCnstr cset with
245
  | None -> assert false
246
  | Some UnsatC -> true
247
  | _ -> false
248

    
249
let fhtMustFind fht f =
250
  match fhtFind fht f with
251
  | Some l -> l
252
  | None -> assert false
253

    
254
let lhtMustFind lht l =
255
  match lhtFind lht l with
256
  | Some f -> f
257
  | None -> assert false
258

    
259

    
260
(* Gets a list of Things we know are unsatisfiable and propagates this
261
   information backwards *)
262
let rec propagateUnsat = function
263
  | [] -> ()
264
  | propElem::tl ->
265
      let tl1 =
266
        match propElem with
267
        | UState (state, idxopt) -> begin
268
            match stateGetStatus state with
269
            | Unsat -> tl
270
            | Sat -> raise (ReasonerError ("Propagation tells state "
271
                                           ^(string_of_int (stateGetIdx state))
272
                                           ^" would be unsat, but it is already sat"))
273
            | Open
274
            | Expandable ->
275
                let mbs =
276
                  match idxopt with
277
                  | None -> stateGetBs state
278
                  | Some idx ->
279
                      let (dep, children) = stateGetRule state idx in
280
                      let getBs core =
281
                        assert (coreGetStatus core = Unsat);
282
                        coreGetBs core
283
                      in
284
                      dep (List.map getBs children)
285
                in
286
                stateSetBs state mbs;
287
                stateSetStatus state Unsat;
288
                let prop acc core =
289
                  let turnsUnsat =
290
                    match coreGetStatus core with
291
                    | Open -> List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core)
292
                    | Expandable
293
                    | Unsat
294
                    | Sat -> false
295
                  in
296
                  if turnsUnsat then (UCore (core, false))::acc else acc
297
                in
298
                List.fold_left prop tl (stateGetParents state)
299
          end
300
        | UCore (core, comesFromCnstr) -> begin
301
            match coreGetStatus core with
302
            | Unsat -> tl
303
            | Sat -> raise (ReasonerError ("Propagation tells core "
304
                                           ^(string_of_int (coreGetIdx core))
305
                                           ^" would be unsat, but it is already sat"))
306
            | Open
307
            | Expandable ->
308
                let mbs =
309
                  if comesFromCnstr then coreGetBs core
310
                  else
311
                    let bs = coreGetBs core in
312
                    let solver = coreGetSolver core in
313
                    let fht = coreGetFht core in
314
                    let lht = lhtInit () in
315
                    let addLits f acc =
316
                      let lit = fhtMustFind fht f in
317
                      lhtAdd lht lit f;
318
                      lit::acc
319
                    in
320
                    let litset = bsetFold addLits bs [] in
321
                    let addClauses state =
322
                      let cbs = stateGetBs state in
323
                      let clause = bsetFold (fun f acc -> (M.neg_lit (fhtMustFind fht f))::acc) cbs [] in
324
                      let okay = M.add_clause solver clause in
325
                      assert okay
326
                    in
327
                    List.iter addClauses (coreGetChildren core);
328
                    let isSat = M.invoke_solver solver litset in
329
                    assert (not isSat);
330
                    let res = bsetMake () in
331
                    let confls = M.get_conflict solver in
332
                    List.iter (fun l -> bsetAdd res (lhtMustFind lht l)) confls;
333
                    res
334
                in
335
                coreSetBs core mbs;
336
                coreSetStatus core Unsat;
337
                if core == graphGetRoot () then raise (CoAlg_finished false) else ();
338
                let prop acc (state, idx) =
339
                  let turnsUnsat =
340
                    match stateGetStatus state with
341
                    | Open
342
                    | Expandable ->
343
                        List.for_all (fun c -> coreGetStatus c = Unsat) (snd (stateGetRule state idx))
344
                    | Unsat
345
                    | Sat -> false
346
                  in
347
                  if turnsUnsat then (UState (state, Some idx))::acc else acc
348
                in
349
                let tl2 = List.fold_left prop tl (coreGetParents core) in
350
                List.fold_left (fun acc cset -> (UCnstr cset)::acc) tl2 (coreGetConstraintParents core)
351
          end
352
        | UCnstr cset ->
353
            match graphFindCnstr cset with
354
            | None
355
            | Some SatC -> assert false
356
            | Some UnsatC -> tl
357
            | Some (UnexpandedC nodes)
358
            | Some (OpenC nodes) ->
359
                graphReplaceCnstr cset UnsatC;
360
                let prop acc node =
361
                  match node with
362
                  | State state ->
363
                      let turnsUnsat =
364
                        match stateGetStatus state with
365
                        | Expandable
366
                        | Open -> cssForall isConstraintUnsat (stateGetConstraints state)
367
                        | Unsat
368
                        | Sat -> false
369
                      in
370
                      if turnsUnsat then (UState (state, None))::acc else acc
371
                  | Core core ->
372
                      let turnsUnsat =
373
                        match coreGetStatus core with
374
                        | Expandable
375
                        | Open -> cssForall isConstraintUnsat (coreGetConstraints core)
376
                        | Unsat
377
                        | Sat -> false
378
                      in
379
                      if turnsUnsat then (UCore (core, true))::acc else acc
380
                in
381
                List.fold_left prop tl nodes
382
      in
383
      propagateUnsat tl1
384

    
385

    
386
(*****************************************************************************)
387
(*                   Propagation of Nominal Constraints                      *)
388
(*****************************************************************************)
389

    
390
let extractAts sort bs =
391
  let ats = csetMake () in
392
  let procNom nom f =
393
    match lfGetType sort f with
394
    | AndF
395
    | OrF -> ()
396
    | TrueFalseF
397
    | AtF -> ()
398
    | _ -> csetAdd ats (lfGetAt (sort, nom) f)
399
  in
400
  let getAts f =
401
    match lfGetType sort f with
402
    | AtF -> csetAdd ats (lfToAt sort f)
403
    | NomF -> bsetIter (fun f1 -> procNom f f1) bs
404
    | _ -> ()
405
  in
406
  bsetIter getAts bs;
407
  ats
408

    
409
let detConstraintsState state =
410
  let procRule accR (_, chldrn) =
411
    let procChldrn accC core =
412
      if coreGetStatus core = Unsat then accC
413
      else cssUnion accC (coreGetConstraints core)
414
    in
415
    let orset = List.fold_left procChldrn cssEmpty chldrn in
416
    let procOrset csetO accO =
417
      let mkUnion csetU accU =
418
        let cset = csetUnion csetO csetU in
419
        cssAdd cset accU
420
      in
421
      cssFold mkUnion accR accO
422
    in
423
    cssFold procOrset orset cssEmpty
424
  in
425
  let sort = stateGetSort state in
426
  let bs = stateGetBs state in
427
  let ats = extractAts sort bs in
428
  if stateGetStatus state = Expandable then csetAddDot ats else ();
429
  List.fold_left procRule (cssSingleton ats) (stateGetRules state)
430

    
431
let detConstraintsCore core =
432
  let sort = coreGetSort core in
433
  let bs = coreGetBs core in
434
  let ats = extractAts sort bs in
435
  let addCnstr acc state =
436
    if stateGetStatus state = Unsat then acc
437
    else
438
      let csets = stateGetConstraints state in
439
      (* cssFold (fun c a -> cssAdd (csetUnion c ats) a) csets acc *)
440
      cssUnion csets acc
441
  in
442
  let initInner =
443
    if coreGetStatus core = Expandable then
444
      (* let cset = csetCopy ats in *)
445
      let cset = ats in
446
      csetAddDot cset;
447
      cssSingleton cset
448
    else cssEmpty
449
  in
450
  List.fold_left addCnstr initInner (coreGetChildren core)
451

    
452
let rec propNom = function
453
  | [] -> ()
454
  | node::tl ->
455
      let tl1 =
456
        match node with
457
        | State state ->
458
            if stateGetStatus state = Unsat then tl
459
            else
460
              let csets = detConstraintsState state in
461
              let oldcsets = stateGetConstraints state in
462
              if cssEqual csets oldcsets then tl
463
              else begin
464
                stateSetConstraints state csets;
465
                List.fold_left (fun acc c -> (Core c)::acc) tl (stateGetParents state)
466
              end
467
        | Core core ->
468
            if coreGetStatus core = Unsat then tl
469
            else
470
              let csets = detConstraintsCore core in
471
              let oldcsets = coreGetConstraints core in
472
              if cssEqual csets oldcsets then tl
473
              else begin
474
                coreSetConstraints core csets;
475
                List.fold_left (fun acc (s, _) -> (State s)::acc) tl (coreGetParents core)
476
              end
477
      in
478
      propNom tl1
479

    
480
let updateConstraints node elemU csets =
481
  let update cset acc =
482
    let cnstr =
483
      match graphFindCnstr cset with
484
      | Some cn -> cn
485
      | None ->
486
          let cn = UnexpandedC [] in
487
          graphInsertCnstr cset cn;
488
          queueInsertCnstr cset;
489
          cn
490
    in
491
    match cnstr with
492
    | UnsatC -> acc
493
    | UnexpandedC parents ->
494
        graphReplaceCnstr cset (UnexpandedC (node::parents));
495
        false
496
    | OpenC parents ->
497
        graphReplaceCnstr cset (OpenC (node::parents));
498
        false
499
    | SatC -> false
500
  in
501
  let isUnsat = cssFold update csets true in
502
  if isUnsat then propagateUnsat [elemU] else ()
503

    
504
let propagateNominals () =
505
  let init = cssSingleton (csetMake ()) in
506
  graphIterStates (fun s -> if stateGetStatus s = Unsat then () else stateSetConstraints s init);
507
  graphIterCores (fun c -> if coreGetStatus c = Unsat then () else coreSetConstraints c init);
508
  graphIterStates (fun s -> propNom [State s]);
509
  graphIterCores (fun c -> propNom [Core c]);
510
  graphClearCnstr ();
511
  let fktS state =
512
    if stateGetStatus state = Unsat then ()
513
    else updateConstraints (State state) (UState (state, None)) (stateGetConstraints state)
514
  in
515
  graphIterStates fktS;
516
  let fktC core =
517
    if coreGetStatus core = Unsat then ()
518
    else updateConstraints (Core core) (UCore (core, true)) (coreGetConstraints core)
519
  in
520
  graphIterCores fktC
521

    
522

    
523
(*****************************************************************************)
524
(*                           Node Expansions                                 *)
525
(*****************************************************************************)
526

    
527
let getLit sort fht solver f =
528
  match fhtFind fht f with
529
  | Some lit -> lit
530
  | None ->
531
      let var = M.new_variable solver in
532
      let lit = M.var_to_lit var true in
533
      fhtAdd fht f lit;
534
      let () =
535
        match lfGetNeg sort f with
536
        | None -> ()
537
        | Some nf ->
538
            let nlit = M.neg_lit lit in
539
            fhtAdd fht nf nlit;
540
      in
541
      lit
542

    
543
let newCore sort bs defer =
544
  (* when creating a now core from a set of formulas bs
545
        bs = { x_1, ...., x_n }
546
           = "x_1 /\ .... /\ x_n"
547
     Then we do this by:
548

    
549
        1. creating a new literal in the sat solver for each
550
           "boolean subformula" from the x_i. "boolean subformula" means that
551
           this subformula is not hidden under modalities but only under
552
           boolean connectives (/\, \/).
553
        2. encoding the relation between a formula and its intermediate boolean
554
           subformulas by a clause:
555
  *)
556
  let fht = fhtInit () in
557
  let solver = M.new_solver () in
558
  let rec addClauses f =
559
    (* step 1: create a literal in the satsolver representing the formula f *)
560
    let lf = getLit sort fht solver f in
561
    (* step 2: encode relation to possible subformulas *)
562
    match lfGetType sort f with
563
    | OrF ->
564
        (*
565
           case 2.(a)   f =  f1 \/ f2
566
                   fill fht such that it says:
567

    
568
                        f  |---> lf
569
                        f1 |---> lf1
570
                        f2 |---> lf2
571
        *)
572
        let f1 = lfGetDest1 sort f in
573
        let f2 = lfGetDest2 sort f in
574
        addClauses f1;
575
        addClauses f2;
576
        let lf1 = fhtMustFind fht f1 in
577
        let lf2 = fhtMustFind fht f2 in
578
        (*
579
            encode the structure of f by adding the clause (lf -> lf1 \/ lf2)
580
        *)
581
        let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in
582
        assert (okay)
583
    | AndF ->
584
        (*
585
           case 2.(b)   f =  f1 /\ f2
586
                   fill fht such that it says:
587

    
588
                        f  |---> lf
589
                        f1 |---> lf1
590
                        f2 |---> lf2
591
        *)
592
        let f1 = lfGetDest1 sort f in
593
        let f2 = lfGetDest2 sort f in
594
        addClauses f1;
595
        addClauses f2;
596
        let lf1 = fhtMustFind fht f1 in
597
        let lf2 = fhtMustFind fht f2 in
598
        (*
599
            encode the structure of f by adding the clauses
600
                    (lf -> lf1) /\ (lf -> lf2)
601
        *)
602
        let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
603
        assert (okay1);
604
        let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in
605
        assert (okay2)
606
    | MuF
607
    | NuF ->
608
       (*
609
          Dest of a fixpoint is it's unfolded version. This adds just
610
          an simple forward implication that could be optimised out
611
          though not without nontrivial transformation of code
612

    
613
            f = μ X . φ   |---> lf
614
            φ[X |-> f]    |---> lf1
615

    
616
          Then adding lf -> lf1 to minisat
617
        *)
618
       let f1 = lfGetDest1 sort f in
619
       addClauses f1;
620
       let lf1 = fhtMustFind fht f1 in
621
       let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
622
       assert (okay1);
623
    | _ -> ()
624
        (* case 2.(c)
625
            We don't need to do anything except adding f to the fht
626
        *)
627
  in
628
  bsetIter addClauses bs;
629
  coreMake sort bs defer solver fht
630

    
631
let getNextState core =
632
  (* Create a new state, which is obtained by a satisfying assignment of the
633
     literals of the minisat solver.
634
     In addition to that, feed the negation of the satisfying assignment back
635
     to the minisat solver in order to obtain different solutions on successive
636
     minisat calls.
637
  *)
638
  let bs = coreGetBs core in
639
  let refocusing = bsetCompare (bsetMakeRealEmpty ()) (coreGetDeferral core) = 0 in
640
  let deferralS =
641
    if refocusing then
642
      bsetCopy bs
643
    else
644
      coreGetDeferral core
645
  in
646
  let fht = coreGetFht core in
647
  let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
648
  let solver = coreGetSolver core in
649
  let isSat = M.invoke_solver solver litset in
650
  (* Clearly, if the current core is unsatisfiable, no further child state can
651
     be created *)
652
  if not isSat then None
653
  else
654
    let sort = coreGetSort core in
655
    (* create a new set of formulas newbs with the property:
656
       if the conjunction of newbs is satisfiable, then the present core is
657
       satisfiable.
658
    *)
659
    let newbs = bsetMake () in
660
    let newdefer = bsetMakeRealEmpty () in
661
    (* if newbs = { l_1, .... l_n }, i.e.
662

    
663
            newbs = l_1 /\ ... /\ l_n
664

    
665
       then we can get essentially different satisfying assignments of bs by
666
       adding another clause
667

    
668
            clause = ¬ newbs = ¬l_1 \/ ... \/ ¬l_n
669

    
670
       By mkExclClause, newbs is filled, and clause is built in the accumulator acc.
671
    *)
672
    let rec mkExclClause deferral f acc =
673
      (* f is a formula that is true in the current satisfying assignment *)
674
      match lfGetType sort f with
675
      | OrF ->
676
          (* if f is true and a disjunction, then one of its disjuncts is true *)
677
          let f1 = lfGetDest1 sort f in
678
          let lf1 = fhtMustFind fht f1 in
679
          (* if the first disjunct f1 is true, then we need to add subformulas
680
             of f1 to newbs&clause *)
681
          if M.literal_status solver lf1 = M.LTRUE then mkExclClause deferral f1 acc
682
          else
683
            (* otherwise f2 must be true *)
684
            let f2 = lfGetDest2 sort f in
685
            let lf2 = fhtMustFind fht f2 in
686
            assert (M.literal_status solver lf2 = M.LTRUE);
687
            mkExclClause deferral f2 acc
688
      | AndF ->
689
          (* if the true f is a conjuction, then both conjunctions must be true *)
690
          let f1 = lfGetDest1 sort f in
691
          let lf1 = fhtMustFind fht f1 in
692
          assert (M.literal_status solver lf1 = M.LTRUE);
693
          let acc1 = mkExclClause deferral f1 acc in
694
          let f2 = lfGetDest2 sort f in
695
          let lf2 = fhtMustFind fht f2 in
696
          assert (M.literal_status solver lf2 = M.LTRUE);
697
          mkExclClause deferral f2 acc1
698
      | MuF
699
      | NuF ->
700
         let f1 = lfGetDest1 sort f in
701
         mkExclClause deferral f1 acc
702
      | _ ->
703
         (* if f is a trivial formula or modality, then add it ... *)
704
         (* ... to newbs *)
705
         bsetAdd newbs f;
706
         let defercandidate = lfGetDeferral sort f in
707
         (if (defercandidate != (Hashtbl.hash "ε") &&
708
                (refocusing || deferral = defercandidate)) then
709
            bsetAdd newdefer f);
710
         (* ... and to the new clause *)
711
         (M.neg_lit (fhtMustFind fht f))::acc
712
    in
713
    let init_clause f acc =
714
      let deferral =
715
        if bsetMem deferralS f then (
716
          lfGetDeferral sort f)
717
        else
718
          (Hashtbl.hash "ε")
719
      in
720
      mkExclClause deferral f acc
721
    in
722
    let clause = bsetFold init_clause bs [] in
723
    let okay = M.add_clause solver clause in
724
    assert (okay);
725
    Some (sort, newbs, newdefer)
726

    
727
let newState sort bs defer =
728
  let (func, sl) = !sortTable.(sort) in
729
  let producer = CoAlgLogics.getExpandingFunctionProducer func in
730
  let exp = producer sort bs defer sl in
731
  stateMake sort bs defer exp
732

    
733
let insertState parent sort bs defer =
734
  let child =
735
    match graphFindState sort (bs, defer) with
736
    | None ->
737
        let s = newState sort bs defer in
738
        graphInsertState sort (bs, defer) s;
739
        queueInsertState s;
740
        s
741
    | Some s -> s
742
  in
743
  coreAddChild parent child;
744
  stateAddParent child parent
745

    
746
let expandCore core =
747
  match getNextState core with
748
  | Some (sort, bs, defer) ->
749
      insertState core sort bs defer;
750
      queueInsertCore core
751
  | None ->
752
      let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in
753
      if isUnsat then propagateUnsat [UCore (core, false)]
754
      else coreSetStatus core Open
755

    
756

    
757
let insertCore sort bs defer =
758
  match graphFindCore sort (bs, defer) with
759
  | None ->
760
     let c = newCore sort bs defer in
761
     graphInsertCore sort (bs, defer) c;
762
     queueInsertCore c;
763
     c
764
  | Some c -> c
765

    
766
let insertRule state dep chldrn =
767
  let chldrn = listFromLazylist chldrn in
768
  let insert (isUns, acc) (sort, bs, defer) =
769
    let bs1 = bsetAddTBox sort bs in
770
    let core = insertCore sort bs1 defer in
771
    let isUns1 = if coreGetStatus core = Unsat then isUns else false in
772
    (isUns1, core::acc)
773
  in
774
  let (isUnsat, children) = List.fold_left insert (true, []) chldrn in
775
  let idx = stateAddRule state dep (List.rev children) in
776
  List.iter (fun c -> coreAddParent c state idx) children;
777
  if isUnsat then begin
778
    propagateUnsat [UState (state, Some idx)];
779
    false
780
  end else true
781

    
782
let rec insertAllRules state = function
783
  | [] -> true
784
  | (dep, chldrn)::tl ->
785
      let notUnsat = insertRule state dep chldrn in
786
      if notUnsat then insertAllRules state tl else false
787

    
788
let expandState state =
789
  match stateNextRule state with
790
  | MultipleElements rules ->
791
      let notUnsat = insertAllRules state rules in
792
      if notUnsat then stateSetStatus state Open
793
  | SingleElement (dep, chldrn) ->
794
      let notUnsat = insertRule state dep chldrn in
795
      if notUnsat then queueInsertState state else ()
796
  | NoMoreElements -> stateSetStatus state Open
797

    
798

    
799
let expandCnstr cset =
800
  let nht = nhtInit () in
801
  let mkCores f =
802
    let (sort, lf) as nom = atFormulaGetNominal f in
803
    let nomset =
804
      match nhtFind nht nom with
805
      | Some ns -> ns
806
      | None ->
807
          let cset1 = csetCopy cset in
808
          csetRemDot cset1;
809
          let bs = csetAddTBox sort cset1 in
810
          bsetAdd bs lf;
811
          nhtAdd nht nom bs;
812
          bs
813
    in
814
    bsetAdd nomset (atFormulaGetSubformula f)
815
  in
816
  csetIter cset mkCores;
817
  let inCores (sort, _) bs (isUns, acc) =
818
    let core = insertCore sort bs bs in (* TODO: think of deferral / μ stuff here *)
819
    coreAddConstraintParent core cset;
820
    (coreGetStatus core = Unsat || isUns, core::acc)
821
  in
822
  let (isUnsat, children) = nhtFold inCores nht (false, []) in
823
  if isUnsat then propagateUnsat [UCnstr cset]
824
  else
825
    match graphFindCnstr cset with
826
    | Some (UnexpandedC parents) -> graphReplaceCnstr cset (OpenC parents)
827
    | _ -> assert false
828

    
829

    
830
(*****************************************************************************)
831
(*                           The Main Loop                                   *)
832
(*****************************************************************************)
833

    
834
let expandNodesLoop (recursiveAction: unit -> unit) =
835
  match queueGetElement () with
836
  | QState state ->
837
      if stateGetStatus state = Expandable then begin
838
        expandState state;
839
        if doNominalPropagation () then begin
840
          propagateNominals ();
841
          if doSatPropagation () then propagateSatMu ()
842
        end else ()
843
      end else ();
844
      recursiveAction ()
845
  | QCore core ->
846
      if coreGetStatus core = Expandable then begin
847
        expandCore core;
848
        if doNominalPropagation () then begin
849
          propagateNominals ();
850
          if doSatPropagation () then propagateSatMu ()
851
        end else ()
852
      end else ();
853
      recursiveAction ()
854
  | QCnstr cset ->
855
      expandCnstr cset;
856
      recursiveAction ()
857
  | QEmpty -> ()
858

    
859
let runReasonerStep () =
860
  let void () = () in
861
  expandNodesLoop void; (* expand at most one node *)
862
  (* if this emptied the queue *)
863
  if queueIsEmpty () then begin
864
    (* then check whether the nominals would add further queue elements *)
865
    print_endline "Propagating nominals...";
866
    propagateNominals ()
867
  end else () (* else: the next step would be to expand another node *)
868

    
869
let rec buildGraphLoop () =
870
  let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in
871
  expandNodesFurther (); (* expand as many queue elements as possible *)
872
  propagateNominals ();
873
  (* if propagating nominals added some more queue members, do all again.. *)
874
  if queueIsEmpty () then () else buildGraphLoop ()
875

    
876
let initReasoner sorts nomTable tbox sf =
877
  sortTable := Array.copy sorts;
878
  let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in
879
  let sort = fst sf in
880
  let bs1 = bsetAddTBox sort bs in
881
  let deferrals = bsetMakeRealEmpty() in
882
  let markDeferral f =
883
    if (Hashtbl.hash "ε") != (lfGetDeferral sort f) then (
884
      bsetAdd deferrals f;)
885
  in
886
  bsetIter markDeferral bs;
887
  graphInit ();
888
  queueInit ();
889
  let root = insertCore sort bs1 deferrals in
890
  graphAddRoot root
891

    
892
let isRootSat () =
893
  match coreGetStatus (graphGetRoot ()) with
894
  | Expandable -> None
895
  | Unsat -> Some false
896
  | Sat
897
  | Open -> if (queueIsEmpty()) then Some true else None
898

    
899
let reasonerFinished () =
900
  match coreGetStatus (graphGetRoot ()) with
901
  | Expandable -> false
902
  | Unsat
903
  | Sat  -> true
904
  | Open -> queueIsEmpty ()
905

    
906

    
907
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
908
    @param verbose An optional switch which determines
909
    whether the procedure shall print some information on the standard output.
910
    The default is false.
911
    @param sorts An array mapping each sort (represented as an integer)
912
    to a functor and a list of sorts which are the arguments of the functor.
913
    @param nomTable A partial function mapping nominals (represented as strings)
914
    to their sorts.
915
    @param tbox A list of sorted formulae.
916
    @param sf A sorted formula.
917
    @return True if sf is satisfiable wrt tbox, false otherwise.
918
 *)
919

    
920
let isSat ?(verbose = false) sorts nomTable tbox sf =
921
  let start = if verbose then Unix.gettimeofday () else 0. in
922
  initReasoner sorts nomTable tbox sf;
923
  let sat =
924
    try
925
      buildGraphLoop ();
926
      (* get whether the root is satisfiable *)
927
      (* we know that the reasoner finished, so the value is there, *)
928
      (* i.e. isRootSat() will give a "Some x" and not "None" *)
929
      CU.fromSome (isRootSat())
930
    with CoAlg_finished res -> res
931
  in
932
  (* print some statistics *)
933
  if verbose then
934
    let stop = Unix.gettimeofday () in
935
    let addup lst = List.fold_left (fun acc sf -> acc + (CoAlgFormula.sizeSortedFormula sf)) 0 lst in
936
    print_newline ();
937
    print_endline ("Query: " ^ (CoAlgFormula.exportQuery tbox sf));
938
    let size = (CoAlgFormula.sizeSortedFormula sf) + (addup tbox) in
939
    print_endline ("Added Size: " ^ (string_of_int size));
940
    (*
941
    print_endline ("Negation Normal Form: " ^ (CoAlgFormula.exportQuery tbox1 sf1));
942
    let nsize = (CoAlgFormula.sizeSortedFormula sf1) + (addup tbox1) in
943
    print_endline ("Added Size: " ^ (string_of_int nsize));
944
    *)
945
    print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable.");
946
    print_endline ("Time: " ^ (string_of_float (stop -. start)));
947
    print_endline ("Generated states: " ^ (string_of_int (graphSizeState ())));
948
    print_endline ("Generated cores: " ^ (string_of_int (graphSizeCore ())));
949
    print_endline ("Generated constraints: " ^ (string_of_int (graphSizeCnstr ())));
950
    print_newline ()
951
  else ();
952
  sat