Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ 4f821479

History | View | Annotate | Download (38.2 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
  setPropagationCounter ((setLengthCore setCores) -
176
                           (setLengthCore setFinishingCores));
177

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

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

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

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

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

    
249

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

    
260

    
261
(*****************************************************************************)
262
(*                     Propagation of Unsatisfiability                       *)
263
(*****************************************************************************)
264

    
265
let isConstraintUnsat cset =
266
  match graphFindCnstr cset with
267
  | None -> assert false
268
  | Some UnsatC -> true
269
  | _ -> false
270

    
271
let fhtMustFind fht f =
272
  match fhtFind fht f with
273
  | Some l -> l
274
  | None -> assert false
275

    
276
let lhtMustFind lht l =
277
  match lhtFind lht l with
278
  | Some f -> f
279
  | None -> assert false
280

    
281

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

    
407
let propagateUnsatMu () =
408
  let setFinishingStates = setEmptyState () in
409
  let setFinishingCores = setEmptyCore () in
410
  let setStates = setEmptyState () in
411
  let setCores = setEmptyCore () in
412
  let emptySet = bsetMakeRealEmpty () in
413

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

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

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

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

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

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

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

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

    
535

    
536
(*****************************************************************************)
537
(*                   Propagation of Nominal Constraints                      *)
538
(*****************************************************************************)
539

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

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

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

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

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

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

    
672

    
673
(*****************************************************************************)
674
(*                           Node Expansions                                 *)
675
(*****************************************************************************)
676

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

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

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

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

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

    
763
            f = μ X . φ   |---> lf
764
            φ[X |-> f]    |---> lf1
765

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

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

    
813
            newbs = l_1 /\ ... /\ l_n
814

    
815
       then we can get essentially different satisfying assignments of bs by
816
       adding another clause
817

    
818
            clause = ¬ newbs = ¬l_1 \/ ... \/ ¬l_n
819

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

    
878
let newState sort bs defer =
879
  let (func, sl) = !sortTable.(sort) in
880
  let producer = CoAlgLogics.getExpandingFunctionProducer func in
881
  let exp = producer sort bs defer sl in
882
  stateMake sort bs defer exp
883

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

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

    
907

    
908
let insertCore sort bs defer =
909
  match graphFindCore sort (bs, defer) with
910
  | None ->
911
     let c = newCore sort bs defer in
912
     graphInsertCore sort (bs, defer) c;
913
     queueInsertCore c;
914
     c
915
  | Some c -> c
916

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

    
933
let rec insertAllRules state = function
934
  | [] -> true
935
  | (dep, chldrn)::tl ->
936
      let notUnsat = insertRule state dep chldrn in
937
      if notUnsat then insertAllRules state tl else false
938

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

    
949

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

    
980

    
981
(*****************************************************************************)
982
(*                           The Main Loop                                   *)
983
(*****************************************************************************)
984

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

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

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

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

    
1043
let isRootSat () =
1044
  match coreGetStatus (graphGetRoot ()) with
1045
  | Expandable -> None
1046
  | Unsat -> Some false
1047
  | Sat -> Some true
1048
  | Open -> if (queueIsEmpty()) then Some true else None
1049

    
1050
let reasonerFinished () =
1051
  match coreGetStatus (graphGetRoot ()) with
1052
  | Expandable -> false
1053
  | Unsat
1054
  | Sat  -> true
1055
  | Open -> queueIsEmpty ()
1056

    
1057

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

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