Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ 31229254

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

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

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

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

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

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

    
233
    (* There needs to be a State still potentially Sat for this core
234
     * to be considered for the fixpoint
235
     *)
236
    and checkFinishingCore (core : core) =
237
      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable || not (setMemState setStates state))
238
                           (coreGetChildren core))
239
      then begin
240
        visitParentStates core
241
      end
242
    in
243
    setIterState checkFinishingState setFinishingStates;
244
    setIterCore checkFinishingCore setFinishingCores;
245

    
246

    
247
    if (setLengthState setStates) = (setLengthState allowedStates) &&
248
         (setLengthCore setCores) = (setLengthCore allowedCores)
249
    then begin
250
        setIterState (fun state -> stateSetStatus state Sat) setStates;
251
        setIterCore (fun core -> coreSetStatus core Sat; if core == graphGetRoot () then raise (CoAlg_finished true) else ()) setCores;
252
      end else
253
      fixpointstep allowedStates allowedCores
254
  in
255
  fixpointstep setStates setCores
256

    
257

    
258
(*****************************************************************************)
259
(*                     Propagation of Unsatisfiability                       *)
260
(*****************************************************************************)
261

    
262
let isConstraintUnsat cset =
263
  match graphFindCnstr cset with
264
  | None -> assert false
265
  | Some UnsatC -> true
266
  | _ -> false
267

    
268
let fhtMustFind fht f =
269
  match fhtFind fht f with
270
  | Some l -> l
271
  | None -> assert false
272

    
273
let lhtMustFind lht l =
274
  match lhtFind lht l with
275
  | Some f -> f
276
  | None -> assert false
277

    
278

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

    
404
let propagateUnsatMu () =
405
  let setFinishingStates = setEmptyState () in
406
  let setFinishingCores = setEmptyCore () in
407
  let setStates = setEmptyState () in
408
  let setCores = setEmptyCore () in
409
  let emptySet = bsetMakeRealEmpty () in
410

    
411
  (* Collect two sets of nodes. All nodes that may be unsatisfiable
412
   * after this iteration are collected into setStates/setCores.
413
   *
414
   * Nodes reaching Points with empty focus as well as Expandable nodes
415
   * (if not Unsat) can not be declared Unsat so we collect these into
416
   * setFinishingStates/setFinishingCores.
417
   *)
418
  let stateCollector state =
419
    match stateGetStatus state with
420
    | Unsat -> ()
421
    | Sat
422
    | Expandable ->
423
       setAddState setStates state;
424
      setAddState setFinishingStates state
425
    | Open ->
426
       setAddState setStates state;
427
      if bsetCompare (stateGetDeferral state) emptySet == 0
428
      then begin
429
        setAddState setFinishingStates state
430
      end
431
      else ()
432

    
433
  and coreCollector core =
434
    match coreGetStatus core with
435
    | Unsat -> ()
436
    | Expandable
437
    | Sat ->
438
       setAddCore setCores core;
439
      setAddCore setFinishingCores core
440
    | Open ->
441
       setAddCore setCores core;
442
      if bsetCompare (coreGetDeferral core) emptySet == 0
443
      then begin
444
        setAddCore setFinishingCores core
445
      end
446
      else ()
447
  in
448
  graphIterStates stateCollector;
449
  graphIterCores coreCollector;
450

    
451
  (* In a fixpoint the set called setFinishingStates/setFinishingCores
452
   * is narrowed down
453
   *
454
   * In each iteration we start with all Nodes and remove all that can
455
   * reach a finishing Node. We then remove all finishing Nodes from the
456
   * respective set which are becoming Unsat and start with the next
457
   * iteration until the fixpoint is reached
458
   *
459
   *
460
   *)
461
  let rec fixpointstep setPrevUnsatStates setPrevUnsatCores =
462
    let setUnsatStates = setCopyState setStates in
463
    let setUnsatCores = setCopyCore setCores in
464

    
465
    let rec visitParentStates (core : core) : unit =
466
      if setMemCore setUnsatCores core
467
      then begin
468
        setRemoveCore setUnsatCores core;
469
        let verifyParent (state,_) =
470
          let rules = stateGetRules state in
471
          let ruleiter (dependencies, corelist) =
472
            List.exists (fun (core : core) -> not (setMemCore setUnsatCores core) || coreGetStatus core == Sat)
473
              corelist
474
          in
475
          if List.for_all ruleiter rules
476
          then visitParentCores state
477
        in
478
        List.iter verifyParent (coreGetParents core)
479
      end
480

    
481
    and visitParentCores (state : state) : unit =
482
      if setMemState setUnsatStates state
483
      then begin
484
        setRemoveState setUnsatStates state;
485
        let verifyParent core =
486
          let acceptable =
487
            List.exists (fun (state : state) -> not (setMemState setUnsatStates state) || stateGetStatus state == Sat)
488
              (coreGetChildren core)
489
          in
490
          if acceptable
491
          then visitParentStates core
492
        in
493
        List.iter verifyParent (stateGetParents state)
494
      end
495
    in
496

    
497
    (* All rule applications need to still be potentially Sat for a
498
     * finishing State to be a valid startingpoint for this fixpoint.
499
     *)
500
    let checkFinishingState (state : state) =
501
      let ruleiter (dependencies, corelist) : bool =
502
        List.for_all (fun (core : core) -> coreGetStatus core == Unsat || setMemCore setPrevUnsatCores core) corelist
503
      in
504
      if not (List.exists ruleiter (stateGetRules state)) || stateGetStatus state == Expandable then begin
505
        visitParentCores state
506
      end
507

    
508
    (* There needs to be a State still potentially Sat for this core
509
     * to be considered for the fixpoint
510
     *)
511
    and checkFinishingCore (core : core) =
512
      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || setMemState setPrevUnsatStates state)
513
                (coreGetChildren core)) ||
514
        coreGetStatus core == Expandable
515
      then begin
516
        visitParentStates core
517
      end
518
    in
519
    setIterState checkFinishingState setFinishingStates;
520
    setIterCore checkFinishingCore setFinishingCores;
521

    
522
    if (setLengthState setPrevUnsatStates) = (setLengthState setUnsatStates) &&
523
      (setLengthCore setPrevUnsatCores) = (setLengthCore setUnsatCores)
524
    then begin
525
        setIterState (fun state -> stateSetStatus state Unsat) setUnsatStates;
526
        setIterCore (fun core -> coreSetStatus core Unsat; if core == graphGetRoot () then raise (CoAlg_finished false) else ()) setUnsatCores;
527
      end else
528
      fixpointstep setUnsatStates setUnsatCores
529
  in
530
  fixpointstep (setEmptyState ()) (setEmptyCore ())
531

    
532

    
533
(*****************************************************************************)
534
(*                   Propagation of Nominal Constraints                      *)
535
(*****************************************************************************)
536

    
537
let extractAts sort bs =
538
  let ats = csetMake () in
539
  let procNom nom f =
540
    match lfGetType sort f with
541
    | AndF
542
    | OrF -> ()
543
    | TrueFalseF
544
    | AtF -> ()
545
    | _ -> csetAdd ats (lfGetAt (sort, nom) f)
546
  in
547
  let getAts f =
548
    match lfGetType sort f with
549
    | AtF -> csetAdd ats (lfToAt sort f)
550
    | NomF -> bsetIter (fun f1 -> procNom f f1) bs
551
    | _ -> ()
552
  in
553
  bsetIter getAts bs;
554
  ats
555

    
556
let detConstraintsState state =
557
  let procRule accR (_, chldrn) =
558
    let procChldrn accC core =
559
      if coreGetStatus core = Unsat then accC
560
      else cssUnion accC (coreGetConstraints core)
561
    in
562
    let orset = List.fold_left procChldrn cssEmpty chldrn in
563
    let procOrset csetO accO =
564
      let mkUnion csetU accU =
565
        let cset = csetUnion csetO csetU in
566
        cssAdd cset accU
567
      in
568
      cssFold mkUnion accR accO
569
    in
570
    cssFold procOrset orset cssEmpty
571
  in
572
  let sort = stateGetSort state in
573
  let bs = stateGetBs state in
574
  let ats = extractAts sort bs in
575
  if stateGetStatus state = Expandable then csetAddDot ats else ();
576
  List.fold_left procRule (cssSingleton ats) (stateGetRules state)
577

    
578
let detConstraintsCore core =
579
  let sort = coreGetSort core in
580
  let bs = coreGetBs core in
581
  let ats = extractAts sort bs in
582
  let addCnstr acc state =
583
    if stateGetStatus state = Unsat then acc
584
    else
585
      let csets = stateGetConstraints state in
586
      (* cssFold (fun c a -> cssAdd (csetUnion c ats) a) csets acc *)
587
      cssUnion csets acc
588
  in
589
  let initInner =
590
    if coreGetStatus core = Expandable then
591
      (* let cset = csetCopy ats in *)
592
      let cset = ats in
593
      csetAddDot cset;
594
      cssSingleton cset
595
    else cssEmpty
596
  in
597
  List.fold_left addCnstr initInner (coreGetChildren core)
598

    
599
let rec propNom = function
600
  | [] -> ()
601
  | node::tl ->
602
      let tl1 =
603
        match node with
604
        | State state ->
605
            if stateGetStatus state = Unsat then tl
606
            else
607
              let csets = detConstraintsState state in
608
              let oldcsets = stateGetConstraints state in
609
              if cssEqual csets oldcsets then tl
610
              else begin
611
                stateSetConstraints state csets;
612
                List.fold_left (fun acc c -> (Core c)::acc) tl (stateGetParents state)
613
              end
614
        | Core core ->
615
            if coreGetStatus core = Unsat then tl
616
            else
617
              let csets = detConstraintsCore core in
618
              let oldcsets = coreGetConstraints core in
619
              if cssEqual csets oldcsets then tl
620
              else begin
621
                coreSetConstraints core csets;
622
                List.fold_left (fun acc (s, _) -> (State s)::acc) tl (coreGetParents core)
623
              end
624
      in
625
      propNom tl1
626

    
627
let updateConstraints node elemU csets =
628
  let update cset acc =
629
    let cnstr =
630
      match graphFindCnstr cset with
631
      | Some cn -> cn
632
      | None ->
633
          let cn = UnexpandedC [] in
634
          graphInsertCnstr cset cn;
635
          queueInsertCnstr cset;
636
          cn
637
    in
638
    match cnstr with
639
    | UnsatC -> acc
640
    | UnexpandedC parents ->
641
        graphReplaceCnstr cset (UnexpandedC (node::parents));
642
        false
643
    | OpenC parents ->
644
        graphReplaceCnstr cset (OpenC (node::parents));
645
        false
646
    | SatC -> false
647
  in
648
  let isUnsat = cssFold update csets true in
649
  if isUnsat then propagateUnsat [elemU] else ()
650

    
651
let propagateNominals () =
652
  let init = cssSingleton (csetMake ()) in
653
  graphIterStates (fun s -> if stateGetStatus s = Unsat then () else stateSetConstraints s init);
654
  graphIterCores (fun c -> if coreGetStatus c = Unsat then () else coreSetConstraints c init);
655
  graphIterStates (fun s -> propNom [State s]);
656
  graphIterCores (fun c -> propNom [Core c]);
657
  graphClearCnstr ();
658
  let fktS state =
659
    if stateGetStatus state = Unsat then ()
660
    else updateConstraints (State state) (UState (state, None)) (stateGetConstraints state)
661
  in
662
  graphIterStates fktS;
663
  let fktC core =
664
    if coreGetStatus core = Unsat then ()
665
    else updateConstraints (Core core) (UCore (core, true)) (coreGetConstraints core)
666
  in
667
  graphIterCores fktC
668

    
669

    
670
(*****************************************************************************)
671
(*                           Node Expansions                                 *)
672
(*****************************************************************************)
673

    
674
let getLit sort fht solver f =
675
  match fhtFind fht f with
676
  | Some lit -> lit
677
  | None ->
678
      let var = M.new_variable solver in
679
      let lit = M.var_to_lit var true in
680
      fhtAdd fht f lit;
681
      let () =
682
        match lfGetNeg sort f with
683
        | None -> ()
684
        | Some nf ->
685
            let nlit = M.neg_lit lit in
686
            fhtAdd fht nf nlit;
687
      in
688
      lit
689

    
690
let newCore sort bs defer =
691
  (* when creating a now core from a set of formulas bs
692
        bs = { x_1, ...., x_n }
693
           = "x_1 /\ .... /\ x_n"
694
     Then we do this by:
695

    
696
        1. creating a new literal in the sat solver for each
697
           "boolean subformula" from the x_i. "boolean subformula" means that
698
           this subformula is not hidden under modalities but only under
699
           boolean connectives (/\, \/).
700
        2. encoding the relation between a formula and its intermediate boolean
701
           subformulas by a clause:
702
  *)
703
  let fht = fhtInit () in
704
  let solver = M.new_solver () in
705
  let rec addClauses f =
706
    (* step 1: create a literal in the satsolver representing the formula f *)
707
    let lf = getLit sort fht solver f in
708
    (* step 2: encode relation to possible subformulas *)
709
    match lfGetType sort f with
710
    | OrF ->
711
        (*
712
           case 2.(a)   f =  f1 \/ f2
713
                   fill fht such that it says:
714

    
715
                        f  |---> lf
716
                        f1 |---> lf1
717
                        f2 |---> lf2
718
        *)
719
        let f1 = lfGetDest1 sort f in
720
        let f2 = lfGetDest2 sort f in
721
        addClauses f1;
722
        addClauses f2;
723
        let lf1 = fhtMustFind fht f1 in
724
        let lf2 = fhtMustFind fht f2 in
725
        (*
726
            encode the structure of f by adding the clause (lf -> lf1 \/ lf2)
727
        *)
728
        let okay = M.add_clause solver [M.neg_lit lf; lf1; lf2] in
729
        assert (okay)
730
    | AndF ->
731
        (*
732
           case 2.(b)   f =  f1 /\ f2
733
                   fill fht such that it says:
734

    
735
                        f  |---> lf
736
                        f1 |---> lf1
737
                        f2 |---> lf2
738
        *)
739
        let f1 = lfGetDest1 sort f in
740
        let f2 = lfGetDest2 sort f in
741
        addClauses f1;
742
        addClauses f2;
743
        let lf1 = fhtMustFind fht f1 in
744
        let lf2 = fhtMustFind fht f2 in
745
        (*
746
            encode the structure of f by adding the clauses
747
                    (lf -> lf1) /\ (lf -> lf2)
748
        *)
749
        let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
750
        assert (okay1);
751
        let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in
752
        assert (okay2)
753
    | MuF
754
    | NuF ->
755
       (*
756
          Dest of a fixpoint is it's unfolded version. This adds just
757
          an simple forward implication that could be optimised out
758
          though not without nontrivial transformation of code
759

    
760
            f = μ X . φ   |---> lf
761
            φ[X |-> f]    |---> lf1
762

    
763
          Then adding lf -> lf1 to minisat
764
        *)
765
       let f1 = lfGetDest1 sort f in
766
       addClauses f1;
767
       let lf1 = fhtMustFind fht f1 in
768
       let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
769
       assert (okay1);
770
    | _ -> ()
771
        (* case 2.(c)
772
            We don't need to do anything except adding f to the fht
773
        *)
774
  in
775
  bsetIter addClauses bs;
776
  coreMake sort bs defer solver fht
777

    
778
let getNextState core =
779
  (* Create a new state, which is obtained by a satisfying assignment of the
780
     literals of the minisat solver.
781
     In addition to that, feed the negation of the satisfying assignment back
782
     to the minisat solver in order to obtain different solutions on successive
783
     minisat calls.
784
  *)
785
  let bs = coreGetBs core in
786
  let refocusing = bsetCompare (bsetMakeRealEmpty ()) (coreGetDeferral core) = 0 in
787
  let deferralS =
788
    if refocusing then
789
      bsetCopy bs
790
    else
791
      coreGetDeferral core
792
  in
793
  let fht = coreGetFht core in
794
  let litset = bsetFold (fun f acc -> (fhtMustFind fht f)::acc) bs [] in
795
  let solver = coreGetSolver core in
796
  let isSat = M.invoke_solver solver litset in
797
  (* Clearly, if the current core is unsatisfiable, no further child state can
798
     be created *)
799
  if not isSat then None
800
  else
801
    let sort = coreGetSort core in
802
    (* create a new set of formulas newbs with the property:
803
       if the conjunction of newbs is satisfiable, then the present core is
804
       satisfiable.
805
    *)
806
    let newbs = bsetMake () in
807
    let newdefer = bsetMakeRealEmpty () in
808
    (* if newbs = { l_1, .... l_n }, i.e.
809

    
810
            newbs = l_1 /\ ... /\ l_n
811

    
812
       then we can get essentially different satisfying assignments of bs by
813
       adding another clause
814

    
815
            clause = ¬ newbs = ¬l_1 \/ ... \/ ¬l_n
816

    
817
       By mkExclClause, newbs is filled, and clause is built in the accumulator acc.
818
    *)
819
    let rec mkExclClause deferral f acc =
820
      (* f is a formula that is true in the current satisfying assignment *)
821
      match lfGetType sort f with
822
      | OrF ->
823
          (* if f is true and a disjunction, then one of its disjuncts is true *)
824
          let f1 = lfGetDest1 sort f in
825
          let lf1 = fhtMustFind fht f1 in
826
          (* if the first disjunct f1 is true, then we need to add subformulas
827
             of f1 to newbs&clause *)
828
          if M.literal_status solver lf1 = M.LTRUE then mkExclClause deferral f1 acc
829
          else
830
            (* otherwise f2 must be true *)
831
            let f2 = lfGetDest2 sort f in
832
            let lf2 = fhtMustFind fht f2 in
833
            assert (M.literal_status solver lf2 = M.LTRUE);
834
            mkExclClause deferral f2 acc
835
      | AndF ->
836
          (* if the true f is a conjuction, then both conjunctions must be true *)
837
          let f1 = lfGetDest1 sort f in
838
          let lf1 = fhtMustFind fht f1 in
839
          assert (M.literal_status solver lf1 = M.LTRUE);
840
          let acc1 = mkExclClause deferral f1 acc in
841
          let f2 = lfGetDest2 sort f in
842
          let lf2 = fhtMustFind fht f2 in
843
          assert (M.literal_status solver lf2 = M.LTRUE);
844
          mkExclClause deferral f2 acc1
845
      | MuF
846
      | NuF ->
847
         let f1 = lfGetDest1 sort f in
848
         mkExclClause deferral f1 acc
849
      | _ ->
850
         (* if f is a trivial formula or modality, then add it ... *)
851
         (* ... to newbs *)
852
         bsetAdd newbs f;
853
         let defercandidate = lfGetDeferral sort f in
854
         (if (defercandidate != (Hashtbl.hash "ε") &&
855
                (refocusing || deferral = defercandidate)) then
856
            bsetAdd newdefer f);
857
         (* ... and to the new clause *)
858
         (M.neg_lit (fhtMustFind fht f))::acc
859
    in
860
    let init_clause f acc =
861
      let deferral =
862
        if bsetMem deferralS f then (
863
          lfGetDeferral sort f)
864
        else
865
          (Hashtbl.hash "ε")
866
      in
867
      mkExclClause deferral f acc
868
    in
869
    let clause = bsetFold init_clause bs [] in
870
    let okay = M.add_clause solver clause in
871
    assert (okay);
872
    Some (sort, newbs, newdefer)
873

    
874
let newState sort bs defer =
875
  let (func, sl) = !sortTable.(sort) in
876
  let producer = CoAlgLogics.getExpandingFunctionProducer func in
877
  let exp = producer sort bs defer sl in
878
  stateMake sort bs defer exp
879

    
880
let insertState parent sort bs defer =
881
  let child =
882
    match graphFindState sort (bs, defer) with
883
    | None ->
884
        let s = newState sort bs defer in
885
        graphInsertState sort (bs, defer) s;
886
        queueInsertState s;
887
        s
888
    | Some s -> s
889
  in
890
  coreAddChild parent child;
891
  stateAddParent child parent
892

    
893
let expandCore core =
894
  match getNextState core with
895
  | Some (sort, bs, defer) ->
896
      insertState core sort bs defer;
897
      queueInsertCore core
898
  | None ->
899
      let isUnsat = List.for_all (fun s -> stateGetStatus s = Unsat) (coreGetChildren core) in
900
      if isUnsat then propagateUnsat [UCore (core, false)]
901
      else coreSetStatus core Open
902

    
903

    
904
let insertCore sort bs defer =
905
  match graphFindCore sort (bs, defer) with
906
  | None ->
907
     let c = newCore sort bs defer in
908
     graphInsertCore sort (bs, defer) c;
909
     queueInsertCore c;
910
     c
911
  | Some c -> c
912

    
913
let insertRule state dep chldrn =
914
  let chldrn = listFromLazylist chldrn in
915
  let insert (isUns, acc) (sort, bs, defer) =
916
    let bs1 = bsetAddTBox sort bs in
917
    let core = insertCore sort bs1 defer in
918
    let isUns1 = if coreGetStatus core = Unsat then isUns else false in
919
    (isUns1, core::acc)
920
  in
921
  let (isUnsat, children) = List.fold_left insert (true, []) chldrn in
922
  let idx = stateAddRule state dep (List.rev children) in
923
  List.iter (fun c -> coreAddParent c state idx) children;
924
  if isUnsat then begin
925
    propagateUnsat [UState (state, Some idx)];
926
    false
927
  end else true
928

    
929
let rec insertAllRules state = function
930
  | [] -> true
931
  | (dep, chldrn)::tl ->
932
      let notUnsat = insertRule state dep chldrn in
933
      if notUnsat then insertAllRules state tl else false
934

    
935
let expandState state =
936
  match stateNextRule state with
937
  | MultipleElements rules ->
938
      let notUnsat = insertAllRules state rules in
939
      if notUnsat then stateSetStatus state Open
940
  | SingleElement (dep, chldrn) ->
941
      let notUnsat = insertRule state dep chldrn in
942
      if notUnsat then queueInsertState state else ()
943
  | NoMoreElements -> stateSetStatus state Open
944

    
945

    
946
let expandCnstr cset =
947
  let nht = nhtInit () in
948
  let mkCores f =
949
    let (sort, lf) as nom = atFormulaGetNominal f in
950
    let nomset =
951
      match nhtFind nht nom with
952
      | Some ns -> ns
953
      | None ->
954
          let cset1 = csetCopy cset in
955
          csetRemDot cset1;
956
          let bs = csetAddTBox sort cset1 in
957
          bsetAdd bs lf;
958
          nhtAdd nht nom bs;
959
          bs
960
    in
961
    bsetAdd nomset (atFormulaGetSubformula f)
962
  in
963
  csetIter cset mkCores;
964
  let inCores (sort, _) bs (isUns, acc) =
965
    let core = insertCore sort bs bs in (* TODO: think of deferral / μ stuff here *)
966
    coreAddConstraintParent core cset;
967
    (coreGetStatus core = Unsat || isUns, core::acc)
968
  in
969
  let (isUnsat, children) = nhtFold inCores nht (false, []) in
970
  if isUnsat then propagateUnsat [UCnstr cset]
971
  else
972
    match graphFindCnstr cset with
973
    | Some (UnexpandedC parents) -> graphReplaceCnstr cset (OpenC parents)
974
    | _ -> assert false
975

    
976

    
977
(*****************************************************************************)
978
(*                           The Main Loop                                   *)
979
(*****************************************************************************)
980

    
981
let expandNodesLoop (recursiveAction: unit -> unit) =
982
  match queueGetElement () with
983
  | QState state ->
984
      if stateGetStatus state = Expandable then begin
985
        expandState state;
986
        if doNominalPropagation () then begin
987
          propagateNominals ();
988
          if doSatPropagation () then (propagateUnsatMu (); propagateSatMu ())
989
        end else ()
990
      end else ();
991
      recursiveAction ()
992
  | QCore core ->
993
      if coreGetStatus core = Expandable then begin
994
        expandCore core;
995
        if doNominalPropagation () then begin
996
          propagateNominals ();
997
          if doSatPropagation () then (propagateUnsatMu (); propagateSatMu ())
998
        end else ()
999
      end else ();
1000
      recursiveAction ()
1001
  | QCnstr cset ->
1002
      expandCnstr cset;
1003
      recursiveAction ()
1004
  | QEmpty -> ()
1005

    
1006
let runReasonerStep () =
1007
  let void () = () in
1008
  expandNodesLoop void; (* expand at most one node *)
1009
  (* if this emptied the queue *)
1010
  if queueIsEmpty () then begin
1011
    (* then check whether the nominals would add further queue elements *)
1012
    print_endline "Propagating nominals...";
1013
    propagateNominals ()
1014
  end else () (* else: the next step would be to expand another node *)
1015

    
1016
let rec buildGraphLoop () =
1017
  let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in
1018
  expandNodesFurther (); (* expand as many queue elements as possible *)
1019
  propagateNominals ();
1020
  (* if propagating nominals added some more queue members, do all again.. *)
1021
  if queueIsEmpty () then () else buildGraphLoop ()
1022

    
1023
let initReasoner sorts nomTable tbox sf =
1024
  sortTable := Array.copy sorts;
1025
  let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in
1026
  let sort = fst sf in
1027
  let bs1 = bsetAddTBox sort bs in
1028
  let deferrals = bsetMakeRealEmpty() in
1029
  let markDeferral f =
1030
    if (Hashtbl.hash "ε") != (lfGetDeferral sort f) then (
1031
      bsetAdd deferrals f;)
1032
  in
1033
  bsetIter markDeferral bs;
1034
  graphInit ();
1035
  queueInit ();
1036
  let root = insertCore sort bs1 deferrals in
1037
  graphAddRoot root
1038

    
1039
let isRootSat () =
1040
  match coreGetStatus (graphGetRoot ()) with
1041
  | Expandable -> None
1042
  | Unsat -> Some false
1043
  | Sat -> Some true
1044
  | Open -> if (queueIsEmpty()) then Some true else None
1045

    
1046
let reasonerFinished () =
1047
  match coreGetStatus (graphGetRoot ()) with
1048
  | Expandable -> false
1049
  | Unsat
1050
  | Sat  -> true
1051
  | Open -> queueIsEmpty ()
1052

    
1053

    
1054
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
1055
    @param verbose An optional switch which determines
1056
    whether the procedure shall print some information on the standard output.
1057
    The default is false.
1058
    @param sorts An array mapping each sort (represented as an integer)
1059
    to a functor and a list of sorts which are the arguments of the functor.
1060
    @param nomTable A partial function mapping nominals (represented as strings)
1061
    to their sorts.
1062
    @param tbox A list of sorted formulae.
1063
    @param sf A sorted formula.
1064
    @return True if sf is satisfiable wrt tbox, false otherwise.
1065
 *)
1066

    
1067
let isSat ?(verbose = false) sorts nomTable tbox sf =
1068
  let start = if verbose then Unix.gettimeofday () else 0. in
1069
  initReasoner sorts nomTable tbox sf;
1070
  let sat =
1071
    try
1072
      buildGraphLoop ();
1073
      propagateUnsatMu ();
1074
      (* get whether the root is satisfiable *)
1075
      (* we know that the reasoner finished, so the value is there, *)
1076
      (* i.e. isRootSat() will give a "Some x" and not "None" *)
1077
      CU.fromSome (isRootSat())
1078
    with CoAlg_finished res -> res
1079
  in
1080
  (* print some statistics *)
1081
  if verbose then
1082
    let stop = Unix.gettimeofday () in
1083
    let addup lst = List.fold_left (fun acc sf -> acc + (CoAlgFormula.sizeSortedFormula sf)) 0 lst in
1084
    print_newline ();
1085
    print_endline ("Query: " ^ (CoAlgFormula.exportQuery tbox sf));
1086
    let size = (CoAlgFormula.sizeSortedFormula sf) + (addup tbox) in
1087
    print_endline ("Added Size: " ^ (string_of_int size));
1088
    (*
1089
    print_endline ("Negation Normal Form: " ^ (CoAlgFormula.exportQuery tbox1 sf1));
1090
    let nsize = (CoAlgFormula.sizeSortedFormula sf1) + (addup tbox1) in
1091
    print_endline ("Added Size: " ^ (string_of_int nsize));
1092
    *)
1093
    print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable.");
1094
    print_endline ("Time: " ^ (string_of_float (stop -. start)));
1095
    print_endline ("Generated states: " ^ (string_of_int (graphSizeState ())));
1096
    print_endline ("Generated cores: " ^ (string_of_int (graphSizeCore ())));
1097
    print_endline ("Generated constraints: " ^ (string_of_int (graphSizeCnstr ())));
1098
    print_newline ()
1099
  else ();
1100
  sat