Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgReasoner.ml @ 0debe698

History | View | Annotate | Download (38.9 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 Some 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 bsetCompare (stateGetDeferral state) emptySet == 0
442
      then begin
443
        setAddState setFinishingStates state
444
      end
445
      else ()
446

    
447
  and coreCollector core =
448
    match coreGetStatus core with
449
    | Unsat -> ()
450
    | Expandable
451
    | Sat ->
452
       setAddCore setCores core;
453
      setAddCore setFinishingCores core
454
    | Open ->
455
       setAddCore setCores core;
456
      if bsetCompare (coreGetDeferral core) emptySet == 0
457
      then begin
458
        setAddCore setFinishingCores core
459
      end
460
      else ()
461
  in
462
  graphIterStates stateCollector;
463
  graphIterCores coreCollector;
464

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

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

    
496
    and visitParentCores (state : state) : unit =
497
      if setMemState setUnsatStates state
498
      then begin
499
        setRemoveState setUnsatStates state;
500
        let verifyParent core =
501
          let acceptable =
502
            List.exists (fun (state : state) -> not (setMemState setUnsatStates state) ||
503
                                                  stateGetStatus state == Sat)
504
              (coreGetChildren core)
505
          in
506
          if acceptable
507
          then visitParentStates core
508
        in
509
        List.iter verifyParent (stateGetParents state)
510
      end
511
    in
512

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

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

    
541
    if (setLengthState setPrevUnsatStates) = (setLengthState setUnsatStates) &&
542
      (setLengthCore setPrevUnsatCores) = (setLengthCore setUnsatCores)
543
    then begin
544
        setIterState (fun state -> stateSetStatus state Unsat) setUnsatStates;
545
        setIterCore (fun core -> propagateUnsat [UCore (core, false)]) setUnsatCores;
546
      end else
547
      fixpointstep setUnsatStates setUnsatCores
548
  in
549
  fixpointstep (setEmptyState ()) (setEmptyCore ())
550

    
551

    
552
(*****************************************************************************)
553
(*                   Propagation of Nominal Constraints                      *)
554
(*****************************************************************************)
555

    
556
let extractAts sort bs =
557
  let ats = csetMake () in
558
  let procNom nom f =
559
    match lfGetType sort f with
560
    | AndF
561
    | OrF -> ()
562
    | TrueFalseF
563
    | AtF -> ()
564
    | _ -> csetAdd ats (lfGetAt (sort, nom) f)
565
  in
566
  let getAts f =
567
    match lfGetType sort f with
568
    | AtF -> csetAdd ats (lfToAt sort f)
569
    | NomF -> bsetIter (fun f1 -> procNom f f1) bs
570
    | _ -> ()
571
  in
572
  bsetIter getAts bs;
573
  ats
574

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

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

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

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

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

    
688

    
689
(*****************************************************************************)
690
(*                           Node Expansions                                 *)
691
(*****************************************************************************)
692

    
693
let getLit sort fht solver f =
694
  match fhtFind fht f with
695
  | Some lit -> lit
696
  | None ->
697
      let var = M.new_variable solver in
698
      let lit = M.var_to_lit var true in
699
      fhtAdd fht f lit;
700
      let () =
701
        match lfGetNeg sort f with
702
        | None -> ()
703
        | Some nf ->
704
            let nlit = M.neg_lit lit in
705
            fhtAdd fht nf nlit;
706
      in
707
      lit
708

    
709
let newCore sort bs defer =
710
  (* when creating a now core from a set of formulas bs
711
        bs = { x_1, ...., x_n }
712
           = "x_1 /\ .... /\ x_n"
713
     Then we do this by:
714

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

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

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

    
779
            f = μ X . φ   |---> lf
780
            φ[X |-> f]    |---> lf1
781

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

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

    
829
            newbs = l_1 /\ ... /\ l_n
830

    
831
       then we can get essentially different satisfying assignments of bs by
832
       adding another clause
833

    
834
            clause = ¬ newbs = ¬l_1 \/ ... \/ ¬l_n
835

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

    
894
let newState sort bs defer =
895
  let (func, sl) = !sortTable.(sort) in
896
  let producer = CoAlgLogics.getExpandingFunctionProducer func in
897
  let exp = producer sort bs defer sl in
898
  stateMake sort bs defer exp
899

    
900
let insertState parent sort bs defer =
901
  let child =
902
    match graphFindState sort (bs, defer) with
903
    | None ->
904
        let s = newState sort bs defer in
905
        graphInsertState sort (bs, defer) s;
906
        queueInsertState s;
907
        s
908
    | Some s -> s
909
  in
910
  coreAddChild parent child;
911
  stateAddParent child parent
912

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

    
926

    
927
let insertCore sort bs defer =
928
  match graphFindCore sort (bs, defer) with
929
  | None ->
930
     let c = newCore sort bs defer in
931
     graphInsertCore sort (bs, defer) c;
932
     queueInsertCore c;
933
     c
934
  | Some c -> c
935

    
936
let insertRule state dep chldrn =
937
  let chldrn = listFromLazylist chldrn in
938
  let insert (isUns, acc) (sort, bs, defer) =
939
    let bs1 = bsetAddTBox sort bs in
940
    let core = insertCore sort bs1 defer in
941
    let isUns1 = if coreGetStatus core = Unsat then isUns else false in
942
    (isUns1, core::acc)
943
  in
944
  let (isUnsat, children) = List.fold_left insert (true, []) chldrn in
945
  let idx = stateAddRule state dep (List.rev children) in
946
  List.iter (fun c -> coreAddParent c state idx) children;
947
  if isUnsat then begin
948
    propagateUnsat [UState (state, Some idx)];
949
    false
950
  end else true
951

    
952
let rec insertAllRules state = function
953
  | [] -> true
954
  | (dep, chldrn)::tl ->
955
      let notUnsat = insertRule state dep chldrn in
956
      if notUnsat then insertAllRules state tl else false
957

    
958
let expandState state =
959
  match stateNextRule state with
960
  | MultipleElements rules ->
961
      let notUnsat = insertAllRules state rules in
962
      if notUnsat then stateSetStatus state Open
963
  | SingleElement (dep, chldrn) ->
964
      let notUnsat = insertRule state dep chldrn in
965
      if notUnsat then queueInsertState state else ()
966
  | NoMoreElements -> stateSetStatus state Open
967

    
968

    
969
let expandCnstr cset =
970
  let nht = nhtInit () in
971
  let mkCores f =
972
    let (sort, lf) as nom = atFormulaGetNominal f in
973
    let nomset =
974
      match nhtFind nht nom with
975
      | Some ns -> ns
976
      | None ->
977
          let cset1 = csetCopy cset in
978
          csetRemDot cset1;
979
          let bs = csetAddTBox sort cset1 in
980
          bsetAdd bs lf;
981
          nhtAdd nht nom bs;
982
          bs
983
    in
984
    bsetAdd nomset (atFormulaGetSubformula f)
985
  in
986
  csetIter cset mkCores;
987
  let inCores (sort, _) bs (isUns, acc) =
988
    let core = insertCore sort bs bs in (* TODO: think of deferral / μ stuff here *)
989
    coreAddConstraintParent core cset;
990
    (coreGetStatus core = Unsat || isUns, core::acc)
991
  in
992
  let (isUnsat, children) = nhtFold inCores nht (false, []) in
993
  if isUnsat then propagateUnsat [UCnstr cset]
994
  else
995
    match graphFindCnstr cset with
996
    | Some (UnexpandedC parents) -> graphReplaceCnstr cset (OpenC parents)
997
    | _ -> assert false
998

    
999

    
1000
(*****************************************************************************)
1001
(*                           The Main Loop                                   *)
1002
(*****************************************************************************)
1003

    
1004
let expandNodesLoop (recursiveAction: unit -> unit) =
1005
  match queueGetElement () with
1006
  | QState state ->
1007
      if stateGetStatus state = Expandable then begin
1008
        expandState state;
1009
        if doNominalPropagation () then begin
1010
          (* propagateNominals (); *)
1011
          if doSatPropagation () then (propagateUnsatMu (); propagateSatMu ())
1012
        end else ()
1013
      end else ();
1014
      recursiveAction ()
1015
  | QCore core ->
1016
      if coreGetStatus core = Expandable then begin
1017
        expandCore core;
1018
        if doNominalPropagation () then begin
1019
          (* propagateNominals (); *)
1020
          if doSatPropagation () then (propagateUnsatMu (); propagateSatMu ())
1021
        end else ()
1022
      end else ();
1023
      recursiveAction ()
1024
  | QCnstr cset ->
1025
      expandCnstr cset;
1026
      recursiveAction ()
1027
  | QEmpty -> ()
1028

    
1029
let runReasonerStep () =
1030
  let void () = () in
1031
  expandNodesLoop void; (* expand at most one node *)
1032
  (* if this emptied the queue *)
1033
  if queueIsEmpty () then begin
1034
    (* then check whether the nominals would add further queue elements *)
1035
    (* print_endline "Propagating nominals..."; *)
1036
    (* propagateNominals () *)
1037
  end else () (* else: the next step would be to expand another node *)
1038

    
1039
let rec buildGraphLoop () =
1040
  let rec expandNodesFurther () = expandNodesLoop expandNodesFurther in
1041
  expandNodesFurther (); (* expand as many queue elements as possible *)
1042
  (* propagateNominals (); *)
1043
  (* if propagating nominals added some more queue members, do all again.. *)
1044
  if queueIsEmpty () then () else buildGraphLoop ()
1045

    
1046
let initReasoner sorts nomTable tbox sf =
1047
  sortTable := Array.copy sorts;
1048
  let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in
1049
  let sort = fst sf in
1050
  let bs1 = bsetAddTBox sort bs in
1051
  let deferrals = bsetMakeRealEmpty() in
1052
  let markDeferral f =
1053
    if (Hashtbl.hash "ε") != (lfGetDeferral sort f) then (
1054
      bsetAdd deferrals f;)
1055
  in
1056
  bsetIter markDeferral bs;
1057
  graphInit ();
1058
  queueInit ();
1059
  let root = insertCore sort bs1 deferrals in
1060
  graphAddRoot root
1061

    
1062
let isRootSat () =
1063
  match coreGetStatus (graphGetRoot ()) with
1064
  | Expandable -> None
1065
  | Unsat -> Some false
1066
  | Sat -> Some true
1067
  | Open -> if (queueIsEmpty()) then Some true else None
1068

    
1069
let reasonerFinished () =
1070
  match coreGetStatus (graphGetRoot ()) with
1071
  | Expandable -> false
1072
  | Unsat
1073
  | Sat  -> true
1074
  | Open -> queueIsEmpty ()
1075

    
1076

    
1077
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
1078
    @param verbose An optional switch which determines
1079
    whether the procedure shall print some information on the standard output.
1080
    The default is false.
1081
    @param sorts An array mapping each sort (represented as an integer)
1082
    to a functor and a list of sorts which are the arguments of the functor.
1083
    @param nomTable A partial function mapping nominals (represented as strings)
1084
    to their sorts.
1085
    @param tbox A list of sorted formulae.
1086
    @param sf A sorted formula.
1087
    @return True if sf is satisfiable wrt tbox, false otherwise.
1088
 *)
1089

    
1090
let isSat ?(verbose = false) sorts nomTable tbox sf =
1091
  let start = if verbose then Unix.gettimeofday () else 0. in
1092
  initReasoner sorts nomTable tbox sf;
1093
  let sat =
1094
    try
1095
      buildGraphLoop ();
1096
      propagateUnsatMu ();
1097
      (* get whether the root is satisfiable *)
1098
      (* we know that the reasoner finished, so the value is there, *)
1099
      (* i.e. isRootSat() will give a "Some x" and not "None" *)
1100
      CU.fromSome (isRootSat())
1101
    with CoAlg_finished res -> res
1102
  in
1103
  (* print some statistics *)
1104
  if verbose then
1105
    let stop = Unix.gettimeofday () in
1106
    let addup lst = List.fold_left (fun acc sf -> acc + (CoAlgFormula.sizeSortedFormula sf)) 0 lst in
1107
    print_newline ();
1108
    print_endline ("Query: " ^ (CoAlgFormula.exportQuery tbox sf));
1109
    let size = (CoAlgFormula.sizeSortedFormula sf) + (addup tbox) in
1110
    print_endline ("Added Size: " ^ (string_of_int size));
1111
    (*
1112
    print_endline ("Negation Normal Form: " ^ (CoAlgFormula.exportQuery tbox1 sf1));
1113
    let nsize = (CoAlgFormula.sizeSortedFormula sf1) + (addup tbox1) in
1114
    print_endline ("Added Size: " ^ (string_of_int nsize));
1115
    *)
1116
    print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable.");
1117
    print_endline ("Time: " ^ (string_of_float (stop -. start)));
1118
    print_endline ("Generated states: " ^ (string_of_int (graphSizeState ())));
1119
    print_endline ("Generated cores: " ^ (string_of_int (graphSizeCore ())));
1120
    print_endline ("Generated constraints: " ^ (string_of_int (graphSizeCnstr ())));
1121
    print_newline ()
1122
  else ();
1123
  sat