Project

General

Profile

Statistics
| Branch: | Revision:

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

History | View | Annotate | Download (40 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
  let openstates = ref 0 in
123

    
124
  (* Collect two sets of nodes. All nodes that may be satisfiable
125
   * after this iteration are collected into setStates/setCores.
126
   *
127
   * As every cycle containing a node with empty focus or an
128
   * satisfiable node should be considered satisfiable, collect these
129
   * decisive nodes into setFinishingStates/setFinishingCores
130
   *
131
   * This also marks in trivial cases nodes as satisfiable.
132
   *)
133
  let stateCollector state =
134
    match stateGetStatus state with
135
    | Unsat -> ()
136
    | Sat ->
137
       setAddState setStates state;
138
       setAddState setFinishingStates state
139
    | Expandable -> ()
140
    | Open ->
141
       openstates := !openstates + 1;
142
       if List.length (stateGetRules state) == 0 || (* States with no rules are satisfiable *)
143
         bsetCompare (bsetMake ()) (stateGetBs state) == 0 (* KD generates nodes with just True as formula *)
144
       then begin
145
         setAddState setFinishingStates state;
146
         stateSetStatus state Sat
147
       end else begin
148
         setAddState setStates state;
149
         if bsetCompare (stateGetDeferral state) emptySet == 0
150
         then begin
151
           setAddState setFinishingStates state
152
         end
153
         else ()
154
       end
155

    
156
  (* As it is enough for a core to have one successfull child, we can
157
   * also handle (some) expandable cores.
158
   *)
159
  and coreCollector core =
160
    match coreGetStatus core with
161
    | Unsat -> ()
162
    | Sat ->
163
       setAddCore setCores core;
164
       setAddCore setFinishingCores core
165
    | Expandable
166
    | Open ->
167
       setAddCore setCores core;
168
       if bsetCompare (coreGetDeferral core) emptySet == 0
169
       then begin
170
         setAddCore setFinishingCores core
171
       end
172
       else ()
173
  in
174
  graphIterStates stateCollector;
175
  graphIterCores coreCollector;
176

    
177
  setPropagationCounter !openstates;
178

    
179
  (* In a fixpoint the set called setStates / setCores is narrowed
180
   * down.
181
   *
182
   * In each step only those states and cores are retained in setStates
183
   * / setCores which reach one of setFinishing{States,Cores} in
184
   * finitely many steps. This new set of States / Cores is collected
185
   * as allowed{States,Cores} during each fixpoint iteration.
186
   *
187
   * Only those finishing nodes are retained that have allowed or
188
   * Successfull Children.
189
   *)
190
  let rec fixpointstep setStates setCores =
191
    let allowedStates = setEmptyState () in
192
    let allowedCores = setEmptyCore () in
193

    
194
    let rec visitParentStates (core : core) : unit =
195
      if not (setMemCore allowedCores core)
196
      then begin
197
        setAddCore allowedCores core;
198
        let verifyParent (state,_) =
199
          let rules = stateGetRules state in
200
          let ruleiter (dependencies, corelist) =
201
            List.exists (fun (core : core) -> setMemCore allowedCores core ||
202
                                                coreGetStatus core == Sat)
203
              corelist
204
          in
205
          if List.for_all ruleiter rules
206
          then visitParentCores state
207
        in
208
        List.iter verifyParent (coreGetParents core)
209
      end
210

    
211
    and visitParentCores (state : state) : unit =
212
      if not (setMemState allowedStates state)
213
      then begin
214
        setAddState allowedStates state;
215
        let verifyParent core =
216
          let acceptable =
217
            List.exists (fun (state : state) -> setMemState allowedStates state ||
218
                                                  stateGetStatus state == Sat)
219
              (coreGetChildren core)
220
          in
221
          if acceptable
222
          then visitParentStates core
223
        in
224
        List.iter verifyParent (stateGetParents state)
225
      end
226
    in
227

    
228
    (* All rule applications need to still be potentially Sat for a
229
     * finishing State to be a valid startingpoint for this fixpoint.
230
     *)
231
    let checkFinishingState (state : state) =
232
      let ruleiter (dependencies, corelist) : bool =
233
        List.for_all (fun (core : core) -> coreGetStatus core == Unsat ||
234
                                             coreGetStatus core == Expandable ||
235
                                               not (setMemCore setCores core)) corelist
236
      in
237
      if not (List.exists ruleiter (stateGetRules state)) then begin
238
        visitParentCores state
239
      end
240

    
241
    (* There needs to be a State still potentially Sat for this core
242
     * to be considered for the fixpoint
243
     *)
244
    and checkFinishingCore (core : core) =
245
      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat ||
246
                                                     stateGetStatus state == Expandable ||
247
                                                       not (setMemState setStates state))
248
                           (coreGetChildren core))
249
      then begin
250
        visitParentStates core
251
      end
252
    in
253
    setIterState checkFinishingState setFinishingStates;
254
    setIterCore checkFinishingCore setFinishingCores;
255

    
256

    
257
    if (setLengthState setStates) = (setLengthState allowedStates) &&
258
         (setLengthCore setCores) = (setLengthCore allowedCores)
259
    then begin
260
        setIterState (fun state -> stateSetStatus state Sat) setStates;
261
        setIterCore (fun core -> coreSetStatus core Sat; if core == graphGetRoot ()
262
                                                         then raise (CoAlg_finished true)
263
                                                         else ()) setCores;
264
      end else
265
      fixpointstep allowedStates allowedCores
266
  in
267
  fixpointstep setStates setCores
268

    
269

    
270
(*****************************************************************************)
271
(*                     Propagation of Unsatisfiability                       *)
272
(*****************************************************************************)
273

    
274
let isConstraintUnsat cset =
275
  match graphFindCnstr cset with
276
  | None -> assert false
277
  | Some UnsatC -> true
278
  | _ -> false
279

    
280
let fhtMustFind fht f =
281
  match fhtFind fht f with
282
  | Some l -> l
283
  | None -> assert false
284

    
285
let lhtMustFind lht l =
286
  match lhtFind lht l with
287
  | Some f -> f
288
  | None -> assert false
289

    
290

    
291
(* Gets a list of Things we know are unsatisfiable and propagates this
292
   information backwards *)
293
let rec propagateUnsat = function
294
  | [] -> ()
295
  | propElem::tl ->
296
      let tl1 =
297
        match propElem with
298
        | UState (state, idxopt) -> begin
299
            match stateGetStatus state with
300
            | Unsat -> tl
301
            | Sat -> raise (ReasonerError ("Propagation tells state "
302
                                           ^(string_of_int (stateGetIdx state))
303
                                           ^" would be unsat, but it is already sat"))
304
            | Open
305
            | Expandable ->
306
                let mbs =
307
                  match idxopt with
308
                  | None -> stateGetBs state
309
                  | Some idx ->
310
                      let (dep, children) = stateGetRule state idx in
311
                      let getBs core =
312
                        assert (coreGetStatus core = Unsat);
313
                        coreGetBs core
314
                      in
315
                      dep (List.map getBs children)
316
                in
317
                stateSetBs state mbs;
318
                stateSetStatus state Unsat;
319
                let prop acc core =
320
                  let turnsUnsat =
321
                    match coreGetStatus core with
322
                    | Open -> List.for_all (fun s -> stateGetStatus s = Unsat)
323
                                           (coreGetChildren core)
324
                    | Expandable
325
                    | Unsat
326
                    | Sat -> false
327
                  in
328
                  if turnsUnsat then (UCore (core, false))::acc else acc
329
                in
330
                List.fold_left prop tl (stateGetParents state)
331
          end
332
        | UCore (core, comesFromCnstr) -> begin
333
            match coreGetStatus core with
334
            | Unsat -> tl
335
            | Sat -> raise (ReasonerError ("Propagation tells core "
336
                                           ^(string_of_int (coreGetIdx core))
337
                                           ^" would be unsat, but it is already sat"))
338
            | Open
339
            | Expandable ->
340
                let mbs =
341
                  if comesFromCnstr then coreGetBs core
342
                  else
343
                    let bs = coreGetBs core in
344
                    let solver = coreGetSolver core in
345
                    let fht = coreGetFht core in
346
                    let lht = lhtInit () in
347
                    let addLits f acc =
348
                      let lit = fhtMustFind fht f in
349
                      lhtAdd lht lit f;
350
                      lit::acc
351
                    in
352
                    let litset = bsetFold addLits bs [] in
353
                    let addClauses state =
354
                      let cbs = stateGetBs state in
355
                      let clause = bsetFold (fun f acc -> (M.neg_lit (fhtMustFind fht f))::acc) cbs [] in
356
                      let okay = M.add_clause solver clause in
357
                      assert okay
358
                    in
359
                    List.iter addClauses (coreGetChildren core);
360
                    let isSat = M.invoke_solver solver litset in
361
                    assert (not isSat);
362
                    let res = bsetMake () in
363
                    let confls = M.get_conflict solver in
364
                    List.iter (fun l -> bsetAdd res (lhtMustFind lht l)) confls;
365
                    res
366
                in
367
                coreSetBs core mbs;
368
                coreSetStatus core Unsat;
369
                coreDeallocateSolver core;
370
                if core == graphGetRoot () then raise (CoAlg_finished false) else ();
371
                let prop acc (state, idx) =
372
                  let turnsUnsat =
373
                    match stateGetStatus state with
374
                    | Open
375
                    | Expandable ->
376
                        List.for_all (fun c -> coreGetStatus c = Unsat) (snd (stateGetRule state idx))
377
                    | Unsat
378
                    | Sat -> false
379
                  in
380
                  if turnsUnsat then (UState (state, Some idx))::acc else acc
381
                in
382
                let tl2 = List.fold_left prop tl (coreGetParents core) in
383
                List.fold_left (fun acc cset -> (UCnstr cset)::acc) tl2 (coreGetConstraintParents core)
384
          end
385
        | UCnstr cset ->
386
            match graphFindCnstr cset with
387
            | None
388
            | Some SatC -> assert false
389
            | Some UnsatC -> tl
390
            | Some (UnexpandedC nodes)
391
            | Some (OpenC nodes) ->
392
                graphReplaceCnstr cset UnsatC;
393
                let prop acc node =
394
                  match node with
395
                  | State state ->
396
                      let turnsUnsat =
397
                        match stateGetStatus state with
398
                        | Expandable
399
                        | Open -> cssForall isConstraintUnsat (stateGetConstraints state)
400
                        | Unsat
401
                        | Sat -> false
402
                      in
403
                      if turnsUnsat then (UState (state, None))::acc else acc
404
                  | Core core ->
405
                      let turnsUnsat =
406
                        match coreGetStatus core with
407
                        | Expandable
408
                        | Open -> cssForall isConstraintUnsat (coreGetConstraints core)
409
                        | Unsat
410
                        | Sat -> false
411
                      in
412
                      if turnsUnsat then (UCore (core, true))::acc else acc
413
                in
414
                List.fold_left prop tl nodes
415
      in
416
      propagateUnsat tl1
417

    
418
let propagateUnsatMu () =
419
  let setFinishingStates = setEmptyState () in
420
  let setFinishingCores = setEmptyCore () in
421
  let setStates = setEmptyState () in
422
  let setCores = setEmptyCore () in
423
  let emptySet = bsetMakeRealEmpty () in
424

    
425
  (* Collect two sets of nodes. All nodes that may be unsatisfiable
426
   * after this iteration are collected into setStates/setCores.
427
   *
428
   * Nodes reaching Points with empty focus as well as Expandable nodes
429
   * (if not Unsat) can not be declared Unsat so we collect these into
430
   * setFinishingStates/setFinishingCores.
431
   *)
432
  let stateCollector state =
433
    match stateGetStatus state with
434
    | Unsat -> ()
435
    | Sat
436
    | Expandable ->
437
       setAddState setStates state;
438
      setAddState setFinishingStates state
439
    | Open ->
440
       setAddState setStates state;
441
      if [] = (stateGetRules state)
442
      then begin
443
        stateSetStatus state Sat;
444
        setAddState setFinishingStates state
445
      end
446
      else ();
447
      if bsetCompare (stateGetDeferral state) emptySet == 0
448
      then begin
449
        setAddState setFinishingStates state
450
      end
451
      else ()
452

    
453
  and coreCollector core =
454
    match coreGetStatus core with
455
    | Unsat -> ()
456
    | Expandable
457
    | Sat ->
458
       setAddCore setCores core;
459
      setAddCore setFinishingCores core
460
    | Open ->
461
       setAddCore setCores core;
462
      if bsetCompare (coreGetDeferral core) emptySet == 0
463
      then begin
464
        setAddCore setFinishingCores core
465
      end
466
      else ()
467
  in
468
  graphIterStates stateCollector;
469
  graphIterCores coreCollector;
470

    
471
  (* In a fixpoint the set called setFinishingStates/setFinishingCores
472
   * is narrowed down
473
   *
474
   * In each iteration we start with all Nodes and remove all that can
475
   * reach a finishing Node. We then remove all finishing Nodes from the
476
   * respective set which are becoming Unsat and start with the next
477
   * iteration until the fixpoint is reached
478
   *
479
   *
480
   *)
481
  let rec fixpointstep setPrevUnsatStates setPrevUnsatCores =
482
    let setUnsatStates = setCopyState setStates in
483
    let setUnsatCores = setCopyCore setCores in
484

    
485
    let rec visitParentStates (core : core) : unit =
486
      if setMemCore setUnsatCores core
487
      then begin
488
        setRemoveCore setUnsatCores core;
489
        let verifyParent (state,_) =
490
          let rules = stateGetRules state in
491
          let ruleiter (dependencies, corelist) =
492
            List.exists (fun (core : core) -> not (setMemCore setUnsatCores core) ||
493
                                                coreGetStatus core == Sat)
494
              corelist
495
          in
496
          if List.for_all ruleiter rules
497
          then visitParentCores state
498
        in
499
        List.iter verifyParent (coreGetParents core)
500
      end
501

    
502
    and visitParentCores (state : state) : unit =
503
      if setMemState setUnsatStates state
504
      then begin
505
        setRemoveState setUnsatStates state;
506
        let verifyParent core =
507
          let acceptable =
508
            List.exists (fun (state : state) -> not (setMemState setUnsatStates state) ||
509
                                                  stateGetStatus state == Sat)
510
              (coreGetChildren core)
511
          in
512
          if acceptable
513
          then visitParentStates core
514
        in
515
        List.iter verifyParent (stateGetParents state)
516
      end
517
    in
518

    
519
    (* All rule applications need to still be potentially Sat for a
520
     * finishing State to be a valid startingpoint for this fixpoint.
521
     *)
522
    let checkFinishingState (state : state) =
523
      let ruleiter (dependencies, corelist) : bool =
524
        List.for_all (fun (core : core) -> coreGetStatus core == Unsat ||
525
                                             setMemCore setPrevUnsatCores core) corelist
526
      in
527
      if not (List.exists ruleiter (stateGetRules state)) ||
528
           stateGetStatus state == Expandable then begin
529
        visitParentCores state
530
      end
531

    
532
    (* There needs to be a State still potentially Sat for this core
533
     * to be considered for the fixpoint
534
     *)
535
    and checkFinishingCore (core : core) =
536
      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat ||
537
                                                     setMemState setPrevUnsatStates state)
538
                (coreGetChildren core)) ||
539
        coreGetStatus core == Expandable
540
      then begin
541
        visitParentStates core
542
      end
543
    in
544
    setIterState checkFinishingState setFinishingStates;
545
    setIterCore checkFinishingCore setFinishingCores;
546

    
547
    if (setLengthState setPrevUnsatStates) = (setLengthState setUnsatStates) &&
548
      (setLengthCore setPrevUnsatCores) = (setLengthCore setUnsatCores)
549
    then begin
550
        setIterState (fun state -> stateSetStatus state Unsat) setUnsatStates;
551
        setIterCore (fun core -> propagateUnsat [UCore (core, false)]) setUnsatCores;
552
      end else
553
      fixpointstep setUnsatStates setUnsatCores
554
  in
555
  fixpointstep (setEmptyState ()) (setEmptyCore ())
556

    
557

    
558
(*****************************************************************************)
559
(*                   Propagation of Nominal Constraints                      *)
560
(*****************************************************************************)
561

    
562
let extractAts sort bs =
563
  let ats = csetMake () in
564
  let procNom nom f =
565
    match lfGetType sort f with
566
    | AndF
567
    | OrF -> ()
568
    | TrueFalseF
569
    | AtF -> ()
570
    | _ -> csetAdd ats (lfGetAt (sort, nom) f)
571
  in
572
  let getAts f =
573
    match lfGetType sort f with
574
    | AtF -> csetAdd ats (lfToAt sort f)
575
    | NomF -> bsetIter (fun f1 -> procNom f f1) bs
576
    | _ -> ()
577
  in
578
  bsetIter getAts bs;
579
  ats
580

    
581
let detConstraintsState state =
582
  let procRule accR (_, chldrn) =
583
    let procChldrn accC core =
584
      if coreGetStatus core = Unsat then accC
585
      else cssUnion accC (coreGetConstraints core)
586
    in
587
    let orset = List.fold_left procChldrn cssEmpty chldrn in
588
    let procOrset csetO accO =
589
      let mkUnion csetU accU =
590
        let cset = csetUnion csetO csetU in
591
        cssAdd cset accU
592
      in
593
      cssFold mkUnion accR accO
594
    in
595
    cssFold procOrset orset cssEmpty
596
  in
597
  let sort = stateGetSort state in
598
  let bs = stateGetBs state in
599
  let ats = extractAts sort bs in
600
  if stateGetStatus state = Expandable then csetAddDot ats else ();
601
  List.fold_left procRule (cssSingleton ats) (stateGetRules state)
602

    
603
let detConstraintsCore core =
604
  let sort = coreGetSort core in
605
  let bs = coreGetBs core in
606
  let ats = extractAts sort bs in
607
  let addCnstr acc state =
608
    if stateGetStatus state = Unsat then acc
609
    else
610
      let csets = stateGetConstraints state in
611
      (* cssFold (fun c a -> cssAdd (csetUnion c ats) a) csets acc *)
612
      cssUnion csets acc
613
  in
614
  let initInner =
615
    if coreGetStatus core = Expandable then
616
      (* let cset = csetCopy ats in *)
617
      let cset = ats in
618
      csetAddDot cset;
619
      cssSingleton cset
620
    else cssEmpty
621
  in
622
  List.fold_left addCnstr initInner (coreGetChildren core)
623

    
624
let rec propNom = function
625
  | [] -> ()
626
  | node::tl ->
627
      let tl1 =
628
        match node with
629
        | State state ->
630
            if stateGetStatus state = Unsat then tl
631
            else
632
              let csets = detConstraintsState state in
633
              let oldcsets = stateGetConstraints state in
634
              if cssEqual csets oldcsets then tl
635
              else begin
636
                stateSetConstraints state csets;
637
                List.fold_left (fun acc c -> (Core c)::acc) tl (stateGetParents state)
638
              end
639
        | Core core ->
640
            if coreGetStatus core = Unsat then tl
641
            else
642
              let csets = detConstraintsCore core in
643
              let oldcsets = coreGetConstraints core in
644
              if cssEqual csets oldcsets then tl
645
              else begin
646
                coreSetConstraints core csets;
647
                List.fold_left (fun acc (s, _) -> (State s)::acc) tl (coreGetParents core)
648
              end
649
      in
650
      propNom tl1
651

    
652
let updateConstraints node elemU csets =
653
  let update cset acc =
654
    let cnstr =
655
      match graphFindCnstr cset with
656
      | Some cn -> cn
657
      | None ->
658
          let cn = UnexpandedC [] in
659
          graphInsertCnstr cset cn;
660
          queueInsertCnstr cset;
661
          cn
662
    in
663
    match cnstr with
664
    | UnsatC -> acc
665
    | UnexpandedC parents ->
666
        graphReplaceCnstr cset (UnexpandedC (node::parents));
667
        false
668
    | OpenC parents ->
669
        graphReplaceCnstr cset (OpenC (node::parents));
670
        false
671
    | SatC -> false
672
  in
673
  let isUnsat = cssFold update csets true in
674
  if isUnsat then propagateUnsat [elemU] else ()
675

    
676
let propagateNominals () =
677
  let init = cssSingleton (csetMake ()) in
678
  graphIterStates (fun s -> if stateGetStatus s = Unsat then () else stateSetConstraints s init);
679
  graphIterCores (fun c -> if coreGetStatus c = Unsat then () else coreSetConstraints c init);
680
  graphIterStates (fun s -> propNom [State s]);
681
  graphIterCores (fun c -> propNom [Core c]);
682
  graphClearCnstr ();
683
  let fktS state =
684
    if stateGetStatus state = Unsat then ()
685
    else updateConstraints (State state) (UState (state, None)) (stateGetConstraints state)
686
  in
687
  graphIterStates fktS;
688
  let fktC core =
689
    if coreGetStatus core = Unsat then ()
690
    else updateConstraints (Core core) (UCore (core, true)) (coreGetConstraints core)
691
  in
692
  graphIterCores fktC
693

    
694

    
695
(*****************************************************************************)
696
(*                           Node Expansions                                 *)
697
(*****************************************************************************)
698

    
699
let getLit sort fht solver f =
700
  match fhtFind fht f with
701
  | Some lit -> lit
702
  | None ->
703
      let var = M.new_variable solver in
704
      let lit = M.var_to_lit var true in
705
      fhtAdd fht f lit;
706
      let () =
707
        match lfGetNeg sort f with
708
        | None -> ()
709
        | Some nf ->
710
            let nlit = M.neg_lit lit in
711
            fhtAdd fht nf nlit;
712
      in
713
      lit
714

    
715
let newCore sort bs defer =
716
  (* when creating a now core from a set of formulas bs
717
        bs = { x_1, ...., x_n }
718
           = "x_1 /\ .... /\ x_n"
719
     Then we do this by:
720

    
721
        1. creating a new literal in the sat solver for each
722
           "boolean subformula" from the x_i. "boolean subformula" means that
723
           this subformula is not hidden under modalities but only under
724
           boolean connectives (/\, \/).
725
        2. encoding the relation between a formula and its intermediate boolean
726
           subformulas by a clause:
727
  *)
728
  let fht = fhtInit () in
729
  let solver = M.new_solver () in
730
  let rec addClauses f =
731
    (* step 1: create a literal in the satsolver representing the formula f *)
732
    let lf = getLit sort fht solver f in
733
    (* step 2: encode relation to possible subformulas *)
734
    match lfGetType sort f with
735
    | OrF ->
736
        (*
737
           case 2.(a)   f =  f1 \/ f2
738
                   fill fht such that it says:
739

    
740
                        f  |---> lf
741
                        f1 |---> lf1
742
                        f2 |---> lf2
743
        *)
744
        let f1 = lfGetDest1 sort f in
745
        let f2 = lfGetDest2 sort f in
746
        addClauses f1;
747
        addClauses f2;
748
        let lf1 = fhtMustFind fht f1 in
749
        let lf2 = fhtMustFind fht f2 in
750
        (*
751
            encode the structure of f by adding the clause (lf -> lf1 \/ lf2)
752
        *)
753
        let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in
754
        assert (okay)
755
    | AndF ->
756
        (*
757
           case 2.(b)   f =  f1 /\ f2
758
                   fill fht such that it says:
759

    
760
                        f  |---> lf
761
                        f1 |---> lf1
762
                        f2 |---> lf2
763
        *)
764
        let f1 = lfGetDest1 sort f in
765
        let f2 = lfGetDest2 sort f in
766
        addClauses f1;
767
        addClauses f2;
768
        let lf1 = fhtMustFind fht f1 in
769
        let lf2 = fhtMustFind fht f2 in
770
        (*
771
            encode the structure of f by adding the clauses
772
                    (lf -> lf1) /\ (lf -> lf2)
773
        *)
774
        let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
775
        assert (okay1);
776
        let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in
777
        assert (okay2)
778
    | MuF
779
    | NuF ->
780
       (*
781
          Dest of a fixpoint is it's unfolded version. This adds just
782
          an simple forward implication that could be optimised out
783
          though not without nontrivial transformation of code
784

    
785
            f = μ X . φ   |---> lf
786
            φ[X |-> f]    |---> lf1
787

    
788
          Then adding lf -> lf1 to minisat
789
        *)
790
       let f1 = lfGetDest1 sort f in
791
       addClauses f1;
792
       let lf1 = fhtMustFind fht f1 in
793
       let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
794
       assert (okay1);
795
    | _ -> ()
796
        (* case 2.(c)
797
            We don't need to do anything except adding f to the fht
798
        *)
799
  in
800
  bsetIter addClauses bs;
801
  coreMake sort bs defer (Some solver) fht
802

    
803
let getNextState core =
804
  (* Create a new state, which is obtained by a satisfying assignment of the
805
     literals of the minisat solver.
806
     In addition to that, feed the negation of the satisfying assignment back
807
     to the minisat solver in order to obtain different solutions on successive
808
     minisat calls.
809
  *)
810
  let bs = coreGetBs core in
811
  let refocusing = bsetCompare (bsetMakeRealEmpty ()) (coreGetDeferral core) = 0 in
812
  let deferralS =
813
    if refocusing then
814
      bsetCopy bs
815
    else
816
      coreGetDeferral core
817
  in
818
  let fht = coreGetFht core in
819
  let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
820
  let solver = coreGetSolver core in
821
  let isSat = M.invoke_solver solver litset in
822
  (* Clearly, if the current core is unsatisfiable, no further child state can
823
     be created *)
824
  if not isSat then None
825
  else
826
    let sort = coreGetSort core in
827
    (* create a new set of formulas newbs with the property:
828
       if the conjunction of newbs is satisfiable, then the present core is
829
       satisfiable.
830
    *)
831
    let newbs = bsetMake () in
832
    let newdefer = bsetMakeRealEmpty () in
833
    (* if newbs = { l_1, .... l_n }, i.e.
834

    
835
            newbs = l_1 /\ ... /\ l_n
836

    
837
       then we can get essentially different satisfying assignments of bs by
838
       adding another clause
839

    
840
            clause = ¬ newbs = ¬l_1 \/ ... \/ ¬l_n
841

    
842
       By mkExclClause, newbs is filled, and clause is built in the accumulator acc.
843
    *)
844
    let rec mkExclClause deferral f acc =
845
      (* f is a formula that is true in the current satisfying assignment *)
846
      match lfGetType sort f with
847
      | OrF ->
848
          (* if f is true and a disjunction, then one of its disjuncts is true *)
849
          let f1 = lfGetDest1 sort f in
850
          let lf1 = fhtMustFind fht f1 in
851
          (* if the first disjunct f1 is true, then we need to add subformulas
852
             of f1 to newbs&clause *)
853
          if M.literal_status solver lf1 = M.LTRUE then mkExclClause deferral f1 acc
854
          else
855
            (* otherwise f2 must be true *)
856
            let f2 = lfGetDest2 sort f in
857
            let lf2 = fhtMustFind fht f2 in
858
            assert (M.literal_status solver lf2 = M.LTRUE);
859
            mkExclClause deferral f2 acc
860
      | AndF ->
861
          (* if the true f is a conjuction, then both conjunctions must be true *)
862
          let f1 = lfGetDest1 sort f in
863
          let lf1 = fhtMustFind fht f1 in
864
          assert (M.literal_status solver lf1 = M.LTRUE);
865
          let acc1 = mkExclClause deferral f1 acc in
866
          let f2 = lfGetDest2 sort f in
867
          let lf2 = fhtMustFind fht f2 in
868
          assert (M.literal_status solver lf2 = M.LTRUE);
869
          mkExclClause deferral f2 acc1
870
      | MuF
871
      | NuF ->
872
         let f1 = lfGetDest1 sort f in
873
         mkExclClause deferral f1 acc
874
      | _ ->
875
         (* if f is a trivial formula or modality, then add it ... *)
876
         (* ... to newbs *)
877
         bsetAdd newbs f;
878
         let defercandidate = lfGetDeferral sort f in
879
         (if (defercandidate != (Hashtbl.hash "ε") &&
880
                (refocusing || deferral = defercandidate)) then
881
            bsetAdd newdefer f);
882
         (* ... and to the new clause *)
883
         (M.neg_lit (fhtMustFind fht f))::acc
884
    in
885
    let init_clause f acc =
886
      let deferral =
887
        (* for each deferral determine which variable it belongs to *)
888
        if bsetMem deferralS f then (
889
          lfGetDeferral sort f)
890
        else
891
          (Hashtbl.hash "ε")
892
      in
893
      mkExclClause deferral f acc
894
    in
895
    let clause = bsetFold init_clause bs [] in
896
    let okay = M.add_clause solver clause in
897
    assert (okay);
898
    Some (sort, newbs, newdefer)
899

    
900
let newState sort bs defer =
901
  let (func, sl) = !sortTable.(sort) in
902
  let producer = CoAlgLogics.getExpandingFunctionProducer func in
903
  let exp = producer sort bs defer sl in
904
  stateMake sort bs defer exp
905

    
906
let insertState parent sort bs defer =
907
  let child =
908
    match graphFindState sort (bs, defer) with
909
    | None ->
910
        let s = newState sort bs defer in
911
        graphInsertState sort (bs, defer) s;
912
        queueInsertState s;
913
        s
914
    | Some s -> s
915
  in
916
  coreAddChild parent child;
917
  stateAddParent child parent
918

    
919
let expandCore core =
920
  match getNextState core with
921
  | Some (sort, bs, defer) ->
922
      insertState core sort bs defer;
923
      queueInsertCore core
924
  | None ->
925
      let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in
926
      if isUnsat
927
      then
928
          propagateUnsat [UCore (core, false)]
929
      else
930
          coreSetStatus core Open
931

    
932

    
933
let insertCore sort bs defer =
934
  match graphFindCore sort (bs, defer) with
935
  | None ->
936
     let c = newCore sort bs defer in
937
     graphInsertCore sort (bs, defer) c;
938
     queueInsertCore c;
939
     c
940
  | Some c -> c
941

    
942
(** Insert cores for the children generated by a modal rule application.
943
  *
944
  * @return true if all new cores are already unsatisfiable, false otherwise
945
  *)
946
let insertRule state dep chldrn =
947
  let chldrn = listFromLazylist chldrn in
948
  let mkCores (sort, bs, defer) =
949
    let bs1 = bsetAddTBox sort bs in
950
    (* For the aconjunctive fragment, instead of adding a core annotated with
951
     * all deferrals, we add a core for each formula in the deferral set. *)
952
    let deferSingletons =
953
      if getFragment () = AconjunctiveAltFree
954
         && bsetCompare defer (bsetMakeRealEmpty ()) <> 0 then
955
        bsetFold (fun f list -> bsetSingleton f::list) defer []
956
      else
957
        [defer] in
958
    List.map (insertCore sort (bsetCopy bs1)) deferSingletons
959
  in
960
  (* A list of cores for each child: [[child1a;child1b]; [child2a;child2b]] *)
961
  let coresPerChild = List.map mkCores chldrn in
962
  (* All combinations that take a core from each child:
963
   * [[ch1a;ch2a]; [ch1a;ch2b]; [ch1b;ch2a]; [ch1b;ch2b]]
964
   * Neccesary because stateAddRule expects each child to have only one core. *)
965
  let coresPerRule = CU.TList.combinations coresPerChild in
966
  let addRule cores =
967
    let idx = stateAddRule state dep cores in
968
    List.iter (fun c -> coreAddParent c state idx) cores;
969
    if List.for_all (fun core -> coreGetStatus core = Unsat) cores then begin
970
      propagateUnsat [UState (state, Some idx)];
971
      true
972
    end else 
973
      false
974
  in
975
  List.mem true (List.map (fun r -> addRule r) coresPerRule)
976
  
977

    
978
(** Call insertRule on all rules
979
  * @return true if any rule application generated only unsat cores
980
  *)
981
let rec insertAllRules state rules =
982
  List.mem true (List.map (fun (dep, children) -> insertRule state dep children) rules)
983

    
984
let expandState state =
985
  match stateNextRule state with
986
  | MultipleElements rules ->
987
      let unsat = insertAllRules state rules in
988
      if not unsat then stateSetStatus state Open
989
  | SingleElement (dep, chldrn) ->
990
      let unsat = insertRule state dep chldrn in
991
      if not unsat then queueInsertState state else ()
992
  | NoMoreElements -> stateSetStatus state Open
993

    
994

    
995
let expandCnstr cset =
996
  let nht = nhtInit () in
997
  let mkCores f =
998
    let (sort, lf) as nom = atFormulaGetNominal f in
999
    let nomset =
1000
      match nhtFind nht nom with
1001
      | Some ns -> ns
1002
      | None ->
1003
          let cset1 = csetCopy cset in
1004
          csetRemDot cset1;
1005
          let bs = csetAddTBox sort cset1 in
1006
          bsetAdd bs lf;
1007
          nhtAdd nht nom bs;
1008
          bs
1009
    in
1010
    bsetAdd nomset (atFormulaGetSubformula f)
1011
  in
1012
  csetIter cset mkCores;
1013
  let inCores (sort, _) bs (isUns, acc) =
1014
    let core = insertCore sort bs bs in (* TODO: think of deferral / μ stuff here *)
1015
    coreAddConstraintParent core cset;
1016
    (coreGetStatus core = Unsat || isUns, core::acc)
1017
  in
1018
  let (isUnsat, children) = nhtFold inCores nht (false, []) in
1019
  if isUnsat then propagateUnsat [UCnstr cset]
1020
  else
1021
    match graphFindCnstr cset with
1022
    | Some (UnexpandedC parents) -> graphReplaceCnstr cset (OpenC parents)
1023
    | _ -> assert false
1024

    
1025

    
1026
(*****************************************************************************)
1027
(*                           The Main Loop                                   *)
1028
(*****************************************************************************)
1029

    
1030
let expandNodesLoop (recursiveAction: unit -> unit) =
1031
  match queueGetElement () with
1032
  | QState state ->
1033
      if stateGetStatus state = Expandable then begin
1034
        expandState state;
1035
        if doNominalPropagation () then begin
1036
          (* propagateNominals (); *)
1037
          if doSatPropagation () then (propagateUnsatMu (); propagateSatMu ())
1038
        end else ()
1039
      end else ();
1040
      recursiveAction ()
1041
  | QCore core ->
1042
      if coreGetStatus core = Expandable then begin
1043
        expandCore core;
1044
        if doNominalPropagation () then begin
1045
          (* propagateNominals (); *)
1046
          if doSatPropagation () then (propagateUnsatMu (); propagateSatMu ())
1047
        end else ()
1048
      end else ();
1049
      recursiveAction ()
1050
  | QCnstr cset ->
1051
      expandCnstr cset;
1052
      recursiveAction ()
1053
  | QEmpty -> ()
1054

    
1055
let runReasonerStep () =
1056
  let void () = () in
1057
  expandNodesLoop void; (* expand at most one node *)
1058
  propagateUnsatMu ();
1059
  (* if this emptied the queue *)
1060
  if queueIsEmpty () then begin
1061
    (* then check whether the nominals would add further queue elements *)
1062
    (* print_endline "Propagating nominals..."; *)
1063
    (* propagateNominals () *)
1064
  end else () (* else: the next step would be to expand another node *)
1065

    
1066
let rec buildGraphLoop () =
1067
  let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in
1068
  expandNodesFurther (); (* expand as many queue elements as possible *)
1069
  (* propagateNominals (); *)
1070
  (* if propagating nominals added some more queue members, do all again.. *)
1071
  if queueIsEmpty () then () else buildGraphLoop ()
1072

    
1073
let initReasoner fragSpec sorts nomTable tbox sf =
1074
  sortTable := Array.copy sorts;
1075
  let (tbox1, sf1, bs) = ppFormulae fragSpec nomTable tbox sf in
1076
  let sort = fst sf in
1077
  let bs1 = bsetAddTBox sort bs in
1078
  let deferrals = bsetMakeRealEmpty() in
1079
  let markDeferral f =
1080
    if (Hashtbl.hash "ε") != (lfGetDeferral sort f) then (
1081
      bsetAdd deferrals f;)
1082
  in
1083
  bsetIter markDeferral bs;
1084
  graphInit ();
1085
  queueInit ();
1086
  let root = insertCore sort bs1 deferrals in
1087
  graphAddRoot root
1088

    
1089
let isRootSat () =
1090
  match coreGetStatus (graphGetRoot ()) with
1091
  | Expandable -> None
1092
  | Unsat -> Some false
1093
  | Sat -> Some true
1094
  | Open -> if (queueIsEmpty()) then Some true else None
1095

    
1096
let reasonerFinished () =
1097
  match coreGetStatus (graphGetRoot ()) with
1098
  | Expandable -> false
1099
  | Unsat
1100
  | Sat  -> true
1101
  | Open -> queueIsEmpty ()
1102

    
1103

    
1104
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
1105
    @param verbose An optional switch which determines
1106
    whether the procedure shall print some information on the standard output.
1107
    The default is false.
1108
    @param sorts An array mapping each sort (represented as an integer)
1109
    to a functor and a list of sorts which are the arguments of the functor.
1110
    @param nomTable A partial function mapping nominals (represented as strings)
1111
    to their sorts.
1112
    @param tbox A list of sorted formulae.
1113
    @param sf A sorted formula.
1114
    @return True if sf is satisfiable wrt tbox, false otherwise.
1115
 *)
1116

    
1117
let isSat ?(verbose = false) fragSpec sorts nomTable tbox sf =
1118
  let start = if verbose then Unix.gettimeofday () else 0. in
1119
  initReasoner fragSpec sorts nomTable tbox sf;
1120
  let sat =
1121
    try
1122
      buildGraphLoop ();
1123
      propagateUnsatMu ();
1124
      (* get whether the root is satisfiable *)
1125
      (* we know that the reasoner finished, so the value is there, *)
1126
      (* i.e. isRootSat() will give a "Some x" and not "None" *)
1127
      CU.fromSome (isRootSat())
1128
    with CoAlg_finished res -> res
1129
  in
1130
  (* print some statistics *)
1131
  if verbose then
1132
    let stop = Unix.gettimeofday () in
1133
    let addup lst = List.fold_left (fun acc sf -> acc + (CoAlgFormula.sizeSortedFormula sf)) 0 lst in
1134
    print_newline ();
1135
    print_endline ("Query: " ^ (CoAlgFormula.exportQuery tbox sf));
1136
    let size = (CoAlgFormula.sizeSortedFormula sf) + (addup tbox) in
1137
    print_endline ("Added Size: " ^ (string_of_int size));
1138
    (*
1139
    print_endline ("Negation Normal Form: " ^ (CoAlgFormula.exportQuery tbox1 sf1));
1140
    let nsize = (CoAlgFormula.sizeSortedFormula sf1) + (addup tbox1) in
1141
    print_endline ("Added Size: " ^ (string_of_int nsize));
1142
    *)
1143
    print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable.");
1144
    print_endline ("Time: " ^ (string_of_float (stop -. start)));
1145
    print_endline ("Generated states: " ^ (string_of_int (graphSizeState ())));
1146
    print_endline ("Generated cores: " ^ (string_of_int (graphSizeCore ())));
1147
    print_endline ("Generated constraints: " ^ (string_of_int (graphSizeCnstr ())));
1148
    print_newline ()
1149
  else ();
1150
  sat
1151

    
1152
(* vim: set et sw=2 sts=2 ts=8 : *)